--- a/src/Pure/Proof/extraction.ML Wed Oct 09 18:48:15 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Wed Oct 09 23:00:52 2019 +0200
@@ -116,7 +116,7 @@
in rew end;
-val chtypes = Proofterm.change_types o SOME;
+val change_types = Proofterm.change_types o SOME;
fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
fun corr_name s vs = extr_name s vs ^ "_correctness";
@@ -749,10 +749,10 @@
(Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
val corr_prf' = mkabsp shyps
- (chtypes [] Proofterm.equal_elim_axm %> lhs %> rhs %%
- (chtypes [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
- (chtypes [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
- (chtypes [T --> propT] Proofterm.reflexive_axm %> f) %%
+ (change_types [] Proofterm.equal_elim_axm %> lhs %> rhs %%
+ (change_types [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
+ (change_types [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
+ (change_types [T --> propT] Proofterm.reflexive_axm %> f) %%
PAxm (Thm.def_name cname, eqn,
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Proofterm.prop_of corr_prf';
--- a/src/Pure/Proof/proof_syntax.ML Wed Oct 09 18:48:15 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Wed Oct 09 23:00:52 2019 +0200
@@ -182,12 +182,13 @@
val thy = Thm.theory_of_thm thm;
val prop = Thm.full_prop_of thm;
val prf = Thm.proof_of thm;
- val prf' =
- (case fst (Proofterm.strip_combt (fst (Proofterm.strip_combP prf))) of
- PThm ({prop = prop', ...}, thm_body) =>
- if prop = prop' then Proofterm.thm_body_proof_raw thm_body else prf
- | _ => prf)
- in if full then Proofterm.reconstruct_proof thy prop prf' else prf' end;
+ in
+ (case fst (Proofterm.strip_combt (fst (Proofterm.strip_combP prf))) of
+ PThm ({prop = prop', ...}, thm_body) =>
+ if prop = prop' then Proofterm.thm_body_proof_raw thm_body else prf
+ | _ => prf)
+ |> full ? Proofterm.reconstruct_proof thy prop
+ end;
fun pretty_proof ctxt prf =
Proof_Context.pretty_term_abbrev
--- a/src/Pure/logic.ML Wed Oct 09 18:48:15 2019 +0200
+++ b/src/Pure/logic.ML Wed Oct 09 23:00:52 2019 +0200
@@ -56,11 +56,13 @@
val mk_arities: arity -> term list
val mk_arity: string * sort list * class -> term
val dest_arity: term -> string * sort list * class
+ val dummy_tfree: sort -> typ
type unconstrain_context =
{present_map: (typ * typ) list,
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
@@ -170,6 +172,7 @@
| dest_equals t = raise TERM ("dest_equals", [t]);
+
(** implies **)
val implies = Const ("Pure.imp", propT --> propT --> propT);
@@ -345,11 +348,14 @@
(* internalized sort constraints *)
+fun dummy_tfree S = TFree ("'dummy", S);
+
type unconstrain_context =
{present_map: (typ * typ) list,
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};
@@ -367,28 +373,41 @@
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
| NONE =>
(case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
SOME U => U
- | NONE => raise TYPE ("Dangling type variable", [T], [])));
+ | 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)) =>
map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
val outer_constraints =
- maps (fn (T, S) => map (pair T) S)
- (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
+ maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
- val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
val ucontext =
{present_map = present_map,
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/proofterm.ML Wed Oct 09 18:48:15 2019 +0200
+++ b/src/Pure/proofterm.ML Wed Oct 09 23:00:52 2019 +0200
@@ -105,7 +105,7 @@
(*proof terms for specific inference rules*)
val implies_intr_proof: term -> proof -> proof
val implies_intr_proof': term -> proof -> proof
- val forall_intr_proof: term -> string -> 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
@@ -127,13 +127,13 @@
val equal_elim_axm: proof
val abstract_rule_axm: proof
val combination_axm: proof
- val reflexive: proof
- val symmetric: proof -> proof
- val transitive: term -> typ -> proof -> proof -> proof
- val abstract_rule: term -> string -> proof -> proof
- val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
- val equal_intr: term -> term -> proof -> proof -> proof
- val equal_elim: term -> term -> proof -> proof -> proof
+ val reflexive_proof: proof
+ val symmetric_proof: proof -> proof
+ val transitive_proof: typ -> term -> proof -> proof -> proof
+ val equal_intr_proof: term -> term -> proof -> proof -> proof
+ val equal_elim_proof: term -> term -> proof -> proof -> proof
+ val abstract_rule_proof: string * term -> proof -> proof
+ val combination_proof: typ -> term -> term -> term -> term -> proof -> proof -> proof
val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
sort list -> proof -> proof
val of_sort_proof: Sorts.algebra ->
@@ -626,12 +626,12 @@
fun del_conflicting_tvars envT T = Term_Subst.instantiateT
(map_filter (fn ixnS as (_, S) =>
(Type.lookup envT ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvarsT T [])) T;
+ SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])) T;
fun del_conflicting_vars env t = Term_Subst.instantiate
(map_filter (fn ixnS as (_, S) =>
(Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
+ SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []),
map_filter (fn (ixnT as (_, T)) =>
(Envir.lookup env ixnT; NONE) handle TYPE _ =>
SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
@@ -868,11 +868,11 @@
(* forall introduction *)
-fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
+fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf);
-fun forall_intr_proof' t prf =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in Abst (a, SOME T, prf_abstract_over t prf) end;
+fun forall_intr_proof' v prf =
+ let val (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T))
+ in forall_intr_proof (a, v) (SOME T) prf end;
(* varify *)
@@ -1055,7 +1055,7 @@
fun strip_shyps_proof algebra present witnessed extra_sorts prf =
let
fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
- val extra = map (fn S => (TFree ("'dummy", S), S)) extra_sorts;
+ val extra = map (`Logic.dummy_tfree) extra_sorts;
val replacements = present @ extra @ witnessed;
fun replace T =
if exists (fn (T', _) => T' = T) present then raise Same.SAME
@@ -1078,8 +1078,13 @@
(** axioms and theorems **)
+fun tvars_of t = map TVar (rev (Term.add_tvars t []));
+fun tfrees_of t = map TFree (rev (Term.add_tfrees t []));
+fun type_variables_of t = tvars_of t @ tfrees_of t;
+
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
+fun variables_of t = vars_of t @ frees_of t;
fun test_args _ [] = true
| test_args is (Bound i :: ts) =
@@ -1232,8 +1237,8 @@
("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
("abstract_rule",
Logic.mk_implies
- (Logic.all x
- (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+ (Logic.all x (Logic.mk_equals (f $ x, g $ x)),
+ Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
("combination", Logic.list_implies
([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
@@ -1241,19 +1246,28 @@
equal_elim_axm, abstract_rule_axm, combination_axm] =
map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
-val reflexive = reflexive_axm % NONE;
+val reflexive_proof = reflexive_axm % NONE;
+
+val is_reflexive_proof = fn PAxm ("Pure.reflexive", _, _) % _ => true | _ => false;
-fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf
- | symmetric prf = symmetric_axm % NONE % NONE %% prf;
+fun symmetric_proof prf =
+ if is_reflexive_proof prf then prf
+ else symmetric_axm % NONE % NONE %% prf;
-fun transitive _ _ (PAxm ("Pure.reflexive", _, _) % _) prf2 = prf2
- | transitive _ _ prf1 (PAxm ("Pure.reflexive", _, _) % _) = prf1
- | transitive u (Type ("prop", [])) prf1 prf2 =
- transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2
- | transitive _ _ prf1 prf2 = transitive_axm % NONE % NONE % NONE %% prf1 %% prf2;
+fun transitive_proof U u prf1 prf2 =
+ if is_reflexive_proof prf1 then prf2
+ else if is_reflexive_proof prf2 then prf1
+ else if U = propT then transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2
+ else transitive_axm % NONE % NONE % NONE %% prf1 %% prf2;
-fun abstract_rule x a prf =
- abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf;
+fun equal_intr_proof A B prf1 prf2 =
+ equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
+
+fun equal_elim_proof A B prf1 prf2 =
+ equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
+
+fun abstract_rule_proof (a, x) prf =
+ abstract_rule_axm % NONE % NONE %% forall_intr_proof (a, x) NONE prf;
fun check_comb (PAxm ("Pure.combination", _, _) % f % _ % _ % _ %% prf %% _) =
is_some f orelse check_comb prf
@@ -1262,7 +1276,7 @@
| check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
| check_comb _ = false;
-fun combination f g t u (Type (_, [T, U])) prf1 prf2 =
+fun combination_proof A f g t u prf1 prf2 =
let
val f = Envir.beta_norm f;
val g = Envir.beta_norm g;
@@ -1275,7 +1289,7 @@
combination_axm %> remove_types f % NONE
| _ => combination_axm %> remove_types f %> remove_types g)
in
- (case T of
+ (case A of
Type ("fun", _) => prf %
(case head_of f of
Abs _ => SOME (remove_types t)
@@ -1288,12 +1302,6 @@
| _ => prf % NONE % NONE %% prf1 %% prf2)
end;
-fun equal_intr A B prf1 prf2 =
- equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
-
-fun equal_elim A B prf1 prf2 =
- equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
-
(** rewriting on proof terms **)
@@ -1567,20 +1575,18 @@
exception MIN_PROOF of unit;
-fun vars_of t = map Var (rev (Term.add_vars t []));
-fun frees_of t = map Free (rev (Term.add_frees t []));
-fun variables_of t = vars_of t @ frees_of t;
-
fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop;
fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
fun app_types shift prop Ts prf =
let
- val tvars = rev (Term.add_tvars prop []);
- val tfrees = rev (Term.add_tfrees prop []);
- val vs = map (fn ((a, i), _) => (a, i + shift)) tvars @ map (fn (a, _) => (a, ~1)) tfrees;
- fun varify (v as (a, S)) = if member (op =) tfrees v then TVar ((a, ~1), S) else TFree v;
- in map_proof_types (typ_subst_TVars (vs ~~ Ts) o map_type_tfree varify) prf end;
+ val inst = type_variables_of prop ~~ Ts;
+ fun subst_same A =
+ (case AList.lookup (op =) inst A of SOME T => T | NONE => raise Same.SAME);
+ val subst_type_same =
+ Term_Subst.map_atypsT_same
+ (fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A);
+ in Same.commit (map_proof_types_same subst_type_same) prf end;
fun guess_name (PThm ({name, ...}, _)) = name
| guess_name (prf %% Hyp _) = guess_name prf
@@ -1856,9 +1862,8 @@
val env' = solve thy cs' env
in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof;
-fun prop_of_atom prop Ts = subst_atomic_types
- (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
- (forall_intr_vfs prop);
+fun prop_of_atom prop Ts =
+ subst_atomic_types (type_variables_of prop ~~ Ts) (forall_intr_vfs prop);
val head_norm = Envir.head_norm Envir.init;
--- a/src/Pure/thm.ML Wed Oct 09 18:48:15 2019 +0200
+++ b/src/Pure/thm.ML Wed Oct 09 23:00:52 2019 +0200
@@ -729,7 +729,10 @@
in make_deriv ps oracles thms prf end;
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
-fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
+
+fun deriv_rule0 make_prf =
+ if ! Proofterm.proofs <= 1 then empty_deriv
+ else deriv_rule1 I (make_deriv [] [] [] (make_prf ()));
fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
make_deriv promises oracles thms (f proof);
@@ -803,7 +806,7 @@
Name_Space.lookup (Theory.axiom_table thy) name
|> Option.map (fn prop =>
let
- val der = deriv_rule0 (Proofterm.axm_proof name prop);
+ val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop);
val cert = Context.Certificate thy;
val maxidx = maxidx_of_term prop;
val shyps = Sorts.insert_term prop [];
@@ -1078,7 +1081,7 @@
raise THM ("assume: prop", 0, [])
else if maxidx <> ~1 then
raise THM ("assume: variables", maxidx, [])
- else Thm (deriv_rule0 (Proofterm.Hyp prop),
+ else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop),
{cert = cert,
tags = [],
maxidx = ~1,
@@ -1154,7 +1157,7 @@
(th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) =
let
fun result a =
- Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
+ Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der,
{cert = join_certificate1 (ct, th),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1205,7 +1208,7 @@
t \<equiv> t
*)
fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
- Thm (deriv_rule0 Proofterm.reflexive,
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1223,7 +1226,7 @@
fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
(case prop of
(eq as Const ("Pure.eq", _)) $ t $ u =>
- Thm (deriv_rule1 Proofterm.symmetric der,
+ Thm (deriv_rule1 Proofterm.symmetric_proof der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1248,10 +1251,10 @@
fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
in
case (prop1, prop2) of
- ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
+ ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
if not (u aconv u') then err "middle term"
else
- Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
+ Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1274,7 +1277,7 @@
(case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
| _ => raise THM ("beta_conversion: not a redex", 0, []));
in
- Thm (deriv_rule0 Proofterm.reflexive,
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1286,7 +1289,7 @@
end;
fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
- Thm (deriv_rule0 Proofterm.reflexive,
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1297,7 +1300,7 @@
prop = Logic.mk_equals (t, Envir.eta_contract t)});
fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
- Thm (deriv_rule0 Proofterm.reflexive,
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1320,7 +1323,7 @@
val (t, u) = Logic.dest_equals prop
handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
val result =
- Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,
+ Thm (deriv_rule1 (Proofterm.abstract_rule_proof (a, x)) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1364,7 +1367,7 @@
(Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
(chktypes fT tT;
- Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
+ Thm (deriv_rule2 (Proofterm.combination_proof (domain_type fT) f g t u) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1392,7 +1395,7 @@
(case (prop1, prop2) of
(Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
if A aconv A' andalso B aconv B' then
- Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
+ Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1421,7 +1424,7 @@
(case prop1 of
Const ("Pure.eq", _) $ A $ B =>
if prop2 aconv A then
- Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
+ Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1628,7 +1631,7 @@
if T <> propT then
raise THM ("trivial: the term must have type prop", 0, [])
else
- Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
+ Thm (deriv_rule0 (fn () => Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1652,7 +1655,7 @@
val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c));
in
if Sign.of_sort thy (T, [c]) then
- Thm (deriv_rule0 (Proofterm.OfClass (T, c)),
+ Thm (deriv_rule0 (fn () => Proofterm.OfClass (T, c)),
{cert = cert,
tags = [],
maxidx = maxidx,