author  wenzelm 
Sat, 15 Nov 2008 21:31:13 +0100  
changeset 28797  9dcd32ee5dbe 
parent 27982  2aaa4a5569a6 
child 29930  80a9a55b0a0e 
permissions  rwrr 
13403  1 
(* Title: HOL/Extraction.thy 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer, TU Muenchen 

4 
*) 

5 

6 
header {* Program extraction for HOL *} 

7 

15131  8 
theory Extraction 
24194  9 
imports Datatype 
16417  10 
uses "Tools/rewrite_hol_proof.ML" 
15131  11 
begin 
13403  12 

13 
subsection {* Setup *} 

14 

16121  15 
setup {* 
16 
let 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

17 
fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $ 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

18 
(Const ("op :", _) $ x $ S)) = (case strip_comb S of 
15531  19 
(Var (ixn, U), ts) => SOME (list_comb (Var (ixn, binder_types U @ 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

20 
[HOLogic.dest_setT (body_type U)] > HOLogic.boolT), ts @ [x])) 
15531  21 
 (Free (s, U), ts) => SOME (list_comb (Free (s, binder_types U @ 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

22 
[HOLogic.dest_setT (body_type U)] > HOLogic.boolT), ts @ [x])) 
15531  23 
 _ => NONE) 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

24 
 realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $ 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

25 
(Const ("op :", _) $ x $ S)) = (case strip_comb S of 
15531  26 
(Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T :: binder_types U @ 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

27 
[HOLogic.dest_setT (body_type U)] > HOLogic.boolT), r :: ts @ [x])) 
15531  28 
 (Free (s, U), ts) => SOME (list_comb (Free (s, T :: binder_types U @ 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

29 
[HOLogic.dest_setT (body_type U)] > HOLogic.boolT), r :: ts @ [x])) 
15531  30 
 _ => NONE) 
31 
 realizes_set_proc _ = NONE; 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

32 

12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

33 
fun mk_realizes_set r rT s (setT as Type ("set", [elT])) = 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

34 
Abs ("x", elT, Const ("realizes", rT > HOLogic.boolT > HOLogic.boolT) $ 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

35 
incr_boundvars 1 r $ (Const ("op :", elT > setT > HOLogic.boolT) $ 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

36 
Bound 0 $ incr_boundvars 1 s)); 
16121  37 
in 
18708  38 
Extraction.add_types 
15531  39 
[("bool", ([], NONE)), 
18708  40 
("set", ([realizes_set_proc], SOME mk_realizes_set))] #> 
41 
Extraction.set_preprocessor (fn thy => 

13403  42 
Proofterm.rewrite_proof_notypes 
28797
9dcd32ee5dbe
rewrite_proof: simplified simprocs (no name required);
wenzelm
parents:
27982
diff
changeset

43 
([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o 
17203  44 
Proofterm.rewrite_proof thy 
13599  45 
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o 
27982  46 
ProofRewriteRules.elim_vars (curry Const @{const_name default})) 
16121  47 
end 
13403  48 
*} 
49 

50 
lemmas [extraction_expand] = 

22281  51 
meta_spec atomize_eq atomize_all atomize_imp atomize_conj 
13403  52 
allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 
20941
beedcae49096
added eq_True eq_False True_implies_equals to extraction_expand
haftmann
parents:
18708
diff
changeset

53 
notE' impE' impE iffE imp_cong simp_thms eq_True eq_False 
18456  54 
induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
55 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 

18511  56 
induct_atomize induct_rulify induct_rulify_fallback 
25424  57 
True_implies_equals TrueE 
13403  58 

59 
datatype sumbool = Left  Right 

60 

61 
subsection {* Type of extracted program *} 

62 

63 
extract_type 

64 
"typeof (Trueprop P) \<equiv> typeof P" 

65 

66 
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> 

67 
typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('Q))" 

68 

69 
"typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE(Null))" 

70 

71 
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> 

72 
typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('P \<Rightarrow> 'Q))" 

73 

74 
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> 

75 
typeof (\<forall>x. P x) \<equiv> Type (TYPE(Null))" 

76 

77 
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow> 

78 
typeof (\<forall>x::'a. P x) \<equiv> Type (TYPE('a \<Rightarrow> 'P))" 

79 

80 
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> 

81 
typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a))" 

82 

83 
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow> 

84 
typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a \<times> 'P))" 

85 

86 
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> 

87 
typeof (P \<or> Q) \<equiv> Type (TYPE(sumbool))" 

88 

89 
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> 

90 
typeof (P \<or> Q) \<equiv> Type (TYPE('Q option))" 

91 

92 
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> 

93 
typeof (P \<or> Q) \<equiv> Type (TYPE('P option))" 

94 

95 
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> 

96 
typeof (P \<or> Q) \<equiv> Type (TYPE('P + 'Q))" 

97 

98 
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> 

99 
typeof (P \<and> Q) \<equiv> Type (TYPE('Q))" 

100 

101 
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> 

102 
typeof (P \<and> Q) \<equiv> Type (TYPE('P))" 

103 

104 
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow> 

105 
typeof (P \<and> Q) \<equiv> Type (TYPE('P \<times> 'Q))" 

106 

107 
"typeof (P = Q) \<equiv> typeof ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" 

108 

109 
"typeof (x \<in> P) \<equiv> typeof P" 

110 

111 
subsection {* Realizability *} 

112 

113 
realizability 

114 
"(realizes t (Trueprop P)) \<equiv> (Trueprop (realizes t P))" 

115 

116 
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

117 
(realizes t (P \<longrightarrow> Q)) \<equiv> (realizes Null P \<longrightarrow> realizes t Q)" 

118 

119 
"(typeof P) \<equiv> (Type (TYPE('P))) \<Longrightarrow> 

120 
(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

121 
(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x::'P. realizes x P \<longrightarrow> realizes Null Q)" 

122 

123 
"(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x. realizes x P \<longrightarrow> realizes (t x) Q)" 

124 

125 
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> 

126 
(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes Null (P x))" 

127 

128 
"(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes (t x) (P x))" 

129 

130 
"(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow> 

131 
(realizes t (\<exists>x. P x)) \<equiv> (realizes Null (P t))" 

132 

133 
"(realizes t (\<exists>x. P x)) \<equiv> (realizes (snd t) (P (fst t)))" 

134 

135 
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

136 
(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

137 
(realizes t (P \<or> Q)) \<equiv> 

138 
(case t of Left \<Rightarrow> realizes Null P  Right \<Rightarrow> realizes Null Q)" 

139 

140 
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

141 
(realizes t (P \<or> Q)) \<equiv> 

142 
(case t of None \<Rightarrow> realizes Null P  Some q \<Rightarrow> realizes q Q)" 

143 

144 
"(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

145 
(realizes t (P \<or> Q)) \<equiv> 

146 
(case t of None \<Rightarrow> realizes Null Q  Some p \<Rightarrow> realizes p P)" 

147 

148 
"(realizes t (P \<or> Q)) \<equiv> 

149 
(case t of Inl p \<Rightarrow> realizes p P  Inr q \<Rightarrow> realizes q Q)" 

150 

151 
"(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

152 
(realizes t (P \<and> Q)) \<equiv> (realizes Null P \<and> realizes t Q)" 

153 

154 
"(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow> 

155 
(realizes t (P \<and> Q)) \<equiv> (realizes t P \<and> realizes Null Q)" 

156 

157 
"(realizes t (P \<and> Q)) \<equiv> (realizes (fst t) P \<and> realizes (snd t) Q)" 

158 

159 
"typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> 

160 
realizes t (\<not> P) \<equiv> \<not> realizes Null P" 

161 

162 
"typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> 

163 
realizes t (\<not> P) \<equiv> (\<forall>x::'P. \<not> realizes x P)" 

164 

165 
"typeof (P::bool) \<equiv> Type (TYPE(Null)) \<Longrightarrow> 

166 
typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> 

167 
realizes t (P = Q) \<equiv> realizes Null P = realizes Null Q" 

168 

169 
"(realizes t (P = Q)) \<equiv> (realizes t ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)))" 

170 

171 
subsection {* Computational content of basic inference rules *} 

172 

173 
theorem disjE_realizer: 

174 
assumes r: "case x of Inl p \<Rightarrow> P p  Inr q \<Rightarrow> Q q" 

175 
and r1: "\<And>p. P p \<Longrightarrow> R (f p)" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)" 

176 
shows "R (case x of Inl p \<Rightarrow> f p  Inr q \<Rightarrow> g q)" 

177 
proof (cases x) 

178 
case Inl 

179 
with r show ?thesis by simp (rule r1) 

180 
next 

181 
case Inr 

182 
with r show ?thesis by simp (rule r2) 

183 
qed 

184 

185 
theorem disjE_realizer2: 

186 
assumes r: "case x of None \<Rightarrow> P  Some q \<Rightarrow> Q q" 

187 
and r1: "P \<Longrightarrow> R f" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)" 

188 
shows "R (case x of None \<Rightarrow> f  Some q \<Rightarrow> g q)" 

189 
proof (cases x) 

190 
case None 

191 
with r show ?thesis by simp (rule r1) 

192 
next 

193 
case Some 

194 
with r show ?thesis by simp (rule r2) 

195 
qed 

196 

197 
theorem disjE_realizer3: 

198 
assumes r: "case x of Left \<Rightarrow> P  Right \<Rightarrow> Q" 

199 
and r1: "P \<Longrightarrow> R f" and r2: "Q \<Longrightarrow> R g" 

200 
shows "R (case x of Left \<Rightarrow> f  Right \<Rightarrow> g)" 

201 
proof (cases x) 

202 
case Left 

203 
with r show ?thesis by simp (rule r1) 

204 
next 

205 
case Right 

206 
with r show ?thesis by simp (rule r2) 

207 
qed 

208 

209 
theorem conjI_realizer: 

210 
"P p \<Longrightarrow> Q q \<Longrightarrow> P (fst (p, q)) \<and> Q (snd (p, q))" 

211 
by simp 

212 

213 
theorem exI_realizer: 

13918
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset

214 
"P y x \<Longrightarrow> P (snd (x, y)) (fst (x, y))" by simp 
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset

215 

2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset

216 
theorem exE_realizer: "P (snd p) (fst p) \<Longrightarrow> 
15393  217 
(\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (let (x, y) = p in f x y)" 
218 
by (cases p) (simp add: Let_def) 

13918
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset

219 

2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset

220 
theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow> 
2134ed516b1b
Tuned realizer for exE rule, to avoid blowup of extracted program.
berghofe
parents:
13725
diff
changeset

221 
(\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp 
13403  222 

27982  223 
setup {* 
224 
Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"}) 

225 
*} 

226 

13403  227 
realizers 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

228 
impI (P, Q): "\<lambda>pq. pq" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

229 
"\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  230 

231 
impI (P): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

232 
"\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  233 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

234 
impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _" 
13403  235 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

236 
impI: "Null" "impI" 
13403  237 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

238 
mp (P, Q): "\<lambda>pq. pq" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

239 
"\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" 
13403  240 

241 
mp (P): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

242 
"\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" 
13403  243 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

244 
mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _" 
13403  245 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

246 
mp: "Null" "mp" 
13403  247 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

248 
allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _" 
13403  249 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

250 
allI: "Null" "allI" 
13403  251 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

252 
spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x" 
13403  253 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

254 
spec: "Null" "spec" 
13403  255 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

256 
exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x" 
13403  257 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

258 
exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h" 
13403  259 

15393  260 
exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

261 
"\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h" 
13403  262 

263 
exE (P): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

264 
"\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _" 
13403  265 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

266 
exE (Q): "\<lambda>x pq. pq x" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

267 
"\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" 
13403  268 

269 
exE: "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

270 
"\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" 
13403  271 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

272 
conjI (P, Q): "Pair" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

273 
"\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h" 
13403  274 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

275 
conjI (P): "\<lambda>p. p" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

276 
"\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _" 
13403  277 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

278 
conjI (Q): "\<lambda>q. q" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

279 
"\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" 
13403  280 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

281 
conjI: "Null" "conjI" 
13403  282 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

283 
conjunct1 (P, Q): "fst" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

284 
"\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _" 
13403  285 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

286 
conjunct1 (P): "\<lambda>p. p" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

287 
"\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _" 
13403  288 

289 
conjunct1 (Q): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

290 
"\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _" 
13403  291 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

292 
conjunct1: "Null" "conjunct1" 
13403  293 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

294 
conjunct2 (P, Q): "snd" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

295 
"\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _" 
13403  296 

297 
conjunct2 (P): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

298 
"\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" 
13403  299 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

300 
conjunct2 (Q): "\<lambda>p. p" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

301 
"\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" 
13403  302 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

303 
conjunct2: "Null" "conjunct2" 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

304 

12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

305 
disjI1 (P, Q): "Inl" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

306 
"\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)" 
13403  307 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

308 
disjI1 (P): "Some" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

309 
"\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)" 
13403  310 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

311 
disjI1 (Q): "None" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

312 
"\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" 
13403  313 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

314 
disjI1: "Left" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

315 
"\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)" 
13403  316 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

317 
disjI2 (P, Q): "Inr" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

318 
"\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" 
13403  319 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

320 
disjI2 (P): "None" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

321 
"\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" 
13403  322 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

323 
disjI2 (Q): "Some" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

324 
"\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" 
13403  325 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

326 
disjI2: "Right" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

327 
"\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)" 
13403  328 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

329 
disjE (P, Q, R): "\<lambda>pq pr qr. 
13403  330 
(case pq of Inl p \<Rightarrow> pr p  Inr q \<Rightarrow> qr q)" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

331 
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

332 
disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" 
13403  333 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

334 
disjE (Q, R): "\<lambda>pq pr qr. 
13403  335 
(case pq of None \<Rightarrow> pr  Some q \<Rightarrow> qr q)" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

336 
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

337 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" 
13403  338 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

339 
disjE (P, R): "\<lambda>pq pr qr. 
13403  340 
(case pq of None \<Rightarrow> qr  Some p \<Rightarrow> pr p)" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

341 
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _). 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

342 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2" 
13403  343 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

344 
disjE (R): "\<lambda>pq pr qr. 
13403  345 
(case pq of Left \<Rightarrow> pr  Right \<Rightarrow> qr)" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

346 
"\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

347 
disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" 
13403  348 

349 
disjE (P, Q): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

350 
"\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" 
13403  351 

352 
disjE (Q): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

353 
"\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" 
13403  354 

355 
disjE (P): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

356 
"\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _). 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

357 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2" 
13403  358 

359 
disjE: "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

360 
"\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" 
13403  361 

27982  362 
FalseE (P): "default" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

363 
"\<Lambda> P. FalseE \<cdot> _" 
13403  364 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

365 
FalseE: "Null" "FalseE" 
13403  366 

367 
notI (P): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

368 
"\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  369 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

370 
notI: "Null" "notI" 
13403  371 

27982  372 
notE (P, R): "\<lambda>p. default" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

373 
"\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" 
13403  374 

375 
notE (P): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

376 
"\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" 
13403  377 

27982  378 
notE (R): "default" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

379 
"\<Lambda> P R. notE \<cdot> _ \<cdot> _" 
13403  380 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

381 
notE: "Null" "notE" 
13403  382 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

383 
subst (P): "\<lambda>s t ps. ps" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

384 
"\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h" 
13403  385 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

386 
subst: "Null" "subst" 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

387 

12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

388 
iffD1 (P, Q): "fst" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

389 
"\<Lambda> Q P pq (h: _) p. 
13403  390 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" 
391 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

392 
iffD1 (P): "\<lambda>p. p" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

393 
"\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" 
13403  394 

395 
iffD1 (Q): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

396 
"\<Lambda> Q P q1 (h: _) q2. 
13403  397 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" 
398 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

399 
iffD1: "Null" "iffD1" 
13403  400 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

401 
iffD2 (P, Q): "snd" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

402 
"\<Lambda> P Q pq (h: _) q. 
13403  403 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" 
404 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

405 
iffD2 (P): "\<lambda>p. p" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

406 
"\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" 
13403  407 

408 
iffD2 (Q): "Null" 

14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

409 
"\<Lambda> P Q q1 (h: _) q2. 
13403  410 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" 
411 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

412 
iffD2: "Null" "iffD2" 
13403  413 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

414 
iffI (P, Q): "Pair" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

415 
"\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot> 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

416 
(\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot> 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

417 
(\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet> 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

418 
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> 
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

419 
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" 
13403  420 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

421 
iffI (P): "\<lambda>p. p" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

422 
"\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> 
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

423 
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> 
13403  424 
(impI \<cdot> _ \<cdot> _ \<bullet> h2)" 
425 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

426 
iffI (Q): "\<lambda>q. q" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

427 
"\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> 
13403  428 
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

429 
(allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" 
13403  430 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

431 
iffI: "Null" "iffI" 
13403  432 

13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

433 
(* 
13403  434 
classical: "Null" 
14168
ed81cd283816
Prepared for extended identifiers (\<alpha>, etc.)
skalberg
parents:
13942
diff
changeset

435 
"\<Lambda> P. classical \<cdot> _" 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13599
diff
changeset

436 
*) 
13403  437 

27982  438 
setup {* 
439 
Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"}) 

440 
*} 

441 

13403  442 
end 