*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Wanting only ==>, prop, and schematic variables; but not so*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 19 Jul 2013 16:22:00 -0500*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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

The blackbox-in level is theorem foo "..." with Trueprop coercion unhidden, and the blackbox-out level is thm foo

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**

**Follow-Ups**:**Re: [isabelle] Wanting only ==>, prop, and schematic variables; but not so***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Unable to prove easy existential "directly"
- Next by Date: [isabelle] Syntax.string_of_term changed in Isabelle2013
- Previous by Thread: Re: [isabelle] Unable to prove easy existential "directly"
- Next by Thread: Re: [isabelle] Wanting only ==>, prop, and schematic variables; but not so
- Cl-isabelle-users July 2013 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