41777

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

25991

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 
*)


5 

58889

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

25991

7 


8 
theory Foundation


9 
imports IFOLP


10 
begin


11 

61337

12 
schematic_goal "?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 

60770

21 
text \<open>A form of conjelimination\<close>

61337

22 
schematic_goal

25991

23 
assumes "p : A & B"


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


25 
shows "?p : C"

41526

26 
apply (rule assms)

25991

27 
apply (rule conjunct1)

41526

28 
apply (rule assms)

25991

29 
apply (rule conjunct2)

41526

30 
apply (rule assms)

25991

31 
done


32 

61337

33 
schematic_goal

25991

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


35 
shows "?p : B  ~B"

41526

36 
apply (rule assms)

25991

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 

61337

51 
schematic_goal

25991

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


53 
shows "?p : B  ~B"

41526

54 
apply (rule assms)

25991

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 

61337

66 
schematic_goal

25991

67 
assumes "p : A  ~A"


68 
and "q : ~ ~A"


69 
shows "?p : A"


70 
apply (rule disjE)

41526

71 
apply (rule assms)

25991

72 
apply assumption


73 
apply (rule FalseE)


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

41526

75 
apply (rule assms)

25991

76 
apply assumption


77 
done


78 


79 


80 
subsection "Examples with quantifiers"


81 

61337

82 
schematic_goal

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)

41526

87 
apply (rule assms [THEN spec])

25991

88 
done


89 

61337

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

25991

91 
apply (rule allI)


92 
apply (rule exI)


93 
apply (rule refl)


94 
done


95 

61337

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

25991

97 
apply (rule exI)


98 
apply (rule allI)


99 
apply (rule refl)?


100 
oops


101 

60770

102 
text \<open>Parallel lifting example.\<close>

61337

103 
schematic_goal "?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 

61337

111 
schematic_goal

25991

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


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


114 
apply (rule conjE)

41526

115 
apply (rule assms)

25991

116 
apply (rule exE)


117 
apply assumption


118 
apply (rule exI)


119 
apply (rule conjI)


120 
apply assumption


121 
apply assumption


122 
done


123 

60770

124 
text \<open>A bigger demonstration of quantifiers  not in the paper.\<close>

61337

125 
schematic_goal "?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
