# HG changeset patch
# User wenzelm
# Date 1246560944 -7200
# Node ID c5221dbc40f6ed8f56b47e17dfd4e594d5c369b8
# Parent  862ae16a799db7cc36b390c730ccf30064228de0
added pro-forma proof constructor Inclass;

diff -r 862ae16a799d -r c5221dbc40f6 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Jul 02 17:34:14 2009 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Thu Jul 02 20:55:44 2009 +0200
@@ -54,6 +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 "MinProof", proofT, Delimfix "?")]
   |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
   |> Sign.add_syntax_i
@@ -112,6 +113,12 @@
                    | NONE => error ("Unknown theorem " ^ quote name))
                  end
              | _ => error ("Illegal proof constant name: " ^ quote s))
+      | prf_of Ts (Const ("Inclass", _) $ 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))
+          | 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
       | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
@@ -141,6 +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 MinProoft = Const ("MinProof", proofT);
 
 val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
@@ -153,6 +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 _ (PBound i) = Bound i
   | term_of Ts (Abst (s, opT, prf)) =
       let val T = the_default dummyT opT
diff -r 862ae16a799d -r c5221dbc40f6 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Jul 02 17:34:14 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 02 20:55:44 2009 +0200
@@ -140,7 +140,8 @@
           let
             val tvars = OldTerm.term_tvars prop;
             val tfrees = OldTerm.term_tfrees prop;
-            val (env', Ts) = (case opTs of
+            val (env', Ts) =
+              (case opTs of
                 NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
               | SOME Ts => (env, Ts));
             val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
@@ -222,6 +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 Oracle (_, prop, opTs)) =
           mk_cnstrts_atom env vTs prop opTs prf
       | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
@@ -318,6 +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 (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 _ _ = error "prop_of: partial proof object";
 
diff -r 862ae16a799d -r c5221dbc40f6 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jul 02 17:34:14 2009 +0200
+++ b/src/Pure/proofterm.ML	Thu Jul 02 20:55:44 2009 +0200
@@ -19,6 +19,7 @@
    | op %% of proof * proof
    | Hyp of term
    | PAxm of string * term * typ list option
+   | Inclass 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)
@@ -140,6 +141,7 @@
  | op %% of proof * proof
  | Hyp of term
  | PAxm of string * term * typ list option
+ | Inclass 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)
@@ -290,6 +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 (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))) =
@@ -317,6 +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 (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
@@ -331,6 +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 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))
@@ -468,6 +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 (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))) =
@@ -713,6 +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' _ _ (Oracle (s, prop, Ts)) =
           Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
       | lift' _ _ (Promise (i, prop, Ts)) =
@@ -967,8 +975,9 @@
              orelse has_duplicates (op =)
                (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
-      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t)
-      | shrink' ls lev ts prfs MinProof = ([], false, map (pair false) ts, MinProof)
+      | 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 =
           let
             val prop =
@@ -1060,6 +1069,9 @@
       | 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)) =
+          if c1 = c2 then matchT inst (T1, T2)
+          else raise PMatch
       | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) =
           if name1 = name2 andalso prop1 = prop2 then
             optmatch matchTs inst (opTs, opUs)
@@ -1091,6 +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 _ _ (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))) =
@@ -1117,6 +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
       | (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 862ae16a799d -r c5221dbc40f6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jul 02 17:34:14 2009 +0200
+++ b/src/Pure/thm.ML	Thu Jul 02 20:55:44 2009 +0200
@@ -1110,15 +1110,21 @@
       prop = Logic.mk_implies (A, A)});
 
 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
-fun class_triv thy c =
+fun class_triv thy raw_c =
   let
-    val Cterm {t, maxidx, sorts, ...} =
-      cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
-        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
-    val der = deriv_rule0 (Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
+    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))
+      handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   in
-    Thm (der, {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx,
-      shyps = sorts, hyps = [], tpairs = [], prop = t})
+    Thm (deriv_rule0 (Pt.Inclass (T, c)),
+     {thy_ref = Theory.check_thy thy,
+      tags = [],
+      maxidx = maxidx,
+      shyps = sorts,
+      hyps = [],
+      tpairs = [],
+      prop = prop})
   end;
 
 (*Internalize sort constraints of type variable*)