clarified Thm.of_class/of_sort/class_triv;
authorwenzelm
Mon Jul 06 20:36:38 2009 +0200 (2009-07-06 ago)
changeset 31944c8a35979a5bc
parent 31943 5e960a0780a2
child 31945 d5f186aa0bed
clarified Thm.of_class/of_sort/class_triv;
src/Pure/Isar/class.ML
src/Pure/axclass.ML
src/Pure/more_thm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Jul 06 19:58:52 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Jul 06 20:36:38 2009 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4      val sup_of_classes = map (snd o rules thy) sups;
     1.5      val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
     1.6      val axclass_intro = #intro (AxClass.get_info thy class);
     1.7 -    val base_sort_trivs = Thm.sort_triv thy (aT, base_sort);
     1.8 +    val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
     1.9      val tac = REPEAT (SOMEGOAL
    1.10        (Tactic.match_tac (axclass_intro :: sup_of_classes
    1.11           @ loc_axiom_intros @ base_sort_trivs)
     2.1 --- a/src/Pure/axclass.ML	Mon Jul 06 19:58:52 2009 +0200
     2.2 +++ b/src/Pure/axclass.ML	Mon Jul 06 20:36:38 2009 +0200
     2.3 @@ -214,7 +214,7 @@
     2.4        |> snd))
     2.5    end;
     2.6  
     2.7 -fun complete_arities thy = 
     2.8 +fun complete_arities thy =
     2.9    let
    2.10      val arities = snd (get_instances thy);
    2.11      val (completions, arities') = arities
    2.12 @@ -575,12 +575,13 @@
    2.13  fun derive_type _ (_, []) = []
    2.14    | derive_type thy (typ, sort) =
    2.15        let
    2.16 +        val certT = Thm.ctyp_of thy;
    2.17          val vars = Term.fold_atyps
    2.18              (fn T as TFree (_, S) => insert (eq_fst op =) (T, S)
    2.19                | T as TVar (_, S) => insert (eq_fst op =) (T, S)
    2.20                | _ => I) typ [];
    2.21          val hyps = vars
    2.22 -          |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
    2.23 +          |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
    2.24          val ths = (typ, sort)
    2.25            |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
    2.26             {class_relation =
     3.1 --- a/src/Pure/more_thm.ML	Mon Jul 06 19:58:52 2009 +0200
     3.2 +++ b/src/Pure/more_thm.ML	Mon Jul 06 20:36:38 2009 +0200
     3.3 @@ -26,7 +26,8 @@
     3.4    val eq_thm_thy: thm * thm -> bool
     3.5    val eq_thm_prop: thm * thm -> bool
     3.6    val equiv_thm: thm * thm -> bool
     3.7 -  val sort_triv: theory -> typ * sort -> thm list
     3.8 +  val class_triv: theory -> class -> thm
     3.9 +  val of_sort: ctyp * sort -> thm list
    3.10    val check_shyps: sort list -> thm -> thm
    3.11    val is_dummy: thm -> bool
    3.12    val plain_prop_of: thm -> term
    3.13 @@ -171,14 +172,10 @@
    3.14  
    3.15  (* type classes and sorts *)
    3.16  
    3.17 -fun sort_triv thy (T, S) =
    3.18 -  let
    3.19 -    val certT = Thm.ctyp_of thy;
    3.20 -    val cT = certT T;
    3.21 -    fun class_triv c =
    3.22 -      Thm.class_triv thy c
    3.23 -      |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
    3.24 -  in map class_triv S end;
    3.25 +fun class_triv thy c =
    3.26 +  Thm.of_class (Thm.ctyp_of thy (TVar ((Name.aT, 0), [c])), c);
    3.27 +
    3.28 +fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
    3.29  
    3.30  fun check_shyps sorts raw_th =
    3.31    let
     4.1 --- a/src/Pure/thm.ML	Mon Jul 06 19:58:52 2009 +0200
     4.2 +++ b/src/Pure/thm.ML	Mon Jul 06 20:36:38 2009 +0200
     4.3 @@ -92,7 +92,7 @@
     4.4    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
     4.5    val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
     4.6    val trivial: cterm -> thm
     4.7 -  val class_triv: theory -> class -> thm
     4.8 +  val of_class: ctyp * class -> thm
     4.9    val unconstrainT: ctyp -> thm -> thm
    4.10    val dest_state: thm * int -> (term * term) list * term list * term * term
    4.11    val lift_rule: cterm -> thm -> thm
    4.12 @@ -1110,22 +1110,28 @@
    4.13        tpairs = [],
    4.14        prop = Logic.mk_implies (A, A)});
    4.15  
    4.16 -(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
    4.17 -fun class_triv thy raw_c =
    4.18 +(*Axiom-scheme reflecting signature contents
    4.19 +        T :: c
    4.20 +  -------------------
    4.21 +  OFCLASS(T, c_class)
    4.22 +*)
    4.23 +fun of_class (cT, raw_c) =
    4.24    let
    4.25 +    val Ctyp {thy_ref, T, ...} = cT;
    4.26 +    val thy = Theory.deref thy_ref;
    4.27      val c = Sign.certify_class thy raw_c;
    4.28 -    val T = TVar ((Name.aT, 0), [c]);
    4.29 -    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c))
    4.30 -      handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    4.31 +    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
    4.32    in
    4.33 -    Thm (deriv_rule0 (Pt.OfClass (T, c)),
    4.34 -     {thy_ref = Theory.check_thy thy,
    4.35 -      tags = [],
    4.36 -      maxidx = maxidx,
    4.37 -      shyps = sorts,
    4.38 -      hyps = [],
    4.39 -      tpairs = [],
    4.40 -      prop = prop})
    4.41 +    if Sign.of_sort thy (T, [c]) then
    4.42 +      Thm (deriv_rule0 (Pt.OfClass (T, c)),
    4.43 +       {thy_ref = Theory.check_thy thy,
    4.44 +        tags = [],
    4.45 +        maxidx = maxidx,
    4.46 +        shyps = sorts,
    4.47 +        hyps = [],
    4.48 +        tpairs = [],
    4.49 +        prop = prop})
    4.50 +    else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
    4.51    end;
    4.52  
    4.53  (*Internalize sort constraints of type variable*)