--- 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!
--- 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 = <a,b>),
-\idx{snd_def} snd(p) == @b. ? a. p = <a,b>),
-\idx{split_def} split(p,c) == c(fst(p),snd(p)))
-
-\idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
-
-\idx{fst_conv} fst(<a,b>) = a
-\idx{snd_conv} snd(<a,b>) = b
-\idx{split_conv} split(<a,b>, c) = c(a,b)
-
-\idx{surjective_pairing} p = <fst(p),snd(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 = <n, Suc(n)>\} ),
-\idx{less_def} m<n == <m,n>: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} <n, Suc(n)> : pred_nat
-\idx{pred_natE}
- [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> 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<j; j<k |] ==> i<k
-\idx{lessI} n < Suc(n)
-\idx{zero_less_Suc} 0 < Suc(n)
-
-\idx{less_not_sym} n<m --> ~m<n
-\idx{less_not_refl} ~ (n<n)
-\idx{not_less0} ~ (n<0)
-
-\idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
-\idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
-
-\idx{less_linear} m<n | m=n | n<m
-
-
-----------------------------------------------------------------
-list.ML
-
- [([list], ([[term]],term))],
- ([Nil], 'a list),
- ([Cons], ['a, 'a list] => '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))
-
--- 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<n ==> m mod n = m
-\tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
-
-\tdx{div_less} m<n ==> m div n = 0
-\tdx{div_geq} [| 0<n; ~m<n |] ==> 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<n --> 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<x+y} to \texttt{z<y}, for
-instance. The simplifier also collects like terms, replacing \texttt{x+y+x*3}
-by \texttt{4*x+y}.
-
-Sometimes numerals are not wanted, because for example \texttt{n+3} does not
-match a pattern of the form \texttt{Suc $k$}. You can re-arrange the form of
-an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as
-\texttt{n+3 = Suc (Suc (Suc n))}. As an alternative, you can disable the
-fancier simplifications by using a basic simpset such as \texttt{HOL_ss}
-rather than the default one, \texttt{simpset()}.
-
-Reasoning about arithmetic inequalities can be tedious. Fortunately, HOL
-provides a decision procedure for \emph{linear arithmetic}: formulae involving
-addition and subtraction. The simplifier invokes a weak version of this
-decision procedure automatically. If this is not sufficent, you can invoke the
-full procedure \ttindex{Lin_Arith.tac} explicitly. It copes with arbitrary
-formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
- min}, {\tt max} and numerical constants. Other subterms are treated as
-atomic, while subformulae not involving numerical types are ignored. Quantified
-subformulae are ignored unless they are positive universal or negative
-existential. The running time is exponential in the number of
-occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
-distinctions.
-If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
-{\tt k dvd} are also supported. The former two are eliminated
-by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
-super-exponential time and space.
-
-If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in
-the library. The theories \texttt{Nat} and \texttt{NatArith} contain
-theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
-Theory \texttt{Divides} contains theorems about \texttt{div} and
-\texttt{mod}. Use Proof General's \emph{find} button (or other search
-facilities) to locate them.
-
-\index{nat@{\textit{nat}} type|)}
-
-
-\begin{figure}
-\index{#@{\tt[]} symbol}
-\index{#@{\tt\#} symbol}
-\index{"@@{\tt\at} symbol}
-\index{*"! symbol}
-\begin{constants}
- \it symbol & \it meta-type & \it priority & \it description \\
- \tt[] & $\alpha\,list$ & & empty list\\
- \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
- list constructor \\
- \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
- \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
- \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
- \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
- \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
- \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
- \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
- & & apply to all\\
- \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
- & & filter functional\\
- \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
- \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
- \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
- & iteration \\
- \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
- \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
- \cdx{length} & $\alpha\,list \To nat$ & & length \\
- \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
- \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
- take/drop a prefix \\
- \cdx{takeWhile},\\
- \cdx{dropWhile} &
- $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
- take/drop a prefix
-\end{constants}
-\subcaption{Constants and infixes}
-
-\begin{center} \tt\frenchspacing
-\begin{tabular}{rrr}
- \it external & \it internal & \it description \\{}
- [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
- \rm finite list \\{}
- [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
- \rm list comprehension
-\end{tabular}
-\end{center}
-\subcaption{Translations}
-\caption{The theory \thydx{List}} \label{hol-list}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}\makeatother
-null [] = True
-null (x#xs) = False
-
-hd (x#xs) = x
-
-tl (x#xs) = xs
-tl [] = []
-
-[] @ ys = ys
-(x#xs) @ ys = x # xs @ ys
-
-set [] = \ttlbrace\ttrbrace
-set (x#xs) = insert x (set xs)
-
-x mem [] = False
-x mem (y#ys) = (if y=x then True else x mem ys)
-
-concat([]) = []
-concat(x#xs) = x @ concat(xs)
-
-rev([]) = []
-rev(x#xs) = rev(xs) @ [x]
-
-length([]) = 0
-length(x#xs) = Suc(length(xs))
-
-xs!0 = hd xs
-xs!(Suc n) = (tl xs)!n
-\end{ttbox}
-\caption{Simple list processing functions}
-\label{fig:HOL:list-simps}
-\end{figure}
-
-\begin{figure}
-\begin{ttbox}\makeatother
-map f [] = []
-map f (x#xs) = f x # map f xs
-
-filter P [] = []
-filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
-
-foldl f a [] = a
-foldl f a (x#xs) = foldl f (f a x) xs
-
-take n [] = []
-take n (x#xs) = (case n of 0 => [] | 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)<f(y)$.
- Typically, $f$ takes the recursive function's arguments (as a tuple) and
- returns a result expressed in terms of the function \texttt{size}. It is
- called a \textbf{measure function}. Recall that \texttt{size} is overloaded
- and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
-
-\item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of
- \texttt{measure}. It specifies a relation such that $x\prec y$ if and only
- if $f(x)$
- is less than $f(y)$ according to~$R$, which must itself be a well-founded
- relation.
-
-\item $R@1\texttt{<*lex*>}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:
--- 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)
--- /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<n ==> m mod n = m
+\tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
+
+\tdx{div_less} m<n ==> m div n = 0
+\tdx{div_geq} [| 0<n; ~m<n |] ==> 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<n --> 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<x+y} to \texttt{z<y}, for
+instance. The simplifier also collects like terms, replacing \texttt{x+y+x*3}
+by \texttt{4*x+y}.
+
+Sometimes numerals are not wanted, because for example \texttt{n+3} does not
+match a pattern of the form \texttt{Suc $k$}. You can re-arrange the form of
+an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as
+\texttt{n+3 = Suc (Suc (Suc n))}. As an alternative, you can disable the
+fancier simplifications by using a basic simpset such as \texttt{HOL_ss}
+rather than the default one, \texttt{simpset()}.
+
+Reasoning about arithmetic inequalities can be tedious. Fortunately, HOL
+provides a decision procedure for \emph{linear arithmetic}: formulae involving
+addition and subtraction. The simplifier invokes a weak version of this
+decision procedure automatically. If this is not sufficent, you can invoke the
+full procedure \ttindex{Lin_Arith.tac} explicitly. It copes with arbitrary
+formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
+ min}, {\tt max} and numerical constants. Other subterms are treated as
+atomic, while subformulae not involving numerical types are ignored. Quantified
+subformulae are ignored unless they are positive universal or negative
+existential. The running time is exponential in the number of
+occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
+distinctions.
+If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
+{\tt k dvd} are also supported. The former two are eliminated
+by case distinctions, again blowing up the running time.
+If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take
+super-exponential time and space.
+
+If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in
+the library. The theories \texttt{Nat} and \texttt{NatArith} contain
+theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
+Theory \texttt{Divides} contains theorems about \texttt{div} and
+\texttt{mod}. Use Proof General's \emph{find} button (or other search
+facilities) to locate them.
+
+\index{nat@{\textit{nat}} type|)}
+
+
+\begin{figure}
+\index{#@{\tt[]} symbol}
+\index{#@{\tt\#} symbol}
+\index{"@@{\tt\at} symbol}
+\index{*"! symbol}
+\begin{constants}
+ \it symbol & \it meta-type & \it priority & \it description \\
+ \tt[] & $\alpha\,list$ & & empty list\\
+ \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
+ list constructor \\
+ \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
+ \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
+ \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
+ \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
+ \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
+ \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
+ \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
+ & & apply to all\\
+ \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
+ & & filter functional\\
+ \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
+ \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
+ \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
+ & iteration \\
+ \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
+ \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
+ \cdx{length} & $\alpha\,list \To nat$ & & length \\
+ \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
+ \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
+ take/drop a prefix \\
+ \cdx{takeWhile},\\
+ \cdx{dropWhile} &
+ $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
+ take/drop a prefix
+\end{constants}
+\subcaption{Constants and infixes}
+
+\begin{center} \tt\frenchspacing
+\begin{tabular}{rrr}
+ \it external & \it internal & \it description \\{}
+ [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
+ \rm finite list \\{}
+ [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
+ \rm list comprehension
+\end{tabular}
+\end{center}
+\subcaption{Translations}
+\caption{The theory \thydx{List}} \label{hol-list}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}\makeatother
+null [] = True
+null (x#xs) = False
+
+hd (x#xs) = x
+
+tl (x#xs) = xs
+tl [] = []
+
+[] @ ys = ys
+(x#xs) @ ys = x # xs @ ys
+
+set [] = \ttlbrace\ttrbrace
+set (x#xs) = insert x (set xs)
+
+x mem [] = False
+x mem (y#ys) = (if y=x then True else x mem ys)
+
+concat([]) = []
+concat(x#xs) = x @ concat(xs)
+
+rev([]) = []
+rev(x#xs) = rev(xs) @ [x]
+
+length([]) = 0
+length(x#xs) = Suc(length(xs))
+
+xs!0 = hd xs
+xs!(Suc n) = (tl xs)!n
+\end{ttbox}
+\caption{Simple list processing functions}
+\label{fig:HOL:list-simps}
+\end{figure}
+
+\begin{figure}
+\begin{ttbox}\makeatother
+map f [] = []
+map f (x#xs) = f x # map f xs
+
+filter P [] = []
+filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
+
+foldl f a [] = a
+foldl f a (x#xs) = foldl f (f a x) xs
+
+take n [] = []
+take n (x#xs) = (case n of 0 => [] | 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)<f(y)$.
+ Typically, $f$ takes the recursive function's arguments (as a tuple) and
+ returns a result expressed in terms of the function \texttt{size}. It is
+ called a \textbf{measure function}. Recall that \texttt{size} is overloaded
+ and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
+
+\item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of
+ \texttt{measure}. It specifies a relation such that $x\prec y$ if and only
+ if $f(x)$
+ is less than $f(y)$ according to~$R$, which must itself be a well-founded
+ relation.
+
+\item $R@1\texttt{<*lex*>}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:
--- /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"
--- /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}
--- 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}
--- 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