just one version of Thm.unconstrainT, which affects all variables;
authorwenzelm
Sun May 09 19:15:21 2010 +0200 (2010-05-09)
changeset 3676846be86127972
parent 36767 d0095729e1f1
child 36769 b6b88bf695b3
just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;
src/HOL/HOL.thy
src/Pure/axclass.ML
src/Pure/logic.ML
src/Pure/thm.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/HOL.thy	Sun May 09 18:09:30 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun May 09 19:15:21 2010 +0200
     1.3 @@ -1869,7 +1869,7 @@
     1.4  proof
     1.5    assume "PROP ?ofclass"
     1.6    show "PROP ?eq"
     1.7 -    by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *}) 
     1.8 +    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
     1.9        (fact `PROP ?ofclass`)
    1.10  next
    1.11    assume "PROP ?eq"
     2.1 --- a/src/Pure/axclass.ML	Sun May 09 18:09:30 2010 +0200
     2.2 +++ b/src/Pure/axclass.ML	Sun May 09 19:15:21 2010 +0200
     2.3 @@ -423,7 +423,7 @@
     2.4      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
     2.5      val th' = th
     2.6        |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
     2.7 -      |> Thm.unconstrain_allTs;
     2.8 +      |> Thm.unconstrainT;
     2.9      val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
    2.10    in
    2.11      thy
    2.12 @@ -449,7 +449,7 @@
    2.13        |> (map o apsnd o map_atyps) (K T);
    2.14      val th' = th
    2.15        |> Drule.instantiate' std_vars []
    2.16 -      |> Thm.unconstrain_allTs;
    2.17 +      |> Thm.unconstrainT;
    2.18      val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
    2.19    in
    2.20      thy
     3.1 --- a/src/Pure/logic.ML	Sun May 09 18:09:30 2010 +0200
     3.2 +++ b/src/Pure/logic.ML	Sun May 09 19:15:21 2010 +0200
     3.3 @@ -46,7 +46,7 @@
     3.4    val name_arity: string * sort list * class -> string
     3.5    val mk_arities: arity -> term list
     3.6    val dest_arity: term -> string * sort list * class
     3.7 -  val unconstrain_allTs: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
     3.8 +  val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term
     3.9    val protectC: term
    3.10    val protect: term -> term
    3.11    val unprotect: term -> term
    3.12 @@ -272,7 +272,7 @@
    3.13  
    3.14  (* internalized sort constraints *)
    3.15  
    3.16 -fun unconstrain_allTs shyps prop =
    3.17 +fun unconstrainT shyps prop =
    3.18    let
    3.19      val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
    3.20      val extra = fold (Sorts.remove_sort o #2) present shyps;
     4.1 --- a/src/Pure/thm.ML	Sun May 09 18:09:30 2010 +0200
     4.2 +++ b/src/Pure/thm.ML	Sun May 09 19:15:21 2010 +0200
     4.3 @@ -138,8 +138,7 @@
     4.4    val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
     4.5    val of_class: ctyp * class -> thm
     4.6    val strip_shyps: thm -> thm
     4.7 -  val unconstrainT: ctyp -> thm -> thm
     4.8 -  val unconstrain_allTs: thm -> thm
     4.9 +  val unconstrainT: thm -> thm
    4.10    val legacy_freezeT: thm -> thm
    4.11    val assumption: int -> thm -> thm Seq.seq
    4.12    val eq_assumption: int -> thm -> thm
    4.13 @@ -1222,7 +1221,7 @@
    4.14        end;
    4.15  
    4.16  (*Internalize sort constraints of type variable*)
    4.17 -fun unconstrainT
    4.18 +fun unconstrain_TVar
    4.19      (Ctyp {thy_ref = thy_ref1, T, ...})
    4.20      (th as Thm (_, {thy_ref = thy_ref2, maxidx, shyps, hyps, tpairs, prop, ...})) =
    4.21    let
    4.22 @@ -1242,8 +1241,8 @@
    4.23        prop = Logic.list_implies (constraints, unconstrain prop)})
    4.24    end;
    4.25  
    4.26 -fun unconstrain_allTs th =
    4.27 -  fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar)
    4.28 +fun unconstrainT th =
    4.29 +  fold (unconstrain_TVar o ctyp_of (theory_of_thm th) o TVar)
    4.30      (fold_terms Term.add_tvars th []) th;
    4.31  
    4.32  
     5.1 --- a/src/Tools/nbe.ML	Sun May 09 18:09:30 2010 +0200
     5.2 +++ b/src/Tools/nbe.ML	Sun May 09 19:15:21 2010 +0200
     5.3 @@ -108,7 +108,9 @@
     5.4      |> Drule.cterm_rule Thm.legacy_freezeT
     5.5      |> conv
     5.6      |> Thm.varifyT_global
     5.7 -    |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
     5.8 +(* FIXME tmp *)
     5.9 +(*    |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs*)
    5.10 +    |> Thm.unconstrainT
    5.11      |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
    5.12          (((v, 0), []), TVar ((v, 0), sort))) vs, [])
    5.13      |> strip_of_class