added pro-forma proof constructor Inclass;
authorwenzelm
Thu Jul 02 20:55:44 2009 +0200 (2009-07-02)
changeset 31903c5221dbc40f6
parent 31902 862ae16a799d
child 31904 a86896359ca4
added pro-forma proof constructor Inclass;
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Jul 02 17:34:14 2009 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Jul 02 20:55:44 2009 +0200
     1.3 @@ -54,6 +54,7 @@
     1.4         (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
     1.5         (Binding.name "Hyp", propT --> proofT, NoSyn),
     1.6         (Binding.name "Oracle", propT --> proofT, NoSyn),
     1.7 +       (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
     1.8         (Binding.name "MinProof", proofT, Delimfix "?")]
     1.9    |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
    1.10    |> Sign.add_syntax_i
    1.11 @@ -112,6 +113,12 @@
    1.12                     | NONE => error ("Unknown theorem " ^ quote name))
    1.13                   end
    1.14               | _ => error ("Illegal proof constant name: " ^ quote s))
    1.15 +      | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) =
    1.16 +          (case try Logic.class_of_const c_class of
    1.17 +            SOME c =>
    1.18 +              change_type (if ty then SOME Ts else NONE)
    1.19 +                (Inclass (TVar ((Name.aT, 0), []), c))
    1.20 +          | NONE => error ("Bad class constant: " ^ quote c_class))
    1.21        | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
    1.22        | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
    1.23        | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
    1.24 @@ -141,6 +148,7 @@
    1.25  val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
    1.26  val Hypt = Const ("Hyp", propT --> proofT);
    1.27  val Oraclet = Const ("Oracle", propT --> proofT);
    1.28 +val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT);
    1.29  val MinProoft = Const ("MinProof", proofT);
    1.30  
    1.31  val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
    1.32 @@ -153,6 +161,8 @@
    1.33    | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
    1.34    | term_of _ (PAxm (name, _, SOME Ts)) =
    1.35        mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
    1.36 +  | term_of _ (Inclass (T, c)) =
    1.37 +      mk_tyapp [T] (Inclasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
    1.38    | term_of _ (PBound i) = Bound i
    1.39    | term_of Ts (Abst (s, opT, prf)) =
    1.40        let val T = the_default dummyT opT
     2.1 --- a/src/Pure/Proof/reconstruct.ML	Thu Jul 02 17:34:14 2009 +0200
     2.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 02 20:55:44 2009 +0200
     2.3 @@ -140,7 +140,8 @@
     2.4            let
     2.5              val tvars = OldTerm.term_tvars prop;
     2.6              val tfrees = OldTerm.term_tfrees prop;
     2.7 -            val (env', Ts) = (case opTs of
     2.8 +            val (env', Ts) =
     2.9 +              (case opTs of
    2.10                  NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
    2.11                | SOME Ts => (env, Ts));
    2.12              val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
    2.13 @@ -222,6 +223,8 @@
    2.14            mk_cnstrts_atom env vTs prop opTs prf
    2.15        | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
    2.16            mk_cnstrts_atom env vTs prop opTs prf
    2.17 +      | mk_cnstrts env _ _ vTs (prf as Inclass (T, c)) =
    2.18 +          mk_cnstrts_atom env vTs (Logic.mk_inclass (T, c)) NONE prf
    2.19        | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
    2.20            mk_cnstrts_atom env vTs prop opTs prf
    2.21        | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
    2.22 @@ -318,6 +321,7 @@
    2.23    | prop_of0 Hs (Hyp t) = t
    2.24    | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
    2.25    | prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
    2.26 +  | prop_of0 Hs (Inclass (T, c)) = Logic.mk_inclass (T, c)
    2.27    | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
    2.28    | prop_of0 _ _ = error "prop_of: partial proof object";
    2.29  
     3.1 --- a/src/Pure/proofterm.ML	Thu Jul 02 17:34:14 2009 +0200
     3.2 +++ b/src/Pure/proofterm.ML	Thu Jul 02 20:55:44 2009 +0200
     3.3 @@ -19,6 +19,7 @@
     3.4     | op %% of proof * proof
     3.5     | Hyp of term
     3.6     | PAxm of string * term * typ list option
     3.7 +   | Inclass of typ * class
     3.8     | Oracle of string * term * typ list option
     3.9     | Promise of serial * term * typ list
    3.10     | PThm of serial * ((string * term * typ list option) * proof_body future)
    3.11 @@ -140,6 +141,7 @@
    3.12   | op %% of proof * proof
    3.13   | Hyp of term
    3.14   | PAxm of string * term * typ list option
    3.15 + | Inclass of typ * class
    3.16   | Oracle of string * term * typ list option
    3.17   | Promise of serial * term * typ list
    3.18   | PThm of serial * ((string * term * typ list option) * proof_body future)
    3.19 @@ -290,6 +292,7 @@
    3.20        | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2
    3.21            handle SAME => prf1 %% mapp prf2)
    3.22        | mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts))
    3.23 +      | mapp (Inclass (T, c)) = Inclass (apsome g (SOME T) |> the, c)
    3.24        | mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts))
    3.25        | mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts)
    3.26        | mapp (PThm (i, ((a, prop, SOME Ts), body))) =
    3.27 @@ -317,6 +320,7 @@
    3.28    | fold_proof_terms f g (prf1 %% prf2) =
    3.29        fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
    3.30    | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
    3.31 +  | fold_proof_terms _ g (Inclass (T, _)) = g T
    3.32    | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
    3.33    | fold_proof_terms _ g (Promise (_, _, Ts)) = fold g Ts
    3.34    | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts
    3.35 @@ -331,6 +335,7 @@
    3.36    | size_of_proof _ = 1;
    3.37  
    3.38  fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
    3.39 +  | change_type (SOME [T]) (Inclass (_, c)) = Inclass (T, c)
    3.40    | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
    3.41    | change_type opTs (Promise _) = error "change_type: unexpected promise"
    3.42    | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body))
    3.43 @@ -468,6 +473,7 @@
    3.44        | norm (prf1 %% prf2) = (norm prf1 %% normh prf2
    3.45            handle SAME => prf1 %% norm prf2)
    3.46        | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (htypeTs norm_types_same) Ts)
    3.47 +      | norm (Inclass (T, c)) = Inclass (htypeT norm_type_same T, c)
    3.48        | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (htypeTs norm_types_same) Ts)
    3.49        | norm (Promise (i, prop, Ts)) = Promise (i, prop, htypeTs norm_types_same Ts)
    3.50        | norm (PThm (i, ((s, t, Ts), body))) =
    3.51 @@ -713,6 +719,8 @@
    3.52            handle SAME => prf1 %% lift' Us Ts prf2)
    3.53        | lift' _ _ (PAxm (s, prop, Ts)) =
    3.54            PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    3.55 +      | lift' _ _ (Inclass (T, c)) =
    3.56 +          Inclass (same (op =) (Logic.incr_tvar inc) T, c)
    3.57        | lift' _ _ (Oracle (s, prop, Ts)) =
    3.58            Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    3.59        | lift' _ _ (Promise (i, prop, Ts)) =
    3.60 @@ -967,8 +975,9 @@
    3.61               orelse has_duplicates (op =)
    3.62                 (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
    3.63               orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
    3.64 -      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t)
    3.65 -      | shrink' ls lev ts prfs MinProof = ([], false, map (pair false) ts, MinProof)
    3.66 +      | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
    3.67 +      | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
    3.68 +      | shrink' ls lev ts prfs (prf as Inclass _) = ([], false, map (pair false) ts, prf)
    3.69        | shrink' ls lev ts prfs prf =
    3.70            let
    3.71              val prop =
    3.72 @@ -1060,6 +1069,9 @@
    3.73        | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
    3.74            if s1 = s2 then optmatch matchTs inst (opTs, opUs)
    3.75            else raise PMatch
    3.76 +      | mtch Ts i j inst (Inclass (T1, c1), Inclass (T2, c2)) =
    3.77 +          if c1 = c2 then matchT inst (T1, T2)
    3.78 +          else raise PMatch
    3.79        | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) =
    3.80            if name1 = name2 andalso prop1 = prop2 then
    3.81              optmatch matchTs inst (opTs, opUs)
    3.82 @@ -1091,6 +1103,7 @@
    3.83            NONE => prf
    3.84          | SOME prf' => incr_pboundvars plev tlev prf')
    3.85        | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts)
    3.86 +      | subst _ _ (Inclass (T, c)) = Inclass (substT T, c)
    3.87        | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts)
    3.88        | subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts)
    3.89        | subst _ _ (PThm (i, ((id, prop, Ts), body))) =
    3.90 @@ -1117,6 +1130,7 @@
    3.91          (_, Hyp (Var _)) => true
    3.92        | (Hyp (Var _), _) => true
    3.93        | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
    3.94 +      | (Inclass (_, c), Inclass (_, d)) => c = d andalso matchrands prf1 prf2
    3.95        | (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) =>
    3.96            a = b andalso propa = propb andalso matchrands prf1 prf2
    3.97        | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
     4.1 --- a/src/Pure/thm.ML	Thu Jul 02 17:34:14 2009 +0200
     4.2 +++ b/src/Pure/thm.ML	Thu Jul 02 20:55:44 2009 +0200
     4.3 @@ -1110,15 +1110,21 @@
     4.4        prop = Logic.mk_implies (A, A)});
     4.5  
     4.6  (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
     4.7 -fun class_triv thy c =
     4.8 +fun class_triv thy raw_c =
     4.9    let
    4.10 -    val Cterm {t, maxidx, sorts, ...} =
    4.11 -      cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
    4.12 -        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    4.13 -    val der = deriv_rule0 (Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
    4.14 +    val c = Sign.certify_class thy raw_c;
    4.15 +    val T = TVar ((Name.aT, 0), [c]);
    4.16 +    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c))
    4.17 +      handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    4.18    in
    4.19 -    Thm (der, {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx,
    4.20 -      shyps = sorts, hyps = [], tpairs = [], prop = t})
    4.21 +    Thm (deriv_rule0 (Pt.Inclass (T, c)),
    4.22 +     {thy_ref = Theory.check_thy thy,
    4.23 +      tags = [],
    4.24 +      maxidx = maxidx,
    4.25 +      shyps = sorts,
    4.26 +      hyps = [],
    4.27 +      tpairs = [],
    4.28 +      prop = prop})
    4.29    end;
    4.30  
    4.31  (*Internalize sort constraints of type variable*)