author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5184  9b8547a9496a 
child 5223  4cb05273f764 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/pl.ML 
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 & Lawrence C Paulson 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1994 TU Muenchen & University of Cambridge 
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 
Soundness and completeness of propositional logic w.r.t. truthtables. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 

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

8 
Prove: If H=p then G=p where G:Fin(H) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

10 

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

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

12 

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

13 
(** Monotonicity **) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

14 
Goalw thms.defs "G<=H ==> thms(G) <= thms(H)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
by (rtac lfp_mono 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
by (REPEAT (ares_tac basic_monos 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
qed "thms_mono"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 

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

19 
(*Rule is called I for Identity Combinator, not for Introduction*) 
5069  20 
Goal "H  p>p"; 
4089  21 
by (best_tac (claset() addIs [thms.K,thms.S,thms.MP]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
qed "thms_I"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 

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

24 
(** Weakening, left and right **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 

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

26 
(* "[ G<=H; G  p ] ==> H  p" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
This order of premises is convenient with RS 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

29 
bind_thm ("weaken_left", (thms_mono RS subsetD)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 

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

31 
(* H  p ==> insert(a,H)  p *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 
val weaken_left_insert = subset_insertI RS weaken_left; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 

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

34 
val weaken_left_Un1 = Un_upper1 RS weaken_left; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 
val weaken_left_Un2 = Un_upper2 RS weaken_left; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

37 
Goal "H  q ==> H  p>q"; 
4089  38 
by (fast_tac (claset() addIs [thms.K,thms.MP]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
qed "weaken_right"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 

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

41 
(*The deduction theorem*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

42 
Goal "insert p H  q ==> H  p>q"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
by (etac thms.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
by (ALLGOALS 
4089  45 
(fast_tac (claset() addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
4161  46 
thms.S RS thms.MP RS thms.MP, weaken_right]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
qed "deduction"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 

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

49 

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

50 
(* "[ insert p H  q; H  p ] ==> H  q" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
The cut rule  not used 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

53 
val cut = deduction RS thms.MP; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 

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

55 
(* H  false ==> H  p *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
val thms_falseE = weaken_right RS (thms.DN RS thms.MP); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 

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

58 
(* [ H  p>false; H  p; q: pl ] ==> H  q *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

59 
bind_thm ("thms_notE", (thms.MP RS thms_falseE)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 

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

61 
(** The function eval **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 

5069  63 
Goalw [eval_def] "tt[false] = False"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

64 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

65 
qed "eval_false"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

66 

5069  67 
Goalw [eval_def] "tt[#v] = (v:tt)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

69 
qed "eval_var"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

70 

5069  71 
Goalw [eval_def] "tt[p>q] = (tt[p]>tt[q])"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

72 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 
qed "eval_imp"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 

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

75 
Addsimps [eval_false, eval_var, eval_imp]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 

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

77 
(*Soundness of the rules wrt truthtable semantics*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

78 
Goalw [sat_def] "H  p ==> H = p"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

79 
by (etac thms.induct 1); 
4089  80 
by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

81 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
qed "soundness"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 

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

84 
(*** Towards the completeness proof ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

85 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

86 
Goal "H  p>false ==> H  p>q"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

87 
by (rtac deduction 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

88 
by (etac (weaken_left_insert RS thms_notE) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

89 
by (rtac thms.H 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

90 
by (rtac insertI1 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

91 
qed "false_imp"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

92 

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

93 
val [premp,premq] = goal PropLog.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

94 
"[ H  p; H  q>false ] ==> H  (p>q)>false"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

95 
by (rtac deduction 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

96 
by (rtac (premq RS weaken_left_insert RS thms.MP) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

97 
by (rtac (thms.H RS thms.MP) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

98 
by (rtac insertI1 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

99 
by (rtac (premp RS weaken_left_insert) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

100 
qed "imp_false"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

101 

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

102 
(*This formulation is required for strong induction hypotheses*) 
5069  103 
Goal "hyps p tt  (if tt[p] then p else p>false)"; 
4831  104 
by (rtac (split_if RS iffD2) 1); 
5184  105 
by (induct_tac "p" 1); 
4089  106 
by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H]))); 
107 
by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 

4161  108 
weaken_right, imp_false] 
109 
addSEs [false_imp]) 1); 

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

110 
qed "hyps_thms_if"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

111 

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

112 
(*Key lemma for completeness; yields a set of assumptions satisfying p*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

113 
val [sat] = goalw PropLog.thy [sat_def] "{} = p ==> hyps p tt  p"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

114 
by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 
rtac hyps_thms_if 2); 
4161  116 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

117 
qed "sat_thms_p"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

118 

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

119 
(*For proving certain theorems in our new propositional logic*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

120 

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

121 
AddSIs [deduction]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

122 
AddIs [thms.H, thms.H RS thms.MP]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

123 

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

124 
(*The excluded middle in the form of an elimination rule*) 
5069  125 
Goal "H  (p>q) > ((p>false)>q) > q"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

126 
by (rtac (deduction RS deduction) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

127 
by (rtac (thms.DN RS thms.MP) 1); 
4089  128 
by (ALLGOALS (best_tac (claset() addSIs prems))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

129 
qed "thms_excluded_middle"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

130 

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

131 
(*Hard to prove directly because it requires cuts*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

132 
val prems = goal PropLog.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

133 
"[ insert p H  q; insert (p>false) H  q ] ==> H  q"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

134 
by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

135 
by (REPEAT (resolve_tac (prems@[deduction]) 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

136 
qed "thms_excluded_middle_rule"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

137 

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

138 
(*** Completeness  lemmas for reducing the set of assumptions ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

139 

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

140 
(*For the case hyps(p,t)insert(#v,Y)  p; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

141 
we also have hyps(p,t){#v} <= hyps(p, t{v}) *) 
5069  142 
Goal "hyps p (t{v}) <= insert (#v>false) ((hyps p t){#v})"; 
5184  143 
by (induct_tac "p" 1); 
4686  144 
by (ALLGOALS Simp_tac); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

145 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

146 
qed "hyps_Diff"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

147 

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

148 
(*For the case hyps(p,t)insert(#v > false,Y)  p; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

149 
we also have hyps(p,t){#v>false} <= hyps(p, insert(v,t)) *) 
5069  150 
Goal "hyps p (insert v t) <= insert (#v) (hyps p t{#v>false})"; 
5184  151 
by (induct_tac "p" 1); 
4686  152 
by (ALLGOALS Simp_tac); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

153 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

154 
qed "hyps_insert"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

155 

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

156 
(** Two lemmas for use with weaken_left **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

157 

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

158 
goal Set.thy "BC <= insert a (Binsert a C)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

159 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

160 
qed "insert_Diff_same"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

161 

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

162 
goal Set.thy "insert a (B{c})  D <= insert a (Binsert c D)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

163 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

164 
qed "insert_Diff_subset2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

165 

5069  166 
Goal "finite(hyps p t)"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

167 
by (induct_tac "p" 1); 
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

168 
by (ALLGOALS Asm_simp_tac); 
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

169 
qed "hyps_finite"; 
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

170 

5069  171 
Goal "hyps p t <= (UN v. {#v, #v>false})"; 
5184  172 
by (induct_tac "p" 1); 
4686  173 
by (ALLGOALS Simp_tac); 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

174 
by (Blast_tac 1); 
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

175 
qed "hyps_subset"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

176 

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

177 
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

178 

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

179 
(*Induction on the finite set of assumptions hyps(p,t0). 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

180 
We may repeatedly subtract assumptions until none are left!*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

181 
val [sat] = goal PropLog.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

182 
"{} = p ==> !t. hyps p t  hyps p t0  p"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

183 
by (rtac (hyps_subset RS (hyps_finite RS finite_subset_induct)) 1); 
4089  184 
by (simp_tac (simpset() addsimps [sat RS sat_thms_p]) 1); 
3724  185 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

186 
(*Case hyps(p,t)insert(#v,Y)  p *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

187 
by (rtac thms_excluded_middle_rule 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

188 
by (rtac (insert_Diff_same RS weaken_left) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

189 
by (etac spec 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

190 
by (rtac (insert_Diff_subset2 RS weaken_left) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

191 
by (rtac (hyps_Diff RS Diff_weaken_left) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

192 
by (etac spec 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

193 
(*Case hyps(p,t)insert(#v > false,Y)  p *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

194 
by (rtac thms_excluded_middle_rule 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

195 
by (rtac (insert_Diff_same RS weaken_left) 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

196 
by (etac spec 2); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

197 
by (rtac (insert_Diff_subset2 RS weaken_left) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

198 
by (rtac (hyps_insert RS Diff_weaken_left) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

199 
by (etac spec 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

200 
qed "completeness_0_lemma"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

201 

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

202 
(*The base case for completeness*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

203 
val [sat] = goal PropLog.thy "{} = p ==> {}  p"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

204 
by (rtac (Diff_cancel RS subst) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

205 
by (rtac (sat RS (completeness_0_lemma RS spec)) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

206 
qed "completeness_0"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

207 

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

208 
(*A semantic analogue of the Deduction Theorem*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

209 
Goalw [sat_def] "insert p H = q ==> H = p>q"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

210 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

211 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

212 
qed "sat_imp"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

213 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

214 
Goal "finite H ==> !p. H = p > H  p"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

215 
by (etac finite_induct 1); 
4089  216 
by (safe_tac ((claset_of Fun.thy) addSIs [completeness_0])); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

217 
by (rtac (weaken_left_insert RS thms.MP) 1); 
4089  218 
by (fast_tac ((claset_of Fun.thy) addSIs [sat_imp]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

219 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

220 
qed "completeness_lemma"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

221 

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

222 
val completeness = completeness_lemma RS spec RS mp; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

223 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

224 
Goal "finite H ==> (H  p) = (H = p)"; 
4089  225 
by (fast_tac (claset() addSEs [soundness, completeness]) 1); 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3120
diff
changeset

226 
qed "syntax_iff_semantics"; 