renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
authorwenzelm
Mon Jul 06 19:58:52 2009 +0200 (2009-07-06)
changeset 319435e960a0780a2
parent 31942 63466160ff27
child 31944 c8a35979a5bc
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
src/HOL/Tools/refute.ML
src/Pure/Isar/class.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/axclass.ML
src/Pure/logic.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Jul 04 23:25:28 2009 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Jul 06 19:58:52 2009 +0200
     1.3 @@ -909,8 +909,8 @@
     1.4              (* and the class definition                               *)
     1.5              let
     1.6                val class   = Logic.class_of_const s
     1.7 -              val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
     1.8 -              val ax_in   = SOME (specialize_type thy (s, T) inclass)
     1.9 +              val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class)
    1.10 +              val ax_in   = SOME (specialize_type thy (s, T) of_class)
    1.11                  (* type match may fail due to sort constraints *)
    1.12                  handle Type.TYPE_MATCH => NONE
    1.13                val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax))
     2.1 --- a/src/Pure/Isar/class.ML	Sat Jul 04 23:25:28 2009 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Mon Jul 06 19:58:52 2009 +0200
     2.3 @@ -83,7 +83,7 @@
     2.4        (fst (Locale.intros_of thy class));
     2.5  
     2.6      (* of_class *)
     2.7 -    val of_class_prop_concl = Logic.mk_inclass (aT, class);
     2.8 +    val of_class_prop_concl = Logic.mk_of_class (aT, class);
     2.9      val of_class_prop = case prop of NONE => of_class_prop_concl
    2.10        | SOME prop => Logic.mk_implies (Morphism.term const_morph
    2.11            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
     3.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Jul 04 23:25:28 2009 +0200
     3.2 +++ b/src/Pure/Proof/proof_syntax.ML	Mon Jul 06 19:58:52 2009 +0200
     3.3 @@ -54,7 +54,7 @@
     3.4         (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
     3.5         (Binding.name "Hyp", propT --> proofT, NoSyn),
     3.6         (Binding.name "Oracle", propT --> proofT, NoSyn),
     3.7 -       (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
     3.8 +       (Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
     3.9         (Binding.name "MinProof", proofT, Delimfix "?")]
    3.10    |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
    3.11    |> Sign.add_syntax_i
    3.12 @@ -113,11 +113,11 @@
    3.13                     | NONE => error ("Unknown theorem " ^ quote name))
    3.14                   end
    3.15               | _ => error ("Illegal proof constant name: " ^ quote s))
    3.16 -      | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) =
    3.17 +      | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) =
    3.18            (case try Logic.class_of_const c_class of
    3.19              SOME c =>
    3.20                change_type (if ty then SOME Ts else NONE)
    3.21 -                (Inclass (TVar ((Name.aT, 0), []), c))
    3.22 +                (OfClass (TVar ((Name.aT, 0), []), c))
    3.23            | NONE => error ("Bad class constant: " ^ quote c_class))
    3.24        | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
    3.25        | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
    3.26 @@ -148,7 +148,7 @@
    3.27  val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
    3.28  val Hypt = Const ("Hyp", propT --> proofT);
    3.29  val Oraclet = Const ("Oracle", propT --> proofT);
    3.30 -val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT);
    3.31 +val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT);
    3.32  val MinProoft = Const ("MinProof", proofT);
    3.33  
    3.34  val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
    3.35 @@ -161,8 +161,8 @@
    3.36    | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
    3.37    | term_of _ (PAxm (name, _, SOME Ts)) =
    3.38        mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
    3.39 -  | term_of _ (Inclass (T, c)) =
    3.40 -      mk_tyapp [T] (Inclasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
    3.41 +  | term_of _ (OfClass (T, c)) =
    3.42 +      mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
    3.43    | term_of _ (PBound i) = Bound i
    3.44    | term_of Ts (Abst (s, opT, prf)) =
    3.45        let val T = the_default dummyT opT
     4.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Jul 04 23:25:28 2009 +0200
     4.2 +++ b/src/Pure/Proof/reconstruct.ML	Mon Jul 06 19:58:52 2009 +0200
     4.3 @@ -223,8 +223,8 @@
     4.4            mk_cnstrts_atom env vTs prop opTs prf
     4.5        | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
     4.6            mk_cnstrts_atom env vTs prop opTs prf
     4.7 -      | mk_cnstrts env _ _ vTs (prf as Inclass (T, c)) =
     4.8 -          mk_cnstrts_atom env vTs (Logic.mk_inclass (T, c)) NONE prf
     4.9 +      | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) =
    4.10 +          mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf
    4.11        | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
    4.12            mk_cnstrts_atom env vTs prop opTs prf
    4.13        | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
    4.14 @@ -321,7 +321,7 @@
    4.15    | prop_of0 Hs (Hyp t) = t
    4.16    | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
    4.17    | prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
    4.18 -  | prop_of0 Hs (Inclass (T, c)) = Logic.mk_inclass (T, c)
    4.19 +  | prop_of0 Hs (OfClass (T, c)) = Logic.mk_of_class (T, c)
    4.20    | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
    4.21    | prop_of0 _ _ = error "prop_of: partial proof object";
    4.22  
     5.1 --- a/src/Pure/axclass.ML	Sat Jul 04 23:25:28 2009 +0200
     5.2 +++ b/src/Pure/axclass.ML	Mon Jul 06 19:58:52 2009 +0200
     5.3 @@ -470,9 +470,9 @@
     5.4  
     5.5      (* definition *)
     5.6  
     5.7 -    val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss;
     5.8 +    val conjs = map (curry Logic.mk_of_class (Term.aT [])) super @ flat axiomss;
     5.9      val class_eq =
    5.10 -      Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
    5.11 +      Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
    5.12  
    5.13      val ([def], def_thy) =
    5.14        thy
    5.15 @@ -605,7 +605,7 @@
    5.16      val ths =
    5.17        sort |> map (fn c =>
    5.18          Goal.finish (the (lookup_type cache' typ c) RS
    5.19 -          Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c))))
    5.20 +          Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
    5.21          |> Thm.adjust_maxidx_thm ~1);
    5.22    in (ths, cache') end;
    5.23  
     6.1 --- a/src/Pure/logic.ML	Sat Jul 04 23:25:28 2009 +0200
     6.2 +++ b/src/Pure/logic.ML	Mon Jul 06 19:58:52 2009 +0200
     6.3 @@ -36,8 +36,8 @@
     6.4    val type_map: (term -> term) -> typ -> typ
     6.5    val const_of_class: class -> string
     6.6    val class_of_const: string -> class
     6.7 -  val mk_inclass: typ * class -> term
     6.8 -  val dest_inclass: term -> typ * class
     6.9 +  val mk_of_class: typ * class -> term
    6.10 +  val dest_of_class: term -> typ * class
    6.11    val name_classrel: string * string -> string
    6.12    val mk_classrel: class * class -> term
    6.13    val dest_classrel: term -> class * class
    6.14 @@ -219,13 +219,13 @@
    6.15    handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
    6.16  
    6.17  
    6.18 -(* class constraints *)
    6.19 +(* class membership *)
    6.20  
    6.21 -fun mk_inclass (ty, c) =
    6.22 +fun mk_of_class (ty, c) =
    6.23    Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
    6.24  
    6.25 -fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
    6.26 -  | dest_inclass t = raise TERM ("dest_inclass", [t]);
    6.27 +fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
    6.28 +  | dest_of_class t = raise TERM ("dest_of_class", [t]);
    6.29  
    6.30  
    6.31  (* class relations *)
    6.32 @@ -233,10 +233,10 @@
    6.33  fun name_classrel (c1, c2) =
    6.34    Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
    6.35  
    6.36 -fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
    6.37 +fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2);
    6.38  
    6.39  fun dest_classrel tm =
    6.40 -  (case dest_inclass tm of
    6.41 +  (case dest_of_class tm of
    6.42      (TVar (_, [c1]), c2) => (c1, c2)
    6.43    | _ => raise TERM ("dest_classrel", [tm]));
    6.44  
    6.45 @@ -251,13 +251,13 @@
    6.46  
    6.47  fun mk_arities (t, Ss, S) =
    6.48    let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
    6.49 -  in map (fn c => mk_inclass (T, c)) S end;
    6.50 +  in map (fn c => mk_of_class (T, c)) S end;
    6.51  
    6.52  fun dest_arity tm =
    6.53    let
    6.54      fun err () = raise TERM ("dest_arity", [tm]);
    6.55  
    6.56 -    val (ty, c) = dest_inclass tm;
    6.57 +    val (ty, c) = dest_of_class tm;
    6.58      val (t, tvars) =
    6.59        (case ty of
    6.60          Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
     7.1 --- a/src/Pure/proofterm.ML	Sat Jul 04 23:25:28 2009 +0200
     7.2 +++ b/src/Pure/proofterm.ML	Mon Jul 06 19:58:52 2009 +0200
     7.3 @@ -19,7 +19,7 @@
     7.4     | op %% of proof * proof
     7.5     | Hyp of term
     7.6     | PAxm of string * term * typ list option
     7.7 -   | Inclass of typ * class
     7.8 +   | OfClass of typ * class
     7.9     | Oracle of string * term * typ list option
    7.10     | Promise of serial * term * typ list
    7.11     | PThm of serial * ((string * term * typ list option) * proof_body future)
    7.12 @@ -141,7 +141,7 @@
    7.13   | op %% of proof * proof
    7.14   | Hyp of term
    7.15   | PAxm of string * term * typ list option
    7.16 - | Inclass of typ * class
    7.17 + | OfClass of typ * class
    7.18   | Oracle of string * term * typ list option
    7.19   | Promise of serial * term * typ list
    7.20   | PThm of serial * ((string * term * typ list option) * proof_body future)
    7.21 @@ -292,7 +292,7 @@
    7.22        | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2
    7.23            handle SAME => prf1 %% mapp prf2)
    7.24        | mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts))
    7.25 -      | mapp (Inclass (T, c)) = Inclass (apsome g (SOME T) |> the, c)
    7.26 +      | mapp (OfClass (T, c)) = OfClass (apsome g (SOME T) |> the, c)
    7.27        | mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts))
    7.28        | mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts)
    7.29        | mapp (PThm (i, ((a, prop, SOME Ts), body))) =
    7.30 @@ -320,7 +320,7 @@
    7.31    | fold_proof_terms f g (prf1 %% prf2) =
    7.32        fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
    7.33    | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
    7.34 -  | fold_proof_terms _ g (Inclass (T, _)) = g T
    7.35 +  | fold_proof_terms _ g (OfClass (T, _)) = g T
    7.36    | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
    7.37    | fold_proof_terms _ g (Promise (_, _, Ts)) = fold g Ts
    7.38    | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts
    7.39 @@ -335,7 +335,7 @@
    7.40    | size_of_proof _ = 1;
    7.41  
    7.42  fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
    7.43 -  | change_type (SOME [T]) (Inclass (_, c)) = Inclass (T, c)
    7.44 +  | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
    7.45    | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
    7.46    | change_type opTs (Promise _) = error "change_type: unexpected promise"
    7.47    | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body))
    7.48 @@ -473,7 +473,7 @@
    7.49        | norm (prf1 %% prf2) = (norm prf1 %% normh prf2
    7.50            handle SAME => prf1 %% norm prf2)
    7.51        | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (htypeTs norm_types_same) Ts)
    7.52 -      | norm (Inclass (T, c)) = Inclass (htypeT norm_type_same T, c)
    7.53 +      | norm (OfClass (T, c)) = OfClass (htypeT norm_type_same T, c)
    7.54        | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (htypeTs norm_types_same) Ts)
    7.55        | norm (Promise (i, prop, Ts)) = Promise (i, prop, htypeTs norm_types_same Ts)
    7.56        | norm (PThm (i, ((s, t, Ts), body))) =
    7.57 @@ -719,8 +719,8 @@
    7.58            handle SAME => prf1 %% lift' Us Ts prf2)
    7.59        | lift' _ _ (PAxm (s, prop, Ts)) =
    7.60            PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    7.61 -      | lift' _ _ (Inclass (T, c)) =
    7.62 -          Inclass (same (op =) (Logic.incr_tvar inc) T, c)
    7.63 +      | lift' _ _ (OfClass (T, c)) =
    7.64 +          OfClass (same (op =) (Logic.incr_tvar inc) T, c)
    7.65        | lift' _ _ (Oracle (s, prop, Ts)) =
    7.66            Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    7.67        | lift' _ _ (Promise (i, prop, Ts)) =
    7.68 @@ -977,7 +977,7 @@
    7.69               orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
    7.70        | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
    7.71        | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
    7.72 -      | shrink' ls lev ts prfs (prf as Inclass _) = ([], false, map (pair false) ts, prf)
    7.73 +      | shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf)
    7.74        | shrink' ls lev ts prfs prf =
    7.75            let
    7.76              val prop =
    7.77 @@ -1069,7 +1069,7 @@
    7.78        | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
    7.79            if s1 = s2 then optmatch matchTs inst (opTs, opUs)
    7.80            else raise PMatch
    7.81 -      | mtch Ts i j inst (Inclass (T1, c1), Inclass (T2, c2)) =
    7.82 +      | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) =
    7.83            if c1 = c2 then matchT inst (T1, T2)
    7.84            else raise PMatch
    7.85        | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) =
    7.86 @@ -1103,7 +1103,7 @@
    7.87            NONE => prf
    7.88          | SOME prf' => incr_pboundvars plev tlev prf')
    7.89        | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts)
    7.90 -      | subst _ _ (Inclass (T, c)) = Inclass (substT T, c)
    7.91 +      | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
    7.92        | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts)
    7.93        | subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts)
    7.94        | subst _ _ (PThm (i, ((id, prop, Ts), body))) =
    7.95 @@ -1130,7 +1130,7 @@
    7.96          (_, Hyp (Var _)) => true
    7.97        | (Hyp (Var _), _) => true
    7.98        | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
    7.99 -      | (Inclass (_, c), Inclass (_, d)) => c = d andalso matchrands prf1 prf2
   7.100 +      | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2
   7.101        | (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) =>
   7.102            a = b andalso propa = propb andalso matchrands prf1 prf2
   7.103        | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
     8.1 --- a/src/Pure/thm.ML	Sat Jul 04 23:25:28 2009 +0200
     8.2 +++ b/src/Pure/thm.ML	Mon Jul 06 19:58:52 2009 +0200
     8.3 @@ -1115,10 +1115,10 @@
     8.4    let
     8.5      val c = Sign.certify_class thy raw_c;
     8.6      val T = TVar ((Name.aT, 0), [c]);
     8.7 -    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c))
     8.8 +    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c))
     8.9        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    8.10    in
    8.11 -    Thm (deriv_rule0 (Pt.Inclass (T, c)),
    8.12 +    Thm (deriv_rule0 (Pt.OfClass (T, c)),
    8.13       {thy_ref = Theory.check_thy thy,
    8.14        tags = [],
    8.15        maxidx = maxidx,
    8.16 @@ -1137,7 +1137,7 @@
    8.17        raise THM ("unconstrainT: not a type variable", 0, [th]);
    8.18      val T' = TVar ((x, i), []);
    8.19      val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
    8.20 -    val constraints = map (curry Logic.mk_inclass T') S;
    8.21 +    val constraints = map (curry Logic.mk_of_class T') S;
    8.22    in
    8.23      Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
    8.24       {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),