# HG changeset patch # User wenzelm # Date 1632680008 -7200 # Node ID d1185d02aef5ca0ca86c05b6adfecbe4df837267 # Parent 99add5178e51519de89c36f31e87c557b6e87ac7# Parent b49bd5d9041f3cb6c5269e4645ed56d3b5aabd40 merged diff -r 99add5178e51 -r d1185d02aef5 NEWS --- a/NEWS Sat Sep 25 07:45:27 2021 +0000 +++ b/NEWS Sun Sep 26 20:13:28 2021 +0200 @@ -44,6 +44,15 @@ Isabelle/jEdit. +*** Isar *** + +* The improper proof command 'guess' is no longer part of by Pure, but +provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY, +existing applications need to import session "Pure-ex" and theory +"Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess' +command, using explicit 'obtain' instead. + + *** Isabelle/jEdit Prover IDE *** * More robust 'proof' outline for method "induct": support nested cases. diff -r 99add5178e51 -r d1185d02aef5 src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Sat Sep 25 07:45:27 2021 +0000 +++ b/src/Doc/Implementation/Proof.thy Sun Sep 26 20:13:28 2021 +0200 @@ -352,10 +352,11 @@ means of a given tactic. This acts like a dual conclusion: the proof demonstrates that the context may be augmented by parameters and assumptions, without affecting any conclusions that do not mention these - parameters. See also @{cite "isabelle-isar-ref"} for the user-level - @{command obtain} and @{command guess} elements. Final results, which may - not refer to the parameters in the conclusion, need to exported explicitly - into the original context.\ + parameters. See also @{cite "isabelle-isar-ref"} for the corresponding Isar + proof command @{command obtain}. Final results, which may not refer to the + parameters in the conclusion, need to exported explicitly into the original + context. +\ text %mlref \ \begin{mldecls} diff -r 99add5178e51 -r d1185d02aef5 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Sat Sep 25 07:45:27 2021 +0000 +++ b/src/Doc/Isar_Ref/Proof.thy Sun Sep 26 20:13:28 2021 +0200 @@ -1321,7 +1321,6 @@ \begin{matharray}{rcl} @{command_def "consider"} & : & \proof(state) | proof(chain) \ proof(prove)\ \\ @{command_def "obtain"} & : & \proof(state) | proof(chain) \ proof(prove)\ \\ - @{command_def "guess"}\\<^sup>*\ & : & \proof(state) | proof(chain) \ proof(prove)\ \\ \end{matharray} Generalized elimination means that hypothetical parameters and premises may @@ -1352,8 +1351,6 @@ concl: (@{syntax props} + @'and') ; prems: (@'if' (@{syntax props'} + @'and'))? - ; - @@{command guess} @{syntax vars} \ \<^descr> @{command consider}~\(a) \<^vec>x \ \<^vec>A \<^vec>x | (b) @@ -1412,29 +1409,14 @@ \quad @{command "fix"}~\\<^vec>x\~@{command "assume"}\\<^sup>* a: \<^vec>A \<^vec>x\ \\ \end{matharray} - \<^descr> @{command guess} is similar to @{command obtain}, but it derives the - obtained context elements from the course of tactical reasoning in the - proof. Thus it can considerably obscure the proof: it is classified as - \<^emph>\improper\. - - A proof with @{command guess} starts with a fixed goal \thesis\. The - subsequent refinement steps may turn this to anything of the form - \\\<^vec>x. \<^vec>A \<^vec>x \ thesis\, but without splitting into new - subgoals. The final goal state is then used as reduction rule for the obtain - pattern described above. Obtained parameters \\<^vec>x\ are marked as - internal by default, and thus inaccessible in the proof text. The variable - names and type constraints given as arguments for @{command "guess"} specify - a prefix of accessible parameters. - - In the proof of @{command consider} and @{command obtain} the local premises are always bound to the fact name @{fact_ref that}, according to structured Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}). - Facts that are established by @{command "obtain"} and @{command "guess"} may - not be polymorphic: any type-variables occurring here are fixed in the - present context. This is a natural consequence of the role of @{command fix} - and @{command assume} in these constructs. + Facts that are established by @{command "obtain"} cannot be polymorphic: any + type-variables occurring here are fixed in the present context. This is a + natural consequence of the role of @{command fix} and @{command assume} in + this construct. \ end diff -r 99add5178e51 -r d1185d02aef5 src/HOL/ROOT --- a/src/HOL/ROOT Sat Sep 25 07:45:27 2021 +0000 +++ b/src/HOL/ROOT Sun Sep 26 20:13:28 2021 +0200 @@ -668,7 +668,6 @@ Execute_Choice Function_Growth Gauge_Integration - Guess HarmonicSeries Hebrew Hex_Bin_Examples diff -r 99add5178e51 -r d1185d02aef5 src/HOL/ex/Guess.thy --- a/src/HOL/ex/Guess.thy Sat Sep 25 07:45:27 2021 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* - Author: Makarius -*) - -section \Proof by guessing\ - -theory Guess -imports Main -begin - -notepad -begin - have 1: "\x. x = x" by simp - - from 1 guess .. - from 1 guess x .. - from 1 guess x :: 'a .. - from 1 guess x :: nat .. - - have 2: "\x y. x = x \ y = y" by simp - from 2 guess apply - apply (erule exE conjE)+ done - from 2 guess x apply - apply (erule exE conjE)+ done - from 2 guess x y apply - apply (erule exE conjE)+ done - from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done - from 2 guess x y :: nat apply - apply (erule exE conjE)+ done -end - -end diff -r 99add5178e51 -r d1185d02aef5 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Sat Sep 25 07:45:27 2021 +0000 +++ b/src/Pure/Isar/obtain.ML Sun Sep 26 20:13:28 2021 +0200 @@ -6,6 +6,7 @@ signature OBTAIN = sig + val obtain_export: Proof.context -> thm -> cterm list -> Assumption.export val obtain_thesis: Proof.context -> ((string * typ) * term) * Proof.context val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list val obtains_attribs: ('typ, 'term) Element.obtain list -> Token.src list @@ -20,10 +21,9 @@ val obtain_cmd: binding -> (binding * string option * mixfix) list -> (binding * string option * mixfix) list -> (string * string list) list list -> (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state + val check_result: Proof.context -> term -> thm -> thm val result: (Proof.context -> tactic) -> thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context - val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state - val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state end; structure Obtain: OBTAIN = @@ -274,152 +274,4 @@ (Drule.strip_imp_prems stmt) fix_ctxt; in ((params, prems), ctxt'') end; - - -(** guess: obtain based on tactical result **) - -(* - - guess x \ - - { - fix thesis - have "PROP ?guess" - apply magic \ \turn goal into \thesis \ #thesis\\ - - apply_end magic \ \turn final \(\x. P x \ thesis) \ #thesis\ into\ - \ \\#((\x. A x \ thesis) \ thesis)\ which is a finished goal state\ - - } - fix x assm <> "A x" -*) - -local - -fun unify_params vars thesis_var raw_rule ctxt = - let - val thy = Proof_Context.theory_of ctxt; - val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); - - fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th); - - val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; - val rule = Thm.incr_indexes (maxidx + 1) raw_rule; - - val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); - val m = length vars; - val n = length params; - val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; - - fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) - handle Type.TUNIFY => - err ("Failed to unify variable " ^ - string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ - string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule; - val (tyenv, _) = fold unify (map #1 vars ~~ take m params) - (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); - val norm_type = Envir.norm_type tyenv; - - val xs = map (apsnd norm_type o fst) vars; - val ys = map (apsnd norm_type) (drop m params); - val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; - val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys'); - - val instT = - TVars.build - (params |> fold (#2 #> Term.fold_atyps (fn T => fn instT => - (case T of - TVar v => - if TVars.defined instT v then instT - else TVars.add (v, Thm.ctyp_of ctxt (norm_type T)) instT - | _ => instT)))); - val closed_rule = rule - |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) - |> Thm.instantiate (instT, Vars.empty); - - val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; - val vars' = - map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ - (map snd vars @ replicate (length ys) NoSyn); - val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule'; - in ((vars', rule''), ctxt') end; - -fun inferred_type (binding, _, mx) ctxt = - let - val x = Variable.check_name binding; - val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt - in ((x, T, mx), ctxt') end; - -fun polymorphic ctxt vars = - let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) - in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; - -fun gen_guess prep_var raw_vars int state = - let - val _ = Proof.assert_forward_or_chain state; - val ctxt = Proof.context_of state; - val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; - - val (thesis_var, thesis) = #1 (obtain_thesis ctxt); - val vars = ctxt - |> fold_map prep_var raw_vars |-> fold_map inferred_type - |> fst |> polymorphic ctxt; - - fun guess_context raw_rule state' = - let - val ((parms, rule), ctxt') = - unify_params vars thesis_var raw_rule (Proof.context_of state'); - val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt'; - val ps = xs ~~ map (#2 o #1) parms; - val ts = map Free ps; - val asms = - Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) - |> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), [])); - val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; - in - state' - |> Proof.map_context (K ctxt') - |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) - |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm - (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts)) - [] [] [(Binding.empty_atts, asms)]) - |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts) - end; - - val goal = Var (("guess", 0), propT); - val pos = Position.thread_data (); - fun print_result ctxt' (k, [(s, [_, th])]) = - Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); - val before_qed = - Method.primitive_text (fn ctxt => - Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> - (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))); - fun after_qed (result_ctxt, results) state' = - let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) - in - state' - |> Proof.end_block - |> guess_context (check_result ctxt thesis res) - end; - in - state - |> Proof.enter_forward - |> Proof.begin_block - |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] - |> Proof.chain_facts chain_facts - |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess" - (SOME before_qed) after_qed - [] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])] - |> snd - |> Proof.refine_singleton - (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis))) - end; - -in - -val guess = gen_guess Proof_Context.cert_var; -val guess_cmd = gen_guess Proof_Context.read_var; - end; - -end; diff -r 99add5178e51 -r d1185d02aef5 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Sep 25 07:45:27 2021 +0000 +++ b/src/Pure/Pure.thy Sun Sep 26 20:13:28 2021 +0200 @@ -62,7 +62,6 @@ and "fix" "assume" "presume" "define" :: prf_asm % "proof" and "consider" :: prf_goal % "proof" and "obtain" :: prf_asm_goal % "proof" - and "guess" :: prf_script_asm_goal % "proof" and "let" "write" :: prf_decl % "proof" and "case" :: prf_asm % "proof" and "{" :: prf_open % "proof" @@ -906,10 +905,6 @@ >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); val _ = - Outer_Syntax.command \<^command_keyword>\guess\ "wild guessing (unstructured)" - (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd)); - -val _ = Outer_Syntax.command \<^command_keyword>\let\ "bind text variables" (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\=\ |-- Parse.term)) >> (Toplevel.proof o Proof.let_bind_cmd)); diff -r 99add5178e51 -r d1185d02aef5 src/Pure/ROOT --- a/src/Pure/ROOT Sat Sep 25 07:45:27 2021 +0000 +++ b/src/Pure/ROOT Sun Sep 26 20:13:28 2021 +0200 @@ -26,6 +26,11 @@ description " Miscellaneous examples and experiments for Isabelle/Pure. " + sessions + "Pure-Examples" theories Def Def_Examples + Guess + Guess_Examples + diff -r 99add5178e51 -r d1185d02aef5 src/Pure/ex/Guess.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ex/Guess.thy Sun Sep 26 20:13:28 2021 +0200 @@ -0,0 +1,191 @@ +(* Title: Pure/ex/Guess.thy + Author: Makarius + +Improper proof command 'guess': variant of 'obtain' based on tactical result. + + + guess x \ + + { + fix thesis + have "PROP ?guess" + apply magic \ \turn goal into \thesis \ #thesis\\ + + apply_end magic \ \turn final \(\x. P x \ thesis) \ #thesis\ into\ + \ \\#((\x. A x \ thesis) \ thesis)\ which is a finished goal state\ + + } + fix x assm <> "A x" +*) + +section \Improper proof command 'guess'\ + +theory Guess + imports Pure + keywords "guess" :: prf_script_asm_goal % "proof" +begin + +text \ + The @{command guess} is similar to @{command obtain}, but it derives the + obtained context elements from the course of tactical reasoning in the + proof. Thus it can considerably obscure the proof: it is provided here as + \<^emph>\improper\ and experimental feature. + + A proof with @{command guess} starts with a fixed goal \thesis\. The + subsequent refinement steps may turn this to anything of the form + \\\<^vec>x. \<^vec>A \<^vec>x \ thesis\, but without splitting into new + subgoals. The final goal state is then used as reduction rule for the obtain + pattern described above. Obtained parameters \\<^vec>x\ are marked as + internal by default, and thus inaccessible in the proof text. The variable + names and type constraints given as arguments for @{command "guess"} specify + a prefix of accessible parameters. + + Some examples are in \<^file>\Guess_Examples.thy\. +\ + +ML \ +signature GUESS = +sig + val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state + val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state +end; + +structure Guess: GUESS = +struct + +local + +fun unify_params vars thesis_var raw_rule ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); + + fun err msg th = error (msg ^ ":\n" ^ Thm.string_of_thm ctxt th); + + val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1; + val rule = Thm.incr_indexes (maxidx + 1) raw_rule; + + val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule)); + val m = length vars; + val n = length params; + val _ = m <= n orelse err "More variables than parameters in obtained rule" rule; + + fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max) + handle Type.TUNIFY => + err ("Failed to unify variable " ^ + string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^ + string_of_term (Syntax_Trans.mark_bound_abs (y, Envir.norm_type tyenv U)) ^ " in") rule; + val (tyenv, _) = fold unify (map #1 vars ~~ take m params) + (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule)); + val norm_type = Envir.norm_type tyenv; + + val xs = map (apsnd norm_type o fst) vars; + val ys = map (apsnd norm_type) (drop m params); + val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; + val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys'); + + val instT = + TVars.build + (params |> fold (#2 #> Term.fold_atyps (fn T => fn instT => + (case T of + TVar v => + if TVars.defined instT v then instT + else TVars.add (v, Thm.ctyp_of ctxt (norm_type T)) instT + | _ => instT)))); + val closed_rule = rule + |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) + |> Thm.instantiate (instT, Vars.empty); + + val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; + val vars' = + map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ + (map snd vars @ replicate (length ys) NoSyn); + val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule'; + in ((vars', rule''), ctxt') end; + +fun inferred_type (binding, _, mx) ctxt = + let + val x = Variable.check_name binding; + val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt + in ((x, T, mx), ctxt') end; + +fun polymorphic ctxt vars = + let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) + in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end; + +fun gen_guess prep_var raw_vars int state = + let + val _ = Proof.assert_forward_or_chain state; + val ctxt = Proof.context_of state; + val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; + + val (thesis_var, thesis) = #1 (Obtain.obtain_thesis ctxt); + val vars = ctxt + |> fold_map prep_var raw_vars |-> fold_map inferred_type + |> fst |> polymorphic ctxt; + + fun guess_context raw_rule state' = + let + val ((parms, rule), ctxt') = + unify_params vars thesis_var raw_rule (Proof.context_of state'); + val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt'; + val ps = xs ~~ map (#2 o #1) parms; + val ts = map Free ps; + val asms = + Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule)) + |> map (fn asm => (Term.betapplys (fold_rev Term.abs ps asm, ts), [])); + val _ = not (null asms) orelse error "Trivial result -- nothing guessed"; + in + state' + |> Proof.map_context (K ctxt') + |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) + |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm + (Obtain.obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts)) + [] [] [(Binding.empty_atts, asms)]) + |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts) + end; + + val goal = Var (("guess", 0), propT); + val pos = Position.thread_data (); + fun print_result ctxt' (k, [(s, [_, th])]) = + Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); + val before_qed = + Method.primitive_text (fn ctxt => + Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #> + (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))); + fun after_qed (result_ctxt, results) state' = + let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) + in + state' + |> Proof.end_block + |> guess_context (Obtain.check_result ctxt thesis res) + end; + in + state + |> Proof.enter_forward + |> Proof.begin_block + |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] + |> Proof.chain_facts chain_facts + |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess" + (SOME before_qed) after_qed + [] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])] + |> snd + |> Proof.refine_singleton + (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis))) + end; + +in + +val guess = gen_guess Proof_Context.cert_var; +val guess_cmd = gen_guess Proof_Context.read_var; + +val _ = + Outer_Syntax.command \<^command_keyword>\guess\ "wild guessing (unstructured)" + (Scan.optional Parse.vars [] >> (Toplevel.proof' o guess_cmd)); + +end; + +end; +\ + +end diff -r 99add5178e51 -r d1185d02aef5 src/Pure/ex/Guess_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ex/Guess_Examples.thy Sun Sep 26 20:13:28 2021 +0200 @@ -0,0 +1,31 @@ +(* Title: Pure/ex/Guess_Examples.thy + Author: Makarius +*) + +section \Proof by wild guessing\ + +theory Guess_Examples +imports "Pure-Examples.Higher_Order_Logic" Guess +begin + +typedecl t +instance t :: type .. + +notepad +begin + have 1: "\x :: 'a. x = x" by (intro exI refl) + + from 1 guess .. + from 1 guess x .. + from 1 guess x :: 'a .. + from 1 guess x :: t .. + + have 2: "\(x::'c) (y::'d). x = x \ y = y" by (intro exI conjI refl) + from 2 guess apply - apply (erule exE conjE)+ done + from 2 guess x apply - apply (erule exE conjE)+ done + from 2 guess x y apply - apply (erule exE conjE)+ done + from 2 guess x :: 'a and y :: 'b apply - apply (erule exE conjE)+ done + from 2 guess x y :: t apply - apply (erule exE conjE)+ done +end + +end