*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML*From*: Makarius <makarius at sketis.net>*Date*: Wed, 14 Mar 2018 15:34:54 +0100*In-reply-to*: <b7190ce4-a7f9-3331-78f4-0079b436992d@sketis.net>*References*: <7ceb42ff-0196-5250-6729-97c7edf16f18@in.tum.de> <b7190ce4-a7f9-3331-78f4-0079b436992d@sketis.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

On 13/03/18 23:07, Makarius wrote: > On 12/03/18 18:23, Manuel Eberl wrote: >> Suppose I have a theorem of the form "A ?x ⟹ B ?x ⟹ C ?x ⟹ D ?x" and the >> three theorems "eventually A F", "eventually B F", "eventually C F". >> >> I now want to get the theorem "eventually D F" in ML, but not just for >> three theorems, but for an arbitrary number of premises. In the end, I'd >> like a function that takes a theorem that is an n-ary implication (like >> above) and a list of n elements, each corresponding to one of the premises. >> >> This is a bit like the "eventually_elim" method, but in a forward >> manner. My current solution is as outlined below, but it strikes me as >> somewhat ugly and fragile. In particular, I dislike the "Thm.assumption" >> in the end, but I don't know how to avoid it. > > The included Scratch.thy is what I made out of it, just trying to > understand it formally and writing it down again with the means of > human-readable Isabelle/Isar and Isabelle/ML (see also "implementation" > manual section "0.1 Style and orthography"). > > It is getting late and I need to postpone investigating the actual > technical question behind it. Or maybe someone else can see it now on > the spot. Here is another version of both the proof method from theory HOL.Filter and the above forward inference in ML (which could be an attribute). Apart from further fine-tuning of Isabelle/ML "style and orthography", I did not change anything significant. So for now I would say that your original approach to go from rule: "A x ⟹ B x ⟹ C x ⟹ D x" for x to the "eventually" rule is fine -- including the Thm.assumption operation. (Incidently the same happens in the Isar proof snippet given at the bottom, to fit the result of fix/assume/show into the pending goal; similarly in the "by fact" step). Of course, it implicitly depends on well-behaved HO-unification problems given to this operation. Where does the situation "Suppose I have a theorem of the form ..." actually emerge? That rule is in Isabelle standard form, as HO Horn clause with removed outer quantification. So fitting it into a goal usually requires unification to recover the lost information of the quantifier prefix. In principle, the rule could be made a closed form (in HOL or non-standard Pure form) and applied with some low-level inference. It does not get automatically better, though, but depends on the actual application. Makarius

theory Scratch imports Main begin ML \<open> fun eventually_elim_tac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => let val mp_facts = facts RL @{thms eventually_rev_mp} val rule = @{thm eventuallyI} |> fold (fn mp_fact => fn th => th RS mp_fact) mp_facts |> funpow (length facts) (fn th => @{thm impI} RS th) val cases_prop = Thm.prop_of (Rule_Cases.internalize_params (rule RS Goal.init (Thm.cterm_of ctxt goal))) val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])] in CONTEXT_CASES cases (resolve_tac ctxt [rule] i) (ctxt, st) end) \<close> method_setup eventually_elim = \<open> Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1)) \<close> "elimination of eventually quantifiers" ML \<open> fun eventually_mono_OF _ rule [] = rule | eventually_mono_OF ctxt rule thms = let val conj_conv = Conv.rewr_conv @{thm conj_imp_eq_imp_imp [symmetric]} val conjs_conv = Conv.every_conv (replicate (length thms - 1) conj_conv) val eventually_conj = foldl1 (fn (P, Q) => @{thm eventually_conj} OF [P, Q]) in (@{thm eventually_mono} OF [eventually_conj thms, Conv.fconv_rule conjs_conv rule]) |> Thm.assumption (SOME ctxt) 1 |> Seq.list_of |> the_single end \<close> notepad begin fix A B C D :: "'a \<Rightarrow> bool" fix F :: "'a filter" assume rule: "A x \<Longrightarrow> B x \<Longrightarrow> C x \<Longrightarrow> D x" for x assume thms: "eventually A F" "eventually B F" "eventually C F" text \<open>Backward refinement -- proof method\<close> from thms have "eventually D F" proof eventually_elim show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x \<Longrightarrow> D x" by (fact rule) qed text \<open>Forward inference -- attribute\<close> ML_val \<open>eventually_mono_OF @{context} @{thm rule} @{thms thms}\<close> end end

**Follow-Ups**:**Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML***From:*Manuel Eberl

**References**:**[isabelle] Applying n-ary monotonicity of "eventually" in ML***From:*Manuel Eberl

**Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML***From:*Makarius

- Previous by Date: Re: [isabelle] Eisbach documentation
- Next by Date: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Previous by Thread: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Next by Thread: Re: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Cl-isabelle-users March 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list