13403

1 
(* Title: HOL/Extraction.thy


2 
ID: $Id$


3 
Author: Stefan Berghofer, TU Muenchen


4 
License: GPL (GNU GENERAL PUBLIC LICENSE)


5 
*)


6 


7 
header {* Program extraction for HOL *}


8 


9 
theory Extraction = Datatype


10 
files


11 
"Tools/rewrite_hol_proof.ML":


12 


13 
subsection {* Setup *}


14 


15 
ML_setup {*


16 
Context.>> (fn thy => thy >


17 
Extraction.set_preprocessor (fn sg =>


18 
Proofterm.rewrite_proof_notypes


19 
([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::


20 
ProofRewriteRules.rprocs true) o


21 
Proofterm.rewrite_proof (Sign.tsig_of sg)


22 
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true)))


23 
*}


24 


25 
lemmas [extraction_expand] =


26 
nat.exhaust atomize_eq atomize_all atomize_imp


27 
allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2


28 
notE' impE' impE iffE imp_cong simp_thms


29 
induct_forall_eq induct_implies_eq induct_equal_eq


30 
induct_forall_def induct_implies_def


31 
induct_atomize induct_rulify1 induct_rulify2


32 


33 
datatype sumbool = Left  Right


34 


35 
subsection {* Type of extracted program *}


36 


37 
extract_type


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


39 


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


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


42 


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


44 


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


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


47 


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


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


50 


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


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


53 


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


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


56 


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


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


59 


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


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


62 


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


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


65 


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


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


68 


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


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


71 


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


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


74 


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


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


77 


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


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


80 


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


82 


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


84 


85 
subsection {* Realizability *}


86 


87 
realizability


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


89 


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


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


92 


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


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


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


96 


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


98 


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


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


101 


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


103 


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


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


106 


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


108 


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


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


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


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


113 


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


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


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


117 


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


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


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


121 


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


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


124 


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


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


127 


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


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


130 


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


132 


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


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


135 


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


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


138 


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


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


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


142 


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


144 


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


146 


147 
theorem disjE_realizer:


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


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


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


151 
proof (cases x)


152 
case Inl


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


154 
next


155 
case Inr


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


157 
qed


158 


159 
theorem disjE_realizer2:


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


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


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


163 
proof (cases x)


164 
case None


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


166 
next


167 
case Some


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


169 
qed


170 


171 
theorem disjE_realizer3:


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


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


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


175 
proof (cases x)


176 
case Left


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


178 
next


179 
case Right


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


181 
qed


182 


183 
theorem conjI_realizer:


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


185 
by simp


186 


187 
theorem exI_realizer:


188 
"P x y \<Longrightarrow> P (fst (x, y)) (snd (x, y))" by simp


189 


190 
realizers


191 
impI (P, Q): "\<lambda>P Q pq. pq"


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


193 


194 
impI (P): "Null"


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


196 


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


198 


199 
impI: "Null" "\<Lambda>P Q. impI \<cdot> _ \<cdot> _"


200 


201 
mp (P, Q): "\<lambda>P Q pq. pq"


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


203 


204 
mp (P): "Null"


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


206 


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


208 


209 
mp: "Null" "\<Lambda>P Q. mp \<cdot> _ \<cdot> _"


210 


211 
allI (P): "\<lambda>P p. p" "\<Lambda>P p. allI \<cdot> _"


212 


213 
allI: "Null" "\<Lambda>P. allI \<cdot> _"


214 


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


216 


217 
spec: "Null" "\<Lambda>P x. spec \<cdot> _ \<cdot> x"


218 


219 
exI (P): "\<lambda>P x p. (x, p)" "\<Lambda>P. exI_realizer \<cdot> _"


220 


221 
exI: "\<lambda>P x. x" "\<Lambda>P x (h: _). h"


222 


223 
exE (P, Q): "\<lambda>P Q p pq. pq (fst p) (snd p)"


224 
"\<Lambda>P Q p (h1: _) pq (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"


225 


226 
exE (P): "Null"


227 
"\<Lambda>P Q p (h1: _) (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"


228 


229 
exE (Q): "\<lambda>P Q x pq. pq x"


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


231 


232 
exE: "Null"


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


234 


235 
conjI (P, Q): "\<lambda>P Q p q. (p, q)"


236 
"\<Lambda>P Q p (h: _) q. conjI_realizer \<cdot>


237 
(\<lambda>p. realizes p P) \<cdot> p \<cdot> (\<lambda>q. realizes q Q) \<cdot> q \<bullet> h"


238 


239 
conjI (P): "\<lambda>P Q p. p"


240 
"\<Lambda>P Q p. conjI \<cdot> _ \<cdot> _"


241 


242 
conjI (Q): "\<lambda>P Q q. q"


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


244 


245 
conjI: "Null"


246 
"\<Lambda>P Q. conjI \<cdot> _ \<cdot> _"


247 


248 
conjunct1 (P, Q): "\<lambda>P Q. fst"


249 
"\<Lambda>P Q pq. conjunct1 \<cdot> _ \<cdot> _"


250 


251 
conjunct1 (P): "\<lambda>P Q p. p"


252 
"\<Lambda>P Q p. conjunct1 \<cdot> _ \<cdot> _"


253 


254 
conjunct1 (Q): "Null"


255 
"\<Lambda>P Q q. conjunct1 \<cdot> _ \<cdot> _"


256 


257 
conjunct1: "Null"


258 
"\<Lambda>P Q. conjunct1 \<cdot> _ \<cdot> _"


259 


260 
conjunct2 (P, Q): "\<lambda>P Q. snd"


261 
"\<Lambda>P Q pq. conjunct2 \<cdot> _ \<cdot> _"


262 


263 
conjunct2 (P): "Null"


264 
"\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _"


265 


266 
conjunct2 (Q): "\<lambda>P Q p. p"


267 
"\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _"


268 


269 
conjunct2: "Null"


270 
"\<Lambda>P Q. conjunct2 \<cdot> _ \<cdot> _"


271 


272 
disjI1 (P, Q): "\<lambda>P Q. Inl"


273 
"\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> (\<lambda>p. realizes p P) \<cdot> _ \<cdot> p)"


274 


275 
disjI1 (P): "\<lambda>P Q. Some"


276 
"\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>p. realizes p P) \<cdot> p)"


277 


278 
disjI1 (Q): "\<lambda>P Q. None"


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


280 


281 
disjI1: "\<lambda>P Q. Left"


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


283 


284 
disjI2 (P, Q): "\<lambda>Q P. Inr"


285 
"\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)"


286 


287 
disjI2 (P): "\<lambda>Q P. None"


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


289 


290 
disjI2 (Q): "\<lambda>Q P. Some"


291 
"\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)"


292 


293 
disjI2: "\<lambda>Q P. Right"


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


295 


296 
disjE (P, Q, R): "\<lambda>P Q R pq pr qr.


297 
(case pq of Inl p \<Rightarrow> pr p  Inr q \<Rightarrow> qr q)"


298 
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.


299 
disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"


300 


301 
disjE (Q, R): "\<lambda>P Q R pq pr qr.


302 
(case pq of None \<Rightarrow> pr  Some q \<Rightarrow> qr q)"


303 
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.


304 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"


305 


306 
disjE (P, R): "\<lambda>P Q R pq pr qr.


307 
(case pq of None \<Rightarrow> qr  Some p \<Rightarrow> pr p)"


308 
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr (h3: _).


309 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2"


310 


311 
disjE (R): "\<lambda>P Q R pq pr qr.


312 
(case pq of Left \<Rightarrow> pr  Right \<Rightarrow> qr)"


313 
"\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.


314 
disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"


315 


316 
disjE (P, Q): "Null"


317 
"\<Lambda>P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"


318 


319 
disjE (Q): "Null"


320 
"\<Lambda>P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"


321 


322 
disjE (P): "Null"


323 
"\<Lambda>P Q R pq (h1: _) (h2: _) (h3: _).


324 
disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2"


325 


326 
disjE: "Null"


327 
"\<Lambda>P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"


328 


329 
FalseE (P): "\<lambda>P. arbitrary"


330 
"\<Lambda>P. FalseE \<cdot> _"


331 


332 
FalseE: "Null"


333 
"\<Lambda>P. FalseE \<cdot> _"


334 


335 
notI (P): "Null"


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


337 


338 
notI: "Null"


339 
"\<Lambda>P. notI \<cdot> _"


340 


341 
notE (P, R): "\<lambda>P R p. arbitrary"


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


343 


344 
notE (P): "Null"


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


346 


347 
notE (R): "\<lambda>P R. arbitrary"


348 
"\<Lambda>P R. notE \<cdot> _ \<cdot> _"


349 


350 
notE: "Null"


351 
"\<Lambda>P R. notE \<cdot> _ \<cdot> _"


352 


353 
subst (P): "\<lambda>s t P ps. ps"


354 
"\<Lambda>s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes ps (P x)) \<bullet> h"


355 


356 
subst: "Null"


357 
"\<Lambda>s t P. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes Null (P x))"


358 


359 
iffD1 (P, Q): "\<lambda>Q P. fst"


360 
"\<Lambda>Q P pq (h: _) p.


361 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"


362 


363 
iffD1 (P): "\<lambda>Q P p. p"


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


365 


366 
iffD1 (Q): "Null"


367 
"\<Lambda>Q P q1 (h: _) q2.


368 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"


369 


370 
iffD1: "Null"


371 
"\<Lambda>Q P. iffD1 \<cdot> _ \<cdot> _"


372 


373 
iffD2 (P, Q): "\<lambda>P Q. snd"


374 
"\<Lambda>P Q pq (h: _) q.


375 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"


376 


377 
iffD2 (P): "\<lambda>P Q p. p"


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


379 


380 
iffD2 (Q): "Null"


381 
"\<Lambda>P Q q1 (h: _) q2.


382 
mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"


383 


384 
iffD2: "Null"


385 
"\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _"


386 


387 
iffI (P, Q): "\<lambda>P Q pq qp. (pq, qp)"


388 
"\<Lambda>P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>


389 
(\<lambda>pq. \<forall>x. realizes x P \<longrightarrow> realizes (pq x) Q) \<cdot> pq \<cdot>


390 
(\<lambda>qp. \<forall>x. realizes x Q \<longrightarrow> realizes (qp x) P) \<cdot> qp \<bullet>


391 
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>


392 
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"


393 


394 
iffI (P): "\<lambda>P Q p. p"


395 
"\<Lambda>P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>


396 
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>


397 
(impI \<cdot> _ \<cdot> _ \<bullet> h2)"


398 


399 
iffI (Q): "\<lambda>P Q q. q"


400 
"\<Lambda>P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>


401 
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>


402 
(allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"


403 


404 
iffI: "Null"


405 
"\<Lambda>P Q. iffI \<cdot> _ \<cdot> _"


406 


407 
classical: "Null"


408 
"\<Lambda>P. classical \<cdot> _"


409 


410 


411 
subsection {* Induction on natural numbers *}


412 


413 
theorem nat_ind_realizer:


414 
"R f 0 \<Longrightarrow> (\<And>y h. R h y \<Longrightarrow> R (g y h) (Suc y)) \<Longrightarrow>


415 
(R::'a \<Rightarrow> nat \<Rightarrow> bool) (nat_rec f g x) x"


416 
proof 


417 
assume r1: "R f 0"


418 
assume r2: "\<And>y h. R h y \<Longrightarrow> R (g y h) (Suc y)"


419 
show "R (nat_rec f g x) x"


420 
proof (induct x)


421 
case 0


422 
from r1 show ?case by simp


423 
next


424 
case (Suc n)


425 
from Suc have "R (g n (nat_rec f g n)) (Suc n)" by (rule r2)


426 
thus ?case by simp


427 
qed


428 
qed


429 


430 
realizers


431 
NatDef.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"


432 
"\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"


433 


434 
NatDef.nat_induct: "Null"


435 
"\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"


436 


437 
Nat.nat.induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"


438 
"\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"


439 


440 
Nat.nat.induct: "Null"


441 
"\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"


442 


443 
end
