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



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.