1.1 --- a/src/HOL/Extraction.thy Tue Jun 01 11:18:51 2010 +0200
1.2 +++ b/src/HOL/Extraction.thy Tue Jun 01 11:30:57 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/Lambda/WeakNorm.thy Tue Jun 01 11:18:51 2010 +0200
2.2 +++ b/src/HOL/Lambda/WeakNorm.thy Tue Jun 01 11:30:57 2010 +0200
2.3 @@ -264,6 +264,7 @@
2.4 lemmas [extraction_expand] = conj_assoc listall_cons_eq
2.5
2.6 extract type_NF
2.7 +
2.8 lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
2.9 apply (rule iffI)
2.10 apply (erule rtranclpR.induct)
3.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 11:18:51 2010 +0200
3.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 11:30:57 2010 +0200
3.3 @@ -22,10 +22,6 @@
3.4 in map (fn ks => i::ks) is @ is end
3.5 else [[]];
3.6
3.7 -fun forall_intr_prf (t, prf) =
3.8 - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
3.9 - in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
3.10 -
3.11 fun prf_of thm =
3.12 Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
3.13
3.14 @@ -130,12 +126,12 @@
3.15
3.16 val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
3.17 val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
3.18 - val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *)
3.19 - member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
3.20 + val ivs1 = map Var (filter_out (fn (_, T) =>
3.21 + @{type_name bool} = tname_of (body_type T)) ivs);
3.22 val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
3.23
3.24 val prf =
3.25 - List.foldr forall_intr_prf
3.26 + Extraction.abs_corr_shyps thy' induct vs ivs2
3.27 (fold_rev (fn (f, p) => fn prf =>
3.28 (case head_of (strip_abs_body f) of
3.29 Free (s, T) =>
3.30 @@ -145,7 +141,7 @@
3.31 end
3.32 | _ => AbsP ("H", SOME p, prf)))
3.33 (rec_fns ~~ prems_of thm)
3.34 - (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
3.35 + (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
3.36
3.37 val r' =
3.38 if null is then r
3.39 @@ -198,18 +194,21 @@
3.40 ||> Sign.restore_naming thy;
3.41
3.42 val P = Var (("P", 0), rT' --> HOLogic.boolT);
3.43 - val prf = forall_intr_prf (y, forall_intr_prf (P,
3.44 - fold_rev (fn (p, r) => fn prf =>
3.45 - forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
3.46 + val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
3.47 + (fold_rev (fn (p, r) => fn prf =>
3.48 + Proofterm.forall_intr_proof' (Logic.varify_global r)
3.49 + (AbsP ("H", SOME (Logic.varify_global p), prf)))
3.50 (prems ~~ rs)
3.51 - (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
3.52 + (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
3.53 + val prf' = Extraction.abs_corr_shyps thy' exhaust []
3.54 + (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
3.55 val r' = Logic.varify_global (Abs ("y", T,
3.56 list_abs (map dest_Free rs, list_comb (r,
3.57 map Bound ((length rs - 1 downto 0) @ [length rs])))));
3.58
3.59 in Extraction.add_realizers_i
3.60 [(exh_name, (["P"], r', prf)),
3.61 - (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
3.62 + (exh_name, ([], Extraction.nullt, prf'))] thy'
3.63 end;
3.64
3.65 fun add_dt_realizers config names thy =
4.1 --- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 11:18:51 2010 +0200
4.2 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 11:30:57 2010 +0200
4.3 @@ -21,18 +21,12 @@
4.4 [name] => name
4.5 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
4.6
4.7 -val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
4.8 -
4.9 fun prf_of thm =
4.10 let
4.11 val thy = Thm.theory_of_thm thm;
4.12 val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
4.13 in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
4.14
4.15 -fun forall_intr_prf t prf =
4.16 - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
4.17 - in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
4.18 -
4.19 fun subsets [] = [[]]
4.20 | subsets (x::xs) =
4.21 let val ys = subsets xs
4.22 @@ -55,15 +49,19 @@
4.23 (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
4.24 | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
4.25
4.26 -fun relevant_vars prop = List.foldr (fn
4.27 - (Var ((a, i), T), vs) => (case strip_type T of
4.28 +fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
4.29 + (case strip_type T of
4.30 (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
4.31 - | _ => vs)
4.32 - | (_, vs) => vs) [] (OldTerm.term_vars prop);
4.33 + | _ => vs)) (Term.add_vars prop []) [];
4.34 +
4.35 +val attach_typeS = map_types (map_atyps
4.36 + (fn TFree (s, []) => TFree (s, HOLogic.typeS)
4.37 + | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
4.38 + | T => T));
4.39
4.40 fun dt_of_intrs thy vs nparms intrs =
4.41 let
4.42 - val iTs = OldTerm.term_tvars (prop_of (hd intrs));
4.43 + val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
4.44 val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
4.45 (Logic.strip_imp_concl (prop_of (hd intrs))));
4.46 val params = map dest_Var (take nparms ts);
4.47 @@ -84,7 +82,7 @@
4.48 fun gen_rvar vs (t as Var ((a, 0), T)) =
4.49 if body_type T <> HOLogic.boolT then t else
4.50 let
4.51 - val U = TVar (("'" ^ a, 0), HOLogic.typeS)
4.52 + val U = TVar (("'" ^ a, 0), [])
4.53 val Ts = binder_types T;
4.54 val i = length Ts;
4.55 val xs = map (pair "x") Ts;
4.56 @@ -98,8 +96,9 @@
4.57
4.58 fun mk_realizes_eqn n vs nparms intrs =
4.59 let
4.60 - val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
4.61 - val iTs = OldTerm.term_tvars concl;
4.62 + val intr = map_types Type.strip_sorts (prop_of (hd intrs));
4.63 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
4.64 + val iTs = rev (Term.add_tvars intr []);
4.65 val Tvs = map TVar iTs;
4.66 val (h as Const (s, T), us) = strip_comb concl;
4.67 val params = List.take (us, nparms);
4.68 @@ -110,7 +109,7 @@
4.69 (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
4.70 val rT = if n then Extraction.nullT
4.71 else Type (space_implode "_" (s ^ "T" :: vs),
4.72 - map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
4.73 + map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
4.74 val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
4.75 val S = list_comb (h, params @ xs);
4.76 val rvs = relevant_vars S;
4.77 @@ -121,7 +120,7 @@
4.78 let val T = (the o AList.lookup (op =) rvs) v
4.79 in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
4.80 Extraction.mk_typ (if n then Extraction.nullT
4.81 - else TVar (("'" ^ v, 0), HOLogic.typeS)))
4.82 + else TVar (("'" ^ v, 0), [])))
4.83 end;
4.84
4.85 val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
4.86 @@ -261,12 +260,12 @@
4.87 val rlzvs = rev (Term.add_vars (prop_of rrule) []);
4.88 val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
4.89 val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
4.90 - val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
4.91 - val rlz'' = fold_rev Logic.all vs2 rlz
4.92 + val rlz' = fold_rev Logic.all rs (prop_of rrule)
4.93 in (name, (vs,
4.94 if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
4.95 - ProofRewriteRules.un_hhf_proof rlz' rlz''
4.96 - (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
4.97 + Extraction.abs_corr_shyps thy rule vs vs2
4.98 + (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
4.99 + (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
4.100 end;
4.101
4.102 fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
4.103 @@ -275,7 +274,7 @@
4.104 let
4.105 val qualifier = Long_Name.qualifier (name_of_thm induct);
4.106 val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
4.107 - val iTs = OldTerm.term_tvars (prop_of (hd intrs));
4.108 + val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
4.109 val ar = length vs + length iTs;
4.110 val params = Inductive.params_of raw_induct;
4.111 val arities = Inductive.arities_of raw_induct;
4.112 @@ -297,8 +296,6 @@
4.113 val thy1' = thy1 |>
4.114 Theory.copy |>
4.115 Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
4.116 - fold (fn s => AxClass.axiomatize_arity
4.117 - (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
4.118 Extraction.add_typeof_eqns_i ty_eqs;
4.119 val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
4.120 SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
4.121 @@ -328,10 +325,10 @@
4.122 end
4.123 else (replicate (length rs) Extraction.nullt, (recs, dummies)))
4.124 rss (rec_thms, dummies);
4.125 - val rintrs = map (fn (intr, c) => Envir.eta_contract
4.126 + val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
4.127 (Extraction.realizes_of thy2 vs
4.128 (if c = Extraction.nullt then c else list_comb (c, map Var (rev
4.129 - (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
4.130 + (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
4.131 (maps snd rss ~~ flat constrss);
4.132 val (rlzpreds, rlzpreds') =
4.133 rintrs |> map (fn rintr =>
4.134 @@ -390,7 +387,9 @@
4.135 val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
4.136 (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
4.137 val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
4.138 - val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
4.139 + val thm = Goal.prove_global thy []
4.140 + (map attach_typeS prems) (attach_typeS concl)
4.141 + (fn {prems, ...} => EVERY
4.142 [rtac (#raw_induct ind_info) 1,
4.143 rewrite_goals_tac rews,
4.144 REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
4.145 @@ -408,10 +407,10 @@
4.146 in
4.147 Extraction.add_realizers_i
4.148 (map (fn (((ind, corr), rlz), r) =>
4.149 - mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
4.150 + mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
4.151 realizers @ (case realizers of
4.152 [(((ind, corr), rlz), r)] =>
4.153 - [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
4.154 + [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
4.155 ind, corr, rlz, r)]
4.156 | _ => [])) thy''
4.157 end;
4.158 @@ -445,7 +444,7 @@
4.159 map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
4.160 [Bound (length prems)]));
4.161 val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
4.162 - val rlz' = strip_all (Logic.unvarify_global rlz);
4.163 + val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
4.164 val rews = map mk_meta_eq case_thms;
4.165 val thm = Goal.prove_global thy []
4.166 (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
4.167 @@ -488,7 +487,7 @@
4.168 val vss = sort (int_ord o pairself length)
4.169 (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
4.170 in
4.171 - fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
4.172 + fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
4.173 end
4.174
4.175 fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
5.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 11:18:51 2010 +0200
5.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 11:30:57 2010 +0200
5.3 @@ -7,7 +7,7 @@
5.4 signature REWRITE_HOL_PROOF =
5.5 sig
5.6 val rews: (Proofterm.proof * Proofterm.proof) list
5.7 - val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
5.8 + val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
5.9 end;
5.10
5.11 structure RewriteHOLProof : REWRITE_HOL_PROOF =
5.12 @@ -16,7 +16,7 @@
5.13 open Proofterm;
5.14
5.15 val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
5.16 - Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
5.17 + Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
5.18
5.19 (** eliminate meta-equality rules **)
5.20
5.21 @@ -24,237 +24,258 @@
5.22 \ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \
5.23 \ (axm.reflexive % TYPE('T3) % x4) %% prf1)) == \
5.24 \ (iffD1 % A % B %% \
5.25 - \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
5.26 + \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
5.27
5.28 "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \
5.29 \ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \
5.30 \ (axm.reflexive % TYPE('T4) % x6) %% prf1))) == \
5.31 \ (iffD2 % A % B %% \
5.32 - \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
5.33 + \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
5.34
5.35 - "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \
5.36 + "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %% \
5.37 \ (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) == \
5.38 \ (cong % TYPE('T) % TYPE('U) % f % g % x % y %% \
5.39 - \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \
5.40 - \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
5.41 + \ (OfClass type_class % TYPE('T)) %% prfU %% \
5.42 + \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %% \
5.43 + \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))",
5.44
5.45 - "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \
5.46 + "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% \
5.47 \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \
5.48 - \ (HOL.trans % TYPE('T) % x % y % z %% \
5.49 - \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \
5.50 - \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
5.51 + \ (HOL.trans % TYPE('T) % x % y % z %% prfT %% \
5.52 + \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %% \
5.53 + \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))",
5.54
5.55 - "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \
5.56 - \ (HOL.refl % TYPE('T) % x)",
5.57 + "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) == \
5.58 + \ (HOL.refl % TYPE('T) % x %% prfT)",
5.59
5.60 - "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
5.61 + "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \
5.62 \ (axm.symmetric % TYPE('T) % x % y %% prf)) == \
5.63 - \ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
5.64 + \ (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))",
5.65
5.66 - "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \
5.67 + "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %% \
5.68 \ (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) == \
5.69 \ (ext % TYPE('T) % TYPE('U) % f % g %% \
5.70 - \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
5.71 + \ (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %% \
5.72 + \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% \
5.73 + \ (OfClass type_class % TYPE('U)) %% (prf % x)))",
5.74
5.75 - "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
5.76 - \ (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
5.77 + "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \
5.78 + \ (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf",
5.79
5.80 - "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
5.81 + "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \
5.82 \ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
5.83 \ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
5.84 \ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \
5.85 \ (iffD1 % A = C % B = D %% \
5.86 - \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
5.87 + \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \
5.88 + \ prfT %% arity_type_bool %% \
5.89 \ (cong % TYPE('T) % TYPE('T=>bool) % \
5.90 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
5.91 - \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
5.92 - \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
5.93 - \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
5.94 - \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
5.95 + \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \
5.96 + \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \
5.97 + \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \
5.98 + \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \
5.99 + \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \
5.100 + \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))",
5.101
5.102 - "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
5.103 + "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \
5.104 \ (axm.symmetric % TYPE('T2) % x5 % x6 %% \
5.105 \ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
5.106 \ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
5.107 \ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \
5.108 \ (iffD2 % A = C % B = D %% \
5.109 - \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
5.110 + \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \
5.111 + \ prfT %% arity_type_bool %% \
5.112 \ (cong % TYPE('T) % TYPE('T=>bool) % \
5.113 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
5.114 - \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
5.115 - \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
5.116 - \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
5.117 - \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
5.118 + \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \
5.119 + \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \
5.120 + \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \
5.121 + \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \
5.122 + \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \
5.123 + \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))",
5.124
5.125 (** rewriting on bool: insert proper congruence rules for logical connectives **)
5.126
5.127 (* All *)
5.128
5.129 - "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
5.130 - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
5.131 - \ (allI % TYPE('a) % Q %% \
5.132 + "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \
5.133 + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
5.134 + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
5.135 + \ (allI % TYPE('a) % Q %% prfa %% \
5.136 \ (Lam x. \
5.137 \ iffD1 % P x % Q x %% (prf % x) %% \
5.138 - \ (spec % TYPE('a) % P % x %% prf')))",
5.139 + \ (spec % TYPE('a) % P % x %% prfa %% prf')))",
5.140
5.141 - "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
5.142 - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
5.143 - \ (allI % TYPE('a) % P %% \
5.144 + "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \
5.145 + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
5.146 + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
5.147 + \ (allI % TYPE('a) % P %% prfa %% \
5.148 \ (Lam x. \
5.149 \ iffD2 % P x % Q x %% (prf % x) %% \
5.150 - \ (spec % TYPE('a) % Q % x %% prf')))",
5.151 + \ (spec % TYPE('a) % Q % x %% prfa %% prf')))",
5.152
5.153 (* Ex *)
5.154
5.155 - "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
5.156 - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
5.157 - \ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \
5.158 + "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \
5.159 + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
5.160 + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
5.161 + \ (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %% \
5.162 \ (Lam x H : P x. \
5.163 - \ exI % TYPE('a) % Q % x %% \
5.164 + \ exI % TYPE('a) % Q % x %% prfa %% \
5.165 \ (iffD1 % P x % Q x %% (prf % x) %% H)))",
5.166
5.167 - "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
5.168 - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
5.169 - \ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \
5.170 + "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \
5.171 + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
5.172 + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
5.173 + \ (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %% \
5.174 \ (Lam x H : Q x. \
5.175 - \ exI % TYPE('a) % P % x %% \
5.176 + \ exI % TYPE('a) % P % x %% prfa %% \
5.177 \ (iffD2 % P x % Q x %% (prf % x) %% H)))",
5.178
5.179 (* & *)
5.180
5.181 - "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
5.182 - \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
5.183 - \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
5.184 + "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
5.185 + \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \
5.186 + \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \
5.187 \ (conjI % B % D %% \
5.188 \ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \
5.189 \ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
5.190
5.191 - "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
5.192 - \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
5.193 - \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
5.194 + "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
5.195 + \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \
5.196 + \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \
5.197 \ (conjI % A % C %% \
5.198 \ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \
5.199 \ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
5.200
5.201 - "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
5.202 - \ (HOL.refl % TYPE(bool=>bool) % op & A)) == \
5.203 - \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
5.204 + "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \
5.205 + \ (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) == \
5.206 + \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \
5.207 \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
5.208 \ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \
5.209 - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \
5.210 - \ (HOL.refl % TYPE(bool) % A)))",
5.211 + \ prfb %% prfbb %% \
5.212 + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %% \
5.213 + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
5.214 + \ (HOL.refl % TYPE(bool) % A %% prfb)))",
5.215
5.216 (* | *)
5.217
5.218 - "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
5.219 - \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
5.220 - \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
5.221 + "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
5.222 + \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \
5.223 + \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \
5.224 \ (disjE % A % C % B | D %% prf3 %% \
5.225 \ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \
5.226 \ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
5.227
5.228 - "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
5.229 - \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
5.230 - \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
5.231 + "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
5.232 + \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \
5.233 + \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \
5.234 \ (disjE % B % D % A | C %% prf3 %% \
5.235 \ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \
5.236 \ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
5.237
5.238 - "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
5.239 - \ (HOL.refl % TYPE(bool=>bool) % op | A)) == \
5.240 - \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
5.241 + "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \
5.242 + \ (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) == \
5.243 + \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \
5.244 \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
5.245 \ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \
5.246 - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %% \
5.247 - \ (HOL.refl % TYPE(bool) % A)))",
5.248 + \ prfb %% prfbb %% \
5.249 + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %% \
5.250 + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
5.251 + \ (HOL.refl % TYPE(bool) % A %% prfb)))",
5.252
5.253 (* --> *)
5.254
5.255 - "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
5.256 - \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
5.257 - \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
5.258 + "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
5.259 + \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \
5.260 + \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \
5.261 \ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \
5.262 \ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
5.263
5.264 - "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
5.265 - \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
5.266 - \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
5.267 + "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
5.268 + \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \
5.269 + \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \
5.270 \ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \
5.271 \ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
5.272
5.273 - "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
5.274 - \ (HOL.refl % TYPE(bool=>bool) % op --> A)) == \
5.275 - \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
5.276 + "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \
5.277 + \ (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) == \
5.278 + \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \
5.279 \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
5.280 \ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \
5.281 - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %% \
5.282 - \ (HOL.refl % TYPE(bool) % A)))",
5.283 + \ prfb %% prfbb %% \
5.284 + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %% \
5.285 + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
5.286 + \ (HOL.refl % TYPE(bool) % A %% prfb)))",
5.287
5.288 (* ~ *)
5.289
5.290 - "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
5.291 - \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
5.292 + "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \
5.293 + \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \
5.294 \ (notI % Q %% (Lam H: Q. \
5.295 \ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
5.296
5.297 - "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
5.298 - \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
5.299 + "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \
5.300 + \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \
5.301 \ (notI % P %% (Lam H: P. \
5.302 \ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
5.303
5.304 (* = *)
5.305
5.306 "(iffD1 % B % D %% \
5.307 - \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
5.308 - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
5.309 - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
5.310 + \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
5.311 + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
5.312 + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
5.313 \ (iffD1 % C % D %% prf2 %% \
5.314 \ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
5.315
5.316 "(iffD2 % B % D %% \
5.317 - \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
5.318 - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
5.319 - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
5.320 + \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
5.321 + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
5.322 + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
5.323 \ (iffD1 % A % B %% prf1 %% \
5.324 \ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
5.325
5.326 "(iffD1 % A % C %% \
5.327 - \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
5.328 - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
5.329 - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \
5.330 + \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
5.331 + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
5.332 + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)== \
5.333 \ (iffD2 % C % D %% prf2 %% \
5.334 \ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
5.335
5.336 "(iffD2 % A % C %% \
5.337 - \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
5.338 - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
5.339 - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
5.340 + \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
5.341 + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
5.342 + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
5.343 \ (iffD2 % A % B %% prf1 %% \
5.344 \ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
5.345
5.346 - "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
5.347 - \ (HOL.refl % TYPE(bool=>bool) % op = A)) == \
5.348 - \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
5.349 + "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \
5.350 + \ (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) == \
5.351 + \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \
5.352 \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
5.353 \ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \
5.354 - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \
5.355 - \ (HOL.refl % TYPE(bool) % A)))",
5.356 + \ prfb %% prfbb %% \
5.357 + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %% \
5.358 + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
5.359 + \ (HOL.refl % TYPE(bool) % A %% prfb)))",
5.360
5.361 (** transitivity, reflexivity, and symmetry **)
5.362
5.363 - "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
5.364 + "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \
5.365 \ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
5.366
5.367 - "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
5.368 + "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \
5.369 \ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
5.370
5.371 - "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
5.372 + "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
5.373
5.374 - "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
5.375 + "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
5.376
5.377 - "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
5.378 + "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)",
5.379
5.380 - "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
5.381 + "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)",
5.382
5.383 (** normalization of HOL proofs **)
5.384
5.385 @@ -262,13 +283,13 @@
5.386
5.387 "(impI % A % B %% (mp % A % B %% prf)) == prf",
5.388
5.389 - "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
5.390 + "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x",
5.391
5.392 - "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
5.393 + "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf",
5.394
5.395 - "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
5.396 + "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)",
5.397
5.398 - "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
5.399 + "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf",
5.400
5.401 "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
5.402
5.403 @@ -286,26 +307,26 @@
5.404 (** Replace congruence rules by substitution rules **)
5.405
5.406 fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
5.407 - prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
5.408 - | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
5.409 + prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
5.410 + | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
5.411 | strip_cong _ _ = NONE;
5.412
5.413 -val subst_prf = fst (strip_combt (Thm.proof_of subst));
5.414 -val sym_prf = fst (strip_combt (Thm.proof_of sym));
5.415 +val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst))));
5.416 +val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym))));
5.417
5.418 fun make_subst Ts prf xs (_, []) = prf
5.419 - | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
5.420 + | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
5.421 let val T = fastype_of1 (Ts, x)
5.422 in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
5.423 else change_type (SOME [T]) subst_prf %> x %> y %>
5.424 Abs ("z", T, list_comb (incr_boundvars 1 f,
5.425 map (incr_boundvars 1) xs @ Bound 0 ::
5.426 - map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
5.427 + map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
5.428 make_subst Ts prf (xs @ [x]) (f, ps)
5.429 end;
5.430
5.431 -fun make_sym Ts ((x, y), prf) =
5.432 - ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
5.433 +fun make_sym Ts ((x, y), (prf, clprf)) =
5.434 + ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
5.435
5.436 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
5.437
5.438 @@ -322,6 +343,6 @@
5.439 apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
5.440 | elim_cong_aux _ _ = NONE;
5.441
5.442 -fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
5.443 +fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
5.444
5.445 end;
6.1 --- a/src/Pure/Isar/class_target.ML Tue Jun 01 11:18:51 2010 +0200
6.2 +++ b/src/Pure/Isar/class_target.ML Tue Jun 01 11:30:57 2010 +0200
6.3 @@ -243,7 +243,7 @@
6.4 | NONE => I
6.5 in
6.6 thy
6.7 - |> AxClass.add_classrel classrel
6.8 + |> AxClass.add_classrel true classrel
6.9 |> ClassData.map (Graph.add_edge (sub, sup))
6.10 |> activate_defs sub (these_defs thy diff_sort)
6.11 |> add_dependency
6.12 @@ -366,7 +366,7 @@
6.13 fun gen_classrel mk_prop classrel thy =
6.14 let
6.15 fun after_qed results =
6.16 - ProofContext.theory ((fold o fold) AxClass.add_classrel results);
6.17 + ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results);
6.18 in
6.19 thy
6.20 |> ProofContext.init_global
6.21 @@ -531,7 +531,7 @@
6.22 val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
6.23 val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
6.24 fun after_qed' results =
6.25 - Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
6.26 + Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results)
6.27 #> after_qed;
6.28 in
6.29 lthy
6.30 @@ -591,7 +591,7 @@
6.31 val sorts = map snd vs;
6.32 val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
6.33 fun after_qed results = ProofContext.theory
6.34 - ((fold o fold) AxClass.add_arity results);
6.35 + ((fold o fold) (AxClass.add_arity true) results);
6.36 in
6.37 thy
6.38 |> ProofContext.init_global
7.1 --- a/src/Pure/Proof/extraction.ML Tue Jun 01 11:18:51 2010 +0200
7.2 +++ b/src/Pure/Proof/extraction.ML Tue Jun 01 11:30:57 2010 +0200
7.3 @@ -24,6 +24,7 @@
7.4 val mk_typ : typ -> term
7.5 val etype_of : theory -> string list -> typ list -> term -> typ
7.6 val realizes_of: theory -> string list -> term -> term -> term
7.7 + val abs_corr_shyps: theory -> thm -> string list -> term list -> Proofterm.proof -> Proofterm.proof
7.8 end;
7.9
7.10 structure Extraction : EXTRACTION =
7.11 @@ -126,11 +127,9 @@
7.12 fun frees_of t = map Free (rev (Term.add_frees t []));
7.13 fun vfs_of t = vars_of t @ frees_of t;
7.14
7.15 -fun forall_intr_prf (t, prf) =
7.16 - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
7.17 - in Abst (a, SOME T, prf_abstract_over t prf) end;
7.18 +val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
7.19
7.20 -val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
7.21 +val mkabsp = fold_rev (fn t => fn prf => AbsP ("H", SOME t, prf));
7.22
7.23 fun strip_abs 0 t = t
7.24 | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
7.25 @@ -161,6 +160,14 @@
7.26 | _ => error "get_var_type: not a variable"
7.27 end;
7.28
7.29 +fun read_term thy T s =
7.30 + let
7.31 + val ctxt = ProofContext.init_global thy
7.32 + |> Proof_Syntax.strip_sorts_consttypes
7.33 + |> ProofContext.set_defsort [];
7.34 + val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
7.35 + in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
7.36 +
7.37
7.38 (**** theory data ****)
7.39
7.40 @@ -175,7 +182,7 @@
7.41 (term -> typ -> term -> typ -> term) option)) list,
7.42 realizers : (string list * (term * proof)) list Symtab.table,
7.43 defs : thm list,
7.44 - expand : (string * term) list,
7.45 + expand : string list,
7.46 prep : (theory -> proof -> proof) option}
7.47
7.48 val empty =
7.49 @@ -198,14 +205,14 @@
7.50 types = AList.merge (op =) (K true) (types1, types2),
7.51 realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
7.52 defs = Library.merge Thm.eq_thm (defs1, defs2),
7.53 - expand = Library.merge (op =) (expand1, expand2), (* FIXME proper aconv !?! *)
7.54 + expand = Library.merge (op =) (expand1, expand2),
7.55 prep = (case prep1 of NONE => prep2 | _ => prep1)};
7.56 );
7.57
7.58 fun read_condeq thy =
7.59 let val thy' = add_syntax thy
7.60 in fn s =>
7.61 - let val t = Logic.varify_global (Syntax.read_prop_global thy' s)
7.62 + let val t = Logic.varify_global (read_term thy' propT s)
7.63 in
7.64 (map Logic.dest_equals (Logic.strip_imp_prems t),
7.65 Logic.dest_equals (Logic.strip_imp_concl t))
7.66 @@ -274,7 +281,7 @@
7.67 fun err () = error ("Unable to determine type of extracted program for\n" ^
7.68 Syntax.string_of_term_global thy t)
7.69 in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
7.70 - [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
7.71 + [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
7.72 Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
7.73 Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
7.74 | _ => err ()
7.75 @@ -300,25 +307,30 @@
7.76 val rtypes = map fst types;
7.77 val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
7.78 val thy' = add_syntax thy;
7.79 - val rd = Proof_Syntax.read_proof thy' false;
7.80 + val rd = Proof_Syntax.read_proof thy' true false;
7.81 in fn (thm, (vs, s1, s2)) =>
7.82 let
7.83 val name = Thm.derivation_name thm;
7.84 val _ = name <> "" orelse error "add_realizers: unnamed theorem";
7.85 - val prop = Pattern.rewrite_term thy'
7.86 - (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
7.87 + val prop = Thm.unconstrainT thm |> prop_of |>
7.88 + Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [];
7.89 val vars = vars_of prop;
7.90 val vars' = filter_out (fn v =>
7.91 member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
7.92 + val shyps = maps (fn Var ((x, i), _) =>
7.93 + if member (op =) vs x then Logic.mk_of_sort
7.94 + (TVar (("'" ^ x, i), []), Sign.defaultS thy')
7.95 + else []) vars;
7.96 val T = etype_of thy' vs [] prop;
7.97 val (T', thw) = Type.legacy_freeze_thaw_type
7.98 (if T = nullT then nullT else map fastype_of vars' ---> T);
7.99 - val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
7.100 + val t = map_types thw (read_term thy' T' s1);
7.101 val r' = freeze_thaw (condrew thy' eqns
7.102 - (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
7.103 + (procs @ [typeof_proc [] vs, rlz_proc]))
7.104 (Const ("realizes", T --> propT --> propT) $
7.105 (if T = nullT then t else list_comb (t, vars')) $ prop);
7.106 - val r = fold_rev Logic.all (map (get_var_type r') vars) r';
7.107 + val r = Logic.list_implies (shyps,
7.108 + fold_rev Logic.all (map (get_var_type r') vars) r');
7.109 val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
7.110 in (name, (vs, (t, prf))) end
7.111 end;
7.112 @@ -337,10 +349,34 @@
7.113 val prop' = Pattern.rewrite_term thy'
7.114 (map (Logic.dest_equals o prop_of) defs) [] prop;
7.115 in freeze_thaw (condrew thy' eqns
7.116 - (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
7.117 + (procs @ [typeof_proc [] vs, rlz_proc]))
7.118 (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
7.119 end;
7.120
7.121 +fun abs_corr_shyps thy thm vs xs prf =
7.122 + let
7.123 + val S = Sign.defaultS thy;
7.124 + val ((atyp_map, constraints, _), prop') =
7.125 + Logic.unconstrainT (#shyps (rep_thm thm)) (prop_of thm);
7.126 + val atyps = fold_types (fold_atyps (insert (op =))) (prop_of thm) [];
7.127 + val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
7.128 + SOME (TVar (("'" ^ v, i), [])) else NONE)
7.129 + (rev (Term.add_vars prop' []));
7.130 + val cs = maps (fn T => map (pair T) S) Ts;
7.131 + val constraints' = map Logic.mk_of_class cs;
7.132 + val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints);
7.133 + fun typ_map T = Type.strip_sorts
7.134 + (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
7.135 + fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
7.136 + val xs' = map (map_types typ_map) xs
7.137 + in
7.138 + prf |>
7.139 + Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
7.140 + fold_rev implies_intr_proof' (map snd constraints) |>
7.141 + fold_rev forall_intr_proof' xs' |>
7.142 + fold_rev implies_intr_proof' constraints'
7.143 + end;
7.144 +
7.145 (** expanding theorems / definitions **)
7.146
7.147 fun add_expand_thm is_def thm thy =
7.148 @@ -354,15 +390,15 @@
7.149 thy |> ExtractionData.put
7.150 (if is_def then
7.151 {realizes_eqns = realizes_eqns,
7.152 - typeof_eqns = add_rule ([],
7.153 - Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
7.154 + typeof_eqns = add_rule ([], Logic.dest_equals (map_types
7.155 + Type.strip_sorts (prop_of (Drule.abs_def thm)))) typeof_eqns,
7.156 types = types,
7.157 realizers = realizers, defs = insert Thm.eq_thm thm defs,
7.158 expand = expand, prep = prep}
7.159 else
7.160 {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
7.161 realizers = realizers, defs = defs,
7.162 - expand = insert (op =) (name, prop_of thm) expand, prep = prep})
7.163 + expand = insert (op =) name expand, prep = prep})
7.164 end;
7.165
7.166 fun extraction_expand is_def =
7.167 @@ -443,9 +479,9 @@
7.168 ExtractionData.get thy;
7.169 val procs = maps (rev o fst o snd) types;
7.170 val rtypes = map fst types;
7.171 - val typroc = typeof_proc (Sign.defaultS thy');
7.172 + val typroc = typeof_proc [];
7.173 val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
7.174 - Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
7.175 + Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
7.176 val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
7.177
7.178 fun find_inst prop Ts ts vs =
7.179 @@ -464,6 +500,13 @@
7.180
7.181 in fold_rev add_args (take n vars ~~ take n ts) ([], []) end;
7.182
7.183 + fun mk_shyps tye = maps (fn (ixn, _) =>
7.184 + Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
7.185 +
7.186 + fun mk_sprfs cs tye = maps (fn (_, T) =>
7.187 + ProofRewriteRules.mk_of_sort_proof thy (map SOME cs)
7.188 + (T, Sign.defaultS thy)) tye;
7.189 +
7.190 fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
7.191 fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
7.192
7.193 @@ -474,22 +517,22 @@
7.194 fun realizes_null vs prop = app_rlz_rews [] vs
7.195 (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
7.196
7.197 - fun corr d defs vs ts Ts hs (PBound i) _ _ = (defs, PBound i)
7.198 + fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i)
7.199
7.200 - | corr d defs vs ts Ts hs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
7.201 + | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
7.202 let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
7.203 - (dummyt :: hs) prf (incr_pboundvars 1 0 prf')
7.204 + (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
7.205 (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
7.206 in (defs', Abst (s, SOME T, corr_prf)) end
7.207
7.208 - | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
7.209 + | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
7.210 let
7.211 val T = etype_of thy' vs Ts prop;
7.212 val u = if T = nullT then
7.213 (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
7.214 else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
7.215 val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
7.216 - (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
7.217 + (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
7.218 val rlz = Const ("realizes", T --> propT --> propT)
7.219 in (defs',
7.220 if T = nullT then AbsP ("R",
7.221 @@ -500,10 +543,10 @@
7.222 (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
7.223 end
7.224
7.225 - | corr d defs vs ts Ts hs (prf % SOME t) (prf' % _) t' =
7.226 + | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' =
7.227 let
7.228 val (Us, T) = strip_type (fastype_of1 (Ts, t));
7.229 - val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
7.230 + val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf'
7.231 (if member (op =) rtypes (tname_of T) then t'
7.232 else (case t' of SOME (u $ _) => SOME u | _ => NONE));
7.233 val u = if not (member (op =) rtypes (tname_of T)) then t else
7.234 @@ -519,7 +562,7 @@
7.235 in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
7.236 in (defs', corr_prf % SOME u) end
7.237
7.238 - | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
7.239 + | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
7.240 let
7.241 val prop = Reconstruct.prop_of' hs prf2';
7.242 val T = etype_of thy' vs Ts prop;
7.243 @@ -529,17 +572,19 @@
7.244 | _ =>
7.245 let val (defs1, u) = extr d defs vs [] Ts hs prf2'
7.246 in (defs1, NONE, SOME u) end)
7.247 - val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs prf1 prf1' f;
7.248 - val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs prf2 prf2' u;
7.249 + val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f;
7.250 + val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u;
7.251 in
7.252 if T = nullT then (defs3, corr_prf1 %% corr_prf2) else
7.253 (defs3, corr_prf1 % u %% corr_prf2)
7.254 end
7.255
7.256 - | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
7.257 + | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
7.258 let
7.259 val prf = join_proof body;
7.260 val (vs', tye) = find_inst prop Ts ts vs;
7.261 + val shyps = mk_shyps tye;
7.262 + val sprfs = mk_sprfs cs tye;
7.263 val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
7.264 val T = etype_of thy' vs' [] prop;
7.265 val defs' = if T = nullT then defs
7.266 @@ -555,28 +600,31 @@
7.267 (if null vs' then ""
7.268 else " (relevant variables: " ^ commas_quote vs' ^ ")"));
7.269 val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
7.270 - val (defs'', corr_prf) =
7.271 - corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
7.272 + val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] []
7.273 + (rev shyps) prf' prf' NONE;
7.274 + val corr_prf = mkabsp shyps corr_prf0;
7.275 val corr_prop = Reconstruct.prop_of corr_prf;
7.276 - val corr_prf' = List.foldr forall_intr_prf
7.277 - (proof_combt
7.278 + val corr_prf' =
7.279 + proof_combP (proof_combt
7.280 (PThm (serial (),
7.281 ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
7.282 - Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
7.283 - (map (get_var_type corr_prop) (vfs_of prop))
7.284 + Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
7.285 + map PBound (length shyps - 1 downto 0)) |>
7.286 + fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
7.287 + mkabsp shyps
7.288 in
7.289 ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
7.290 - prf_subst_TVars tye' corr_prf')
7.291 + proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
7.292 end
7.293 - | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf'))
7.294 + | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
7.295 | SOME rs => (case find vs' rs of
7.296 - SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
7.297 + SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
7.298 | NONE => error ("corr: no realizer for instance of theorem " ^
7.299 quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
7.300 (Reconstruct.prop_of (proof_combt (prf0, ts))))))
7.301 end
7.302
7.303 - | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
7.304 + | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
7.305 let
7.306 val (vs', tye) = find_inst prop Ts ts vs;
7.307 val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
7.308 @@ -584,13 +632,14 @@
7.309 if etype_of thy' vs' [] prop = nullT andalso
7.310 realizes_null vs' prop aconv prop then (defs, prf0)
7.311 else case find vs' (Symtab.lookup_list realizers s) of
7.312 - SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
7.313 + SOME (_, prf) => (defs,
7.314 + proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
7.315 | NONE => error ("corr: no realizer for instance of axiom " ^
7.316 quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
7.317 (Reconstruct.prop_of (proof_combt (prf0, ts)))))
7.318 end
7.319
7.320 - | corr d defs vs ts Ts hs _ _ _ = error "corr: bad proof"
7.321 + | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
7.322
7.323 and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i)
7.324
7.325 @@ -630,6 +679,7 @@
7.326 let
7.327 val prf = join_proof body;
7.328 val (vs', tye) = find_inst prop Ts ts vs;
7.329 + val shyps = mk_shyps tye;
7.330 val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
7.331 in
7.332 case Symtab.lookup realizers s of
7.333 @@ -641,18 +691,18 @@
7.334 else " (relevant variables: " ^ commas_quote vs' ^ ")"));
7.335 val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
7.336 val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
7.337 - val (defs'', corr_prf) =
7.338 - corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
7.339 + val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] []
7.340 + (rev shyps) prf' prf' (SOME t);
7.341
7.342 val nt = Envir.beta_norm t;
7.343 val args = filter_out (fn v => member (op =) rtypes
7.344 (tname_of (body_type (fastype_of v)))) (vfs_of prop);
7.345 val args' = filter (fn v => Logic.occs (v, nt)) args;
7.346 - val t' = mkabs nt args';
7.347 + val t' = mkabs args' nt;
7.348 val T = fastype_of t';
7.349 val cname = extr_name s vs';
7.350 val c = Const (cname, T);
7.351 - val u = mkabs (list_comb (c, args')) args;
7.352 + val u = mkabs args (list_comb (c, args'));
7.353 val eqn = Logic.mk_equals (c, t');
7.354 val rlz =
7.355 Const ("realizes", fastype_of nt --> propT --> propT);
7.356 @@ -661,20 +711,22 @@
7.357 val f = app_rlz_rews [] vs'
7.358 (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
7.359
7.360 - val corr_prf' =
7.361 - chtype [] equal_elim_axm %> lhs %> rhs %%
7.362 + val corr_prf' = mkabsp shyps
7.363 + (chtype [] equal_elim_axm %> lhs %> rhs %%
7.364 (chtype [propT] symmetric_axm %> rhs %> lhs %%
7.365 (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
7.366 (chtype [T --> propT] reflexive_axm %> f) %%
7.367 PAxm (cname ^ "_def", eqn,
7.368 - SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
7.369 + SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
7.370 val corr_prop = Reconstruct.prop_of corr_prf';
7.371 - val corr_prf'' = List.foldr forall_intr_prf
7.372 - (proof_combt
7.373 + val corr_prf'' =
7.374 + proof_combP (proof_combt
7.375 (PThm (serial (),
7.376 ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
7.377 - Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
7.378 - (map (get_var_type corr_prop) (vfs_of prop));
7.379 + Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
7.380 + map PBound (length shyps - 1 downto 0)) |>
7.381 + fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
7.382 + mkabsp shyps
7.383 in
7.384 ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
7.385 subst_TVars tye' u)
7.386 @@ -731,7 +783,7 @@
7.387 in
7.388 thy'
7.389 |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
7.390 - Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
7.391 + Thm.varifyT_global (funpow (length (vars_of corr_prop))
7.392 (Thm.forall_elim_var 0) (Thm.forall_intr_frees
7.393 (ProofChecker.thm_of_proof thy'
7.394 (fst (Proofterm.freeze_thaw_prf prf))))))
8.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 11:18:51 2010 +0200
8.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 11:30:57 2010 +0200
8.3 @@ -6,14 +6,17 @@
8.4
8.5 signature PROOF_REWRITE_RULES =
8.6 sig
8.7 - val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
8.8 + val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
8.9 val rprocs : bool ->
8.10 - (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
8.11 + (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
8.12 val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
8.13 val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
8.14 val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
8.15 val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
8.16 val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
8.17 + val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
8.18 + val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
8.19 + (Proofterm.proof * Proofterm.proof) option
8.20 end;
8.21
8.22 structure ProofRewriteRules : PROOF_REWRITE_RULES =
8.23 @@ -21,7 +24,7 @@
8.24
8.25 open Proofterm;
8.26
8.27 -fun rew b _ =
8.28 +fun rew b _ _ =
8.29 let
8.30 fun ?? x = if b then SOME x else NONE;
8.31 fun ax (prf as PAxm (s, prop, _)) Ts =
8.32 @@ -219,31 +222,36 @@
8.33 fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
8.34
8.35 fun insert_refl defs Ts (prf1 %% prf2) =
8.36 - insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
8.37 + let val (prf1', b) = insert_refl defs Ts prf1
8.38 + in
8.39 + if b then (prf1', true)
8.40 + else (prf1' %% fst (insert_refl defs Ts prf2), false)
8.41 + end
8.42 | insert_refl defs Ts (Abst (s, SOME T, prf)) =
8.43 - Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
8.44 + (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
8.45 | insert_refl defs Ts (AbsP (s, t, prf)) =
8.46 - AbsP (s, t, insert_refl defs Ts prf)
8.47 + (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
8.48 | insert_refl defs Ts prf = (case strip_combt prf of
8.49 (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
8.50 if member (op =) defs s then
8.51 let
8.52 val vs = vars_of prop;
8.53 val tvars = Term.add_tvars prop [] |> rev;
8.54 - val (_, rhs) = Logic.dest_equals prop;
8.55 + val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
8.56 val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
8.57 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
8.58 map the ts);
8.59 in
8.60 - change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
8.61 + (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true)
8.62 end
8.63 - else prf
8.64 - | (_, []) => prf
8.65 - | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
8.66 + else (prf, false)
8.67 + | (_, []) => (prf, false)
8.68 + | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
8.69
8.70 fun elim_defs thy r defs prf =
8.71 let
8.72 - val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
8.73 + val defs' = map (Logic.dest_equals o
8.74 + map_types Type.strip_sorts o prop_of o Drule.abs_def) defs;
8.75 val defnames = map Thm.derivation_name defs;
8.76 val f = if not r then I else
8.77 let
8.78 @@ -258,7 +266,7 @@
8.79 in Reconstruct.expand_proof thy thms end;
8.80 in
8.81 rewrite_terms (Pattern.rewrite_term thy defs' [])
8.82 - (insert_refl defnames [] (f prf))
8.83 + (fst (insert_refl defnames [] (f prf)))
8.84 end;
8.85
8.86
8.87 @@ -327,4 +335,35 @@
8.88 mk_prf Q
8.89 end;
8.90
8.91 +
8.92 +(**** expand OfClass proofs ****)
8.93 +
8.94 +fun mk_of_sort_proof thy hs (T, S) =
8.95 + let
8.96 + val hs' = map
8.97 + (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
8.98 + | NONE => NONE) hs;
8.99 + val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
8.100 + fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
8.101 + val subst = map_atyps
8.102 + (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
8.103 + | T as TFree (s, _) => TFree (s, get_sort T));
8.104 + fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
8.105 + ~1 => error "expand_of_class: missing class hypothesis"
8.106 + | i => PBound i;
8.107 + fun reconstruct prf prop = prf |>
8.108 + Reconstruct.reconstruct_proof thy prop |>
8.109 + Reconstruct.expand_proof thy [("", NONE)] |>
8.110 + Same.commit (map_proof_same Same.same Same.same hyp)
8.111 + in
8.112 + map2 reconstruct
8.113 + (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
8.114 + (Logic.mk_of_sort (T, S))
8.115 + end;
8.116 +
8.117 +fun expand_of_class thy Ts hs (OfClass (T, c)) =
8.118 + mk_of_sort_proof thy hs (T, [c]) |>
8.119 + hd |> rpair no_skel |> SOME
8.120 + | expand_of_class thy Ts hs _ = NONE;
8.121 +
8.122 end;
9.1 --- a/src/Pure/Proof/proof_syntax.ML Tue Jun 01 11:18:51 2010 +0200
9.2 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jun 01 11:30:57 2010 +0200
9.3 @@ -11,8 +11,9 @@
9.4 val proof_of_term: theory -> bool -> term -> Proofterm.proof
9.5 val term_of_proof: Proofterm.proof -> term
9.6 val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
9.7 - val read_term: theory -> typ -> string -> term
9.8 - val read_proof: theory -> bool -> string -> Proofterm.proof
9.9 + val strip_sorts_consttypes: Proof.context -> Proof.context
9.10 + val read_term: theory -> bool -> typ -> string -> term
9.11 + val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
9.12 val proof_syntax: Proofterm.proof -> theory -> theory
9.13 val proof_of: bool -> thm -> Proofterm.proof
9.14 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
9.15 @@ -109,7 +110,7 @@
9.16 | "thm" :: xs =>
9.17 let val name = Long_Name.implode xs;
9.18 in (case AList.lookup (op =) thms name of
9.19 - SOME thm => fst (strip_combt (Thm.proof_of thm))
9.20 + SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm))))
9.21 | NONE => error ("Unknown theorem " ^ quote name))
9.22 end
9.23 | _ => error ("Illegal proof constant name: " ^ quote s))
9.24 @@ -198,7 +199,14 @@
9.25 (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
9.26 end;
9.27
9.28 -fun read_term thy =
9.29 +fun strip_sorts_consttypes ctxt =
9.30 + let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt)
9.31 + in Symtab.fold (fn (s, (T, _)) =>
9.32 + ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T)))
9.33 + tab ctxt
9.34 + end;
9.35 +
9.36 +fun read_term thy topsort =
9.37 let
9.38 val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
9.39 val axm_names = map fst (Theory.all_axioms_of thy);
9.40 @@ -208,15 +216,19 @@
9.41 (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
9.42 |> ProofContext.init_global
9.43 |> ProofContext.allow_dummies
9.44 - |> ProofContext.set_mode ProofContext.mode_schematic;
9.45 + |> ProofContext.set_mode ProofContext.mode_schematic
9.46 + |> (if topsort then
9.47 + strip_sorts_consttypes #>
9.48 + ProofContext.set_defsort []
9.49 + else I);
9.50 in
9.51 fn ty => fn s =>
9.52 (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
9.53 |> Type_Infer.constrain ty |> Syntax.check_term ctxt
9.54 end;
9.55
9.56 -fun read_proof thy =
9.57 - let val rd = read_term thy proofT
9.58 +fun read_proof thy topsort =
9.59 + let val rd = read_term thy topsort proofT
9.60 in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end;
9.61
9.62 fun proof_syntax prf =
10.1 --- a/src/Pure/Proof/proofchecker.ML Tue Jun 01 11:18:51 2010 +0200
10.2 +++ b/src/Pure/Proof/proofchecker.ML Tue Jun 01 11:30:57 2010 +0200
10.3 @@ -28,6 +28,48 @@
10.4 val beta_eta_convert =
10.5 Conv.fconv_rule Drule.beta_eta_conversion;
10.6
10.7 +(* equality modulo renaming of type variables *)
10.8 +fun is_equal t t' =
10.9 + let
10.10 + val atoms = fold_types (fold_atyps (insert (op =))) t [];
10.11 + val atoms' = fold_types (fold_atyps (insert (op =))) t' []
10.12 + in
10.13 + length atoms = length atoms' andalso
10.14 + map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
10.15 + end;
10.16 +
10.17 +fun pretty_prf thy vs Hs prf =
10.18 + let val prf' = prf |> prf_subst_bounds (map Free vs) |>
10.19 + prf_subst_pbounds (map (Hyp o prop_of) Hs)
10.20 + in
10.21 + (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
10.22 + Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
10.23 + end;
10.24 +
10.25 +fun pretty_term thy vs _ t =
10.26 + let val t' = subst_bounds (map Free vs, t)
10.27 + in
10.28 + (Syntax.pretty_term_global thy t',
10.29 + Syntax.pretty_typ_global thy (fastype_of t'))
10.30 + end;
10.31 +
10.32 +fun appl_error thy prt vs Hs s f a =
10.33 + let
10.34 + val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
10.35 + val (pp_a, pp_aT) = prt thy vs Hs a
10.36 + in
10.37 + error (cat_lines
10.38 + [s,
10.39 + "",
10.40 + Pretty.string_of (Pretty.block
10.41 + [Pretty.str "Operator:", Pretty.brk 2, pp_f,
10.42 + Pretty.str " ::", Pretty.brk 1, pp_fT]),
10.43 + Pretty.string_of (Pretty.block
10.44 + [Pretty.str "Operand:", Pretty.brk 3, pp_a,
10.45 + Pretty.str " ::", Pretty.brk 1, pp_aT]),
10.46 + ""])
10.47 + end;
10.48 +
10.49 fun thm_of_proof thy prf =
10.50 let
10.51 val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
10.52 @@ -45,9 +87,9 @@
10.53
10.54 fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
10.55 let
10.56 - val thm = Drule.implies_intr_hyps (lookup name);
10.57 + val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
10.58 val {prop, ...} = rep_thm thm;
10.59 - val _ = if prop aconv prop' then () else
10.60 + val _ = if is_equal prop prop' then () else
10.61 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
10.62 Syntax.string_of_term_global thy prop ^ "\n\n" ^
10.63 Syntax.string_of_term_global thy prop');
10.64 @@ -70,7 +112,10 @@
10.65 let
10.66 val thm = thm_of (vs, names) Hs prf;
10.67 val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
10.68 - in Thm.forall_elim ct thm end
10.69 + in
10.70 + Thm.forall_elim ct thm
10.71 + handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
10.72 + end
10.73
10.74 | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
10.75 let
10.76 @@ -86,6 +131,7 @@
10.77 val thm' = beta_eta_convert (thm_of vars Hs prf');
10.78 in
10.79 Thm.implies_elim thm thm'
10.80 + handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
10.81 end
10.82
10.83 | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
11.1 --- a/src/Pure/Proof/reconstruct.ML Tue Jun 01 11:18:51 2010 +0200
11.2 +++ b/src/Pure/Proof/reconstruct.ML Tue Jun 01 11:30:57 2010 +0200
11.3 @@ -28,11 +28,7 @@
11.4 fun forall_intr_vfs prop = fold_rev Logic.all
11.5 (vars_of prop @ frees_of prop) prop;
11.6
11.7 -fun forall_intr_prf t prf =
11.8 - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
11.9 - in Abst (a, SOME T, prf_abstract_over t prf) end;
11.10 -
11.11 -fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
11.12 +fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof'
11.13 (vars_of prop @ frees_of prop) prf;
11.14
11.15
12.1 --- a/src/Pure/axclass.ML Tue Jun 01 11:18:51 2010 +0200
12.2 +++ b/src/Pure/axclass.ML Tue Jun 01 11:30:57 2010 +0200
12.3 @@ -24,8 +24,8 @@
12.4 val read_classrel: theory -> xstring * xstring -> class * class
12.5 val declare_overloaded: string * typ -> theory -> term * theory
12.6 val define_overloaded: binding -> string * term -> theory -> thm * theory
12.7 - val add_classrel: thm -> theory -> theory
12.8 - val add_arity: thm -> theory -> theory
12.9 + val add_classrel: bool -> thm -> theory -> theory
12.10 + val add_arity: bool -> thm -> theory -> theory
12.11 val prove_classrel: class * class -> tactic -> theory -> theory
12.12 val prove_arity: string * sort list * sort -> tactic -> theory -> theory
12.13 val define_class: binding * class list -> string list ->
12.14 @@ -412,46 +412,55 @@
12.15
12.16 (* primitive rules *)
12.17
12.18 -fun add_classrel raw_th thy =
12.19 +fun add_classrel store raw_th thy =
12.20 let
12.21 val th = Thm.strip_shyps (Thm.transfer thy raw_th);
12.22 val prop = Thm.plain_prop_of th;
12.23 fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
12.24 val rel = Logic.dest_classrel prop handle TERM _ => err ();
12.25 val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
12.26 - val th' = th
12.27 + val (th', thy') =
12.28 + if store then PureThy.store_thm
12.29 + (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
12.30 + else (th, thy);
12.31 + val th'' = th'
12.32 |> Thm.unconstrainT
12.33 - |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] [];
12.34 + |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
12.35 in
12.36 - thy
12.37 + thy'
12.38 |> Sign.primitive_classrel (c1, c2)
12.39 - |> (#2 oo put_trancl_classrel) ((c1, c2), th')
12.40 + |> (#2 oo put_trancl_classrel) ((c1, c2), th'')
12.41 |> perhaps complete_arities
12.42 end;
12.43
12.44 -fun add_arity raw_th thy =
12.45 +fun add_arity store raw_th thy =
12.46 let
12.47 val th = Thm.strip_shyps (Thm.transfer thy raw_th);
12.48 val prop = Thm.plain_prop_of th;
12.49 fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
12.50 - val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
12.51 + val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
12.52 +
12.53 + val (th', thy') =
12.54 + if store then PureThy.store_thm
12.55 + (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
12.56 + else (th, thy);
12.57
12.58 val args = Name.names Name.context Name.aT Ss;
12.59 val T = Type (t, map TFree args);
12.60 - val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), [])))) args;
12.61 + val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
12.62
12.63 - val missing_params = Sign.complete_sort thy [c]
12.64 - |> maps (these o Option.map #params o try (get_info thy))
12.65 - |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
12.66 + val missing_params = Sign.complete_sort thy' [c]
12.67 + |> maps (these o Option.map #params o try (get_info thy'))
12.68 + |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t))
12.69 |> (map o apsnd o map_atyps) (K T);
12.70 - val th' = th
12.71 + val th'' = th'
12.72 |> Thm.unconstrainT
12.73 |> Drule.instantiate' std_vars [];
12.74 in
12.75 - thy
12.76 + thy'
12.77 |> fold (#2 oo declare_overloaded) missing_params
12.78 |> Sign.primitive_arity (t, Ss, [c])
12.79 - |> put_arity ((t, Ss, c), th')
12.80 + |> put_arity ((t, Ss, c), th'')
12.81 end;
12.82
12.83
12.84 @@ -468,7 +477,7 @@
12.85 thy
12.86 |> PureThy.add_thms [((Binding.name
12.87 (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
12.88 - |-> (fn [th'] => add_classrel th')
12.89 + |-> (fn [th'] => add_classrel false th')
12.90 end;
12.91
12.92 fun prove_arity raw_arity tac thy =
12.93 @@ -484,7 +493,7 @@
12.94 in
12.95 thy
12.96 |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
12.97 - |-> fold add_arity
12.98 + |-> fold (add_arity false)
12.99 end;
12.100
12.101
12.102 @@ -618,11 +627,11 @@
12.103
12.104 fun ax_classrel prep =
12.105 axiomatize (map o prep) (map Logic.mk_classrel)
12.106 - (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
12.107 + (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false);
12.108
12.109 fun ax_arity prep =
12.110 axiomatize (prep o ProofContext.init_global) Logic.mk_arities
12.111 - (map (prefix arity_prefix) o Logic.name_arities) add_arity;
12.112 + (map (prefix arity_prefix) o Logic.name_arities) (add_arity false);
12.113
12.114 fun class_const c =
12.115 (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
13.1 --- a/src/Pure/logic.ML Tue Jun 01 11:18:51 2010 +0200
13.2 +++ b/src/Pure/logic.ML Tue Jun 01 11:30:57 2010 +0200
13.3 @@ -46,7 +46,8 @@
13.4 val name_arity: string * sort list * class -> string
13.5 val mk_arities: arity -> term list
13.6 val dest_arity: term -> string * sort list * class
13.7 - val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
13.8 + val unconstrainT: sort list -> term ->
13.9 + ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
13.10 val protectC: term
13.11 val protect: term -> term
13.12 val unprotect: term -> term
13.13 @@ -299,11 +300,15 @@
13.14 map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
13.15 constraints_map;
13.16
13.17 + val outer_constraints =
13.18 + maps (fn (T, S) => map (pair T) S)
13.19 + (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
13.20 +
13.21 val prop' =
13.22 prop
13.23 |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
13.24 |> curry list_implies (map snd constraints);
13.25 - in ((atyp_map, constraints), prop') end;
13.26 + in ((atyp_map, constraints, outer_constraints), prop') end;
13.27
13.28
13.29
14.1 --- a/src/Pure/proofterm.ML Tue Jun 01 11:18:51 2010 +0200
14.2 +++ b/src/Pure/proofterm.ML Tue Jun 01 11:30:57 2010 +0200
14.3 @@ -58,6 +58,8 @@
14.4 val strip_combt: proof -> proof * term option list
14.5 val strip_combP: proof -> proof * proof list
14.6 val strip_thm: proof_body -> proof_body
14.7 + val map_proof_same: term Same.operation -> typ Same.operation
14.8 + -> (typ * class -> proof) -> proof Same.operation
14.9 val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
14.10 val map_proof_types_same: typ Same.operation -> proof Same.operation
14.11 val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
14.12 @@ -80,7 +82,9 @@
14.13
14.14 (** proof terms for specific inference rules **)
14.15 val implies_intr_proof: term -> proof -> proof
14.16 + val implies_intr_proof': term -> proof -> proof
14.17 val forall_intr_proof: term -> string -> proof -> proof
14.18 + val forall_intr_proof': term -> proof -> proof
14.19 val varify_proof: term -> (string * sort) list -> proof -> proof
14.20 val legacy_freezeT: term -> proof -> proof
14.21 val rotate_proof: term list -> term -> int -> proof -> proof
14.22 @@ -121,13 +125,13 @@
14.23
14.24 (** rewriting on proof terms **)
14.25 val add_prf_rrule: proof * proof -> theory -> theory
14.26 - val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory
14.27 + val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
14.28 val no_skel: proof
14.29 val normal_skel: proof
14.30 val rewrite_proof: theory -> (proof * proof) list *
14.31 - (typ list -> proof -> (proof * proof) option) list -> proof -> proof
14.32 + (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
14.33 val rewrite_proof_notypes: (proof * proof) list *
14.34 - (typ list -> proof -> (proof * proof) option) list -> proof -> proof
14.35 + (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
14.36 val rew_proof: theory -> proof -> proof
14.37
14.38 val promise_proof: theory -> serial -> term -> proof
14.39 @@ -618,7 +622,7 @@
14.40
14.41 (***** implication introduction *****)
14.42
14.43 -fun implies_intr_proof h prf =
14.44 +fun gen_implies_intr_proof f h prf =
14.45 let
14.46 fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME
14.47 | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
14.48 @@ -630,14 +634,21 @@
14.49 | abshyp _ _ = raise Same.SAME
14.50 and abshyph i prf = (abshyp i prf handle Same.SAME => prf);
14.51 in
14.52 - AbsP ("H", NONE (*h*), abshyph 0 prf)
14.53 + AbsP ("H", f h, abshyph 0 prf)
14.54 end;
14.55
14.56 +val implies_intr_proof = gen_implies_intr_proof (K NONE);
14.57 +val implies_intr_proof' = gen_implies_intr_proof SOME;
14.58 +
14.59
14.60 (***** forall introduction *****)
14.61
14.62 fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
14.63
14.64 +fun forall_intr_proof' t prf =
14.65 + let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
14.66 + in Abst (a, SOME T, prf_abstract_over t prf) end;
14.67 +
14.68
14.69 (***** varify *****)
14.70
14.71 @@ -1105,7 +1116,7 @@
14.72
14.73 fun flt (i: int) = filter (fn n => n < i);
14.74
14.75 -fun fomatch Ts tymatch j =
14.76 +fun fomatch Ts tymatch j instsp p =
14.77 let
14.78 fun mtch (instsp as (tyinsts, insts)) = fn
14.79 (Var (ixn, T), t) =>
14.80 @@ -1120,7 +1131,7 @@
14.81 | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
14.82 | (Bound i, Bound j) => if i=j then instsp else raise PMatch
14.83 | _ => raise PMatch
14.84 - in mtch end;
14.85 + in mtch instsp (pairself Envir.beta_eta_contract p) end;
14.86
14.87 fun match_proof Ts tymatch =
14.88 let
14.89 @@ -1253,72 +1264,72 @@
14.90
14.91 fun rewrite_prf tymatch (rules, procs) prf =
14.92 let
14.93 - fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
14.94 - | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
14.95 - | rew Ts prf =
14.96 - (case get_first (fn r => r Ts prf) procs of
14.97 + fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
14.98 + | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
14.99 + | rew Ts hs prf =
14.100 + (case get_first (fn r => r Ts hs prf) procs of
14.101 NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
14.102 (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
14.103 handle PMatch => NONE) (filter (could_unify prf o fst) rules)
14.104 | some => some);
14.105
14.106 - fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
14.107 - if prf_loose_Pbvar1 prf' 0 then rew Ts prf
14.108 + fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) =
14.109 + if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf
14.110 else
14.111 let val prf'' = incr_pboundvars (~1) 0 prf'
14.112 - in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
14.113 - | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
14.114 - if prf_loose_bvar1 prf' 0 then rew Ts prf
14.115 + in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
14.116 + | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) =
14.117 + if prf_loose_bvar1 prf' 0 then rew Ts hs prf
14.118 else
14.119 let val prf'' = incr_pboundvars 0 (~1) prf'
14.120 - in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
14.121 - | rew0 Ts prf = rew Ts prf;
14.122 + in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
14.123 + | rew0 Ts hs prf = rew Ts hs prf;
14.124
14.125 - fun rew1 _ (Hyp (Var _)) _ = NONE
14.126 - | rew1 Ts skel prf = (case rew2 Ts skel prf of
14.127 - SOME prf1 => (case rew0 Ts prf1 of
14.128 - SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2))
14.129 + fun rew1 _ _ (Hyp (Var _)) _ = NONE
14.130 + | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of
14.131 + SOME prf1 => (case rew0 Ts hs prf1 of
14.132 + SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
14.133 | NONE => SOME prf1)
14.134 - | NONE => (case rew0 Ts prf of
14.135 - SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1))
14.136 + | NONE => (case rew0 Ts hs prf of
14.137 + SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
14.138 | NONE => NONE))
14.139
14.140 - and rew2 Ts skel (prf % SOME t) = (case prf of
14.141 + and rew2 Ts hs skel (prf % SOME t) = (case prf of
14.142 Abst (_, _, body) =>
14.143 let val prf' = prf_subst_bounds [t] body
14.144 - in SOME (the_default prf' (rew2 Ts no_skel prf')) end
14.145 - | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of
14.146 + in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
14.147 + | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
14.148 SOME prf' => SOME (prf' % SOME t)
14.149 | NONE => NONE))
14.150 - | rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
14.151 - (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf)
14.152 - | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
14.153 + | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
14.154 + (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
14.155 + | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of
14.156 AbsP (_, _, body) =>
14.157 let val prf' = prf_subst_pbounds [prf2] body
14.158 - in SOME (the_default prf' (rew2 Ts no_skel prf')) end
14.159 + in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
14.160 | _ =>
14.161 let val (skel1, skel2) = (case skel of
14.162 skel1 %% skel2 => (skel1, skel2)
14.163 | _ => (no_skel, no_skel))
14.164 - in case rew1 Ts skel1 prf1 of
14.165 - SOME prf1' => (case rew1 Ts skel2 prf2 of
14.166 + in case rew1 Ts hs skel1 prf1 of
14.167 + SOME prf1' => (case rew1 Ts hs skel2 prf2 of
14.168 SOME prf2' => SOME (prf1' %% prf2')
14.169 | NONE => SOME (prf1' %% prf2))
14.170 - | NONE => (case rew1 Ts skel2 prf2 of
14.171 + | NONE => (case rew1 Ts hs skel2 prf2 of
14.172 SOME prf2' => SOME (prf1 %% prf2')
14.173 | NONE => NONE)
14.174 end)
14.175 - | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
14.176 + | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs
14.177 (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
14.178 SOME prf' => SOME (Abst (s, T, prf'))
14.179 | NONE => NONE)
14.180 - | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts
14.181 + | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs)
14.182 (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
14.183 SOME prf' => SOME (AbsP (s, t, prf'))
14.184 | NONE => NONE)
14.185 - | rew2 _ _ _ = NONE;
14.186 + | rew2 _ _ _ _ = NONE;
14.187
14.188 - in the_default prf (rew1 [] no_skel prf) end;
14.189 + in the_default prf (rew1 [] [] no_skel prf) end;
14.190
14.191 fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
14.192 Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
14.193 @@ -1332,7 +1343,7 @@
14.194 (
14.195 type T =
14.196 (stamp * (proof * proof)) list *
14.197 - (stamp * (typ list -> proof -> (proof * proof) option)) list;
14.198 + (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list;
14.199
14.200 val empty = ([], []);
14.201 val extend = I;
14.202 @@ -1373,7 +1384,7 @@
14.203 | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
14.204 | fill _ = NONE;
14.205 val (rules, procs) = get_data thy;
14.206 - val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
14.207 + val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
14.208 in PBody {oracles = oracles, thms = thms, proof = proof} end;
14.209
14.210 fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
14.211 @@ -1421,12 +1432,13 @@
14.212 val (postproc, ofclasses, prop1, args1) =
14.213 if do_unconstrain then
14.214 let
14.215 - val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
14.216 + val ((atyp_map, constraints, outer_constraints), prop1) =
14.217 + Logic.unconstrainT shyps prop;
14.218 val postproc = unconstrainT_body thy (atyp_map, constraints);
14.219 val args1 =
14.220 (map o Option.map o Term.map_types o Term.map_atyps)
14.221 (Type.strip_sorts o atyp_map) args;
14.222 - in (postproc, map (OfClass o fst) constraints, prop1, args1) end
14.223 + in (postproc, map OfClass outer_constraints, prop1, args1) end
14.224 else (I, [], prop, args);
14.225 val argsP = ofclasses @ map Hyp hyps;
14.226
14.227 @@ -1447,7 +1459,7 @@
14.228 val head = PThm (i, ((name, prop1, NONE), body'));
14.229 in ((i, (name, prop1, body')), head, args, argsP, args1) end;
14.230
14.231 -val unconstrain_thm_proofs = Unsynchronized.ref false;
14.232 +val unconstrain_thm_proofs = Unsynchronized.ref true;
14.233
14.234 fun thm_proof thy name shyps hyps concl promises body =
14.235 let val (pthm, head, args, argsP, _) =
15.1 --- a/src/Pure/type_infer.ML Tue Jun 01 11:18:51 2010 +0200
15.2 +++ b/src/Pure/type_infer.ML Tue Jun 01 11:30:57 2010 +0200
15.3 @@ -295,11 +295,11 @@
15.4 | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
15.5 | occurs_check _ _ _ = ();
15.6
15.7 - fun assign i (T as Param (i', _)) S (tye_idx as (tye, idx)) =
15.8 + fun assign i (T as Param (i', _)) S tye_idx =
15.9 if i = i' then tye_idx
15.10 - else meet (T, S) (Inttab.update_new (i, T) tye, idx)
15.11 - | assign i T S (tye, idx) =
15.12 - (occurs_check tye i T; meet (T, S) (Inttab.update_new (i, T) tye, idx));
15.13 + else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
15.14 + | assign i T S (tye_idx as (tye, _)) =
15.15 + (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
15.16
15.17
15.18 (* unification *)