--- 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
--- 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";
--- 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
--- 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*)