src/HOL/Extraction.thy
changeset 37233 b78f31ca4675
parent 34913 d8cb720c9c53
child 48891 c0eafbd55de3
     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