Stream: Beginner Questions

Topic: How to manipulate theorems using functions (ML functions)?

view this post on Zulip Yiming Xu (Sep 14 2024 at 09:42):

In HOL4, I can start with a definition and turn it into an induction principle using ML functions using the CONVs. Like this:

val normal_modal_logic = Define`
NML (S: form set) <=> !A B p q f form.
                  (ptaut form ==> form IN S) /\
                  (IMP (BOX (IMP p q)) (IMP (BOX p) (BOX q))) IN S /\
                  (IMP (DIAM p) (NOT (BOX (NOT p)))) IN S /\
                  (IMP (NOT (BOX (NOT p))) (DIAM p)) IN S /\
                  (A IN S ==> (subst f A) IN S) /\
                  (A IN S ==> (BOX A) IN S) /\
                  ((IMP A B) IN S /\ A IN S ==> B IN S)`;

val NMLG_def = Define`
NMLG (Γ:form set) = BIGINTER {A | (normal A) /\ (Γ SUBSET A)}`;


val normal_modal_logic = Define`
NML (S: form set) <=> !A B p q f form.
                  (ptaut form ==> form IN S) /\
                  (IMP (BOX (IMP p q)) (IMP (BOX p) (BOX q))) IN S /\
                  (IMP (DIAM p) (NOT (BOX (NOT p)))) IN S /\
                  (IMP (NOT (BOX (NOT p))) (DIAM p)) IN S /\
                  (A IN S ==> (subst f A) IN S) /\
                  (A IN S ==> (BOX A) IN S) /\
                  ((IMP A B) IN S /\ A IN S ==> B IN S)`;


val NMLG_ind = save_thm(
  "NMLG_ind",
  ``phi ∈ NMLG G``
    |> SIMP_CONV (srw_ss()) [NMLG_def, normal_modal_logic]
    |> EQ_IMP_RULE |> #1
    |> UNDISCH |> SPEC_ALL |> UNDISCH
    |> DISCH ``(phi : form) ∈ NMLG G``
    |> Q.GEN `phi`
    |> DISCH_ALL |> Q.GEN `P`)

Something similar also exists in Lean (although I do not quite know how to use them...)

Is there any way to do something similar in Isabelle? I hope something is written in the reference manual, but I can hardly find any.

view this post on Zulip Yiming Xu (Sep 14 2024 at 09:45):

Say, in above, the t |> f means passing a HOL term into an ML function. Here we start with the HOL term phi ∈ NMLG G of type bool, apply the function SIMP_CONV (srw_ss()) [NMLG_def, normal_modal_logic] on it, it will produce a theorem, with is an "iff". Then the next function takes the theorem, apply the ML function EQ_IMP_RULE on it, to split it into two directions, and the next function takes the forward implication, etc.

view this post on Zulip Yiming Xu (Sep 14 2024 at 09:46):

I believe it can be done by stating the lemma and prove it, but I find some time using functions are more straightforward, and avoid the potential mistakes that may occur when writing out the theorem by hand.

view this post on Zulip Yiming Xu (Sep 14 2024 at 09:51):

The thm NMLG_ind derived using functions:
image.png
It is done by unfolding the definition of big intersection.

Last updated: Dec 21 2024 at 16:20 UTC