# HG changeset patch # User wenzelm # Date 1346096254 -7200 # Node ID b5758f5a469cdb592247a482c4cc92f9e86e0aa6 # Parent ac15a85e92824b9f0eafcec183f8842af40838ef more standard document preparation within session context; diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/HOL-eg.txt --- a/doc-src/HOL/HOL-eg.txt Mon Aug 27 21:30:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,151 +0,0 @@ -(**** HOL examples -- process using Doc/tout HOL-eg.txt ****) - -Pretty.setmargin 72; (*existing macros just allow this margin*) -print_depth 0; - - -(*** Conjunction rules ***) - -val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q"; -by (resolve_tac [and_def RS ssubst] 1); -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [mp RS mp] 1); -by (REPEAT (resolve_tac prems 1)); -val conjI = result(); - -val prems = goal HOL_Rule.thy "[| P & Q |] ==> P"; -prths (prems RL [and_def RS subst]); -prths (prems RL [and_def RS subst] RL [spec] RL [mp]); -by (resolve_tac it 1); -by (REPEAT (ares_tac [impI] 1)); -val conjunct1 = result(); - - -(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) - -goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; -by (resolve_tac [notI] 1); -by (eresolve_tac [rangeE] 1); -by (eresolve_tac [equalityCE] 1); -by (dresolve_tac [CollectD] 1); -by (contr_tac 1); -by (swap_res_tac [CollectI] 1); -by (assume_tac 1); - -choplev 0; -by (best_tac (set_cs addSEs [equalityCE]) 1); - - -goal Set.thy "! f:: 'a=>'a set. ! x. ~ f(x) = ?S(f)"; -by (REPEAT (resolve_tac [allI,notI] 1)); -by (eresolve_tac [equalityCE] 1); -by (dresolve_tac [CollectD] 1); -by (contr_tac 1); -by (swap_res_tac [CollectI] 1); -by (assume_tac 1); - -choplev 0; -by (best_tac (set_cs addSEs [equalityCE]) 1); - - -goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? a. f(a) = S)"; -by (best_tac (set_cs addSEs [equalityCE]) 1); - - - - -> val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q"; -Level 0 -P & Q - 1. P & Q -> by (resolve_tac [and_def RS ssubst] 1); -Level 1 -P & Q - 1. ! R. (P --> Q --> R) --> R -> by (resolve_tac [allI] 1); -Level 2 -P & Q - 1. !!R. (P --> Q --> R) --> R -> by (resolve_tac [impI] 1); -Level 3 -P & Q - 1. !!R. P --> Q --> R ==> R -> by (eresolve_tac [mp RS mp] 1); -Level 4 -P & Q - 1. !!R. P - 2. !!R. Q -> by (REPEAT (resolve_tac prems 1)); -Level 5 -P & Q -No subgoals! - - - -> val prems = goal HOL_Rule.thy "[| P & Q |] ==> P"; -Level 0 -P - 1. P -> prths (prems RL [and_def RS subst]); -! R. (P --> Q --> R) --> R [P & Q] -P & Q [P & Q] - -> prths (prems RL [and_def RS subst] RL [spec] RL [mp]); -P --> Q --> ?Q ==> ?Q [P & Q] - -> by (resolve_tac it 1); -Level 1 -P - 1. P --> Q --> P -> by (REPEAT (ares_tac [impI] 1)); -Level 2 -P -No subgoals! - - - - -> goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; -Level 0 -~?S : range(f) - 1. ~?S : range(f) -> by (resolve_tac [notI] 1); -Level 1 -~?S : range(f) - 1. ?S : range(f) ==> False -> by (eresolve_tac [rangeE] 1); -Level 2 -~?S : range(f) - 1. !!x. ?S = f(x) ==> False -> by (eresolve_tac [equalityCE] 1); -Level 3 -~?S : range(f) - 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False - 2. !!x. [| ~?c3(x) : ?S; ~?c3(x) : f(x) |] ==> False -> by (dresolve_tac [CollectD] 1); -Level 4 -~{x. ?P7(x)} : range(f) - 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False - 2. !!x. [| ~?c3(x) : {x. ?P7(x)}; ~?c3(x) : f(x) |] ==> False -> by (contr_tac 1); -Level 5 -~{x. ~x : f(x)} : range(f) - 1. !!x. [| ~x : {x. ~x : f(x)}; ~x : f(x) |] ==> False -> by (swap_res_tac [CollectI] 1); -Level 6 -~{x. ~x : f(x)} : range(f) - 1. !!x. [| ~x : f(x); ~False |] ==> ~x : f(x) -> by (assume_tac 1); -Level 7 -~{x. ~x : f(x)} : range(f) -No subgoals! - -> choplev 0; -Level 0 -~?S : range(f) - 1. ~?S : range(f) -> by (best_tac (set_cs addSEs [equalityCE]) 1); -Level 1 -~{x. ~x : f(x)} : range(f) -No subgoals! diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/HOL-rules.txt --- a/doc-src/HOL/HOL-rules.txt Mon Aug 27 21:30:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,403 +0,0 @@ -ruleshell.ML lemmas.ML set.ML fun.ML subset.ML equalities.ML prod.ML sum.ML wf.ML mono.ML fixedpt.ML nat.ML list.ML ----------------------------------------------------------------- -ruleshell.ML - -\idx{refl} t = t::'a -\idx{subst} [| s = t; P(s) |] ==> P(t::'a) -\idx{abs},!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))) -\idx{disch} (P ==> Q) ==> P-->Q -\idx{mp} [| P-->Q; P |] ==> Q - -\idx{True_def} True = ((%x.x)=(%x.x)) -\idx{All_def} All = (%P. P = (%x.True)) -\idx{Ex_def} Ex = (%P. P(Eps(P))) -\idx{False_def} False = (!P.P) -\idx{not_def} not = (%P. P-->False) -\idx{and_def} op & = (%P Q. !R. (P-->Q-->R) --> R) -\idx{or_def} op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R) -\idx{Ex1_def} Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x)) - -\idx{iff} (P-->Q) --> (Q-->P) --> (P=Q) -\idx{True_or_False} (P=True) | (P=False) -\idx{select} P(x::'a) --> P(Eps(P)) - -\idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y) -\idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x))) -\idx{Cond_def} Cond = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y)) - ----------------------------------------------------------------- -lemmas.ML - -\idx{sym} s=t ==> t=s -\idx{trans} [| r=s; s=t |] ==> r=t -\idx{box_equals} - [| a=b; a=c; b=d |] ==> c=d -\idx{ap_term} s=t ==> f(s)=f(t) -\idx{ap_thm} s::'a=>'b = t ==> s(x)=t(x) -\idx{cong} - [| f = g; x::'a = y |] ==> f(x) = g(y) -\idx{iffI} - [| P ==> Q; Q ==> P |] ==> P=Q -\idx{iffD1} [| P=Q; Q |] ==> P -\idx{iffE} - [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R -\idx{eqTrueI} P ==> P=True -\idx{eqTrueE} P=True ==> P -\idx{allI} (!!x::'a. P(x)) ==> !x. P(x) -\idx{spec} !x::'a.P(x) ==> P(x) -\idx{allE} [| !x.P(x); P(x) ==> R |] ==> R -\idx{all_dupE} - [| ! x.P(x); [| P(x); ! x.P(x) |] ==> R - |] ==> R -\idx{FalseE} False ==> P -\idx{False_neq_True} False=True ==> P -\idx{notI} (P ==> False) ==> ~P -\idx{notE} [| ~P; P |] ==> R -\idx{impE} [| P-->Q; P; Q ==> R |] ==> R -\idx{rev_mp} [| P; P --> Q |] ==> Q -\idx{contrapos} [| ~Q; P==>Q |] ==> ~P -\idx{exI} P(x) ==> ? x::'a.P(x) -\idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q - -\idx{conjI} [| P; Q |] ==> P&Q -\idx{conjunct1} [| P & Q |] ==> P -\idx{conjunct2} [| P & Q |] ==> Q -\idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R -\idx{disjI1} P ==> P|Q -\idx{disjI2} Q ==> P|Q -\idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R -\idx{ccontr} (~P ==> False) ==> P -\idx{classical} (~P ==> P) ==> P -\idx{notnotD} ~~P ==> P -\idx{ex1I} - [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x) -\idx{ex1E} - [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R -\idx{select_equality} - [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a -\idx{disjCI} (~Q ==> P) ==> P|Q -\idx{excluded_middle} ~P | P -\idx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R -\idx{iffCE} - [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R -\idx{exCI} (! x. ~P(x) ==> P(a)) ==> ? x.P(x) -\idx{swap} ~P ==> (~Q ==> P) ==> Q - ----------------------------------------------------------------- -simpdata.ML - -\idx{if_True} Cond(True,x,y) = x -\idx{if_False} Cond(False,x,y) = y -\idx{if_P} P ==> Cond(P,x,y) = x -\idx{if_not_P} ~P ==> Cond(P,x,y) = y -\idx{expand_if} - P(Cond(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y))) - ----------------------------------------------------------------- -\idx{set.ML} - -\idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\} -\idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a) -\idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B - -\idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x) -\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x) -\idx{subset_def} A <= B == ! x:A. x:B -\idx{Un_def} A Un B == \{x.x:A | x:B\} -\idx{Int_def} A Int B == \{x.x:A & x:B\} -\idx{Compl_def} Compl(A) == \{x. ~x:A\} -\idx{Inter_def} Inter(S) == \{x. ! A:S. x:A\} -\idx{Union_def} Union(S) == \{x. ? A:S. x:A\} -\idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\} -\idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\} -\idx{mono_def} mono(f) == (!A B. A <= B --> f(A) <= f(B)) -\idx{image_def} f``A == \{y. ? x:A. y=f(x)\} -\idx{singleton_def} \{a\} == \{x.x=a\} -\idx{range_def} range(f) == \{y. ? x. y=f(x)\} -\idx{One_One_def} One_One(f) == ! x y. f(x)=f(y) --> x=y -\idx{One_One_on_def} One_One_on(f,A) == !x y. x:A --> y:A --> f(x)=f(y) --> x=y -\idx{Onto_def} Onto(f) == ! y. ? x. y=f(x) - - -\idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\} - -\idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x) -\idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x) -\idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q - -\idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x) -\idx{bexCI} [| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A.P(x) -\idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q - -\idx{ball_cong} - [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==> - (! x:A. P(x)) = (! x:A'. P'(x)) - -\idx{bex_cong} - [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==> - (? x:A. P(x)) = (? x:A'. P'(x)) - -\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B -\idx{subsetD} [| A <= B; c:A |] ==> c:B -\idx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P - -\idx{subset_refl} A <= A -\idx{subset_antisym} [| A <= B; B <= A |] ==> A = B -\idx{subset_trans} [| A<=B; B<=C |] ==> A<=C - -\idx{equalityD1} A = B ==> A<=B -\idx{equalityD2} A = B ==> B<=A -\idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P - -\idx{singletonI} a : \{a\} -\idx{singletonD} b : \{a\} ==> b=a - -\idx{imageI} [| x:A |] ==> f(x) : f``A -\idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P - -\idx{rangeI} f(x) : range(f) -\idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P - -\idx{UnionI} [| X:C; A:X |] ==> A : Union(C) -\idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R - -\idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C) -\idx{InterD} [| A : Inter(C); X:C |] ==> A:X -\idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R - -\idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x)) -\idx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R - -\idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x)) -\idx{INT_D} [| b : (INT x:A. B(x)); a:A |] ==> b: B(a) -\idx{INT_E} [| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R - -\idx{UnI1} c:A ==> c : A Un B -\idx{UnI2} c:B ==> c : A Un B -\idx{UnCI} (~c:B ==> c:A) ==> c : A Un B -\idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P - -\idx{IntI} [| c:A; c:B |] ==> c : A Int B -\idx{IntD1} c : A Int B ==> c:A -\idx{IntD2} c : A Int B ==> c:B -\idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P - -\idx{ComplI} [| c:A ==> False |] ==> c : Compl(A) -\idx{ComplD} [| c : Compl(A) |] ==> ~c:A - -\idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f) -\idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B) - - ----------------------------------------------------------------- -\idx{fun.ML} - -\idx{One_OneI} [| !! x y. f(x) = f(y) ==> x=y |] ==> One_One(f) -\idx{One_One_inverseI} (!!x. g(f(x)) = x) ==> One_One(f) -\idx{One_OneD} [| One_One(f); f(x) = f(y) |] ==> x=y - -\idx{Inv_f_f} One_One(f) ==> Inv(f,f(x)) = x -\idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y - -\idx{Inv_injective} - [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y - -\idx{One_One_onI} - (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> One_One_on(f,A) - -\idx{One_One_on_inverseI} - (!!x. x:A ==> g(f(x)) = x) ==> One_One_on(f,A) - -\idx{One_One_onD} - [| One_One_on(f,A); f(x)=f(y); x:A; y:A |] ==> x=y - -\idx{One_One_on_contraD} - [| One_One_on(f,A); ~x=y; x:A; y:A |] ==> ~ f(x)=f(y) - - ----------------------------------------------------------------- -\idx{subset.ML} - -\idx{Union_upper} B:A ==> B <= Union(A) -\idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C - -\idx{Inter_lower} B:A ==> Inter(A) <= B -\idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A) - -\idx{Un_upper1} A <= A Un B -\idx{Un_upper2} B <= A Un B -\idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C - -\idx{Int_lower1} A Int B <= A -\idx{Int_lower2} A Int B <= B -\idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B - - ----------------------------------------------------------------- -\idx{equalities.ML} - -\idx{Int_absorb} A Int A = A -\idx{Int_commute} A Int B = B Int A -\idx{Int_assoc} (A Int B) Int C = A Int (B Int C) -\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) - -\idx{Un_absorb} A Un A = A -\idx{Un_commute} A Un B = B Un A -\idx{Un_assoc} (A Un B) Un C = A Un (B Un C) -\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) - -\idx{Compl_disjoint} A Int Compl(A) = \{x.False\} -\idx{Compl_partition A Un Compl(A) = \{x.True\} -\idx{double_complement} Compl(Compl(A)) = A - - -\idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B) -\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B) - -\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) -\idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C) -\idx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C) - -\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B) -\idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C) -\idx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C) - - ----------------------------------------------------------------- -prod.ML - - mixfix = [ Delimfix((1<_,/_>), ['a,'b] => ('a,'b)prod, Pair), - TInfixl(*, prod, 20) ], -thy = extend_theory Set.thy Prod - [([prod],([[term],[term]],term))], - ([fst], 'a * 'b => 'a), - ([snd], 'a * 'b => 'b), - ([split], ['a * 'b, ['a,'b]=>'c] => 'c)], -\idx{fst_def} fst(p) == @a. ? b. p = ), -\idx{snd_def} snd(p) == @b. ? a. p = ), -\idx{split_def} split(p,c) == c(fst(p),snd(p))) - -\idx{Pair_inject} [| = ; [| a=a'; b=b' |] ==> R |] ==> R - -\idx{fst_conv} fst() = a -\idx{snd_conv} snd() = b -\idx{split_conv} split(, c) = c(a,b) - -\idx{surjective_pairing} p = - ----------------------------------------------------------------- -sum.ML - - mixfix = [TInfixl(+, sum, 10)], -thy = extend_theory Prod.thy sum - [([sum], ([[term],[term]],term))], - [Inl], 'a => 'a+'b), - [Inr], 'b => 'a+'b), - [when], ['a+'b, 'a=>'c, 'b=>'c] =>'c)], -\idx{when_def} when == (%p f g. @z. (!x. p=Inl(x) --> z=f(x)) - & (!y. p=Inr(y) --> z=g(y)))) - -\idx{Inl_not_Inr} ~ (Inl(a) = Inr(b)) - -\idx{One_One_Inl} One_One(Inl) - -\idx{One_One_Inr} One_One(Inr) - -\idx{when_Inl_conv} when(Inl(x), f, g) = f(x) - -\idx{when_Inr_conv} when(Inr(x), f, g) = g(x) - -\idx{sumE} - [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) - |] ==> P(s) - -\idx{surjective_sum} when(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s) - - -???????????????????????????????????????????????????????????????? -trancl? - ----------------------------------------------------------------- -nat.ML - - Sext\{mixfix=[Delimfix(0, nat, 0), - Infixl(<,[nat,nat] => bool,50)], -thy = extend_theory Trancl.thy Nat -[nat], ([],term)) -[nat_case], [nat, 'a, nat=>'a] =>'a), -[pred_nat],nat*nat) set), -[nat_rec], [nat, 'a, [nat, 'a]=>'a] => 'a) - -\idx{nat_case_def} nat_case == (%n a f. @z. (n=0 --> z=a) - & (!x. n=Suc(x) --> z=f(x)))), -\idx{pred_nat_def} pred_nat == \{p. ? n. p = \} ), -\idx{less_def} m:trancl(pred_nat)), -\idx{nat_rec_def} - nat_rec(n,c,d) == wfrec(trancl(pred_nat), - %rec l. nat_case(l, c, %m. d(m,rec(m))), - n) ) - -\idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n) - - -\idx{Suc_not_Zero} ~ (Suc(m) = 0) -\idx{One_One_Suc} One_One(Suc) -\idx{n_not_Suc_n} ~(n=Suc(n)) - -\idx{nat_case_0_conv} nat_case(0, a, f) = a - -\idx{nat_case_Suc_conv} nat_case(Suc(k), a, f) = f(k) - -\idx{pred_natI} : pred_nat -\idx{pred_natE} - [| p : pred_nat; !!x n. [| p = |] ==> R - |] ==> R - -\idx{wf_pred_nat} wf(pred_nat) - -\idx{nat_rec_0_conv} nat_rec(0,c,h) = c - -\idx{nat_rec_Suc_conv} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h)) - - -(*** Basic properties of less than ***) -\idx{less_trans} [| i i ~m P(m) |] ==> P(n) |] ==> P(n) - -\idx{less_linear} m 'a list), - ([list_rec], ['a list, 'b, ['a ,'a list, 'b]=>'b] => 'b), - ([list_all], ('a => bool) => ('a list => bool)), - ([map], ('a=>'b) => ('a list => 'b list)) - -\idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r)) ) - -\idx{list_induct} - [| P(Nil); - !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |] ==> P(l) - -\idx{Cons_not_Nil} ~ Cons(x,xs) = Nil -\idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys) - -\idx{list_rec_Nil_conv} list_rec(Nil,c,h) = c -\idx{list_rec_Cons_conv} list_rec(Cons(a,l), c, h) = - h(a, l, list_rec(l,c,h)) - -\idx{map_Nil_conv} map(f,Nil) = Nil -\idx{map_Cons_conv} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs)) - diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Mon Aug 27 21:30:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2089 +0,0 @@ -\chapter{Higher-Order Logic} -\index{higher-order logic|(} -\index{HOL system@{\sc hol} system} - -\begin{figure} -\begin{constants} - \it name &\it meta-type & \it description \\ - \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ - \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\ - \cdx{True} & $bool$ & tautology ($\top$) \\ - \cdx{False} & $bool$ & absurdity ($\bot$) \\ - \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\ - \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder -\end{constants} -\subcaption{Constants} - -\begin{constants} -\index{"@@{\tt\at} symbol} -\index{*"! symbol}\index{*"? symbol} -\index{*"?"! symbol}\index{*"E"X"! symbol} - \it symbol &\it name &\it meta-type & \it description \\ - \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & - Hilbert description ($\varepsilon$) \\ - \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ & - universal quantifier ($\forall$) \\ - \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & - existential quantifier ($\exists$) \\ - \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & - unique existence ($\exists!$)\\ - \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & - least element -\end{constants} -\subcaption{Binders} - -\begin{constants} -\index{*"= symbol} -\index{&@{\tt\&} symbol} -\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working -\index{*"-"-"> symbol} - \it symbol & \it meta-type & \it priority & \it description \\ - \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & - Left 55 & composition ($\circ$) \\ - \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\ - \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ - \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & - less than or equals ($\leq$)\\ - \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ - \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ - \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) -\end{constants} -\subcaption{Infixes} -\caption{Syntax of \texttt{HOL}} \label{hol-constants} -\end{figure} - - -\begin{figure} -\index{*let symbol} -\index{*in symbol} -\dquotes -\[\begin{array}{rclcl} - term & = & \hbox{expression of class~$term$} \\ - & | & "SOME~" id " . " formula - & | & "\at~" id " . " formula \\ - & | & - \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ - & | & - \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\ - & | & "LEAST"~ id " . " formula \\[2ex] - formula & = & \hbox{expression of type~$bool$} \\ - & | & term " = " term \\ - & | & term " \ttilde= " term \\ - & | & term " < " term \\ - & | & term " <= " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & "ALL~" id~id^* " . " formula - & | & "!~~~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula - & | & "?~~~" id~id^* " . " formula \\ - & | & "EX!~" id~id^* " . " formula - & | & "?!~~" id~id^* " . " formula \\ - \end{array} -\] -\caption{Full grammar for HOL} \label{hol-grammar} -\end{figure} - - -\section{Syntax} - -Figure~\ref{hol-constants} lists the constants (including infixes and -binders), while Fig.\ts\ref{hol-grammar} presents the grammar of -higher-order logic. Note that $a$\verb|~=|$b$ is translated to -$\lnot(a=b)$. - -\begin{warn} - HOL has no if-and-only-if connective; logical equivalence is expressed using - equality. But equality has a high priority, as befitting a relation, while - if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$ - abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$ - to mean logical equivalence, enclose both operands in parentheses. -\end{warn} - -\subsection{Types and overloading} -The universal type class of higher-order terms is called~\cldx{term}. -By default, explicit type variables have class \cldx{term}. In -particular the equality symbol and quantifiers are polymorphic over -class \texttt{term}. - -The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, -formulae are terms. The built-in type~\tydx{fun}, which constructs -function types, is overloaded with arity {\tt(term,\thinspace - term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt - term} if $\sigma$ and~$\tau$ do, allowing quantification over -functions. - -HOL allows new types to be declared as subsets of existing types, -either using the primitive \texttt{typedef} or the more convenient -\texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}). - -Several syntactic type classes --- \cldx{plus}, \cldx{minus}, -\cldx{times} and -\cldx{power} --- permit overloading of the operators {\tt+},\index{*"+ - symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol} -and \verb|^|.\index{^@\verb.^. symbol} -% -They are overloaded to denote the obvious arithmetic operations on types -\tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the -exponent always has type~\tdx{nat}.) Non-arithmetic overloadings are also -done: the operator {\tt-} can denote set difference, while \verb|^| can -denote exponentiation of relations (iterated composition). Unary minus is -also written as~{\tt-} and is overloaded like its 2-place counterpart; it even -can stand for set complement. - -The constant \cdx{0} is also overloaded. It serves as the zero element of -several types, of which the most important is \tdx{nat} (the natural -numbers). The type class \cldx{plus_ac0} comprises all types for which 0 -and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These -types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also -multisets. The summation operator \cdx{setsum} is available for all types in -this class. - -Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order -signatures. The relations $<$ and $\leq$ are polymorphic over this -class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and -the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass -\cldx{order} of \cldx{ord} which axiomatizes the types that are partially -ordered with respect to~$\leq$. A further subclass \cldx{linorder} of -\cldx{order} axiomatizes linear orderings. -For details, see the file \texttt{Ord.thy}. - -If you state a goal containing overloaded functions, you may need to include -type constraints. Type inference may otherwise make the goal more -polymorphic than you intended, with confusing results. For example, the -variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type -$\alpha::\{ord,plus\}$, although you may have expected them to have some -numeric type, e.g. $nat$. Instead you should have stated the goal as -$(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have -type $nat$. - -\begin{warn} - If resolution fails for no obvious reason, try setting - \ttindex{show_types} to \texttt{true}, causing Isabelle to display - types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as - well, causing Isabelle to display type classes and sorts. - - \index{unification!incompleteness of} - Where function types are involved, Isabelle's unification code does not - guarantee to find instantiations for type variables automatically. Be - prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, - possibly instantiating type variables. Setting - \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report - omitted search paths during unification.\index{tracing!of unification} -\end{warn} - - -\subsection{Binders} - -Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$ -satisfying~$P$, if such exists. Since all terms in HOL denote something, a -description is always meaningful, but we do not know its value unless $P$ -defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x. -P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}. - -Existential quantification is defined by -\[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] -The unique existence quantifier, $\exists!x. P$, is defined in terms -of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested -quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates -$\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there -exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. - -\medskip - -\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The -basic Isabelle/HOL binders have two notations. Apart from the usual -\texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also -supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ -and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be -followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a -quantification. Both notations are accepted for input. The print mode -``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by -passing option \texttt{-m HOL} to the \texttt{isabelle} executable), -then~{\tt!}\ and~{\tt?}\ are displayed. - -\medskip - -If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a -variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined -to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see -Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ -choice operator, so \texttt{Least} is always meaningful, but may yield -nothing useful in case there is not a unique least element satisfying -$P$.\footnote{Class $ord$ does not require much of its instances, so - $\leq$ need not be a well-ordering, not even an order at all!} - -\medskip All these binders have priority 10. - -\begin{warn} -The low priority of binders means that they need to be enclosed in -parenthesis when they occur in the context of other operations. For example, -instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$. -\end{warn} - - -\subsection{The let and case constructions} -Local abbreviations can be introduced by a \texttt{let} construct whose -syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into -the constant~\cdx{Let}. It can be expanded by rewriting with its -definition, \tdx{Let_def}. - -HOL also defines the basic syntax -\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] -as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} -and \sdx{of} are reserved words. Initially, this is mere syntax and has no -logical meaning. By declaring translations, you can cause instances of the -\texttt{case} construct to denote applications of particular case operators. -This is what happens automatically for each \texttt{datatype} definition -(see~{\S}\ref{sec:HOL:datatype}). - -\begin{warn} -Both \texttt{if} and \texttt{case} constructs have as low a priority as -quantifiers, which requires additional enclosing parentheses in the context -of most other operations. For example, instead of $f~x = {\tt if\dots -then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots -else\dots})$. -\end{warn} - -\section{Rules of inference} - -\begin{figure} -\begin{ttbox}\makeatother -\tdx{refl} t = (t::'a) -\tdx{subst} [| s = t; P s |] ==> P (t::'a) -\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x) -\tdx{impI} (P ==> Q) ==> P-->Q -\tdx{mp} [| P-->Q; P |] ==> Q -\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) -\tdx{someI} P(x::'a) ==> P(@x. P x) -\tdx{True_or_False} (P=True) | (P=False) -\end{ttbox} -\caption{The \texttt{HOL} rules} \label{hol-rules} -\end{figure} - -Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with -their~{\ML} names. Some of the rules deserve additional comments: -\begin{ttdescription} -\item[\tdx{ext}] expresses extensionality of functions. -\item[\tdx{iff}] asserts that logically equivalent formulae are - equal. -\item[\tdx{someI}] gives the defining property of the Hilbert - $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule - \tdx{some_equality} (see below) is often easier to use. -\item[\tdx{True_or_False}] makes the logic classical.\footnote{In - fact, the $\varepsilon$-operator already makes the logic classical, as - shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.} -\end{ttdescription} - - -\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message -\begin{ttbox}\makeatother -\tdx{True_def} True == ((\%x::bool. x)=(\%x. x)) -\tdx{All_def} All == (\%P. P = (\%x. True)) -\tdx{Ex_def} Ex == (\%P. P(@x. P x)) -\tdx{False_def} False == (!P. P) -\tdx{not_def} not == (\%P. P-->False) -\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R) -\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R) -\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x)) - -\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x)) -\tdx{if_def} If P x y == - (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y)) -\tdx{Let_def} Let s f == f s -\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" -\end{ttbox} -\caption{The \texttt{HOL} definitions} \label{hol-defs} -\end{figure} - - -HOL follows standard practice in higher-order logic: only a few connectives -are taken as primitive, with the remainder defined obscurely -(Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the -corresponding definitions \cite[page~270]{mgordon-hol} using -object-equality~({\tt=}), which is possible because equality in higher-order -logic may equate formulae and even functions over formulae. But theory~HOL, -like all other Isabelle theories, uses meta-equality~({\tt==}) for -definitions. -\begin{warn} -The definitions above should never be expanded and are shown for completeness -only. Instead users should reason in terms of the derived rules shown below -or, better still, using high-level tactics. -\end{warn} - -Some of the rules mention type variables; for example, \texttt{refl} -mentions the type variable~{\tt'a}. This allows you to instantiate -type variables explicitly by calling \texttt{res_inst_tac}. - - -\begin{figure} -\begin{ttbox} -\tdx{sym} s=t ==> t=s -\tdx{trans} [| r=s; s=t |] ==> r=t -\tdx{ssubst} [| t=s; P s |] ==> P t -\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d -\tdx{arg_cong} x = y ==> f x = f y -\tdx{fun_cong} f = g ==> f x = g x -\tdx{cong} [| f = g; x = y |] ==> f x = g y -\tdx{not_sym} t ~= s ==> s ~= t -\subcaption{Equality} - -\tdx{TrueI} True -\tdx{FalseE} False ==> P - -\tdx{conjI} [| P; Q |] ==> P&Q -\tdx{conjunct1} [| P&Q |] ==> P -\tdx{conjunct2} [| P&Q |] ==> Q -\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R - -\tdx{disjI1} P ==> P|Q -\tdx{disjI2} Q ==> P|Q -\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R - -\tdx{notI} (P ==> False) ==> ~ P -\tdx{notE} [| ~ P; P |] ==> R -\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R -\subcaption{Propositional logic} - -\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q -\tdx{iffD1} [| P=Q; P |] ==> Q -\tdx{iffD2} [| P=Q; Q |] ==> P -\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R -\subcaption{Logical equivalence} - -\end{ttbox} -\caption{Derived rules for HOL} \label{hol-lemmas1} -\end{figure} -% -%\tdx{eqTrueI} P ==> P=True -%\tdx{eqTrueE} P=True ==> P - - -\begin{figure} -\begin{ttbox}\makeatother -\tdx{allI} (!!x. P x) ==> !x. P x -\tdx{spec} !x. P x ==> P x -\tdx{allE} [| !x. P x; P x ==> R |] ==> R -\tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R - -\tdx{exI} P x ==> ? x. P x -\tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q - -\tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x -\tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R - |] ==> R - -\tdx{some_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a -\subcaption{Quantifiers and descriptions} - -\tdx{ccontr} (~P ==> False) ==> P -\tdx{classical} (~P ==> P) ==> P -\tdx{excluded_middle} ~P | P - -\tdx{disjCI} (~Q ==> P) ==> P|Q -\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x -\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R -\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R -\tdx{notnotD} ~~P ==> P -\tdx{swap} ~P ==> (~Q ==> P) ==> Q -\subcaption{Classical logic} - -\tdx{if_P} P ==> (if P then x else y) = x -\tdx{if_not_P} ~ P ==> (if P then x else y) = y -\tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y)) -\subcaption{Conditionals} -\end{ttbox} -\caption{More derived rules} \label{hol-lemmas2} -\end{figure} - -Some derived rules are shown in Figures~\ref{hol-lemmas1} -and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules -for the logical connectives, as well as sequent-style elimination rules for -conjunctions, implications, and universal quantifiers. - -Note the equality rules: \tdx{ssubst} performs substitution in -backward proofs, while \tdx{box_equals} supports reasoning by -simplifying both sides of an equation. - -The following simple tactics are occasionally useful: -\begin{ttdescription} -\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI} - repeatedly to remove all outermost universal quantifiers and implications - from subgoal $i$. -\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on - $P$ for subgoal $i$: the latter is replaced by two identical subgoals with - the added assumptions $P$ and $\lnot P$, respectively. -\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then - \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining - from an induction hypothesis. As a generalization of \texttt{mp_tac}, - if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and - $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables) - then it replaces the universally quantified implication by $Q \vec{a}$. - It may instantiate unknowns. It fails if it can do nothing. -\end{ttdescription} - - -\begin{figure} -\begin{center} -\begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ -\index{{}@\verb'{}' symbol} - \verb|{}| & $\alpha\,set$ & the empty set \\ - \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ - & insertion of element \\ - \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ - & comprehension \\ - \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ - & intersection over a set\\ - \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ - & union over a set\\ - \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ - &set of sets intersection \\ - \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ - &set of sets union \\ - \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ - & powerset \\[1ex] - \cdx{range} & $(\alpha\To\beta )\To\beta\,set$ - & range of a function \\[1ex] - \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ - & bounded quantifiers -\end{tabular} -\end{center} -\subcaption{Constants} - -\begin{center} -\begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it priority & \it description \\ - \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & - intersection\\ - \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & - union -\end{tabular} -\end{center} -\subcaption{Binders} - -\begin{center} -\index{*"`"` symbol} -\index{*": symbol} -\index{*"<"= symbol} -\begin{tabular}{rrrr} - \it symbol & \it meta-type & \it priority & \it description \\ - \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$ - & Left 90 & image \\ - \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ - & Left 70 & intersection ($\int$) \\ - \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ - & Left 65 & union ($\un$) \\ - \tt: & $[\alpha ,\alpha\,set]\To bool$ - & Left 50 & membership ($\in$) \\ - \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ - & Left 50 & subset ($\subseteq$) -\end{tabular} -\end{center} -\subcaption{Infixes} -\caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax} -\end{figure} - - -\begin{figure} -\begin{center} \tt\frenchspacing -\index{*"! symbol} -\begin{tabular}{rrr} - \it external & \it internal & \it description \\ - $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm not in\\ - {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ - {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) & - \rm comprehension \\ - \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ & - \rm intersection \\ - \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ & - \rm union \\ - \sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ & - Ball $A$ $\lambda x.\ P[x]$ & - \rm bounded $\forall$ \\ - \sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $x$:$A$.\ $P[x]$ & - Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$ -\end{tabular} -\end{center} -\subcaption{Translations} - -\dquotes -\[\begin{array}{rclcl} - term & = & \hbox{other terms\ldots} \\ - & | & "{\ttlbrace}{\ttrbrace}" \\ - & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ - & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\ - & | & term " `` " term \\ - & | & term " Int " term \\ - & | & term " Un " term \\ - & | & "INT~~" id ":" term " . " term \\ - & | & "UN~~~" id ":" term " . " term \\ - & | & "INT~~" id~id^* " . " term \\ - & | & "UN~~~" id~id^* " . " term \\[2ex] - formula & = & \hbox{other formulae\ldots} \\ - & | & term " : " term \\ - & | & term " \ttilde: " term \\ - & | & term " <= " term \\ - & | & "ALL " id ":" term " . " formula - & | & "!~" id ":" term " . " formula \\ - & | & "EX~~" id ":" term " . " formula - & | & "?~" id ":" term " . " formula \\ - \end{array} -\] -\subcaption{Full Grammar} -\caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2} -\end{figure} - - -\section{A formulation of set theory} -Historically, higher-order logic gives a foundation for Russell and -Whitehead's theory of classes. Let us use modern terminology and call them -{\bf sets}, but note that these sets are distinct from those of ZF set theory, -and behave more like ZF classes. -\begin{itemize} -\item -Sets are given by predicates over some type~$\sigma$. Types serve to -define universes for sets, but type-checking is still significant. -\item -There is a universal set (for each type). Thus, sets have complements, and -may be defined by absolute comprehension. -\item -Although sets may contain other sets as elements, the containing set must -have a more complex type. -\end{itemize} -Finite unions and intersections have the same behaviour in HOL as they do -in~ZF. In HOL the intersection of the empty set is well-defined, denoting the -universal set for the given type. - -\subsection{Syntax of set theory}\index{*set type} -HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially -the same as $\alpha\To bool$. The new type is defined for clarity and to -avoid complications involving function types in unification. The isomorphisms -between the two types are declared explicitly. They are very natural: -\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :} -maps in the other direction (ignoring argument order). - -Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax -translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new -constructs. Infix operators include union and intersection ($A\un B$ -and $A\int B$), the subset and membership relations, and the image -operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to -$\lnot(a\in b)$. - -The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in -the obvious manner using~\texttt{insert} and~$\{\}$: -\begin{eqnarray*} - \{a, b, c\} & \equiv & - \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) -\end{eqnarray*} - -The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of -suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain -free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x. -P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF; -the type of~$x$ implicitly restricts the comprehension. - -The set theory defines two {\bf bounded quantifiers}: -\begin{eqnarray*} - \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ - \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] -\end{eqnarray*} -The constants~\cdx{Ball} and~\cdx{Bex} are defined -accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may -write\index{*"! symbol}\index{*"? symbol} -\index{*ALL symbol}\index{*EX symbol} -% -\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The -original notation of Gordon's {\sc hol} system is supported as well: -\texttt{!}\ and \texttt{?}. - -Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and -$\bigcap@{x\in A}B[x]$, are written -\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and -\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}. - -Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x -B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and -\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous -union and intersection operators when $A$ is the universal set. - -The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are -not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$, -respectively. - - - -\begin{figure} \underscoreon -\begin{ttbox} -\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a -\tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A - -\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace} -\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B -\tdx{Ball_def} Ball A P == ! x. x:A --> P x -\tdx{Bex_def} Bex A P == ? x. x:A & P x -\tdx{subset_def} A <= B == ! x:A. x:B -\tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace} -\tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace} -\tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace} -\tdx{Compl_def} -A == {\ttlbrace}x. ~ x:A{\ttrbrace} -\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} -\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} -\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B -\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B -\tdx{Inter_def} Inter S == (INT x:S. x) -\tdx{Union_def} Union S == (UN x:S. x) -\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} -\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace} -\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace} -\end{ttbox} -\caption{Rules of the theory \texttt{Set}} \label{hol-set-rules} -\end{figure} - - -\begin{figure} \underscoreon -\begin{ttbox} -\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace} -\tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a -\tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W - -\tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x -\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x -\tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q - -\tdx{bexI} [| P x; x:A |] ==> ? x:A. P x -\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x -\tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q -\subcaption{Comprehension and Bounded quantifiers} - -\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B -\tdx{subsetD} [| A <= B; c:A |] ==> c:B -\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P - -\tdx{subset_refl} A <= A -\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C - -\tdx{equalityI} [| A <= B; B <= A |] ==> A = B -\tdx{equalityD1} A = B ==> A<=B -\tdx{equalityD2} A = B ==> B<=A -\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P - -\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P; - [| ~ c:A; ~ c:B |] ==> P - |] ==> P -\subcaption{The subset and equality relations} -\end{ttbox} -\caption{Derived rules for set theory} \label{hol-set1} -\end{figure} - - -\begin{figure} \underscoreon -\begin{ttbox} -\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P - -\tdx{insertI1} a : insert a B -\tdx{insertI2} a : B ==> a : insert b B -\tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P - -\tdx{ComplI} [| c:A ==> False |] ==> c : -A -\tdx{ComplD} [| c : -A |] ==> ~ c:A - -\tdx{UnI1} c:A ==> c : A Un B -\tdx{UnI2} c:B ==> c : A Un B -\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B -\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P - -\tdx{IntI} [| c:A; c:B |] ==> c : A Int B -\tdx{IntD1} c : A Int B ==> c:A -\tdx{IntD2} c : A Int B ==> c:B -\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P - -\tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x) -\tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R - -\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x) -\tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a -\tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R - -\tdx{UnionI} [| X:C; A:X |] ==> A : Union C -\tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R - -\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C -\tdx{InterD} [| A : Inter C; X:C |] ==> A:X -\tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R - -\tdx{PowI} A<=B ==> A: Pow B -\tdx{PowD} A: Pow B ==> A<=B - -\tdx{imageI} [| x:A |] ==> f x : f``A -\tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P - -\tdx{rangeI} f x : range f -\tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P -\end{ttbox} -\caption{Further derived rules for set theory} \label{hol-set2} -\end{figure} - - -\subsection{Axioms and rules of set theory} -Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The -axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert -that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of -course, \hbox{\tt op :} also serves as the membership relation. - -All the other axioms are definitions. They include the empty set, bounded -quantifiers, unions, intersections, complements and the subset relation. -They also include straightforward constructions on functions: image~({\tt``}) -and \texttt{range}. - -%The predicate \cdx{inj_on} is used for simulating type definitions. -%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the -%set~$A$, which specifies a subset of its domain type. In a type -%definition, $f$ is the abstraction function and $A$ is the set of valid -%representations; we should not expect $f$ to be injective outside of~$A$. - -%\begin{figure} \underscoreon -%\begin{ttbox} -%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x -%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y -% -%\tdx{Inv_injective} -% [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y -% -% -%\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f -%\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B -% -%\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f -%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f -%\tdx{injD} [| inj f; f x = f y |] ==> x=y -% -%\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A -%\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y -% -%\tdx{inj_on_inverseI} -% (!!x. x:A ==> g(f x) = x) ==> inj_on f A -%\tdx{inj_on_contraD} -% [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y -%\end{ttbox} -%\caption{Derived rules involving functions} \label{hol-fun} -%\end{figure} - - -\begin{figure} \underscoreon -\begin{ttbox} -\tdx{Union_upper} B:A ==> B <= Union A -\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C - -\tdx{Inter_lower} B:A ==> Inter A <= B -\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A - -\tdx{Un_upper1} A <= A Un B -\tdx{Un_upper2} B <= A Un B -\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C - -\tdx{Int_lower1} A Int B <= A -\tdx{Int_lower2} A Int B <= B -\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B -\end{ttbox} -\caption{Derived rules involving subsets} \label{hol-subset} -\end{figure} - - -\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message -\begin{ttbox} -\tdx{Int_absorb} A Int A = A -\tdx{Int_commute} A Int B = B Int A -\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) -\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) - -\tdx{Un_absorb} A Un A = A -\tdx{Un_commute} A Un B = B Un A -\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) -\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) - -\tdx{Compl_disjoint} A Int (-A) = {\ttlbrace}x. False{\ttrbrace} -\tdx{Compl_partition} A Un (-A) = {\ttlbrace}x. True{\ttrbrace} -\tdx{double_complement} -(-A) = A -\tdx{Compl_Un} -(A Un B) = (-A) Int (-B) -\tdx{Compl_Int} -(A Int B) = (-A) Un (-B) - -\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B) -\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C) - -\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B) -\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C) - -\end{ttbox} -\caption{Set equalities} \label{hol-equalities} -\end{figure} -%\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) -%\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) - -Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are -obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such -as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical -reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are -not strictly necessary but yield more natural proofs. Similarly, -\tdx{equalityCE} supports classical reasoning about extensionality, after the -fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs -pertaining to set theory. - -Figure~\ref{hol-subset} presents lattice properties of the subset relation. -Unions form least upper bounds; non-empty intersections form greatest lower -bounds. Reasoning directly about subsets often yields clearer proofs than -reasoning about the membership relation. See the file \texttt{HOL/subset.ML}. - -Figure~\ref{hol-equalities} presents many common set equalities. They -include commutative, associative and distributive laws involving unions, -intersections and complements. For a complete listing see the file {\tt -HOL/equalities.ML}. - -\begin{warn} -\texttt{Blast_tac} proves many set-theoretic theorems automatically. -Hence you seldom need to refer to the theorems above. -\end{warn} - -\begin{figure} -\begin{center} -\begin{tabular}{rrr} - \it name &\it meta-type & \it description \\ - \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ - & injective/surjective \\ - \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$ - & injective over subset\\ - \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function -\end{tabular} -\end{center} - -\underscoreon -\begin{ttbox} -\tdx{inj_def} inj f == ! x y. f x=f y --> x=y -\tdx{surj_def} surj f == ! y. ? x. y=f x -\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y -\tdx{inv_def} inv f == (\%y. @x. f(x)=y) -\end{ttbox} -\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun} -\end{figure} - -\subsection{Properties of functions}\nopagebreak -Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. -Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse -of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived -rules. Reasoning about function composition (the operator~\sdx{o}) and the -predicate~\cdx{surj} is done simply by expanding the definitions. - -There is also a large collection of monotonicity theorems for constructions -on sets in the file \texttt{HOL/mono.ML}. - - -\section{Simplification and substitution} - -Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset -(\texttt{simpset()}), which works for most purposes. A quite minimal -simplification set for higher-order logic is~\ttindexbold{HOL_ss}; -even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which -also expresses logical equivalence, may be used for rewriting. See -the file \texttt{HOL/simpdata.ML} for a complete listing of the basic -simplification rules. - -See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% -{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution -and simplification. - -\begin{warn}\index{simplification!of conjunctions}% - Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The - left part of a conjunction helps in simplifying the right part. This effect - is not available by default: it can be slow. It can be obtained by - including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. -\end{warn} - -\begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}% - By default only the condition of an \ttindex{if} is simplified but not the - \texttt{then} and \texttt{else} parts. Of course the latter are simplified - once the condition simplifies to \texttt{True} or \texttt{False}. To ensure - full simplification of all parts of a conditional you must remove - \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$. -\end{warn} - -If the simplifier cannot use a certain rewrite rule --- either because -of nontermination or because its left-hand side is too flexible --- -then you might try \texttt{stac}: -\begin{ttdescription} -\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$, - replaces in subgoal $i$ instances of $lhs$ by corresponding instances of - $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking - may be necessary to select the desired ones. - -If $thm$ is a conditional equality, the instantiated condition becomes an -additional (first) subgoal. -\end{ttdescription} - -HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an -equality throughout a subgoal and its hypotheses. This tactic uses HOL's -general substitution rule. - -\subsection{Case splitting} -\label{subsec:HOL:case:splitting} - -HOL also provides convenient means for case splitting during rewriting. Goals -containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots} -often require a case distinction on $b$. This is expressed by the theorem -\tdx{split_if}: -$$ -\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~ -((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y}))) -\eqno{(*)} -$$ -For example, a simple instance of $(*)$ is -\[ -x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~ -((x \in A \to x \in A) \land (x \notin A \to x \in \{x\})) -\] -Because $(*)$ is too general as a rewrite rule for the simplifier (the -left-hand side is not a higher-order pattern in the sense of -\iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}% -{Chap.\ts\ref{chap:simplification}}), there is a special infix function -\ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset} -(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a -simpset, as in -\begin{ttbox} -by(simp_tac (simpset() addsplits [split_if]) 1); -\end{ttbox} -The effect is that after each round of simplification, one occurrence of -\texttt{if} is split acording to \texttt{split_if}, until all occurences of -\texttt{if} have been eliminated. - -It turns out that using \texttt{split_if} is almost always the right thing to -do. Hence \texttt{split_if} is already included in the default simpset. If -you want to delete it from a simpset, use \ttindexbold{delsplits}, which is -the inverse of \texttt{addsplits}: -\begin{ttbox} -by(simp_tac (simpset() delsplits [split_if]) 1); -\end{ttbox} - -In general, \texttt{addsplits} accepts rules of the form -\[ -\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs -\] -where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the -right form because internally the left-hand side is -$\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples -are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list} -and~{\S}\ref{subsec:datatype:basics}). - -Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also -imperative versions of \texttt{addsplits} and \texttt{delsplits} -\begin{ttbox} -\ttindexbold{Addsplits}: thm list -> unit -\ttindexbold{Delsplits}: thm list -> unit -\end{ttbox} -for adding splitting rules to, and deleting them from the current simpset. - - -\section{Types}\label{sec:HOL:Types} -This section describes HOL's basic predefined types ($\alpha \times \beta$, -$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new -types in general. The most important type construction, the -\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}. - - -\subsection{Product and sum types}\index{*"* type}\index{*"+ type} -\label{subsec:prod-sum} - -\begin{figure}[htbp] -\begin{constants} - \it symbol & \it meta-type & & \it description \\ - \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ - & & ordered pairs $(a,b)$ \\ - \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ - \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ - \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ - & & generalized projection\\ - \cdx{Sigma} & - $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & - & general sum of sets -\end{constants} -%\tdx{fst_def} fst p == @a. ? b. p = (a,b) -%\tdx{snd_def} snd p == @b. ? a. p = (a,b) -%\tdx{split_def} split c p == c (fst p) (snd p) -\begin{ttbox}\makeatletter -\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace} - -\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b') -\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R -\tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q - -\tdx{fst_conv} fst (a,b) = a -\tdx{snd_conv} snd (a,b) = b -\tdx{surjective_pairing} p = (fst p,snd p) - -\tdx{split} split c (a,b) = c a b -\tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y)) - -\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B - -\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P - |] ==> P -\end{ttbox} -\caption{Type $\alpha\times\beta$}\label{hol-prod} -\end{figure} - -Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type -$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General -tuples are simulated by pairs nested to the right: -\begin{center} -\begin{tabular}{c|c} -external & internal \\ -\hline -$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\ -\hline -$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\ -\end{tabular} -\end{center} -In addition, it is possible to use tuples -as patterns in abstractions: -\begin{center} -{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} -\end{center} -Nested patterns are also supported. They are translated stepwise: -\begin{eqnarray*} -\hbox{\tt\%($x$,$y$,$z$).\ $t$} - & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\ - & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\ - & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))} -\end{eqnarray*} -The reverse translation is performed upon printing. -\begin{warn} - The translation between patterns and \texttt{split} is performed automatically - by the parser and printer. Thus the internal and external form of a term - may differ, which can affects proofs. For example the term {\tt - (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the - default simpset) to rewrite to {\tt(b,a)}. -\end{warn} -In addition to explicit $\lambda$-abstractions, patterns can be used in any -variable binding construct which is internally described by a -$\lambda$-abstraction. Some important examples are -\begin{description} -\item[Let:] \texttt{let {\it pattern} = $t$ in $u$} -\item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$} -\item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$} -\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} -\item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}} -\end{description} - -There is a simple tactic which supports reasoning about patterns: -\begin{ttdescription} -\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all - {\tt!!}-quantified variables of product type by individual variables for - each component. A simple example: -\begin{ttbox} -{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} -by(split_all_tac 1); -{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} -\end{ttbox} -\end{ttdescription} - -Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit} -which contains only a single element named {\tt()} with the property -\begin{ttbox} -\tdx{unit_eq} u = () -\end{ttbox} -\bigskip - -Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$ -which associates to the right and has a lower priority than $*$: $\tau@1 + -\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$. - -The definition of products and sums in terms of existing types is not -shown. The constructions are fairly standard and can be found in the -respective theory files. Although the sum and product types are -constructed manually for foundational reasons, they are represented as -actual datatypes later. - -\begin{figure} -\begin{constants} - \it symbol & \it meta-type & & \it description \\ - \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ - \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ - \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ - & & conditional -\end{constants} -\begin{ttbox}\makeatletter -\tdx{Inl_not_Inr} Inl a ~= Inr b - -\tdx{inj_Inl} inj Inl -\tdx{inj_Inr} inj Inr - -\tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s - -\tdx{sum_case_Inl} sum_case f g (Inl x) = f x -\tdx{sum_case_Inr} sum_case f g (Inr x) = g x - -\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s -\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) & - (! y. s = Inr(y) --> R(g(y)))) -\end{ttbox} -\caption{Type $\alpha+\beta$}\label{hol-sum} -\end{figure} - -\begin{figure} -\index{*"< symbol} -\index{*"* symbol} -\index{*div symbol} -\index{*mod symbol} -\index{*dvd symbol} -\index{*"+ symbol} -\index{*"- symbol} -\begin{constants} - \it symbol & \it meta-type & \it priority & \it description \\ - \cdx{0} & $\alpha$ & & zero \\ - \cdx{Suc} & $nat \To nat$ & & successor function\\ - \tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\ - \tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\ - \tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\ - \tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & ``divides'' relation\\ - \tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\ - \tt - & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction -\end{constants} -\subcaption{Constants and infixes} - -\begin{ttbox}\makeatother -\tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n - -\tdx{Suc_not_Zero} Suc m ~= 0 -\tdx{inj_Suc} inj Suc -\tdx{n_not_Suc_n} n~=Suc n -\subcaption{Basic properties} -\end{ttbox} -\caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1} -\end{figure} - - -\begin{figure} -\begin{ttbox}\makeatother - 0+n = n - (Suc m)+n = Suc(m+n) - - m-0 = m - 0-n = n - Suc(m)-Suc(n) = m-n - - 0*n = 0 - Suc(m)*n = n + m*n - -\tdx{mod_less} m m mod n = m -\tdx{mod_geq} [| 0 m mod n = (m-n) mod n - -\tdx{div_less} m m div n = 0 -\tdx{div_geq} [| 0 m div n = Suc((m-n) div n) -\end{ttbox} -\caption{Recursion equations for the arithmetic operators} \label{hol-nat2} -\end{figure} - -\subsection{The type of natural numbers, \textit{nat}} -\index{nat@{\textit{nat}} type|(} - -The theory \thydx{Nat} defines the natural numbers in a roundabout but -traditional way. The axiom of infinity postulates a type~\tydx{ind} of -individuals, which is non-empty and closed under an injective operation. The -natural numbers are inductively generated by choosing an arbitrary individual -for~0 and using the injective operation to take successors. This is a least -fixedpoint construction. - -Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded -functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min}, -\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} -also shows that {\tt<=} is a linear order, so \tydx{nat} is -also an instance of class \cldx{linorder}. - -Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines -addition, multiplication and subtraction. Theory \thydx{Divides} defines -division, remainder and the ``divides'' relation. The numerous theorems -proved include commutative, associative, distributive, identity and -cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The -recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on -\texttt{nat} are part of the default simpset. - -Functions on \tydx{nat} can be defined by primitive or well-founded recursion; -see {\S}\ref{sec:HOL:recursive}. A simple example is addition. -Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following -the standard convention. -\begin{ttbox} -\sdx{primrec} - "0 + n = n" - "Suc m + n = Suc (m + n)" -\end{ttbox} -There is also a \sdx{case}-construct -of the form -\begin{ttbox} -case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) -\end{ttbox} -Note that Isabelle insists on precisely this format; you may not even change -the order of the two cases. -Both \texttt{primrec} and \texttt{case} are realized by a recursion operator -\cdx{nat_rec}, which is available because \textit{nat} is represented as -a datatype. - -%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. -%Recursion along this relation resembles primitive recursion, but is -%stronger because we are in higher-order logic; using primitive recursion to -%define a higher-order function, we can easily Ackermann's function, which -%is not primitive recursive \cite[page~104]{thompson91}. -%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the -%natural numbers are most easily expressed using recursion along~$<$. - -Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ -in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived -theorem \tdx{less_induct}: -\begin{ttbox} -[| !!n. [| ! m. m P m |] ==> P n |] ==> P n -\end{ttbox} - - -\subsection{Numerical types and numerical reasoning} - -The integers (type \tdx{int}) are also available in HOL, and the reals (type -\tdx{real}) are available in the logic image \texttt{HOL-Complex}. They support -the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and -multiplication (\texttt{*}), and much else. Type \tdx{int} provides the -\texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real -division and other operations. Both types belong to class \cldx{linorder}, so -they inherit the relational operators and all the usual properties of linear -orderings. For full details, please survey the theories in subdirectories -\texttt{Integ}, \texttt{Real}, and \texttt{Complex}. - -All three numeric types admit numerals of the form \texttt{$sd\ldots d$}, -where $s$ is an optional minus sign and $d\ldots d$ is a string of digits. -Numerals are represented internally by a datatype for binary notation, which -allows numerical calculations to be performed by rewriting. For example, the -integer division of \texttt{54342339} by \texttt{3452} takes about five -seconds. By default, the simplifier cancels like terms on the opposite sites -of relational operators (reducing \texttt{z+x [] | Suc(m) => x # take m xs) - -drop n [] = [] -drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs) - -takeWhile P [] = [] -takeWhile P (x#xs) = (if P x then x#takeWhile P xs else []) - -dropWhile P [] = [] -dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) -\end{ttbox} -\caption{Further list processing functions} -\label{fig:HOL:list-simps2} -\end{figure} - - -\subsection{The type constructor for lists, \textit{list}} -\label{subsec:list} -\index{list@{\textit{list}} type|(} - -Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list -operations with their types and syntax. Type $\alpha \; list$ is -defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}. -As a result the generic structural induction and case analysis tactics -\texttt{induct\_tac} and \texttt{cases\_tac} also become available for -lists. A \sdx{case} construct of the form -\begin{center}\tt -case $e$ of [] => $a$ | \(x\)\#\(xs\) => b -\end{center} -is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There -is also a case splitting rule \tdx{split_list_case} -\[ -\begin{array}{l} -P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~ - x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\ -((e = \texttt{[]} \to P(a)) \land - (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs))) -\end{array} -\] -which can be fed to \ttindex{addsplits} just like -\texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}). - -\texttt{List} provides a basic library of list processing functions defined by -primitive recursion. The recursion equations -are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}. - -\index{list@{\textit{list}} type|)} - - -\section{Datatype definitions} -\label{sec:HOL:datatype} -\index{*datatype|(} - -Inductive datatypes, similar to those of \ML, frequently appear in -applications of Isabelle/HOL. In principle, such types could be defined by -hand via \texttt{typedef}, but this would be far too -tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ -\cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an -appropriate \texttt{typedef} based on a least fixed-point construction, and -proves freeness theorems and induction rules, as well as theorems for -recursion and case combinators. The user just has to give a simple -specification of new inductive types using a notation similar to {\ML} or -Haskell. - -The current datatype package can handle both mutual and indirect recursion. -It also offers to represent existing types as datatypes giving the advantage -of a more uniform view on standard theories. - - -\subsection{Basics} -\label{subsec:datatype:basics} - -A general \texttt{datatype} definition is of the following form: -\[ -\begin{array}{llcl} -\mathtt{datatype} & (\vec{\alpha})t@1 & = & - C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~ - C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\ - & & \vdots \\ -\mathtt{and} & (\vec{\alpha})t@n & = & - C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~ - C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}} -\end{array} -\] -where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables, -$C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em - admissible} types containing at most the type variables $\alpha@1, \ldots, -\alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em - admissible} if and only if -\begin{itemize} -\item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the -newly defined type constructors $t@1,\ldots,t@n$, or -\item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or -\item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is -the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$ -are admissible types. -\item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible -type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined -types are {\em strictly positive}) -\end{itemize} -If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$ -of the form -\[ -(\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t' -\] -this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple -example of a datatype is the type \texttt{list}, which can be defined by -\begin{ttbox} -datatype 'a list = Nil - | Cons 'a ('a list) -\end{ttbox} -Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled -by the mutually recursive datatype definition -\begin{ttbox} -datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp) - | Sum ('a aexp) ('a aexp) - | Diff ('a aexp) ('a aexp) - | Var 'a - | Num nat -and 'a bexp = Less ('a aexp) ('a aexp) - | And ('a bexp) ('a bexp) - | Or ('a bexp) ('a bexp) -\end{ttbox} -The datatype \texttt{term}, which is defined by -\begin{ttbox} -datatype ('a, 'b) term = Var 'a - | App 'b ((('a, 'b) term) list) -\end{ttbox} -is an example for a datatype with nested recursion. Using nested recursion -involving function spaces, we may also define infinitely branching datatypes, e.g. -\begin{ttbox} -datatype 'a tree = Atom 'a | Branch "nat => 'a tree" -\end{ttbox} - -\medskip - -Types in HOL must be non-empty. Each of the new datatypes -$(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a -constructor $C^j@i$ with the following property: for all argument types -$\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype -$(\vec{\alpha})t@{j'}$ is non-empty. - -If there are no nested occurrences of the newly defined datatypes, obviously -at least one of the newly defined datatypes $(\vec{\alpha})t@j$ -must have a constructor $C^j@i$ without recursive arguments, a \emph{base - case}, to ensure that the new types are non-empty. If there are nested -occurrences, a datatype can even be non-empty without having a base case -itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t - list)} is non-empty as well. - - -\subsubsection{Freeness of the constructors} - -The datatype constructors are automatically defined as functions of their -respective type: -\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \] -These functions have certain {\em freeness} properties. They construct -distinct values: -\[ -C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad -\mbox{for all}~ i \neq i'. -\] -The constructor functions are injective: -\[ -(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) = -(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i}) -\] -Since the number of distinctness inequalities is quadratic in the number of -constructors, the datatype package avoids proving them separately if there are -too many constructors. Instead, specific inequalities are proved by a suitable -simplification procedure on demand.\footnote{This procedure, which is already part -of the default simpset, may be referred to by the ML identifier -\texttt{DatatypePackage.distinct_simproc}.} - -\subsubsection{Structural induction} - -The datatype package also provides structural induction rules. For -datatypes without nested recursion, this is of the following form: -\[ -\infer{P@1~x@1 \land \dots \land P@n~x@n} - {\begin{array}{lcl} - \Forall x@1 \dots x@{m^1@1}. - \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots; - P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp & - P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\ - & \vdots \\ - \Forall x@1 \dots x@{m^1@{k@1}}. - \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots; - P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp & - P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\ - & \vdots \\ - \Forall x@1 \dots x@{m^n@1}. - \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots; - P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp & - P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\ - & \vdots \\ - \Forall x@1 \dots x@{m^n@{k@n}}. - \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots - P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp & - P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right) - \end{array}} -\] -where -\[ -\begin{array}{rcl} -Rec^j@i & := & - \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, - \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex] -&& \left\{(i',i'')~\left|~ - 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land - \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\} -\end{array} -\] -i.e.\ the properties $P@j$ can be assumed for all recursive arguments. - -For datatypes with nested recursion, such as the \texttt{term} example from -above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds -a definition like -\begin{ttbox} -datatype ('a,'b) term = Var 'a - | App 'b ((('a, 'b) term) list) -\end{ttbox} -to an equivalent definition without nesting: -\begin{ttbox} -datatype ('a,'b) term = Var - | App 'b (('a, 'b) term_list) -and ('a,'b) term_list = Nil' - | Cons' (('a,'b) term) (('a,'b) term_list) -\end{ttbox} -Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt - Nil'} and \texttt{Cons'} are not really introduced. One can directly work with -the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing -constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for -\texttt{term} gets the form -\[ -\infer{P@1~x@1 \land P@2~x@2} - {\begin{array}{l} - \Forall x.~P@1~(\mathtt{Var}~x) \\ - \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\ - P@2~\mathtt{Nil} \\ - \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2) - \end{array}} -\] -Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term} -and one for the type \texttt{(('a, 'b) term) list}. - -For a datatype with function types such as \texttt{'a tree}, the induction rule -is of the form -\[ -\infer{P~t} - {\Forall a.~P~(\mathtt{Atom}~a) & - \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)} -\] - -\medskip In principle, inductive types are already fully determined by -freeness and structural induction. For convenience in applications, -the following derived constructions are automatically provided for any -datatype. - -\subsubsection{The \sdx{case} construct} - -The type comes with an \ML-like \texttt{case}-construct: -\[ -\begin{array}{rrcl} -\mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\ - \vdots \\ - \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j} -\end{array} -\] -where the $x@{i,j}$ are either identifiers or nested tuple patterns as in -{\S}\ref{subsec:prod-sum}. -\begin{warn} - All constructors must be present, their order is fixed, and nested patterns - are not supported (with the exception of tuples). Violating this - restriction results in strange error messages. -\end{warn} - -To perform case distinction on a goal containing a \texttt{case}-construct, -the theorem $t@j.$\texttt{split} is provided: -\[ -\begin{array}{@{}rcl@{}} -P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=& -\!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to - P(f@1~x@1\dots x@{m^j@1})) \\ -&&\!\!\! ~\land~ \dots ~\land \\ -&&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to - P(f@{k@j}~x@1\dots x@{m^j@{k@j}}))) -\end{array} -\] -where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct. -This theorem can be added to a simpset via \ttindex{addsplits} -(see~{\S}\ref{subsec:HOL:case:splitting}). - -Case splitting on assumption works as well, by using the rule -$t@j.$\texttt{split_asm} in the same manner. Both rules are available under -$t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though). - -\begin{warn}\index{simplification!of \texttt{case}}% - By default only the selector expression ($e$ above) in a - \texttt{case}-construct is simplified, in analogy with \texttt{if} (see - page~\pageref{if-simp}). Only if that reduces to a constructor is one of - the arms of the \texttt{case}-construct exposed and simplified. To ensure - full simplification of all parts of a \texttt{case}-construct for datatype - $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for - example by \texttt{delcongs [thm "$t$.weak_case_cong"]}. -\end{warn} - -\subsubsection{The function \cdx{size}}\label{sec:HOL:size} - -Theory \texttt{NatArith} declares a generic function \texttt{size} of type -$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size} -by overloading according to the following scheme: -%%% FIXME: This formula is too big and is completely unreadable -\[ -size(C^j@i~x@1~\dots~x@{m^j@i}) = \! -\left\{ -\begin{array}{ll} -0 & \!\mbox{if $Rec^j@i = \emptyset$} \\ -1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} & - \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, - \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$} -\end{array} -\right. -\] -where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the -size of a leaf is 0 and the size of a node is the sum of the sizes of its -subtrees ${}+1$. - -\subsection{Defining datatypes} - -The theory syntax for datatype definitions is given in the -Isabelle/Isar reference manual. In order to be well-formed, a -datatype definition has to obey the rules stated in the previous -section. As a result the theory is extended with the new types, the -constructors, and the theorems listed in the previous section. - -Most of the theorems about datatypes become part of the default simpset and -you never need to see them again because the simplifier applies them -automatically. Only induction or case distinction are usually invoked by hand. -\begin{ttdescription} -\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] - applies structural induction on variable $x$ to subgoal $i$, provided the - type of $x$ is a datatype. -\item[\texttt{induct_tac} - {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous - structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This - is the canonical way to prove properties of mutually recursive datatypes - such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as - \texttt{term}. -\end{ttdescription} -In some cases, induction is overkill and a case distinction over all -constructors of the datatype suffices. -\begin{ttdescription} -\item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$] - performs a case analysis for the term $u$ whose type must be a datatype. - If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal - $i$ is replaced by $k@j$ new subgoals which contain the additional - assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for $i'=1$, $\dots$,~$k@j$. -\end{ttdescription} - -Note that induction is only allowed on free variables that should not occur -among the premises of the subgoal. Case distinction applies to arbitrary terms. - -\bigskip - - -For the technically minded, we exhibit some more details. Processing the -theory file produces an \ML\ structure which, in addition to the usual -components, contains a structure named $t$ for each datatype $t$ defined in -the file. Each structure $t$ contains the following elements: -\begin{ttbox} -val distinct : thm list -val inject : thm list -val induct : thm -val exhaust : thm -val cases : thm list -val split : thm -val split_asm : thm -val recs : thm list -val size : thm list -val simps : thm list -\end{ttbox} -\texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size} -and \texttt{split} contain the theorems -described above. For user convenience, \texttt{distinct} contains -inequalities in both directions. The reduction rules of the {\tt - case}-construct are in \texttt{cases}. All theorems from {\tt - distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. -In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct} -and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. - - -\section{Old-style recursive function definitions}\label{sec:HOL:recursive} -\index{recursion!general|(} -\index{*recdef|(} - -Old-style recursive definitions via \texttt{recdef} requires that you -supply a well-founded relation that governs the recursion. Recursive -calls are only allowed if they make the argument decrease under the -relation. Complicated recursion forms, such as nested recursion, can -be dealt with. Termination can even be proved at a later time, though -having unsolved termination conditions around can make work -difficult.% -\footnote{This facility is based on Konrad Slind's TFL - package~\cite{slind-tfl}. Thanks are due to Konrad for implementing - TFL and assisting with its installation.} - -Using \texttt{recdef}, you can declare functions involving nested recursion -and pattern-matching. Recursion need not involve datatypes and there are few -syntactic restrictions. Termination is proved by showing that each recursive -call makes the argument smaller in a suitable sense, which you specify by -supplying a well-founded relation. - -Here is a simple example, the Fibonacci function. The first line declares -\texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on -the natural numbers). Pattern-matching is used here: \texttt{1} is a -macro for \texttt{Suc~0}. -\begin{ttbox} -consts fib :: "nat => nat" -recdef fib "less_than" - "fib 0 = 0" - "fib 1 = 1" - "fib (Suc(Suc x)) = (fib x + fib (Suc x))" -\end{ttbox} - -With \texttt{recdef}, function definitions may be incomplete, and patterns may -overlap, as in functional programming. The \texttt{recdef} package -disambiguates overlapping patterns by taking the order of rules into account. -For missing patterns, the function is defined to return a default value. - -%For example, here is a declaration of the list function \cdx{hd}: -%\begin{ttbox} -%consts hd :: 'a list => 'a -%recdef hd "\{\}" -% "hd (x#l) = x" -%\end{ttbox} -%Because this function is not recursive, we may supply the empty well-founded -%relation, $\{\}$. - -The well-founded relation defines a notion of ``smaller'' for the function's -argument type. The relation $\prec$ is \textbf{well-founded} provided it -admits no infinitely decreasing chains -\[ \cdots\prec x@n\prec\cdots\prec x@1. \] -If the function's argument has type~$\tau$, then $\prec$ has to be a relation -over~$\tau$: it must have type $(\tau\times\tau)set$. - -Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection -of operators for building well-founded relations. The package recognises -these operators and automatically proves that the constructed relation is -well-founded. Here are those operators, in order of importance: -\begin{itemize} -\item \texttt{less_than} is ``less than'' on the natural numbers. - (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$. - -\item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the - relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if - $f(x)}R@2$ is the lexicographic product of two relations. - It - is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only - if $x@1$ - is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$ - is less than $y@2$ according to~$R@2$. - -\item \texttt{finite_psubset} is the proper subset relation on finite sets. -\end{itemize} - -We can use \texttt{measure} to declare Euclid's algorithm for the greatest -common divisor. The measure function, $\lambda(m,n). n$, specifies that the -recursion terminates because argument~$n$ decreases. -\begin{ttbox} -recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" - "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" -\end{ttbox} - -The general form of a well-founded recursive definition is -\begin{ttbox} -recdef {\it function} {\it rel} - congs {\it congruence rules} {\bf(optional)} - simpset {\it simplification set} {\bf(optional)} - {\it reduction rules} -\end{ttbox} -where -\begin{itemize} -\item \textit{function} is the name of the function, either as an \textit{id} - or a \textit{string}. - -\item \textit{rel} is a HOL expression for the well-founded termination - relation. - -\item \textit{congruence rules} are required only in highly exceptional - circumstances. - -\item The \textit{simplification set} is used to prove that the supplied - relation is well-founded. It is also used to prove the \textbf{termination - conditions}: assertions that arguments of recursive calls decrease under - \textit{rel}. By default, simplification uses \texttt{simpset()}, which - is sufficient to prove well-foundedness for the built-in relations listed - above. - -\item \textit{reduction rules} specify one or more recursion equations. Each - left-hand side must have the form $f\,t$, where $f$ is the function and $t$ - is a tuple of distinct variables. If more than one equation is present then - $f$ is defined by pattern-matching on components of its argument whose type - is a \texttt{datatype}. - - The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as - a list of theorems. -\end{itemize} - -With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to -prove one termination condition. It remains as a precondition of the -recursion theorems: -\begin{ttbox} -gcd.simps; -{\out ["! m n. n ~= 0 --> m mod n < n} -{\out ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] } -{\out : thm list} -\end{ttbox} -The theory \texttt{HOL/ex/Primes} illustrates how to prove termination -conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard -function \texttt{goalw}, which sets up a goal to prove, but its argument -should be the identifier $f$\texttt{.simps} and its effect is to set up a -proof of the termination conditions: -\begin{ttbox} -Tfl.tgoalw thy [] gcd.simps; -{\out Level 0} -{\out ! m n. n ~= 0 --> m mod n < n} -{\out 1. ! m n. n ~= 0 --> m mod n < n} -\end{ttbox} -This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem -is proved, it can be used to eliminate the termination conditions from -elements of \texttt{gcd.simps}. Theory \texttt{HOL/Subst/Unify} is a much -more complicated example of this process, where the termination conditions can -only be proved by complicated reasoning involving the recursive function -itself. - -Isabelle/HOL can prove the \texttt{gcd} function's termination condition -automatically if supplied with the right simpset. -\begin{ttbox} -recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" - simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" - "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" -\end{ttbox} - -If all termination conditions were proved automatically, $f$\texttt{.simps} -is added to the simpset automatically, just as in \texttt{primrec}. -The simplification rules corresponding to clause $i$ (where counting starts -at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms - "$f$.$i$"}, -which returns a list of theorems. Thus you can, for example, remove specific -clauses from the simpset. Note that a single clause may give rise to a set of -simplification rules in order to capture the fact that if clauses overlap, -their order disambiguates them. - -A \texttt{recdef} definition also returns an induction rule specialised for -the recursive function. For the \texttt{gcd} function above, the induction -rule is -\begin{ttbox} -gcd.induct; -{\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm} -\end{ttbox} -This rule should be used to reason inductively about the \texttt{gcd} -function. It usually makes the induction hypothesis available at all -recursive calls, leading to very direct proofs. If any termination conditions -remain unproved, they will become additional premises of this rule. - -\index{recursion!general|)} -\index{*recdef|)} - - -\section{Example: Cantor's Theorem}\label{sec:hol-cantor} -Cantor's Theorem states that every set has more subsets than it has -elements. It has become a favourite example in higher-order logic since -it is so easily expressed: -\[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool. - \forall x::\alpha. f~x \not= S -\] -% -Viewing types as sets, $\alpha\To bool$ represents the powerset -of~$\alpha$. This version states that for every function from $\alpha$ to -its powerset, some subset is outside its range. - -The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and -the operator \cdx{range}. -\begin{ttbox} -context Set.thy; -\end{ttbox} -The set~$S$ is given as an unknown instead of a -quantified variable so that we may inspect the subset found by the proof. -\begin{ttbox} -Goal "?S ~: range\thinspace(f :: 'a=>'a set)"; -{\out Level 0} -{\out ?S ~: range f} -{\out 1. ?S ~: range f} -\end{ttbox} -The first two steps are routine. The rule \tdx{rangeE} replaces -$\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$. -\begin{ttbox} -by (resolve_tac [notI] 1); -{\out Level 1} -{\out ?S ~: range f} -{\out 1. ?S : range f ==> False} -\ttbreak -by (eresolve_tac [rangeE] 1); -{\out Level 2} -{\out ?S ~: range f} -{\out 1. !!x. ?S = f x ==> False} -\end{ttbox} -Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, -we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for -any~$\Var{c}$. -\begin{ttbox} -by (eresolve_tac [equalityCE] 1); -{\out Level 3} -{\out ?S ~: range f} -{\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False} -{\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False} -\end{ttbox} -Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a -comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies -$\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD} -instantiates~$\Var{S}$ and creates the new assumption. -\begin{ttbox} -by (dresolve_tac [CollectD] 1); -{\out Level 4} -{\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f} -{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} -{\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False} -\end{ttbox} -Forcing a contradiction between the two assumptions of subgoal~1 -completes the instantiation of~$S$. It is now the set $\{x. x\not\in -f~x\}$, which is the standard diagonal construction. -\begin{ttbox} -by (contr_tac 1); -{\out Level 5} -{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} -{\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False} -\end{ttbox} -The rest should be easy. To apply \tdx{CollectI} to the negated -assumption, we employ \ttindex{swap_res_tac}: -\begin{ttbox} -by (swap_res_tac [CollectI] 1); -{\out Level 6} -{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} -{\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x} -\ttbreak -by (assume_tac 1); -{\out Level 7} -{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} -{\out No subgoals!} -\end{ttbox} -How much creativity is required? As it happens, Isabelle can prove this -theorem automatically. The default classical set \texttt{claset()} contains -rules for most of the constructs of HOL's set theory. We must augment it with -\tdx{equalityCE} to break up set equalities, and then apply best-first search. -Depth-first search would diverge, but best-first search successfully navigates -through the large search space. \index{search!best-first} -\begin{ttbox} -choplev 0; -{\out Level 0} -{\out ?S ~: range f} -{\out 1. ?S ~: range f} -\ttbreak -by (best_tac (claset() addSEs [equalityCE]) 1); -{\out Level 1} -{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} -{\out No subgoals!} -\end{ttbox} -If you run this example interactively, make sure your current theory contains -theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}. -Otherwise the default claset may not contain the rules for set theory. -\index{higher-order logic|)} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "logics-HOL" -%%% End: diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/Makefile --- a/doc-src/HOL/Makefile Mon Aug 27 21:30:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ - -## targets - -default: dvi - - -## dependencies - -include ../Makefile.in - -NAME = logics-HOL -FILES = logics-HOL.tex ../Logics/syntax.tex HOL.tex \ - ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib - -dvi: $(NAME).dvi - -$(NAME).dvi: $(FILES) isabelle_hol.eps - $(LATEX) $(NAME) - $(BIBTEX) $(NAME) - $(LATEX) $(NAME) - $(LATEX) $(NAME) - $(SEDINDEX) $(NAME) - $(LATEX) $(NAME) - -pdf: $(NAME).pdf - -$(NAME).pdf: $(FILES) isabelle_hol.pdf - $(PDFLATEX) $(NAME) - $(BIBTEX) $(NAME) - $(PDFLATEX) $(NAME) - $(PDFLATEX) $(NAME) - $(SEDINDEX) $(NAME) - $(FIXBOOKMARKS) $(NAME).out - $(PDFLATEX) $(NAME) diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/document/HOL.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/HOL/document/HOL.tex Mon Aug 27 21:37:34 2012 +0200 @@ -0,0 +1,2089 @@ +\chapter{Higher-Order Logic} +\index{higher-order logic|(} +\index{HOL system@{\sc hol} system} + +\begin{figure} +\begin{constants} + \it name &\it meta-type & \it description \\ + \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ + \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\ + \cdx{True} & $bool$ & tautology ($\top$) \\ + \cdx{False} & $bool$ & absurdity ($\bot$) \\ + \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\ + \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder +\end{constants} +\subcaption{Constants} + +\begin{constants} +\index{"@@{\tt\at} symbol} +\index{*"! symbol}\index{*"? symbol} +\index{*"?"! symbol}\index{*"E"X"! symbol} + \it symbol &\it name &\it meta-type & \it description \\ + \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & + Hilbert description ($\varepsilon$) \\ + \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ & + universal quantifier ($\forall$) \\ + \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & + existential quantifier ($\exists$) \\ + \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & + unique existence ($\exists!$)\\ + \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & + least element +\end{constants} +\subcaption{Binders} + +\begin{constants} +\index{*"= symbol} +\index{&@{\tt\&} symbol} +\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working +\index{*"-"-"> symbol} + \it symbol & \it meta-type & \it priority & \it description \\ + \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & + Left 55 & composition ($\circ$) \\ + \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\ + \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ + \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & + less than or equals ($\leq$)\\ + \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ + \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ + \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) +\end{constants} +\subcaption{Infixes} +\caption{Syntax of \texttt{HOL}} \label{hol-constants} +\end{figure} + + +\begin{figure} +\index{*let symbol} +\index{*in symbol} +\dquotes +\[\begin{array}{rclcl} + term & = & \hbox{expression of class~$term$} \\ + & | & "SOME~" id " . " formula + & | & "\at~" id " . " formula \\ + & | & + \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ + & | & + \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\ + & | & "LEAST"~ id " . " formula \\[2ex] + formula & = & \hbox{expression of type~$bool$} \\ + & | & term " = " term \\ + & | & term " \ttilde= " term \\ + & | & term " < " term \\ + & | & term " <= " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & "ALL~" id~id^* " . " formula + & | & "!~~~" id~id^* " . " formula \\ + & | & "EX~~" id~id^* " . " formula + & | & "?~~~" id~id^* " . " formula \\ + & | & "EX!~" id~id^* " . " formula + & | & "?!~~" id~id^* " . " formula \\ + \end{array} +\] +\caption{Full grammar for HOL} \label{hol-grammar} +\end{figure} + + +\section{Syntax} + +Figure~\ref{hol-constants} lists the constants (including infixes and +binders), while Fig.\ts\ref{hol-grammar} presents the grammar of +higher-order logic. Note that $a$\verb|~=|$b$ is translated to +$\lnot(a=b)$. + +\begin{warn} + HOL has no if-and-only-if connective; logical equivalence is expressed using + equality. But equality has a high priority, as befitting a relation, while + if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$ + abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$ + to mean logical equivalence, enclose both operands in parentheses. +\end{warn} + +\subsection{Types and overloading} +The universal type class of higher-order terms is called~\cldx{term}. +By default, explicit type variables have class \cldx{term}. In +particular the equality symbol and quantifiers are polymorphic over +class \texttt{term}. + +The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, +formulae are terms. The built-in type~\tydx{fun}, which constructs +function types, is overloaded with arity {\tt(term,\thinspace + term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt + term} if $\sigma$ and~$\tau$ do, allowing quantification over +functions. + +HOL allows new types to be declared as subsets of existing types, +either using the primitive \texttt{typedef} or the more convenient +\texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}). + +Several syntactic type classes --- \cldx{plus}, \cldx{minus}, +\cldx{times} and +\cldx{power} --- permit overloading of the operators {\tt+},\index{*"+ + symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol} +and \verb|^|.\index{^@\verb.^. symbol} +% +They are overloaded to denote the obvious arithmetic operations on types +\tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the +exponent always has type~\tdx{nat}.) Non-arithmetic overloadings are also +done: the operator {\tt-} can denote set difference, while \verb|^| can +denote exponentiation of relations (iterated composition). Unary minus is +also written as~{\tt-} and is overloaded like its 2-place counterpart; it even +can stand for set complement. + +The constant \cdx{0} is also overloaded. It serves as the zero element of +several types, of which the most important is \tdx{nat} (the natural +numbers). The type class \cldx{plus_ac0} comprises all types for which 0 +and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These +types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also +multisets. The summation operator \cdx{setsum} is available for all types in +this class. + +Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order +signatures. The relations $<$ and $\leq$ are polymorphic over this +class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and +the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass +\cldx{order} of \cldx{ord} which axiomatizes the types that are partially +ordered with respect to~$\leq$. A further subclass \cldx{linorder} of +\cldx{order} axiomatizes linear orderings. +For details, see the file \texttt{Ord.thy}. + +If you state a goal containing overloaded functions, you may need to include +type constraints. Type inference may otherwise make the goal more +polymorphic than you intended, with confusing results. For example, the +variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type +$\alpha::\{ord,plus\}$, although you may have expected them to have some +numeric type, e.g. $nat$. Instead you should have stated the goal as +$(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have +type $nat$. + +\begin{warn} + If resolution fails for no obvious reason, try setting + \ttindex{show_types} to \texttt{true}, causing Isabelle to display + types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as + well, causing Isabelle to display type classes and sorts. + + \index{unification!incompleteness of} + Where function types are involved, Isabelle's unification code does not + guarantee to find instantiations for type variables automatically. Be + prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, + possibly instantiating type variables. Setting + \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report + omitted search paths during unification.\index{tracing!of unification} +\end{warn} + + +\subsection{Binders} + +Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$ +satisfying~$P$, if such exists. Since all terms in HOL denote something, a +description is always meaningful, but we do not know its value unless $P$ +defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x. +P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}. + +Existential quantification is defined by +\[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] +The unique existence quantifier, $\exists!x. P$, is defined in terms +of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested +quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates +$\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there +exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. + +\medskip + +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The +basic Isabelle/HOL binders have two notations. Apart from the usual +\texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also +supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ +and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be +followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a +quantification. Both notations are accepted for input. The print mode +``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by +passing option \texttt{-m HOL} to the \texttt{isabelle} executable), +then~{\tt!}\ and~{\tt?}\ are displayed. + +\medskip + +If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a +variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined +to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see +Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ +choice operator, so \texttt{Least} is always meaningful, but may yield +nothing useful in case there is not a unique least element satisfying +$P$.\footnote{Class $ord$ does not require much of its instances, so + $\leq$ need not be a well-ordering, not even an order at all!} + +\medskip All these binders have priority 10. + +\begin{warn} +The low priority of binders means that they need to be enclosed in +parenthesis when they occur in the context of other operations. For example, +instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$. +\end{warn} + + +\subsection{The let and case constructions} +Local abbreviations can be introduced by a \texttt{let} construct whose +syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into +the constant~\cdx{Let}. It can be expanded by rewriting with its +definition, \tdx{Let_def}. + +HOL also defines the basic syntax +\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] +as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} +and \sdx{of} are reserved words. Initially, this is mere syntax and has no +logical meaning. By declaring translations, you can cause instances of the +\texttt{case} construct to denote applications of particular case operators. +This is what happens automatically for each \texttt{datatype} definition +(see~{\S}\ref{sec:HOL:datatype}). + +\begin{warn} +Both \texttt{if} and \texttt{case} constructs have as low a priority as +quantifiers, which requires additional enclosing parentheses in the context +of most other operations. For example, instead of $f~x = {\tt if\dots +then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots +else\dots})$. +\end{warn} + +\section{Rules of inference} + +\begin{figure} +\begin{ttbox}\makeatother +\tdx{refl} t = (t::'a) +\tdx{subst} [| s = t; P s |] ==> P (t::'a) +\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x) +\tdx{impI} (P ==> Q) ==> P-->Q +\tdx{mp} [| P-->Q; P |] ==> Q +\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) +\tdx{someI} P(x::'a) ==> P(@x. P x) +\tdx{True_or_False} (P=True) | (P=False) +\end{ttbox} +\caption{The \texttt{HOL} rules} \label{hol-rules} +\end{figure} + +Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with +their~{\ML} names. Some of the rules deserve additional comments: +\begin{ttdescription} +\item[\tdx{ext}] expresses extensionality of functions. +\item[\tdx{iff}] asserts that logically equivalent formulae are + equal. +\item[\tdx{someI}] gives the defining property of the Hilbert + $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule + \tdx{some_equality} (see below) is often easier to use. +\item[\tdx{True_or_False}] makes the logic classical.\footnote{In + fact, the $\varepsilon$-operator already makes the logic classical, as + shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.} +\end{ttdescription} + + +\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message +\begin{ttbox}\makeatother +\tdx{True_def} True == ((\%x::bool. x)=(\%x. x)) +\tdx{All_def} All == (\%P. P = (\%x. True)) +\tdx{Ex_def} Ex == (\%P. P(@x. P x)) +\tdx{False_def} False == (!P. P) +\tdx{not_def} not == (\%P. P-->False) +\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R) +\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R) +\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x)) + +\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x)) +\tdx{if_def} If P x y == + (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y)) +\tdx{Let_def} Let s f == f s +\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" +\end{ttbox} +\caption{The \texttt{HOL} definitions} \label{hol-defs} +\end{figure} + + +HOL follows standard practice in higher-order logic: only a few connectives +are taken as primitive, with the remainder defined obscurely +(Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the +corresponding definitions \cite[page~270]{mgordon-hol} using +object-equality~({\tt=}), which is possible because equality in higher-order +logic may equate formulae and even functions over formulae. But theory~HOL, +like all other Isabelle theories, uses meta-equality~({\tt==}) for +definitions. +\begin{warn} +The definitions above should never be expanded and are shown for completeness +only. Instead users should reason in terms of the derived rules shown below +or, better still, using high-level tactics. +\end{warn} + +Some of the rules mention type variables; for example, \texttt{refl} +mentions the type variable~{\tt'a}. This allows you to instantiate +type variables explicitly by calling \texttt{res_inst_tac}. + + +\begin{figure} +\begin{ttbox} +\tdx{sym} s=t ==> t=s +\tdx{trans} [| r=s; s=t |] ==> r=t +\tdx{ssubst} [| t=s; P s |] ==> P t +\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d +\tdx{arg_cong} x = y ==> f x = f y +\tdx{fun_cong} f = g ==> f x = g x +\tdx{cong} [| f = g; x = y |] ==> f x = g y +\tdx{not_sym} t ~= s ==> s ~= t +\subcaption{Equality} + +\tdx{TrueI} True +\tdx{FalseE} False ==> P + +\tdx{conjI} [| P; Q |] ==> P&Q +\tdx{conjunct1} [| P&Q |] ==> P +\tdx{conjunct2} [| P&Q |] ==> Q +\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R + +\tdx{disjI1} P ==> P|Q +\tdx{disjI2} Q ==> P|Q +\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R + +\tdx{notI} (P ==> False) ==> ~ P +\tdx{notE} [| ~ P; P |] ==> R +\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R +\subcaption{Propositional logic} + +\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q +\tdx{iffD1} [| P=Q; P |] ==> Q +\tdx{iffD2} [| P=Q; Q |] ==> P +\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R +\subcaption{Logical equivalence} + +\end{ttbox} +\caption{Derived rules for HOL} \label{hol-lemmas1} +\end{figure} +% +%\tdx{eqTrueI} P ==> P=True +%\tdx{eqTrueE} P=True ==> P + + +\begin{figure} +\begin{ttbox}\makeatother +\tdx{allI} (!!x. P x) ==> !x. P x +\tdx{spec} !x. P x ==> P x +\tdx{allE} [| !x. P x; P x ==> R |] ==> R +\tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R + +\tdx{exI} P x ==> ? x. P x +\tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q + +\tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x +\tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R + |] ==> R + +\tdx{some_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a +\subcaption{Quantifiers and descriptions} + +\tdx{ccontr} (~P ==> False) ==> P +\tdx{classical} (~P ==> P) ==> P +\tdx{excluded_middle} ~P | P + +\tdx{disjCI} (~Q ==> P) ==> P|Q +\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x +\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R +\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R +\tdx{notnotD} ~~P ==> P +\tdx{swap} ~P ==> (~Q ==> P) ==> Q +\subcaption{Classical logic} + +\tdx{if_P} P ==> (if P then x else y) = x +\tdx{if_not_P} ~ P ==> (if P then x else y) = y +\tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y)) +\subcaption{Conditionals} +\end{ttbox} +\caption{More derived rules} \label{hol-lemmas2} +\end{figure} + +Some derived rules are shown in Figures~\ref{hol-lemmas1} +and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules +for the logical connectives, as well as sequent-style elimination rules for +conjunctions, implications, and universal quantifiers. + +Note the equality rules: \tdx{ssubst} performs substitution in +backward proofs, while \tdx{box_equals} supports reasoning by +simplifying both sides of an equation. + +The following simple tactics are occasionally useful: +\begin{ttdescription} +\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI} + repeatedly to remove all outermost universal quantifiers and implications + from subgoal $i$. +\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on + $P$ for subgoal $i$: the latter is replaced by two identical subgoals with + the added assumptions $P$ and $\lnot P$, respectively. +\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then + \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining + from an induction hypothesis. As a generalization of \texttt{mp_tac}, + if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and + $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables) + then it replaces the universally quantified implication by $Q \vec{a}$. + It may instantiate unknowns. It fails if it can do nothing. +\end{ttdescription} + + +\begin{figure} +\begin{center} +\begin{tabular}{rrr} + \it name &\it meta-type & \it description \\ +\index{{}@\verb'{}' symbol} + \verb|{}| & $\alpha\,set$ & the empty set \\ + \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ + & insertion of element \\ + \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ + & comprehension \\ + \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ + & intersection over a set\\ + \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ + & union over a set\\ + \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ + &set of sets intersection \\ + \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ + &set of sets union \\ + \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ + & powerset \\[1ex] + \cdx{range} & $(\alpha\To\beta )\To\beta\,set$ + & range of a function \\[1ex] + \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ + & bounded quantifiers +\end{tabular} +\end{center} +\subcaption{Constants} + +\begin{center} +\begin{tabular}{llrrr} + \it symbol &\it name &\it meta-type & \it priority & \it description \\ + \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & + intersection\\ + \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & + union +\end{tabular} +\end{center} +\subcaption{Binders} + +\begin{center} +\index{*"`"` symbol} +\index{*": symbol} +\index{*"<"= symbol} +\begin{tabular}{rrrr} + \it symbol & \it meta-type & \it priority & \it description \\ + \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$ + & Left 90 & image \\ + \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 70 & intersection ($\int$) \\ + \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 65 & union ($\un$) \\ + \tt: & $[\alpha ,\alpha\,set]\To bool$ + & Left 50 & membership ($\in$) \\ + \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ + & Left 50 & subset ($\subseteq$) +\end{tabular} +\end{center} +\subcaption{Infixes} +\caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax} +\end{figure} + + +\begin{figure} +\begin{center} \tt\frenchspacing +\index{*"! symbol} +\begin{tabular}{rrr} + \it external & \it internal & \it description \\ + $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm not in\\ + {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ + {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) & + \rm comprehension \\ + \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ & + \rm intersection \\ + \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ & + \rm union \\ + \sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ & + Ball $A$ $\lambda x.\ P[x]$ & + \rm bounded $\forall$ \\ + \sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $x$:$A$.\ $P[x]$ & + Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$ +\end{tabular} +\end{center} +\subcaption{Translations} + +\dquotes +\[\begin{array}{rclcl} + term & = & \hbox{other terms\ldots} \\ + & | & "{\ttlbrace}{\ttrbrace}" \\ + & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ + & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\ + & | & term " `` " term \\ + & | & term " Int " term \\ + & | & term " Un " term \\ + & | & "INT~~" id ":" term " . " term \\ + & | & "UN~~~" id ":" term " . " term \\ + & | & "INT~~" id~id^* " . " term \\ + & | & "UN~~~" id~id^* " . " term \\[2ex] + formula & = & \hbox{other formulae\ldots} \\ + & | & term " : " term \\ + & | & term " \ttilde: " term \\ + & | & term " <= " term \\ + & | & "ALL " id ":" term " . " formula + & | & "!~" id ":" term " . " formula \\ + & | & "EX~~" id ":" term " . " formula + & | & "?~" id ":" term " . " formula \\ + \end{array} +\] +\subcaption{Full Grammar} +\caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2} +\end{figure} + + +\section{A formulation of set theory} +Historically, higher-order logic gives a foundation for Russell and +Whitehead's theory of classes. Let us use modern terminology and call them +{\bf sets}, but note that these sets are distinct from those of ZF set theory, +and behave more like ZF classes. +\begin{itemize} +\item +Sets are given by predicates over some type~$\sigma$. Types serve to +define universes for sets, but type-checking is still significant. +\item +There is a universal set (for each type). Thus, sets have complements, and +may be defined by absolute comprehension. +\item +Although sets may contain other sets as elements, the containing set must +have a more complex type. +\end{itemize} +Finite unions and intersections have the same behaviour in HOL as they do +in~ZF. In HOL the intersection of the empty set is well-defined, denoting the +universal set for the given type. + +\subsection{Syntax of set theory}\index{*set type} +HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially +the same as $\alpha\To bool$. The new type is defined for clarity and to +avoid complications involving function types in unification. The isomorphisms +between the two types are declared explicitly. They are very natural: +\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :} +maps in the other direction (ignoring argument order). + +Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax +translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new +constructs. Infix operators include union and intersection ($A\un B$ +and $A\int B$), the subset and membership relations, and the image +operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to +$\lnot(a\in b)$. + +The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in +the obvious manner using~\texttt{insert} and~$\{\}$: +\begin{eqnarray*} + \{a, b, c\} & \equiv & + \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) +\end{eqnarray*} + +The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of +suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain +free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x. +P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF; +the type of~$x$ implicitly restricts the comprehension. + +The set theory defines two {\bf bounded quantifiers}: +\begin{eqnarray*} + \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ + \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] +\end{eqnarray*} +The constants~\cdx{Ball} and~\cdx{Bex} are defined +accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may +write\index{*"! symbol}\index{*"? symbol} +\index{*ALL symbol}\index{*EX symbol} +% +\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The +original notation of Gordon's {\sc hol} system is supported as well: +\texttt{!}\ and \texttt{?}. + +Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and +$\bigcap@{x\in A}B[x]$, are written +\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and +\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}. + +Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x +B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and +\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous +union and intersection operators when $A$ is the universal set. + +The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are +not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$, +respectively. + + + +\begin{figure} \underscoreon +\begin{ttbox} +\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a +\tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A + +\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace} +\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B +\tdx{Ball_def} Ball A P == ! x. x:A --> P x +\tdx{Bex_def} Bex A P == ? x. x:A & P x +\tdx{subset_def} A <= B == ! x:A. x:B +\tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace} +\tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace} +\tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace} +\tdx{Compl_def} -A == {\ttlbrace}x. ~ x:A{\ttrbrace} +\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} +\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} +\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B +\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B +\tdx{Inter_def} Inter S == (INT x:S. x) +\tdx{Union_def} Union S == (UN x:S. x) +\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} +\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace} +\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace} +\end{ttbox} +\caption{Rules of the theory \texttt{Set}} \label{hol-set-rules} +\end{figure} + + +\begin{figure} \underscoreon +\begin{ttbox} +\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace} +\tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a +\tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W + +\tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x +\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x +\tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q + +\tdx{bexI} [| P x; x:A |] ==> ? x:A. P x +\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x +\tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q +\subcaption{Comprehension and Bounded quantifiers} + +\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B +\tdx{subsetD} [| A <= B; c:A |] ==> c:B +\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P + +\tdx{subset_refl} A <= A +\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C + +\tdx{equalityI} [| A <= B; B <= A |] ==> A = B +\tdx{equalityD1} A = B ==> A<=B +\tdx{equalityD2} A = B ==> B<=A +\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P + +\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P; + [| ~ c:A; ~ c:B |] ==> P + |] ==> P +\subcaption{The subset and equality relations} +\end{ttbox} +\caption{Derived rules for set theory} \label{hol-set1} +\end{figure} + + +\begin{figure} \underscoreon +\begin{ttbox} +\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P + +\tdx{insertI1} a : insert a B +\tdx{insertI2} a : B ==> a : insert b B +\tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P + +\tdx{ComplI} [| c:A ==> False |] ==> c : -A +\tdx{ComplD} [| c : -A |] ==> ~ c:A + +\tdx{UnI1} c:A ==> c : A Un B +\tdx{UnI2} c:B ==> c : A Un B +\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B +\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P + +\tdx{IntI} [| c:A; c:B |] ==> c : A Int B +\tdx{IntD1} c : A Int B ==> c:A +\tdx{IntD2} c : A Int B ==> c:B +\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P + +\tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x) +\tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R + +\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x) +\tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a +\tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R + +\tdx{UnionI} [| X:C; A:X |] ==> A : Union C +\tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R + +\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C +\tdx{InterD} [| A : Inter C; X:C |] ==> A:X +\tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R + +\tdx{PowI} A<=B ==> A: Pow B +\tdx{PowD} A: Pow B ==> A<=B + +\tdx{imageI} [| x:A |] ==> f x : f``A +\tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P + +\tdx{rangeI} f x : range f +\tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P +\end{ttbox} +\caption{Further derived rules for set theory} \label{hol-set2} +\end{figure} + + +\subsection{Axioms and rules of set theory} +Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The +axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert +that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of +course, \hbox{\tt op :} also serves as the membership relation. + +All the other axioms are definitions. They include the empty set, bounded +quantifiers, unions, intersections, complements and the subset relation. +They also include straightforward constructions on functions: image~({\tt``}) +and \texttt{range}. + +%The predicate \cdx{inj_on} is used for simulating type definitions. +%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the +%set~$A$, which specifies a subset of its domain type. In a type +%definition, $f$ is the abstraction function and $A$ is the set of valid +%representations; we should not expect $f$ to be injective outside of~$A$. + +%\begin{figure} \underscoreon +%\begin{ttbox} +%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x +%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y +% +%\tdx{Inv_injective} +% [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y +% +% +%\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f +%\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B +% +%\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f +%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f +%\tdx{injD} [| inj f; f x = f y |] ==> x=y +% +%\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A +%\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y +% +%\tdx{inj_on_inverseI} +% (!!x. x:A ==> g(f x) = x) ==> inj_on f A +%\tdx{inj_on_contraD} +% [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y +%\end{ttbox} +%\caption{Derived rules involving functions} \label{hol-fun} +%\end{figure} + + +\begin{figure} \underscoreon +\begin{ttbox} +\tdx{Union_upper} B:A ==> B <= Union A +\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C + +\tdx{Inter_lower} B:A ==> Inter A <= B +\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A + +\tdx{Un_upper1} A <= A Un B +\tdx{Un_upper2} B <= A Un B +\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C + +\tdx{Int_lower1} A Int B <= A +\tdx{Int_lower2} A Int B <= B +\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B +\end{ttbox} +\caption{Derived rules involving subsets} \label{hol-subset} +\end{figure} + + +\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message +\begin{ttbox} +\tdx{Int_absorb} A Int A = A +\tdx{Int_commute} A Int B = B Int A +\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) +\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) + +\tdx{Un_absorb} A Un A = A +\tdx{Un_commute} A Un B = B Un A +\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) +\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) + +\tdx{Compl_disjoint} A Int (-A) = {\ttlbrace}x. False{\ttrbrace} +\tdx{Compl_partition} A Un (-A) = {\ttlbrace}x. True{\ttrbrace} +\tdx{double_complement} -(-A) = A +\tdx{Compl_Un} -(A Un B) = (-A) Int (-B) +\tdx{Compl_Int} -(A Int B) = (-A) Un (-B) + +\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B) +\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C) + +\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B) +\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C) + +\end{ttbox} +\caption{Set equalities} \label{hol-equalities} +\end{figure} +%\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) +%\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) + +Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are +obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such +as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical +reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are +not strictly necessary but yield more natural proofs. Similarly, +\tdx{equalityCE} supports classical reasoning about extensionality, after the +fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs +pertaining to set theory. + +Figure~\ref{hol-subset} presents lattice properties of the subset relation. +Unions form least upper bounds; non-empty intersections form greatest lower +bounds. Reasoning directly about subsets often yields clearer proofs than +reasoning about the membership relation. See the file \texttt{HOL/subset.ML}. + +Figure~\ref{hol-equalities} presents many common set equalities. They +include commutative, associative and distributive laws involving unions, +intersections and complements. For a complete listing see the file {\tt +HOL/equalities.ML}. + +\begin{warn} +\texttt{Blast_tac} proves many set-theoretic theorems automatically. +Hence you seldom need to refer to the theorems above. +\end{warn} + +\begin{figure} +\begin{center} +\begin{tabular}{rrr} + \it name &\it meta-type & \it description \\ + \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ + & injective/surjective \\ + \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$ + & injective over subset\\ + \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function +\end{tabular} +\end{center} + +\underscoreon +\begin{ttbox} +\tdx{inj_def} inj f == ! x y. f x=f y --> x=y +\tdx{surj_def} surj f == ! y. ? x. y=f x +\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y +\tdx{inv_def} inv f == (\%y. @x. f(x)=y) +\end{ttbox} +\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun} +\end{figure} + +\subsection{Properties of functions}\nopagebreak +Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. +Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse +of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived +rules. Reasoning about function composition (the operator~\sdx{o}) and the +predicate~\cdx{surj} is done simply by expanding the definitions. + +There is also a large collection of monotonicity theorems for constructions +on sets in the file \texttt{HOL/mono.ML}. + + +\section{Simplification and substitution} + +Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset +(\texttt{simpset()}), which works for most purposes. A quite minimal +simplification set for higher-order logic is~\ttindexbold{HOL_ss}; +even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which +also expresses logical equivalence, may be used for rewriting. See +the file \texttt{HOL/simpdata.ML} for a complete listing of the basic +simplification rules. + +See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% +{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution +and simplification. + +\begin{warn}\index{simplification!of conjunctions}% + Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The + left part of a conjunction helps in simplifying the right part. This effect + is not available by default: it can be slow. It can be obtained by + including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. +\end{warn} + +\begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}% + By default only the condition of an \ttindex{if} is simplified but not the + \texttt{then} and \texttt{else} parts. Of course the latter are simplified + once the condition simplifies to \texttt{True} or \texttt{False}. To ensure + full simplification of all parts of a conditional you must remove + \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$. +\end{warn} + +If the simplifier cannot use a certain rewrite rule --- either because +of nontermination or because its left-hand side is too flexible --- +then you might try \texttt{stac}: +\begin{ttdescription} +\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$, + replaces in subgoal $i$ instances of $lhs$ by corresponding instances of + $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking + may be necessary to select the desired ones. + +If $thm$ is a conditional equality, the instantiated condition becomes an +additional (first) subgoal. +\end{ttdescription} + +HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an +equality throughout a subgoal and its hypotheses. This tactic uses HOL's +general substitution rule. + +\subsection{Case splitting} +\label{subsec:HOL:case:splitting} + +HOL also provides convenient means for case splitting during rewriting. Goals +containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots} +often require a case distinction on $b$. This is expressed by the theorem +\tdx{split_if}: +$$ +\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~ +((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y}))) +\eqno{(*)} +$$ +For example, a simple instance of $(*)$ is +\[ +x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~ +((x \in A \to x \in A) \land (x \notin A \to x \in \{x\})) +\] +Because $(*)$ is too general as a rewrite rule for the simplifier (the +left-hand side is not a higher-order pattern in the sense of +\iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}% +{Chap.\ts\ref{chap:simplification}}), there is a special infix function +\ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset} +(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a +simpset, as in +\begin{ttbox} +by(simp_tac (simpset() addsplits [split_if]) 1); +\end{ttbox} +The effect is that after each round of simplification, one occurrence of +\texttt{if} is split acording to \texttt{split_if}, until all occurences of +\texttt{if} have been eliminated. + +It turns out that using \texttt{split_if} is almost always the right thing to +do. Hence \texttt{split_if} is already included in the default simpset. If +you want to delete it from a simpset, use \ttindexbold{delsplits}, which is +the inverse of \texttt{addsplits}: +\begin{ttbox} +by(simp_tac (simpset() delsplits [split_if]) 1); +\end{ttbox} + +In general, \texttt{addsplits} accepts rules of the form +\[ +\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs +\] +where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the +right form because internally the left-hand side is +$\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples +are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list} +and~{\S}\ref{subsec:datatype:basics}). + +Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also +imperative versions of \texttt{addsplits} and \texttt{delsplits} +\begin{ttbox} +\ttindexbold{Addsplits}: thm list -> unit +\ttindexbold{Delsplits}: thm list -> unit +\end{ttbox} +for adding splitting rules to, and deleting them from the current simpset. + + +\section{Types}\label{sec:HOL:Types} +This section describes HOL's basic predefined types ($\alpha \times \beta$, +$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new +types in general. The most important type construction, the +\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}. + + +\subsection{Product and sum types}\index{*"* type}\index{*"+ type} +\label{subsec:prod-sum} + +\begin{figure}[htbp] +\begin{constants} + \it symbol & \it meta-type & & \it description \\ + \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ + & & ordered pairs $(a,b)$ \\ + \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ + \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ + \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ + & & generalized projection\\ + \cdx{Sigma} & + $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & + & general sum of sets +\end{constants} +%\tdx{fst_def} fst p == @a. ? b. p = (a,b) +%\tdx{snd_def} snd p == @b. ? a. p = (a,b) +%\tdx{split_def} split c p == c (fst p) (snd p) +\begin{ttbox}\makeatletter +\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace} + +\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b') +\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R +\tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q + +\tdx{fst_conv} fst (a,b) = a +\tdx{snd_conv} snd (a,b) = b +\tdx{surjective_pairing} p = (fst p,snd p) + +\tdx{split} split c (a,b) = c a b +\tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y)) + +\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B + +\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P + |] ==> P +\end{ttbox} +\caption{Type $\alpha\times\beta$}\label{hol-prod} +\end{figure} + +Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type +$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General +tuples are simulated by pairs nested to the right: +\begin{center} +\begin{tabular}{c|c} +external & internal \\ +\hline +$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\ +\hline +$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\ +\end{tabular} +\end{center} +In addition, it is possible to use tuples +as patterns in abstractions: +\begin{center} +{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} +\end{center} +Nested patterns are also supported. They are translated stepwise: +\begin{eqnarray*} +\hbox{\tt\%($x$,$y$,$z$).\ $t$} + & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\ + & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\ + & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))} +\end{eqnarray*} +The reverse translation is performed upon printing. +\begin{warn} + The translation between patterns and \texttt{split} is performed automatically + by the parser and printer. Thus the internal and external form of a term + may differ, which can affects proofs. For example the term {\tt + (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the + default simpset) to rewrite to {\tt(b,a)}. +\end{warn} +In addition to explicit $\lambda$-abstractions, patterns can be used in any +variable binding construct which is internally described by a +$\lambda$-abstraction. Some important examples are +\begin{description} +\item[Let:] \texttt{let {\it pattern} = $t$ in $u$} +\item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$} +\item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$} +\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} +\item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}} +\end{description} + +There is a simple tactic which supports reasoning about patterns: +\begin{ttdescription} +\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all + {\tt!!}-quantified variables of product type by individual variables for + each component. A simple example: +\begin{ttbox} +{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} +by(split_all_tac 1); +{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} +\end{ttbox} +\end{ttdescription} + +Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit} +which contains only a single element named {\tt()} with the property +\begin{ttbox} +\tdx{unit_eq} u = () +\end{ttbox} +\bigskip + +Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$ +which associates to the right and has a lower priority than $*$: $\tau@1 + +\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$. + +The definition of products and sums in terms of existing types is not +shown. The constructions are fairly standard and can be found in the +respective theory files. Although the sum and product types are +constructed manually for foundational reasons, they are represented as +actual datatypes later. + +\begin{figure} +\begin{constants} + \it symbol & \it meta-type & & \it description \\ + \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ + \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ + \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ + & & conditional +\end{constants} +\begin{ttbox}\makeatletter +\tdx{Inl_not_Inr} Inl a ~= Inr b + +\tdx{inj_Inl} inj Inl +\tdx{inj_Inr} inj Inr + +\tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s + +\tdx{sum_case_Inl} sum_case f g (Inl x) = f x +\tdx{sum_case_Inr} sum_case f g (Inr x) = g x + +\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s +\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) & + (! y. s = Inr(y) --> R(g(y)))) +\end{ttbox} +\caption{Type $\alpha+\beta$}\label{hol-sum} +\end{figure} + +\begin{figure} +\index{*"< symbol} +\index{*"* symbol} +\index{*div symbol} +\index{*mod symbol} +\index{*dvd symbol} +\index{*"+ symbol} +\index{*"- symbol} +\begin{constants} + \it symbol & \it meta-type & \it priority & \it description \\ + \cdx{0} & $\alpha$ & & zero \\ + \cdx{Suc} & $nat \To nat$ & & successor function\\ + \tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\ + \tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\ + \tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\ + \tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & ``divides'' relation\\ + \tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\ + \tt - & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction +\end{constants} +\subcaption{Constants and infixes} + +\begin{ttbox}\makeatother +\tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n + +\tdx{Suc_not_Zero} Suc m ~= 0 +\tdx{inj_Suc} inj Suc +\tdx{n_not_Suc_n} n~=Suc n +\subcaption{Basic properties} +\end{ttbox} +\caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1} +\end{figure} + + +\begin{figure} +\begin{ttbox}\makeatother + 0+n = n + (Suc m)+n = Suc(m+n) + + m-0 = m + 0-n = n + Suc(m)-Suc(n) = m-n + + 0*n = 0 + Suc(m)*n = n + m*n + +\tdx{mod_less} m m mod n = m +\tdx{mod_geq} [| 0 m mod n = (m-n) mod n + +\tdx{div_less} m m div n = 0 +\tdx{div_geq} [| 0 m div n = Suc((m-n) div n) +\end{ttbox} +\caption{Recursion equations for the arithmetic operators} \label{hol-nat2} +\end{figure} + +\subsection{The type of natural numbers, \textit{nat}} +\index{nat@{\textit{nat}} type|(} + +The theory \thydx{Nat} defines the natural numbers in a roundabout but +traditional way. The axiom of infinity postulates a type~\tydx{ind} of +individuals, which is non-empty and closed under an injective operation. The +natural numbers are inductively generated by choosing an arbitrary individual +for~0 and using the injective operation to take successors. This is a least +fixedpoint construction. + +Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded +functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min}, +\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} +also shows that {\tt<=} is a linear order, so \tydx{nat} is +also an instance of class \cldx{linorder}. + +Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines +addition, multiplication and subtraction. Theory \thydx{Divides} defines +division, remainder and the ``divides'' relation. The numerous theorems +proved include commutative, associative, distributive, identity and +cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The +recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on +\texttt{nat} are part of the default simpset. + +Functions on \tydx{nat} can be defined by primitive or well-founded recursion; +see {\S}\ref{sec:HOL:recursive}. A simple example is addition. +Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following +the standard convention. +\begin{ttbox} +\sdx{primrec} + "0 + n = n" + "Suc m + n = Suc (m + n)" +\end{ttbox} +There is also a \sdx{case}-construct +of the form +\begin{ttbox} +case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) +\end{ttbox} +Note that Isabelle insists on precisely this format; you may not even change +the order of the two cases. +Both \texttt{primrec} and \texttt{case} are realized by a recursion operator +\cdx{nat_rec}, which is available because \textit{nat} is represented as +a datatype. + +%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. +%Recursion along this relation resembles primitive recursion, but is +%stronger because we are in higher-order logic; using primitive recursion to +%define a higher-order function, we can easily Ackermann's function, which +%is not primitive recursive \cite[page~104]{thompson91}. +%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the +%natural numbers are most easily expressed using recursion along~$<$. + +Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ +in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived +theorem \tdx{less_induct}: +\begin{ttbox} +[| !!n. [| ! m. m P m |] ==> P n |] ==> P n +\end{ttbox} + + +\subsection{Numerical types and numerical reasoning} + +The integers (type \tdx{int}) are also available in HOL, and the reals (type +\tdx{real}) are available in the logic image \texttt{HOL-Complex}. They support +the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and +multiplication (\texttt{*}), and much else. Type \tdx{int} provides the +\texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real +division and other operations. Both types belong to class \cldx{linorder}, so +they inherit the relational operators and all the usual properties of linear +orderings. For full details, please survey the theories in subdirectories +\texttt{Integ}, \texttt{Real}, and \texttt{Complex}. + +All three numeric types admit numerals of the form \texttt{$sd\ldots d$}, +where $s$ is an optional minus sign and $d\ldots d$ is a string of digits. +Numerals are represented internally by a datatype for binary notation, which +allows numerical calculations to be performed by rewriting. For example, the +integer division of \texttt{54342339} by \texttt{3452} takes about five +seconds. By default, the simplifier cancels like terms on the opposite sites +of relational operators (reducing \texttt{z+x [] | Suc(m) => x # take m xs) + +drop n [] = [] +drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs) + +takeWhile P [] = [] +takeWhile P (x#xs) = (if P x then x#takeWhile P xs else []) + +dropWhile P [] = [] +dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) +\end{ttbox} +\caption{Further list processing functions} +\label{fig:HOL:list-simps2} +\end{figure} + + +\subsection{The type constructor for lists, \textit{list}} +\label{subsec:list} +\index{list@{\textit{list}} type|(} + +Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list +operations with their types and syntax. Type $\alpha \; list$ is +defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}. +As a result the generic structural induction and case analysis tactics +\texttt{induct\_tac} and \texttt{cases\_tac} also become available for +lists. A \sdx{case} construct of the form +\begin{center}\tt +case $e$ of [] => $a$ | \(x\)\#\(xs\) => b +\end{center} +is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There +is also a case splitting rule \tdx{split_list_case} +\[ +\begin{array}{l} +P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~ + x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\ +((e = \texttt{[]} \to P(a)) \land + (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs))) +\end{array} +\] +which can be fed to \ttindex{addsplits} just like +\texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}). + +\texttt{List} provides a basic library of list processing functions defined by +primitive recursion. The recursion equations +are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}. + +\index{list@{\textit{list}} type|)} + + +\section{Datatype definitions} +\label{sec:HOL:datatype} +\index{*datatype|(} + +Inductive datatypes, similar to those of \ML, frequently appear in +applications of Isabelle/HOL. In principle, such types could be defined by +hand via \texttt{typedef}, but this would be far too +tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ +\cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an +appropriate \texttt{typedef} based on a least fixed-point construction, and +proves freeness theorems and induction rules, as well as theorems for +recursion and case combinators. The user just has to give a simple +specification of new inductive types using a notation similar to {\ML} or +Haskell. + +The current datatype package can handle both mutual and indirect recursion. +It also offers to represent existing types as datatypes giving the advantage +of a more uniform view on standard theories. + + +\subsection{Basics} +\label{subsec:datatype:basics} + +A general \texttt{datatype} definition is of the following form: +\[ +\begin{array}{llcl} +\mathtt{datatype} & (\vec{\alpha})t@1 & = & + C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~ + C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\ + & & \vdots \\ +\mathtt{and} & (\vec{\alpha})t@n & = & + C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~ + C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}} +\end{array} +\] +where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables, +$C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em + admissible} types containing at most the type variables $\alpha@1, \ldots, +\alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em + admissible} if and only if +\begin{itemize} +\item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the +newly defined type constructors $t@1,\ldots,t@n$, or +\item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or +\item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is +the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$ +are admissible types. +\item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible +type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined +types are {\em strictly positive}) +\end{itemize} +If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$ +of the form +\[ +(\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t' +\] +this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple +example of a datatype is the type \texttt{list}, which can be defined by +\begin{ttbox} +datatype 'a list = Nil + | Cons 'a ('a list) +\end{ttbox} +Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled +by the mutually recursive datatype definition +\begin{ttbox} +datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp) + | Sum ('a aexp) ('a aexp) + | Diff ('a aexp) ('a aexp) + | Var 'a + | Num nat +and 'a bexp = Less ('a aexp) ('a aexp) + | And ('a bexp) ('a bexp) + | Or ('a bexp) ('a bexp) +\end{ttbox} +The datatype \texttt{term}, which is defined by +\begin{ttbox} +datatype ('a, 'b) term = Var 'a + | App 'b ((('a, 'b) term) list) +\end{ttbox} +is an example for a datatype with nested recursion. Using nested recursion +involving function spaces, we may also define infinitely branching datatypes, e.g. +\begin{ttbox} +datatype 'a tree = Atom 'a | Branch "nat => 'a tree" +\end{ttbox} + +\medskip + +Types in HOL must be non-empty. Each of the new datatypes +$(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a +constructor $C^j@i$ with the following property: for all argument types +$\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype +$(\vec{\alpha})t@{j'}$ is non-empty. + +If there are no nested occurrences of the newly defined datatypes, obviously +at least one of the newly defined datatypes $(\vec{\alpha})t@j$ +must have a constructor $C^j@i$ without recursive arguments, a \emph{base + case}, to ensure that the new types are non-empty. If there are nested +occurrences, a datatype can even be non-empty without having a base case +itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t + list)} is non-empty as well. + + +\subsubsection{Freeness of the constructors} + +The datatype constructors are automatically defined as functions of their +respective type: +\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \] +These functions have certain {\em freeness} properties. They construct +distinct values: +\[ +C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad +\mbox{for all}~ i \neq i'. +\] +The constructor functions are injective: +\[ +(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) = +(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i}) +\] +Since the number of distinctness inequalities is quadratic in the number of +constructors, the datatype package avoids proving them separately if there are +too many constructors. Instead, specific inequalities are proved by a suitable +simplification procedure on demand.\footnote{This procedure, which is already part +of the default simpset, may be referred to by the ML identifier +\texttt{DatatypePackage.distinct_simproc}.} + +\subsubsection{Structural induction} + +The datatype package also provides structural induction rules. For +datatypes without nested recursion, this is of the following form: +\[ +\infer{P@1~x@1 \land \dots \land P@n~x@n} + {\begin{array}{lcl} + \Forall x@1 \dots x@{m^1@1}. + \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots; + P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp & + P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\ + & \vdots \\ + \Forall x@1 \dots x@{m^1@{k@1}}. + \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots; + P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp & + P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\ + & \vdots \\ + \Forall x@1 \dots x@{m^n@1}. + \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots; + P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp & + P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\ + & \vdots \\ + \Forall x@1 \dots x@{m^n@{k@n}}. + \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots + P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp & + P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right) + \end{array}} +\] +where +\[ +\begin{array}{rcl} +Rec^j@i & := & + \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, + \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex] +&& \left\{(i',i'')~\left|~ + 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land + \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\} +\end{array} +\] +i.e.\ the properties $P@j$ can be assumed for all recursive arguments. + +For datatypes with nested recursion, such as the \texttt{term} example from +above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds +a definition like +\begin{ttbox} +datatype ('a,'b) term = Var 'a + | App 'b ((('a, 'b) term) list) +\end{ttbox} +to an equivalent definition without nesting: +\begin{ttbox} +datatype ('a,'b) term = Var + | App 'b (('a, 'b) term_list) +and ('a,'b) term_list = Nil' + | Cons' (('a,'b) term) (('a,'b) term_list) +\end{ttbox} +Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt + Nil'} and \texttt{Cons'} are not really introduced. One can directly work with +the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing +constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for +\texttt{term} gets the form +\[ +\infer{P@1~x@1 \land P@2~x@2} + {\begin{array}{l} + \Forall x.~P@1~(\mathtt{Var}~x) \\ + \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\ + P@2~\mathtt{Nil} \\ + \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2) + \end{array}} +\] +Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term} +and one for the type \texttt{(('a, 'b) term) list}. + +For a datatype with function types such as \texttt{'a tree}, the induction rule +is of the form +\[ +\infer{P~t} + {\Forall a.~P~(\mathtt{Atom}~a) & + \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)} +\] + +\medskip In principle, inductive types are already fully determined by +freeness and structural induction. For convenience in applications, +the following derived constructions are automatically provided for any +datatype. + +\subsubsection{The \sdx{case} construct} + +The type comes with an \ML-like \texttt{case}-construct: +\[ +\begin{array}{rrcl} +\mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\ + \vdots \\ + \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j} +\end{array} +\] +where the $x@{i,j}$ are either identifiers or nested tuple patterns as in +{\S}\ref{subsec:prod-sum}. +\begin{warn} + All constructors must be present, their order is fixed, and nested patterns + are not supported (with the exception of tuples). Violating this + restriction results in strange error messages. +\end{warn} + +To perform case distinction on a goal containing a \texttt{case}-construct, +the theorem $t@j.$\texttt{split} is provided: +\[ +\begin{array}{@{}rcl@{}} +P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=& +\!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to + P(f@1~x@1\dots x@{m^j@1})) \\ +&&\!\!\! ~\land~ \dots ~\land \\ +&&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to + P(f@{k@j}~x@1\dots x@{m^j@{k@j}}))) +\end{array} +\] +where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct. +This theorem can be added to a simpset via \ttindex{addsplits} +(see~{\S}\ref{subsec:HOL:case:splitting}). + +Case splitting on assumption works as well, by using the rule +$t@j.$\texttt{split_asm} in the same manner. Both rules are available under +$t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though). + +\begin{warn}\index{simplification!of \texttt{case}}% + By default only the selector expression ($e$ above) in a + \texttt{case}-construct is simplified, in analogy with \texttt{if} (see + page~\pageref{if-simp}). Only if that reduces to a constructor is one of + the arms of the \texttt{case}-construct exposed and simplified. To ensure + full simplification of all parts of a \texttt{case}-construct for datatype + $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for + example by \texttt{delcongs [thm "$t$.weak_case_cong"]}. +\end{warn} + +\subsubsection{The function \cdx{size}}\label{sec:HOL:size} + +Theory \texttt{NatArith} declares a generic function \texttt{size} of type +$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size} +by overloading according to the following scheme: +%%% FIXME: This formula is too big and is completely unreadable +\[ +size(C^j@i~x@1~\dots~x@{m^j@i}) = \! +\left\{ +\begin{array}{ll} +0 & \!\mbox{if $Rec^j@i = \emptyset$} \\ +1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} & + \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, + \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$} +\end{array} +\right. +\] +where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the +size of a leaf is 0 and the size of a node is the sum of the sizes of its +subtrees ${}+1$. + +\subsection{Defining datatypes} + +The theory syntax for datatype definitions is given in the +Isabelle/Isar reference manual. In order to be well-formed, a +datatype definition has to obey the rules stated in the previous +section. As a result the theory is extended with the new types, the +constructors, and the theorems listed in the previous section. + +Most of the theorems about datatypes become part of the default simpset and +you never need to see them again because the simplifier applies them +automatically. Only induction or case distinction are usually invoked by hand. +\begin{ttdescription} +\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] + applies structural induction on variable $x$ to subgoal $i$, provided the + type of $x$ is a datatype. +\item[\texttt{induct_tac} + {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous + structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This + is the canonical way to prove properties of mutually recursive datatypes + such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as + \texttt{term}. +\end{ttdescription} +In some cases, induction is overkill and a case distinction over all +constructors of the datatype suffices. +\begin{ttdescription} +\item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$] + performs a case analysis for the term $u$ whose type must be a datatype. + If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal + $i$ is replaced by $k@j$ new subgoals which contain the additional + assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for $i'=1$, $\dots$,~$k@j$. +\end{ttdescription} + +Note that induction is only allowed on free variables that should not occur +among the premises of the subgoal. Case distinction applies to arbitrary terms. + +\bigskip + + +For the technically minded, we exhibit some more details. Processing the +theory file produces an \ML\ structure which, in addition to the usual +components, contains a structure named $t$ for each datatype $t$ defined in +the file. Each structure $t$ contains the following elements: +\begin{ttbox} +val distinct : thm list +val inject : thm list +val induct : thm +val exhaust : thm +val cases : thm list +val split : thm +val split_asm : thm +val recs : thm list +val size : thm list +val simps : thm list +\end{ttbox} +\texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size} +and \texttt{split} contain the theorems +described above. For user convenience, \texttt{distinct} contains +inequalities in both directions. The reduction rules of the {\tt + case}-construct are in \texttt{cases}. All theorems from {\tt + distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. +In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct} +and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. + + +\section{Old-style recursive function definitions}\label{sec:HOL:recursive} +\index{recursion!general|(} +\index{*recdef|(} + +Old-style recursive definitions via \texttt{recdef} requires that you +supply a well-founded relation that governs the recursion. Recursive +calls are only allowed if they make the argument decrease under the +relation. Complicated recursion forms, such as nested recursion, can +be dealt with. Termination can even be proved at a later time, though +having unsolved termination conditions around can make work +difficult.% +\footnote{This facility is based on Konrad Slind's TFL + package~\cite{slind-tfl}. Thanks are due to Konrad for implementing + TFL and assisting with its installation.} + +Using \texttt{recdef}, you can declare functions involving nested recursion +and pattern-matching. Recursion need not involve datatypes and there are few +syntactic restrictions. Termination is proved by showing that each recursive +call makes the argument smaller in a suitable sense, which you specify by +supplying a well-founded relation. + +Here is a simple example, the Fibonacci function. The first line declares +\texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on +the natural numbers). Pattern-matching is used here: \texttt{1} is a +macro for \texttt{Suc~0}. +\begin{ttbox} +consts fib :: "nat => nat" +recdef fib "less_than" + "fib 0 = 0" + "fib 1 = 1" + "fib (Suc(Suc x)) = (fib x + fib (Suc x))" +\end{ttbox} + +With \texttt{recdef}, function definitions may be incomplete, and patterns may +overlap, as in functional programming. The \texttt{recdef} package +disambiguates overlapping patterns by taking the order of rules into account. +For missing patterns, the function is defined to return a default value. + +%For example, here is a declaration of the list function \cdx{hd}: +%\begin{ttbox} +%consts hd :: 'a list => 'a +%recdef hd "\{\}" +% "hd (x#l) = x" +%\end{ttbox} +%Because this function is not recursive, we may supply the empty well-founded +%relation, $\{\}$. + +The well-founded relation defines a notion of ``smaller'' for the function's +argument type. The relation $\prec$ is \textbf{well-founded} provided it +admits no infinitely decreasing chains +\[ \cdots\prec x@n\prec\cdots\prec x@1. \] +If the function's argument has type~$\tau$, then $\prec$ has to be a relation +over~$\tau$: it must have type $(\tau\times\tau)set$. + +Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection +of operators for building well-founded relations. The package recognises +these operators and automatically proves that the constructed relation is +well-founded. Here are those operators, in order of importance: +\begin{itemize} +\item \texttt{less_than} is ``less than'' on the natural numbers. + (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$. + +\item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the + relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if + $f(x)}R@2$ is the lexicographic product of two relations. + It + is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only + if $x@1$ + is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$ + is less than $y@2$ according to~$R@2$. + +\item \texttt{finite_psubset} is the proper subset relation on finite sets. +\end{itemize} + +We can use \texttt{measure} to declare Euclid's algorithm for the greatest +common divisor. The measure function, $\lambda(m,n). n$, specifies that the +recursion terminates because argument~$n$ decreases. +\begin{ttbox} +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" +\end{ttbox} + +The general form of a well-founded recursive definition is +\begin{ttbox} +recdef {\it function} {\it rel} + congs {\it congruence rules} {\bf(optional)} + simpset {\it simplification set} {\bf(optional)} + {\it reduction rules} +\end{ttbox} +where +\begin{itemize} +\item \textit{function} is the name of the function, either as an \textit{id} + or a \textit{string}. + +\item \textit{rel} is a HOL expression for the well-founded termination + relation. + +\item \textit{congruence rules} are required only in highly exceptional + circumstances. + +\item The \textit{simplification set} is used to prove that the supplied + relation is well-founded. It is also used to prove the \textbf{termination + conditions}: assertions that arguments of recursive calls decrease under + \textit{rel}. By default, simplification uses \texttt{simpset()}, which + is sufficient to prove well-foundedness for the built-in relations listed + above. + +\item \textit{reduction rules} specify one or more recursion equations. Each + left-hand side must have the form $f\,t$, where $f$ is the function and $t$ + is a tuple of distinct variables. If more than one equation is present then + $f$ is defined by pattern-matching on components of its argument whose type + is a \texttt{datatype}. + + The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as + a list of theorems. +\end{itemize} + +With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to +prove one termination condition. It remains as a precondition of the +recursion theorems: +\begin{ttbox} +gcd.simps; +{\out ["! m n. n ~= 0 --> m mod n < n} +{\out ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] } +{\out : thm list} +\end{ttbox} +The theory \texttt{HOL/ex/Primes} illustrates how to prove termination +conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard +function \texttt{goalw}, which sets up a goal to prove, but its argument +should be the identifier $f$\texttt{.simps} and its effect is to set up a +proof of the termination conditions: +\begin{ttbox} +Tfl.tgoalw thy [] gcd.simps; +{\out Level 0} +{\out ! m n. n ~= 0 --> m mod n < n} +{\out 1. ! m n. n ~= 0 --> m mod n < n} +\end{ttbox} +This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem +is proved, it can be used to eliminate the termination conditions from +elements of \texttt{gcd.simps}. Theory \texttt{HOL/Subst/Unify} is a much +more complicated example of this process, where the termination conditions can +only be proved by complicated reasoning involving the recursive function +itself. + +Isabelle/HOL can prove the \texttt{gcd} function's termination condition +automatically if supplied with the right simpset. +\begin{ttbox} +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" + simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" +\end{ttbox} + +If all termination conditions were proved automatically, $f$\texttt{.simps} +is added to the simpset automatically, just as in \texttt{primrec}. +The simplification rules corresponding to clause $i$ (where counting starts +at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms + "$f$.$i$"}, +which returns a list of theorems. Thus you can, for example, remove specific +clauses from the simpset. Note that a single clause may give rise to a set of +simplification rules in order to capture the fact that if clauses overlap, +their order disambiguates them. + +A \texttt{recdef} definition also returns an induction rule specialised for +the recursive function. For the \texttt{gcd} function above, the induction +rule is +\begin{ttbox} +gcd.induct; +{\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm} +\end{ttbox} +This rule should be used to reason inductively about the \texttt{gcd} +function. It usually makes the induction hypothesis available at all +recursive calls, leading to very direct proofs. If any termination conditions +remain unproved, they will become additional premises of this rule. + +\index{recursion!general|)} +\index{*recdef|)} + + +\section{Example: Cantor's Theorem}\label{sec:hol-cantor} +Cantor's Theorem states that every set has more subsets than it has +elements. It has become a favourite example in higher-order logic since +it is so easily expressed: +\[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool. + \forall x::\alpha. f~x \not= S +\] +% +Viewing types as sets, $\alpha\To bool$ represents the powerset +of~$\alpha$. This version states that for every function from $\alpha$ to +its powerset, some subset is outside its range. + +The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and +the operator \cdx{range}. +\begin{ttbox} +context Set.thy; +\end{ttbox} +The set~$S$ is given as an unknown instead of a +quantified variable so that we may inspect the subset found by the proof. +\begin{ttbox} +Goal "?S ~: range\thinspace(f :: 'a=>'a set)"; +{\out Level 0} +{\out ?S ~: range f} +{\out 1. ?S ~: range f} +\end{ttbox} +The first two steps are routine. The rule \tdx{rangeE} replaces +$\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$. +\begin{ttbox} +by (resolve_tac [notI] 1); +{\out Level 1} +{\out ?S ~: range f} +{\out 1. ?S : range f ==> False} +\ttbreak +by (eresolve_tac [rangeE] 1); +{\out Level 2} +{\out ?S ~: range f} +{\out 1. !!x. ?S = f x ==> False} +\end{ttbox} +Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, +we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for +any~$\Var{c}$. +\begin{ttbox} +by (eresolve_tac [equalityCE] 1); +{\out Level 3} +{\out ?S ~: range f} +{\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False} +{\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False} +\end{ttbox} +Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a +comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies +$\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD} +instantiates~$\Var{S}$ and creates the new assumption. +\begin{ttbox} +by (dresolve_tac [CollectD] 1); +{\out Level 4} +{\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f} +{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} +{\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False} +\end{ttbox} +Forcing a contradiction between the two assumptions of subgoal~1 +completes the instantiation of~$S$. It is now the set $\{x. x\not\in +f~x\}$, which is the standard diagonal construction. +\begin{ttbox} +by (contr_tac 1); +{\out Level 5} +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} +{\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False} +\end{ttbox} +The rest should be easy. To apply \tdx{CollectI} to the negated +assumption, we employ \ttindex{swap_res_tac}: +\begin{ttbox} +by (swap_res_tac [CollectI] 1); +{\out Level 6} +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} +{\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x} +\ttbreak +by (assume_tac 1); +{\out Level 7} +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} +{\out No subgoals!} +\end{ttbox} +How much creativity is required? As it happens, Isabelle can prove this +theorem automatically. The default classical set \texttt{claset()} contains +rules for most of the constructs of HOL's set theory. We must augment it with +\tdx{equalityCE} to break up set equalities, and then apply best-first search. +Depth-first search would diverge, but best-first search successfully navigates +through the large search space. \index{search!best-first} +\begin{ttbox} +choplev 0; +{\out Level 0} +{\out ?S ~: range f} +{\out 1. ?S ~: range f} +\ttbreak +by (best_tac (claset() addSEs [equalityCE]) 1); +{\out Level 1} +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} +{\out No subgoals!} +\end{ttbox} +If you run this example interactively, make sure your current theory contains +theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}. +Otherwise the default claset may not contain the rules for set theory. +\index{higher-order logic|)} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "logics-HOL" +%%% End: diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/document/build --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/HOL/document/build Mon Aug 27 21:37:34 2012 +0200 @@ -0,0 +1,26 @@ +#!/bin/bash + +set -e + +FORMAT="$1" +VARIANT="$2" + +"$ISABELLE_TOOL" logo -o isabelle_hol.pdf "HOL" +"$ISABELLE_TOOL" logo -o isabelle_hol.eps "HOL" + +cp "$ISABELLE_HOME/doc-src/iman.sty" . +cp "$ISABELLE_HOME/doc-src/extra.sty" . +cp "$ISABELLE_HOME/doc-src/ttbox.sty" . +cp "$ISABELLE_HOME/doc-src/proof.sty" . +cp "$ISABELLE_HOME/doc-src/manual.bib" . +cp "$ISABELLE_HOME/doc-src/Logics/document/syntax.tex" . + +"$ISABELLE_TOOL" latex -o sty +"$ISABELLE_TOOL" latex -o "$FORMAT" +"$ISABELLE_TOOL" latex -o bbl +"$ISABELLE_TOOL" latex -o "$FORMAT" +"$ISABELLE_TOOL" latex -o "$FORMAT" +"$ISABELLE_HOME/doc-src/sedindex" root +[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out +"$ISABELLE_TOOL" latex -o "$FORMAT" +"$ISABELLE_TOOL" latex -o "$FORMAT" diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/HOL/document/root.tex Mon Aug 27 21:37:34 2012 +0200 @@ -0,0 +1,60 @@ +\documentclass[12pt,a4paper]{report} +\usepackage{isabelle,isabellesym} +\usepackage{graphicx,iman,extra,ttbox,proof,latexsym,pdfsetup} + +%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} +%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} +%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} +%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} + + +\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] + Isabelle's Logics: HOL% + \thanks{The research has been funded by the EPSRC (grants GR/G53279, + GR\slash H40570, GR/K57381, GR/K77051, GR/M75440), by ESPRIT (projects 3245: + Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm + \emph{Deduktion}.}} + +\author{Tobias Nipkow\footnote +{Institut f\"ur Informatik, Technische Universit\"at M\"unchen, + \texttt{nipkow@in.tum.de}} and +Lawrence C. Paulson\footnote +{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}} and +Markus Wenzel\footnote +{Institut f\"ur Informatik, Technische Universit\"at M\"unchen, + \texttt{wenzelm@in.tum.de}}} + +\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip + \hrule\bigskip} +\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} + +\newcommand\bs{\char '134 } % A backslash character for \tt font + +\makeindex + +\underscoreoff + +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? + +\pagestyle{headings} +\sloppy +\binperiod %%%treat . like a binary operator + +\begin{document} +\maketitle + +\begin{abstract} + This manual describes Isabelle's formalization of Higher-Order Logic, a + polymorphic version of Church's Simple Theory of Types. HOL can be best + understood as a simply-typed version of classical set theory. The monograph + \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a + gentle introduction on using Isabelle/HOL in practice. +\end{abstract} + +\pagenumbering{roman} \tableofcontents \clearfirst +\input{syntax} +\include{HOL} +\bibliographystyle{plain} +\bibliography{manual} +\printindex +\end{document} diff -r ac15a85e9282 -r b5758f5a469c doc-src/HOL/logics-HOL.tex --- a/doc-src/HOL/logics-HOL.tex Mon Aug 27 21:30:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -\documentclass[12pt,a4paper]{report} -\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym} -\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup} - -%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} -%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} -%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} -%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} - - -\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] - Isabelle's Logics: HOL% - \thanks{The research has been funded by the EPSRC (grants GR/G53279, - GR\slash H40570, GR/K57381, GR/K77051, GR/M75440), by ESPRIT (projects 3245: - Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm - \emph{Deduktion}.}} - -\author{Tobias Nipkow\footnote -{Institut f\"ur Informatik, Technische Universit\"at M\"unchen, - \texttt{nipkow@in.tum.de}} and -Lawrence C. Paulson\footnote -{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}} and -Markus Wenzel\footnote -{Institut f\"ur Informatik, Technische Universit\"at M\"unchen, - \texttt{wenzelm@in.tum.de}}} - -\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip - \hrule\bigskip} -\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} - -\newcommand\bs{\char '134 } % A backslash character for \tt font - -\makeindex - -\underscoreoff - -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? - -\pagestyle{headings} -\sloppy -\binperiod %%%treat . like a binary operator - -\begin{document} -\maketitle - -\begin{abstract} - This manual describes Isabelle's formalization of Higher-Order Logic, a - polymorphic version of Church's Simple Theory of Types. HOL can be best - understood as a simply-typed version of classical set theory. The monograph - \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a - gentle introduction on using Isabelle/HOL in practice. -\end{abstract} - -\pagenumbering{roman} \tableofcontents \clearfirst -\input{../Logics/syntax} -\include{HOL} -\bibliographystyle{plain} -\bibliography{../manual} -\printindex -\end{document} diff -r ac15a85e9282 -r b5758f5a469c doc-src/ROOT --- a/doc-src/ROOT Mon Aug 27 21:30:18 2012 +0200 +++ b/doc-src/ROOT Mon Aug 27 21:37:34 2012 +0200 @@ -123,6 +123,19 @@ "document/build" "document/root.tex" +session "Logics-HOL" (doc) in "HOL" = Pure + + options [document_variants = "logics-HOL"] + theories + files + "../iman.sty" + "../extra.sty" + "../ttbox.sty" + "../proof.sty" + "../manual.bib" + "../Logics/document/syntax.tex" + "document/build" + "document/root.tex" + session Main (doc) in "Main" = HOL + options [document_variants = "main"] theories Main_Doc