[isabelle] refl can be proved

[Makarius]

lemma refl: "t = t"
proof -
have "(THE x. x = t) = t" by (rule the_eq_trivial)
from this and this show "t = t" by (rule subst)
qed

What can we learn from that?

The usual way to characterize equality is via refl and subst,
independently of later add-ons to the logic.


The axiomatization of Isabelle/HOL is somewhat historic and accidental,
following a report by Mike Gordon from 1986, which in turn followed the
paper by Alonzo Church from 1940.

In this distance past logicians where still following a bad habit to
make the textual representation of the foundations as small as possible,
without taking care about clarity. Who in his right mind would base the
EX quantifier on Hilbert's Choice operator, for example? There are other
historical oddities and tidbits to be (re)discovered.


Here is also my own version of Higher-Order Logic for illustrative
purposes: $ISABELLE_HOME/src/HOL/Isar_Examples/Higher_Order_Logic.thy --
it introduces Hilbert's "Eps" late in the theory, but omits the definite
description operator "The".

Many more variations on the theme are possible, but they have no
practical relevance of using the HOL logic in applications: definitional
packages and proof tools are much more important than axiomatizations.
That is the main lesson learned after decades of trying to make logics
work in Interactive Theorem Proving.


Makarius

[Ching-Tsun Chou]

Continuing with my previous example below, I add:

lemma evSS_sum: "ev (n+m) ⟹ ev (Suc (Suc (n+m)))"
proof -
assume "ev (n+m)"
then show "ev (Suc (Suc (n+m)))" by (rule ev_SS)
qed

theorem ev_sum: "ev n ⟹ ev m ⟹ ev (n+m)"
proof (induction rule: ev.induct)
case ev_0
then show ?case by (simp)
next
case (ev_SS n)
then have "ev (n+m)" by (auto)
then have "ev (Suc (Suc (n+m)))" *by (rule ev_SS)*
then show ?case by (auto simp add: ev_SS)
qed

The proof of evSS_sum works. But in the proof of ev_sum, the boldfaced "by
(rule ev_SS)" fails with the following error message:

Failed to apply initial proof method⌂:
using this:
ev (n + m)
goal (1 subgoal):
1. ev (Suc (Suc (n + m)))

Why??? The proof method seems to be used in identical contexts in both
cases. Why does it work in one case but not in the other?

Thanks!
- Ching Tsun

For the life of me, I cannot figure out why the highlighted line of my
proof below does not work. It seems to me that I have proved all facts
necessary to finish the proof. What did I miss?
Many thanks in advance!
- Ching Tsun
theory JustTest
imports Main
begin
inductive ev :: "nat ⇒ bool" where
ev_0: "ev 0" |
ev_SS: "ev n ⟹ ev (Suc (Suc n))"
fun double :: "nat ⇒ nat" where
"double 0 = 0" |
"double (Suc n) = Suc (Suc (double n))"
fun evn :: "nat ⇒ bool" where
"evn 0 = True" |
"evn (Suc 0) = False" |
"evn (Suc (Suc n)) = evn n"
lemma ev_imp_evn: "ev n ⟹ evn n"
apply (induction rule: ev.induct)
apply (simp_all)
done
lemma evn_imp_ev: "evn n ⟹ ev n"
apply (induction n rule: evn.induct)
apply (simp_all add: ev_0 ev_SS)
done
theorem not_ev_1: "¬ ev (Suc 0)"
proof
assume "ev (Suc 0)"
then have "evn (Suc 0)" by (rule ev_imp_evn)
then show False by (simp)
qed
theorem not_ev_double_plus_1: "¬ ev (Suc (double n))"
proof (induction n)
case 0
then show ?case by (simp add: not_ev_1)
next
fix n assume p1: "¬ ev (Suc (double n))"
assume "ev (Suc (double (Suc n)))"
then have "evn (Suc (double (Suc n)))" by (rule ev_imp_evn)
then have "evn (Suc (double n))" by (simp)
then have p2: "ev (Suc (double n))" by (rule evn_imp_ev)
*from p1 p2 show ?thesis by (blast)*
qed
end

[Christian Sternagel]

Dear Ching Tsun,

without having had time to actual try your example in Isabelle/jEdit,

Post by Ching-Tsun Chou
lemma evSS_sum: "ev (n+m) ⟹ ev (Suc (Suc (n+m)))"
proof -
assume "ev (n+m)"
then show "ev (Suc (Suc (n+m)))" by (rule ev_SS)

"ev_SS" in the line above refers to one case of the inductive definition
of "ev"

Post by Ching-Tsun Chou
qed
theorem ev_sum: "ev n ⟹ ev m ⟹ ev (n+m)"
proof (induction rule: ev.induct)
case ev_0
then show ?case by (simp)
next
case (ev_SS n)
then have "ev (n+m)" by (auto)
then have "ev (Suc (Suc (n+m)))" *by (rule ev_SS)*

"ev_SS" in the line above refers to the facts that where introduced by
"case (ev_SS n)", which might be very different from the meaning in the
previous lemma.

You may want to rename the case locally, e.g., via

case A: (ev_SS n)

cheers

chris

Post by Ching-Tsun Chou
then show ?case by (auto simp add: ev_SS)
qed
The proof of evSS_sum works. But in the proof of ev_sum, the boldfaced "by
ev (n + m)
1. ev (Suc (Suc (n + m)))
Why??? The proof method seems to be used in identical contexts in both
cases. Why does it work in one case but not in the other?
Thanks!
- Ching Tsun

For the life of me, I cannot figure out why the highlighted line of my
proof below does not work. It seems to me that I have proved all facts
necessary to finish the proof. What did I miss?
Many thanks in advance!
- Ching Tsun
theory JustTest
imports Main
begin
inductive ev :: "nat ⇒ bool" where
ev_0: "ev 0" |
ev_SS: "ev n ⟹ ev (Suc (Suc n))"
fun double :: "nat ⇒ nat" where
"double 0 = 0" |
"double (Suc n) = Suc (Suc (double n))"
fun evn :: "nat ⇒ bool" where
"evn 0 = True" |
"evn (Suc 0) = False" |
"evn (Suc (Suc n)) = evn n"
lemma ev_imp_evn: "ev n ⟹ evn n"
apply (induction rule: ev.induct)
apply (simp_all)
done
lemma evn_imp_ev: "evn n ⟹ ev n"
apply (induction n rule: evn.induct)
apply (simp_all add: ev_0 ev_SS)
done
theorem not_ev_1: "¬ ev (Suc 0)"
proof
assume "ev (Suc 0)"
then have "evn (Suc 0)" by (rule ev_imp_evn)
then show False by (simp)
qed
theorem not_ev_double_plus_1: "¬ ev (Suc (double n))"
proof (induction n)
case 0
then show ?case by (simp add: not_ev_1)
next
fix n assume p1: "¬ ev (Suc (double n))"
assume "ev (Suc (double (Suc n)))"
then have "evn (Suc (double (Suc n)))" by (rule ev_imp_evn)
then have "evn (Suc (double n))" by (simp)
then have p2: "ev (Suc (double n))" by (rule evn_imp_ev)
*from p1 p2 show ?thesis by (blast)*
qed
end