Thanks, Konrad! The proof of SYM in the HOL4 manual Description (p 46) is fine
because the HOL4 SUBST is much more powerful than the HOL Light INST. On p 26,
SUBST is described by
SUBST : (thm * term)list -> term -> thm -> thm
t[t1 , . . . , tn ] yields t[t1',...,tn']
. where t[t1 , . . . , tn ] denotes a term t with some free
occurrences of the terms t1,...,tn singled out [...]
The second argument is a template term t[x1 , . . . , xn ] in which
occurrences of the variable xi (where 1 ≤ i ≤ n) are used to mark the
places where substitutions with |- ti =ti are to be done.
The template stuff looks pretty clever. I suppose the term t[x1 , . . . , xn ]
means t with the variable xi replacing each free occurence of ti we want
replaced by ti'. I think it should say that the variables xi don't occur in t.
Now the proof of SYM work:
1. Gamma |- t1 = t2 [Hypothesis]
2. |- t1 = t1 [REFL]
3. Gamma |- t2 = t1 [SUBST 1,2]
step 3 uses SUBST to replace the left t1 of theorem 2 with the t2 of theorem 1.
We'd do this with
SUBST [(theorem-1, x)] ] `x = t1` theorem-2;;
With theorem-1 and theorem-2 referring to the theorems of step 1 & 2.
I believe line 3 says is
replace some number of occurrences of the lhs of the theorem of
line 1 in the theorem of line 2
I think the line 3 proof could be more descriptive than [SUBST 1,2], but it's
fine, anyone can figure this out, it's such a short proof.
While we here, don't you agree that John's INST replaces every free occurence
of ti?
INST : (term * term) list -> thm -> thm
When INST [t1,x1; ...; tn,xn] is applied to a theorem, it gives a new
theorem that systematically replaces free instances of each variable xi with
the corresponding term ti in both assumptions and conclusion.
A |- t
----------------------------------- INST_TYPE [t1,x1;...;tn,xn]
A[t1,...,tn/x1,...,xn]
|- t[t1,...,tn/x1,...,xn]
There is very little difference between FOL and HOL: the major data
structures are as follows.
FOL: term --> formula --> sequent --> theorem
HOL: type ---> term ------------------> sequent --> theorem
Thanks, I did not know that sequent was FOL lingo. I see there's Gentzen's
Sequent calculus
http://en.wikipedia.org/wiki/Sequent_calculus
and I know Freek and others talk about Gentzen.
--
Best,
Bill
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
