--- a/src/HOL/Extraction.thy Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Extraction.thy Fri Oct 11 22:06:49 2019 +0200
@@ -17,11 +17,11 @@
[("bool", ([], NONE))] #>
Extraction.set_preprocessor (fn thy =>
Proofterm.rewrite_proof_notypes
- ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o
+ ([], Rewrite_HOL_Proof.elim_cong :: Proof_Rewrite_Rules.rprocs true) o
Proofterm.rewrite_proof thy
- (RewriteHOLProof.rews,
- ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o
- ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
+ (Rewrite_HOL_Proof.rews,
+ Proof_Rewrite_Rules.rprocs true @ [Proof_Rewrite_Rules.expand_of_class thy]) o
+ Proof_Rewrite_Rules.elim_vars (curry Const \<^const_name>\<open>default\<close>))
\<close>
lemmas [extraction_expand] =
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy Fri Oct 11 22:06:49 2019 +0200
@@ -23,14 +23,14 @@
val thm = @{thm ex};
(*proof body with digest*)
- val body = Proofterm.strip_thm (Thm.proof_body_of thm);
+ val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
(*proof term only*)
val prf = Proofterm.proof_of body;
(*clean output*)
- Pretty.writeln (Proof_Syntax.pretty_clean_proof_of \<^context> false thm);
- Pretty.writeln (Proof_Syntax.pretty_clean_proof_of \<^context> true thm);
+ Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> false thm);
+ Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> true thm);
(*all theorems used in the graph of nested proofs*)
val all_thms =
--- a/src/HOL/Proofs/ex/XML_Data.thy Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy Fri Oct 11 22:06:49 2019 +0200
@@ -13,7 +13,8 @@
ML \<open>
fun export_proof thy thm =
- Proofterm.encode (Sign.consts_of thy) (Thm.clean_proof_of true thm);
+ Proofterm.encode (Sign.consts_of thy)
+ (Proofterm.reconstruct_proof thy (Thm.prop_of thm) (Thm.standard_proof_of true thm));
fun import_proof thy xml =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 11 22:06:49 2019 +0200
@@ -117,7 +117,7 @@
NONE => NONE
| SOME body =>
let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in
- SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
+ SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm_body body))
handle TOO_MANY () => NONE
end)
--- a/src/HOL/Tools/inductive_realizer.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Oct 11 22:06:49 2019 +0200
@@ -269,7 +269,7 @@
in (name, (vs,
if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
Extraction.abs_corr_shyps thy rule vs vs2
- (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
+ (Proof_Rewrite_Rules.un_hhf_proof rlz' (attach_typeS rlz)
(fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
end;
--- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Oct 11 22:06:49 2019 +0200
@@ -10,7 +10,7 @@
val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
end;
-structure RewriteHOLProof : REWRITE_HOL_PROOF =
+structure Rewrite_HOL_Proof : REWRITE_HOL_PROOF =
struct
val rews =
--- a/src/Pure/Isar/isar_cmd.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Oct 11 22:06:49 2019 +0200
@@ -250,7 +250,7 @@
| SOME srcs =>
let
val ctxt = Toplevel.context_of state;
- val pretty_proof = Proof_Syntax.pretty_clean_proof_of ctxt full;
+ val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full;
in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
fun string_of_prop ctxt s =
--- a/src/Pure/PIDE/xml.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/PIDE/xml.ML Fri Oct 11 22:06:49 2019 +0200
@@ -11,6 +11,7 @@
type 'a A
type 'a T
type 'a V
+ type 'a P
val int_atom: int A
val bool_atom: bool A
val unit_atom: unit A
@@ -290,6 +291,7 @@
type 'a A = 'a -> string;
type 'a T = 'a -> body;
type 'a V = 'a -> string list * body;
+type 'a P = 'a -> string list;
(* atomic values *)
@@ -347,6 +349,7 @@
type 'a A = string -> 'a;
type 'a T = body -> 'a;
type 'a V = string list * body -> 'a;
+type 'a P = string list -> 'a;
(* atomic values *)
--- a/src/Pure/PIDE/xml.scala Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/PIDE/xml.scala Fri Oct 11 22:06:49 2019 +0200
@@ -241,6 +241,7 @@
{
type T[A] = A => XML.Body
type V[A] = PartialFunction[A, (List[String], XML.Body)]
+ type P[A] = PartialFunction[A, List[String]]
/* atomic values */
@@ -309,6 +310,7 @@
{
type T[A] = XML.Body => A
type V[A] = (List[String], XML.Body) => A
+ type P[A] = PartialFunction[List[String], A]
/* atomic values */
--- a/src/Pure/Proof/extraction.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Oct 11 22:06:49 2019 +0200
@@ -177,7 +177,7 @@
let
val (oracles, thms) =
([prf], ([], [])) |-> Proofterm.fold_proof_atoms false
- (fn Oracle (name, prop, _) => apfst (cons (name, prop))
+ (fn Oracle (name, prop, _) => apfst (cons (name, SOME prop))
| PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
| _ => I);
val body =
@@ -505,7 +505,7 @@
val rtypes = map fst types;
val typroc = typeof_proc [];
val prep = the_default (K I) prep thy' o
- ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
+ Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
Proofterm.expand_proof thy' (map (rpair NONE) ("" :: expand));
val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
@@ -529,7 +529,7 @@
Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye;
fun mk_sprfs cs tye = maps (fn (_, T) =>
- ProofRewriteRules.mk_of_sort_proof thy' (map SOME cs)
+ Proof_Rewrite_Rules.expand_of_sort_proof thy' (map SOME cs)
(T, Sign.defaultS thy)) tye;
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
--- a/src/Pure/Proof/proof_checker.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/proof_checker.ML Fri Oct 11 22:06:49 2019 +0200
@@ -137,6 +137,13 @@
| thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t)
+ | thm_of _ _ (OfClass (T, c)) =
+ if Sign.of_sort thy (T, [c])
+ then Thm.of_class (Thm.global_ctyp_of thy T, c)
+ else
+ error ("thm_of_proof: bad OfClass proof " ^
+ Syntax.string_of_term_global thy (Logic.mk_of_class (T, c)))
+
| thm_of _ _ _ = error "thm_of_proof: partial proof term";
in beta_eta_convert (thm_of ([], prf_names) [] prf) end
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Oct 11 22:06:49 2019 +0200
@@ -14,12 +14,13 @@
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
- val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+ val expand_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list
+ val expand_of_class_proof : theory -> term option list -> typ * class -> proof
val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof ->
(Proofterm.proof * Proofterm.proof) option
end;
-structure ProofRewriteRules : PROOF_REWRITE_RULES =
+structure Proof_Rewrite_Rules : PROOF_REWRITE_RULES =
struct
fun rew b _ _ =
@@ -255,20 +256,22 @@
val defs' = map (Logic.dest_equals o
map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
val defnames = map Thm.derivation_name defs;
- val f = if not r then I else
- let
- val cnames = map (fst o dest_Const o fst) defs';
- val thms = Proofterm.fold_proof_atoms true
- (fn PThm ({name, prop, ...}, _) =>
- if member (op =) defnames name orelse
- not (exists_Const (member (op =) cnames o #1) prop)
- then I
- else cons (name, SOME prop)
- | _ => I) [prf] [];
- in Proofterm.expand_proof thy thms end;
+ val prf' =
+ if r then
+ let
+ val cnames = map (fst o dest_Const o fst) defs';
+ val thms = Proofterm.fold_proof_atoms true
+ (fn PThm ({name, prop, ...}, _) =>
+ if member (op =) defnames name orelse
+ not (exists_Const (member (op =) cnames o #1) prop)
+ then I
+ else cons (name, SOME prop)
+ | _ => I) [prf] [];
+ in Proofterm.expand_proof thy thms prf end
+ else prf;
in
rewrite_terms (Pattern.rewrite_term thy defs' [])
- (fst (insert_refl defnames [] (f prf)))
+ (fst (insert_refl defnames [] prf'))
end;
@@ -340,33 +343,35 @@
(**** expand OfClass proofs ****)
-fun mk_of_sort_proof thy hs (T, S) =
+fun expand_of_sort_proof thy hyps (T, S) =
let
- val hs' = map
- (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
- | NONE => NONE) hs;
- val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
+ val of_class_hyps = map (fn SOME t => try Logic.dest_of_class t | NONE => NONE) hyps;
+ fun of_class_index p =
+ (case find_index (fn SOME h => h = p | NONE => false) of_class_hyps of
+ ~1 => raise Fail "expand_of_class_proof: missing class hypothesis"
+ | i => PBound i);
+
+ val sorts = AList.coalesce (op =) (rev (map_filter I of_class_hyps));
fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
val subst = map_atyps
- (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
- | T as TFree (s, _) => TFree (s, get_sort T));
- fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
- ~1 => error "expand_of_class: missing class hypothesis"
- | i => PBound i;
- fun reconstruct prf prop = prf |>
- Proofterm.reconstruct_proof thy prop |>
- Proofterm.expand_proof thy [("", NONE)] |>
- Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
+ (fn T as TVar (ai, _) => TVar (ai, get_sort T)
+ | T as TFree (a, _) => TFree (a, get_sort T));
+
+ fun reconstruct prop =
+ Proofterm.reconstruct_proof thy prop #>
+ Proofterm.expand_proof thy [("", NONE)] #>
+ Same.commit (Proofterm.map_proof_same Same.same Same.same of_class_index);
in
- map2 reconstruct
+ map2 reconstruct (Logic.mk_of_sort (T, S))
(Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.classrel_proof thy) (Thm.arity_proof thy)
(OfClass o apfst Type.strip_sorts) (subst T, S))
- (Logic.mk_of_sort (T, S))
end;
-fun expand_of_class thy Ts hs (OfClass (T, c)) =
- mk_of_sort_proof thy hs (T, [c]) |>
- hd |> rpair Proofterm.no_skel |> SOME
- | expand_of_class thy Ts hs _ = NONE;
+fun expand_of_class_proof thy hyps (T, c) =
+ hd (expand_of_sort_proof thy hyps (T, [c]));
+
+fun expand_of_class thy (_: typ list) hyps (OfClass (T, c)) =
+ SOME (expand_of_class_proof thy hyps (T, c), Proofterm.no_skel)
+ | expand_of_class _ _ _ _ = NONE;
end;
--- a/src/Pure/Proof/proof_syntax.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Fri Oct 11 22:06:49 2019 +0200
@@ -13,7 +13,7 @@
val proof_syntax: Proofterm.proof -> theory -> theory
val proof_of: bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
- val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
+ val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
structure Proof_Syntax : PROOF_SYNTAX =
@@ -195,7 +195,7 @@
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
(Proofterm.term_of_proof prf);
-fun pretty_clean_proof_of ctxt full thm =
- pretty_proof ctxt (Thm.clean_proof_of full thm);
+fun pretty_standard_proof_of ctxt full thm =
+ pretty_proof ctxt (Thm.standard_proof_of full thm);
end;
--- a/src/Pure/Thy/document_antiquotations.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Oct 11 22:06:49 2019 +0200
@@ -57,7 +57,7 @@
let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
in Pretty.str (Proof_Context.extern_type ctxt name) end;
-fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
+fun pretty_prf full ctxt = Proof_Syntax.pretty_standard_proof_of ctxt full;
fun pretty_theory ctxt (name, pos) =
(Theory.check {long = true} ctxt (name, pos); Pretty.str name);
--- a/src/Pure/Thy/export_theory.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML Fri Oct 11 22:06:49 2019 +0200
@@ -271,7 +271,7 @@
in
(prop, (deps, proof)) |>
let open XML.Encode Term_XML.Encode
- in pair encode_prop (pair (list string) (option (Proofterm.encode_full consts))) end
+ in pair encode_prop (pair (list string) (option (Proofterm.encode_standard consts))) end
end;
fun buffer_export_thm (serial, thm_name) =
--- a/src/Pure/Thy/thm_deps.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML Fri Oct 11 22:06:49 2019 +0200
@@ -105,7 +105,7 @@
val used =
Proofterm.fold_body_thms
(fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
- (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
+ (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
Symtab.empty;
fun is_unused a = not (Symtab.defined used a);
--- a/src/Pure/logic.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/logic.ML Fri Oct 11 22:06:49 2019 +0200
@@ -62,7 +62,6 @@
constraints_map: (sort * typ) list,
atyp_map: typ -> typ,
map_atyps: typ -> typ,
- map_atyps': typ -> typ,
constraints: ((typ * class) * term) list,
outer_constraints: (typ * class) list};
val unconstrainT: sort list -> term -> unconstrain_context * term
@@ -355,7 +354,6 @@
constraints_map: (sort * typ) list,
atyp_map: typ -> typ,
map_atyps: typ -> typ,
- map_atyps': typ -> typ,
constraints: ((typ * class) * term) list,
outer_constraints: (typ * class) list};
@@ -373,9 +371,6 @@
map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
- val present_map' = map (fn (T, T') => (Type.strip_sorts T', T)) present_map;
- val constraints_map' = map (fn (S, T') => (Type.strip_sorts T', dummy_tfree S)) constraints_map;
-
fun atyp_map T =
(case AList.lookup (op =) present_map T of
SOME U => U
@@ -384,16 +379,7 @@
SOME U => U
| NONE => raise TYPE ("Dangling type variable ", [T], [prop])));
- fun atyp_map' T =
- (case AList.lookup (op =) present_map' T of
- SOME U => U
- | NONE =>
- (case AList.lookup (op =) constraints_map' T of
- SOME U => U
- | NONE => raise TYPE ("Dangling type variable", [T], [prop])));
-
val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
- val map_atyps' = Term.map_atyps atyp_map';
val constraints =
constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
@@ -407,7 +393,6 @@
constraints_map = constraints_map,
atyp_map = atyp_map,
map_atyps = map_atyps,
- map_atyps' = map_atyps',
constraints = constraints,
outer_constraints = outer_constraints};
val prop' = prop
--- a/src/Pure/more_thm.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/more_thm.ML Fri Oct 11 22:06:49 2019 +0200
@@ -114,7 +114,7 @@
val untag: string -> attribute
val kind: string -> attribute
val reconstruct_proof_of: thm -> Proofterm.proof
- val clean_proof_of: bool -> thm -> Proofterm.proof
+ val standard_proof_of: bool -> thm -> Proofterm.proof
val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
val show_consts: bool Config.T
@@ -656,16 +656,10 @@
fun reconstruct_proof_of thm =
Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-fun clean_proof_of full thm =
- let
- val thy = Thm.theory_of_thm thm;
- val (_, prop) =
- Logic.unconstrainT (Thm.shyps_of thm)
- (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
- in
- Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
- |> Proofterm.reconstruct_proof thy prop
- |> Proofterm.expand_proof thy [("", NONE)]
+fun standard_proof_of full thm =
+ let val thy = Thm.theory_of_thm thm in
+ reconstruct_proof_of thm
+ |> Proofterm.expand_proof thy [("", NONE), (Thm.raw_derivation_name thm, NONE)]
|> Proofterm.rew_proof thy
|> Proofterm.no_thm_proofs
|> not full ? Proofterm.shrink_proof
--- a/src/Pure/proofterm.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/proofterm.ML Fri Oct 11 22:06:49 2019 +0200
@@ -23,7 +23,7 @@
| Hyp of term
| PAxm of string * term * typ list option
| OfClass of typ * class
- | Oracle of string * term option * typ list option
+ | Oracle of string * term * typ list option
| PThm of thm_header * thm_body
and proof_body = PBody of
{oracles: (string * term option) Ord_List.T,
@@ -61,7 +61,7 @@
val encode: Consts.T -> proof XML.Encode.T
val encode_body: Consts.T -> proof_body XML.Encode.T
- val encode_full: Consts.T -> proof XML.Encode.T
+ val encode_standard: Consts.T -> proof XML.Encode.T
val decode: Consts.T -> proof XML.Decode.T
val decode_body: Consts.T -> proof_body XML.Decode.T
@@ -77,7 +77,7 @@
val proof_combP: proof * proof list -> proof
val strip_combt: proof -> proof * term option list
val strip_combP: proof -> proof * proof list
- val strip_thm: proof_body -> proof_body
+ val strip_thm_body: proof_body -> proof_body
val map_proof_same: term Same.operation -> typ Same.operation
-> (typ * class -> proof) -> proof Same.operation
val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
@@ -103,21 +103,22 @@
val term_of_proof: proof -> term
(*proof terms for specific inference rules*)
+ val trivial_proof: proof
val implies_intr_proof: term -> proof -> proof
val implies_intr_proof': term -> proof -> proof
val forall_intr_proof: string * term -> typ option -> proof -> proof
val forall_intr_proof': term -> proof -> proof
val varify_proof: term -> (string * sort) list -> proof -> proof
val legacy_freezeT: term -> proof -> proof
- val rotate_proof: term list -> term -> int -> proof -> proof
+ val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
val permute_prems_proof: term list -> int -> int -> proof -> proof
- val generalize: string list * string list -> int -> proof -> proof
+ val generalize_proof: string list * string list -> int -> term -> proof -> proof
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-> proof -> proof
val lift_proof: term -> int -> term -> proof -> proof
val incr_indexes: int -> proof -> proof
val assumption_proof: term list -> term -> int -> proof -> proof
- val bicompose_proof: bool -> term list -> term list -> term list -> term option ->
+ val bicompose_proof: bool -> term list -> term list -> term option -> term list ->
int -> int -> proof -> proof -> proof
val equality_axms: (string * term) list
val reflexive_axm: proof
@@ -141,7 +142,7 @@
(string * class list list * class -> proof) ->
(typ * class -> proof) -> typ * sort -> proof list
val axm_proof: string -> term -> proof
- val oracle_proof: string -> term -> oracle * proof
+ val oracle_proof: string -> term -> proof
val shrink_proof: proof -> proof
(*rewriting on proof terms*)
@@ -196,7 +197,7 @@
| Hyp of term
| PAxm of string * term * typ list option
| OfClass of typ * class
- | Oracle of string * term option * typ list option
+ | Oracle of string * term * typ list option
| PThm of thm_header * thm_body
and proof_body = PBody of
{oracles: (string * term option) Ord_List.T,
@@ -210,7 +211,6 @@
type oracle = string * term option;
val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
-val oracle_prop = the_default Term.dummy;
type thm = serial * thm_node;
val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
@@ -337,7 +337,7 @@
fn Hyp a => ([], term consts a),
fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
fn OfClass (a, b) => ([b], typ a),
- fn Oracle (a, b, c) => ([a], pair (option (term consts)) (option (list typ)) (b, c)),
+ fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
([int_atom serial, theory_name, name],
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
@@ -350,17 +350,17 @@
(a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
(Future.join (thm_node_body thm_node))))));
-fun full_proof consts prf = prf |> variant
+fun standard_proof consts prf = prf |> variant
[fn MinProof => ([], []),
fn PBound a => ([int_atom a], []),
- fn Abst (a, SOME b, c) => ([a], pair typ (full_proof consts) (b, c)),
- fn AbsP (a, SOME b, c) => ([a], pair (term consts) (full_proof consts) (b, c)),
- fn a % SOME b => ([], pair (full_proof consts) (term consts) (a, b)),
- fn a %% b => ([], pair (full_proof consts) (full_proof consts) (a, b)),
+ fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
+ fn AbsP (a, SOME b, c) => ([a], pair (term consts) (standard_proof consts) (b, c)),
+ fn a % SOME b => ([], pair (standard_proof consts) (term consts) (a, b)),
+ fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
fn Hyp a => ([], term consts a),
fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
fn OfClass (T, c) => ([c], typ T),
- fn Oracle (name, prop, SOME Ts) => ([name], pair (option (term consts)) (list typ) (prop, Ts)),
+ fn Oracle (name, prop, SOME Ts) => ([name], pair (term consts) (list typ) (prop, Ts)),
fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
([int_atom serial, theory_name, name], list typ Ts)];
@@ -368,7 +368,7 @@
val encode = proof;
val encode_body = proof_body;
-val encode_full = full_proof;
+val encode_standard = standard_proof;
end;
@@ -389,8 +389,7 @@
fn ([], a) => Hyp (term consts a),
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
fn ([b], a) => OfClass (typ a, b),
- fn ([a], b) =>
- let val (c, d) = pair (option (term consts)) (option (list typ)) b in Oracle (a, c, d) end,
+ fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
fn ([a, b, c], d) =>
let
val ((e, (f, (g, h)))) =
@@ -450,13 +449,13 @@
| stripc x = x
in stripc (prf, []) end;
-fun strip_thm (body as PBody {proof, ...}) =
+fun strip_thm_body (body as PBody {proof, ...}) =
(case fst (strip_combt (fst (strip_combP proof))) of
PThm (_, Thm_Body {body = body', ...}) => Future.join body'
| _ => body);
-val mk_Abst = fold_rev (fn (s, _: typ) => fn prf => Abst (s, NONE, prf));
-fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
+val mk_Abst = fold_rev (fn (x, _: typ) => fn prf => Abst (x, NONE, prf));
+val mk_AbsP = fold_rev (fn _: term => fn prf => AbsP ("H", NONE, prf));
fun map_proof_same term typ ofclass =
let
@@ -832,7 +831,7 @@
val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
| term_of _ (Hyp t) = Hypt $ t
- | term_of _ (Oracle (_, t, _)) = Oraclet $ oracle_prop t
+ | term_of _ (Oracle (_, t, _)) = Oraclet $ t
| term_of _ MinProof = MinProoft;
in
@@ -845,6 +844,11 @@
(** inference rules **)
+(* trivial implication *)
+
+val trivial_proof = AbsP ("H", NONE, PBound 0);
+
+
(* implication introduction *)
fun gen_implies_intr_proof f h prf =
@@ -921,35 +925,44 @@
(* rotate assumptions *)
-fun rotate_proof Bs Bi m prf =
+fun rotate_proof Bs Bi' params asms m prf =
let
- val params = Term.strip_all_vars Bi;
- val asms = Logic.strip_imp_prems (Term.strip_all_body Bi);
val i = length asms;
val j = length Bs;
in
- mk_AbsP (j+1, proof_combP (prf, map PBound
- (j downto 1) @ [mk_Abst params (mk_AbsP (i,
- proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
+ mk_AbsP (Bs @ [Bi']) (proof_combP (prf, map PBound
+ (j downto 1) @ [mk_Abst params (mk_AbsP asms
+ (proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
end;
(* permute premises *)
-fun permute_prems_proof prems j k prf =
- let val n = length prems
- in mk_AbsP (n, proof_combP (prf,
- map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+fun permute_prems_proof prems' j k prf =
+ let val n = length prems' in
+ mk_AbsP prems'
+ (proof_combP (prf, map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
end;
(* generalization *)
-fun generalize (tfrees, frees) idx =
- Same.commit (map_proof_terms_same
- (Term_Subst.generalize_same (tfrees, frees) idx)
- (Term_Subst.generalizeT_same tfrees idx));
+fun generalize_proof (tfrees, frees) idx prop prf =
+ let
+ val gen =
+ if null frees then []
+ else
+ fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T) | _ => I)
+ (Term_Subst.generalize (tfrees, []) idx prop) [];
+ in
+ prf
+ |> Same.commit (map_proof_terms_same
+ (Term_Subst.generalize_same (tfrees, []) idx)
+ (Term_Subst.generalizeT_same tfrees idx))
+ |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
+ |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen
+ end;
(* instantiation *)
@@ -1003,7 +1016,7 @@
map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
(i + k - 1 downto i));
in
- mk_AbsP (k, lift [] [] 0 0 Bi)
+ mk_AbsP ps (lift [] [] 0 0 Bi)
end;
fun incr_indexes i =
@@ -1023,8 +1036,7 @@
in all_prf t end;
fun assumption_proof Bs Bi n prf =
- mk_AbsP (length Bs, proof_combP (prf,
- map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
+ mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
(* composition of object rule with proof state *)
@@ -1036,12 +1048,12 @@
| flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
-fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf =
+fun bicompose_proof flatten Bs As A oldAs n m rprf sprf =
let
- val la = length newAs;
val lb = length Bs;
+ val la = length As;
in
- mk_AbsP (lb+la, proof_combP (sprf,
+ mk_AbsP (Bs @ As) (proof_combP (sprf,
map PBound (lb + la - 1 downto la)) %%
proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @
map (if flatten then flatten_params_proof 0 0 n else PBound o snd)
@@ -1146,13 +1158,15 @@
val frees = map SOME (frees_of prop);
in vars @ frees end;
-fun axm_proof name prop =
- proof_combt' (PAxm (name, prop, NONE), prop_args prop);
+fun const_proof mk name prop =
+ let
+ val args = prop_args prop;
+ val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop;
+ val head = mk (name, prop1, NONE);
+ in proof_combP (proof_combt' (head, args), map OfClass outer_constraints) end;
-fun oracle_proof name prop =
- if ! proofs = 0
- then ((name, NONE), Oracle (name, NONE, NONE))
- else ((name, SOME prop), proof_combt' (Oracle (name, SOME prop, NONE), prop_args prop));
+val axm_proof = const_proof PAxm;
+val oracle_proof = const_proof Oracle;
val shrink_proof =
let
@@ -1191,7 +1205,7 @@
val prop =
(case prf of
PAxm (_, prop, _) => prop
- | Oracle (_, prop, _) => oracle_prop prop
+ | Oracle (_, prop, _) => prop
| PThm ({prop, ...}, _) => prop
| _ => raise Fail "shrink: proof not in normal form");
val vs = vars_of prop;
@@ -1786,7 +1800,7 @@
| 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 (oracle_prop prop) opTs prf
+ mk_cnstrts_atom env vTs prop opTs prf
| mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
| mk_cnstrts _ _ _ _ MinProof = raise MIN_PROOF ()
in mk_cnstrts env [] [] Symtab.empty cprf end;
@@ -1882,7 +1896,7 @@
| prop_of0 _ (PThm ({prop, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts
| prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
| prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c)
- | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom (oracle_prop prop) Ts
+ | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
| prop_of0 _ _ = error "prop_of: partial proof object";
val prop_of' = Envir.beta_eta_contract oo prop_of0;
@@ -1893,45 +1907,45 @@
fun expand_proof thy thms prf =
let
- fun expand maxidx prfs (AbsP (s, t, prf)) =
- let val (maxidx', prfs', prf') = expand maxidx prfs prf
- in (maxidx', prfs', AbsP (s, t, prf')) end
- | expand maxidx prfs (Abst (s, T, prf)) =
- let val (maxidx', prfs', prf') = expand maxidx prfs prf
- in (maxidx', prfs', Abst (s, T, prf')) end
- | expand maxidx prfs (prf1 %% prf2) =
- let
- val (maxidx', prfs', prf1') = expand maxidx prfs prf1;
- val (maxidx'', prfs'', prf2') = expand maxidx' prfs' prf2;
- in (maxidx'', prfs'', prf1' %% prf2') end
- | expand maxidx prfs (prf % t) =
- let val (maxidx', prfs', prf') = expand maxidx prfs prf
- in (maxidx', prfs', prf' % t) end
- | expand maxidx prfs (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) =
- if not (exists
- (fn (b, NONE) => a = b
- | (b, SOME prop') => a = b andalso prop = prop') thms)
- then (maxidx, prfs, prf) else
+ fun do_expand a prop =
+ exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms;
+
+ fun expand seen maxidx (AbsP (s, t, prf)) =
+ let val (seen', maxidx', prf') = expand seen maxidx prf
+ in (seen', maxidx', AbsP (s, t, prf')) end
+ | expand seen maxidx (Abst (s, T, prf)) =
+ let val (seen', maxidx', prf') = expand seen maxidx prf
+ in (seen', maxidx', Abst (s, T, prf')) end
+ | expand seen maxidx (prf1 %% prf2) =
let
- val (maxidx', prf, prfs') =
- (case AList.lookup (op =) prfs (a, prop) of
- NONE =>
- let
- val prf' =
- thm_body_proof_open thm_body
- |> reconstruct_proof thy prop
- |> forall_intr_vfs_prf prop;
- val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf'
- in
- (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
- ((a, prop), (maxidx', prf)) :: prfs')
- end
- | SOME (maxidx', prf) =>
- (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs));
- in (maxidx', prfs', app_types (maxidx + 1) prop Ts prf) end
- | expand maxidx prfs prf = (maxidx, prfs, prf);
+ val (seen', maxidx', prf1') = expand seen maxidx prf1;
+ val (seen'', maxidx'', prf2') = expand seen' maxidx' prf2;
+ in (seen'', maxidx'', prf1' %% prf2') end
+ | expand seen maxidx (prf % t) =
+ let val (seen', maxidx', prf') = expand seen maxidx prf
+ in (seen', maxidx', prf' % t) end
+ | expand seen maxidx (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) =
+ if do_expand a prop then
+ let
+ val (seen', maxidx', prf') =
+ (case AList.lookup (op =) seen (a, prop) of
+ NONE =>
+ let
+ val prf1 =
+ thm_body_proof_open thm_body
+ |> reconstruct_proof thy prop
+ |> forall_intr_vfs_prf prop;
+ val (seen1, maxidx1, prf2) = expand_init seen prf1
+ val seen2 = ((a, prop), (maxidx1, prf2)) :: seen1;
+ in (seen2, maxidx1, prf2) end
+ | SOME (maxidx1, prf1) => (seen, maxidx1, prf1));
+ val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop Ts;
+ in (seen', maxidx' + maxidx + 1, prf'') end
+ else (seen, maxidx, prf)
+ | expand seen maxidx prf = (seen, maxidx, prf)
+ and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf;
- in #3 (expand (maxidx_proof prf ~1) [] prf) end;
+ in #3 (expand_init [] prf) end;
end;
@@ -2068,7 +2082,7 @@
val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext);
fun ofclass (ty, c) =
let val ty' = Term.map_atyps (#atyp_map ucontext) ty;
- in the_single (of_sort_proof algebra classrel_proof arity_proof hyp_map (ty', [c])) end;
+ in the_single (of_sort_proof algebra classrel_proof arity_proof hyp_map (ty', [c])) end;
in
Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
#> fold_rev (implies_intr_proof o snd) (#constraints ucontext)
@@ -2078,7 +2092,7 @@
fun encode_export consts prop prf =
let open XML.Encode Term_XML.Encode
- in pair (term consts) (encode_full consts) (prop, prf) end;
+ in pair (term consts) (encode_standard consts) (prop, prf) end;
fun export_proof thy i prop prf =
let
--- a/src/Pure/term.scala Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/term.scala Fri Oct 11 22:06:49 2019 +0200
@@ -57,7 +57,7 @@
case class Hyp(hyp: Term) extends Proof
case class PAxm(name: String, types: List[Typ]) extends Proof
case class OfClass(typ: Typ, cls: String) extends Proof
- case class Oracle(name: String, prop: Option[Term], types: List[Typ]) extends Proof
+ case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
case class PThm(serial: Long, theory_name: String, approximative_name: String, types: List[Typ])
extends Proof
@@ -153,7 +153,7 @@
case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
case Oracle(name, prop, types) =>
- store(Oracle(cache_string(name), prop.map(cache_term(_)), cache_typs(types)))
+ store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
case PThm(serial, theory_name, name, types) =>
store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
}
--- a/src/Pure/term_xml.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/term_xml.ML Fri Oct 11 22:06:49 2019 +0200
@@ -7,10 +7,13 @@
signature TERM_XML_OPS =
sig
type 'a T
+ type 'a P
+ val indexname: indexname P
val sort: sort T
+ val typ_raw: typ T
+ val term_raw: term T
val typ: typ T
val term: Consts.T -> term T
- val term_raw: term T
end
signature TERM_XML =
@@ -27,29 +30,33 @@
open XML.Encode;
+fun indexname (a, b) = if b = 0 then [a] else [a, int_atom b];
+
val sort = list string;
-fun typ T = T |> variant
- [fn Type (a, b) => ([a], list typ b),
+fun typ_raw T = T |> variant
+ [fn Type (a, b) => ([a], list typ_raw b),
fn TFree (a, b) => ([a], sort b),
- fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
+ fn TVar (a, b) => (indexname a, sort b)];
+
+fun term_raw t = t |> variant
+ [fn Const (a, b) => ([a], typ_raw b),
+ fn Free (a, b) => ([a], typ_raw b),
+ fn Var (a, b) => (indexname a, typ_raw b),
+ fn Bound a => ([int_atom a], []),
+ fn Abs (a, b, c) => ([a], pair typ_raw term_raw (b, c)),
+ fn op $ a => ([], pair term_raw term_raw a)];
+
+fun typ T = option typ_raw (if T = dummyT then NONE else SOME T);
fun term consts t = t |> variant
[fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
fn Free (a, b) => ([a], typ b),
- fn Var ((a, b), c) => ([a, int_atom b], typ c),
+ fn Var (a, b) => (indexname a, typ b),
fn Bound a => ([int_atom a], []),
fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
fn op $ a => ([], pair (term consts) (term consts) a)];
-fun term_raw t = t |> variant
- [fn Const (a, b) => ([a], typ b),
- fn Free (a, b) => ([a], typ b),
- fn Var ((a, b), c) => ([a, int_atom b], typ c),
- fn Bound a => ([int_atom a], []),
- fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
- fn op $ a => ([], pair term_raw term_raw a)];
-
end;
structure Decode =
@@ -57,29 +64,34 @@
open XML.Decode;
+fun indexname [a] = (a, 0)
+ | indexname [a, b] = (a, int_atom b);
+
val sort = list string;
-fun typ T = T |> variant
- [fn ([a], b) => Type (a, list typ b),
+fun typ_raw body = body |> variant
+ [fn ([a], b) => Type (a, list typ_raw b),
fn ([a], b) => TFree (a, sort b),
- fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
+ fn (a, b) => TVar (indexname a, sort b)];
-fun term consts t = t |> variant
+fun term_raw body = body |> variant
+ [fn ([a], b) => Const (a, typ_raw b),
+ fn ([a], b) => Free (a, typ_raw b),
+ fn (a, b) => Var (indexname a, typ_raw b),
+ fn ([a], []) => Bound (int_atom a),
+ fn ([a], b) => let val (c, d) = pair typ_raw term_raw b in Abs (a, c, d) end,
+ fn ([], a) => op $ (pair term_raw term_raw a)];
+
+val typ = option typ_raw #> the_default dummyT;
+
+fun term consts body = body |> variant
[fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
fn ([a], b) => Free (a, typ b),
- fn ([a, b], c) => Var ((a, int_atom b), typ c),
+ fn (a, b) => Var (indexname a, typ b),
fn ([a], []) => Bound (int_atom a),
fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
fn ([], a) => op $ (pair (term consts) (term consts) a)];
-fun term_raw t = t |> variant
- [fn ([a], b) => Const (a, typ b),
- fn ([a], b) => Free (a, typ b),
- fn ([a, b], c) => Var ((a, int_atom b), typ c),
- fn ([a], []) => Bound (int_atom a),
- fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
- fn ([], a) => op $ (pair term_raw term_raw a)];
-
end;
end;
--- a/src/Pure/term_xml.scala Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/term_xml.scala Fri Oct 11 22:06:49 2019 +0200
@@ -15,19 +15,26 @@
{
import XML.Encode._
+ val indexname: P[Indexname] =
+ { case Indexname(a, 0) => List(a)
+ case Indexname(a, b) => List(a, int_atom(b)) }
+
val sort: T[Sort] = list(string)
- def typ: T[Typ] =
+ def typ_raw: T[Typ] =
variant[Typ](List(
- { case Type(a, b) => (List(a), list(typ)(b)) },
+ { case Type(a, b) => (List(a), list(typ_raw)(b)) },
{ case TFree(a, b) => (List(a), sort(b)) },
- { case TVar(Indexname(a, b), c) => (List(a, int_atom(b)), sort(c)) }))
+ { case TVar(a, b) => (indexname(a), sort(b)) }))
+
+ val typ: T[Typ] =
+ { case t => option(typ_raw)(if (t == dummyT) None else Some(t)) }
def term: T[Term] =
variant[Term](List(
{ case Const(a, b) => (List(a), list(typ)(b)) },
{ case Free(a, b) => (List(a), typ(b)) },
- { case Var(Indexname(a, b), c) => (List(a, int_atom(b)), typ(c)) },
+ { case Var(a, b) => (indexname(a), typ(b)) },
{ case Bound(a) => (List(int_atom(a)), Nil) },
{ case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
{ case App(a, b) => (Nil, pair(term, term)(a, b)) }))
@@ -37,19 +44,25 @@
{
import XML.Decode._
+ val indexname: P[Indexname] =
+ { case List(a) => Indexname(a, 0)
+ case List(a, b) => Indexname(a, int_atom(b)) }
+
val sort: T[Sort] = list(string)
- def typ: T[Typ] =
+ def typ_raw: T[Typ] =
variant[Typ](List(
- { case (List(a), b) => Type(a, list(typ)(b)) },
+ { case (List(a), b) => Type(a, list(typ_raw)(b)) },
{ case (List(a), b) => TFree(a, sort(b)) },
- { case (List(a, b), c) => TVar(Indexname(a, int_atom(b)), sort(c)) }))
+ { case (a, b) => TVar(indexname(a), sort(b)) }))
+
+ def typ(body: XML.Body): Typ = option(typ_raw)(body).getOrElse(dummyT)
def term: T[Term] =
variant[Term](List(
{ case (List(a), b) => Const(a, list(typ)(b)) },
{ case (List(a), b) => Free(a, typ(b)) },
- { case (List(a, b), c) => Var(Indexname(a, int_atom(b)), typ(c)) },
+ { case (a, b) => Var(indexname(a), typ(b)) },
{ case (List(a), Nil) => Bound(int_atom(a)) },
{ case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
{ case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
@@ -65,7 +78,7 @@
{ case (Nil, a) => Hyp(term(a)) },
{ case (List(a), b) => PAxm(a, list(typ)(b)) },
{ case (List(a), b) => OfClass(typ(b), a) },
- { case (List(a), b) => val (c, d) = pair(option(term), list(typ))(b); Oracle(a, c, d) },
+ { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
{ case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
}
}
--- a/src/Pure/thm.ML Fri Oct 11 11:08:32 2019 +0200
+++ b/src/Pure/thm.ML Fri Oct 11 22:06:49 2019 +0200
@@ -713,6 +713,9 @@
val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);
+fun bad_proofs i =
+ error ("Illegal level of detail for proof objects: " ^ string_of_int i);
+
fun deriv_rule2 f
(Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
(Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
@@ -725,7 +728,7 @@
2 => f prf1 prf2
| 1 => MinProof
| 0 => MinProof
- | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
+ | i => bad_proofs i);
in make_deriv ps oracles thms prf end;
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
@@ -1043,7 +1046,14 @@
if T <> propT then
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
- let val (oracle, prf) = Proofterm.oracle_proof name prop in
+ let
+ val (oracle, prf) =
+ (case ! Proofterm.proofs of
+ 2 => ((name, SOME prop), Proofterm.oracle_proof name prop)
+ | 1 => ((name, SOME prop), MinProof)
+ | 0 => ((name, NONE), MinProof)
+ | i => bad_proofs i);
+ in
Thm (make_deriv [] [oracle] [] prf,
{cert = Context.join_certificate (Context.Certificate thy', cert2),
tags = [],
@@ -1496,12 +1506,12 @@
val _ = exists bad_term hyps andalso
raise THM ("generalize: variable free in assumptions", 0, [th]);
- val gen = Term_Subst.generalize (tfrees, frees) idx;
- val prop' = gen prop;
- val tpairs' = map (apply2 gen) tpairs;
+ val generalize = Term_Subst.generalize (tfrees, frees) idx;
+ val prop' = generalize prop;
+ val tpairs' = map (apply2 generalize) tpairs;
val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
in
- Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
+ Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der,
{cert = cert,
tags = [],
maxidx = maxidx',
@@ -1631,7 +1641,7 @@
if T <> propT then
raise THM ("trivial: the term must have type prop", 0, [])
else
- Thm (deriv_rule0 (fn () => Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
+ Thm (deriv_rule0 (fn () => Proofterm.trivial_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1828,23 +1838,24 @@
val (context, cert') = make_context_certificate [state] opt_ctxt cert;
val (tpairs, Bs, Bi, C) = dest_state (state, i);
fun newth n (env, tpairs) =
- Thm (deriv_rule1
- ((if Envir.is_empty env then I else Proofterm.norm_proof' env) o
- Proofterm.assumption_proof Bs Bi n) der,
- {tags = [],
- maxidx = Envir.maxidx_of env,
- constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
- shyps = Envir.insert_sorts env shyps,
- hyps = hyps,
- tpairs =
- if Envir.is_empty env then tpairs
- else map (apply2 (Envir.norm_term env)) tpairs,
- prop =
- if Envir.is_empty env then (*avoid wasted normalizations*)
- Logic.list_implies (Bs, C)
- else (*normalize the new rule fully*)
- Envir.norm_term env (Logic.list_implies (Bs, C)),
- cert = cert'});
+ let
+ val normt = Envir.norm_term env;
+ fun assumption_proof prf =
+ Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf;
+ in
+ Thm (deriv_rule1
+ (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der,
+ {tags = [],
+ maxidx = Envir.maxidx_of env,
+ constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
+ shyps = Envir.insert_sorts env shyps,
+ hyps = hyps,
+ tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs,
+ prop =
+ if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*)
+ else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*),
+ cert = cert'})
+ end;
val (close, asms, concl) = Logic.assum_problems (~1, Bi);
val concl' = close concl;
@@ -1898,7 +1909,7 @@
in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
else raise THM ("rotate_rule", k, [state]);
in
- Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
+ Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1923,14 +1934,16 @@
handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
val n_j = length moved_prems;
val m = if k < 0 then n_j + k else k;
- val prop' =
- if 0 = m orelse m = n_j then prop
+ val (prems', prop') =
+ if 0 = m orelse m = n_j then (prems, prop)
else if 0 < m andalso m < n_j then
- let val (ps, qs) = chop m moved_prems
- in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
+ let
+ val (ps, qs) = chop m moved_prems;
+ val prems' = fixed_prems @ qs @ ps;
+ in (prems', Logic.list_implies (prems', concl)) end
else raise THM ("permute_prems: k", k, [rl]);
in
- Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
+ Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -2079,14 +2092,14 @@
val constraints' =
union_constraints constraints1 constraints2
|> insert_constraints_env (Context.certificate_theory cert) env;
+ fun bicompose_proof prf1 prf2 =
+ Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1)
+ prf1 prf2
val th =
Thm (deriv_rule2
- ((if Envir.is_empty env then I
- else if Envir.above env smax then
- (fn f => fn der => f (Proofterm.norm_proof' env der))
- else
- curry op oo (Proofterm.norm_proof' env))
- (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
+ (if Envir.is_empty env then bicompose_proof
+ else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env
+ else Proofterm.norm_proof' env oo bicompose_proof) rder' sder,
{tags = [],
maxidx = Envir.maxidx_of env,
constraints = constraints',