Adapted to new format of proof terms containing explicit proofs of class membership.
--- a/src/HOL/Extraction.thy Tue Jun 01 11:04:49 2010 +0200
+++ b/src/HOL/Extraction.thy Tue Jun 01 11:13:09 2010 +0200
@@ -18,7 +18,8 @@
Proofterm.rewrite_proof_notypes
([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
Proofterm.rewrite_proof thy
- (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
+ (RewriteHOLProof.rews,
+ ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
ProofRewriteRules.elim_vars (curry Const @{const_name default}))
*}
@@ -199,223 +200,212 @@
theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
(\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
-setup {*
- Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"})
-*}
-
realizers
impI (P, Q): "\<lambda>pq. pq"
- "\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
+ "\<Lambda> (c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
impI (P): "Null"
- "\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
+ "\<Lambda> (c: _) P Q (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
- impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _"
+ impI (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. impI \<cdot> _ \<cdot> _"
impI: "Null" "impI"
mp (P, Q): "\<lambda>pq. pq"
- "\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) (d: _) P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
mp (P): "Null"
- "\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
- mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _"
+ mp (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. mp \<cdot> _ \<cdot> _"
mp: "Null" "mp"
- allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _"
+ allI (P): "\<lambda>p. p" "\<Lambda> (c: _) P (d: _) p. allI \<cdot> _ \<bullet> d"
allI: "Null" "allI"
- spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x"
+ spec (P): "\<lambda>x p. p x" "\<Lambda> (c: _) P x (d: _) p. spec \<cdot> _ \<cdot> x \<bullet> d"
spec: "Null" "spec"
- exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x"
+ 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"
- exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h"
+ exI: "\<lambda>x. x" "\<Lambda> P x (c: _) (h: _). h"
exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y"
- "\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h"
+ "\<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"
exE (P): "Null"
- "\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q (d: _) p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d"
exE (Q): "\<lambda>x pq. pq x"
- "\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
+ "\<Lambda> (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1"
exE: "Null"
- "\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
+ "\<Lambda> P Q (c: _) x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1"
conjI (P, Q): "Pair"
- "\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h"
+ "\<Lambda> (c: _) (d: _) P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> c \<bullet> d \<bullet> h"
conjI (P): "\<lambda>p. p"
- "\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjI \<cdot> _ \<cdot> _"
conjI (Q): "\<lambda>q. q"
- "\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
+ "\<Lambda> (c: _) P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h"
conjI: "Null" "conjI"
conjunct1 (P, Q): "fst"
- "\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) (d: _) P Q pq. conjunct1 \<cdot> _ \<cdot> _"
conjunct1 (P): "\<lambda>p. p"
- "\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjunct1 \<cdot> _ \<cdot> _"
conjunct1 (Q): "Null"
- "\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q q. conjunct1 \<cdot> _ \<cdot> _"
conjunct1: "Null" "conjunct1"
conjunct2 (P, Q): "snd"
- "\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) (d: _) P Q pq. conjunct2 \<cdot> _ \<cdot> _"
conjunct2 (P): "Null"
- "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
conjunct2 (Q): "\<lambda>p. p"
- "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _"
conjunct2: "Null" "conjunct2"
disjI1 (P, Q): "Inl"
- "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)"
+ "\<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)"
disjI1 (P): "Some"
- "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)"
+ "\<Lambda> (c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
disjI1 (Q): "None"
- "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
+ "\<Lambda> (c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
disjI1: "Left"
- "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)"
+ "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
disjI2 (P, Q): "Inr"
- "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
+ "\<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)"
disjI2 (P): "None"
- "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)"
+ "\<Lambda> (c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
disjI2 (Q): "Some"
- "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)"
+ "\<Lambda> (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
disjI2: "Right"
- "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)"
+ "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
disjE (P, Q, R): "\<lambda>pq pr qr.
(case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
- disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
+ "\<Lambda> (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr.
+ disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> e \<bullet> h1 \<bullet> h2"
disjE (Q, R): "\<lambda>pq pr qr.
(case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
- disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
+ "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr.
+ disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h2"
disjE (P, R): "\<lambda>pq pr qr.
(case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _).
- disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2"
+ "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _).
+ disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h3 \<bullet> h2"
disjE (R): "\<lambda>pq pr qr.
(case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)"
- "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr.
- disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2"
+ "\<Lambda> (c: _) P Q R pq (h1: _) pr (h2: _) qr.
+ disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> h1 \<bullet> h2"
disjE (P, Q): "Null"
- "\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
+ "\<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"
disjE (Q): "Null"
- "\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool"
disjE (P): "Null"
- "\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _).
- disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2"
+ "\<Lambda> (c: _) P Q R pq (h1: _) (h2: _) (h3: _).
+ disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool \<bullet> h1 \<bullet> h3 \<bullet> h2"
disjE: "Null"
- "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
+ "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> arity_type_bool"
FalseE (P): "default"
- "\<Lambda> P. FalseE \<cdot> _"
+ "\<Lambda> (c: _) P. FalseE \<cdot> _"
FalseE: "Null" "FalseE"
notI (P): "Null"
- "\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
+ "\<Lambda> (c: _) P (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))"
notI: "Null" "notI"
notE (P, R): "\<lambda>p. default"
- "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) (d: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
notE (P): "Null"
- "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
+ "\<Lambda> (c: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)"
notE (R): "default"
- "\<Lambda> P R. notE \<cdot> _ \<cdot> _"
+ "\<Lambda> (c: _) P R. notE \<cdot> _ \<cdot> _"
notE: "Null" "notE"
subst (P): "\<lambda>s t ps. ps"
- "\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h"
+ "\<Lambda> (c: _) s t P (d: _) (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> d \<bullet> h"
subst: "Null" "subst"
iffD1 (P, Q): "fst"
- "\<Lambda> Q P pq (h: _) p.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (d: _) (c: _) Q P pq (h: _) p.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> d \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD1 (P): "\<lambda>p. p"
- "\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
+ "\<Lambda> (c: _) Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)"
iffD1 (Q): "Null"
- "\<Lambda> Q P q1 (h: _) q2.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (c: _) Q P q1 (h: _) q2.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD1: "Null" "iffD1"
iffD2 (P, Q): "snd"
- "\<Lambda> P Q pq (h: _) q.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (c: _) (d: _) P Q pq (h: _) q.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> d \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD2 (P): "\<lambda>p. p"
- "\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
+ "\<Lambda> (c: _) P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)"
iffD2 (Q): "Null"
- "\<Lambda> P Q q1 (h: _) q2.
- mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
+ "\<Lambda> (c: _) P Q q1 (h: _) q2.
+ mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))"
iffD2: "Null" "iffD2"
iffI (P, Q): "Pair"
- "\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
+ "\<Lambda> (c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot>
(\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot>
(\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
+ (arity_type_fun \<bullet> c \<bullet> d) \<bullet>
+ (arity_type_fun \<bullet> d \<bullet> c) \<bullet>
+ (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
+ (allI \<cdot> _ \<bullet> d \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
iffI (P): "\<lambda>p. p"
- "\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
+ "\<Lambda> (c: _) P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
+ (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet>
(impI \<cdot> _ \<cdot> _ \<bullet> h2)"
iffI (Q): "\<lambda>q. q"
- "\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
+ "\<Lambda> (c: _) P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet>
(impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet>
- (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
+ (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))"
iffI: "Null" "iffI"
-(*
- classical: "Null"
- "\<Lambda> P. classical \<cdot> _"
-*)
-
-setup {*
- Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"})
-*}
-
end
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 11:04:49 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 11:13:09 2010 +0200
@@ -22,10 +22,6 @@
in map (fn ks => i::ks) is @ is end
else [[]];
-fun forall_intr_prf (t, prf) =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
-
fun prf_of thm =
Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
@@ -130,12 +126,12 @@
val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
- val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *)
- member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
+ val ivs1 = map Var (filter_out (fn (_, T) =>
+ @{type_name bool} = tname_of (body_type T)) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
val prf =
- List.foldr forall_intr_prf
+ Extraction.abs_corr_shyps thy' induct vs ivs2
(fold_rev (fn (f, p) => fn prf =>
(case head_of (strip_abs_body f) of
Free (s, T) =>
@@ -145,7 +141,7 @@
end
| _ => AbsP ("H", SOME p, prf)))
(rec_fns ~~ prems_of thm)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
+ (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
@@ -198,18 +194,21 @@
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
- val prf = forall_intr_prf (y, forall_intr_prf (P,
- fold_rev (fn (p, r) => fn prf =>
- forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
+ val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
+ (fold_rev (fn (p, r) => fn prf =>
+ Proofterm.forall_intr_proof' (Logic.varify_global r)
+ (AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
+ (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ val prf' = Extraction.abs_corr_shyps thy' exhaust []
+ (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
val r' = Logic.varify_global (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
in Extraction.add_realizers_i
[(exh_name, (["P"], r', prf)),
- (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
+ (exh_name, ([], Extraction.nullt, prf'))] thy'
end;
fun add_dt_realizers config names thy =
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 11:04:49 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 11:13:09 2010 +0200
@@ -21,18 +21,12 @@
[name] => name
| _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
-val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
-
fun prf_of thm =
let
val thy = Thm.theory_of_thm thm;
val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
-fun forall_intr_prf t prf =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
-
fun subsets [] = [[]]
| subsets (x::xs) =
let val ys = subsets xs
@@ -55,15 +49,19 @@
(subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
| strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
-fun relevant_vars prop = List.foldr (fn
- (Var ((a, i), T), vs) => (case strip_type T of
+fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
+ (case strip_type T of
(_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
- | _ => vs)
- | (_, vs) => vs) [] (OldTerm.term_vars prop);
+ | _ => vs)) (Term.add_vars prop []) [];
+
+val attach_typeS = map_types (map_atyps
+ (fn TFree (s, []) => TFree (s, HOLogic.typeS)
+ | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
+ | T => T));
fun dt_of_intrs thy vs nparms intrs =
let
- val iTs = OldTerm.term_tvars (prop_of (hd intrs));
+ val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (prop_of (hd intrs))));
val params = map dest_Var (take nparms ts);
@@ -84,7 +82,7 @@
fun gen_rvar vs (t as Var ((a, 0), T)) =
if body_type T <> HOLogic.boolT then t else
let
- val U = TVar (("'" ^ a, 0), HOLogic.typeS)
+ val U = TVar (("'" ^ a, 0), [])
val Ts = binder_types T;
val i = length Ts;
val xs = map (pair "x") Ts;
@@ -98,8 +96,9 @@
fun mk_realizes_eqn n vs nparms intrs =
let
- val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
- val iTs = OldTerm.term_tvars concl;
+ val intr = map_types Type.strip_sorts (prop_of (hd intrs));
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
+ val iTs = rev (Term.add_tvars intr []);
val Tvs = map TVar iTs;
val (h as Const (s, T), us) = strip_comb concl;
val params = List.take (us, nparms);
@@ -110,7 +109,7 @@
(Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
val rT = if n then Extraction.nullT
else Type (space_implode "_" (s ^ "T" :: vs),
- map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
+ map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
val S = list_comb (h, params @ xs);
val rvs = relevant_vars S;
@@ -121,7 +120,7 @@
let val T = (the o AList.lookup (op =) rvs) v
in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
Extraction.mk_typ (if n then Extraction.nullT
- else TVar (("'" ^ v, 0), HOLogic.typeS)))
+ else TVar (("'" ^ v, 0), [])))
end;
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
@@ -261,12 +260,12 @@
val rlzvs = rev (Term.add_vars (prop_of rrule) []);
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
- val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
- val rlz'' = fold_rev Logic.all vs2 rlz
+ val rlz' = fold_rev Logic.all rs (prop_of rrule)
in (name, (vs,
if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
- ProofRewriteRules.un_hhf_proof rlz' rlz''
- (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
+ Extraction.abs_corr_shyps thy rule vs vs2
+ (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
+ (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
end;
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
@@ -275,7 +274,7 @@
let
val qualifier = Long_Name.qualifier (name_of_thm induct);
val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
- val iTs = OldTerm.term_tvars (prop_of (hd intrs));
+ val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
val ar = length vs + length iTs;
val params = Inductive.params_of raw_induct;
val arities = Inductive.arities_of raw_induct;
@@ -297,8 +296,6 @@
val thy1' = thy1 |>
Theory.copy |>
Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
- fold (fn s => AxClass.axiomatize_arity
- (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
@@ -328,10 +325,10 @@
end
else (replicate (length rs) Extraction.nullt, (recs, dummies)))
rss (rec_thms, dummies);
- val rintrs = map (fn (intr, c) => Envir.eta_contract
+ val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
(Extraction.realizes_of thy2 vs
(if c = Extraction.nullt then c else list_comb (c, map Var (rev
- (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
+ (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
(maps snd rss ~~ flat constrss);
val (rlzpreds, rlzpreds') =
rintrs |> map (fn rintr =>
@@ -390,7 +387,9 @@
val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
(fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
- val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
+ val thm = Goal.prove_global thy []
+ (map attach_typeS prems) (attach_typeS concl)
+ (fn {prems, ...} => EVERY
[rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
@@ -408,10 +407,10 @@
in
Extraction.add_realizers_i
(map (fn (((ind, corr), rlz), r) =>
- mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
+ mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
realizers @ (case realizers of
[(((ind, corr), rlz), r)] =>
- [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
+ [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
ind, corr, rlz, r)]
| _ => [])) thy''
end;
@@ -445,7 +444,7 @@
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
[Bound (length prems)]));
val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
- val rlz' = strip_all (Logic.unvarify_global rlz);
+ val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
val rews = map mk_meta_eq case_thms;
val thm = Goal.prove_global thy []
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
@@ -488,7 +487,7 @@
val vss = sort (int_ord o pairself length)
(subsets (map fst (relevant_vars (concl_of (hd intrs)))))
in
- fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
+ fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
end
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
--- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 11:04:49 2010 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 11:13:09 2010 +0200
@@ -7,7 +7,7 @@
signature REWRITE_HOL_PROOF =
sig
val rews: (Proofterm.proof * Proofterm.proof) list
- val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
+ val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
end;
structure RewriteHOLProof : REWRITE_HOL_PROOF =
@@ -16,7 +16,7 @@
open Proofterm;
val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
- Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT)
+ Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
(** eliminate meta-equality rules **)
@@ -24,237 +24,258 @@
\ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \
\ (axm.reflexive % TYPE('T3) % x4) %% prf1)) == \
\ (iffD1 % A % B %% \
- \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
+ \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
"(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \
\ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \
\ (axm.reflexive % TYPE('T4) % x6) %% prf1))) == \
\ (iffD2 % A % B %% \
- \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
+ \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
- "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \
+ "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %% \
\ (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) == \
\ (cong % TYPE('T) % TYPE('U) % f % g % x % y %% \
- \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
-
- "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \
- \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \
- \ (HOL.trans % TYPE('T) % x % y % z %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
+ \ (OfClass type_class % TYPE('T)) %% prfU %% \
+ \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))",
- "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \
- \ (HOL.refl % TYPE('T) % x)",
+ "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% \
+ \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \
+ \ (HOL.trans % TYPE('T) % x % y % z %% prfT %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))",
- "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
+ "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) == \
+ \ (HOL.refl % TYPE('T) % x %% prfT)",
+
+ "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \
\ (axm.symmetric % TYPE('T) % x % y %% prf)) == \
- \ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
+ \ (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))",
- "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \
+ "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %% \
\ (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) == \
\ (ext % TYPE('T) % TYPE('U) % f % g %% \
- \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
+ \ (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %% \
+ \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% \
+ \ (OfClass type_class % TYPE('U)) %% (prf % x)))",
- "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
- \ (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
+ "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \
+ \ (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf",
- "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
+ "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \
\ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
\ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \
\ (iffD1 % A = C % B = D %% \
- \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ prfT %% arity_type_bool %% \
\ (cong % TYPE('T) % TYPE('T=>bool) % \
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
- \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
+ \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \
+ \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \
+ \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))",
- "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
+ "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \
\ (axm.symmetric % TYPE('T2) % x5 % x6 %% \
\ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
\ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \
\ (iffD2 % A = C % B = D %% \
- \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ prfT %% arity_type_bool %% \
\ (cong % TYPE('T) % TYPE('T=>bool) % \
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
- \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \
- \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
+ \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \
+ \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \
+ \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \
+ \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))",
(** rewriting on bool: insert proper congruence rules for logical connectives **)
(* All *)
- "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (allI % TYPE('a) % Q %% \
+ "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (allI % TYPE('a) % Q %% prfa %% \
\ (Lam x. \
\ iffD1 % P x % Q x %% (prf % x) %% \
- \ (spec % TYPE('a) % P % x %% prf')))",
+ \ (spec % TYPE('a) % P % x %% prfa %% prf')))",
- "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (allI % TYPE('a) % P %% \
+ "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (allI % TYPE('a) % P %% prfa %% \
\ (Lam x. \
\ iffD2 % P x % Q x %% (prf % x) %% \
- \ (spec % TYPE('a) % Q % x %% prf')))",
+ \ (spec % TYPE('a) % Q % x %% prfa %% prf')))",
(* Ex *)
- "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \
+ "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %% \
\ (Lam x H : P x. \
- \ exI % TYPE('a) % Q % x %% \
+ \ exI % TYPE('a) % Q % x %% prfa %% \
\ (iffD1 % P x % Q x %% (prf % x) %% H)))",
- "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
- \ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \
+ "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \
+ \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \
+ \ (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %% \
\ (Lam x H : Q x. \
- \ exI % TYPE('a) % P % x %% \
+ \ exI % TYPE('a) % P % x %% prfa %% \
\ (iffD2 % P x % Q x %% (prf % x) %% H)))",
(* & *)
- "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
- \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
+ "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (conjI % B % D %% \
\ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \
\ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
- "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \
- \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \
+ "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (conjI % A % C %% \
\ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \
\ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
- "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op & A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(* | *)
- "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
- \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (disjE % A % C % B | D %% prf3 %% \
\ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \
\ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
- "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \
- \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (disjE % B % D % A | C %% prf3 %% \
\ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \
\ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
- "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op | A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(* --> *)
- "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
- \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \
\ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
- "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \
- \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \
+ "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \
+ \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \
+ \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \
\ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \
\ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
- "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op --> A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(* ~ *)
- "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
- \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
+ "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \
\ (notI % Q %% (Lam H: Q. \
\ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
- "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \
- \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \
+ "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \
\ (notI % P %% (Lam H: P. \
\ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
(* = *)
"(iffD1 % B % D %% \
- \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
+ \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD1 % C % D %% prf2 %% \
\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
"(iffD2 % B % D %% \
- \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
+ \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD1 % A % B %% prf1 %% \
\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
"(iffD1 % A % C %% \
- \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \
+ \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)== \
\ (iffD2 % C % D %% prf2 %% \
\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
"(iffD2 % A % C %% \
- \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
- \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
- \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
+ \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \
+ \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD2 % A % B %% prf1 %% \
\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
- "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
- \ (HOL.refl % TYPE(bool=>bool) % op = A)) == \
- \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
+ "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \
+ \ (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) == \
+ \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \
- \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \
- \ (HOL.refl % TYPE(bool) % A)))",
+ \ prfb %% prfbb %% \
+ \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %% \
+ \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \
+ \ (HOL.refl % TYPE(bool) % A %% prfb)))",
(** transitivity, reflexivity, and symmetry **)
- "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
+ "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \
\ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
- "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \
+ "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \
\ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
- "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
+ "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
- "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
+ "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
- "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
+ "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)",
- "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
+ "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)",
(** normalization of HOL proofs **)
@@ -262,13 +283,13 @@
"(impI % A % B %% (mp % A % B %% prf)) == prf",
- "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
+ "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x",
- "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
+ "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf",
- "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
+ "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)",
- "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
+ "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf",
"(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
@@ -286,26 +307,26 @@
(** Replace congruence rules by substitution rules **)
fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
- prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
- | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
+ prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
+ | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
-val subst_prf = fst (strip_combt (Thm.proof_of subst));
-val sym_prf = fst (strip_combt (Thm.proof_of sym));
+val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst))));
+val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym))));
fun make_subst Ts prf xs (_, []) = prf
- | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
+ | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
let val T = fastype_of1 (Ts, x)
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
else change_type (SOME [T]) subst_prf %> x %> y %>
Abs ("z", T, list_comb (incr_boundvars 1 f,
map (incr_boundvars 1) xs @ Bound 0 ::
- map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
+ map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
make_subst Ts prf (xs @ [x]) (f, ps)
end;
-fun make_sym Ts ((x, y), prf) =
- ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
+fun make_sym Ts ((x, y), (prf, clprf)) =
+ ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
@@ -322,6 +343,6 @@
apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
-fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
+fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
end;
--- a/src/Pure/Proof/extraction.ML Tue Jun 01 11:04:49 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Jun 01 11:13:09 2010 +0200
@@ -24,6 +24,7 @@
val mk_typ : typ -> term
val etype_of : theory -> string list -> typ list -> term -> typ
val realizes_of: theory -> string list -> term -> term -> term
+ val abs_corr_shyps: theory -> thm -> string list -> term list -> Proofterm.proof -> Proofterm.proof
end;
structure Extraction : EXTRACTION =
@@ -126,11 +127,9 @@
fun frees_of t = map Free (rev (Term.add_frees t []));
fun vfs_of t = vars_of t @ frees_of t;
-fun forall_intr_prf (t, prf) =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, prf_abstract_over t prf) end;
+val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
-val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
+val mkabsp = fold_rev (fn t => fn prf => AbsP ("H", SOME t, prf));
fun strip_abs 0 t = t
| strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
@@ -161,6 +160,14 @@
| _ => error "get_var_type: not a variable"
end;
+fun read_term thy T s =
+ let
+ val ctxt = ProofContext.init_global thy
+ |> Proof_Syntax.strip_sorts_consttypes
+ |> ProofContext.set_defsort [];
+ val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
+ in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
+
(**** theory data ****)
@@ -175,7 +182,7 @@
(term -> typ -> term -> typ -> term) option)) list,
realizers : (string list * (term * proof)) list Symtab.table,
defs : thm list,
- expand : (string * term) list,
+ expand : string list,
prep : (theory -> proof -> proof) option}
val empty =
@@ -198,14 +205,14 @@
types = AList.merge (op =) (K true) (types1, types2),
realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
- expand = Library.merge (op =) (expand1, expand2), (* FIXME proper aconv !?! *)
+ expand = Library.merge (op =) (expand1, expand2),
prep = (case prep1 of NONE => prep2 | _ => prep1)};
);
fun read_condeq thy =
let val thy' = add_syntax thy
in fn s =>
- let val t = Logic.varify_global (Syntax.read_prop_global thy' s)
+ let val t = Logic.varify_global (read_term thy' propT s)
in
(map Logic.dest_equals (Logic.strip_imp_prems t),
Logic.dest_equals (Logic.strip_imp_concl t))
@@ -274,7 +281,7 @@
fun err () = error ("Unable to determine type of extracted program for\n" ^
Syntax.string_of_term_global thy t)
in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
- [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
+ [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts),
Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ())
| _ => err ()
@@ -300,25 +307,30 @@
val rtypes = map fst types;
val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
val thy' = add_syntax thy;
- val rd = Proof_Syntax.read_proof thy' false;
+ val rd = Proof_Syntax.read_proof thy' true false;
in fn (thm, (vs, s1, s2)) =>
let
val name = Thm.derivation_name thm;
val _ = name <> "" orelse error "add_realizers: unnamed theorem";
- val prop = Pattern.rewrite_term thy'
- (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
+ val prop = Thm.unconstrainT thm |> prop_of |>
+ Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [];
val vars = vars_of prop;
val vars' = filter_out (fn v =>
member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
+ val shyps = maps (fn Var ((x, i), _) =>
+ if member (op =) vs x then Logic.mk_of_sort
+ (TVar (("'" ^ x, i), []), Sign.defaultS thy')
+ else []) vars;
val T = etype_of thy' vs [] prop;
val (T', thw) = Type.legacy_freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
- val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
+ val t = map_types thw (read_term thy' T' s1);
val r' = freeze_thaw (condrew thy' eqns
- (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
+ (procs @ [typeof_proc [] vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
(if T = nullT then t else list_comb (t, vars')) $ prop);
- val r = fold_rev Logic.all (map (get_var_type r') vars) r';
+ val r = Logic.list_implies (shyps,
+ fold_rev Logic.all (map (get_var_type r') vars) r');
val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
in (name, (vs, (t, prf))) end
end;
@@ -337,10 +349,34 @@
val prop' = Pattern.rewrite_term thy'
(map (Logic.dest_equals o prop_of) defs) [] prop;
in freeze_thaw (condrew thy' eqns
- (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
+ (procs @ [typeof_proc [] vs, rlz_proc]))
(Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop')
end;
+fun abs_corr_shyps thy thm vs xs prf =
+ let
+ val S = Sign.defaultS thy;
+ val ((atyp_map, constraints, _), prop') =
+ Logic.unconstrainT (#shyps (rep_thm thm)) (prop_of thm);
+ val atyps = fold_types (fold_atyps (insert (op =))) (prop_of thm) [];
+ val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
+ SOME (TVar (("'" ^ v, i), [])) else NONE)
+ (rev (Term.add_vars prop' []));
+ val cs = maps (fn T => map (pair T) S) Ts;
+ val constraints' = map Logic.mk_of_class cs;
+ val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints);
+ fun typ_map T = Type.strip_sorts
+ (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
+ fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
+ val xs' = map (map_types typ_map) xs
+ in
+ prf |>
+ Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
+ fold_rev implies_intr_proof' (map snd constraints) |>
+ fold_rev forall_intr_proof' xs' |>
+ fold_rev implies_intr_proof' constraints'
+ end;
+
(** expanding theorems / definitions **)
fun add_expand_thm is_def thm thy =
@@ -354,15 +390,15 @@
thy |> ExtractionData.put
(if is_def then
{realizes_eqns = realizes_eqns,
- typeof_eqns = add_rule ([],
- Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
+ typeof_eqns = add_rule ([], Logic.dest_equals (map_types
+ Type.strip_sorts (prop_of (Drule.abs_def thm)))) typeof_eqns,
types = types,
realizers = realizers, defs = insert Thm.eq_thm thm defs,
expand = expand, prep = prep}
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
realizers = realizers, defs = defs,
- expand = insert (op =) (name, prop_of thm) expand, prep = prep})
+ expand = insert (op =) name expand, prep = prep})
end;
fun extraction_expand is_def =
@@ -443,9 +479,9 @@
ExtractionData.get thy;
val procs = maps (rev o fst o snd) types;
val rtypes = map fst types;
- val typroc = typeof_proc (Sign.defaultS thy');
+ val typroc = typeof_proc [];
val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
- Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
+ Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
fun find_inst prop Ts ts vs =
@@ -464,6 +500,13 @@
in fold_rev add_args (take n vars ~~ take n ts) ([], []) end;
+ fun mk_shyps tye = maps (fn (ixn, _) =>
+ Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
+
+ fun mk_sprfs cs tye = maps (fn (_, T) =>
+ ProofRewriteRules.mk_of_sort_proof thy (map SOME cs)
+ (T, Sign.defaultS thy)) tye;
+
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
@@ -474,22 +517,22 @@
fun realizes_null vs prop = app_rlz_rews [] vs
(Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
- fun corr d defs vs ts Ts hs (PBound i) _ _ = (defs, PBound i)
+ fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i)
- | corr d defs vs ts Ts hs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
+ | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
- (dummyt :: hs) prf (incr_pboundvars 1 0 prf')
+ (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
(case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
in (defs', Abst (s, SOME T, corr_prf)) end
- | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
+ | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
let
val T = etype_of thy' vs Ts prop;
val u = if T = nullT then
(case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
- (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
+ (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
val rlz = Const ("realizes", T --> propT --> propT)
in (defs',
if T = nullT then AbsP ("R",
@@ -500,10 +543,10 @@
(rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
end
- | corr d defs vs ts Ts hs (prf % SOME t) (prf' % _) t' =
+ | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' =
let
val (Us, T) = strip_type (fastype_of1 (Ts, t));
- val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
+ val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf'
(if member (op =) rtypes (tname_of T) then t'
else (case t' of SOME (u $ _) => SOME u | _ => NONE));
val u = if not (member (op =) rtypes (tname_of T)) then t else
@@ -519,7 +562,7 @@
in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end
in (defs', corr_prf % SOME u) end
- | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t =
+ | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
let
val prop = Reconstruct.prop_of' hs prf2';
val T = etype_of thy' vs Ts prop;
@@ -529,17 +572,19 @@
| _ =>
let val (defs1, u) = extr d defs vs [] Ts hs prf2'
in (defs1, NONE, SOME u) end)
- val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs prf1 prf1' f;
- val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs prf2 prf2' u;
+ val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f;
+ val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u;
in
if T = nullT then (defs3, corr_prf1 %% corr_prf2) else
(defs3, corr_prf1 % u %% corr_prf2)
end
- | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
+ | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
let
val prf = join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
+ val shyps = mk_shyps tye;
+ val sprfs = mk_sprfs cs tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
val T = etype_of thy' vs' [] prop;
val defs' = if T = nullT then defs
@@ -555,28 +600,31 @@
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
- val (defs'', corr_prf) =
- corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
+ val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] []
+ (rev shyps) prf' prf' NONE;
+ val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Reconstruct.prop_of corr_prf;
- val corr_prf' = List.foldr forall_intr_prf
- (proof_combt
+ val corr_prf' =
+ proof_combP (proof_combt
(PThm (serial (),
((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
- Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
- (map (get_var_type corr_prop) (vfs_of prop))
+ Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
+ map PBound (length shyps - 1 downto 0)) |>
+ fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
+ mkabsp shyps
in
((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
- prf_subst_TVars tye' corr_prf')
+ proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
end
- | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf'))
+ | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
| SOME rs => (case find vs' rs of
- SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
+ SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
| NONE => error ("corr: no realizer for instance of theorem " ^
quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts))))))
end
- | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
+ | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
let
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
@@ -584,13 +632,14 @@
if etype_of thy' vs' [] prop = nullT andalso
realizes_null vs' prop aconv prop then (defs, prf0)
else case find vs' (Symtab.lookup_list realizers s) of
- SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
+ SOME (_, prf) => (defs,
+ proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
| NONE => error ("corr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Reconstruct.prop_of (proof_combt (prf0, ts)))))
end
- | corr d defs vs ts Ts hs _ _ _ = error "corr: bad proof"
+ | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i)
@@ -630,6 +679,7 @@
let
val prf = join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
+ val shyps = mk_shyps tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
case Symtab.lookup realizers s of
@@ -641,18 +691,18 @@
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
- val (defs'', corr_prf) =
- corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
+ val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] []
+ (rev shyps) prf' prf' (SOME t);
val nt = Envir.beta_norm t;
val args = filter_out (fn v => member (op =) rtypes
(tname_of (body_type (fastype_of v)))) (vfs_of prop);
val args' = filter (fn v => Logic.occs (v, nt)) args;
- val t' = mkabs nt args';
+ val t' = mkabs args' nt;
val T = fastype_of t';
val cname = extr_name s vs';
val c = Const (cname, T);
- val u = mkabs (list_comb (c, args')) args;
+ val u = mkabs args (list_comb (c, args'));
val eqn = Logic.mk_equals (c, t');
val rlz =
Const ("realizes", fastype_of nt --> propT --> propT);
@@ -661,20 +711,22 @@
val f = app_rlz_rews [] vs'
(Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
- val corr_prf' =
- chtype [] equal_elim_axm %> lhs %> rhs %%
+ val corr_prf' = mkabsp shyps
+ (chtype [] equal_elim_axm %> lhs %> rhs %%
(chtype [propT] symmetric_axm %> rhs %> lhs %%
(chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
(chtype [T --> propT] reflexive_axm %> f) %%
PAxm (cname ^ "_def", eqn,
- SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
+ SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Reconstruct.prop_of corr_prf';
- val corr_prf'' = List.foldr forall_intr_prf
- (proof_combt
+ val corr_prf'' =
+ proof_combP (proof_combt
(PThm (serial (),
((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
- Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
- (map (get_var_type corr_prop) (vfs_of prop));
+ Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
+ map PBound (length shyps - 1 downto 0)) |>
+ fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
+ mkabsp shyps
in
((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
subst_TVars tye' u)
@@ -731,7 +783,7 @@
in
thy'
|> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
- Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
+ Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
(ProofChecker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
--- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 11:04:49 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 11:13:09 2010 +0200
@@ -6,14 +6,17 @@
signature PROOF_REWRITE_RULES =
sig
- val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
+ val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
val rprocs : bool ->
- (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
+ (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
+ val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+ val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
+ (Proofterm.proof * Proofterm.proof) option
end;
structure ProofRewriteRules : PROOF_REWRITE_RULES =
@@ -21,7 +24,7 @@
open Proofterm;
-fun rew b _ =
+fun rew b _ _ =
let
fun ?? x = if b then SOME x else NONE;
fun ax (prf as PAxm (s, prop, _)) Ts =
@@ -219,31 +222,36 @@
fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
fun insert_refl defs Ts (prf1 %% prf2) =
- insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
+ let val (prf1', b) = insert_refl defs Ts prf1
+ in
+ if b then (prf1', true)
+ else (prf1' %% fst (insert_refl defs Ts prf2), false)
+ end
| insert_refl defs Ts (Abst (s, SOME T, prf)) =
- Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
+ (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
| insert_refl defs Ts (AbsP (s, t, prf)) =
- AbsP (s, t, insert_refl defs Ts prf)
+ (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
| insert_refl defs Ts prf = (case strip_combt prf of
(PThm (_, ((s, prop, SOME Ts), _)), ts) =>
if member (op =) defs s then
let
val vs = vars_of prop;
val tvars = Term.add_tvars prop [] |> rev;
- val (_, rhs) = Logic.dest_equals prop;
+ val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
(fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
map the ts);
in
- change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
+ (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true)
end
- else prf
- | (_, []) => prf
- | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
+ else (prf, false)
+ | (_, []) => (prf, false)
+ | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
fun elim_defs thy r defs prf =
let
- val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
+ val defs' = map (Logic.dest_equals o
+ map_types Type.strip_sorts o prop_of o Drule.abs_def) defs;
val defnames = map Thm.derivation_name defs;
val f = if not r then I else
let
@@ -258,7 +266,7 @@
in Reconstruct.expand_proof thy thms end;
in
rewrite_terms (Pattern.rewrite_term thy defs' [])
- (insert_refl defnames [] (f prf))
+ (fst (insert_refl defnames [] (f prf)))
end;
@@ -327,4 +335,35 @@
mk_prf Q
end;
+
+(**** expand OfClass proofs ****)
+
+fun mk_of_sort_proof thy hs (T, S) =
+ let
+ val hs' = map
+ (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
+ | NONE => NONE) hs;
+ val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
+ fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
+ val subst = map_atyps
+ (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
+ | T as TFree (s, _) => TFree (s, get_sort T));
+ fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
+ ~1 => error "expand_of_class: missing class hypothesis"
+ | i => PBound i;
+ fun reconstruct prf prop = prf |>
+ Reconstruct.reconstruct_proof thy prop |>
+ Reconstruct.expand_proof thy [("", NONE)] |>
+ Same.commit (map_proof_same Same.same Same.same hyp)
+ in
+ map2 reconstruct
+ (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
+ (Logic.mk_of_sort (T, S))
+ end;
+
+fun expand_of_class thy Ts hs (OfClass (T, c)) =
+ mk_of_sort_proof thy hs (T, [c]) |>
+ hd |> rpair no_skel |> SOME
+ | expand_of_class thy Ts hs _ = NONE;
+
end;