(*--{*\<^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>`*}*)