[isabelle] Wanting only ==>, prop, and schematic variables; but not so



Hi,

I put this up in case someone wants to add to what I've learned.

Attached is a THY and PDF of my exercise. The PDF shows my efforts to make a printout self-contained. The numbered links take you to a theorem summary, which has a bibliography link with a line number, which takes you to the bibliography entry, which links to a Mercurial source file with line numbers.

Being positively influenced by the concept of sequents, though only just starting to dive into sequents, I saw that there is turnstile, which is used as the meta-language symbol to give meaning to everything else.

There is then the meta-object symbol ==>, and wanting life to be simple, I wanted to say that it is ==> that gives meaning to everything else. However, willing for life to be more complex, I decided that at the blackbox-in and blackbox-out levels, there is only prop, schematic variables, and ==>.

The blackbox-in level is

   theorem foo "..."

with Trueprop coercion unhidden, and the blackbox-out level is

   thm foo

with Trueprop coercion unhidden, and you can't blame me for wanting only prop, schematic variables, and ==>, when that's all I've seen for months at the blackbox level.

In drule.ML, I stumbled on "equal_intr_rule", which expresses meta-logic \<equiv> in terms of ==>. I also saw "triv_forall_equality", and in logical haste, I decided that by proving a theorem that uses \<And> and \<equiv>, and using only "equal_intr_rule", that would allow me to take the perspective that at the blackbox level, it is ==> that gives meaning, rather than \<And> and \<equiv>, where the function arrow operator was far from my mind, though surely it's at a lower level anyway.

The theorem I chose was "atomize_all", but I hit a snag, which was fortunate. I set up the assumptions correctly for "equal_intr_rule", but "rule" didn't use them to prove "atomize_all" in one step, so I resorted to "simp" to do parts of the proof.

The main value of the exercise was in seeing that the simplifier was creating rewrite rules from the assumptions, so it gave new meaning to those mysterious 'Adding rewrite rule "??.unknown"' statements.

What I was looking for was evidence that \<And> and \<equiv> operate independently from ==>, so that they all have to be considered fundamental. Looking at the simp trace kind of gave me that evidence, but someone can correct me if I'm wrong.

Also, when "rule" didn't use the assumptions I gave it, it then made goals based on "equal_intr_rule". But it didn't do an exact instantiation. \<And> is used in the conclusion of "atomize_all", so "rule" made some decisions, and did some rearranging of the use of \<And> before it printed the goals, which indicates to me that it's fundamental.

I'm a little closer to being able to eventually describe how ==>, \<And>, and \<equiv> all fit in at the meta-logic level.

Regards,
GB

(*--{*\<^isub>`\<langle>``*)
(*******************************************************************************)
theory i130719_triv_forall_equality
imports Complex_Main 
begin
(*******************************************************************************)

(*\<bullet>The meaning of operator \<^isub>^\<equiv>\<^isub>_ can possibly be derived from operator \<^isub>^\<Longrightarrow>\<^isub>_ using 
  rule \<^isub>^equal_intr_rule\<^isub>_.*)

thm equal_intr_rule (*                                       --"\<langle>\<cdot>_eq:in:rul.Pu\<cdot>\<rangle>"
  o\<bar> \<^isub>^\<lbrakk>PROP phi \<Longrightarrow> PROP psi; PROP psi \<Longrightarrow> PROP phi\<rbrakk> \<Longrightarrow> PROP phi \<equiv> PROP psi\<^isub>_.*)
         
theorem
  "   (A \<Longrightarrow> B)
  \<Longrightarrow> (B \<Longrightarrow> A)
  \<Longrightarrow> (Trueprop A \<equiv> Trueprop B)"
by(rule equal_intr_rule)                                     --"\<langle>\<cdot>_eq:in:rul.Pu\<cdot>\<rangle>"

(*\<bullet>The meaning of operator \<^isub>^\<And>\<^isub>_ can possibily be derived from operator \<^isub>^\<equiv>\<^isub>_ using 
  rule \<^isub>^triv_forall_equality\<^isub>_, so the meaning of \<^isub>^\<And>\<^isub>_ can possibly be derived from
  \<^isub>^\<Longrightarrow>\<^isub>_ using \<^isub>^equal_intr_rule\<^isub>_. (THIS IS BOGUS. I don't know what all I can get 
  out of \<^isub>^triv_forall_equality\<^isub>_, but it served its purpose for now.)*)
  
thm triv_forall_equality (*                                  --"\<langle>\<cdot>_tr:fo:equ.Pu\<cdot>\<rangle>"
  o\<bar> \<^isub>^(\<And>x. PROP V) \<equiv> PROP V\<^isub>_.*)
  
theorem
  "((\<And>x. PROP V) \<equiv> PROP V)"
apply(rule equal_intr_rule)(*                                --"\<langle>\<cdot>_eq:in:rul.Pu\<cdot>\<rangle>"
  2g\<bar>\<^isub>1\<bar> \<^isub>^(\<And>x. PROP V) \<Longrightarrow> PROP V\<^isub>_ \<bar>\<^isub>2\<bar> \<^isub>^\<And>x. PROP V \<Longrightarrow> PROP V\<^isub>_.
    This is to show that \<^isub>^apply(rule equal_intr_rule)\<^isub>_ will produces goals  
  instead of completing the proof when no assumptions are given which match 
  the assumptions of \<^isub>^equal_intr_rule\<^isub>_. This information and that of the next  
  comment are used to set the stage for a comment below on the proof of
  \<^isub>^atomize_all\<^isub>_.*)
oops
  
theorem
  "   ((\<And>x. PROP V) \<Longrightarrow> PROP V)
  \<Longrightarrow> (PROP V \<Longrightarrow> (\<And>x. PROP V))
  \<Longrightarrow> ((\<And>x. PROP V) \<equiv> PROP V)"
by(rule equal_intr_rule)(*                                   --"\<langle>\<cdot>_eq:in:rul.Pu\<cdot>\<rangle>"
  The two assumptions of \<^isub>^equal_intr_rule\<^isub>_ are provided this time. Rather than 
  produce two goals, \<^isub>^rule\<^isub>_ now completes the proof in one step, using only the 
  rule \<^isub>^equal_intr_rule\<^isub>_.*)

(*\<bullet>Now consider the theorem \<^isub>^atomize_all\<^isub>_, it uses \<^isub>^\<And>\<^isub>_ and \<^isub>^\<equiv>\<^isub>_, but not \<^isub>^\<Longrightarrow>\<^isub>_. If 
  \<^isub>^atomize_all\<^isub>_ can be proved only using \<^isub>^equal_intr_rule\<^isub>_, then it seems the 
  perspective is justified that all Isabelle/HOL logical meaning is a result
  of \<^isub>^prop\<^isub>_, schematic variables, \<^isub>^\<Longrightarrow>\<^isub>_, and nothing more, or at least, \<hungarumlaut>something 
  more\<hungarumlaut> does not have to include \<^isub>^\<And>\<^isub>_ and \<^isub>^\<equiv>\<^isub>_. (NOT ALL BOGUS, BUT BOGUS.)*)
  
thm atomize_all (*                                               --"\<langle>\<cdot>_at:all.H\<cdot>\<rangle>"
  o\<bar> \<^isub>^(\<And>x. P x) \<equiv> \<forall>x. P x\<^isub>_.*)

theorem 
  "   ((\<And>x. P x) \<Longrightarrow> (\<forall>x. P x))
  \<Longrightarrow> ((\<forall>x. P x) \<Longrightarrow> (\<And>x. P x))
  \<Longrightarrow> ((\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x))"
apply(rule equal_intr_rule)(*                                --"\<langle>\<cdot>_eq:in:rul.Pu\<cdot>\<rangle>"  
  2g\<bar>\<^isub>1\<bar> \<^isub>^\<lbrakk>(\<And>x. P x) \<Longrightarrow> \<forall>x. P x; \<And>x. All P \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> (\<And>x. P x) \<Longrightarrow> \<forall>x. P x\<^isub>_ 
    \<bar>\<^isub>2\<bar> \<^isub>^\<And>x. \<lbrakk>(\<And>x. P x) \<Longrightarrow> \<forall>x. P x; \<And>x. All P \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<forall>x. P x \<Longrightarrow> P x\<^isub>_.
    Life is not simple. The right assumptions were provided, but \<^isub>^rule\<^isub>_ did not
  use them. Instead, \<^isub>^rule\<^isub>_ produced two goals. The conclusion can still be proved, 
  but it cannot be completed in one step with \<^isub>^equal_intr_rule\<^isub>_.
    It might be that \<^isub>^Trueprop\<^isub>_ operating on \<^isub>^(\<forall>x. P x)\<^isub>_ both automatically and 
  explicitly causes complications. Having to use \<^isub>^simp\<^isub>_ below ends up being good. 
  It shows that \<^isub>^\<And>\<^isub>_ and \<^isub>^\<equiv>\<^isub>_ appear to have a life of their own when it comes to 
  rewriting.*)
using[[simp_trace]]
apply(simp only: triv_forall_equality)(*                     --"\<langle>\<cdot>_tr:fo:equ.Pu\<cdot>\<rangle>"
  2g\<bar>\<^isub>1\<bar> \<^isub>^\<lbrakk>True \<Longrightarrow> \<forall>x. True; All P \<Longrightarrow> True\<rbrakk> \<Longrightarrow> (\<And>x. P x) \<Longrightarrow> \<forall>x. True\<^isub>_ 
    \<bar>\<^isub>2\<bar> \<^isub>^\<And>x. \<lbrakk>(\<And>x. P x) \<Longrightarrow> \<forall>x. P x; \<And>x. All P \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<forall>x. P x \<Longrightarrow> P x\<^isub>_.   
    Now it starts to get complicated. From the \<^isub>^simp\<^isub>_ trace, some rewriting is 
  being done which is based on \<^isub>^\<Longrightarrow>\<^isub>_. For example, from the second assumption 
  given, a rewrite rule is created:
      \<^isub>^[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:\<^isub>_
      \<^isub>^((\<And>x. P x) \<Longrightarrow> \<forall>x. P x) \<Longrightarrow> (\<And>x. All P \<Longrightarrow> P x) \<Longrightarrow> (\<And>x. P x) \<Longrightarrow> \<forall>x. P x\<^isub>_
      \<^isub>^[1]Adding rewrite rule "??.unknown":\<^isub>_
      \<^isub>^All P \<Longrightarrow> P ?x1 \<equiv> True.\<^isub>_      
  There is a \<hungarumlaut>perspective\<hungarumlaut> problem with this. The simplifier appears to be using 
  the presence of the symbol \<^isub>^\<And>\<^isub>_ to decide that this is a rewrite rule. Addition-
  ally, the symbol \<^isub>^\<equiv>\<^isub>_ is being used to state the new rewrite rule.
    Also, \<^isub>^triv_forall_equality\<^isub>_ is being used to do some rewriting. For example, 
  there is the following rewriting:
      \<^isub>^[1]Applying instance of rewrite rule "Pure.triv_forall_equality":\<^isub>_
      \<^isub>^(\<And>x. PROP ?V) \<equiv> PROP ?V\<^isub>_
      \<^isub>^[1]Rewriting:\<^isub>_
      \<^isub>^(\<And>x. True) \<equiv> True.\<^isub>_
  Again, it appears that the meta-logic symbols \<^isub>^\<And>\<^isub>_ and \<^isub>^\<equiv>\<^isub>_ are used independently 
  of \<^isub>^\<Longrightarrow>\<^isub>_. If \<^isub>^simp\<^isub>_ is using \<^isub>^\<Longrightarrow>\<^isub>_ to determine these equivalencies, it is not making 
  it known.*)
apply(simp only: simp_thms(35))(*                               --"\<langle>\<cdot>_si:thm.H\<cdot>\<rangle>"
  1g\<bar>\<^isub>1\<bar> \<^isub>^\<And>x. \<lbrakk>(\<And>x. P x) \<Longrightarrow> \<forall>x. P x; \<And>x. All P \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<forall>x. P x \<Longrightarrow> P x\<^isub>_.
    The rewriting \<^isub>^\<forall>x. True \<equiv> True\<^isub>_ is done to complete the previous goal.*)
by(simp only: triv_forall_equality)(*                        --"\<langle>\<cdot>_tr:fo:equ.Pu\<cdot>\<rangle>"
  And finally, more rewriting similar to what was done with the first use of
  \<^isub>^triv_forall_equality\<^isub>_.*)
  
(*******************************************************************************)
end
(*******************************************************************************)
(*``\<rangle>\<^isub>`*}*)






Attachment: i130719_triv_forall_equality.pdf
Description: Adobe PDF document



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