author  nipkow 
Sun, 03 May 2015 15:38:25 +0200  
changeset 60169  5ef8ed685965 
parent 60151  9023d59acce6 
child 60758  d8d85a8172b5 
permissions  rwrr 
13403  1 
(* Title: HOL/Extraction.thy 
2 
Author: Stefan Berghofer, TU Muenchen 

3 
*) 

4 

58889  5 
section {* Program extraction for HOL *} 
13403  6 

15131  7 
theory Extraction 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
55642
diff
changeset

8 
imports Option 
15131  9 
begin 
13403  10 

48891  11 
ML_file "Tools/rewrite_hol_proof.ML" 
12 

13403  13 
subsection {* Setup *} 
14 

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

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

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

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

27 
lemmas [extraction_expand] = 

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

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

60070
73c6e58a105c
prepared for more metasimp rules (by Stefan Berghofer)
nipkow
parents:
59940
diff
changeset

34 
True_implies_equals implies_True_equals TrueE 
60169
5ef8ed685965
swap False to the right in assumptions to be eliminated at the right end
nipkow
parents:
60151
diff
changeset

35 
False_implies_equals implies_False_swap 
13403  36 

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

37 
lemmas [extraction_expand_def] = 
59940
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
58889
diff
changeset

38 
HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def 
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
58889
diff
changeset

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

40 

58350
919149921e46
added 'extraction' plugins  this might help 'HOLProofs'
blanchet
parents:
58343
diff
changeset

41 
datatype (plugins only: code extraction) sumbool = Left  Right 
13403  42 

43 
subsection {* Type of extracted program *} 

44 

45 
extract_type 

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

47 

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

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

50 

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

52 

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

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

55 

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

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

58 

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

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

61 

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

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

64 

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

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

67 

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

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

70 

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

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

73 

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

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

76 

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

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

79 

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

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

82 

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

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

85 

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

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

88 

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

90 

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

92 

93 
subsection {* Realizability *} 

94 

95 
realizability 

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

97 

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

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

100 

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

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

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

104 

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

106 

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

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

109 

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

111 

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

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

114 

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

116 

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

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

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

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

121 

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

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

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

125 

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

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

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

129 

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

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

132 

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

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

135 

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

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

138 

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

140 

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

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

143 

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

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

146 

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

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

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

150 

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

152 

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

154 

155 
theorem disjE_realizer: 

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

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

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

159 
proof (cases x) 

160 
case Inl 

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

162 
next 

163 
case Inr 

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

165 
qed 

166 

167 
theorem disjE_realizer2: 

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

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

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

171 
proof (cases x) 

172 
case None 

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

174 
next 

175 
case Some 

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

177 
qed 

178 

179 
theorem disjE_realizer3: 

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

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

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

183 
proof (cases x) 

184 
case Left 

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

186 
next 

187 
case Right 

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

189 
qed 

190 

191 
theorem conjI_realizer: 

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

193 
by simp 

194 

195 
theorem exI_realizer: 

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

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

197 

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

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

201 

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

202 
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

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

205 
realizers 

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

206 
impI (P, Q): "\<lambda>pq. pq" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

207 
"\<^bold>\<lambda>(c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  208 

209 
impI (P): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

210 
"\<^bold>\<lambda>(c: _) P Q (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  211 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

212 
impI (Q): "\<lambda>q. q" "\<^bold>\<lambda>(c: _) P Q q. impI \<cdot> _ \<cdot> _" 
13403  213 

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

214 
impI: "Null" "impI" 
13403  215 

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

216 
mp (P, Q): "\<lambda>pq. pq" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

217 
"\<^bold>\<lambda>(c: _) (d: _) P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  218 

219 
mp (P): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

220 
"\<^bold>\<lambda>(c: _) P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  221 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

222 
mp (Q): "\<lambda>q. q" "\<^bold>\<lambda>(c: _) P Q q. mp \<cdot> _ \<cdot> _" 
13403  223 

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

224 
mp: "Null" "mp" 
13403  225 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

226 
allI (P): "\<lambda>p. p" "\<^bold>\<lambda>(c: _) P (d: _) p. allI \<cdot> _ \<bullet> d" 
13403  227 

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

228 
allI: "Null" "allI" 
13403  229 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

230 
spec (P): "\<lambda>x p. p x" "\<^bold>\<lambda>(c: _) P x (d: _) p. spec \<cdot> _ \<cdot> x \<bullet> d" 
13403  231 

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

232 
spec: "Null" "spec" 
13403  233 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

234 
exI (P): "\<lambda>x p. (x, p)" "\<^bold>\<lambda>(c: _) P x (d: _) p. exI_realizer \<cdot> P \<cdot> p \<cdot> x \<bullet> c \<bullet> d" 
13403  235 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

236 
exI: "\<lambda>x. x" "\<^bold>\<lambda>P x (c: _) (h: _). h" 
13403  237 

15393  238 
exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

239 
"\<^bold>\<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  240 

241 
exE (P): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

242 
"\<^bold>\<lambda>(c: _) P Q (d: _) p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d" 
13403  243 

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

244 
exE (Q): "\<lambda>x pq. pq x" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

245 
"\<^bold>\<lambda>(c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" 
13403  246 

247 
exE: "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

248 
"\<^bold>\<lambda>P Q (c: _) x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" 
13403  249 

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

250 
conjI (P, Q): "Pair" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

251 
"\<^bold>\<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  252 

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

253 
conjI (P): "\<lambda>p. p" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

254 
"\<^bold>\<lambda>(c: _) P Q p. conjI \<cdot> _ \<cdot> _" 
13403  255 

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

256 
conjI (Q): "\<lambda>q. q" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

257 
"\<^bold>\<lambda>(c: _) P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" 
13403  258 

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

259 
conjI: "Null" "conjI" 
13403  260 

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

261 
conjunct1 (P, Q): "fst" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

262 
"\<^bold>\<lambda>(c: _) (d: _) P Q pq. conjunct1 \<cdot> _ \<cdot> _" 
13403  263 

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

264 
conjunct1 (P): "\<lambda>p. p" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

265 
"\<^bold>\<lambda>(c: _) P Q p. conjunct1 \<cdot> _ \<cdot> _" 
13403  266 

267 
conjunct1 (Q): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

268 
"\<^bold>\<lambda>(c: _) P Q q. conjunct1 \<cdot> _ \<cdot> _" 
13403  269 

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

270 
conjunct1: "Null" "conjunct1" 
13403  271 

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

272 
conjunct2 (P, Q): "snd" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

273 
"\<^bold>\<lambda>(c: _) (d: _) P Q pq. conjunct2 \<cdot> _ \<cdot> _" 
13403  274 

275 
conjunct2 (P): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

276 
"\<^bold>\<lambda>(c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _" 
13403  277 

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

278 
conjunct2 (Q): "\<lambda>p. p" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

279 
"\<^bold>\<lambda>(c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _" 
13403  280 

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

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

282 

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

283 
disjI1 (P, Q): "Inl" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

284 
"\<^bold>\<lambda>(c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.case_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)" 
13403  285 

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

286 
disjI1 (P): "Some" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

287 
"\<^bold>\<lambda>(c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)" 
13403  288 

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

289 
disjI1 (Q): "None" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

290 
"\<^bold>\<lambda>(c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)" 
13403  291 

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

292 
disjI1: "Left" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

293 
"\<^bold>\<lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)" 
13403  294 

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

295 
disjI2 (P, Q): "Inr" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

296 
"\<^bold>\<lambda>(d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.case_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)" 
13403  297 

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

298 
disjI2 (P): "None" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

299 
"\<^bold>\<lambda>(c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)" 
13403  300 

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

301 
disjI2 (Q): "Some" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

302 
"\<^bold>\<lambda>(c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)" 
13403  303 

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

304 
disjI2: "Right" 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55404
diff
changeset

305 
"\<^bold>\<lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)" 
13403  306 

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

307 
disjE (P, Q, R): "\<lambda>pq pr qr. 
13403  308 
(case pq of Inl p \<Rightarrow> pr p  Inr q \<Rightarrow> qr q)" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

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

312 
disjE (Q, R): "\<lambda>pq pr qr. 
13403  313 
(case pq of None \<Rightarrow> pr  Some q \<Rightarrow> qr q)" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

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

317 
disjE (P, R): "\<lambda>pq pr qr. 
13403  318 
(case pq of None \<Rightarrow> qr  Some p \<Rightarrow> pr p)" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

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

322 
disjE (R): "\<lambda>pq pr qr. 
13403  323 
(case pq of Left \<Rightarrow> pr  Right \<Rightarrow> qr)" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

327 
disjE (P, Q): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

328 
"\<^bold>\<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  329 

330 
disjE (Q): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

331 
"\<^bold>\<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  332 

333 
disjE (P): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

335 
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  336 

337 
disjE: "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

338 
"\<^bold>\<lambda>P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> arity_type_bool" 
13403  339 

27982  340 
FalseE (P): "default" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

341 
"\<^bold>\<lambda>(c: _) P. FalseE \<cdot> _" 
13403  342 

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

343 
FalseE: "Null" "FalseE" 
13403  344 

345 
notI (P): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

346 
"\<^bold>\<lambda>(c: _) P (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. notI \<cdot> _ \<bullet> (h \<cdot> x))" 
13403  347 

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

348 
notI: "Null" "notI" 
13403  349 

27982  350 
notE (P, R): "\<lambda>p. default" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

351 
"\<^bold>\<lambda>(c: _) (d: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  352 

353 
notE (P): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

354 
"\<^bold>\<lambda>(c: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" 
13403  355 

27982  356 
notE (R): "default" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

357 
"\<^bold>\<lambda>(c: _) P R. notE \<cdot> _ \<cdot> _" 
13403  358 

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

359 
notE: "Null" "notE" 
13403  360 

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

361 
subst (P): "\<lambda>s t ps. ps" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

362 
"\<^bold>\<lambda>(c: _) s t P (d: _) (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> d \<bullet> h" 
13403  363 

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

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

365 

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

366 
iffD1 (P, Q): "fst" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

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

370 
iffD1 (P): "\<lambda>p. p" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

371 
"\<^bold>\<lambda>(c: _) Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" 
13403  372 

373 
iffD1 (Q): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

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

377 
iffD1: "Null" "iffD1" 
13403  378 

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

379 
iffD2 (P, Q): "snd" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

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

383 
iffD2 (P): "\<lambda>p. p" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

384 
"\<^bold>\<lambda>(c: _) P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" 
13403  385 

386 
iffD2 (Q): "Null" 

52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

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

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

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

390 
iffD2: "Null" "iffD2" 
13403  391 

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

392 
iffI (P, Q): "Pair" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

393 
"\<^bold>\<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

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

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

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

397 
(arity_type_fun \<bullet> d \<bullet> c) \<bullet> 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

398 
(allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> 
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

399 
(allI \<cdot> _ \<bullet> d \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" 
13403  400 

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

401 
iffI (P): "\<lambda>p. p" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

402 
"\<^bold>\<lambda>(c: _) P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> 
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

403 
(allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> 
13403  404 
(impI \<cdot> _ \<cdot> _ \<bullet> h2)" 
405 

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

406 
iffI (Q): "\<lambda>q. q" 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

407 
"\<^bold>\<lambda>(c: _) P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> 
13403  408 
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> 
52486
b1565e37678b
just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
wenzelm
parents:
48891
diff
changeset

409 
(allI \<cdot> _ \<bullet> c \<bullet> (\<^bold>\<lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" 
13403  410 

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

411 
iffI: "Null" "iffI" 
13403  412 

413 
end 