Hi Bill,
It can get quite confusing sometimes, especially when "," is involved. I
think people (or those that are not already super-familiar with the syntax)
intuitively expect mandatory surrounding parentheses around pairs/tuples.
But anyway, this should help you. In the following list for HOL Light,
higher items bind more tightly (i.e. have higher "precedence") than lower
items:
- function application
- type annotation
- all prefixes
- "," separators in set enumeration (i.e. { a, b, c })
- all infixes, including "," for pairs
- all binders, including "\" and "let", and "if"
- ";" separators in list enumeration (i.e. [ a; b; c ])
Note that this is just my own informal list, derived from observed
behaviour, and there might be errors in it. Please someone say if they find
an error!
Mark.
on 6/12/12 5:14 AM, Bill Richter <[email protected]> wrote:
> 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
>
>
>
------------------------------------------------------------------------------
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
