Email Gateway (Aug 19 2022 at 13:11): Email Gateway (Aug 19 2022 at 13:11):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Planning to rework an SML application I did three years ago, I wanted to
have a start trying something in a sample theory, attached to this message
and pasted below in case the attachment disappears.
On the last line of the simple lemma proof, at “from 4 show "t1 ≅ t2" by
(simp add: 3)”, if I move the mouse cursor over “≅” while Ctrl is pressed,
I get a tool‑tip which tells me it's a fixed variable as well as a free
variable. Surprising, as to me it's a fixed variable, but I don't mind
more. More disturbing, is what I see in the Output pan when I move the
caret to the end of the same line ; it displays “t1 ≅ t2” and if I move
the mouse cursor over it while Ctrl is pressed, it says it's a free
variable, and just a free variable, and it draws the “≅” in blue instead
of black. Why does it become a free variable in the Output pan ?
As a question aside, is there a more explicit way to substitute the second
“t1” in 4 using the equivalence from 3 ? I feel I already came a similar
question one year ago, but I'm not able to remember what I did (I'm
seasoned with Isabelle).
-----%<---------->%-----
theory Sample
imports Main
begin
typedecl atom;
typedecl variable;
datatype "term" =
Any ("ε")
| Atom atom ("α")
| Variable variable ("υ")
| Compound "term list" ("ω")
;
locale unification =
fixes
unifies :: "[term, term] ⇒ bool" (infix "≅" 500) and
"interpretation" :: "variable ⇒ term" ("⊢")
assumes
self: "t ≅ t" and
comm: "t1 ≅ t2 ⟷ t2 ≅ t1" and
inter: "(υ v) ≅ t ⟷ (⊢ v) ≅ t" and
rec: "(ω (t1 # r1)) ≅ (ω (t2 # r2)) ⟷ t1 ≅ t2 ∧ (ω r1) ≅ (ω r2)"
;
lemma (in unification) l1: "t1 = t2 ⟹ t1 ≅ t2"
proof -
assume 1: "t1 = t2"
have 2: "t1 = t2 ⟹ t1 ≡ t2" by (fact HOL.eq_reflection[of t1 t2])
have 3: "t1 ≡ t2" by (fact 2[OF 1])
have 4: "t1 ≅ t1" by (fact self[of t1])
from 4 show "t1 ≅ t2" by (simp add: 3)
qed
;
end
-----%<---------->%-----
Sample.thy
Email Gateway (Aug 19 2022 at 13:12):From: Makarius <makarius@sketis.net>
On Wed, 4 Dec 2013, Yannick Duchêne (Hibou57) wrote:
On the last line of the simple lemma proof, at “from 4 show "t1 ≅ t2"
by (simp add: 3)”, if I move the mouse cursor over “≅” while Ctrl is
pressed, I get a tool‑tip which tells me it's a fixed variable as well
as a free variable. Surprising, as to me it's a fixed variable, but I
don't mind more. More disturbing, is what I see in the Output pan when I
move the caret to the end of the same line ; it displays “t1 ≅ t2” and
if I move the mouse cursor over it while Ctrl is pressed, it says it's a
free variable, and just a free variable, and it draws the “≅” in blue
instead of black. Why does it become a free variable in the Output pan ?
I don't see an actual constant in the example, although a fixed variable
is better understood as "local constant".
The PIDE markup seen in the input or output represents certain aspects of
the formal processing by the prover. This sometimes exposes more internal
details than make sense to the user. It needs some further refinements,
but that is part of the concept: more and more useful markup information
is provided and rendered -- this is a continuous process over the years.
As a question aside, is there a more explicit way to substitute the
second “t1” in 4 using the equivalence from 3 ? I feel I already came a
similar question one year ago, but I'm not able to remember what I did
lemma (in unification) l1: "t1 = t2 ⟹ t1 ≅ t2"
proof -
assume 1: "t1 = t2"
have 2: "t1 = t2 ⟹ t1 ≡ t2" by (fact HOL.eq_reflection[of t1 t2])
have 3: "t1 ≡ t2" by (fact 2[OF 1])
have 4: "t1 ≅ t1" by (fact self[of t1])
from 4 show "t1 ≅ t2" by (simp add: 3)
qed
The use of Pure equality and HOL.eq_reflection looks a bit strange: you
should bever need that in HOL applications, unless some old forms are
somehow ported.
A more imminent proof just normalizes wrt. "t1 = t2" and the solves via
reflexivity ("self"):
lemma (in unification) "t1 = t2 ⟹ t1 ≅ t2"
by (simp add: self)
More explicit reasoning can be done by calculations in Isar, but its
substitution steps will always replace all occurrences of the subterm in
question (according to the standard policy of Larry's implementation of
Huet). Going from "t1 ≅ t1" to "t1 ≅ t2" is not immediate in this
scheme.
Maybe some experts on hand-crafted substitution can point out frequently
used patterns, without too much "term surgery".
Makarius
Email Gateway (Aug 19 2022 at 13:12):From: Yannick <yannick_duchene@yahoo.fr>
On Wed, 04 Dec 2013 13:22:15 +0100, Makarius <makarius@sketis.net> wrote:
The PIDE markup seen in the input or output represents certain aspects of
the formal processing by the prover. This sometimes exposes more
internal
details than make sense to the user. It needs some further refinements,
but that is part of the concept: more and more useful markup information
is provided and rendered -- this is a continuous process over the years.
OK, so may be it says it's a free variable when it does not already know
it's fixed.
The use of Pure equality and HOL.eq_reflection looks a bit strange: you
should bever need that in HOL applications, unless some old forms are
somehow ported.
I've just checked, and “HOL.thy” indeed says “(admissible axiom)”. Will
try to learn to do without it.
Thanks for the pointers you gave on both topics.
Email Gateway (Aug 19 2022 at 13:13):From: Makarius <makarius@sketis.net>
In some sense this belongs to the "implementation" of Isabelle/HOL on top
of the Isabelle/Pure framework.
These days you should hardly ever need == in Isabelle/HOL applications.
This is different to !! and ==>, which have a specific purpose to outline
Natural Deduction rule schemes in a declarative manner, independently of
the object-logic.
Makarius
Email Gateway (Aug 19 2022 at 13:13):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Does that mean substitution/simplification is not expressed with “==” but
“=” instead ? I always though “==” was the standard for that purpose with
logic.
Email Gateway (Aug 19 2022 at 13:13):From: Makarius <makarius@sketis.net>
The basic substitution rules of Isabelle/HOL directly refer to =, not ==.
This is also relevant to calculational reasoning, e.g. see
print_trans_rules. (That gives only very limited support for some basic
Pure reasoning with ==).
Some other tools go to the bottom of Pure and use == internally, such as
the Simplifier itself (which is somewhat independent of the object-logic).
This is also one of several points in the system where both = and == are
allowed in user input, but this duplication of interfaces is not
universal.
That was important in the past, because the primite 'defs' command was
used routinely in user theories, and thus there was considerable mix-up of
connectives. For many years already, the 'definition' command allows to
use = of Isabelle/HOL, just like other specification elements that are
proper to HOL.
Makarius
Last updated: Apr 24 2024 at 20:16 UTC