author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 37233  b78f31ca4675 
child 48891  c0eafbd55de3 
permissions  rwrr 
13403  1 
(* Title: HOL/Extraction.thy 
2 
Author: Stefan Berghofer, TU Muenchen 

3 
*) 

4 

5 
header {* Program extraction for HOL *} 

6 

15131  7 
theory Extraction 
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
29930
diff
changeset

8 
imports Option 
16417  9 
uses "Tools/rewrite_hol_proof.ML" 
15131  10 
begin 
13403  11 

12 
subsection {* Setup *} 

13 

16121  14 
setup {* 
18708  15 
Extraction.add_types 
29930  16 
[("bool", ([], NONE))] #> 
18708  17 
Extraction.set_preprocessor (fn thy => 
13403  18 
Proofterm.rewrite_proof_notypes 
28797
9dcd32ee5dbe
rewrite_proof: simplified simprocs (no name required);
wenzelm
parents:
27982
diff
changeset

19 
([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o 
17203  20 
Proofterm.rewrite_proof thy 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

21 
(RewriteHOLProof.rews, 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

22 
ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o 
27982  23 
ProofRewriteRules.elim_vars (curry Const @{const_name default})) 
13403  24 
*} 
25 

26 
lemmas [extraction_expand] = 

22281  27 
meta_spec atomize_eq atomize_all atomize_imp atomize_conj 
13403  28 
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

29 
notE' impE' impE iffE imp_cong simp_thms eq_True eq_False 
18456  30 
induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq 
34913  31 
induct_atomize induct_atomize' induct_rulify induct_rulify' 
32 
induct_rulify_fallback induct_trueI 

25424  33 
True_implies_equals TrueE 
13403  34 

33704
6aeb8454efc1
add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
wenzelm
parents:
30235
diff
changeset

35 
lemmas [extraction_expand_def] = 
6aeb8454efc1
add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
wenzelm
parents:
30235
diff
changeset

36 
induct_forall_def induct_implies_def induct_equal_def induct_conj_def 
34913  37 
induct_true_def induct_false_def 
33704
6aeb8454efc1
add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
wenzelm
parents:
30235
diff
changeset

38 

13403  39 
datatype sumbool = Left  Right 
40 

41 
subsection {* Type of extracted program *} 

42 

43 
extract_type 

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

45 

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

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

48 

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

50 

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

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

53 

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

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

56 

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

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

59 

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

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

62 

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

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

65 

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

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

68 

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

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

71 

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

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

74 

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

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

77 

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

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

80 

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

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

83 

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

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

86 

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

88 

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

90 

91 
subsection {* Realizability *} 

92 

93 
realizability 

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

95 

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

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

98 

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

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

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

102 

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

104 

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

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

107 

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

109 

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

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

112 

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

114 

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

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

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

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

119 

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

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

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

123 

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

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

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

127 

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

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

130 

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

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

133 

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

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

136 

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

138 

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

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

141 

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

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

144 

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

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

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

148 

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

150 

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

152 

153 
theorem disjE_realizer: 

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

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

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

157 
proof (cases x) 

158 
case Inl 

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

160 
next 

161 
case Inr 

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

163 
qed 

164 

165 
theorem disjE_realizer2: 

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

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

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

169 
proof (cases x) 

170 
case None 

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

172 
next 

173 
case Some 

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

175 
qed 

176 

177 
theorem disjE_realizer3: 

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

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

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

181 
proof (cases x) 

182 
case Left 

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

184 
next 

185 
case Right 

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

187 
qed 

188 

189 
theorem conjI_realizer: 

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

191 
by simp 

192 

193 
theorem exI_realizer: 

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

194 
"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

195 

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

196 
theorem exE_realizer: "P (snd p) (fst p) \<Longrightarrow> 
15393  197 
(\<And>x y. P y x \<Longrightarrow> Q (f x y)) \<Longrightarrow> Q (let (x, y) = p in f x y)" 
198 
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

199 

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

200 
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

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

203 
realizers 

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

204 
impI (P, Q): "\<lambda>pq. pq" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

205 
"\<Lambda> (c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  206 

207 
impI (P): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

208 
"\<Lambda> (c: _) P Q (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  209 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

210 
impI (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. impI \<cdot> _ \<cdot> _" 
13403  211 

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

212 
impI: "Null" "impI" 
13403  213 

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

214 
mp (P, Q): "\<lambda>pq. pq" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

215 
"\<Lambda> (c: _) (d: _) P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  216 

217 
mp (P): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

218 
"\<Lambda> (c: _) P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  219 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

220 
mp (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. mp \<cdot> _ \<cdot> _" 
13403  221 

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

222 
mp: "Null" "mp" 
13403  223 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

224 
allI (P): "\<lambda>p. p" "\<Lambda> (c: _) P (d: _) p. allI \<cdot> _ \<bullet> d" 
13403  225 

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

226 
allI: "Null" "allI" 
13403  227 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

228 
spec (P): "\<lambda>x p. p x" "\<Lambda> (c: _) P x (d: _) p. spec \<cdot> _ \<cdot> x \<bullet> d" 
13403  229 

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

230 
spec: "Null" "spec" 
13403  231 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

232 
exI (P): "\<lambda>x p. (x, p)" "\<Lambda> (c: _) P x (d: _) p. exI_realizer \<cdot> P \<cdot> p \<cdot> x \<bullet> c \<bullet> d" 
13403  233 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

234 
exI: "\<lambda>x. x" "\<Lambda> P x (c: _) (h: _). h" 
13403  235 

15393  236 
exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

237 
"\<Lambda> (c: _) (d: _) P Q (e: _) p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> c \<bullet> e \<bullet> d \<bullet> h" 
13403  238 

239 
exE (P): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

240 
"\<Lambda> (c: _) P Q (d: _) p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d" 
13403  241 

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

242 
exE (Q): "\<lambda>x pq. pq x" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

243 
"\<Lambda> (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" 
13403  244 

245 
exE: "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

246 
"\<Lambda> P Q (c: _) x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" 
13403  247 

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

248 
conjI (P, Q): "Pair" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

249 
"\<Lambda> (c: _) (d: _) P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> c \<bullet> d \<bullet> h" 
13403  250 

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

251 
conjI (P): "\<lambda>p. p" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

252 
"\<Lambda> (c: _) P Q p. conjI \<cdot> _ \<cdot> _" 
13403  253 

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

254 
conjI (Q): "\<lambda>q. q" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

255 
"\<Lambda> (c: _) P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" 
13403  256 

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

257 
conjI: "Null" "conjI" 
13403  258 

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

259 
conjunct1 (P, Q): "fst" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

260 
"\<Lambda> (c: _) (d: _) P Q pq. conjunct1 \<cdot> _ \<cdot> _" 
13403  261 

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

262 
conjunct1 (P): "\<lambda>p. p" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

263 
"\<Lambda> (c: _) P Q p. conjunct1 \<cdot> _ \<cdot> _" 
13403  264 

265 
conjunct1 (Q): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

266 
"\<Lambda> (c: _) P Q q. conjunct1 \<cdot> _ \<cdot> _" 
13403  267 

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

268 
conjunct1: "Null" "conjunct1" 
13403  269 

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

270 
conjunct2 (P, Q): "snd" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

271 
"\<Lambda> (c: _) (d: _) P Q pq. conjunct2 \<cdot> _ \<cdot> _" 
13403  272 

273 
conjunct2 (P): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

274 
"\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _" 
13403  275 

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

276 
conjunct2 (Q): "\<lambda>p. p" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

277 
"\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _" 
13403  278 

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

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

280 

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

281 
disjI1 (P, Q): "Inl" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

282 
"\<Lambda> (c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)" 
13403  283 

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

284 
disjI1 (P): "Some" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

285 
"\<Lambda> (c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)" 
13403  286 

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

287 
disjI1 (Q): "None" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

288 
"\<Lambda> (c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)" 
13403  289 

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

290 
disjI1: "Left" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

291 
"\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)" 
13403  292 

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

293 
disjI2 (P, Q): "Inr" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

294 
"\<Lambda> (d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)" 
13403  295 

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

296 
disjI2 (P): "None" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

297 
"\<Lambda> (c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)" 
13403  298 

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

299 
disjI2 (Q): "Some" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

300 
"\<Lambda> (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)" 
13403  301 

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

302 
disjI2: "Right" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

303 
"\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)" 
13403  304 

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

305 
disjE (P, Q, R): "\<lambda>pq pr qr. 
13403  306 
(case pq of Inl p \<Rightarrow> pr p  Inr q \<Rightarrow> qr q)" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

307 
"\<Lambda> (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr. 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

308 
disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> e \<bullet> h1 \<bullet> h2" 
13403  309 

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

310 
disjE (Q, R): "\<lambda>pq pr qr. 
13403  311 
(case pq of None \<Rightarrow> pr  Some q \<Rightarrow> qr q)" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

312 
"\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr. 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

313 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h2" 
13403  314 

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

315 
disjE (P, R): "\<lambda>pq pr qr. 
13403  316 
(case pq of None \<Rightarrow> qr  Some p \<Rightarrow> pr p)" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

317 
"\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _). 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

318 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h3 \<bullet> h2" 
13403  319 

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

320 
disjE (R): "\<lambda>pq pr qr. 
13403  321 
(case pq of Left \<Rightarrow> pr  Right \<Rightarrow> qr)" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

322 
"\<Lambda> (c: _) P Q R pq (h1: _) pr (h2: _) qr. 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

323 
disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> h1 \<bullet> h2" 
13403  324 

325 
disjE (P, Q): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

326 
"\<Lambda> (c: _) (d: _) P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d \<bullet> arity_type_bool" 
13403  327 

328 
disjE (Q): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

329 
"\<Lambda> (c: _) P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool" 
13403  330 

331 
disjE (P): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

332 
"\<Lambda> (c: _) P Q R pq (h1: _) (h2: _) (h3: _). 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

333 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool \<bullet> h1 \<bullet> h3 \<bullet> h2" 
13403  334 

335 
disjE: "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

336 
"\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> arity_type_bool" 
13403  337 

27982  338 
FalseE (P): "default" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

339 
"\<Lambda> (c: _) P. FalseE \<cdot> _" 
13403  340 

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

341 
FalseE: "Null" "FalseE" 
13403  342 

343 
notI (P): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

344 
"\<Lambda> (c: _) P (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  345 

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

346 
notI: "Null" "notI" 
13403  347 

27982  348 
notE (P, R): "\<lambda>p. default" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

349 
"\<Lambda> (c: _) (d: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  350 

351 
notE (P): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

352 
"\<Lambda> (c: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  353 

27982  354 
notE (R): "default" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

355 
"\<Lambda> (c: _) P R. notE \<cdot> _ \<cdot> _" 
13403  356 

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

357 
notE: "Null" "notE" 
13403  358 

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

359 
subst (P): "\<lambda>s t ps. ps" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

360 
"\<Lambda> (c: _) s t P (d: _) (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> d \<bullet> h" 
13403  361 

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

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

363 

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

364 
iffD1 (P, Q): "fst" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

365 
"\<Lambda> (d: _) (c: _) Q P pq (h: _) p. 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

366 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> d \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" 
13403  367 

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

368 
iffD1 (P): "\<lambda>p. p" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

369 
"\<Lambda> (c: _) Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" 
13403  370 

371 
iffD1 (Q): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

372 
"\<Lambda> (c: _) Q P q1 (h: _) q2. 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

373 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" 
13403  374 

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

375 
iffD1: "Null" "iffD1" 
13403  376 

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

377 
iffD2 (P, Q): "snd" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

378 
"\<Lambda> (c: _) (d: _) P Q pq (h: _) q. 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

379 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> d \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" 
13403  380 

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

381 
iffD2 (P): "\<lambda>p. p" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

382 
"\<Lambda> (c: _) P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" 
13403  383 

384 
iffD2 (Q): "Null" 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

385 
"\<Lambda> (c: _) P Q q1 (h: _) q2. 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

386 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" 
13403  387 

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

388 
iffD2: "Null" "iffD2" 
13403  389 

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

390 
iffI (P, Q): "Pair" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

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

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

393 
(\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet> 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

394 
(arity_type_fun \<bullet> c \<bullet> d) \<bullet> 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

395 
(arity_type_fun \<bullet> d \<bullet> c) \<bullet> 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

396 
(allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

397 
(allI \<cdot> _ \<bullet> d \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" 
13403  398 

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

399 
iffI (P): "\<lambda>p. p" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

400 
"\<Lambda> (c: _) P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

401 
(allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> 
13403  402 
(impI \<cdot> _ \<cdot> _ \<bullet> h2)" 
403 

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

404 
iffI (Q): "\<lambda>q. q" 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

405 
"\<Lambda> (c: _) P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> 
13403  406 
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
34913
diff
changeset

407 
(allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" 
13403  408 

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

409 
iffI: "Null" "iffI" 
13403  410 

411 
end 