author  wenzelm 
Wed, 31 Aug 2005 15:46:40 +0200  
changeset 17203  29b2563f5c11 
parent 16417  9bc16273c2d4 
child 18456  8cc35e95450a 
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 
15140  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 
38 
[Extraction.add_types 

15531  39 
[("bool", ([], NONE)), 
16121  40 
("set", ([realizes_set_proc], SOME mk_realizes_set))], 
17203  41 
Extraction.set_preprocessor (fn thy => 
13403  42 
Proofterm.rewrite_proof_notypes 
43 
([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) :: 

44 
ProofRewriteRules.rprocs true) o 

17203  45 
Proofterm.rewrite_proof thy 
13599  46 
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o 
16121  47 
ProofRewriteRules.elim_vars (curry Const "arbitrary"))] 
48 
end 

13403  49 
*} 
50 

51 
lemmas [extraction_expand] = 

13468
71118807d303
Removed (now unneeded) declaration of realizers for induction on natural numbers.
berghofe
parents:
13452
diff
changeset

52 
atomize_eq atomize_all atomize_imp 
13403  53 
allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 
54 
notE' impE' impE iffE imp_cong simp_thms 

55 
induct_forall_eq induct_implies_eq induct_equal_eq 

13942  56 
induct_forall_def induct_implies_def induct_impliesI 
13403  57 
induct_atomize induct_rulify1 induct_rulify2 
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 

223 
realizers 

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

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

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

227 
impI (P): "Null" 

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

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

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

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

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

232 
impI: "Null" "impI" 
13403  233 

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

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

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

237 
mp (P): "Null" 

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

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

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

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

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

242 
mp: "Null" "mp" 
13403  243 

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

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

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

246 
allI: "Null" "allI" 
13403  247 

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

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

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

250 
spec: "Null" "spec" 
13403  251 

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

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

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

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

15393  256 
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

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

259 
exE (P): "Null" 

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

260 
"\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _" 
13403  261 

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

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

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

265 
exE: "Null" 

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

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

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

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

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

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

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

272 
"\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _" 
13403  273 

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

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

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

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

277 
conjI: "Null" "conjI" 
13403  278 

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

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

280 
"\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _" 
13403  281 

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

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

283 
"\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _" 
13403  284 

285 
conjunct1 (Q): "Null" 

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

286 
"\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _" 
13403  287 

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

288 
conjunct1: "Null" "conjunct1" 
13403  289 

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

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

291 
"\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _" 
13403  292 

293 
conjunct2 (P): "Null" 

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

294 
"\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" 
13403  295 

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

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

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

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

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

300 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

325 
disjE (P, Q, R): "\<lambda>pq pr qr. 
13403  326 
(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

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

328 
disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" 
13403  329 

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

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

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

333 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" 
13403  334 

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

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

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

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

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

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

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

343 
disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" 
13403  344 

345 
disjE (P, Q): "Null" 

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

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

348 
disjE (Q): "Null" 

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

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

351 
disjE (P): "Null" 

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

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

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

355 
disjE: "Null" 

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

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

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

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

359 
"\<Lambda> P. FalseE \<cdot> _" 
13403  360 

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

361 
FalseE: "Null" "FalseE" 
13403  362 

363 
notI (P): "Null" 

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

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

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

366 
notI: "Null" "notI" 
13403  367 

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

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

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

371 
notE (P): "Null" 

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

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

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

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

375 
"\<Lambda> P R. notE \<cdot> _ \<cdot> _" 
13403  376 

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

377 
notE: "Null" "notE" 
13403  378 

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

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

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

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

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

383 

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

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

385 
"\<Lambda> Q P pq (h: _) p. 
13403  386 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" 
387 

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

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

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

391 
iffD1 (Q): "Null" 

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

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

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

395 
iffD1: "Null" "iffD1" 
13403  396 

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

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

398 
"\<Lambda> P Q pq (h: _) q. 
13403  399 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" 
400 

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

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

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

404 
iffD2 (Q): "Null" 

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

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

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

408 
iffD2: "Null" "iffD2" 
13403  409 

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

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

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

412 
(\<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

413 
(\<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

414 
(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

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

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

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

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

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

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

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

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

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

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

427 
iffI: "Null" "iffI" 
13403  428 

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

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

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

432 
*) 
13403  433 

434 
end 