# HG changeset patch # User wenzelm # Date 1570654852 -7200 # Node ID 5bc338cee4a0814f6d183d440b4705cdcd488483 # Parent c39bd607203b1eae6c87ce544ffbc3912f7f8e6c# Parent a74ab9230cb3e17f66373e02847adab5a4f12db9 merged diff -r c39bd607203b -r 5bc338cee4a0 src/Pure/Proof/extraction.ML --- 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'; diff -r c39bd607203b -r 5bc338cee4a0 src/Pure/Proof/proof_syntax.ML --- 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 diff -r c39bd607203b -r 5bc338cee4a0 src/Pure/logic.ML --- 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 diff -r c39bd607203b -r 5bc338cee4a0 src/Pure/proofterm.ML --- 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; diff -r c39bd607203b -r 5bc338cee4a0 src/Pure/thm.ML --- 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 \ 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,