--- 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))
--- 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);
--- 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
--- 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";
--- 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;
--- 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 ())
--- 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
--- 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),