# HG changeset patch # User wenzelm # Date 1246903132 -7200 # Node ID 5e960a0780a294d79b7e71a04016166fc9219dc2 # Parent 63466160ff2758d0a2e9449b16da5937bb950085 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort; diff -r 63466160ff27 -r 5e960a0780a2 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/HOL/Tools/refute.ML Mon Jul 06 19:58:52 2009 +0200 @@ -909,8 +909,8 @@ (* and the class definition *) let val class = Logic.class_of_const s - val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class) - val ax_in = SOME (specialize_type thy (s, T) inclass) + val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class) + val ax_in = SOME (specialize_type thy (s, T) of_class) (* type match may fail due to sort constraints *) handle Type.TYPE_MATCH => NONE val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/Pure/Isar/class.ML Mon Jul 06 19:58:52 2009 +0200 @@ -83,7 +83,7 @@ (fst (Locale.intros_of thy class)); (* of_class *) - val of_class_prop_concl = Logic.mk_inclass (aT, class); + val of_class_prop_concl = Logic.mk_of_class (aT, class); val of_class_prop = case prop of NONE => of_class_prop_concl | SOME prop => Logic.mk_implies (Morphism.term const_morph ((map_types o map_atyps) (K aT) prop), of_class_prop_concl); diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Mon Jul 06 19:58:52 2009 +0200 @@ -54,7 +54,7 @@ (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), (Binding.name "Hyp", propT --> proofT, NoSyn), (Binding.name "Oracle", propT --> proofT, NoSyn), - (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn), + (Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT, NoSyn), (Binding.name "MinProof", proofT, Delimfix "?")] |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"] |> Sign.add_syntax_i @@ -113,11 +113,11 @@ | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) - | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) = + | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) = (case try Logic.class_of_const c_class of SOME c => change_type (if ty then SOME Ts else NONE) - (Inclass (TVar ((Name.aT, 0), []), c)) + (OfClass (TVar ((Name.aT, 0), []), c)) | NONE => error ("Bad class constant: " ^ quote c_class)) | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v @@ -148,7 +148,7 @@ val AppPt = Const ("AppP", [proofT, proofT] ---> proofT); val Hypt = Const ("Hyp", propT --> proofT); val Oraclet = Const ("Oracle", propT --> proofT); -val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT); +val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT); val MinProoft = Const ("MinProof", proofT); val mk_tyapp = fold (fn T => fn prf => Const ("Appt", @@ -161,8 +161,8 @@ | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) | term_of _ (PAxm (name, _, SOME Ts)) = mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) - | term_of _ (Inclass (T, c)) = - mk_tyapp [T] (Inclasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) + | term_of _ (OfClass (T, c)) = + mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) | term_of _ (PBound i) = Bound i | term_of Ts (Abst (s, opT, prf)) = let val T = the_default dummyT opT diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Mon Jul 06 19:58:52 2009 +0200 @@ -223,8 +223,8 @@ mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf - | mk_cnstrts env _ _ vTs (prf as Inclass (T, c)) = - mk_cnstrts_atom env vTs (Logic.mk_inclass (T, c)) NONE prf + | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) = + mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs) @@ -321,7 +321,7 @@ | prop_of0 Hs (Hyp t) = t | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts | prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts - | prop_of0 Hs (Inclass (T, c)) = Logic.mk_inclass (T, c) + | prop_of0 Hs (OfClass (T, c)) = Logic.mk_of_class (T, c) | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts | prop_of0 _ _ = error "prop_of: partial proof object"; diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/Pure/axclass.ML Mon Jul 06 19:58:52 2009 +0200 @@ -470,9 +470,9 @@ (* definition *) - val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss; + val conjs = map (curry Logic.mk_of_class (Term.aT [])) super @ flat axiomss; val class_eq = - Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_balanced conjs); + Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs); val ([def], def_thy) = thy @@ -605,7 +605,7 @@ val ths = sort |> map (fn c => Goal.finish (the (lookup_type cache' typ c) RS - Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c)))) + Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c)))) |> Thm.adjust_maxidx_thm ~1); in (ths, cache') end; diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/logic.ML --- a/src/Pure/logic.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/Pure/logic.ML Mon Jul 06 19:58:52 2009 +0200 @@ -36,8 +36,8 @@ val type_map: (term -> term) -> typ -> typ val const_of_class: class -> string val class_of_const: string -> class - val mk_inclass: typ * class -> term - val dest_inclass: term -> typ * class + val mk_of_class: typ * class -> term + val dest_of_class: term -> typ * class val name_classrel: string * string -> string val mk_classrel: class * class -> term val dest_classrel: term -> class * class @@ -219,13 +219,13 @@ handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); -(* class constraints *) +(* class membership *) -fun mk_inclass (ty, c) = +fun mk_of_class (ty, c) = Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty; -fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) - | dest_inclass t = raise TERM ("dest_inclass", [t]); +fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class) + | dest_of_class t = raise TERM ("dest_of_class", [t]); (* class relations *) @@ -233,10 +233,10 @@ fun name_classrel (c1, c2) = Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2; -fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2); +fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2); fun dest_classrel tm = - (case dest_inclass tm of + (case dest_of_class tm of (TVar (_, [c1]), c2) => (c1, c2) | _ => raise TERM ("dest_classrel", [tm])); @@ -251,13 +251,13 @@ fun mk_arities (t, Ss, S) = let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss)) - in map (fn c => mk_inclass (T, c)) S end; + in map (fn c => mk_of_class (T, c)) S end; fun dest_arity tm = let fun err () = raise TERM ("dest_arity", [tm]); - val (ty, c) = dest_inclass tm; + val (ty, c) = dest_of_class tm; val (t, tvars) = (case ty of Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ()) diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/Pure/proofterm.ML Mon Jul 06 19:58:52 2009 +0200 @@ -19,7 +19,7 @@ | op %% of proof * proof | Hyp of term | PAxm of string * term * typ list option - | Inclass of typ * class + | OfClass of typ * class | Oracle of string * term * typ list option | Promise of serial * term * typ list | PThm of serial * ((string * term * typ list option) * proof_body future) @@ -141,7 +141,7 @@ | op %% of proof * proof | Hyp of term | PAxm of string * term * typ list option - | Inclass of typ * class + | OfClass of typ * class | Oracle of string * term * typ list option | Promise of serial * term * typ list | PThm of serial * ((string * term * typ list option) * proof_body future) @@ -292,7 +292,7 @@ | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2 handle SAME => prf1 %% mapp prf2) | mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts)) - | mapp (Inclass (T, c)) = Inclass (apsome g (SOME T) |> the, c) + | mapp (OfClass (T, c)) = OfClass (apsome g (SOME T) |> the, c) | mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts)) | mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts) | mapp (PThm (i, ((a, prop, SOME Ts), body))) = @@ -320,7 +320,7 @@ | fold_proof_terms f g (prf1 %% prf2) = fold_proof_terms f g prf1 #> fold_proof_terms f g prf2 | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts - | fold_proof_terms _ g (Inclass (T, _)) = g T + | fold_proof_terms _ g (OfClass (T, _)) = g T | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts | fold_proof_terms _ g (Promise (_, _, Ts)) = fold g Ts | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts @@ -335,7 +335,7 @@ | size_of_proof _ = 1; fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs) - | change_type (SOME [T]) (Inclass (_, c)) = Inclass (T, c) + | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c) | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs) | change_type opTs (Promise _) = error "change_type: unexpected promise" | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body)) @@ -473,7 +473,7 @@ | norm (prf1 %% prf2) = (norm prf1 %% normh prf2 handle SAME => prf1 %% norm prf2) | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (htypeTs norm_types_same) Ts) - | norm (Inclass (T, c)) = Inclass (htypeT norm_type_same T, c) + | norm (OfClass (T, c)) = OfClass (htypeT norm_type_same T, c) | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (htypeTs norm_types_same) Ts) | norm (Promise (i, prop, Ts)) = Promise (i, prop, htypeTs norm_types_same Ts) | norm (PThm (i, ((s, t, Ts), body))) = @@ -719,8 +719,8 @@ handle SAME => prf1 %% lift' Us Ts prf2) | lift' _ _ (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts) - | lift' _ _ (Inclass (T, c)) = - Inclass (same (op =) (Logic.incr_tvar inc) T, c) + | lift' _ _ (OfClass (T, c)) = + OfClass (same (op =) (Logic.incr_tvar inc) T, c) | lift' _ _ (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts) | lift' _ _ (Promise (i, prop, Ts)) = @@ -977,7 +977,7 @@ orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf) | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf) - | shrink' ls lev ts prfs (prf as Inclass _) = ([], false, map (pair false) ts, prf) + | shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf) | shrink' ls lev ts prfs prf = let val prop = @@ -1069,7 +1069,7 @@ | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) = if s1 = s2 then optmatch matchTs inst (opTs, opUs) else raise PMatch - | mtch Ts i j inst (Inclass (T1, c1), Inclass (T2, c2)) = + | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) = if c1 = c2 then matchT inst (T1, T2) else raise PMatch | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) = @@ -1103,7 +1103,7 @@ NONE => prf | SOME prf' => incr_pboundvars plev tlev prf') | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts) - | subst _ _ (Inclass (T, c)) = Inclass (substT T, c) + | subst _ _ (OfClass (T, c)) = OfClass (substT T, c) | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts) | subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts) | subst _ _ (PThm (i, ((id, prop, Ts), body))) = @@ -1130,7 +1130,7 @@ (_, Hyp (Var _)) => true | (Hyp (Var _), _) => true | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2 - | (Inclass (_, c), Inclass (_, d)) => c = d andalso matchrands prf1 prf2 + | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2 | (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) => a = b andalso propa = propb andalso matchrands prf1 prf2 | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2 diff -r 63466160ff27 -r 5e960a0780a2 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Jul 04 23:25:28 2009 +0200 +++ b/src/Pure/thm.ML Mon Jul 06 19:58:52 2009 +0200 @@ -1115,10 +1115,10 @@ let val c = Sign.certify_class thy raw_c; val T = TVar ((Name.aT, 0), [c]); - val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c)) + val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c)) handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); in - Thm (deriv_rule0 (Pt.Inclass (T, c)), + Thm (deriv_rule0 (Pt.OfClass (T, c)), {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx, @@ -1137,7 +1137,7 @@ raise THM ("unconstrainT: not a type variable", 0, [th]); val T' = TVar ((x, i), []); val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U)); - val constraints = map (curry Logic.mk_inclass T') S; + val constraints = map (curry Logic.mk_of_class T') S; in Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])), {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),