25991

1 
(* Title: FOLP/ex/Foundation.ML


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 
*)


5 


6 
header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"


7 


8 
theory Foundation


9 
imports IFOLP


10 
begin


11 

36319

12 
schematic_lemma "?p : A&B > (C>A&C)"

25991

13 
apply (rule impI)


14 
apply (rule impI)


15 
apply (rule conjI)


16 
prefer 2 apply assumption


17 
apply (rule conjunct1)


18 
apply assumption


19 
done


20 


21 
text {*A form of conjelimination*}

36319

22 
schematic_lemma

25991

23 
assumes "p : A & B"


24 
and "!!x y. x : A ==> y : B ==> f(x, y) : C"


25 
shows "?p : C"


26 
apply (rule prems)


27 
apply (rule conjunct1)


28 
apply (rule prems)


29 
apply (rule conjunct2)


30 
apply (rule prems)


31 
done


32 

36319

33 
schematic_lemma

25991

34 
assumes "!!A x. x : ~ ~A ==> cla(x) : A"


35 
shows "?p : B  ~B"


36 
apply (rule prems)


37 
apply (rule notI)


38 
apply (rule_tac P = "~B" in notE)


39 
apply (rule_tac [2] notI)


40 
apply (rule_tac [2] P = "B  ~B" in notE)


41 
prefer 2 apply assumption


42 
apply (rule_tac [2] disjI1)


43 
prefer 2 apply assumption


44 
apply (rule notI)


45 
apply (rule_tac P = "B  ~B" in notE)


46 
apply assumption


47 
apply (rule disjI2)


48 
apply assumption


49 
done


50 

36319

51 
schematic_lemma

25991

52 
assumes "!!A x. x : ~ ~A ==> cla(x) : A"


53 
shows "?p : B  ~B"


54 
apply (rule prems)


55 
apply (rule notI)


56 
apply (rule notE)


57 
apply (rule_tac [2] notI)


58 
apply (erule_tac [2] notE)


59 
apply (erule_tac [2] disjI1)


60 
apply (rule notI)


61 
apply (erule notE)


62 
apply (erule disjI2)


63 
done


64 


65 

36319

66 
schematic_lemma

25991

67 
assumes "p : A  ~A"


68 
and "q : ~ ~A"


69 
shows "?p : A"


70 
apply (rule disjE)


71 
apply (rule prems)


72 
apply assumption


73 
apply (rule FalseE)


74 
apply (rule_tac P = "~A" in notE)


75 
apply (rule prems)


76 
apply assumption


77 
done


78 


79 


80 
subsection "Examples with quantifiers"


81 

36319

82 
schematic_lemma

25991

83 
assumes "p : ALL z. G(z)"


84 
shows "?p : ALL z. G(z)H(z)"


85 
apply (rule allI)


86 
apply (rule disjI1)


87 
apply (rule prems [THEN spec])


88 
done


89 

36319

90 
schematic_lemma "?p : ALL x. EX y. x=y"

25991

91 
apply (rule allI)


92 
apply (rule exI)


93 
apply (rule refl)


94 
done


95 

36319

96 
schematic_lemma "?p : EX y. ALL x. x=y"

25991

97 
apply (rule exI)


98 
apply (rule allI)


99 
apply (rule refl)?


100 
oops


101 


102 
text {* Parallel lifting example. *}

36319

103 
schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"

25991

104 
apply (rule exI allI)


105 
apply (rule exI allI)


106 
apply (rule exI allI)


107 
apply (rule exI allI)


108 
apply (rule exI allI)


109 
oops


110 

36319

111 
schematic_lemma

25991

112 
assumes "p : (EX z. F(z)) & B"


113 
shows "?p : EX z. F(z) & B"


114 
apply (rule conjE)


115 
apply (rule prems)


116 
apply (rule exE)


117 
apply assumption


118 
apply (rule exI)


119 
apply (rule conjI)


120 
apply assumption


121 
apply assumption


122 
done


123 


124 
text {* A bigger demonstration of quantifiers  not in the paper. *}

36319

125 
schematic_lemma "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"

25991

126 
apply (rule impI)


127 
apply (rule allI)


128 
apply (rule exE, assumption)


129 
apply (rule exI)


130 
apply (rule allE, assumption)


131 
apply assumption


132 
done


133 


134 
end
