Added theory for setting up program extraction.
authorberghofe
Sun Jul 21 15:42:30 2002 +0200 (2002-07-21)
changeset 13403bc2b32ee62fd
parent 13402 e6e826bb8c3c
child 13404 eeac2bbfe958
Added theory for setting up program extraction.
src/HOL/Extraction.thy
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Extraction.thy	Sun Jul 21 15:42:30 2002 +0200
     1.3 @@ -0,0 +1,443 @@
     1.4 +(*  Title:      HOL/Extraction.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +*)
     1.9 +
    1.10 +header {* Program extraction for HOL *}
    1.11 +
    1.12 +theory Extraction = Datatype
    1.13 +files
    1.14 +  "Tools/rewrite_hol_proof.ML":
    1.15 +
    1.16 +subsection {* Setup *}
    1.17 +
    1.18 +ML_setup {*
    1.19 +  Context.>> (fn thy => thy |>
    1.20 +    Extraction.set_preprocessor (fn sg =>
    1.21 +      Proofterm.rewrite_proof_notypes
    1.22 +        ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
    1.23 +          ProofRewriteRules.rprocs true) o
    1.24 +      Proofterm.rewrite_proof (Sign.tsig_of sg)
    1.25 +        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true)))
    1.26 +*}
    1.27 +
    1.28 +lemmas [extraction_expand] =
    1.29 +  nat.exhaust atomize_eq atomize_all atomize_imp
    1.30 +  allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
    1.31 +  notE' impE' impE iffE imp_cong simp_thms
    1.32 +  induct_forall_eq induct_implies_eq induct_equal_eq
    1.33 +  induct_forall_def induct_implies_def
    1.34 +  induct_atomize induct_rulify1 induct_rulify2
    1.35 +
    1.36 +datatype sumbool = Left | Right
    1.37 +
    1.38 +subsection {* Type of extracted program *}
    1.39 +
    1.40 +extract_type
    1.41 +  "typeof (Trueprop P) \<equiv> typeof P"
    1.42 +
    1.43 +  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
    1.44 +     typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('Q))"
    1.45 +
    1.46 +  "typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE(Null))"
    1.47 +
    1.48 +  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
    1.49 +     typeof (P \<longrightarrow> Q) \<equiv> Type (TYPE('P \<Rightarrow> 'Q))"
    1.50 +
    1.51 +  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
    1.52 +     typeof (\<forall>x. P x) \<equiv> Type (TYPE(Null))"
    1.53 +
    1.54 +  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow>
    1.55 +     typeof (\<forall>x::'a. P x) \<equiv> Type (TYPE('a \<Rightarrow> 'P))"
    1.56 +
    1.57 +  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
    1.58 +     typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a))"
    1.59 +
    1.60 +  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE('P))) \<Longrightarrow>
    1.61 +     typeof (\<exists>x::'a. P x) \<equiv> Type (TYPE('a \<times> 'P))"
    1.62 +
    1.63 +  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
    1.64 +     typeof (P \<or> Q) \<equiv> Type (TYPE(sumbool))"
    1.65 +
    1.66 +  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
    1.67 +     typeof (P \<or> Q) \<equiv> Type (TYPE('Q option))"
    1.68 +
    1.69 +  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
    1.70 +     typeof (P \<or> Q) \<equiv> Type (TYPE('P option))"
    1.71 +
    1.72 +  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
    1.73 +     typeof (P \<or> Q) \<equiv> Type (TYPE('P + 'Q))"
    1.74 +
    1.75 +  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
    1.76 +     typeof (P \<and> Q) \<equiv> Type (TYPE('Q))"
    1.77 +
    1.78 +  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
    1.79 +     typeof (P \<and> Q) \<equiv> Type (TYPE('P))"
    1.80 +
    1.81 +  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow> typeof Q \<equiv> Type (TYPE('Q)) \<Longrightarrow>
    1.82 +     typeof (P \<and> Q) \<equiv> Type (TYPE('P \<times> 'Q))"
    1.83 +
    1.84 +  "typeof (P = Q) \<equiv> typeof ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))"
    1.85 +
    1.86 +  "typeof (x \<in> P) \<equiv> typeof P"
    1.87 +
    1.88 +subsection {* Realizability *}
    1.89 +
    1.90 +realizability
    1.91 +  "(realizes t (Trueprop P)) \<equiv> (Trueprop (realizes t P))"
    1.92 +
    1.93 +  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
    1.94 +     (realizes t (P \<longrightarrow> Q)) \<equiv> (realizes Null P \<longrightarrow> realizes t Q)"
    1.95 +
    1.96 +  "(typeof P) \<equiv> (Type (TYPE('P))) \<Longrightarrow>
    1.97 +   (typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
    1.98 +     (realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x::'P. realizes x P \<longrightarrow> realizes Null Q)"
    1.99 +
   1.100 +  "(realizes t (P \<longrightarrow> Q)) \<equiv> (\<forall>x. realizes x P \<longrightarrow> realizes (t x) Q)"
   1.101 +
   1.102 +  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
   1.103 +     (realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes Null (P x))"
   1.104 +
   1.105 +  "(realizes t (\<forall>x. P x)) \<equiv> (\<forall>x. realizes (t x) (P x))"
   1.106 +
   1.107 +  "(\<lambda>x. typeof (P x)) \<equiv> (\<lambda>x. Type (TYPE(Null))) \<Longrightarrow>
   1.108 +     (realizes t (\<exists>x. P x)) \<equiv> (realizes Null (P t))"
   1.109 +
   1.110 +  "(realizes t (\<exists>x. P x)) \<equiv> (realizes (snd t) (P (fst t)))"
   1.111 +
   1.112 +  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
   1.113 +   (typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
   1.114 +     (realizes t (P \<or> Q)) \<equiv>
   1.115 +     (case t of Left \<Rightarrow> realizes Null P | Right \<Rightarrow> realizes Null Q)"
   1.116 +
   1.117 +  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
   1.118 +     (realizes t (P \<or> Q)) \<equiv>
   1.119 +     (case t of None \<Rightarrow> realizes Null P | Some q \<Rightarrow> realizes q Q)"
   1.120 +
   1.121 +  "(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
   1.122 +     (realizes t (P \<or> Q)) \<equiv>
   1.123 +     (case t of None \<Rightarrow> realizes Null Q | Some p \<Rightarrow> realizes p P)"
   1.124 +
   1.125 +  "(realizes t (P \<or> Q)) \<equiv>
   1.126 +   (case t of Inl p \<Rightarrow> realizes p P | Inr q \<Rightarrow> realizes q Q)"
   1.127 +
   1.128 +  "(typeof P) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
   1.129 +     (realizes t (P \<and> Q)) \<equiv> (realizes Null P \<and> realizes t Q)"
   1.130 +
   1.131 +  "(typeof Q) \<equiv> (Type (TYPE(Null))) \<Longrightarrow>
   1.132 +     (realizes t (P \<and> Q)) \<equiv> (realizes t P \<and> realizes Null Q)"
   1.133 +
   1.134 +  "(realizes t (P \<and> Q)) \<equiv> (realizes (fst t) P \<and> realizes (snd t) Q)"
   1.135 +
   1.136 +  "typeof P \<equiv> Type (TYPE(Null)) \<Longrightarrow>
   1.137 +     realizes t (\<not> P) \<equiv> \<not> realizes Null P"
   1.138 +
   1.139 +  "typeof P \<equiv> Type (TYPE('P)) \<Longrightarrow>
   1.140 +     realizes t (\<not> P) \<equiv> (\<forall>x::'P. \<not> realizes x P)"
   1.141 +
   1.142 +  "typeof (P::bool) \<equiv> Type (TYPE(Null)) \<Longrightarrow>
   1.143 +   typeof Q \<equiv> Type (TYPE(Null)) \<Longrightarrow>
   1.144 +     realizes t (P = Q) \<equiv> realizes Null P = realizes Null Q"
   1.145 +
   1.146 +  "(realizes t (P = Q)) \<equiv> (realizes t ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)))"
   1.147 +
   1.148 +subsection {* Computational content of basic inference rules *}
   1.149 +
   1.150 +theorem disjE_realizer:
   1.151 +  assumes r: "case x of Inl p \<Rightarrow> P p | Inr q \<Rightarrow> Q q"
   1.152 +  and r1: "\<And>p. P p \<Longrightarrow> R (f p)" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)"
   1.153 +  shows "R (case x of Inl p \<Rightarrow> f p | Inr q \<Rightarrow> g q)"
   1.154 +proof (cases x)
   1.155 +  case Inl
   1.156 +  with r show ?thesis by simp (rule r1)
   1.157 +next
   1.158 +  case Inr
   1.159 +  with r show ?thesis by simp (rule r2)
   1.160 +qed
   1.161 +
   1.162 +theorem disjE_realizer2:
   1.163 +  assumes r: "case x of None \<Rightarrow> P | Some q \<Rightarrow> Q q"
   1.164 +  and r1: "P \<Longrightarrow> R f" and r2: "\<And>q. Q q \<Longrightarrow> R (g q)"
   1.165 +  shows "R (case x of None \<Rightarrow> f | Some q \<Rightarrow> g q)"
   1.166 +proof (cases x)
   1.167 +  case None
   1.168 +  with r show ?thesis by simp (rule r1)
   1.169 +next
   1.170 +  case Some
   1.171 +  with r show ?thesis by simp (rule r2)
   1.172 +qed
   1.173 +
   1.174 +theorem disjE_realizer3:
   1.175 +  assumes r: "case x of Left \<Rightarrow> P | Right \<Rightarrow> Q"
   1.176 +  and r1: "P \<Longrightarrow> R f" and r2: "Q \<Longrightarrow> R g"
   1.177 +  shows "R (case x of Left \<Rightarrow> f | Right \<Rightarrow> g)"
   1.178 +proof (cases x)
   1.179 +  case Left
   1.180 +  with r show ?thesis by simp (rule r1)
   1.181 +next
   1.182 +  case Right
   1.183 +  with r show ?thesis by simp (rule r2)
   1.184 +qed
   1.185 +
   1.186 +theorem conjI_realizer:
   1.187 +  "P p \<Longrightarrow> Q q \<Longrightarrow> P (fst (p, q)) \<and> Q (snd (p, q))"
   1.188 +  by simp
   1.189 +
   1.190 +theorem exI_realizer:
   1.191 +  "P x y \<Longrightarrow> P (fst (x, y)) (snd (x, y))" by simp
   1.192 +
   1.193 +realizers
   1.194 +  impI (P, Q): "\<lambda>P Q pq. pq"
   1.195 +    "\<Lambda>P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
   1.196 +
   1.197 +  impI (P): "Null"
   1.198 +    "\<Lambda>P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
   1.199 +
   1.200 +  impI (Q): "\<lambda>P Q q. q" "\<Lambda>P Q q. impI \<cdot> _ \<cdot> _"
   1.201 +
   1.202 +  impI: "Null" "\<Lambda>P Q. impI \<cdot> _ \<cdot> _"
   1.203 +
   1.204 +  mp (P, Q): "\<lambda>P Q pq. pq"
   1.205 +    "\<Lambda>P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.206 +
   1.207 +  mp (P): "Null"
   1.208 +    "\<Lambda>P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.209 +
   1.210 +  mp (Q): "\<lambda>P Q q. q" "\<Lambda>P Q q. mp \<cdot> _ \<cdot> _"
   1.211 +
   1.212 +  mp: "Null" "\<Lambda>P Q. mp \<cdot> _ \<cdot> _"
   1.213 +
   1.214 +  allI (P): "\<lambda>P p. p" "\<Lambda>P p. allI \<cdot> _"
   1.215 +
   1.216 +  allI: "Null" "\<Lambda>P. allI \<cdot> _"
   1.217 +
   1.218 +  spec (P): "\<lambda>P x p. p x" "\<Lambda>P x p. spec \<cdot> _ \<cdot> x"
   1.219 +
   1.220 +  spec: "Null" "\<Lambda>P x. spec \<cdot> _ \<cdot> x"
   1.221 +
   1.222 +  exI (P): "\<lambda>P x p. (x, p)" "\<Lambda>P. exI_realizer \<cdot> _"
   1.223 +
   1.224 +  exI: "\<lambda>P x. x" "\<Lambda>P x (h: _). h"
   1.225 +
   1.226 +  exE (P, Q): "\<lambda>P Q p pq. pq (fst p) (snd p)"
   1.227 +    "\<Lambda>P Q p (h1: _) pq (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"
   1.228 +
   1.229 +  exE (P): "Null"
   1.230 +    "\<Lambda>P Q p (h1: _) (h2: _). h2 \<cdot> (fst p) \<cdot> (snd p) \<bullet> h1"
   1.231 +
   1.232 +  exE (Q): "\<lambda>P Q x pq. pq x"
   1.233 +    "\<Lambda>P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
   1.234 +
   1.235 +  exE: "Null"
   1.236 +    "\<Lambda>P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
   1.237 +
   1.238 +  conjI (P, Q): "\<lambda>P Q p q. (p, q)"
   1.239 +    "\<Lambda>P Q p (h: _) q. conjI_realizer \<cdot>
   1.240 +       (\<lambda>p. realizes p P) \<cdot> p \<cdot> (\<lambda>q. realizes q Q) \<cdot> q \<bullet> h"
   1.241 +
   1.242 +  conjI (P): "\<lambda>P Q p. p"
   1.243 +    "\<Lambda>P Q p. conjI \<cdot> _ \<cdot> _"
   1.244 +
   1.245 +  conjI (Q): "\<lambda>P Q q. q"
   1.246 +    "\<Lambda>P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
   1.247 +
   1.248 +  conjI: "Null"
   1.249 +    "\<Lambda>P Q. conjI \<cdot> _ \<cdot> _"
   1.250 +
   1.251 +  conjunct1 (P, Q): "\<lambda>P Q. fst"
   1.252 +    "\<Lambda>P Q pq. conjunct1 \<cdot> _ \<cdot> _"
   1.253 +
   1.254 +  conjunct1 (P): "\<lambda>P Q p. p"
   1.255 +    "\<Lambda>P Q p. conjunct1 \<cdot> _ \<cdot> _"
   1.256 +
   1.257 +  conjunct1 (Q): "Null"
   1.258 +    "\<Lambda>P Q q. conjunct1 \<cdot> _ \<cdot> _"
   1.259 +
   1.260 +  conjunct1: "Null"
   1.261 +    "\<Lambda>P Q. conjunct1 \<cdot> _ \<cdot> _"
   1.262 +
   1.263 +  conjunct2 (P, Q): "\<lambda>P Q. snd"
   1.264 +    "\<Lambda>P Q pq. conjunct2 \<cdot> _ \<cdot> _"
   1.265 +
   1.266 +  conjunct2 (P): "Null"
   1.267 +    "\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.268 +
   1.269 +  conjunct2 (Q): "\<lambda>P Q p. p"
   1.270 +    "\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.271 +
   1.272 +  conjunct2: "Null"
   1.273 +    "\<Lambda>P Q. conjunct2 \<cdot> _ \<cdot> _"
   1.274 +
   1.275 +  disjI1 (P, Q): "\<lambda>P Q. Inl"
   1.276 +    "\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> (\<lambda>p. realizes p P) \<cdot> _ \<cdot> p)"
   1.277 +
   1.278 +  disjI1 (P): "\<lambda>P Q. Some"
   1.279 +    "\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>p. realizes p P) \<cdot> p)"
   1.280 +
   1.281 +  disjI1 (Q): "\<lambda>P Q. None"
   1.282 +    "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
   1.283 +
   1.284 +  disjI1: "\<lambda>P Q. Left"
   1.285 +    "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)"
   1.286 +
   1.287 +  disjI2 (P, Q): "\<lambda>Q P. Inr"
   1.288 +    "\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)"
   1.289 +
   1.290 +  disjI2 (P): "\<lambda>Q P. None"
   1.291 +    "\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
   1.292 +
   1.293 +  disjI2 (Q): "\<lambda>Q P. Some"
   1.294 +    "\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> (\<lambda>q. realizes q Q) \<cdot> q)"
   1.295 +
   1.296 +  disjI2: "\<lambda>Q P. Right"
   1.297 +    "\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)"
   1.298 +
   1.299 +  disjE (P, Q, R): "\<lambda>P Q R pq pr qr.
   1.300 +     (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
   1.301 +    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.
   1.302 +       disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.303 +
   1.304 +  disjE (Q, R): "\<lambda>P Q R pq pr qr.
   1.305 +     (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)"
   1.306 +    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.
   1.307 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.308 +
   1.309 +  disjE (P, R): "\<lambda>P Q R pq pr qr.
   1.310 +     (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)"
   1.311 +    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr (h3: _).
   1.312 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.313 +
   1.314 +  disjE (R): "\<lambda>P Q R pq pr qr.
   1.315 +     (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)"
   1.316 +    "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr.
   1.317 +       disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes r R) \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.318 +
   1.319 +  disjE (P, Q): "Null"
   1.320 +    "\<Lambda>P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"
   1.321 +
   1.322 +  disjE (Q): "Null"
   1.323 +    "\<Lambda>P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"
   1.324 +
   1.325 +  disjE (P): "Null"
   1.326 +    "\<Lambda>P Q R pq (h1: _) (h2: _) (h3: _).
   1.327 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.328 +
   1.329 +  disjE: "Null"
   1.330 +    "\<Lambda>P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>r. realizes Null R) \<cdot> _ \<cdot> _"
   1.331 +
   1.332 +  FalseE (P): "\<lambda>P. arbitrary"
   1.333 +    "\<Lambda>P. FalseE \<cdot> _"
   1.334 +
   1.335 +  FalseE: "Null"
   1.336 +    "\<Lambda>P. FalseE \<cdot> _"
   1.337 +
   1.338 +  notI (P): "Null"
   1.339 +    "\<Lambda>P (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
   1.340 +
   1.341 +  notI: "Null"
   1.342 +    "\<Lambda>P. notI \<cdot> _"
   1.343 +
   1.344 +  notE (P, R): "\<lambda>P R p. arbitrary"
   1.345 +    "\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.346 +
   1.347 +  notE (P): "Null"
   1.348 +    "\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.349 +
   1.350 +  notE (R): "\<lambda>P R. arbitrary"
   1.351 +    "\<Lambda>P R. notE \<cdot> _ \<cdot> _"
   1.352 +
   1.353 +  notE: "Null"
   1.354 +    "\<Lambda>P R. notE \<cdot> _ \<cdot> _"
   1.355 +
   1.356 +  subst (P): "\<lambda>s t P ps. ps"
   1.357 +    "\<Lambda>s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes ps (P x)) \<bullet> h"
   1.358 +
   1.359 +  subst: "Null"
   1.360 +    "\<Lambda>s t P. subst \<cdot> s \<cdot> t \<cdot> (\<lambda>x. realizes Null (P x))"
   1.361 +
   1.362 +  iffD1 (P, Q): "\<lambda>Q P. fst"
   1.363 +    "\<Lambda>Q P pq (h: _) p.
   1.364 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.365 +
   1.366 +  iffD1 (P): "\<lambda>Q P p. p"
   1.367 +    "\<Lambda>Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.368 +
   1.369 +  iffD1 (Q): "Null"
   1.370 +    "\<Lambda>Q P q1 (h: _) q2.
   1.371 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.372 +
   1.373 +  iffD1: "Null"
   1.374 +    "\<Lambda>Q P. iffD1 \<cdot> _ \<cdot> _"
   1.375 +
   1.376 +  iffD2 (P, Q): "\<lambda>P Q. snd"
   1.377 +    "\<Lambda>P Q pq (h: _) q.
   1.378 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.379 +
   1.380 +  iffD2 (P): "\<lambda>P Q p. p"
   1.381 +    "\<Lambda>P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.382 +
   1.383 +  iffD2 (Q): "Null"
   1.384 +    "\<Lambda>P Q q1 (h: _) q2.
   1.385 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.386 +
   1.387 +  iffD2: "Null"
   1.388 +    "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _"
   1.389 +
   1.390 +  iffI (P, Q): "\<lambda>P Q pq qp. (pq, qp)"
   1.391 +    "\<Lambda>P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
   1.392 +       (\<lambda>pq. \<forall>x. realizes x P \<longrightarrow> realizes (pq x) Q) \<cdot> pq \<cdot>
   1.393 +       (\<lambda>qp. \<forall>x. realizes x Q \<longrightarrow> realizes (qp x) P) \<cdot> qp \<bullet>
   1.394 +       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.395 +       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.396 +
   1.397 +  iffI (P): "\<lambda>P Q p. p"
   1.398 +    "\<Lambda>P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.399 +       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.400 +       (impI \<cdot> _ \<cdot> _ \<bullet> h2)"
   1.401 +
   1.402 +  iffI (Q): "\<lambda>P Q q. q"
   1.403 +    "\<Lambda>P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.404 +       (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>
   1.405 +       (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.406 +
   1.407 +  iffI: "Null"
   1.408 +    "\<Lambda>P Q. iffI \<cdot> _ \<cdot> _"
   1.409 +
   1.410 +  classical: "Null"
   1.411 +    "\<Lambda>P. classical \<cdot> _"
   1.412 +
   1.413 +
   1.414 +subsection {* Induction on natural numbers *}
   1.415 +
   1.416 +theorem nat_ind_realizer:
   1.417 +  "R f 0 \<Longrightarrow> (\<And>y h. R h y \<Longrightarrow> R (g y h) (Suc y)) \<Longrightarrow>
   1.418 +     (R::'a \<Rightarrow> nat \<Rightarrow> bool) (nat_rec f g x) x"
   1.419 +proof -
   1.420 +  assume r1: "R f 0"
   1.421 +  assume r2: "\<And>y h. R h y \<Longrightarrow> R (g y h) (Suc y)"
   1.422 +  show "R (nat_rec f g x) x"
   1.423 +  proof (induct x)
   1.424 +    case 0
   1.425 +    from r1 show ?case by simp
   1.426 +  next
   1.427 +    case (Suc n)
   1.428 +    from Suc have "R (g n (nat_rec f g n)) (Suc n)" by (rule r2)
   1.429 +    thus ?case by simp
   1.430 +  qed
   1.431 +qed
   1.432 +
   1.433 +realizers
   1.434 +  NatDef.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
   1.435 +    "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
   1.436 +
   1.437 +  NatDef.nat_induct: "Null"
   1.438 +    "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"
   1.439 +
   1.440 +  Nat.nat.induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
   1.441 +    "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
   1.442 +
   1.443 +  Nat.nat.induct: "Null"
   1.444 +    "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"
   1.445 +
   1.446 +end
     2.1 --- a/src/HOL/IsaMakefile	Sun Jul 21 15:37:04 2002 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Sun Jul 21 15:42:30 2002 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    HOL-AxClasses \
     2.5    HOL-Bali \
     2.6    HOL-CTL \
     2.7 +  HOL-Extraction \
     2.8    HOL-GroupTheory \
     2.9        HOL-Real-HahnBanach \
    2.10        HOL-Real-ex \
    2.11 @@ -80,7 +81,8 @@
    2.12    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    2.13    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
    2.14    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
    2.15 -  Divides.thy Finite_Set.ML Finite_Set.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
    2.16 +  Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
    2.17 +  Fun.ML Fun.thy Gfp.ML Gfp.thy \
    2.18    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
    2.19    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    2.20    Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \
    2.21 @@ -99,7 +101,8 @@
    2.22    Tools/datatype_rep_proofs.ML \
    2.23    Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \
    2.24    Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
    2.25 -  Tools/record_package.ML Tools/split_rule.ML Tools/typedef_package.ML \
    2.26 +  Tools/record_package.ML Tools/rewrite_hol_proof.ML \
    2.27 +  Tools/split_rule.ML Tools/typedef_package.ML \
    2.28    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    2.29    Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
    2.30    Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
    2.31 @@ -537,6 +540,17 @@
    2.32  	@$(ISATOOL) usedir $(OUT)/HOL CTL
    2.33  
    2.34  
    2.35 +## HOL-Extraction
    2.36 +
    2.37 +HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
    2.38 +
    2.39 +$(LOG)/HOL-Extraction.gz: $(OUT)/HOL \
    2.40 +  Extraction/Higman.thy Extraction/ROOT.ML Extraction/QuotRem.thy \
    2.41 +  Extraction/Warshall.thy Extraction/document/root.tex \
    2.42 +  Extraction/document/root.bib
    2.43 +	@$(ISATOOL) usedir $(OUT)/HOL Extraction
    2.44 +
    2.45 +
    2.46  ## HOL-IOA
    2.47  
    2.48  HOL-IOA: HOL $(LOG)/HOL-IOA.gz
     3.1 --- a/src/HOL/Main.thy	Sun Jul 21 15:37:04 2002 +0200
     3.2 +++ b/src/HOL/Main.thy	Sun Jul 21 15:42:30 2002 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  
     3.5  header {* Main HOL *}
     3.6  
     3.7 -theory Main = Map + Hilbert_Choice:
     3.8 +theory Main = Map + Hilbert_Choice + Extraction:
     3.9  
    3.10  text {*
    3.11    Theory @{text Main} includes everything.  Note that theory @{text
     4.1 --- a/src/HOL/ROOT.ML	Sun Jul 21 15:37:04 2002 +0200
     4.2 +++ b/src/HOL/ROOT.ML	Sun Jul 21 15:42:30 2002 +0200
     4.3 @@ -42,3 +42,5 @@
     4.4  print_depth 8;
     4.5  
     4.6  Goal "True";  (*leave subgoal package empty*)
     4.7 +
     4.8 +val HOL_proofs = !proofs;