Adapted to new format of proof terms containing explicit proofs of class membership.
authorberghofe
Tue Jun 01 11:13:09 2010 +0200 (2010-06-01)
changeset 37233b78f31ca4675
parent 37232 c10fb22a5e0c
child 37234 95bfc649fe19
Adapted to new format of proof terms containing explicit proofs of class membership.
src/HOL/Extraction.thy
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/rewrite_hol_proof.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
     1.1 --- a/src/HOL/Extraction.thy	Tue Jun 01 11:04:49 2010 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Tue Jun 01 11:13:09 2010 +0200
     1.3 @@ -18,7 +18,8 @@
     1.4        Proofterm.rewrite_proof_notypes
     1.5          ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
     1.6        Proofterm.rewrite_proof thy
     1.7 -        (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
     1.8 +        (RewriteHOLProof.rews,
     1.9 +         ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
    1.10        ProofRewriteRules.elim_vars (curry Const @{const_name default}))
    1.11  *}
    1.12  
    1.13 @@ -199,223 +200,212 @@
    1.14  theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
    1.15    (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
    1.16  
    1.17 -setup {*
    1.18 -  Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"})
    1.19 -*}
    1.20 -
    1.21  realizers
    1.22    impI (P, Q): "\<lambda>pq. pq"
    1.23 -    "\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.24 +    "\<Lambda> (c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.25  
    1.26    impI (P): "Null"
    1.27 -    "\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.28 +    "\<Lambda> (c: _) P Q (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.29  
    1.30 -  impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _"
    1.31 +  impI (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. impI \<cdot> _ \<cdot> _"
    1.32  
    1.33    impI: "Null" "impI"
    1.34  
    1.35    mp (P, Q): "\<lambda>pq. pq"
    1.36 -    "\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
    1.37 +    "\<Lambda> (c: _) (d: _) P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
    1.38  
    1.39    mp (P): "Null"
    1.40 -    "\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
    1.41 +    "\<Lambda> (c: _) P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
    1.42  
    1.43 -  mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _"
    1.44 +  mp (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. mp \<cdot> _ \<cdot> _"
    1.45  
    1.46    mp: "Null" "mp"
    1.47  
    1.48 -  allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _"
    1.49 +  allI (P): "\<lambda>p. p" "\<Lambda> (c: _) P (d: _) p. allI \<cdot> _ \<bullet> d"
    1.50  
    1.51    allI: "Null" "allI"
    1.52  
    1.53 -  spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x"
    1.54 +  spec (P): "\<lambda>x p. p x" "\<Lambda> (c: _) P x (d: _) p. spec \<cdot> _ \<cdot> x \<bullet> d"
    1.55  
    1.56    spec: "Null" "spec"
    1.57  
    1.58 -  exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x"
    1.59 +  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"
    1.60  
    1.61 -  exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h"
    1.62 +  exI: "\<lambda>x. x" "\<Lambda> P x (c: _) (h: _). h"
    1.63  
    1.64    exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y"
    1.65 -    "\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h"
    1.66 +    "\<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"
    1.67  
    1.68    exE (P): "Null"
    1.69 -    "\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _"
    1.70 +    "\<Lambda> (c: _) P Q (d: _) p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d"
    1.71  
    1.72    exE (Q): "\<lambda>x pq. pq x"
    1.73 -    "\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
    1.74 +    "\<Lambda> (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
    1.75  
    1.76    exE: "Null"
    1.77 -    "\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
    1.78 +    "\<Lambda> P Q (c: _) x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
    1.79  
    1.80    conjI (P, Q): "Pair"
    1.81 -    "\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h"
    1.82 +    "\<Lambda> (c: _) (d: _) P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> c \<bullet> d \<bullet> h"
    1.83  
    1.84    conjI (P): "\<lambda>p. p"
    1.85 -    "\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _"
    1.86 +    "\<Lambda> (c: _) P Q p. conjI \<cdot> _ \<cdot> _"
    1.87  
    1.88    conjI (Q): "\<lambda>q. q"
    1.89 -    "\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
    1.90 +    "\<Lambda> (c: _) P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
    1.91  
    1.92    conjI: "Null" "conjI"
    1.93  
    1.94    conjunct1 (P, Q): "fst"
    1.95 -    "\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _"
    1.96 +    "\<Lambda> (c: _) (d: _) P Q pq. conjunct1 \<cdot> _ \<cdot> _"
    1.97  
    1.98    conjunct1 (P): "\<lambda>p. p"
    1.99 -    "\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _"
   1.100 +    "\<Lambda> (c: _) P Q p. conjunct1 \<cdot> _ \<cdot> _"
   1.101  
   1.102    conjunct1 (Q): "Null"
   1.103 -    "\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _"
   1.104 +    "\<Lambda> (c: _) P Q q. conjunct1 \<cdot> _ \<cdot> _"
   1.105  
   1.106    conjunct1: "Null" "conjunct1"
   1.107  
   1.108    conjunct2 (P, Q): "snd"
   1.109 -    "\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _"
   1.110 +    "\<Lambda> (c: _) (d: _) P Q pq. conjunct2 \<cdot> _ \<cdot> _"
   1.111  
   1.112    conjunct2 (P): "Null"
   1.113 -    "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.114 +    "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.115  
   1.116    conjunct2 (Q): "\<lambda>p. p"
   1.117 -    "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.118 +    "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
   1.119  
   1.120    conjunct2: "Null" "conjunct2"
   1.121  
   1.122    disjI1 (P, Q): "Inl"
   1.123 -    "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)"
   1.124 +    "\<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)"
   1.125  
   1.126    disjI1 (P): "Some"
   1.127 -    "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)"
   1.128 +    "\<Lambda> (c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
   1.129  
   1.130    disjI1 (Q): "None"
   1.131 -    "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
   1.132 +    "\<Lambda> (c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
   1.133  
   1.134    disjI1: "Left"
   1.135 -    "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)"
   1.136 +    "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
   1.137  
   1.138    disjI2 (P, Q): "Inr"
   1.139 -    "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
   1.140 +    "\<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)"
   1.141  
   1.142    disjI2 (P): "None"
   1.143 -    "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
   1.144 +    "\<Lambda> (c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
   1.145  
   1.146    disjI2 (Q): "Some"
   1.147 -    "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
   1.148 +    "\<Lambda> (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
   1.149  
   1.150    disjI2: "Right"
   1.151 -    "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)"
   1.152 +    "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
   1.153  
   1.154    disjE (P, Q, R): "\<lambda>pq pr qr.
   1.155       (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
   1.156 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
   1.157 -       disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.158 +    "\<Lambda> (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr.
   1.159 +       disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> e \<bullet> h1 \<bullet> h2"
   1.160  
   1.161    disjE (Q, R): "\<lambda>pq pr qr.
   1.162       (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)"
   1.163 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
   1.164 -       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.165 +    "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr.
   1.166 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h2"
   1.167  
   1.168    disjE (P, R): "\<lambda>pq pr qr.
   1.169       (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)"
   1.170 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _).
   1.171 -       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.172 +    "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _).
   1.173 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.174  
   1.175    disjE (R): "\<lambda>pq pr qr.
   1.176       (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)"
   1.177 -    "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
   1.178 -       disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
   1.179 +    "\<Lambda> (c: _) P Q R pq (h1: _) pr (h2: _) qr.
   1.180 +       disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> h1 \<bullet> h2"
   1.181  
   1.182    disjE (P, Q): "Null"
   1.183 -    "\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
   1.184 +    "\<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"
   1.185  
   1.186    disjE (Q): "Null"
   1.187 -    "\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
   1.188 +    "\<Lambda> (c: _) P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool"
   1.189  
   1.190    disjE (P): "Null"
   1.191 -    "\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _).
   1.192 -       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.193 +    "\<Lambda> (c: _) P Q R pq (h1: _) (h2: _) (h3: _).
   1.194 +       disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool \<bullet> h1 \<bullet> h3 \<bullet> h2"
   1.195  
   1.196    disjE: "Null"
   1.197 -    "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
   1.198 +    "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> arity_type_bool"
   1.199  
   1.200    FalseE (P): "default"
   1.201 -    "\<Lambda> P. FalseE \<cdot> _"
   1.202 +    "\<Lambda> (c: _) P. FalseE \<cdot> _"
   1.203  
   1.204    FalseE: "Null" "FalseE"
   1.205  
   1.206    notI (P): "Null"
   1.207 -    "\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
   1.208 +    "\<Lambda> (c: _) P (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
   1.209  
   1.210    notI: "Null" "notI"
   1.211  
   1.212    notE (P, R): "\<lambda>p. default"
   1.213 -    "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.214 +    "\<Lambda> (c: _) (d: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
   1.215  
   1.216    notE (P): "Null"
   1.217 -    "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
   1.218 +    "\<Lambda> (c: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
   1.219  
   1.220    notE (R): "default"
   1.221 -    "\<Lambda> P R. notE \<cdot> _ \<cdot> _"
   1.222 +    "\<Lambda> (c: _) P R. notE \<cdot> _ \<cdot> _"
   1.223  
   1.224    notE: "Null" "notE"
   1.225  
   1.226    subst (P): "\<lambda>s t ps. ps"
   1.227 -    "\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h"
   1.228 +    "\<Lambda> (c: _) s t P (d: _) (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> d \<bullet> h"
   1.229  
   1.230    subst: "Null" "subst"
   1.231  
   1.232    iffD1 (P, Q): "fst"
   1.233 -    "\<Lambda> Q P pq (h: _) p.
   1.234 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.235 +    "\<Lambda> (d: _) (c: _) Q P pq (h: _) p.
   1.236 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> d \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.237  
   1.238    iffD1 (P): "\<lambda>p. p"
   1.239 -    "\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.240 +    "\<Lambda> (c: _) Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.241  
   1.242    iffD1 (Q): "Null"
   1.243 -    "\<Lambda> Q P q1 (h: _) q2.
   1.244 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.245 +    "\<Lambda> (c: _) Q P q1 (h: _) q2.
   1.246 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.247  
   1.248    iffD1: "Null" "iffD1"
   1.249  
   1.250    iffD2 (P, Q): "snd"
   1.251 -    "\<Lambda> P Q pq (h: _) q.
   1.252 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.253 +    "\<Lambda> (c: _) (d: _) P Q pq (h: _) q.
   1.254 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> d \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.255  
   1.256    iffD2 (P): "\<lambda>p. p"
   1.257 -    "\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.258 +    "\<Lambda> (c: _) P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
   1.259  
   1.260    iffD2 (Q): "Null"
   1.261 -    "\<Lambda> P Q q1 (h: _) q2.
   1.262 -       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.263 +    "\<Lambda> (c: _) P Q q1 (h: _) q2.
   1.264 +       mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
   1.265  
   1.266    iffD2: "Null" "iffD2"
   1.267  
   1.268    iffI (P, Q): "Pair"
   1.269 -    "\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
   1.270 +    "\<Lambda> (c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
   1.271         (\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot>
   1.272         (\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet>
   1.273 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.274 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.275 +       (arity_type_fun \<bullet> c \<bullet> d) \<bullet>
   1.276 +       (arity_type_fun \<bullet> d \<bullet> c) \<bullet>
   1.277 +       (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.278 +       (allI \<cdot> _ \<bullet> d \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.279  
   1.280    iffI (P): "\<lambda>p. p"
   1.281 -    "\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.282 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.283 +    "\<Lambda> (c: _) P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.284 +       (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
   1.285         (impI \<cdot> _ \<cdot> _ \<bullet> h2)"
   1.286  
   1.287    iffI (Q): "\<lambda>q. q"
   1.288 -    "\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.289 +    "\<Lambda> (c: _) P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
   1.290         (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>
   1.291 -       (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.292 +       (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
   1.293  
   1.294    iffI: "Null" "iffI"
   1.295  
   1.296 -(*
   1.297 -  classical: "Null"
   1.298 -    "\<Lambda> P. classical \<cdot> _"
   1.299 -*)
   1.300 -
   1.301 -setup {*
   1.302 -  Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"})
   1.303 -*}
   1.304 -
   1.305  end
     2.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 01 11:04:49 2010 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 01 11:13:09 2010 +0200
     2.3 @@ -22,10 +22,6 @@
     2.4      in map (fn ks => i::ks) is @ is end
     2.5    else [[]];
     2.6  
     2.7 -fun forall_intr_prf (t, prf) =
     2.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     2.9 -  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    2.10 -
    2.11  fun prf_of thm =
    2.12    Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    2.13  
    2.14 @@ -130,12 +126,12 @@
    2.15  
    2.16      val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
    2.17      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    2.18 -    val ivs1 = map Var (filter_out (fn (_, T) =>  (* FIXME set (!??) *)
    2.19 -      member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
    2.20 +    val ivs1 = map Var (filter_out (fn (_, T) =>
    2.21 +      @{type_name bool} = tname_of (body_type T)) ivs);
    2.22      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
    2.23  
    2.24      val prf =
    2.25 -      List.foldr forall_intr_prf
    2.26 +      Extraction.abs_corr_shyps thy' induct vs ivs2
    2.27          (fold_rev (fn (f, p) => fn prf =>
    2.28            (case head_of (strip_abs_body f) of
    2.29               Free (s, T) =>
    2.30 @@ -145,7 +141,7 @@
    2.31                 end
    2.32            | _ => AbsP ("H", SOME p, prf)))
    2.33              (rec_fns ~~ prems_of thm)
    2.34 -            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
    2.35 +            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    2.36  
    2.37      val r' =
    2.38        if null is then r
    2.39 @@ -198,18 +194,21 @@
    2.40        ||> Sign.restore_naming thy;
    2.41  
    2.42      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    2.43 -    val prf = forall_intr_prf (y, forall_intr_prf (P,
    2.44 -      fold_rev (fn (p, r) => fn prf =>
    2.45 -          forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
    2.46 +    val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
    2.47 +      (fold_rev (fn (p, r) => fn prf =>
    2.48 +          Proofterm.forall_intr_proof' (Logic.varify_global r)
    2.49 +            (AbsP ("H", SOME (Logic.varify_global p), prf)))
    2.50          (prems ~~ rs)
    2.51 -        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
    2.52 +        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    2.53 +    val prf' = Extraction.abs_corr_shyps thy' exhaust []
    2.54 +      (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
    2.55      val r' = Logic.varify_global (Abs ("y", T,
    2.56        list_abs (map dest_Free rs, list_comb (r,
    2.57          map Bound ((length rs - 1 downto 0) @ [length rs])))));
    2.58  
    2.59    in Extraction.add_realizers_i
    2.60      [(exh_name, (["P"], r', prf)),
    2.61 -     (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
    2.62 +     (exh_name, ([], Extraction.nullt, prf'))] thy'
    2.63    end;
    2.64  
    2.65  fun add_dt_realizers config names thy =
     3.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:04:49 2010 +0200
     3.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:13:09 2010 +0200
     3.3 @@ -21,18 +21,12 @@
     3.4      [name] => name
     3.5    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
     3.6  
     3.7 -val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
     3.8 -
     3.9  fun prf_of thm =
    3.10    let
    3.11      val thy = Thm.theory_of_thm thm;
    3.12      val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    3.13    in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    3.14  
    3.15 -fun forall_intr_prf t prf =
    3.16 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    3.17 -  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    3.18 -
    3.19  fun subsets [] = [[]]
    3.20    | subsets (x::xs) =
    3.21        let val ys = subsets xs
    3.22 @@ -55,15 +49,19 @@
    3.23        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    3.24    | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
    3.25  
    3.26 -fun relevant_vars prop = List.foldr (fn
    3.27 -      (Var ((a, i), T), vs) => (case strip_type T of
    3.28 +fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
    3.29 +     (case strip_type T of
    3.30          (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
    3.31 -      | _ => vs)
    3.32 -    | (_, vs) => vs) [] (OldTerm.term_vars prop);
    3.33 +      | _ => vs)) (Term.add_vars prop []) [];
    3.34 +
    3.35 +val attach_typeS = map_types (map_atyps
    3.36 +  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
    3.37 +    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
    3.38 +    | T => T));
    3.39  
    3.40  fun dt_of_intrs thy vs nparms intrs =
    3.41    let
    3.42 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
    3.43 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
    3.44      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
    3.45        (Logic.strip_imp_concl (prop_of (hd intrs))));
    3.46      val params = map dest_Var (take nparms ts);
    3.47 @@ -84,7 +82,7 @@
    3.48  fun gen_rvar vs (t as Var ((a, 0), T)) =
    3.49        if body_type T <> HOLogic.boolT then t else
    3.50          let
    3.51 -          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
    3.52 +          val U = TVar (("'" ^ a, 0), [])
    3.53            val Ts = binder_types T;
    3.54            val i = length Ts;
    3.55            val xs = map (pair "x") Ts;
    3.56 @@ -98,8 +96,9 @@
    3.57  
    3.58  fun mk_realizes_eqn n vs nparms intrs =
    3.59    let
    3.60 -    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
    3.61 -    val iTs = OldTerm.term_tvars concl;
    3.62 +    val intr = map_types Type.strip_sorts (prop_of (hd intrs));
    3.63 +    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
    3.64 +    val iTs = rev (Term.add_tvars intr []);
    3.65      val Tvs = map TVar iTs;
    3.66      val (h as Const (s, T), us) = strip_comb concl;
    3.67      val params = List.take (us, nparms);
    3.68 @@ -110,7 +109,7 @@
    3.69        (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
    3.70      val rT = if n then Extraction.nullT
    3.71        else Type (space_implode "_" (s ^ "T" :: vs),
    3.72 -        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
    3.73 +        map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
    3.74      val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
    3.75      val S = list_comb (h, params @ xs);
    3.76      val rvs = relevant_vars S;
    3.77 @@ -121,7 +120,7 @@
    3.78        let val T = (the o AList.lookup (op =) rvs) v
    3.79        in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
    3.80          Extraction.mk_typ (if n then Extraction.nullT
    3.81 -          else TVar (("'" ^ v, 0), HOLogic.typeS)))
    3.82 +          else TVar (("'" ^ v, 0), [])))
    3.83        end;
    3.84  
    3.85      val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
    3.86 @@ -261,12 +260,12 @@
    3.87      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
    3.88      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
    3.89      val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
    3.90 -    val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
    3.91 -    val rlz'' = fold_rev Logic.all vs2 rlz
    3.92 +    val rlz' = fold_rev Logic.all rs (prop_of rrule)
    3.93    in (name, (vs,
    3.94      if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
    3.95 -    ProofRewriteRules.un_hhf_proof rlz' rlz''
    3.96 -      (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
    3.97 +    Extraction.abs_corr_shyps thy rule vs vs2
    3.98 +      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
    3.99 +         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
   3.100    end;
   3.101  
   3.102  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
   3.103 @@ -275,7 +274,7 @@
   3.104    let
   3.105      val qualifier = Long_Name.qualifier (name_of_thm induct);
   3.106      val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
   3.107 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
   3.108 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
   3.109      val ar = length vs + length iTs;
   3.110      val params = Inductive.params_of raw_induct;
   3.111      val arities = Inductive.arities_of raw_induct;
   3.112 @@ -297,8 +296,6 @@
   3.113      val thy1' = thy1 |>
   3.114        Theory.copy |>
   3.115        Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
   3.116 -      fold (fn s => AxClass.axiomatize_arity
   3.117 -        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   3.118          Extraction.add_typeof_eqns_i ty_eqs;
   3.119      val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
   3.120        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   3.121 @@ -328,10 +325,10 @@
   3.122          end
   3.123        else (replicate (length rs) Extraction.nullt, (recs, dummies)))
   3.124          rss (rec_thms, dummies);
   3.125 -    val rintrs = map (fn (intr, c) => Envir.eta_contract
   3.126 +    val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
   3.127        (Extraction.realizes_of thy2 vs
   3.128          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   3.129 -          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
   3.130 +          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
   3.131              (maps snd rss ~~ flat constrss);
   3.132      val (rlzpreds, rlzpreds') =
   3.133        rintrs |> map (fn rintr =>
   3.134 @@ -390,7 +387,9 @@
   3.135          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   3.136            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
   3.137          val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
   3.138 -        val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
   3.139 +        val thm = Goal.prove_global thy []
   3.140 +          (map attach_typeS prems) (attach_typeS concl)
   3.141 +          (fn {prems, ...} => EVERY
   3.142            [rtac (#raw_induct ind_info) 1,
   3.143             rewrite_goals_tac rews,
   3.144             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   3.145 @@ -408,10 +407,10 @@
   3.146        in
   3.147          Extraction.add_realizers_i
   3.148            (map (fn (((ind, corr), rlz), r) =>
   3.149 -              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
   3.150 +              mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
   3.151              realizers @ (case realizers of
   3.152               [(((ind, corr), rlz), r)] =>
   3.153 -               [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
   3.154 +               [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
   3.155                    ind, corr, rlz, r)]
   3.156             | _ => [])) thy''
   3.157        end;
   3.158 @@ -445,7 +444,7 @@
   3.159              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   3.160              [Bound (length prems)]));
   3.161          val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
   3.162 -        val rlz' = strip_all (Logic.unvarify_global rlz);
   3.163 +        val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
   3.164          val rews = map mk_meta_eq case_thms;
   3.165          val thm = Goal.prove_global thy []
   3.166            (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
   3.167 @@ -488,7 +487,7 @@
   3.168      val vss = sort (int_ord o pairself length)
   3.169        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   3.170    in
   3.171 -    fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
   3.172 +    fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
   3.173    end
   3.174  
   3.175  fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
     4.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 01 11:04:49 2010 +0200
     4.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 01 11:13:09 2010 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  signature REWRITE_HOL_PROOF =
     4.5  sig
     4.6    val rews: (Proofterm.proof * Proofterm.proof) list
     4.7 -  val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     4.8 +  val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     4.9  end;
    4.10  
    4.11  structure RewriteHOLProof : REWRITE_HOL_PROOF =
    4.12 @@ -16,7 +16,7 @@
    4.13  open Proofterm;
    4.14  
    4.15  val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
    4.16 -    Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
    4.17 +    Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
    4.18  
    4.19    (** eliminate meta-equality rules **)
    4.20  
    4.21 @@ -24,237 +24,258 @@
    4.22   \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
    4.23   \      (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==  \
    4.24   \  (iffD1 % A % B %%  \
    4.25 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
    4.26 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    4.27  
    4.28     "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
    4.29   \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
    4.30   \      (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==  \
    4.31   \  (iffD2 % A % B %%  \
    4.32 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
    4.33 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    4.34  
    4.35 -   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
    4.36 +   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %%  \
    4.37   \    (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==  \
    4.38   \  (cong % TYPE('T) % TYPE('U) % f % g % x % y %%  \
    4.39 - \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %%  \
    4.40 - \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
    4.41 -
    4.42 -   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %%  \
    4.43 - \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
    4.44 - \  (HOL.trans % TYPE('T) % x % y % z %%  \
    4.45 - \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %%  \
    4.46 - \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
    4.47 + \    (OfClass type_class % TYPE('T)) %% prfU %%  \
    4.48 + \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %%  \
    4.49 + \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))",
    4.50  
    4.51 -   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) ==  \
    4.52 - \  (HOL.refl % TYPE('T) % x)",
    4.53 +   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %%  \
    4.54 + \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
    4.55 + \  (HOL.trans % TYPE('T) % x % y % z %% prfT %%  \
    4.56 + \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %%  \
    4.57 + \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))",
    4.58  
    4.59 -   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    4.60 +   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) ==  \
    4.61 + \  (HOL.refl % TYPE('T) % x %% prfT)",
    4.62 +
    4.63 +   "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    4.64   \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
    4.65 - \  (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
    4.66 + \  (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))",
    4.67  
    4.68 -   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %%  \
    4.69 +   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %%  \
    4.70   \    (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==  \
    4.71   \  (ext % TYPE('T) % TYPE('U) % f % g %%  \
    4.72 - \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
    4.73 + \    (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %%  \
    4.74 + \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %%  \
    4.75 + \       (OfClass type_class % TYPE('U)) %% (prf % x)))",
    4.76  
    4.77 -   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    4.78 - \    (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
    4.79 +   "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    4.80 + \    (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf",
    4.81  
    4.82 -   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
    4.83 +   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
    4.84   \    (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
    4.85   \      (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
    4.86   \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
    4.87   \  (iffD1 % A = C % B = D %%  \
    4.88 - \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
    4.89 + \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
    4.90 + \      prfT %% arity_type_bool %%  \
    4.91   \      (cong % TYPE('T) % TYPE('T=>bool) %  \
    4.92   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    4.93 - \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    4.94 - \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    4.95 - \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    4.96 - \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
    4.97 + \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
    4.98 + \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
    4.99 + \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
   4.100 + \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
   4.101 + \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
   4.102 + \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))",
   4.103  
   4.104 -   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
   4.105 +   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
   4.106   \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
   4.107   \      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
   4.108   \        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
   4.109   \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
   4.110   \  (iffD2 % A = C % B = D %%  \
   4.111 - \    (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %%  \
   4.112 + \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
   4.113 + \      prfT %% arity_type_bool %%  \
   4.114   \      (cong % TYPE('T) % TYPE('T=>bool) %  \
   4.115   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
   4.116 - \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
   4.117 - \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
   4.118 - \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
   4.119 - \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
   4.120 + \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
   4.121 + \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
   4.122 + \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
   4.123 + \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
   4.124 + \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
   4.125 + \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))",
   4.126  
   4.127     (** rewriting on bool: insert proper congruence rules for logical connectives **)
   4.128  
   4.129     (* All *)
   4.130  
   4.131 -   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
   4.132 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   4.133 - \  (allI % TYPE('a) % Q %%  \
   4.134 +   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   4.135 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   4.136 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   4.137 + \  (allI % TYPE('a) % Q %% prfa %%  \
   4.138   \    (Lam x.  \
   4.139   \        iffD1 % P x % Q x %% (prf % x) %%  \
   4.140 - \         (spec % TYPE('a) % P % x %% prf')))",
   4.141 + \         (spec % TYPE('a) % P % x %% prfa %% prf')))",
   4.142  
   4.143 -   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
   4.144 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   4.145 - \  (allI % TYPE('a) % P %%  \
   4.146 +   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   4.147 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   4.148 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   4.149 + \  (allI % TYPE('a) % P %% prfa %%  \
   4.150   \    (Lam x.  \
   4.151   \        iffD2 % P x % Q x %% (prf % x) %%  \
   4.152 - \         (spec % TYPE('a) % Q % x %% prf')))",
   4.153 + \         (spec % TYPE('a) % Q % x %% prfa %% prf')))",
   4.154  
   4.155     (* Ex *)
   4.156  
   4.157 -   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
   4.158 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   4.159 - \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
   4.160 +   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   4.161 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   4.162 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   4.163 + \  (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %%  \
   4.164   \    (Lam x H : P x.  \
   4.165 - \        exI % TYPE('a) % Q % x %%  \
   4.166 + \        exI % TYPE('a) % Q % x %% prfa %%  \
   4.167   \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
   4.168  
   4.169 -   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
   4.170 - \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') ==  \
   4.171 - \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
   4.172 +   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   4.173 + \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   4.174 + \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   4.175 + \  (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %%  \
   4.176   \    (Lam x H : Q x.  \
   4.177 - \        exI % TYPE('a) % P % x %%  \
   4.178 + \        exI % TYPE('a) % P % x %% prfa %%  \
   4.179   \         (iffD2 % P x % Q x %% (prf % x) %% H)))",
   4.180  
   4.181     (* & *)
   4.182  
   4.183 -   "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   4.184 - \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
   4.185 - \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
   4.186 +   "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   4.187 + \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %%  \
   4.188 + \      (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   4.189   \  (conjI % B % D %%  \
   4.190   \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
   4.191   \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
   4.192  
   4.193 -   "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   4.194 - \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
   4.195 - \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
   4.196 +   "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   4.197 + \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %%  \
   4.198 + \      (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   4.199   \  (conjI % A % C %%  \
   4.200   \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
   4.201   \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
   4.202  
   4.203 -   "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
   4.204 - \    (HOL.refl % TYPE(bool=>bool) % op & A)) ==  \
   4.205 - \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
   4.206 +   "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %%  \
   4.207 + \    (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) ==  \
   4.208 + \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %%  \
   4.209   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   4.210   \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
   4.211 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
   4.212 - \        (HOL.refl % TYPE(bool) % A)))",
   4.213 + \        prfb %% prfbb %%  \
   4.214 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %%  \
   4.215 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   4.216 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   4.217  
   4.218     (* | *)
   4.219  
   4.220 -   "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   4.221 - \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   4.222 - \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   4.223 +   "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   4.224 + \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %%  \
   4.225 + \      (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   4.226   \  (disjE % A % C % B | D %% prf3 %%  \
   4.227   \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
   4.228   \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
   4.229  
   4.230 -   "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   4.231 - \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   4.232 - \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   4.233 +   "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   4.234 + \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %%  \
   4.235 + \      (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   4.236   \  (disjE % B % D % A | C %% prf3 %%  \
   4.237   \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
   4.238   \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
   4.239  
   4.240 -   "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   4.241 - \    (HOL.refl % TYPE(bool=>bool) % op | A)) ==  \
   4.242 - \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   4.243 +   "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %%  \
   4.244 + \    (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) ==  \
   4.245 + \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %%  \
   4.246   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   4.247   \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
   4.248 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
   4.249 - \        (HOL.refl % TYPE(bool) % A)))",
   4.250 + \        prfb %% prfbb %%  \
   4.251 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %%  \
   4.252 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   4.253 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   4.254  
   4.255     (* --> *)
   4.256  
   4.257 -   "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   4.258 - \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   4.259 - \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   4.260 +   "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   4.261 + \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %%  \
   4.262 + \      (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   4.263   \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
   4.264   \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
   4.265  
   4.266 -   "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   4.267 - \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   4.268 - \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   4.269 +   "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   4.270 + \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %%  \
   4.271 + \      (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   4.272   \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
   4.273   \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
   4.274  
   4.275 -   "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   4.276 - \    (HOL.refl % TYPE(bool=>bool) % op --> A)) ==  \
   4.277 - \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   4.278 +   "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %%  \
   4.279 + \    (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) ==  \
   4.280 + \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %%  \
   4.281   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   4.282   \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
   4.283 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
   4.284 - \        (HOL.refl % TYPE(bool) % A)))",
   4.285 + \        prfb %% prfbb %%  \
   4.286 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %%  \
   4.287 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   4.288 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   4.289  
   4.290     (* ~ *)
   4.291  
   4.292 -   "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   4.293 - \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   4.294 +   "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   4.295 + \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   4.296   \  (notI % Q %% (Lam H: Q.  \
   4.297   \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
   4.298  
   4.299 -   "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   4.300 - \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   4.301 +   "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   4.302 + \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   4.303   \  (notI % P %% (Lam H: P.  \
   4.304   \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
   4.305  
   4.306     (* = *)
   4.307  
   4.308     "(iffD1 % B % D %%  \
   4.309 - \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   4.310 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   4.311 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   4.312 + \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   4.313 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   4.314 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   4.315   \  (iffD1 % C % D %% prf2 %%  \
   4.316   \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
   4.317  
   4.318     "(iffD2 % B % D %%  \
   4.319 - \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   4.320 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   4.321 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   4.322 + \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   4.323 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   4.324 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   4.325   \  (iffD1 % A % B %% prf1 %%  \
   4.326   \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
   4.327  
   4.328     "(iffD1 % A % C %%  \
   4.329 - \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   4.330 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   4.331 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   4.332 + \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   4.333 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   4.334 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   4.335   \  (iffD2 % C % D %% prf2 %%  \
   4.336   \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
   4.337  
   4.338     "(iffD2 % A % C %%  \
   4.339 - \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %%  \
   4.340 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %%  \
   4.341 - \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   4.342 + \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   4.343 + \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   4.344 + \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   4.345   \  (iffD2 % A % B %% prf1 %%  \
   4.346   \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
   4.347  
   4.348 -   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   4.349 - \    (HOL.refl % TYPE(bool=>bool) % op = A)) ==  \
   4.350 - \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   4.351 +   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   4.352 + \    (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) ==  \
   4.353 + \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   4.354   \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   4.355   \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
   4.356 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
   4.357 - \        (HOL.refl % TYPE(bool) % A)))",
   4.358 + \        prfb %% prfbb %%  \
   4.359 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %%  \
   4.360 + \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   4.361 + \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   4.362  
   4.363     (** transitivity, reflexivity, and symmetry **)
   4.364  
   4.365 -   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   4.366 +   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   4.367   \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
   4.368  
   4.369 -   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   4.370 +   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   4.371   \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
   4.372  
   4.373 -   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
   4.374 +   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   4.375  
   4.376 -   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
   4.377 +   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   4.378  
   4.379 -   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
   4.380 +   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)",
   4.381  
   4.382 -   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
   4.383 +   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)",
   4.384  
   4.385     (** normalization of HOL proofs **)
   4.386  
   4.387 @@ -262,13 +283,13 @@
   4.388  
   4.389     "(impI % A % B %% (mp % A % B %% prf)) == prf",
   4.390  
   4.391 -   "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
   4.392 +   "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x",
   4.393  
   4.394 -   "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
   4.395 +   "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf",
   4.396  
   4.397 -   "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
   4.398 +   "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)",
   4.399  
   4.400 -   "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
   4.401 +   "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf",
   4.402  
   4.403     "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
   4.404  
   4.405 @@ -286,26 +307,26 @@
   4.406  (** Replace congruence rules by substitution rules **)
   4.407  
   4.408  fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
   4.409 -      prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
   4.410 -  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
   4.411 +      prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
   4.412 +  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
   4.413    | strip_cong _ _ = NONE;
   4.414  
   4.415 -val subst_prf = fst (strip_combt (Thm.proof_of subst));
   4.416 -val sym_prf = fst (strip_combt (Thm.proof_of sym));
   4.417 +val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst))));
   4.418 +val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym))));
   4.419  
   4.420  fun make_subst Ts prf xs (_, []) = prf
   4.421 -  | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
   4.422 +  | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
   4.423        let val T = fastype_of1 (Ts, x)
   4.424        in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
   4.425          else change_type (SOME [T]) subst_prf %> x %> y %>
   4.426            Abs ("z", T, list_comb (incr_boundvars 1 f,
   4.427              map (incr_boundvars 1) xs @ Bound 0 ::
   4.428 -            map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
   4.429 +            map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
   4.430            make_subst Ts prf (xs @ [x]) (f, ps)
   4.431        end;
   4.432  
   4.433 -fun make_sym Ts ((x, y), prf) =
   4.434 -  ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
   4.435 +fun make_sym Ts ((x, y), (prf, clprf)) =
   4.436 +  ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
   4.437  
   4.438  fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
   4.439  
   4.440 @@ -322,6 +343,6 @@
   4.441          apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
   4.442    | elim_cong_aux _ _ = NONE;
   4.443  
   4.444 -fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
   4.445 +fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
   4.446  
   4.447  end;
     5.1 --- a/src/Pure/Proof/extraction.ML	Tue Jun 01 11:04:49 2010 +0200
     5.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jun 01 11:13:09 2010 +0200
     5.3 @@ -24,6 +24,7 @@
     5.4    val mk_typ : typ -> term
     5.5    val etype_of : theory -> string list -> typ list -> term -> typ
     5.6    val realizes_of: theory -> string list -> term -> term -> term
     5.7 +  val abs_corr_shyps: theory -> thm -> string list -> term list -> Proofterm.proof -> Proofterm.proof
     5.8  end;
     5.9  
    5.10  structure Extraction : EXTRACTION =
    5.11 @@ -126,11 +127,9 @@
    5.12  fun frees_of t = map Free (rev (Term.add_frees t []));
    5.13  fun vfs_of t = vars_of t @ frees_of t;
    5.14  
    5.15 -fun forall_intr_prf (t, prf) =
    5.16 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    5.17 -  in Abst (a, SOME T, prf_abstract_over t prf) end;
    5.18 +val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
    5.19  
    5.20 -val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
    5.21 +val mkabsp = fold_rev (fn t => fn prf => AbsP ("H", SOME t, prf));
    5.22  
    5.23  fun strip_abs 0 t = t
    5.24    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
    5.25 @@ -161,6 +160,14 @@
    5.26      | _ => error "get_var_type: not a variable"
    5.27    end;
    5.28  
    5.29 +fun read_term thy T s =
    5.30 +  let
    5.31 +    val ctxt = ProofContext.init_global thy
    5.32 +      |> Proof_Syntax.strip_sorts_consttypes
    5.33 +      |> ProofContext.set_defsort [];
    5.34 +    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    5.35 +  in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
    5.36 +
    5.37  
    5.38  (**** theory data ****)
    5.39  
    5.40 @@ -175,7 +182,7 @@
    5.41         (term -> typ -> term -> typ -> term) option)) list,
    5.42       realizers : (string list * (term * proof)) list Symtab.table,
    5.43       defs : thm list,
    5.44 -     expand : (string * term) list,
    5.45 +     expand : string list,
    5.46       prep : (theory -> proof -> proof) option}
    5.47  
    5.48    val empty =
    5.49 @@ -198,14 +205,14 @@
    5.50       types = AList.merge (op =) (K true) (types1, types2),
    5.51       realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
    5.52       defs = Library.merge Thm.eq_thm (defs1, defs2),
    5.53 -     expand = Library.merge (op =) (expand1, expand2),   (* FIXME proper aconv !?! *)
    5.54 +     expand = Library.merge (op =) (expand1, expand2),
    5.55       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    5.56  );
    5.57  
    5.58  fun read_condeq thy =
    5.59    let val thy' = add_syntax thy
    5.60    in fn s =>
    5.61 -    let val t = Logic.varify_global (Syntax.read_prop_global thy' s)
    5.62 +    let val t = Logic.varify_global (read_term thy' propT s)
    5.63      in
    5.64        (map Logic.dest_equals (Logic.strip_imp_prems t),
    5.65          Logic.dest_equals (Logic.strip_imp_concl t))
    5.66 @@ -274,7 +281,7 @@
    5.67      fun err () = error ("Unable to determine type of extracted program for\n" ^
    5.68        Syntax.string_of_term_global thy t)
    5.69    in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
    5.70 -    [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
    5.71 +    [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
    5.72        Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
    5.73        Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
    5.74      | _ => err ()
    5.75 @@ -300,25 +307,30 @@
    5.76      val rtypes = map fst types;
    5.77      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    5.78      val thy' = add_syntax thy;
    5.79 -    val rd = Proof_Syntax.read_proof thy' false;
    5.80 +    val rd = Proof_Syntax.read_proof thy' true false;
    5.81    in fn (thm, (vs, s1, s2)) =>
    5.82      let
    5.83        val name = Thm.derivation_name thm;
    5.84        val _ = name <> "" orelse error "add_realizers: unnamed theorem";
    5.85 -      val prop = Pattern.rewrite_term thy'
    5.86 -        (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
    5.87 +      val prop = Thm.unconstrainT thm |> prop_of |>
    5.88 +        Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [];
    5.89        val vars = vars_of prop;
    5.90        val vars' = filter_out (fn v =>
    5.91          member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
    5.92 +      val shyps = maps (fn Var ((x, i), _) =>
    5.93 +        if member (op =) vs x then Logic.mk_of_sort
    5.94 +          (TVar (("'" ^ x, i), []), Sign.defaultS thy')
    5.95 +        else []) vars;
    5.96        val T = etype_of thy' vs [] prop;
    5.97        val (T', thw) = Type.legacy_freeze_thaw_type
    5.98          (if T = nullT then nullT else map fastype_of vars' ---> T);
    5.99 -      val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
   5.100 +      val t = map_types thw (read_term thy' T' s1);
   5.101        val r' = freeze_thaw (condrew thy' eqns
   5.102 -        (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   5.103 +        (procs @ [typeof_proc [] vs, rlz_proc]))
   5.104            (Const ("realizes", T --> propT --> propT) $
   5.105              (if T = nullT then t else list_comb (t, vars')) $ prop);
   5.106 -      val r = fold_rev Logic.all (map (get_var_type r') vars) r';
   5.107 +      val r = Logic.list_implies (shyps,
   5.108 +        fold_rev Logic.all (map (get_var_type r') vars) r');
   5.109        val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
   5.110      in (name, (vs, (t, prf))) end
   5.111    end;
   5.112 @@ -337,10 +349,34 @@
   5.113      val prop' = Pattern.rewrite_term thy'
   5.114        (map (Logic.dest_equals o prop_of) defs) [] prop;
   5.115    in freeze_thaw (condrew thy' eqns
   5.116 -    (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   5.117 +    (procs @ [typeof_proc [] vs, rlz_proc]))
   5.118        (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
   5.119    end;
   5.120  
   5.121 +fun abs_corr_shyps thy thm vs xs prf =
   5.122 +  let
   5.123 +    val S = Sign.defaultS thy;
   5.124 +    val ((atyp_map, constraints, _), prop') =
   5.125 +      Logic.unconstrainT (#shyps (rep_thm thm)) (prop_of thm);
   5.126 +    val atyps = fold_types (fold_atyps (insert (op =))) (prop_of thm) [];
   5.127 +    val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
   5.128 +        SOME (TVar (("'" ^ v, i), [])) else NONE)
   5.129 +      (rev (Term.add_vars prop' []));
   5.130 +    val cs = maps (fn T => map (pair T) S) Ts;
   5.131 +    val constraints' = map Logic.mk_of_class cs;
   5.132 +    val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints);
   5.133 +    fun typ_map T = Type.strip_sorts
   5.134 +      (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
   5.135 +    fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
   5.136 +    val xs' = map (map_types typ_map) xs
   5.137 +  in
   5.138 +    prf |>
   5.139 +    Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
   5.140 +    fold_rev implies_intr_proof' (map snd constraints) |>
   5.141 +    fold_rev forall_intr_proof' xs' |>
   5.142 +    fold_rev implies_intr_proof' constraints'
   5.143 +  end;
   5.144 +
   5.145  (** expanding theorems / definitions **)
   5.146  
   5.147  fun add_expand_thm is_def thm thy =
   5.148 @@ -354,15 +390,15 @@
   5.149      thy |> ExtractionData.put
   5.150        (if is_def then
   5.151          {realizes_eqns = realizes_eqns,
   5.152 -         typeof_eqns = add_rule ([],
   5.153 -           Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
   5.154 +         typeof_eqns = add_rule ([], Logic.dest_equals (map_types
   5.155 +           Type.strip_sorts (prop_of (Drule.abs_def thm)))) typeof_eqns,
   5.156           types = types,
   5.157           realizers = realizers, defs = insert Thm.eq_thm thm defs,
   5.158           expand = expand, prep = prep}
   5.159        else
   5.160          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
   5.161           realizers = realizers, defs = defs,
   5.162 -         expand = insert (op =) (name, prop_of thm) expand, prep = prep})
   5.163 +         expand = insert (op =) name expand, prep = prep})
   5.164    end;
   5.165  
   5.166  fun extraction_expand is_def =
   5.167 @@ -443,9 +479,9 @@
   5.168        ExtractionData.get thy;
   5.169      val procs = maps (rev o fst o snd) types;
   5.170      val rtypes = map fst types;
   5.171 -    val typroc = typeof_proc (Sign.defaultS thy');
   5.172 +    val typroc = typeof_proc [];
   5.173      val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
   5.174 -      Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
   5.175 +      Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
   5.176      val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
   5.177  
   5.178      fun find_inst prop Ts ts vs =
   5.179 @@ -464,6 +500,13 @@
   5.180  
   5.181        in fold_rev add_args (take n vars ~~ take n ts) ([], []) end;
   5.182  
   5.183 +    fun mk_shyps tye = maps (fn (ixn, _) =>
   5.184 +      Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
   5.185 +
   5.186 +    fun mk_sprfs cs tye = maps (fn (_, T) =>
   5.187 +      ProofRewriteRules.mk_of_sort_proof thy (map SOME cs)
   5.188 +        (T, Sign.defaultS thy)) tye;
   5.189 +
   5.190      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
   5.191      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
   5.192  
   5.193 @@ -474,22 +517,22 @@
   5.194      fun realizes_null vs prop = app_rlz_rews [] vs
   5.195        (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
   5.196  
   5.197 -    fun corr d defs vs ts Ts hs (PBound i) _ _ = (defs, PBound i)
   5.198 +    fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i)
   5.199  
   5.200 -      | corr d defs vs ts Ts hs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
   5.201 +      | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
   5.202            let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
   5.203 -            (dummyt :: hs) prf (incr_pboundvars 1 0 prf')
   5.204 +            (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
   5.205              (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
   5.206            in (defs', Abst (s, SOME T, corr_prf)) end
   5.207  
   5.208 -      | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
   5.209 +      | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
   5.210            let
   5.211              val T = etype_of thy' vs Ts prop;
   5.212              val u = if T = nullT then 
   5.213                  (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
   5.214                else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
   5.215              val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
   5.216 -              (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
   5.217 +              (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
   5.218              val rlz = Const ("realizes", T --> propT --> propT)
   5.219            in (defs',
   5.220              if T = nullT then AbsP ("R",
   5.221 @@ -500,10 +543,10 @@
   5.222                  (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
   5.223            end
   5.224  
   5.225 -      | corr d defs vs ts Ts hs (prf % SOME t) (prf' % _) t' =
   5.226 +      | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' =
   5.227            let
   5.228              val (Us, T) = strip_type (fastype_of1 (Ts, t));
   5.229 -            val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
   5.230 +            val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf'
   5.231                (if member (op =) rtypes (tname_of T) then t'
   5.232                 else (case t' of SOME (u $ _) => SOME u | _ => NONE));
   5.233              val u = if not (member (op =) rtypes (tname_of T)) then t else
   5.234 @@ -519,7 +562,7 @@
   5.235                in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
   5.236            in (defs', corr_prf % SOME u) end
   5.237  
   5.238 -      | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
   5.239 +      | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
   5.240            let
   5.241              val prop = Reconstruct.prop_of' hs prf2';
   5.242              val T = etype_of thy' vs Ts prop;
   5.243 @@ -529,17 +572,19 @@
   5.244                 | _ =>
   5.245                   let val (defs1, u) = extr d defs vs [] Ts hs prf2'
   5.246                   in (defs1, NONE, SOME u) end)
   5.247 -            val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs prf1 prf1' f;
   5.248 -            val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs prf2 prf2' u;
   5.249 +            val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f;
   5.250 +            val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u;
   5.251            in
   5.252              if T = nullT then (defs3, corr_prf1 %% corr_prf2) else
   5.253                (defs3, corr_prf1 % u %% corr_prf2)
   5.254            end
   5.255  
   5.256 -      | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
   5.257 +      | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
   5.258            let
   5.259              val prf = join_proof body;
   5.260              val (vs', tye) = find_inst prop Ts ts vs;
   5.261 +            val shyps = mk_shyps tye;
   5.262 +            val sprfs = mk_sprfs cs tye;
   5.263              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
   5.264              val T = etype_of thy' vs' [] prop;
   5.265              val defs' = if T = nullT then defs
   5.266 @@ -555,28 +600,31 @@
   5.267                        (if null vs' then ""
   5.268                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   5.269                      val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   5.270 -                    val (defs'', corr_prf) =
   5.271 -                      corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
   5.272 +                    val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] []
   5.273 +                      (rev shyps) prf' prf' NONE;
   5.274 +                    val corr_prf = mkabsp shyps corr_prf0;
   5.275                      val corr_prop = Reconstruct.prop_of corr_prf;
   5.276 -                    val corr_prf' = List.foldr forall_intr_prf
   5.277 -                      (proof_combt
   5.278 +                    val corr_prf' =
   5.279 +                      proof_combP (proof_combt
   5.280                           (PThm (serial (),
   5.281                            ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
   5.282 -                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
   5.283 -                      (map (get_var_type corr_prop) (vfs_of prop))
   5.284 +                            Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
   5.285 +                              map PBound (length shyps - 1 downto 0)) |>
   5.286 +                      fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
   5.287 +                      mkabsp shyps
   5.288                    in
   5.289                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
   5.290 -                     prf_subst_TVars tye' corr_prf')
   5.291 +                     proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
   5.292                    end
   5.293 -              | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf'))
   5.294 +              | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
   5.295              | SOME rs => (case find vs' rs of
   5.296 -                SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
   5.297 +                SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
   5.298                | NONE => error ("corr: no realizer for instance of theorem " ^
   5.299                    quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   5.300                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   5.301            end
   5.302  
   5.303 -      | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
   5.304 +      | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
   5.305            let
   5.306              val (vs', tye) = find_inst prop Ts ts vs;
   5.307              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
   5.308 @@ -584,13 +632,14 @@
   5.309              if etype_of thy' vs' [] prop = nullT andalso
   5.310                realizes_null vs' prop aconv prop then (defs, prf0)
   5.311              else case find vs' (Symtab.lookup_list realizers s) of
   5.312 -              SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
   5.313 +              SOME (_, prf) => (defs,
   5.314 +                proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
   5.315              | NONE => error ("corr: no realizer for instance of axiom " ^
   5.316                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   5.317                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   5.318            end
   5.319  
   5.320 -      | corr d defs vs ts Ts hs _ _ _ = error "corr: bad proof"
   5.321 +      | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
   5.322  
   5.323      and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i)
   5.324  
   5.325 @@ -630,6 +679,7 @@
   5.326            let
   5.327              val prf = join_proof body;
   5.328              val (vs', tye) = find_inst prop Ts ts vs;
   5.329 +            val shyps = mk_shyps tye;
   5.330              val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
   5.331            in
   5.332              case Symtab.lookup realizers s of
   5.333 @@ -641,18 +691,18 @@
   5.334                         else " (relevant variables: " ^ commas_quote vs' ^ ")"));
   5.335                      val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
   5.336                      val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
   5.337 -                    val (defs'', corr_prf) =
   5.338 -                      corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
   5.339 +                    val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] []
   5.340 +                      (rev shyps) prf' prf' (SOME t);
   5.341  
   5.342                      val nt = Envir.beta_norm t;
   5.343                      val args = filter_out (fn v => member (op =) rtypes
   5.344                        (tname_of (body_type (fastype_of v)))) (vfs_of prop);
   5.345                      val args' = filter (fn v => Logic.occs (v, nt)) args;
   5.346 -                    val t' = mkabs nt args';
   5.347 +                    val t' = mkabs args' nt;
   5.348                      val T = fastype_of t';
   5.349                      val cname = extr_name s vs';
   5.350                      val c = Const (cname, T);
   5.351 -                    val u = mkabs (list_comb (c, args')) args;
   5.352 +                    val u = mkabs args (list_comb (c, args'));
   5.353                      val eqn = Logic.mk_equals (c, t');
   5.354                      val rlz =
   5.355                        Const ("realizes", fastype_of nt --> propT --> propT);
   5.356 @@ -661,20 +711,22 @@
   5.357                      val f = app_rlz_rews [] vs'
   5.358                        (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
   5.359  
   5.360 -                    val corr_prf' =
   5.361 -                      chtype [] equal_elim_axm %> lhs %> rhs %%
   5.362 +                    val corr_prf' = mkabsp shyps
   5.363 +                      (chtype [] equal_elim_axm %> lhs %> rhs %%
   5.364                         (chtype [propT] symmetric_axm %> rhs %> lhs %%
   5.365                           (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
   5.366                             (chtype [T --> propT] reflexive_axm %> f) %%
   5.367                             PAxm (cname ^ "_def", eqn,
   5.368 -                             SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
   5.369 +                             SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
   5.370                      val corr_prop = Reconstruct.prop_of corr_prf';
   5.371 -                    val corr_prf'' = List.foldr forall_intr_prf
   5.372 -                      (proof_combt
   5.373 +                    val corr_prf'' =
   5.374 +                      proof_combP (proof_combt
   5.375                          (PThm (serial (),
   5.376                           ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
   5.377 -                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
   5.378 -                      (map (get_var_type corr_prop) (vfs_of prop));
   5.379 +                           Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
   5.380 +                             map PBound (length shyps - 1 downto 0)) |>
   5.381 +                      fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
   5.382 +                      mkabsp shyps
   5.383                    in
   5.384                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
   5.385                       subst_TVars tye' u)
   5.386 @@ -731,7 +783,7 @@
   5.387             in
   5.388               thy'
   5.389               |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
   5.390 -                  Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
   5.391 +                  Thm.varifyT_global (funpow (length (vars_of corr_prop))
   5.392                      (Thm.forall_elim_var 0) (Thm.forall_intr_frees
   5.393                        (ProofChecker.thm_of_proof thy'
   5.394                         (fst (Proofterm.freeze_thaw_prf prf))))))
     6.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jun 01 11:04:49 2010 +0200
     6.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jun 01 11:13:09 2010 +0200
     6.3 @@ -6,14 +6,17 @@
     6.4  
     6.5  signature PROOF_REWRITE_RULES =
     6.6  sig
     6.7 -  val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     6.8 +  val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
     6.9    val rprocs : bool ->
    6.10 -    (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
    6.11 +    (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
    6.12    val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
    6.13    val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
    6.14    val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
    6.15    val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    6.16    val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    6.17 +  val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
    6.18 +  val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
    6.19 +    (Proofterm.proof * Proofterm.proof) option
    6.20  end;
    6.21  
    6.22  structure ProofRewriteRules : PROOF_REWRITE_RULES =
    6.23 @@ -21,7 +24,7 @@
    6.24  
    6.25  open Proofterm;
    6.26  
    6.27 -fun rew b _ =
    6.28 +fun rew b _ _ =
    6.29    let
    6.30      fun ?? x = if b then SOME x else NONE;
    6.31      fun ax (prf as PAxm (s, prop, _)) Ts =
    6.32 @@ -219,31 +222,36 @@
    6.33  fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
    6.34  
    6.35  fun insert_refl defs Ts (prf1 %% prf2) =
    6.36 -      insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
    6.37 +      let val (prf1', b) = insert_refl defs Ts prf1
    6.38 +      in
    6.39 +        if b then (prf1', true)
    6.40 +        else (prf1' %% fst (insert_refl defs Ts prf2), false)
    6.41 +      end
    6.42    | insert_refl defs Ts (Abst (s, SOME T, prf)) =
    6.43 -      Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
    6.44 +      (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
    6.45    | insert_refl defs Ts (AbsP (s, t, prf)) =
    6.46 -      AbsP (s, t, insert_refl defs Ts prf)
    6.47 +      (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
    6.48    | insert_refl defs Ts prf = (case strip_combt prf of
    6.49          (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
    6.50            if member (op =) defs s then
    6.51              let
    6.52                val vs = vars_of prop;
    6.53                val tvars = Term.add_tvars prop [] |> rev;
    6.54 -              val (_, rhs) = Logic.dest_equals prop;
    6.55 +              val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
    6.56                val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
    6.57                  (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
    6.58                  map the ts);
    6.59              in
    6.60 -              change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
    6.61 +              (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true)
    6.62              end
    6.63 -          else prf
    6.64 -      | (_, []) => prf
    6.65 -      | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
    6.66 +          else (prf, false)
    6.67 +      | (_, []) => (prf, false)
    6.68 +      | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
    6.69  
    6.70  fun elim_defs thy r defs prf =
    6.71    let
    6.72 -    val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
    6.73 +    val defs' = map (Logic.dest_equals o
    6.74 +      map_types Type.strip_sorts o prop_of o Drule.abs_def) defs;
    6.75      val defnames = map Thm.derivation_name defs;
    6.76      val f = if not r then I else
    6.77        let
    6.78 @@ -258,7 +266,7 @@
    6.79        in Reconstruct.expand_proof thy thms end;
    6.80    in
    6.81      rewrite_terms (Pattern.rewrite_term thy defs' [])
    6.82 -      (insert_refl defnames [] (f prf))
    6.83 +      (fst (insert_refl defnames [] (f prf)))
    6.84    end;
    6.85  
    6.86  
    6.87 @@ -327,4 +335,35 @@
    6.88      mk_prf Q
    6.89    end;
    6.90  
    6.91 +
    6.92 +(**** expand OfClass proofs ****)
    6.93 +
    6.94 +fun mk_of_sort_proof thy hs (T, S) =
    6.95 +  let
    6.96 +    val hs' = map
    6.97 +      (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
    6.98 +        | NONE => NONE) hs;
    6.99 +    val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
   6.100 +    fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
   6.101 +    val subst = map_atyps
   6.102 +      (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
   6.103 +        | T as TFree (s, _) => TFree (s, get_sort T));
   6.104 +    fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
   6.105 +        ~1 => error "expand_of_class: missing class hypothesis"
   6.106 +      | i => PBound i;
   6.107 +    fun reconstruct prf prop = prf |>
   6.108 +      Reconstruct.reconstruct_proof thy prop |>
   6.109 +      Reconstruct.expand_proof thy [("", NONE)] |>
   6.110 +      Same.commit (map_proof_same Same.same Same.same hyp)
   6.111 +  in
   6.112 +    map2 reconstruct
   6.113 +      (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
   6.114 +      (Logic.mk_of_sort (T, S))
   6.115 +  end;
   6.116 +
   6.117 +fun expand_of_class thy Ts hs (OfClass (T, c)) =
   6.118 +      mk_of_sort_proof thy hs (T, [c]) |>
   6.119 +      hd |> rpair no_skel |> SOME
   6.120 +  | expand_of_class thy Ts hs _ = NONE;
   6.121 +
   6.122  end;