25991

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


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 
*)


6 


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


8 


9 
theory Foundation


10 
imports IFOLP


11 
begin


12 


13 
lemma "?p : A&B > (C>A&C)"


14 
apply (rule impI)


15 
apply (rule impI)


16 
apply (rule conjI)


17 
prefer 2 apply assumption


18 
apply (rule conjunct1)


19 
apply assumption


20 
done


21 


22 
text {*A form of conjelimination*}


23 
lemma


24 
assumes "p : A & B"


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


26 
shows "?p : C"


27 
apply (rule prems)


28 
apply (rule conjunct1)


29 
apply (rule prems)


30 
apply (rule conjunct2)


31 
apply (rule prems)


32 
done


33 


34 
lemma


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


36 
shows "?p : B  ~B"


37 
apply (rule prems)


38 
apply (rule notI)


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


40 
apply (rule_tac [2] notI)


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


42 
prefer 2 apply assumption


43 
apply (rule_tac [2] disjI1)


44 
prefer 2 apply assumption


45 
apply (rule notI)


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


47 
apply assumption


48 
apply (rule disjI2)


49 
apply assumption


50 
done


51 


52 
lemma


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


54 
shows "?p : B  ~B"


55 
apply (rule prems)


56 
apply (rule notI)


57 
apply (rule notE)


58 
apply (rule_tac [2] notI)


59 
apply (erule_tac [2] notE)


60 
apply (erule_tac [2] disjI1)


61 
apply (rule notI)


62 
apply (erule notE)


63 
apply (erule disjI2)


64 
done


65 


66 


67 
lemma


68 
assumes "p : A  ~A"


69 
and "q : ~ ~A"


70 
shows "?p : A"


71 
apply (rule disjE)


72 
apply (rule prems)


73 
apply assumption


74 
apply (rule FalseE)


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


76 
apply (rule prems)


77 
apply assumption


78 
done


79 


80 


81 
subsection "Examples with quantifiers"


82 


83 
lemma


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


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


86 
apply (rule allI)


87 
apply (rule disjI1)


88 
apply (rule prems [THEN spec])


89 
done


90 


91 
lemma "?p : ALL x. EX y. x=y"


92 
apply (rule allI)


93 
apply (rule exI)


94 
apply (rule refl)


95 
done


96 


97 
lemma "?p : EX y. ALL x. x=y"


98 
apply (rule exI)


99 
apply (rule allI)


100 
apply (rule refl)?


101 
oops


102 


103 
text {* Parallel lifting example. *}


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


105 
apply (rule exI allI)


106 
apply (rule exI allI)


107 
apply (rule exI allI)


108 
apply (rule exI allI)


109 
apply (rule exI allI)


110 
oops


111 


112 
lemma


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


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


115 
apply (rule conjE)


116 
apply (rule prems)


117 
apply (rule exE)


118 
apply assumption


119 
apply (rule exI)


120 
apply (rule conjI)


121 
apply assumption


122 
apply assumption


123 
done


124 


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


126 
lemma "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"


127 
apply (rule impI)


128 
apply (rule allI)


129 
apply (rule exE, assumption)


130 
apply (rule exI)


131 
apply (rule allE, assumption)


132 
apply assumption


133 
done


134 


135 
end
