PropositionTutorial : THEORY BEGIN A, B, C: bool prop: THEOREM (A IMPLIES (B IMPLIES C)) AND (A IMPLIES B) AND A IMPLIES C END PropositionTutorial PropositionLogic : THEORY BEGIN % All lemmas in this THEORY PropositionLogic can be proven by using % only the strategies (flatten) and (split). P,Q,R,P1,P2,Q1,Q2 : bool simple : LEMMA P AND Q IMPLIES P OR Q simple1 : LEMMA (P IMPLIES Q) IMPLIES (Q IMPLIES R) IMPLIES (P IMPLIES R) pierces_law: LEMMA ((P IMPLIES Q) IMPLIES P) IMPLIES P distribution1 : LEMMA ((P1 OR P2) AND R) IFF ((P1 AND R) OR (P2 AND R)) distribution2 : LEMMA ((P1 OR P2) AND (Q1 OR Q2)) IFF ((P1 AND Q1) OR (P1 AND Q2) OR (P2 AND Q2) OR (P2 AND Q1)) de_morgan1: LEMMA (NOT (P OR Q)) IFF ((NOT P) AND (NOT Q)) % Now try to prove the next lemma using the strategy (prop). de_morgan2: LEMMA (NOT (P AND Q)) IFF ((NOT P) OR (NOT Q)) END PropositionLogic PredicateTutorial: THEORY BEGIN T : TYPE x, y, z: VAR T % Note that y and z are not used in this example. P, Q : [T -> bool] % Now also use strategies (skolem!), (inst?) pred_calc: THEOREM (FORALL x: P(x) AND Q(x)) IMPLIES (FORALL x: P(x)) AND (FORALL x: Q(x)) END PredicateTutorial Predicate[A:Type]: THEORY BEGIN IMPORTING PropositionLogic Pred1,Pred2,Pred3: VAR [A->bool] % The VAR keyword implies that in all % lemmas in this THEORY the predicates % Pred1, Pred2 and Pred3 will be % universally quantified automatically. Rel: VAR [A,A->bool] % All lemmas can be proven using the strategies (skolem), (skolem!), (inst), % (inst?), (flatten), (split) and (prop). simple2 : LEMMA (FORALL (x:A) : Pred1(x) IMPLIES Pred2(x) ) AND (FORALL (x:A) : Pred2(x) IMPLIES Pred3(x) ) IMPLIES (FORALL (x:A) : Pred1(x) IMPLIES Pred3(x) ) % The strategies (skolem!) and (flatten) can be invoked using the shortcut % (skosimp*). Try this! distribution2 : LEMMA (FORALL (x:A) : ((Pred1(x) OR Pred2(x)) AND Pred3(x))) IFF (FORALL (x:A) : ((Pred1(x) AND Pred3(x)) OR (Pred2(x)) AND Pred3(x))) forall_exists : LEMMA ((EXISTS (x:A) : (FORALL (y:A) : Rel(x,y))) IMPLIES (FORALL (y:A) : (EXISTS (x:A) : Rel(x,y)))) OR ((FORALL (y:A) : (EXISTS (x:A) : Rel(x,y))) IMPLIES (EXISTS (x:A) : (FORALL (y:A) : Rel(x,y)))) END Predicate DecisionsTutorial : THEORY BEGIN x,y,v: VAR real f: [real -> real] eq1 : THEOREM x = f(x) IMPLIES f(f(f(x))) = x g: [real, real -> real] % All theorems can be proven using (skolem!), (flatten) and (assert). eq2 : THEOREM x = f(y) IMPLIES g(f(y + 2 - 2), x + 2) = g(x, f(y) + 2) arith : THEOREM % Proved by decision procedures x < 2*y AND y < 3*v IMPLIES 3*x < 18*v badarith : CONJECTURE % Not proved; statement is false. x < 2*y AND y < 3*v IMPLIES 3*x < 17*v badarith1 : CONJECTURE % Not proved; statement true but non-linear. x<0 AND y<0 IMPLIES x*y>0 i,j,k: VAR int intarith : THEOREM % Proved by decision procedures 2*i < 5 AND i>1 IMPLIES i=2 badarith2 : CONJECTURE % Not proved; stmt. true of integers but not reals 2*x < 5 AND x>1 IMPLIES x=2 range : THEOREM % Proved by decision procedures i>0 AND i<3 IMPLIES i=1 OR i=2 END DecisionsTutorial HalfsTutorial : THEORY BEGIN % All lemmas and theorems can be proven by using (skosimp*), (skolem), % (skolem!), (inst), (inst?), (expand), (induct), (prop), (assert), (flatten), % (lift-if), (lemma). i, j, k: VAR nat half(i): RECURSIVE nat = (IF i=0 THEN 0 ELSIF i=1 THEN 0 ELSE half(i-2)+1 ENDIF) MEASURE (LAMBDA i:i) half_halves: THEOREM half(2*i) = i half_half: THEOREM half(2*half(2*i))=i END HalfsTutorial sum : THEORY BEGIN % All lemmas and theorems can be proven by using (skosimp*), (skolem), % (skolem!), (inst), (inst?), (expand), (induct), (prop), (assert), (flatten), % (lift-if). inf : LEMMA (FORALL (n:nat) : EXISTS (m:nat) : ( m > n)) n: VAR nat sum(n): RECURSIVE nat = (IF n = 0 THEN 0 ELSE n + sum(n - 1) ENDIF) MEASURE n closed_form: THEOREM sum(n) = (n * (n + 1))/2 f,g : VAR [nat -> nat] sum(f,n) : RECURSIVE nat = IF n = 0 THEN 0 ELSE f(n-1) + sum(f, n - 1) ENDIF MEASURE n sum_plus : LEMMA sum((lambda n : f(n) + g(n)), n) = sum(f,n) + sum(g,n) square(n) : nat = n * n sum_of_squares : LEMMA 6 * sum(square, n+1) = n * (n+1) * (2*n + 1) cube(n) : nat = n * n * n sum_of_cubes : LEMMA 4 * sum(cube, n+1) = n*n*(n+1)*(n+1) END sum Squares : THEORY BEGIN % The important strategies in this theory are (induct), (replace), (use) % and (lemma). % Look into the so-called prelude to find appropriate lemmas. r, s : VAR nonneg_real sqrts(r) : PRED[nonneg_real] = {s|s*s=r} even_or_odd : LEMMA FORALL (n:nat) : even?(n) XOR odd?(n) square_even_odd : LEMMA FORALL (n:nat) : (even?(n) IMPLIES even?(n*n)) AND (odd?(n) IMPLIES odd?(n*n)) sqrt2 : LEMMA % Hint: (lemma "NAT_induction") FORALL(n,m:nat) : n>0 IMPLIES NOT n*n = 2*m*m sqrt_unique : LEMMA FORALL(s1,s2 : (sqrts(r))) : s1 = s2 sqrt_nonempty_bounded : LEMMA nonempty?[nonneg_real]({s | s * s <= r}) AND bounded_above?({s | s * s <= r}) sqrt : [nonneg_real -> real] = LAMBDA r: lub({ s | s * s <= r }) sqrt_nonneg : LEMMA % Hint: (use "lub_lemma") sqrt(r) >= 0 JUDGEMENT sqrt HAS_TYPE [nonneg_real -> nonneg_real] sqrt_ub : LEMMA s * s <= r IMPLIES s <= sqrt(r) END Squares StampsTutorial : THEORY BEGIN i, three, five: VAR nat stamps : LEMMA (FORALL i: (EXISTS three, five: i + 8 = 3 * three + 5 * five)) END StampsTutorial