author  wenzelm 
Mon, 11 Sep 2006 21:35:19 +0200  
changeset 20503  503ac4c5ef91 
parent 19736  d8d0f8f51d69 
child 21404  eb85850d3eb7 
permissions  rwrr 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

1 
(* Title: HOL/Induct/PropLog.thy 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
ID: $Id$ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Author: Tobias Nipkow 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

4 
Copyright 1994 TU Muenchen & University of Cambridge 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 
*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

7 
header {* Metatheory of propositional logic *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

8 

16417  9 
theory PropLog imports Main begin 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

10 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

11 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

12 
Datatype definition of propositional logic formulae and inductive 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

13 
definition of the propositional tautologies. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

14 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

15 
Inductive definition of propositional logic. Soundness and 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

16 
completeness w.r.t.\ truthtables. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

17 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

18 
Prove: If @{text "H = p"} then @{text "G = p"} where @{text "G \<in> 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

19 
Fin(H)"} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

20 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

21 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

22 
subsection {* The datatype of propositions *} 
5184  23 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
datatype 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

25 
'a pl = false  var 'a ("#_" [1000])  ">" "'a pl" "'a pl" (infixr 90) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

26 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

27 
subsection {* The proof system *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

28 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
consts 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

30 
thms :: "'a pl set => 'a pl set" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 

19736  32 
abbreviation 
33 
thm_rel :: "['a pl set, 'a pl] => bool" (infixl "" 50) 

34 
"H  p == p \<in> thms H" 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
inductive "thms(H)" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

37 
intros 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

38 
H [intro]: "p\<in>H ==> H  p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

39 
K: "H  p>q>p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

40 
S: "H  (p>q>r) > (p>q) > p>r" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

41 
DN: "H  ((p>false) > false) > p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

42 
MP: "[ H  p>q; H  p ] ==> H  q" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

43 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

44 
subsection {* The semantics *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

45 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

46 
subsubsection {* Semantics of propositional logic. *} 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

48 
consts 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

49 
eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

50 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

51 
primrec "tt[[false]] = False" 
18260  52 
"tt[[#v]] = (v \<in> tt)" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

53 
eval_imp: "tt[[p>q]] = (tt[[p]] > tt[[q]])" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

55 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

56 
A finite set of hypotheses from @{text t} and the @{text Var}s in 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

57 
@{text p}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

58 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

59 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

60 
consts 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

61 
hyps :: "['a pl, 'a set] => 'a pl set" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 

5184  63 
primrec 
10759  64 
"hyps false tt = {}" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

65 
"hyps (#v) tt = {if v \<in> tt then #v else #v>false}" 
10759  66 
"hyps (p>q) tt = hyps p tt Un hyps q tt" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

68 
subsubsection {* Logical consequence *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

69 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

70 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

71 
For every valuation, if all elements of @{text H} are true then so 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

72 
is @{text p}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

73 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

74 

19736  75 
definition 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

76 
sat :: "['a pl set, 'a pl] => bool" (infixl "=" 50) 
19736  77 
"H = p = (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) > tt[[p]])" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

78 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

79 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

80 
subsection {* Proof theory of propositional logic *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

81 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

82 
lemma thms_mono: "G<=H ==> thms(G) <= thms(H)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

83 
apply (unfold thms.defs ) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

84 
apply (rule lfp_mono) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

85 
apply (assumption  rule basic_monos)+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

86 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

87 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

88 
lemma thms_I: "H  p>p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

89 
 {*Called @{text I} for Identity Combinator, not for Introduction. *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

90 
by (best intro: thms.K thms.S thms.MP) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

91 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

92 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

93 
subsubsection {* Weakening, left and right *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

94 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

95 
lemma weaken_left: "[ G \<subseteq> H; Gp ] ==> Hp" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

96 
 {* Order of premises is convenient with @{text THEN} *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

97 
by (erule thms_mono [THEN subsetD]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

98 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

99 
lemmas weaken_left_insert = subset_insertI [THEN weaken_left] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

100 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

101 
lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

102 
lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

103 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

104 
lemma weaken_right: "H  q ==> H  p>q" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

105 
by (fast intro: thms.K thms.MP) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

106 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

107 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

108 
subsubsection {* The deduction theorem *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

109 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

110 
theorem deduction: "insert p H  q ==> H  p>q" 
18260  111 
apply (induct set: thms) 
112 
apply (fast intro: thms_I thms.H thms.K thms.S thms.DN 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

113 
thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

114 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

115 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

116 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

117 
subsubsection {* The cut rule *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

118 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

119 
lemmas cut = deduction [THEN thms.MP] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

120 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

121 
lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

122 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

123 
lemmas thms_notE = thms.MP [THEN thms_falseE, standard] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

124 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

125 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

126 
subsubsection {* Soundness of the rules wrt truthtable semantics *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

127 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

128 
theorem soundness: "H  p ==> H = p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

129 
apply (unfold sat_def) 
18260  130 
apply (induct set: thms) 
131 
apply auto 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

132 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

133 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

134 
subsection {* Completeness *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

135 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

136 
subsubsection {* Towards the completeness proof *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

137 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

138 
lemma false_imp: "H  p>false ==> H  p>q" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

139 
apply (rule deduction) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

140 
apply (erule weaken_left_insert [THEN thms_notE]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

141 
apply blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

142 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

143 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

144 
lemma imp_false: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

145 
"[ H  p; H  q>false ] ==> H  (p>q)>false" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

146 
apply (rule deduction) 
18260  147 
apply (blast intro: weaken_left_insert thms.MP thms.H) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

148 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

149 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

150 
lemma hyps_thms_if: "hyps p tt  (if tt[[p]] then p else p>false)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

151 
 {* Typical example of strengthening the induction statement. *} 
18260  152 
apply simp 
153 
apply (induct p) 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

154 
apply (simp_all add: thms_I thms.H) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

155 
apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

156 
imp_false false_imp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

157 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

158 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

159 
lemma sat_thms_p: "{} = p ==> hyps p tt  p" 
18260  160 
 {* Key lemma for completeness; yields a set of assumptions 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

161 
satisfying @{text p} *} 
18260  162 
apply (unfold sat_def) 
163 
apply (drule spec, erule mp [THEN if_P, THEN subst], 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

164 
rule_tac [2] hyps_thms_if, simp) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

165 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

166 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

167 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

168 
For proving certain theorems in our new propositional logic. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

169 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

170 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

171 
declare deduction [intro!] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

172 
declare thms.H [THEN thms.MP, intro] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

173 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

174 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

175 
The excluded middle in the form of an elimination rule. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

176 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

177 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

178 
lemma thms_excluded_middle: "H  (p>q) > ((p>false)>q) > q" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

179 
apply (rule deduction [THEN deduction]) 
18260  180 
apply (rule thms.DN [THEN thms.MP], best) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

181 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

182 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

183 
lemma thms_excluded_middle_rule: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

184 
"[ insert p H  q; insert (p>false) H  q ] ==> H  q" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

185 
 {* Hard to prove directly because it requires cuts *} 
18260  186 
by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

187 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

188 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

189 
subsection{* Completeness  lemmas for reducing the set of assumptions*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

190 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

191 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

192 
For the case @{prop "hyps p t  insert #v Y  p"} we also have @{prop 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

193 
"hyps p t  {#v} \<subseteq> hyps p (t{v})"}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

194 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

195 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

196 
lemma hyps_Diff: "hyps p (t{v}) <= insert (#v>false) ((hyps p t){#v})" 
18260  197 
by (induct p) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

198 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

199 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

200 
For the case @{prop "hyps p t  insert (#v > Fls) Y  p"} we also have 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

201 
@{prop "hyps p t{#v>Fls} \<subseteq> hyps p (insert v t)"}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

202 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

203 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

204 
lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t{#v>false})" 
18260  205 
by (induct p) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

206 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

207 
text {* Two lemmas for use with @{text weaken_left} *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

208 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

209 
lemma insert_Diff_same: "BC <= insert a (Binsert a C)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

210 
by fast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

211 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

212 
lemma insert_Diff_subset2: "insert a (B{c})  D <= insert a (Binsert c D)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

213 
by fast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

214 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

215 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

216 
The set @{term "hyps p t"} is finite, and elements have the form 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

217 
@{term "#v"} or @{term "#v>Fls"}. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

218 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

219 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

220 
lemma hyps_finite: "finite(hyps p t)" 
18260  221 
by (induct p) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

222 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

223 
lemma hyps_subset: "hyps p t <= (UN v. {#v, #v>false})" 
18260  224 
by (induct p) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

225 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

226 
lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

227 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

228 
subsubsection {* Completeness theorem *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

229 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

230 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

231 
Induction on the finite set of assumptions @{term "hyps p t0"}. We 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

232 
may repeatedly subtract assumptions until none are left! 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

233 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

234 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

235 
lemma completeness_0_lemma: 
18260  236 
"{} = p ==> \<forall>t. hyps p t  hyps p t0  p" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

237 
apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

238 
apply (simp add: sat_thms_p, safe) 
16563  239 
txt{*Case @{text"hyps p tinsert(#v,Y)  p"} *} 
18260  240 
apply (iprover intro: thms_excluded_middle_rule 
241 
insert_Diff_same [THEN weaken_left] 

242 
insert_Diff_subset2 [THEN weaken_left] 

16563  243 
hyps_Diff [THEN Diff_weaken_left]) 
244 
txt{*Case @{text"hyps p tinsert(#v > false,Y)  p"} *} 

18260  245 
apply (iprover intro: thms_excluded_middle_rule 
246 
insert_Diff_same [THEN weaken_left] 

247 
insert_Diff_subset2 [THEN weaken_left] 

16563  248 
hyps_insert [THEN Diff_weaken_left]) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

249 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

250 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

251 
text{*The base case for completeness*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

252 
lemma completeness_0: "{} = p ==> {}  p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

253 
apply (rule Diff_cancel [THEN subst]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

254 
apply (erule completeness_0_lemma [THEN spec]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

255 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

256 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

257 
text{*A semantic analogue of the Deduction Theorem*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

258 
lemma sat_imp: "insert p H = q ==> H = p>q" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

259 
by (unfold sat_def, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

260 

18260  261 
theorem completeness: "finite H ==> H = p ==> H  p" 
20503  262 
apply (induct arbitrary: p rule: finite_induct) 
16563  263 
apply (blast intro: completeness_0) 
17589  264 
apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP]) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

265 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

266 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

267 
theorem syntax_iff_semantics: "finite H ==> (H  p) = (H = p)" 
16563  268 
by (blast intro: soundness completeness) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

269 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

270 
end 