proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
authorwenzelm
Tue May 04 14:38:59 2010 +0200 (2010-05-04 ago)
changeset 366212fd4e2c76636
parent 36620 e6bb250402b5
child 36645 30bd207ec222
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;
src/Pure/proofterm.ML
src/Pure/thm.ML
src/Pure/type.ML
     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)