I'm trying to learn HOL Light by reading the tutorial, and I keep running into
things I don't understand. Maybe it's a good idea to have a thread for the
experts to straighten out beginners like me. Here's my latest problem, about
parenthesis and maybe precedence. I have an improved proof of the universal
property of the Cartesian product below (John's code, with my modified
definition of composition), but I don't understand why it works. I knew this
worked:
parse_as_infix("timesp",(20, "right"));;
let CartesianProductp = new_definition
`! X Y. X timesp Y = {pair:A#B | ? x y. pair = x,y /\ x IN X /\ y IN Y}`;;
let IN_CartesianProduct = thm `;
! X Y x:A y:B.
x,y IN X timesp Y <=> x IN X /\ y IN Y
by CartesianProductp, SET_RULE, PAIR_EQ`;;
But why do I need the variable pair? I wanted
parse_as_infix("timeb",(20, "right"));;
let CartesianProductb = new_definition
`! X Y. X timeb Y = {x,y:A#B | x IN X /\ y IN Y}`;;
let IN_CartesianProductb = thm `;
! X Y x:A y:B.
x,y IN X timeb Y <=> x IN X /\ y IN Y
by CartesianProductb, SET_RULE, PAIR_EQ`;;
But this theorem earns a #8 syntax or type error hol. So let's try
parentheses, as John does in the tutorial (the bug problem, p 64 ff):
parse_as_infix("timec",(20, "right"));;
let CartesianProductc = new_definition
`! X Y. X timec Y = {(x,y):A#B | x IN X /\ y IN Y}`;;
let IN_CartesianProductc = thm `;
! X Y x:A y:B.
x,y IN X timec Y <=> x IN X /\ y IN Y
by CartesianProductc, SET_RULE, PAIR_EQ`;;
Now this works! In spite of the fact that the def is printed without
parentheses:
# val CartesianProductc : thm = |- !X Y. X timec Y = {x,y | x IN X /\ y IN Y}
What's going on? Is this related to the parentheses here, which are printed:
FST;;
val it : thm = |- !x y. FST (x,y) = x
The comma infix "," has precedence 14. Is that lower than the precedence of
function application? There's a lot written in the tutorial about precedence,
but I found nothing about the precedence of function application, forall,
exists or lambda. Here's my improved code, which is due to John except my
definition of composition, first with the statements using math characters:
(*
parse_as_infix("∉",(11, "right"));;
parse_as_infix("∏",(20, "right"));;
parse_as_infix("∘",(20, "right"));;
parse_as_infix("→",(13,"right"));;
∉ |- ∀a l. a ∉ l ⇔ ¬(a ∈ l)
CartesianProduct
|- ∀ X Y. X ∏ Y = {x,y | x ∈ X ∧ y ∈ Y}
IN_CartesianProduct
|- ∀ X Y x y. x,y ∈ X ∏ Y ⇔ x ∈ X ∧ y ∈ Y
FunctionSpace
|- ∀ s t. s → t =
{f | (∀ x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. x ∉ s ⇒ f x = @y. T}
IN_FunctionSpace
|- ∀ s t f. f ∈ s → t ⇔
(∀ x. x ∈ s ⇒ f x ∈ t) ∧ ∀ x. x ∉ s ⇒ f x = @y. T
FunctionComposition
|- ∀ x f s g. (g ∘ (f,s)) x = (if x ∈ s then g (f x) else @y. T)
UniversalPropertyProduct
|- ∀ M A B f g.
f ∈ M → A ∧ g ∈ M → B
⇒ (∃! h. h ∈ M → A ∏ B ∧ FST ∘ (h,M) = f ∧ SND ∘ (h,M) = g)
*)
horizon := 0;;
timeout := 50;;
parse_as_infix("NOTIN",(11, "right"));;
parse_as_infix("times",(20, "right"));;
parse_as_infix("composition",(20, "right"));;
parse_as_infix("--->",(13,"right"));;
let NOTIN = new_definition
`! a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
let CartesianProduct = new_definition
`! X Y. X times Y = {(x,y):A#B | x IN X /\ y IN Y}`;;
let IN_CartesianProduct = thm `;
! X Y x:A y:B.
x,y IN X times Y <=> x IN X /\ y IN Y
by CartesianProduct, SET_RULE, PAIR_EQ`;;
let FunctionSpace = new_definition
`! s t. s ---> t = {f: A->B | (! x. x IN s ==> f x IN t) /\
! x. x NOTIN s ==> f x = @y. T}`;;
let IN_FunctionSpace = thm `;
! s: A->bool t: B->bool f: A->B. f IN s ---> t
<=> (! x. x IN s ==> f x IN t) /\ ! x. x NOTIN s ==> f x = @y. T
by FunctionSpace, SET_RULE`;;
let FunctionComposition = new_definition
`! f:A->B s:A->bool g:B->C x.
(g composition (f,s)) x = if x IN s then g (f x) else @y:C. T`;;
let UniversalPropertyProduct = thm `;
let M be mu->bool;
let A be alpha->bool;
let B be beta->bool;
let f be mu->alpha;
let g be mu->beta;
assume f IN M ---> A /\ g IN M ---> B [H1];
thus ?! h. h IN M ---> A times B /\ FST composition (h,M) = f /\ SND
composition (h,M) = g
proof
consider h such that
h = \x. if x IN M then f x,g x else @y. T;
! x. (x IN M ==> h x = f x,g x) /\ (x NOTIN M ==> h x = @y. T)
[hDef] by -, NOTIN;
! x. x IN M ==> h x IN A times B [hProd] by -, H1, IN_FunctionSpace,
IN_CartesianProduct;
! x. x IN M ==> FST (h x) = f x /\ SND (h x) = g x by hDef,
FST_DEF, SND_DEF, PAIR_EQ;
! x. (x IN M ==> (FST composition (h,M)) x = f x) /\ (x NOTIN M ==>
(FST composition (h,M)) x = f x) /\
(x IN M ==> (SND composition (h,M)) x = g x) /\ (x NOTIN M ==> (SND
composition (h,M)) x = g x) by FunctionComposition, NOTIN, -, H1,
IN_FunctionSpace;
h IN M ---> A times B /\ FST composition (h,M) = f /\ SND composition
(h,M) = g [hWorks] by hDef, hProd, IN_FunctionSpace, -, NOTIN, FUN_EQ_THM;
! k. (k IN M ---> A times B /\ FST composition (k,M) = f /\ SND
composition (k,M) = g) ==> h = k
proof
let k be mu->alpha#beta;
assume k IN M ---> A times B /\ FST composition (k,M) = f /\ SND
composition (k,M) = g [kWorks];
! x. x NOTIN M ==> k x = @y. T [kOffM] by -, IN_FunctionSpace;
! x. x IN M ==> k x = f x,g x
proof
let x be mu;
assume x IN M [xM];
FST (k x) = f x /\ SND (k x) = g x by -, kWorks, FunctionComposition;
k x = FST (k x), SND (k x) /\ FST (k x) = f x /\ SND (k x) = g x
by -, PAIR, kWorks;
qed by -, PAIR_EQ;
qed by hDef, -, kOffM, FUN_EQ_THM, NOTIN;
qed by hWorks, -, EXISTS_UNIQUE_THM;
`;;
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
