author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46579  fa035a015ea8 
child 54711  15a642b9ffac 
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 
Author: Tobias Nipkow 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

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

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

5 

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

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

7 

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

9 

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

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

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

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

13 

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

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

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

16 

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

17 
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

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

19 
*} 
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 
subsection {* The datatype of propositions *} 
5184  22 

24824  23 
datatype 'a pl = 
24 
false  

25 
var 'a ("#_" [1000])  

26 
imp "'a pl" "'a pl" (infixr ">" 90) 

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

27 

46579  28 

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

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

30 

46579  31 
inductive thms :: "['a pl set, 'a pl] => bool" (infixl "" 50) 
23746  32 
for H :: "'a pl set" 
46579  33 
where 
34 
H: "p\<in>H ==> H  p" 

35 
 K: "H  p>q>p" 

36 
 S: "H  (p>q>r) > (p>q) > p>r" 

37 
 DN: "H  ((p>false) > false) > p" 

38 
 MP: "[ H  p>q; H  p ] ==> H  q" 

39 

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

40 

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

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

42 

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

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

44 

46579  45 
primrec eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100) 
46 
where 

47 
"tt[[false]] = False" 

48 
 "tt[[#v]] = (v \<in> tt)" 

49 
 eval_imp: "tt[[p>q]] = (tt[[p]] > tt[[q]])" 

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

50 

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

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

52 
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

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

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

55 

46579  56 
primrec hyps :: "['a pl, 'a set] => 'a pl set" 
57 
where 

10759  58 
"hyps false tt = {}" 
39246  59 
 "hyps (#v) tt = {if v \<in> tt then #v else #v>false}" 
60 
 "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

61 

46579  62 

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

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

64 

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

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

66 
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

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

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

69 

46579  70 
definition sat :: "['a pl set, 'a pl] => bool" (infixl "=" 50) 
71 
where "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

72 

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 
subsection {* Proof theory of propositional logic *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

75 

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

76 
lemma thms_mono: "G<=H ==> thms(G) <= thms(H)" 
23746  77 
apply (rule predicate1I) 
78 
apply (erule thms.induct) 

79 
apply (auto intro: thms.intros) 

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

80 
done 
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_I: "H  p>p" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

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

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

85 

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

86 

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

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

88 

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

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

90 
 {* Order of premises is convenient with @{text THEN} *} 
23746  91 
by (erule thms_mono [THEN predicate1D]) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

92 

46579  93 
lemma weaken_left_insert: "G  p \<Longrightarrow> insert a G  p" 
94 
by (rule weaken_left) (rule subset_insertI) 

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

95 

46579  96 
lemma weaken_left_Un1: "G  p \<Longrightarrow> G \<union> B  p" 
97 
by (rule weaken_left) (rule Un_upper1) 

98 

99 
lemma weaken_left_Un2: "G  p \<Longrightarrow> A \<union> G  p" 

100 
by (rule weaken_left) (rule Un_upper2) 

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

101 

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

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

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

104 

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

105 

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

106 
subsubsection {* The deduction theorem *} 
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 
theorem deduction: "insert p H  q ==> H  p>q" 
18260  109 
apply (induct set: thms) 
110 
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

111 
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

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

113 

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

114 

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

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

116 

46579  117 
lemma cut: "insert p H  q \<Longrightarrow> H  p \<Longrightarrow> H  q" 
118 
by (rule thms.MP) (rule deduction) 

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

119 

46579  120 
lemma thms_falseE: "H  false \<Longrightarrow> H  q" 
121 
by (rule thms.MP, rule thms.DN) (rule weaken_right) 

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

122 

46579  123 
lemma thms_notE: "H  p > false \<Longrightarrow> H  p \<Longrightarrow> H  q" 
124 
by (rule thms_falseE) (rule thms.MP) 

13075
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 

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

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

128 

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

129 
theorem soundness: "H  p ==> H = p" 
46579  130 
by (induct set: thms) (auto simp: sat_def) 
131 

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

132 

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

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

134 

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

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

136 

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

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

138 
apply (rule deduction) 
27034  139 
apply (metis H insert_iff weaken_left_insert thms_notE) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

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

141 

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

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

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

144 
apply (rule deduction) 
27034  145 
apply (metis H MP insert_iff weaken_left_insert) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

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

147 

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

148 
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

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

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

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

153 
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

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

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

156 

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

157 
lemma sat_thms_p: "{} = p ==> hyps p tt  p" 
18260  158 
 {* 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

159 
satisfying @{text p} *} 
18260  160 
apply (unfold sat_def) 
161 
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

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

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

164 

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

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

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

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

168 

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

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

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

171 

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

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

173 
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

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

175 

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

176 
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

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

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

180 

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

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

182 
"[ 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

183 
 {* Hard to prove directly because it requires cuts *} 
18260  184 
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

185 

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

186 

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

187 
subsection{* Completeness  lemmas for reducing the set of assumptions*} 
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 
text {* 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset

190 
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

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

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

193 

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

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

196 

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

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

198 
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

199 
@{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

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

201 

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

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

204 

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

205 
text {* Two lemmas for use with @{text weaken_left} *} 
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 
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

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

209 

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

210 
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

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

212 

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

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

214 
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

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

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

217 

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

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

220 

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

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

223 

46579  224 
lemma Diff_weaken_left: "A \<subseteq> C \<Longrightarrow> A  B  p \<Longrightarrow> C  B  p" 
225 
by (rule Diff_mono [OF _ subset_refl, THEN weaken_left]) 

226 

13075
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" 
46579  259 
by (auto simp: sat_def) 
13075
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 