proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
* present type variables are only compared wrt. first component (the atomic type), not the duplicated sort;
* extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem);
* deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;
1.1 --- a/src/Pure/proofterm.ML Tue May 04 12:30:15 2010 +0200
1.2 +++ b/src/Pure/proofterm.ML Tue May 04 14:38:59 2010 +0200
1.3 @@ -108,6 +108,8 @@
1.4 val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
1.5 val equal_intr: term -> term -> proof -> proof -> proof
1.6 val equal_elim: term -> term -> proof -> proof -> proof
1.7 + val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
1.8 + sort list -> proof -> proof
1.9 val axm_proof: string -> term -> proof
1.10 val oracle_proof: string -> term -> oracle * proof
1.11 val promise_proof: theory -> serial -> term -> proof
1.12 @@ -884,6 +886,22 @@
1.13 equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
1.14
1.15
1.16 +(**** sort hypotheses ****)
1.17 +
1.18 +fun strip_shyps_proof algebra present witnessed extra_sorts prf =
1.19 + let
1.20 + fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
1.21 + val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
1.22 + val replacements = present @ extra @ witnessed;
1.23 + fun replace T =
1.24 + if exists (fn (T', _) => T' = T) present then raise Same.SAME
1.25 + else
1.26 + (case get_first (get (Type.sort_of_atyp T)) replacements of
1.27 + SOME T' => T'
1.28 + | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
1.29 + in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
1.30 +
1.31 +
1.32 (***** axioms and theorems *****)
1.33
1.34 val proofs = Unsynchronized.ref 2;
2.1 --- a/src/Pure/thm.ML Tue May 04 12:30:15 2010 +0200
2.2 +++ b/src/Pure/thm.ML Tue May 04 14:38:59 2010 +0200
2.3 @@ -512,6 +512,9 @@
2.4 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
2.5 fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
2.6
2.7 +fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
2.8 + make_deriv promises oracles thms (f proof);
2.9 +
2.10
2.11 (* fulfilled proofs *)
2.12
2.13 @@ -1204,14 +1207,17 @@
2.14 | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
2.15 let
2.16 val thy = Theory.deref thy_ref;
2.17 - val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
2.18 + val algebra = Sign.classes_of thy;
2.19 +
2.20 + val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
2.21 val extra = fold (Sorts.remove_sort o #2) present shyps;
2.22 val witnessed = Sign.witness_sorts thy present extra;
2.23 val extra' = fold (Sorts.remove_sort o #2) witnessed extra
2.24 - |> Sorts.minimal_sorts (Sign.classes_of thy);
2.25 + |> Sorts.minimal_sorts algebra;
2.26 val shyps' = fold (Sorts.insert_sort o #2) present extra';
2.27 in
2.28 - Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
2.29 + Thm (deriv_rule_unconditional (Pt.strip_shyps_proof algebra present witnessed extra') der,
2.30 + {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
2.31 shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
2.32 end;
2.33
3.1 --- a/src/Pure/type.ML Tue May 04 12:30:15 2010 +0200
3.2 +++ b/src/Pure/type.ML Tue May 04 14:38:59 2010 +0200
3.3 @@ -53,6 +53,7 @@
3.4 val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
3.5
3.6 (*special treatment of type vars*)
3.7 + val sort_of_atyp: typ -> sort
3.8 val strip_sorts: typ -> typ
3.9 val no_tvars: typ -> typ
3.10 val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
3.11 @@ -271,6 +272,13 @@
3.12
3.13 (** special treatment of type vars **)
3.14
3.15 +(* sort_of_atyp *)
3.16 +
3.17 +fun sort_of_atyp (TFree (_, S)) = S
3.18 + | sort_of_atyp (TVar (_, S)) = S
3.19 + | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []);
3.20 +
3.21 +
3.22 (* strip_sorts *)
3.23
3.24 fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)