1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/HOL/HOL-eg.txt Tue May 04 18:03:56 1999 +0200
1.3 @@ -0,0 +1,151 @@
1.4 +(**** HOL examples -- process using Doc/tout HOL-eg.txt ****)
1.5 +
1.6 +Pretty.setmargin 72; (*existing macros just allow this margin*)
1.7 +print_depth 0;
1.8 +
1.9 +
1.10 +(*** Conjunction rules ***)
1.11 +
1.12 +val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q";
1.13 +by (resolve_tac [and_def RS ssubst] 1);
1.14 +by (resolve_tac [allI] 1);
1.15 +by (resolve_tac [impI] 1);
1.16 +by (eresolve_tac [mp RS mp] 1);
1.17 +by (REPEAT (resolve_tac prems 1));
1.18 +val conjI = result();
1.19 +
1.20 +val prems = goal HOL_Rule.thy "[| P & Q |] ==> P";
1.21 +prths (prems RL [and_def RS subst]);
1.22 +prths (prems RL [and_def RS subst] RL [spec] RL [mp]);
1.23 +by (resolve_tac it 1);
1.24 +by (REPEAT (ares_tac [impI] 1));
1.25 +val conjunct1 = result();
1.26 +
1.27 +
1.28 +(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
1.29 +
1.30 +goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1.31 +by (resolve_tac [notI] 1);
1.32 +by (eresolve_tac [rangeE] 1);
1.33 +by (eresolve_tac [equalityCE] 1);
1.34 +by (dresolve_tac [CollectD] 1);
1.35 +by (contr_tac 1);
1.36 +by (swap_res_tac [CollectI] 1);
1.37 +by (assume_tac 1);
1.38 +
1.39 +choplev 0;
1.40 +by (best_tac (set_cs addSEs [equalityCE]) 1);
1.41 +
1.42 +
1.43 +goal Set.thy "! f:: 'a=>'a set. ! x. ~ f(x) = ?S(f)";
1.44 +by (REPEAT (resolve_tac [allI,notI] 1));
1.45 +by (eresolve_tac [equalityCE] 1);
1.46 +by (dresolve_tac [CollectD] 1);
1.47 +by (contr_tac 1);
1.48 +by (swap_res_tac [CollectI] 1);
1.49 +by (assume_tac 1);
1.50 +
1.51 +choplev 0;
1.52 +by (best_tac (set_cs addSEs [equalityCE]) 1);
1.53 +
1.54 +
1.55 +goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? a. f(a) = S)";
1.56 +by (best_tac (set_cs addSEs [equalityCE]) 1);
1.57 +
1.58 +
1.59 +
1.60 +
1.61 +> val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q";
1.62 +Level 0
1.63 +P & Q
1.64 + 1. P & Q
1.65 +> by (resolve_tac [and_def RS ssubst] 1);
1.66 +Level 1
1.67 +P & Q
1.68 + 1. ! R. (P --> Q --> R) --> R
1.69 +> by (resolve_tac [allI] 1);
1.70 +Level 2
1.71 +P & Q
1.72 + 1. !!R. (P --> Q --> R) --> R
1.73 +> by (resolve_tac [impI] 1);
1.74 +Level 3
1.75 +P & Q
1.76 + 1. !!R. P --> Q --> R ==> R
1.77 +> by (eresolve_tac [mp RS mp] 1);
1.78 +Level 4
1.79 +P & Q
1.80 + 1. !!R. P
1.81 + 2. !!R. Q
1.82 +> by (REPEAT (resolve_tac prems 1));
1.83 +Level 5
1.84 +P & Q
1.85 +No subgoals!
1.86 +
1.87 +
1.88 +
1.89 +> val prems = goal HOL_Rule.thy "[| P & Q |] ==> P";
1.90 +Level 0
1.91 +P
1.92 + 1. P
1.93 +> prths (prems RL [and_def RS subst]);
1.94 +! R. (P --> Q --> R) --> R [P & Q]
1.95 +P & Q [P & Q]
1.96 +
1.97 +> prths (prems RL [and_def RS subst] RL [spec] RL [mp]);
1.98 +P --> Q --> ?Q ==> ?Q [P & Q]
1.99 +
1.100 +> by (resolve_tac it 1);
1.101 +Level 1
1.102 +P
1.103 + 1. P --> Q --> P
1.104 +> by (REPEAT (ares_tac [impI] 1));
1.105 +Level 2
1.106 +P
1.107 +No subgoals!
1.108 +
1.109 +
1.110 +
1.111 +
1.112 +> goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1.113 +Level 0
1.114 +~?S : range(f)
1.115 + 1. ~?S : range(f)
1.116 +> by (resolve_tac [notI] 1);
1.117 +Level 1
1.118 +~?S : range(f)
1.119 + 1. ?S : range(f) ==> False
1.120 +> by (eresolve_tac [rangeE] 1);
1.121 +Level 2
1.122 +~?S : range(f)
1.123 + 1. !!x. ?S = f(x) ==> False
1.124 +> by (eresolve_tac [equalityCE] 1);
1.125 +Level 3
1.126 +~?S : range(f)
1.127 + 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False
1.128 + 2. !!x. [| ~?c3(x) : ?S; ~?c3(x) : f(x) |] ==> False
1.129 +> by (dresolve_tac [CollectD] 1);
1.130 +Level 4
1.131 +~{x. ?P7(x)} : range(f)
1.132 + 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False
1.133 + 2. !!x. [| ~?c3(x) : {x. ?P7(x)}; ~?c3(x) : f(x) |] ==> False
1.134 +> by (contr_tac 1);
1.135 +Level 5
1.136 +~{x. ~x : f(x)} : range(f)
1.137 + 1. !!x. [| ~x : {x. ~x : f(x)}; ~x : f(x) |] ==> False
1.138 +> by (swap_res_tac [CollectI] 1);
1.139 +Level 6
1.140 +~{x. ~x : f(x)} : range(f)
1.141 + 1. !!x. [| ~x : f(x); ~False |] ==> ~x : f(x)
1.142 +> by (assume_tac 1);
1.143 +Level 7
1.144 +~{x. ~x : f(x)} : range(f)
1.145 +No subgoals!
1.146 +
1.147 +> choplev 0;
1.148 +Level 0
1.149 +~?S : range(f)
1.150 + 1. ~?S : range(f)
1.151 +> by (best_tac (set_cs addSEs [equalityCE]) 1);
1.152 +Level 1
1.153 +~{x. ~x : f(x)} : range(f)
1.154 +No subgoals!
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/HOL/HOL-rules.txt Tue May 04 18:03:56 1999 +0200
2.3 @@ -0,0 +1,403 @@
2.4 +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
2.5 +----------------------------------------------------------------
2.6 +ruleshell.ML
2.7 +
2.8 +\idx{refl} t = t::'a
2.9 +\idx{subst} [| s = t; P(s) |] ==> P(t::'a)
2.10 +\idx{abs},!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x)))
2.11 +\idx{disch} (P ==> Q) ==> P-->Q
2.12 +\idx{mp} [| P-->Q; P |] ==> Q
2.13 +
2.14 +\idx{True_def} True = ((%x.x)=(%x.x))
2.15 +\idx{All_def} All = (%P. P = (%x.True))
2.16 +\idx{Ex_def} Ex = (%P. P(Eps(P)))
2.17 +\idx{False_def} False = (!P.P)
2.18 +\idx{not_def} not = (%P. P-->False)
2.19 +\idx{and_def} op & = (%P Q. !R. (P-->Q-->R) --> R)
2.20 +\idx{or_def} op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)
2.21 +\idx{Ex1_def} Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x))
2.22 +
2.23 +\idx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
2.24 +\idx{True_or_False} (P=True) | (P=False)
2.25 +\idx{select} P(x::'a) --> P(Eps(P))
2.26 +
2.27 +\idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y)
2.28 +\idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x)))
2.29 +\idx{Cond_def} Cond = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))
2.30 +
2.31 +----------------------------------------------------------------
2.32 +lemmas.ML
2.33 +
2.34 +\idx{sym} s=t ==> t=s
2.35 +\idx{trans} [| r=s; s=t |] ==> r=t
2.36 +\idx{box_equals}
2.37 + [| a=b; a=c; b=d |] ==> c=d
2.38 +\idx{ap_term} s=t ==> f(s)=f(t)
2.39 +\idx{ap_thm} s::'a=>'b = t ==> s(x)=t(x)
2.40 +\idx{cong}
2.41 + [| f = g; x::'a = y |] ==> f(x) = g(y)
2.42 +\idx{iffI}
2.43 + [| P ==> Q; Q ==> P |] ==> P=Q
2.44 +\idx{iffD1} [| P=Q; Q |] ==> P
2.45 +\idx{iffE}
2.46 + [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
2.47 +\idx{eqTrueI} P ==> P=True
2.48 +\idx{eqTrueE} P=True ==> P
2.49 +\idx{allI} (!!x::'a. P(x)) ==> !x. P(x)
2.50 +\idx{spec} !x::'a.P(x) ==> P(x)
2.51 +\idx{allE} [| !x.P(x); P(x) ==> R |] ==> R
2.52 +\idx{all_dupE}
2.53 + [| ! x.P(x); [| P(x); ! x.P(x) |] ==> R
2.54 + |] ==> R
2.55 +\idx{FalseE} False ==> P
2.56 +\idx{False_neq_True} False=True ==> P
2.57 +\idx{notI} (P ==> False) ==> ~P
2.58 +\idx{notE} [| ~P; P |] ==> R
2.59 +\idx{impE} [| P-->Q; P; Q ==> R |] ==> R
2.60 +\idx{rev_mp} [| P; P --> Q |] ==> Q
2.61 +\idx{contrapos} [| ~Q; P==>Q |] ==> ~P
2.62 +\idx{exI} P(x) ==> ? x::'a.P(x)
2.63 +\idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
2.64 +
2.65 +\idx{conjI} [| P; Q |] ==> P&Q
2.66 +\idx{conjunct1} [| P & Q |] ==> P
2.67 +\idx{conjunct2} [| P & Q |] ==> Q
2.68 +\idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
2.69 +\idx{disjI1} P ==> P|Q
2.70 +\idx{disjI2} Q ==> P|Q
2.71 +\idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
2.72 +\idx{ccontr} (~P ==> False) ==> P
2.73 +\idx{classical} (~P ==> P) ==> P
2.74 +\idx{notnotD} ~~P ==> P
2.75 +\idx{ex1I}
2.76 + [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
2.77 +\idx{ex1E}
2.78 + [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R
2.79 +\idx{select_equality}
2.80 + [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
2.81 +\idx{disjCI} (~Q ==> P) ==> P|Q
2.82 +\idx{excluded_middle} ~P | P
2.83 +\idx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R
2.84 +\idx{iffCE}
2.85 + [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
2.86 +\idx{exCI} (! x. ~P(x) ==> P(a)) ==> ? x.P(x)
2.87 +\idx{swap} ~P ==> (~Q ==> P) ==> Q
2.88 +
2.89 +----------------------------------------------------------------
2.90 +simpdata.ML
2.91 +
2.92 +\idx{if_True} Cond(True,x,y) = x
2.93 +\idx{if_False} Cond(False,x,y) = y
2.94 +\idx{if_P} P ==> Cond(P,x,y) = x
2.95 +\idx{if_not_P} ~P ==> Cond(P,x,y) = y
2.96 +\idx{expand_if}
2.97 + P(Cond(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
2.98 +
2.99 +----------------------------------------------------------------
2.100 +\idx{set.ML}
2.101 +
2.102 +\idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
2.103 +\idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
2.104 +\idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
2.105 +
2.106 +\idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
2.107 +\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
2.108 +\idx{subset_def} A <= B == ! x:A. x:B
2.109 +\idx{Un_def} A Un B == \{x.x:A | x:B\}
2.110 +\idx{Int_def} A Int B == \{x.x:A & x:B\}
2.111 +\idx{Compl_def} Compl(A) == \{x. ~x:A\}
2.112 +\idx{Inter_def} Inter(S) == \{x. ! A:S. x:A\}
2.113 +\idx{Union_def} Union(S) == \{x. ? A:S. x:A\}
2.114 +\idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
2.115 +\idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
2.116 +\idx{mono_def} mono(f) == (!A B. A <= B --> f(A) <= f(B))
2.117 +\idx{image_def} f``A == \{y. ? x:A. y=f(x)\}
2.118 +\idx{singleton_def} \{a\} == \{x.x=a\}
2.119 +\idx{range_def} range(f) == \{y. ? x. y=f(x)\}
2.120 +\idx{One_One_def} One_One(f) == ! x y. f(x)=f(y) --> x=y
2.121 +\idx{One_One_on_def} One_One_on(f,A) == !x y. x:A --> y:A --> f(x)=f(y) --> x=y
2.122 +\idx{Onto_def} Onto(f) == ! y. ? x. y=f(x)
2.123 +
2.124 +
2.125 +\idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
2.126 +
2.127 +\idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
2.128 +\idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
2.129 +\idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
2.130 +
2.131 +\idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
2.132 +\idx{bexCI} [| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
2.133 +\idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
2.134 +
2.135 +\idx{ball_cong}
2.136 + [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
2.137 + (! x:A. P(x)) = (! x:A'. P'(x))
2.138 +
2.139 +\idx{bex_cong}
2.140 + [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
2.141 + (? x:A. P(x)) = (? x:A'. P'(x))
2.142 +
2.143 +\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
2.144 +\idx{subsetD} [| A <= B; c:A |] ==> c:B
2.145 +\idx{subsetCE} [| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P
2.146 +
2.147 +\idx{subset_refl} A <= A
2.148 +\idx{subset_antisym} [| A <= B; B <= A |] ==> A = B
2.149 +\idx{subset_trans} [| A<=B; B<=C |] ==> A<=C
2.150 +
2.151 +\idx{equalityD1} A = B ==> A<=B
2.152 +\idx{equalityD2} A = B ==> B<=A
2.153 +\idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
2.154 +
2.155 +\idx{singletonI} a : \{a\}
2.156 +\idx{singletonD} b : \{a\} ==> b=a
2.157 +
2.158 +\idx{imageI} [| x:A |] ==> f(x) : f``A
2.159 +\idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
2.160 +
2.161 +\idx{rangeI} f(x) : range(f)
2.162 +\idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
2.163 +
2.164 +\idx{UnionI} [| X:C; A:X |] ==> A : Union(C)
2.165 +\idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
2.166 +
2.167 +\idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
2.168 +\idx{InterD} [| A : Inter(C); X:C |] ==> A:X
2.169 +\idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
2.170 +
2.171 +\idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
2.172 +\idx{UN_E} [| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R
2.173 +
2.174 +\idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
2.175 +\idx{INT_D} [| b : (INT x:A. B(x)); a:A |] ==> b: B(a)
2.176 +\idx{INT_E} [| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
2.177 +
2.178 +\idx{UnI1} c:A ==> c : A Un B
2.179 +\idx{UnI2} c:B ==> c : A Un B
2.180 +\idx{UnCI} (~c:B ==> c:A) ==> c : A Un B
2.181 +\idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
2.182 +
2.183 +\idx{IntI} [| c:A; c:B |] ==> c : A Int B
2.184 +\idx{IntD1} c : A Int B ==> c:A
2.185 +\idx{IntD2} c : A Int B ==> c:B
2.186 +\idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
2.187 +
2.188 +\idx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
2.189 +\idx{ComplD} [| c : Compl(A) |] ==> ~c:A
2.190 +
2.191 +\idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
2.192 +\idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
2.193 +
2.194 +
2.195 +----------------------------------------------------------------
2.196 +\idx{fun.ML}
2.197 +
2.198 +\idx{One_OneI} [| !! x y. f(x) = f(y) ==> x=y |] ==> One_One(f)
2.199 +\idx{One_One_inverseI} (!!x. g(f(x)) = x) ==> One_One(f)
2.200 +\idx{One_OneD} [| One_One(f); f(x) = f(y) |] ==> x=y
2.201 +
2.202 +\idx{Inv_f_f} One_One(f) ==> Inv(f,f(x)) = x
2.203 +\idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
2.204 +
2.205 +\idx{Inv_injective}
2.206 + [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
2.207 +
2.208 +\idx{One_One_onI}
2.209 + (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> One_One_on(f,A)
2.210 +
2.211 +\idx{One_One_on_inverseI}
2.212 + (!!x. x:A ==> g(f(x)) = x) ==> One_One_on(f,A)
2.213 +
2.214 +\idx{One_One_onD}
2.215 + [| One_One_on(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
2.216 +
2.217 +\idx{One_One_on_contraD}
2.218 + [| One_One_on(f,A); ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)
2.219 +
2.220 +
2.221 +----------------------------------------------------------------
2.222 +\idx{subset.ML}
2.223 +
2.224 +\idx{Union_upper} B:A ==> B <= Union(A)
2.225 +\idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
2.226 +
2.227 +\idx{Inter_lower} B:A ==> Inter(A) <= B
2.228 +\idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
2.229 +
2.230 +\idx{Un_upper1} A <= A Un B
2.231 +\idx{Un_upper2} B <= A Un B
2.232 +\idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
2.233 +
2.234 +\idx{Int_lower1} A Int B <= A
2.235 +\idx{Int_lower2} A Int B <= B
2.236 +\idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
2.237 +
2.238 +
2.239 +----------------------------------------------------------------
2.240 +\idx{equalities.ML}
2.241 +
2.242 +\idx{Int_absorb} A Int A = A
2.243 +\idx{Int_commute} A Int B = B Int A
2.244 +\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)
2.245 +\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
2.246 +
2.247 +\idx{Un_absorb} A Un A = A
2.248 +\idx{Un_commute} A Un B = B Un A
2.249 +\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)
2.250 +\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
2.251 +
2.252 +\idx{Compl_disjoint} A Int Compl(A) = \{x.False\}
2.253 +\idx{Compl_partition A Un Compl(A) = \{x.True\}
2.254 +\idx{double_complement} Compl(Compl(A)) = A
2.255 +
2.256 +
2.257 +\idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
2.258 +\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
2.259 +
2.260 +\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
2.261 +\idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C)
2.262 +\idx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
2.263 +
2.264 +\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
2.265 +\idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C)
2.266 +\idx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
2.267 +
2.268 +
2.269 +----------------------------------------------------------------
2.270 +prod.ML
2.271 +
2.272 + mixfix = [ Delimfix((1<_,/_>), ['a,'b] => ('a,'b)prod, Pair),
2.273 + TInfixl(*, prod, 20) ],
2.274 +thy = extend_theory Set.thy Prod
2.275 + [([prod],([[term],[term]],term))],
2.276 + ([fst], 'a * 'b => 'a),
2.277 + ([snd], 'a * 'b => 'b),
2.278 + ([split], ['a * 'b, ['a,'b]=>'c] => 'c)],
2.279 +\idx{fst_def} fst(p) == @a. ? b. p = <a,b>),
2.280 +\idx{snd_def} snd(p) == @b. ? a. p = <a,b>),
2.281 +\idx{split_def} split(p,c) == c(fst(p),snd(p)))
2.282 +
2.283 +\idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
2.284 +
2.285 +\idx{fst_conv} fst(<a,b>) = a
2.286 +\idx{snd_conv} snd(<a,b>) = b
2.287 +\idx{split_conv} split(<a,b>, c) = c(a,b)
2.288 +
2.289 +\idx{surjective_pairing} p = <fst(p),snd(p)>
2.290 +
2.291 +----------------------------------------------------------------
2.292 +sum.ML
2.293 +
2.294 + mixfix = [TInfixl(+, sum, 10)],
2.295 +thy = extend_theory Prod.thy sum
2.296 + [([sum], ([[term],[term]],term))],
2.297 + [Inl], 'a => 'a+'b),
2.298 + [Inr], 'b => 'a+'b),
2.299 + [when], ['a+'b, 'a=>'c, 'b=>'c] =>'c)],
2.300 +\idx{when_def} when == (%p f g. @z. (!x. p=Inl(x) --> z=f(x))
2.301 + & (!y. p=Inr(y) --> z=g(y))))
2.302 +
2.303 +\idx{Inl_not_Inr} ~ (Inl(a) = Inr(b))
2.304 +
2.305 +\idx{One_One_Inl} One_One(Inl)
2.306 +
2.307 +\idx{One_One_Inr} One_One(Inr)
2.308 +
2.309 +\idx{when_Inl_conv} when(Inl(x), f, g) = f(x)
2.310 +
2.311 +\idx{when_Inr_conv} when(Inr(x), f, g) = g(x)
2.312 +
2.313 +\idx{sumE}
2.314 + [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y))
2.315 + |] ==> P(s)
2.316 +
2.317 +\idx{surjective_sum} when(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
2.318 +
2.319 +
2.320 +????????????????????????????????????????????????????????????????
2.321 +trancl?
2.322 +
2.323 +----------------------------------------------------------------
2.324 +nat.ML
2.325 +
2.326 + Sext\{mixfix=[Delimfix(0, nat, 0),
2.327 + Infixl(<,[nat,nat] => bool,50)],
2.328 +thy = extend_theory Trancl.thy Nat
2.329 +[nat], ([],term))
2.330 +[nat_case], [nat, 'a, nat=>'a] =>'a),
2.331 +[pred_nat],nat*nat) set),
2.332 +[nat_rec], [nat, 'a, [nat, 'a]=>'a] => 'a)
2.333 +
2.334 +\idx{nat_case_def} nat_case == (%n a f. @z. (n=0 --> z=a)
2.335 + & (!x. n=Suc(x) --> z=f(x)))),
2.336 +\idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\} ),
2.337 +\idx{less_def} m<n == <m,n>:trancl(pred_nat)),
2.338 +\idx{nat_rec_def}
2.339 + nat_rec(n,c,d) == wfrec(trancl(pred_nat),
2.340 + %rec l. nat_case(l, c, %m. d(m,rec(m))),
2.341 + n) )
2.342 +
2.343 +\idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
2.344 +
2.345 +
2.346 +\idx{Suc_not_Zero} ~ (Suc(m) = 0)
2.347 +\idx{One_One_Suc} One_One(Suc)
2.348 +\idx{n_not_Suc_n} ~(n=Suc(n))
2.349 +
2.350 +\idx{nat_case_0_conv} nat_case(0, a, f) = a
2.351 +
2.352 +\idx{nat_case_Suc_conv} nat_case(Suc(k), a, f) = f(k)
2.353 +
2.354 +\idx{pred_natI} <n, Suc(n)> : pred_nat
2.355 +\idx{pred_natE}
2.356 + [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R
2.357 + |] ==> R
2.358 +
2.359 +\idx{wf_pred_nat} wf(pred_nat)
2.360 +
2.361 +\idx{nat_rec_0_conv} nat_rec(0,c,h) = c
2.362 +
2.363 +\idx{nat_rec_Suc_conv} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
2.364 +
2.365 +
2.366 +(*** Basic properties of less than ***)
2.367 +\idx{less_trans} [| i<j; j<k |] ==> i<k
2.368 +\idx{lessI} n < Suc(n)
2.369 +\idx{zero_less_Suc} 0 < Suc(n)
2.370 +
2.371 +\idx{less_not_sym} n<m --> ~m<n
2.372 +\idx{less_not_refl} ~ (n<n)
2.373 +\idx{not_less0} ~ (n<0)
2.374 +
2.375 +\idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
2.376 +\idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
2.377 +
2.378 +\idx{less_linear} m<n | m=n | n<m
2.379 +
2.380 +
2.381 +----------------------------------------------------------------
2.382 +list.ML
2.383 +
2.384 + [([list], ([[term]],term))],
2.385 + ([Nil], 'a list),
2.386 + ([Cons], ['a, 'a list] => 'a list),
2.387 + ([list_rec], ['a list, 'b, ['a ,'a list, 'b]=>'b] => 'b),
2.388 + ([list_all], ('a => bool) => ('a list => bool)),
2.389 + ([map], ('a=>'b) => ('a list => 'b list))
2.390 +
2.391 +\idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r)) )
2.392 +
2.393 +\idx{list_induct}
2.394 + [| P(Nil);
2.395 + !!x xs. [| P(xs) |] ==> P(Cons(x,xs)) |] ==> P(l)
2.396 +
2.397 +\idx{Cons_not_Nil} ~ Cons(x,xs) = Nil
2.398 +\idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)
2.399 +
2.400 +\idx{list_rec_Nil_conv} list_rec(Nil,c,h) = c
2.401 +\idx{list_rec_Cons_conv} list_rec(Cons(a,l), c, h) =
2.402 + h(a, l, list_rec(l,c,h))
2.403 +
2.404 +\idx{map_Nil_conv} map(f,Nil) = Nil
2.405 +\idx{map_Cons_conv} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))
2.406 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/HOL/HOL.tex Tue May 04 18:03:56 1999 +0200
3.3 @@ -0,0 +1,2981 @@
3.4 +%% $Id$
3.5 +\chapter{Higher-Order Logic}
3.6 +\index{higher-order logic|(}
3.7 +\index{HOL system@{\sc hol} system}
3.8 +
3.9 +The theory~\thydx{HOL} implements higher-order logic. It is based on
3.10 +Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
3.11 +Church's original paper~\cite{church40}. Andrews's
3.12 +book~\cite{andrews86} is a full description of the original
3.13 +Church-style higher-order logic. Experience with the {\sc hol} system
3.14 +has demonstrated that higher-order logic is widely applicable in many
3.15 +areas of mathematics and computer science, not just hardware
3.16 +verification, {\sc hol}'s original \textit{raison d'\^etre\/}. It is
3.17 +weaker than {\ZF} set theory but for most applications this does not
3.18 +matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\
3.19 +to~{\ZF}.
3.20 +
3.21 +The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
3.22 +different syntax. Ancient releases of Isabelle included still another version
3.23 +of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This
3.24 +version no longer exists, but \thydx{ZF} supports a similar style of
3.25 +reasoning.} follows $\lambda$-calculus and functional programming. Function
3.26 +application is curried. To apply the function~$f$ of type
3.27 +$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply
3.28 +write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that
3.29 +$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered
3.30 +pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.
3.31 +
3.32 +\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
3.33 +identifies object-level types with meta-level types, taking advantage of
3.34 +Isabelle's built-in type-checker. It identifies object-level functions
3.35 +with meta-level functions, so it uses Isabelle's operations for abstraction
3.36 +and application.
3.37 +
3.38 +These identifications allow Isabelle to support \HOL\ particularly
3.39 +nicely, but they also mean that \HOL\ requires more sophistication
3.40 +from the user --- in particular, an understanding of Isabelle's type
3.41 +system. Beginners should work with \texttt{show_types} (or even
3.42 +\texttt{show_sorts}) set to \texttt{true}.
3.43 +% Gain experience by
3.44 +%working in first-order logic before attempting to use higher-order logic.
3.45 +%This chapter assumes familiarity with~{\FOL{}}.
3.46 +
3.47 +
3.48 +\begin{figure}
3.49 +\begin{constants}
3.50 + \it name &\it meta-type & \it description \\
3.51 + \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
3.52 + \cdx{Not} & $bool\To bool$ & negation ($\neg$) \\
3.53 + \cdx{True} & $bool$ & tautology ($\top$) \\
3.54 + \cdx{False} & $bool$ & absurdity ($\bot$) \\
3.55 + \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
3.56 + \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
3.57 +\end{constants}
3.58 +\subcaption{Constants}
3.59 +
3.60 +\begin{constants}
3.61 +\index{"@@{\tt\at} symbol}
3.62 +\index{*"! symbol}\index{*"? symbol}
3.63 +\index{*"?"! symbol}\index{*"E"X"! symbol}
3.64 + \it symbol &\it name &\it meta-type & \it description \\
3.65 + \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
3.66 + Hilbert description ($\varepsilon$) \\
3.67 + {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha\To bool)\To bool$ &
3.68 + universal quantifier ($\forall$) \\
3.69 + {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
3.70 + existential quantifier ($\exists$) \\
3.71 + {\tt?!} or \texttt{EX!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
3.72 + unique existence ($\exists!$)\\
3.73 + \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &
3.74 + least element
3.75 +\end{constants}
3.76 +\subcaption{Binders}
3.77 +
3.78 +\begin{constants}
3.79 +\index{*"= symbol}
3.80 +\index{&@{\tt\&} symbol}
3.81 +\index{*"| symbol}
3.82 +\index{*"-"-"> symbol}
3.83 + \it symbol & \it meta-type & \it priority & \it description \\
3.84 + \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
3.85 + Left 55 & composition ($\circ$) \\
3.86 + \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\
3.87 + \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
3.88 + \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
3.89 + less than or equals ($\leq$)\\
3.90 + \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
3.91 + \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
3.92 + \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
3.93 +\end{constants}
3.94 +\subcaption{Infixes}
3.95 +\caption{Syntax of \texttt{HOL}} \label{hol-constants}
3.96 +\end{figure}
3.97 +
3.98 +
3.99 +\begin{figure}
3.100 +\index{*let symbol}
3.101 +\index{*in symbol}
3.102 +\dquotes
3.103 +\[\begin{array}{rclcl}
3.104 + term & = & \hbox{expression of class~$term$} \\
3.105 + & | & "\at~" id " . " formula \\
3.106 + & | &
3.107 + \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
3.108 + & | &
3.109 + \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\
3.110 + & | & "LEAST"~ id " . " formula \\[2ex]
3.111 + formula & = & \hbox{expression of type~$bool$} \\
3.112 + & | & term " = " term \\
3.113 + & | & term " \ttilde= " term \\
3.114 + & | & term " < " term \\
3.115 + & | & term " <= " term \\
3.116 + & | & "\ttilde\ " formula \\
3.117 + & | & formula " \& " formula \\
3.118 + & | & formula " | " formula \\
3.119 + & | & formula " --> " formula \\
3.120 + & | & "!~~~" id~id^* " . " formula
3.121 + & | & "ALL~" id~id^* " . " formula \\
3.122 + & | & "?~~~" id~id^* " . " formula
3.123 + & | & "EX~~" id~id^* " . " formula \\
3.124 + & | & "?!~~" id~id^* " . " formula
3.125 + & | & "EX!~" id~id^* " . " formula
3.126 + \end{array}
3.127 +\]
3.128 +\caption{Full grammar for \HOL} \label{hol-grammar}
3.129 +\end{figure}
3.130 +
3.131 +
3.132 +\section{Syntax}
3.133 +
3.134 +Figure~\ref{hol-constants} lists the constants (including infixes and
3.135 +binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
3.136 +higher-order logic. Note that $a$\verb|~=|$b$ is translated to
3.137 +$\neg(a=b)$.
3.138 +
3.139 +\begin{warn}
3.140 + \HOL\ has no if-and-only-if connective; logical equivalence is expressed
3.141 + using equality. But equality has a high priority, as befitting a
3.142 + relation, while if-and-only-if typically has the lowest priority. Thus,
3.143 + $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
3.144 + When using $=$ to mean logical equivalence, enclose both operands in
3.145 + parentheses.
3.146 +\end{warn}
3.147 +
3.148 +\subsection{Types and classes}
3.149 +The universal type class of higher-order terms is called~\cldx{term}.
3.150 +By default, explicit type variables have class \cldx{term}. In
3.151 +particular the equality symbol and quantifiers are polymorphic over
3.152 +class \texttt{term}.
3.153 +
3.154 +The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
3.155 +formulae are terms. The built-in type~\tydx{fun}, which constructs
3.156 +function types, is overloaded with arity {\tt(term,\thinspace
3.157 + term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt
3.158 + term} if $\sigma$ and~$\tau$ do, allowing quantification over
3.159 +functions.
3.160 +
3.161 +\HOL\ offers various methods for introducing new types.
3.162 +See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
3.163 +
3.164 +Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
3.165 +signatures; the relations $<$ and $\leq$ are polymorphic over this
3.166 +class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
3.167 +the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
3.168 +\cldx{order} of \cldx{ord} which axiomatizes partially ordered types
3.169 +(w.r.t.\ $\le$).
3.170 +
3.171 +Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
3.172 +\cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
3.173 + symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In
3.174 +particular, {\tt-} is instantiated for set difference and subtraction
3.175 +on natural numbers.
3.176 +
3.177 +If you state a goal containing overloaded functions, you may need to include
3.178 +type constraints. Type inference may otherwise make the goal more
3.179 +polymorphic than you intended, with confusing results. For example, the
3.180 +variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type
3.181 +$\alpha::\{ord,plus\}$, although you may have expected them to have some
3.182 +numeric type, e.g. $nat$. Instead you should have stated the goal as
3.183 +$(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have
3.184 +type $nat$.
3.185 +
3.186 +\begin{warn}
3.187 + If resolution fails for no obvious reason, try setting
3.188 + \ttindex{show_types} to \texttt{true}, causing Isabelle to display
3.189 + types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as
3.190 + well, causing Isabelle to display type classes and sorts.
3.191 +
3.192 + \index{unification!incompleteness of}
3.193 + Where function types are involved, Isabelle's unification code does not
3.194 + guarantee to find instantiations for type variables automatically. Be
3.195 + prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
3.196 + possibly instantiating type variables. Setting
3.197 + \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
3.198 + omitted search paths during unification.\index{tracing!of unification}
3.199 +\end{warn}
3.200 +
3.201 +
3.202 +\subsection{Binders}
3.203 +
3.204 +Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for
3.205 +some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\
3.206 +denote something, a description is always meaningful, but we do not
3.207 +know its value unless $P$ defines it uniquely. We may write
3.208 +descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
3.209 +\hbox{\tt \at $x$.\ $P[x]$}.
3.210 +
3.211 +Existential quantification is defined by
3.212 +\[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
3.213 +The unique existence quantifier, $\exists!x. P$, is defined in terms
3.214 +of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
3.215 +quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates
3.216 +$\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there
3.217 +exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
3.218 +
3.219 +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
3.220 +Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
3.221 +uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
3.222 +existential quantifier must be followed by a space; thus {\tt?x} is an
3.223 +unknown, while \verb'? x. f x=y' is a quantification. Isabelle's usual
3.224 +notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
3.225 +available. Both notations are accepted for input. The {\ML} reference
3.226 +\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
3.227 +true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
3.228 +to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed.
3.229 +
3.230 +If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
3.231 +variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
3.232 +to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see
3.233 +Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
3.234 +choice operator, so \texttt{Least} is always meaningful, but may yield
3.235 +nothing useful in case there is not a unique least element satisfying
3.236 +$P$.\footnote{Class $ord$ does not require much of its instances, so
3.237 + $\le$ need not be a well-ordering, not even an order at all!}
3.238 +
3.239 +\medskip All these binders have priority 10.
3.240 +
3.241 +\begin{warn}
3.242 +The low priority of binders means that they need to be enclosed in
3.243 +parenthesis when they occur in the context of other operations. For example,
3.244 +instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.
3.245 +\end{warn}
3.246 +
3.247 +
3.248 +\subsection{The \sdx{let} and \sdx{case} constructions}
3.249 +Local abbreviations can be introduced by a \texttt{let} construct whose
3.250 +syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
3.251 +the constant~\cdx{Let}. It can be expanded by rewriting with its
3.252 +definition, \tdx{Let_def}.
3.253 +
3.254 +\HOL\ also defines the basic syntax
3.255 +\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
3.256 +as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}
3.257 +and \sdx{of} are reserved words. Initially, this is mere syntax and has no
3.258 +logical meaning. By declaring translations, you can cause instances of the
3.259 +\texttt{case} construct to denote applications of particular case operators.
3.260 +This is what happens automatically for each \texttt{datatype} definition
3.261 +(see~\S\ref{sec:HOL:datatype}).
3.262 +
3.263 +\begin{warn}
3.264 +Both \texttt{if} and \texttt{case} constructs have as low a priority as
3.265 +quantifiers, which requires additional enclosing parentheses in the context
3.266 +of most other operations. For example, instead of $f~x = {\tt if\dots
3.267 +then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots
3.268 +else\dots})$.
3.269 +\end{warn}
3.270 +
3.271 +\section{Rules of inference}
3.272 +
3.273 +\begin{figure}
3.274 +\begin{ttbox}\makeatother
3.275 +\tdx{refl} t = (t::'a)
3.276 +\tdx{subst} [| s = t; P s |] ==> P (t::'a)
3.277 +\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)
3.278 +\tdx{impI} (P ==> Q) ==> P-->Q
3.279 +\tdx{mp} [| P-->Q; P |] ==> Q
3.280 +\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
3.281 +\tdx{selectI} P(x::'a) ==> P(@x. P x)
3.282 +\tdx{True_or_False} (P=True) | (P=False)
3.283 +\end{ttbox}
3.284 +\caption{The \texttt{HOL} rules} \label{hol-rules}
3.285 +\end{figure}
3.286 +
3.287 +Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
3.288 +with their~{\ML} names. Some of the rules deserve additional
3.289 +comments:
3.290 +\begin{ttdescription}
3.291 +\item[\tdx{ext}] expresses extensionality of functions.
3.292 +\item[\tdx{iff}] asserts that logically equivalent formulae are
3.293 + equal.
3.294 +\item[\tdx{selectI}] gives the defining property of the Hilbert
3.295 + $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule
3.296 + \tdx{select_equality} (see below) is often easier to use.
3.297 +\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
3.298 + fact, the $\varepsilon$-operator already makes the logic classical, as
3.299 + shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
3.300 +\end{ttdescription}
3.301 +
3.302 +
3.303 +\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
3.304 +\begin{ttbox}\makeatother
3.305 +\tdx{True_def} True == ((\%x::bool. x)=(\%x. x))
3.306 +\tdx{All_def} All == (\%P. P = (\%x. True))
3.307 +\tdx{Ex_def} Ex == (\%P. P(@x. P x))
3.308 +\tdx{False_def} False == (!P. P)
3.309 +\tdx{not_def} not == (\%P. P-->False)
3.310 +\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
3.311 +\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
3.312 +\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))
3.313 +
3.314 +\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))
3.315 +\tdx{if_def} If P x y ==
3.316 + (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
3.317 +\tdx{Let_def} Let s f == f s
3.318 +\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
3.319 +\end{ttbox}
3.320 +\caption{The \texttt{HOL} definitions} \label{hol-defs}
3.321 +\end{figure}
3.322 +
3.323 +
3.324 +\HOL{} follows standard practice in higher-order logic: only a few
3.325 +connectives are taken as primitive, with the remainder defined obscurely
3.326 +(Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
3.327 +corresponding definitions \cite[page~270]{mgordon-hol} using
3.328 +object-equality~({\tt=}), which is possible because equality in
3.329 +higher-order logic may equate formulae and even functions over formulae.
3.330 +But theory~\HOL{}, like all other Isabelle theories, uses
3.331 +meta-equality~({\tt==}) for definitions.
3.332 +\begin{warn}
3.333 +The definitions above should never be expanded and are shown for completeness
3.334 +only. Instead users should reason in terms of the derived rules shown below
3.335 +or, better still, using high-level tactics
3.336 +(see~\S\ref{sec:HOL:generic-packages}).
3.337 +\end{warn}
3.338 +
3.339 +Some of the rules mention type variables; for example, \texttt{refl}
3.340 +mentions the type variable~{\tt'a}. This allows you to instantiate
3.341 +type variables explicitly by calling \texttt{res_inst_tac}.
3.342 +
3.343 +
3.344 +\begin{figure}
3.345 +\begin{ttbox}
3.346 +\tdx{sym} s=t ==> t=s
3.347 +\tdx{trans} [| r=s; s=t |] ==> r=t
3.348 +\tdx{ssubst} [| t=s; P s |] ==> P t
3.349 +\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
3.350 +\tdx{arg_cong} x = y ==> f x = f y
3.351 +\tdx{fun_cong} f = g ==> f x = g x
3.352 +\tdx{cong} [| f = g; x = y |] ==> f x = g y
3.353 +\tdx{not_sym} t ~= s ==> s ~= t
3.354 +\subcaption{Equality}
3.355 +
3.356 +\tdx{TrueI} True
3.357 +\tdx{FalseE} False ==> P
3.358 +
3.359 +\tdx{conjI} [| P; Q |] ==> P&Q
3.360 +\tdx{conjunct1} [| P&Q |] ==> P
3.361 +\tdx{conjunct2} [| P&Q |] ==> Q
3.362 +\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
3.363 +
3.364 +\tdx{disjI1} P ==> P|Q
3.365 +\tdx{disjI2} Q ==> P|Q
3.366 +\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
3.367 +
3.368 +\tdx{notI} (P ==> False) ==> ~ P
3.369 +\tdx{notE} [| ~ P; P |] ==> R
3.370 +\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
3.371 +\subcaption{Propositional logic}
3.372 +
3.373 +\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
3.374 +\tdx{iffD1} [| P=Q; P |] ==> Q
3.375 +\tdx{iffD2} [| P=Q; Q |] ==> P
3.376 +\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
3.377 +%
3.378 +%\tdx{eqTrueI} P ==> P=True
3.379 +%\tdx{eqTrueE} P=True ==> P
3.380 +\subcaption{Logical equivalence}
3.381 +
3.382 +\end{ttbox}
3.383 +\caption{Derived rules for \HOL} \label{hol-lemmas1}
3.384 +\end{figure}
3.385 +
3.386 +
3.387 +\begin{figure}
3.388 +\begin{ttbox}\makeatother
3.389 +\tdx{allI} (!!x. P x) ==> !x. P x
3.390 +\tdx{spec} !x. P x ==> P x
3.391 +\tdx{allE} [| !x. P x; P x ==> R |] ==> R
3.392 +\tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R
3.393 +
3.394 +\tdx{exI} P x ==> ? x. P x
3.395 +\tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q
3.396 +
3.397 +\tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x
3.398 +\tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R
3.399 + |] ==> R
3.400 +
3.401 +\tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a
3.402 +\subcaption{Quantifiers and descriptions}
3.403 +
3.404 +\tdx{ccontr} (~P ==> False) ==> P
3.405 +\tdx{classical} (~P ==> P) ==> P
3.406 +\tdx{excluded_middle} ~P | P
3.407 +
3.408 +\tdx{disjCI} (~Q ==> P) ==> P|Q
3.409 +\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x
3.410 +\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
3.411 +\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
3.412 +\tdx{notnotD} ~~P ==> P
3.413 +\tdx{swap} ~P ==> (~Q ==> P) ==> Q
3.414 +\subcaption{Classical logic}
3.415 +
3.416 +%\tdx{if_True} (if True then x else y) = x
3.417 +%\tdx{if_False} (if False then x else y) = y
3.418 +\tdx{if_P} P ==> (if P then x else y) = x
3.419 +\tdx{if_not_P} ~ P ==> (if P then x else y) = y
3.420 +\tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
3.421 +\subcaption{Conditionals}
3.422 +\end{ttbox}
3.423 +\caption{More derived rules} \label{hol-lemmas2}
3.424 +\end{figure}
3.425 +
3.426 +Some derived rules are shown in Figures~\ref{hol-lemmas1}
3.427 +and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
3.428 +for the logical connectives, as well as sequent-style elimination rules for
3.429 +conjunctions, implications, and universal quantifiers.
3.430 +
3.431 +Note the equality rules: \tdx{ssubst} performs substitution in
3.432 +backward proofs, while \tdx{box_equals} supports reasoning by
3.433 +simplifying both sides of an equation.
3.434 +
3.435 +The following simple tactics are occasionally useful:
3.436 +\begin{ttdescription}
3.437 +\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
3.438 + repeatedly to remove all outermost universal quantifiers and implications
3.439 + from subgoal $i$.
3.440 +\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction
3.441 + on $P$ for subgoal $i$: the latter is replaced by two identical subgoals
3.442 + with the added assumptions $P$ and $\neg P$, respectively.
3.443 +\end{ttdescription}
3.444 +
3.445 +
3.446 +\begin{figure}
3.447 +\begin{center}
3.448 +\begin{tabular}{rrr}
3.449 + \it name &\it meta-type & \it description \\
3.450 +\index{{}@\verb'{}' symbol}
3.451 + \verb|{}| & $\alpha\,set$ & the empty set \\
3.452 + \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
3.453 + & insertion of element \\
3.454 + \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
3.455 + & comprehension \\
3.456 + \cdx{Compl} & $\alpha\,set\To\alpha\,set$
3.457 + & complement \\
3.458 + \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
3.459 + & intersection over a set\\
3.460 + \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
3.461 + & union over a set\\
3.462 + \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
3.463 + &set of sets intersection \\
3.464 + \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
3.465 + &set of sets union \\
3.466 + \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
3.467 + & powerset \\[1ex]
3.468 + \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
3.469 + & range of a function \\[1ex]
3.470 + \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
3.471 + & bounded quantifiers
3.472 +\end{tabular}
3.473 +\end{center}
3.474 +\subcaption{Constants}
3.475 +
3.476 +\begin{center}
3.477 +\begin{tabular}{llrrr}
3.478 + \it symbol &\it name &\it meta-type & \it priority & \it description \\
3.479 + \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
3.480 + intersection over a type\\
3.481 + \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
3.482 + union over a type
3.483 +\end{tabular}
3.484 +\end{center}
3.485 +\subcaption{Binders}
3.486 +
3.487 +\begin{center}
3.488 +\index{*"`"` symbol}
3.489 +\index{*": symbol}
3.490 +\index{*"<"= symbol}
3.491 +\begin{tabular}{rrrr}
3.492 + \it symbol & \it meta-type & \it priority & \it description \\
3.493 + \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$
3.494 + & Left 90 & image \\
3.495 + \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
3.496 + & Left 70 & intersection ($\int$) \\
3.497 + \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
3.498 + & Left 65 & union ($\un$) \\
3.499 + \tt: & $[\alpha ,\alpha\,set]\To bool$
3.500 + & Left 50 & membership ($\in$) \\
3.501 + \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
3.502 + & Left 50 & subset ($\subseteq$)
3.503 +\end{tabular}
3.504 +\end{center}
3.505 +\subcaption{Infixes}
3.506 +\caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
3.507 +\end{figure}
3.508 +
3.509 +
3.510 +\begin{figure}
3.511 +\begin{center} \tt\frenchspacing
3.512 +\index{*"! symbol}
3.513 +\begin{tabular}{rrr}
3.514 + \it external & \it internal & \it description \\
3.515 + $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
3.516 + {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
3.517 + {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) &
3.518 + \rm comprehension \\
3.519 + \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ &
3.520 + \rm intersection \\
3.521 + \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &
3.522 + \rm union \\
3.523 + \tt ! $x$:$A$. $P[x]$ or \sdx{ALL} $x$:$A$. $P[x]$ &
3.524 + Ball $A$ $\lambda x. P[x]$ &
3.525 + \rm bounded $\forall$ \\
3.526 + \sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ &
3.527 + Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$
3.528 +\end{tabular}
3.529 +\end{center}
3.530 +\subcaption{Translations}
3.531 +
3.532 +\dquotes
3.533 +\[\begin{array}{rclcl}
3.534 + term & = & \hbox{other terms\ldots} \\
3.535 + & | & "{\ttlbrace}{\ttrbrace}" \\
3.536 + & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
3.537 + & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
3.538 + & | & term " `` " term \\
3.539 + & | & term " Int " term \\
3.540 + & | & term " Un " term \\
3.541 + & | & "INT~~" id ":" term " . " term \\
3.542 + & | & "UN~~~" id ":" term " . " term \\
3.543 + & | & "INT~~" id~id^* " . " term \\
3.544 + & | & "UN~~~" id~id^* " . " term \\[2ex]
3.545 + formula & = & \hbox{other formulae\ldots} \\
3.546 + & | & term " : " term \\
3.547 + & | & term " \ttilde: " term \\
3.548 + & | & term " <= " term \\
3.549 + & | & "!~" id ":" term " . " formula
3.550 + & | & "ALL " id ":" term " . " formula \\
3.551 + & | & "?~" id ":" term " . " formula
3.552 + & | & "EX~~" id ":" term " . " formula
3.553 + \end{array}
3.554 +\]
3.555 +\subcaption{Full Grammar}
3.556 +\caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
3.557 +\end{figure}
3.558 +
3.559 +
3.560 +\section{A formulation of set theory}
3.561 +Historically, higher-order logic gives a foundation for Russell and
3.562 +Whitehead's theory of classes. Let us use modern terminology and call them
3.563 +{\bf sets}, but note that these sets are distinct from those of {\ZF} set
3.564 +theory, and behave more like {\ZF} classes.
3.565 +\begin{itemize}
3.566 +\item
3.567 +Sets are given by predicates over some type~$\sigma$. Types serve to
3.568 +define universes for sets, but type-checking is still significant.
3.569 +\item
3.570 +There is a universal set (for each type). Thus, sets have complements, and
3.571 +may be defined by absolute comprehension.
3.572 +\item
3.573 +Although sets may contain other sets as elements, the containing set must
3.574 +have a more complex type.
3.575 +\end{itemize}
3.576 +Finite unions and intersections have the same behaviour in \HOL\ as they
3.577 +do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
3.578 +denoting the universal set for the given type.
3.579 +
3.580 +\subsection{Syntax of set theory}\index{*set type}
3.581 +\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
3.582 +essentially the same as $\alpha\To bool$. The new type is defined for
3.583 +clarity and to avoid complications involving function types in unification.
3.584 +The isomorphisms between the two types are declared explicitly. They are
3.585 +very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
3.586 +\hbox{\tt op :} maps in the other direction (ignoring argument order).
3.587 +
3.588 +Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
3.589 +translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
3.590 +constructs. Infix operators include union and intersection ($A\un B$
3.591 +and $A\int B$), the subset and membership relations, and the image
3.592 +operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
3.593 +$\neg(a\in b)$.
3.594 +
3.595 +The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
3.596 +the obvious manner using~\texttt{insert} and~$\{\}$:
3.597 +\begin{eqnarray*}
3.598 + \{a, b, c\} & \equiv &
3.599 + \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
3.600 +\end{eqnarray*}
3.601 +
3.602 +The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
3.603 +that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
3.604 +occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
3.605 +x. P[x])$. It defines sets by absolute comprehension, which is impossible
3.606 +in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
3.607 +
3.608 +The set theory defines two {\bf bounded quantifiers}:
3.609 +\begin{eqnarray*}
3.610 + \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
3.611 + \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
3.612 +\end{eqnarray*}
3.613 +The constants~\cdx{Ball} and~\cdx{Bex} are defined
3.614 +accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
3.615 +write\index{*"! symbol}\index{*"? symbol}
3.616 +\index{*ALL symbol}\index{*EX symbol}
3.617 +%
3.618 +\hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's
3.619 +usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
3.620 +for input. As with the primitive quantifiers, the {\ML} reference
3.621 +\ttindex{HOL_quantifiers} specifies which notation to use for output.
3.622 +
3.623 +Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
3.624 +$\bigcap@{x\in A}B[x]$, are written
3.625 +\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and
3.626 +\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.
3.627 +
3.628 +Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
3.629 +B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and
3.630 +\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous
3.631 +union and intersection operators when $A$ is the universal set.
3.632 +
3.633 +The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
3.634 +not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
3.635 +respectively.
3.636 +
3.637 +
3.638 +
3.639 +\begin{figure} \underscoreon
3.640 +\begin{ttbox}
3.641 +\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a
3.642 +\tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A
3.643 +
3.644 +\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace}
3.645 +\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B
3.646 +\tdx{Ball_def} Ball A P == ! x. x:A --> P x
3.647 +\tdx{Bex_def} Bex A P == ? x. x:A & P x
3.648 +\tdx{subset_def} A <= B == ! x:A. x:B
3.649 +\tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace}
3.650 +\tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace}
3.651 +\tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace}
3.652 +\tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace}
3.653 +\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
3.654 +\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
3.655 +\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B
3.656 +\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B
3.657 +\tdx{Inter_def} Inter S == (INT x:S. x)
3.658 +\tdx{Union_def} Union S == (UN x:S. x)
3.659 +\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}
3.660 +\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
3.661 +\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
3.662 +\end{ttbox}
3.663 +\caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
3.664 +\end{figure}
3.665 +
3.666 +
3.667 +\begin{figure} \underscoreon
3.668 +\begin{ttbox}
3.669 +\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}
3.670 +\tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a
3.671 +\tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W
3.672 +
3.673 +\tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
3.674 +\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
3.675 +\tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q
3.676 +
3.677 +\tdx{bexI} [| P x; x:A |] ==> ? x:A. P x
3.678 +\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x
3.679 +\tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q
3.680 +\subcaption{Comprehension and Bounded quantifiers}
3.681 +
3.682 +\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B
3.683 +\tdx{subsetD} [| A <= B; c:A |] ==> c:B
3.684 +\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
3.685 +
3.686 +\tdx{subset_refl} A <= A
3.687 +\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
3.688 +
3.689 +\tdx{equalityI} [| A <= B; B <= A |] ==> A = B
3.690 +\tdx{equalityD1} A = B ==> A<=B
3.691 +\tdx{equalityD2} A = B ==> B<=A
3.692 +\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
3.693 +
3.694 +\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
3.695 + [| ~ c:A; ~ c:B |] ==> P
3.696 + |] ==> P
3.697 +\subcaption{The subset and equality relations}
3.698 +\end{ttbox}
3.699 +\caption{Derived rules for set theory} \label{hol-set1}
3.700 +\end{figure}
3.701 +
3.702 +
3.703 +\begin{figure} \underscoreon
3.704 +\begin{ttbox}
3.705 +\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P
3.706 +
3.707 +\tdx{insertI1} a : insert a B
3.708 +\tdx{insertI2} a : B ==> a : insert b B
3.709 +\tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P
3.710 +
3.711 +\tdx{ComplI} [| c:A ==> False |] ==> c : Compl A
3.712 +\tdx{ComplD} [| c : Compl A |] ==> ~ c:A
3.713 +
3.714 +\tdx{UnI1} c:A ==> c : A Un B
3.715 +\tdx{UnI2} c:B ==> c : A Un B
3.716 +\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
3.717 +\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
3.718 +
3.719 +\tdx{IntI} [| c:A; c:B |] ==> c : A Int B
3.720 +\tdx{IntD1} c : A Int B ==> c:A
3.721 +\tdx{IntD2} c : A Int B ==> c:B
3.722 +\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
3.723 +
3.724 +\tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)
3.725 +\tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R
3.726 +
3.727 +\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
3.728 +\tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a
3.729 +\tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R
3.730 +
3.731 +\tdx{UnionI} [| X:C; A:X |] ==> A : Union C
3.732 +\tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R
3.733 +
3.734 +\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C
3.735 +\tdx{InterD} [| A : Inter C; X:C |] ==> A:X
3.736 +\tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R
3.737 +
3.738 +\tdx{PowI} A<=B ==> A: Pow B
3.739 +\tdx{PowD} A: Pow B ==> A<=B
3.740 +
3.741 +\tdx{imageI} [| x:A |] ==> f x : f``A
3.742 +\tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P
3.743 +
3.744 +\tdx{rangeI} f x : range f
3.745 +\tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P
3.746 +\end{ttbox}
3.747 +\caption{Further derived rules for set theory} \label{hol-set2}
3.748 +\end{figure}
3.749 +
3.750 +
3.751 +\subsection{Axioms and rules of set theory}
3.752 +Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
3.753 +axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
3.754 +that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of
3.755 +course, \hbox{\tt op :} also serves as the membership relation.
3.756 +
3.757 +All the other axioms are definitions. They include the empty set, bounded
3.758 +quantifiers, unions, intersections, complements and the subset relation.
3.759 +They also include straightforward constructions on functions: image~({\tt``})
3.760 +and \texttt{range}.
3.761 +
3.762 +%The predicate \cdx{inj_on} is used for simulating type definitions.
3.763 +%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
3.764 +%set~$A$, which specifies a subset of its domain type. In a type
3.765 +%definition, $f$ is the abstraction function and $A$ is the set of valid
3.766 +%representations; we should not expect $f$ to be injective outside of~$A$.
3.767 +
3.768 +%\begin{figure} \underscoreon
3.769 +%\begin{ttbox}
3.770 +%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x
3.771 +%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y
3.772 +%
3.773 +%\tdx{Inv_injective}
3.774 +% [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y
3.775 +%
3.776 +%
3.777 +%\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f
3.778 +%\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B
3.779 +%
3.780 +%\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f
3.781 +%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
3.782 +%\tdx{injD} [| inj f; f x = f y |] ==> x=y
3.783 +%
3.784 +%\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A
3.785 +%\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y
3.786 +%
3.787 +%\tdx{inj_on_inverseI}
3.788 +% (!!x. x:A ==> g(f x) = x) ==> inj_on f A
3.789 +%\tdx{inj_on_contraD}
3.790 +% [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y
3.791 +%\end{ttbox}
3.792 +%\caption{Derived rules involving functions} \label{hol-fun}
3.793 +%\end{figure}
3.794 +
3.795 +
3.796 +\begin{figure} \underscoreon
3.797 +\begin{ttbox}
3.798 +\tdx{Union_upper} B:A ==> B <= Union A
3.799 +\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C
3.800 +
3.801 +\tdx{Inter_lower} B:A ==> Inter A <= B
3.802 +\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A
3.803 +
3.804 +\tdx{Un_upper1} A <= A Un B
3.805 +\tdx{Un_upper2} B <= A Un B
3.806 +\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
3.807 +
3.808 +\tdx{Int_lower1} A Int B <= A
3.809 +\tdx{Int_lower2} A Int B <= B
3.810 +\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
3.811 +\end{ttbox}
3.812 +\caption{Derived rules involving subsets} \label{hol-subset}
3.813 +\end{figure}
3.814 +
3.815 +
3.816 +\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
3.817 +\begin{ttbox}
3.818 +\tdx{Int_absorb} A Int A = A
3.819 +\tdx{Int_commute} A Int B = B Int A
3.820 +\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
3.821 +\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
3.822 +
3.823 +\tdx{Un_absorb} A Un A = A
3.824 +\tdx{Un_commute} A Un B = B Un A
3.825 +\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
3.826 +\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
3.827 +
3.828 +\tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x. False{\ttrbrace}
3.829 +\tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x. True{\ttrbrace}
3.830 +\tdx{double_complement} Compl(Compl A) = A
3.831 +\tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B)
3.832 +\tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B)
3.833 +
3.834 +\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)
3.835 +\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)
3.836 +\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
3.837 +
3.838 +\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)
3.839 +\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)
3.840 +\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
3.841 +\end{ttbox}
3.842 +\caption{Set equalities} \label{hol-equalities}
3.843 +\end{figure}
3.844 +
3.845 +
3.846 +Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
3.847 +obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
3.848 +such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
3.849 +are designed for classical reasoning; the rules \tdx{subsetD},
3.850 +\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
3.851 +strictly necessary but yield more natural proofs. Similarly,
3.852 +\tdx{equalityCE} supports classical reasoning about extensionality,
3.853 +after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for
3.854 +proofs pertaining to set theory.
3.855 +
3.856 +Figure~\ref{hol-subset} presents lattice properties of the subset relation.
3.857 +Unions form least upper bounds; non-empty intersections form greatest lower
3.858 +bounds. Reasoning directly about subsets often yields clearer proofs than
3.859 +reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.
3.860 +
3.861 +Figure~\ref{hol-equalities} presents many common set equalities. They
3.862 +include commutative, associative and distributive laws involving unions,
3.863 +intersections and complements. For a complete listing see the file {\tt
3.864 +HOL/equalities.ML}.
3.865 +
3.866 +\begin{warn}
3.867 +\texttt{Blast_tac} proves many set-theoretic theorems automatically.
3.868 +Hence you seldom need to refer to the theorems above.
3.869 +\end{warn}
3.870 +
3.871 +\begin{figure}
3.872 +\begin{center}
3.873 +\begin{tabular}{rrr}
3.874 + \it name &\it meta-type & \it description \\
3.875 + \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
3.876 + & injective/surjective \\
3.877 + \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$
3.878 + & injective over subset\\
3.879 + \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
3.880 +\end{tabular}
3.881 +\end{center}
3.882 +
3.883 +\underscoreon
3.884 +\begin{ttbox}
3.885 +\tdx{inj_def} inj f == ! x y. f x=f y --> x=y
3.886 +\tdx{surj_def} surj f == ! y. ? x. y=f x
3.887 +\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y
3.888 +\tdx{inv_def} inv f == (\%y. @x. f(x)=y)
3.889 +\end{ttbox}
3.890 +\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
3.891 +\end{figure}
3.892 +
3.893 +\subsection{Properties of functions}\nopagebreak
3.894 +Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
3.895 +Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse
3.896 +of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
3.897 +rules. Reasoning about function composition (the operator~\sdx{o}) and the
3.898 +predicate~\cdx{surj} is done simply by expanding the definitions.
3.899 +
3.900 +There is also a large collection of monotonicity theorems for constructions
3.901 +on sets in the file \texttt{HOL/mono.ML}.
3.902 +
3.903 +\section{Generic packages}
3.904 +\label{sec:HOL:generic-packages}
3.905 +
3.906 +\HOL\ instantiates most of Isabelle's generic packages, making available the
3.907 +simplifier and the classical reasoner.
3.908 +
3.909 +\subsection{Simplification and substitution}
3.910 +
3.911 +Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
3.912 +(\texttt{simpset()}), which works for most purposes. A quite minimal
3.913 +simplification set for higher-order logic is~\ttindexbold{HOL_ss};
3.914 +even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which
3.915 +also expresses logical equivalence, may be used for rewriting. See
3.916 +the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
3.917 +simplification rules.
3.918 +
3.919 +See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
3.920 +{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
3.921 +and simplification.
3.922 +
3.923 +\begin{warn}\index{simplification!of conjunctions}%
3.924 + Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
3.925 + left part of a conjunction helps in simplifying the right part. This effect
3.926 + is not available by default: it can be slow. It can be obtained by
3.927 + including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
3.928 +\end{warn}
3.929 +
3.930 +If the simplifier cannot use a certain rewrite rule --- either because
3.931 +of nontermination or because its left-hand side is too flexible ---
3.932 +then you might try \texttt{stac}:
3.933 +\begin{ttdescription}
3.934 +\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
3.935 + replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
3.936 + $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking
3.937 + may be necessary to select the desired ones.
3.938 +
3.939 +If $thm$ is a conditional equality, the instantiated condition becomes an
3.940 +additional (first) subgoal.
3.941 +\end{ttdescription}
3.942 +
3.943 + \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
3.944 + for an equality throughout a subgoal and its hypotheses. This tactic uses
3.945 + \HOL's general substitution rule.
3.946 +
3.947 +\subsubsection{Case splitting}
3.948 +\label{subsec:HOL:case:splitting}
3.949 +
3.950 +\HOL{} also provides convenient means for case splitting during
3.951 +rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
3.952 +then\dots else\dots} often require a case distinction on $b$. This is
3.953 +expressed by the theorem \tdx{split_if}:
3.954 +$$
3.955 +\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
3.956 +((\Var{b} \to \Var{P}(\Var{x})) \land (\neg \Var{b} \to \Var{P}(\Var{y})))
3.957 +\eqno{(*)}
3.958 +$$
3.959 +For example, a simple instance of $(*)$ is
3.960 +\[
3.961 +x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~
3.962 +((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))
3.963 +\]
3.964 +Because $(*)$ is too general as a rewrite rule for the simplifier (the
3.965 +left-hand side is not a higher-order pattern in the sense of
3.966 +\iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
3.967 +{Chap.\ts\ref{chap:simplification}}), there is a special infix function
3.968 +\ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
3.969 +(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
3.970 +simpset, as in
3.971 +\begin{ttbox}
3.972 +by(simp_tac (simpset() addsplits [split_if]) 1);
3.973 +\end{ttbox}
3.974 +The effect is that after each round of simplification, one occurrence of
3.975 +\texttt{if} is split acording to \texttt{split_if}, until all occurences of
3.976 +\texttt{if} have been eliminated.
3.977 +
3.978 +It turns out that using \texttt{split_if} is almost always the right thing to
3.979 +do. Hence \texttt{split_if} is already included in the default simpset. If
3.980 +you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
3.981 +the inverse of \texttt{addsplits}:
3.982 +\begin{ttbox}
3.983 +by(simp_tac (simpset() delsplits [split_if]) 1);
3.984 +\end{ttbox}
3.985 +
3.986 +In general, \texttt{addsplits} accepts rules of the form
3.987 +\[
3.988 +\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
3.989 +\]
3.990 +where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
3.991 +right form because internally the left-hand side is
3.992 +$\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
3.993 +are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list}
3.994 +and~\S\ref{subsec:datatype:basics}).
3.995 +
3.996 +Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
3.997 +imperative versions of \texttt{addsplits} and \texttt{delsplits}
3.998 +\begin{ttbox}
3.999 +\ttindexbold{Addsplits}: thm list -> unit
3.1000 +\ttindexbold{Delsplits}: thm list -> unit
3.1001 +\end{ttbox}
3.1002 +for adding splitting rules to, and deleting them from the current simpset.
3.1003 +
3.1004 +\subsection{Classical reasoning}
3.1005 +
3.1006 +\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
3.1007 +well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
3.1008 +rule; recall Fig.\ts\ref{hol-lemmas2} above.
3.1009 +
3.1010 +The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
3.1011 +Best_tac} refer to the default claset (\texttt{claset()}), which works for most
3.1012 +purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
3.1013 +propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier
3.1014 +rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules,
3.1015 +and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
3.1016 +{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
3.1017 +
3.1018 +
3.1019 +\section{Types}\label{sec:HOL:Types}
3.1020 +This section describes \HOL's basic predefined types ($\alpha \times
3.1021 +\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
3.1022 +introducing new types in general. The most important type
3.1023 +construction, the \texttt{datatype}, is treated separately in
3.1024 +\S\ref{sec:HOL:datatype}.
3.1025 +
3.1026 +
3.1027 +\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
3.1028 +\label{subsec:prod-sum}
3.1029 +
3.1030 +\begin{figure}[htbp]
3.1031 +\begin{constants}
3.1032 + \it symbol & \it meta-type & & \it description \\
3.1033 + \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
3.1034 + & & ordered pairs $(a,b)$ \\
3.1035 + \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
3.1036 + \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
3.1037 + \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
3.1038 + & & generalized projection\\
3.1039 + \cdx{Sigma} &
3.1040 + $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
3.1041 + & general sum of sets
3.1042 +\end{constants}
3.1043 +\begin{ttbox}\makeatletter
3.1044 +%\tdx{fst_def} fst p == @a. ? b. p = (a,b)
3.1045 +%\tdx{snd_def} snd p == @b. ? a. p = (a,b)
3.1046 +%\tdx{split_def} split c p == c (fst p) (snd p)
3.1047 +\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
3.1048 +
3.1049 +\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
3.1050 +\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
3.1051 +\tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
3.1052 +
3.1053 +\tdx{fst_conv} fst (a,b) = a
3.1054 +\tdx{snd_conv} snd (a,b) = b
3.1055 +\tdx{surjective_pairing} p = (fst p,snd p)
3.1056 +
3.1057 +\tdx{split} split c (a,b) = c a b
3.1058 +\tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
3.1059 +
3.1060 +\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
3.1061 +\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
3.1062 +\end{ttbox}
3.1063 +\caption{Type $\alpha\times\beta$}\label{hol-prod}
3.1064 +\end{figure}
3.1065 +
3.1066 +Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
3.1067 +$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
3.1068 +tuples are simulated by pairs nested to the right:
3.1069 +\begin{center}
3.1070 +\begin{tabular}{c|c}
3.1071 +external & internal \\
3.1072 +\hline
3.1073 +$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
3.1074 +\hline
3.1075 +$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
3.1076 +\end{tabular}
3.1077 +\end{center}
3.1078 +In addition, it is possible to use tuples
3.1079 +as patterns in abstractions:
3.1080 +\begin{center}
3.1081 +{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}
3.1082 +\end{center}
3.1083 +Nested patterns are also supported. They are translated stepwise:
3.1084 +{\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$
3.1085 +{\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$
3.1086 + $z$.\ $t$))}. The reverse translation is performed upon printing.
3.1087 +\begin{warn}
3.1088 + The translation between patterns and \texttt{split} is performed automatically
3.1089 + by the parser and printer. Thus the internal and external form of a term
3.1090 + may differ, which can affects proofs. For example the term {\tt
3.1091 + (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
3.1092 + default simpset) to rewrite to {\tt(b,a)}.
3.1093 +\end{warn}
3.1094 +In addition to explicit $\lambda$-abstractions, patterns can be used in any
3.1095 +variable binding construct which is internally described by a
3.1096 +$\lambda$-abstraction. Some important examples are
3.1097 +\begin{description}
3.1098 +\item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
3.1099 +\item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$}
3.1100 +\item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
3.1101 +\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
3.1102 +\item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
3.1103 +\end{description}
3.1104 +
3.1105 +There is a simple tactic which supports reasoning about patterns:
3.1106 +\begin{ttdescription}
3.1107 +\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
3.1108 + {\tt!!}-quantified variables of product type by individual variables for
3.1109 + each component. A simple example:
3.1110 +\begin{ttbox}
3.1111 +{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
3.1112 +by(split_all_tac 1);
3.1113 +{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
3.1114 +\end{ttbox}
3.1115 +\end{ttdescription}
3.1116 +
3.1117 +Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
3.1118 +which contains only a single element named {\tt()} with the property
3.1119 +\begin{ttbox}
3.1120 +\tdx{unit_eq} u = ()
3.1121 +\end{ttbox}
3.1122 +\bigskip
3.1123 +
3.1124 +Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
3.1125 +which associates to the right and has a lower priority than $*$: $\tau@1 +
3.1126 +\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
3.1127 +
3.1128 +The definition of products and sums in terms of existing types is not
3.1129 +shown. The constructions are fairly standard and can be found in the
3.1130 +respective theory files.
3.1131 +
3.1132 +\begin{figure}
3.1133 +\begin{constants}
3.1134 + \it symbol & \it meta-type & & \it description \\
3.1135 + \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
3.1136 + \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
3.1137 + \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
3.1138 + & & conditional
3.1139 +\end{constants}
3.1140 +\begin{ttbox}\makeatletter
3.1141 +%\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
3.1142 +% (!y. p=Inr y --> z=g y))
3.1143 +%
3.1144 +\tdx{Inl_not_Inr} Inl a ~= Inr b
3.1145 +
3.1146 +\tdx{inj_Inl} inj Inl
3.1147 +\tdx{inj_Inr} inj Inr
3.1148 +
3.1149 +\tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s
3.1150 +
3.1151 +\tdx{sum_case_Inl} sum_case f g (Inl x) = f x
3.1152 +\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
3.1153 +
3.1154 +\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
3.1155 +\tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
3.1156 + (! y. s = Inr(y) --> R(g(y))))
3.1157 +\end{ttbox}
3.1158 +\caption{Type $\alpha+\beta$}\label{hol-sum}
3.1159 +\end{figure}
3.1160 +
3.1161 +\begin{figure}
3.1162 +\index{*"< symbol}
3.1163 +\index{*"* symbol}
3.1164 +\index{*div symbol}
3.1165 +\index{*mod symbol}
3.1166 +\index{*"+ symbol}
3.1167 +\index{*"- symbol}
3.1168 +\begin{constants}
3.1169 + \it symbol & \it meta-type & \it priority & \it description \\
3.1170 + \cdx{0} & $nat$ & & zero \\
3.1171 + \cdx{Suc} & $nat \To nat$ & & successor function\\
3.1172 +% \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\
3.1173 +% \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
3.1174 +% & & primitive recursor\\
3.1175 + \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
3.1176 + \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
3.1177 + \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
3.1178 + \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
3.1179 + \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
3.1180 +\end{constants}
3.1181 +\subcaption{Constants and infixes}
3.1182 +
3.1183 +\begin{ttbox}\makeatother
3.1184 +\tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n
3.1185 +
3.1186 +\tdx{Suc_not_Zero} Suc m ~= 0
3.1187 +\tdx{inj_Suc} inj Suc
3.1188 +\tdx{n_not_Suc_n} n~=Suc n
3.1189 +\subcaption{Basic properties}
3.1190 +\end{ttbox}
3.1191 +\caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
3.1192 +\end{figure}
3.1193 +
3.1194 +
3.1195 +\begin{figure}
3.1196 +\begin{ttbox}\makeatother
3.1197 + 0+n = n
3.1198 + (Suc m)+n = Suc(m+n)
3.1199 +
3.1200 + m-0 = m
3.1201 + 0-n = n
3.1202 + Suc(m)-Suc(n) = m-n
3.1203 +
3.1204 + 0*n = 0
3.1205 + Suc(m)*n = n + m*n
3.1206 +
3.1207 +\tdx{mod_less} m<n ==> m mod n = m
3.1208 +\tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
3.1209 +
3.1210 +\tdx{div_less} m<n ==> m div n = 0
3.1211 +\tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)
3.1212 +\end{ttbox}
3.1213 +\caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
3.1214 +\end{figure}
3.1215 +
3.1216 +\subsection{The type of natural numbers, \textit{nat}}
3.1217 +\index{nat@{\textit{nat}} type|(}
3.1218 +
3.1219 +The theory \thydx{NatDef} defines the natural numbers in a roundabout but
3.1220 +traditional way. The axiom of infinity postulates a type~\tydx{ind} of
3.1221 +individuals, which is non-empty and closed under an injective operation. The
3.1222 +natural numbers are inductively generated by choosing an arbitrary individual
3.1223 +for~0 and using the injective operation to take successors. This is a least
3.1224 +fixedpoint construction. For details see the file \texttt{NatDef.thy}.
3.1225 +
3.1226 +Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the
3.1227 +overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also
3.1228 +\cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory
3.1229 +\thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order,
3.1230 +so \tydx{nat} is also an instance of class \cldx{order}.
3.1231 +
3.1232 +Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines
3.1233 +addition, multiplication and subtraction. Theory \thydx{Divides} defines
3.1234 +division, remainder and the ``divides'' relation. The numerous theorems
3.1235 +proved include commutative, associative, distributive, identity and
3.1236 +cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The
3.1237 +recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
3.1238 +\texttt{nat} are part of the default simpset.
3.1239 +
3.1240 +Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
3.1241 +see \S\ref{sec:HOL:recursive}. A simple example is addition.
3.1242 +Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
3.1243 +the standard convention.
3.1244 +\begin{ttbox}
3.1245 +\sdx{primrec}
3.1246 + "0 + n = n"
3.1247 + "Suc m + n = Suc (m + n)"
3.1248 +\end{ttbox}
3.1249 +There is also a \sdx{case}-construct
3.1250 +of the form
3.1251 +\begin{ttbox}
3.1252 +case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
3.1253 +\end{ttbox}
3.1254 +Note that Isabelle insists on precisely this format; you may not even change
3.1255 +the order of the two cases.
3.1256 +Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
3.1257 +\cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}.
3.1258 +
3.1259 +%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
3.1260 +%Recursion along this relation resembles primitive recursion, but is
3.1261 +%stronger because we are in higher-order logic; using primitive recursion to
3.1262 +%define a higher-order function, we can easily Ackermann's function, which
3.1263 +%is not primitive recursive \cite[page~104]{thompson91}.
3.1264 +%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
3.1265 +%natural numbers are most easily expressed using recursion along~$<$.
3.1266 +
3.1267 +Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
3.1268 +in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived
3.1269 +theorem \tdx{less_induct}:
3.1270 +\begin{ttbox}
3.1271 +[| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
3.1272 +\end{ttbox}
3.1273 +
3.1274 +
3.1275 +Reasoning about arithmetic inequalities can be tedious. Fortunately HOL
3.1276 +provides a decision procedure for quantifier-free linear arithmetic (i.e.\
3.1277 +only addition and subtraction). The simplifier invokes a weak version of this
3.1278 +decision procedure automatically. If this is not sufficent, you can invoke
3.1279 +the full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary
3.1280 +formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
3.1281 + min}, {\tt max} and numerical constants; other subterms are treated as
3.1282 +atomic; subformulae not involving type $nat$ are ignored; quantified
3.1283 +subformulae are ignored unless they are positive universal or negative
3.1284 +existential. Note that the running time is exponential in the number of
3.1285 +occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
3.1286 +distinctions. Note also that \texttt{arith_tac} is not complete: if
3.1287 +divisibility plays a role, it may fail to prove a valid formula, for example
3.1288 +$m+m \neq n+n+1$. Fortunately such examples are rare in practice.
3.1289 +
3.1290 +If \texttt{arith_tac} fails you, try to find relevant arithmetic results in
3.1291 +the library. The theory \texttt{NatDef} contains theorems about {\tt<} and
3.1292 +{\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},
3.1293 +\texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about
3.1294 +\texttt{div} and \texttt{mod}. Use the \texttt{find}-functions to locate them
3.1295 +(see the {\em Reference Manual\/}).
3.1296 +
3.1297 +\begin{figure}
3.1298 +\index{#@{\tt[]} symbol}
3.1299 +\index{#@{\tt\#} symbol}
3.1300 +\index{"@@{\tt\at} symbol}
3.1301 +\index{*"! symbol}
3.1302 +\begin{constants}
3.1303 + \it symbol & \it meta-type & \it priority & \it description \\
3.1304 + \tt[] & $\alpha\,list$ & & empty list\\
3.1305 + \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
3.1306 + list constructor \\
3.1307 + \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
3.1308 + \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
3.1309 + \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
3.1310 + \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
3.1311 + \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
3.1312 + \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
3.1313 + \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
3.1314 + & & apply to all\\
3.1315 + \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
3.1316 + & & filter functional\\
3.1317 + \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
3.1318 + \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
3.1319 + \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
3.1320 + & iteration \\
3.1321 + \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
3.1322 + \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
3.1323 + \cdx{length} & $\alpha\,list \To nat$ & & length \\
3.1324 + \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
3.1325 + \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
3.1326 + take or drop a prefix \\
3.1327 + \cdx{takeWhile},\\
3.1328 + \cdx{dropWhile} &
3.1329 + $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
3.1330 + take or drop a prefix
3.1331 +\end{constants}
3.1332 +\subcaption{Constants and infixes}
3.1333 +
3.1334 +\begin{center} \tt\frenchspacing
3.1335 +\begin{tabular}{rrr}
3.1336 + \it external & \it internal & \it description \\{}
3.1337 + [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
3.1338 + \rm finite list \\{}
3.1339 + [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
3.1340 + \rm list comprehension
3.1341 +\end{tabular}
3.1342 +\end{center}
3.1343 +\subcaption{Translations}
3.1344 +\caption{The theory \thydx{List}} \label{hol-list}
3.1345 +\end{figure}
3.1346 +
3.1347 +
3.1348 +\begin{figure}
3.1349 +\begin{ttbox}\makeatother
3.1350 +null [] = True
3.1351 +null (x#xs) = False
3.1352 +
3.1353 +hd (x#xs) = x
3.1354 +tl (x#xs) = xs
3.1355 +tl [] = []
3.1356 +
3.1357 +[] @ ys = ys
3.1358 +(x#xs) @ ys = x # xs @ ys
3.1359 +
3.1360 +map f [] = []
3.1361 +map f (x#xs) = f x # map f xs
3.1362 +
3.1363 +filter P [] = []
3.1364 +filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
3.1365 +
3.1366 +set [] = \ttlbrace\ttrbrace
3.1367 +set (x#xs) = insert x (set xs)
3.1368 +
3.1369 +x mem [] = False
3.1370 +x mem (y#ys) = (if y=x then True else x mem ys)
3.1371 +
3.1372 +foldl f a [] = a
3.1373 +foldl f a (x#xs) = foldl f (f a x) xs
3.1374 +
3.1375 +concat([]) = []
3.1376 +concat(x#xs) = x @ concat(xs)
3.1377 +
3.1378 +rev([]) = []
3.1379 +rev(x#xs) = rev(xs) @ [x]
3.1380 +
3.1381 +length([]) = 0
3.1382 +length(x#xs) = Suc(length(xs))
3.1383 +
3.1384 +xs!0 = hd xs
3.1385 +xs!(Suc n) = (tl xs)!n
3.1386 +
3.1387 +take n [] = []
3.1388 +take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
3.1389 +
3.1390 +drop n [] = []
3.1391 +drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
3.1392 +
3.1393 +takeWhile P [] = []
3.1394 +takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
3.1395 +
3.1396 +dropWhile P [] = []
3.1397 +dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)
3.1398 +\end{ttbox}
3.1399 +\caption{Recursions equations for list processing functions}
3.1400 +\label{fig:HOL:list-simps}
3.1401 +\end{figure}
3.1402 +\index{nat@{\textit{nat}} type|)}
3.1403 +
3.1404 +
3.1405 +\subsection{The type constructor for lists, \textit{list}}
3.1406 +\label{subsec:list}
3.1407 +\index{list@{\textit{list}} type|(}
3.1408 +
3.1409 +Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
3.1410 +operations with their types and syntax. Type $\alpha \; list$ is
3.1411 +defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
3.1412 +As a result the generic structural induction and case analysis tactics
3.1413 +\texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for
3.1414 +lists. A \sdx{case} construct of the form
3.1415 +\begin{center}\tt
3.1416 +case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
3.1417 +\end{center}
3.1418 +is defined by translation. For details see~\S\ref{sec:HOL:datatype}. There
3.1419 +is also a case splitting rule \tdx{split_list_case}
3.1420 +\[
3.1421 +\begin{array}{l}
3.1422 +P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
3.1423 + x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\
3.1424 +((e = \texttt{[]} \to P(a)) \land
3.1425 + (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))
3.1426 +\end{array}
3.1427 +\]
3.1428 +which can be fed to \ttindex{addsplits} just like
3.1429 +\texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}).
3.1430 +
3.1431 +\texttt{List} provides a basic library of list processing functions defined by
3.1432 +primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations
3.1433 +are shown in Fig.\ts\ref{fig:HOL:list-simps}.
3.1434 +
3.1435 +\index{list@{\textit{list}} type|)}
3.1436 +
3.1437 +
3.1438 +\subsection{Introducing new types} \label{sec:typedef}
3.1439 +
3.1440 +The \HOL-methodology dictates that all extensions to a theory should
3.1441 +be \textbf{definitional}. The type definition mechanism that
3.1442 +meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms},
3.1443 +which are inherited from {\Pure} and described elsewhere, are just
3.1444 +syntactic abbreviations that have no logical meaning.
3.1445 +
3.1446 +\begin{warn}
3.1447 + Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
3.1448 + unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
3.1449 +\end{warn}
3.1450 +A \bfindex{type definition} identifies the new type with a subset of
3.1451 +an existing type. More precisely, the new type is defined by
3.1452 +exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
3.1453 +theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,
3.1454 +and the new type denotes this subset. New functions are defined that
3.1455 +establish an isomorphism between the new type and the subset. If
3.1456 +type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,
3.1457 +then the type definition creates a type constructor
3.1458 +$(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
3.1459 +
3.1460 +\begin{figure}[htbp]
3.1461 +\begin{rail}
3.1462 +typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
3.1463 +
3.1464 +type : typevarlist name ( () | '(' infix ')' );
3.1465 +set : string;
3.1466 +witness : () | '(' id ')';
3.1467 +\end{rail}
3.1468 +\caption{Syntax of type definitions}
3.1469 +\label{fig:HOL:typedef}
3.1470 +\end{figure}
3.1471 +
3.1472 +The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
3.1473 +the definition of `typevarlist' and `infix' see
3.1474 +\iflabelundefined{chap:classical}
3.1475 +{the appendix of the {\em Reference Manual\/}}%
3.1476 +{Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
3.1477 +following meaning:
3.1478 +\begin{description}
3.1479 +\item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
3.1480 + optional infix annotation.
3.1481 +\item[\it name:] an alphanumeric name $T$ for the type constructor
3.1482 + $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.
3.1483 +\item[\it set:] the representing subset $A$.
3.1484 +\item[\it witness:] name of a theorem of the form $a:A$ proving
3.1485 + non-emptiness. It can be omitted in case Isabelle manages to prove
3.1486 + non-emptiness automatically.
3.1487 +\end{description}
3.1488 +If all context conditions are met (no duplicate type variables in
3.1489 +`typevarlist', no extra type variables in `set', and no free term variables
3.1490 +in `set'), the following components are added to the theory:
3.1491 +\begin{itemize}
3.1492 +\item a type $ty :: (term,\dots,term)term$
3.1493 +\item constants
3.1494 +\begin{eqnarray*}
3.1495 +T &::& \tau\;set \\
3.1496 +Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
3.1497 +Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty
3.1498 +\end{eqnarray*}
3.1499 +\item a definition and three axioms
3.1500 +\[
3.1501 +\begin{array}{ll}
3.1502 +T{\tt_def} & T \equiv A \\
3.1503 +{\tt Rep_}T & Rep_T\,x \in T \\
3.1504 +{\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\
3.1505 +{\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y
3.1506 +\end{array}
3.1507 +\]
3.1508 +stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
3.1509 +and its inverse $Abs_T$.
3.1510 +\end{itemize}
3.1511 +Below are two simple examples of \HOL\ type definitions. Non-emptiness
3.1512 +is proved automatically here.
3.1513 +\begin{ttbox}
3.1514 +typedef unit = "{\ttlbrace}True{\ttrbrace}"
3.1515 +
3.1516 +typedef (prod)
3.1517 + ('a, 'b) "*" (infixr 20)
3.1518 + = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"
3.1519 +\end{ttbox}
3.1520 +
3.1521 +Type definitions permit the introduction of abstract data types in a safe
3.1522 +way, namely by providing models based on already existing types. Given some
3.1523 +abstract axiomatic description $P$ of a type, this involves two steps:
3.1524 +\begin{enumerate}
3.1525 +\item Find an appropriate type $\tau$ and subset $A$ which has the desired
3.1526 + properties $P$, and make a type definition based on this representation.
3.1527 +\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
3.1528 +\end{enumerate}
3.1529 +You can now forget about the representation and work solely in terms of the
3.1530 +abstract properties $P$.
3.1531 +
3.1532 +\begin{warn}
3.1533 +If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
3.1534 +declaring the type and its operations and by stating the desired axioms, you
3.1535 +should make sure the type has a non-empty model. You must also have a clause
3.1536 +\par
3.1537 +\begin{ttbox}
3.1538 +arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
3.1539 +\end{ttbox}
3.1540 +in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
3.1541 +class of all \HOL\ types.
3.1542 +\end{warn}
3.1543 +
3.1544 +
3.1545 +\section{Records}
3.1546 +
3.1547 +At a first approximation, records are just a minor generalisation of tuples,
3.1548 +where components may be addressed by labels instead of just position (think of
3.1549 +{\ML}, for example). The version of records offered by Isabelle/HOL is
3.1550 +slightly more advanced, though, supporting \emph{extensible record schemes}.
3.1551 +This admits operations that are polymorphic with respect to record extension,
3.1552 +yielding ``object-oriented'' effects like (single) inheritance. See also
3.1553 +\cite{Naraschewski-Wenzel:1998:TPHOL} for more details on object-oriented
3.1554 +verification and record subtyping in HOL.
3.1555 +
3.1556 +
3.1557 +\subsection{Basics}
3.1558 +
3.1559 +Isabelle/HOL supports fixed and schematic records both at the level of terms
3.1560 +and types. The concrete syntax is as follows:
3.1561 +
3.1562 +\begin{center}
3.1563 +\begin{tabular}{l|l|l}
3.1564 + & record terms & record types \\ \hline
3.1565 + fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
3.1566 + schematic & $\record{x = a\fs y = b\fs \more = m}$ &
3.1567 + $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
3.1568 +\end{tabular}
3.1569 +\end{center}
3.1570 +
3.1571 +\noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.
3.1572 +
3.1573 +A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
3.1574 +$y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$,
3.1575 +assuming that $a \ty A$ and $b \ty B$.
3.1576 +
3.1577 +A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
3.1578 +$x$ and $y$ as before, but also possibly further fields as indicated by the
3.1579 +``$\more$'' notation (which is actually part of the syntax). The improper
3.1580 +field ``$\more$'' of a record scheme is called the \emph{more part}.
3.1581 +Logically it is just a free variable, which is occasionally referred to as
3.1582 +\emph{row variable} in the literature. The more part of a record scheme may
3.1583 +be instantiated by zero or more further components. For example, above scheme
3.1584 +might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,
3.1585 +where $m'$ refers to a different more part. Fixed records are special
3.1586 +instances of record schemes, where ``$\more$'' is properly terminated by the
3.1587 +$() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an
3.1588 +abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
3.1589 +
3.1590 +\medskip
3.1591 +
3.1592 +There are two key features that make extensible records in a simply typed
3.1593 +language like HOL feasible:
3.1594 +\begin{enumerate}
3.1595 +\item the more part is internalised, as a free term or type variable,
3.1596 +\item field names are externalised, they cannot be accessed within the logic
3.1597 + as first-class values.
3.1598 +\end{enumerate}
3.1599 +
3.1600 +\medskip
3.1601 +
3.1602 +In Isabelle/HOL record types have to be defined explicitly, fixing their field
3.1603 +names and types, and their (optional) parent record (see
3.1604 +\S\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
3.1605 +syntax, while obeying the canonical order of fields as given by their
3.1606 +declaration. The record package also provides several operations like
3.1607 +selectors and updates (see \S\ref{sec:HOL:record-ops}), together with
3.1608 +characteristic properties (see \S\ref{sec:HOL:record-thms}).
3.1609 +
3.1610 +There is an example theory demonstrating most basic aspects of extensible
3.1611 +records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
3.1612 +
3.1613 +
3.1614 +\subsection{Defining records}\label{sec:HOL:record-def}
3.1615 +
3.1616 +The theory syntax for record type definitions is shown in
3.1617 +Fig.~\ref{fig:HOL:record}. For the definition of `typevarlist' and `type' see
3.1618 +\iflabelundefined{chap:classical}
3.1619 +{the appendix of the {\em Reference Manual\/}}%
3.1620 +{Appendix~\ref{app:TheorySyntax}}.
3.1621 +
3.1622 +\begin{figure}[htbp]
3.1623 +\begin{rail}
3.1624 +record : 'record' typevarlist name '=' parent (field +);
3.1625 +
3.1626 +parent : ( () | type '+');
3.1627 +field : name '::' type;
3.1628 +\end{rail}
3.1629 +\caption{Syntax of record type definitions}
3.1630 +\label{fig:HOL:record}
3.1631 +\end{figure}
3.1632 +
3.1633 +A general \ttindex{record} specification is of the following form:
3.1634 +\[
3.1635 +\mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
3.1636 + (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l
3.1637 +\]
3.1638 +where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,
3.1639 +$\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.
3.1640 +Type constructor $t$ has to be new, while $s$ has to specify an existing
3.1641 +record type. Furthermore, the $\vec c@l$ have to be distinct field names.
3.1642 +There has to be at least one field.
3.1643 +
3.1644 +In principle, field names may never be shared with other records. This is no
3.1645 +actual restriction in practice, since $\vec c@l$ are internally declared
3.1646 +within a separate name space qualified by the name $t$ of the record.
3.1647 +
3.1648 +\medskip
3.1649 +
3.1650 +Above definition introduces a new record type $(\vec\alpha@n) \, t$ by
3.1651 +extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty
3.1652 +\vec\sigma@l$. The parent record specification is optional, by omitting it
3.1653 +$t$ becomes a \emph{root record}. The hierarchy of all records declared
3.1654 +within a theory forms a forest structure, i.e.\ a set of trees, where any of
3.1655 +these is rooted by some root record.
3.1656 +
3.1657 +For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the
3.1658 +fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,
3.1659 +\zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty
3.1660 + \vec\sigma@l\fs \more \ty \zeta}$.
3.1661 +
3.1662 +\medskip
3.1663 +
3.1664 +The following simple example defines a root record type $point$ with fields $x
3.1665 +\ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with
3.1666 +an additional $colour$ component.
3.1667 +
3.1668 +\begin{ttbox}
3.1669 + record point =
3.1670 + x :: nat
3.1671 + y :: nat
3.1672 +
3.1673 + record cpoint = point +
3.1674 + colour :: string
3.1675 +\end{ttbox}
3.1676 +
3.1677 +
3.1678 +\subsection{Record operations}\label{sec:HOL:record-ops}
3.1679 +
3.1680 +Any record definition of the form presented above produces certain standard
3.1681 +operations. Selectors and updates are provided for any field, including the
3.1682 +improper one ``$more$''. There are also cumulative record constructor
3.1683 +functions.
3.1684 +
3.1685 +To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$
3.1686 +is a root record with fields $\vec c@l \ty \vec\sigma@l$.
3.1687 +
3.1688 +\medskip
3.1689 +
3.1690 +\textbf{Selectors} and \textbf{updates} are available for any field (including
3.1691 +``$more$'') as follows:
3.1692 +\begin{matharray}{lll}
3.1693 + c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\
3.1694 + c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To
3.1695 + \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}
3.1696 +\end{matharray}
3.1697 +
3.1698 +There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
3.1699 +term $x_update \, a \, r$. Repeated updates are also supported: $r \,
3.1700 +\record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
3.1701 +$r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of
3.1702 +postfix notation the order of fields shown here is reverse than in the actual
3.1703 +term. This might lead to confusion in conjunction with proof tools like
3.1704 +ordered rewriting.
3.1705 +
3.1706 +Since repeated updates are just function applications, fields may be freely
3.1707 +permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
3.1708 +is concerned. Thus commutativity of updates can be proven within the logic
3.1709 +for any two fields, but not as a general theorem: fields are not first-class
3.1710 +values.
3.1711 +
3.1712 +\medskip
3.1713 +
3.1714 +\textbf{Make} operations provide cumulative record constructor functions:
3.1715 +\begin{matharray}{lll}
3.1716 + make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\
3.1717 + make_scheme & \ty & \vec\sigma@l \To
3.1718 + \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\
3.1719 +\end{matharray}
3.1720 +\noindent
3.1721 +These functions are curried. The corresponding definitions in terms of actual
3.1722 +record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$
3.1723 +rewrites to $\record{x = a\fs y = b}$.
3.1724 +
3.1725 +\medskip
3.1726 +
3.1727 +Any of above selector, update and make operations are declared within a local
3.1728 +name space prefixed by the name $t$ of the record. In case that different
3.1729 +records share base names of fields, one has to qualify names explicitly (e.g.\
3.1730 +$t\dtt c@i_update$). This is recommended especially for operations like
3.1731 +$make$ or $update_more$ that always have the same base name. Just use $t\dtt
3.1732 +make$ etc.\ to avoid confusion.
3.1733 +
3.1734 +\bigskip
3.1735 +
3.1736 +We reconsider the case of non-root records, which are derived of some parent
3.1737 +record. In general, the latter may depend on another parent as well,
3.1738 +resulting in a list of \emph{ancestor records}. Appending the lists of fields
3.1739 +of all ancestors results in a certain field prefix. The record package
3.1740 +automatically takes care of this by lifting operations over this context of
3.1741 +ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields
3.1742 +$\vec d@k \ty \vec\rho@k$, selectors will get the following types:
3.1743 +\begin{matharray}{lll}
3.1744 + c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}
3.1745 + \To \sigma@i
3.1746 +\end{matharray}
3.1747 +\noindent
3.1748 +Update and make operations are analogous.
3.1749 +
3.1750 +
3.1751 +\subsection{Proof tools}\label{sec:HOL:record-thms}
3.1752 +
3.1753 +The record package provides the following proof rules for any record type $t$.
3.1754 +\begin{enumerate}
3.1755 +
3.1756 +\item Standard conversions (selectors or updates applied to record constructor
3.1757 + terms, make function definitions) are part of the standard simpset (via
3.1758 + \texttt{addsimps}).
3.1759 +
3.1760 +\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
3.1761 + \conj y=y'$ are made part of the standard simpset and claset (via
3.1762 + \texttt{addIffs}).
3.1763 +
3.1764 +\item A tactic for record field splitting (\ttindex{record_split_tac}) is made
3.1765 + part of the standard claset (via \texttt{addSWrapper}). This tactic is
3.1766 + based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a,
3.1767 + b))$ for any field.
3.1768 +\end{enumerate}
3.1769 +
3.1770 +The first two kinds of rules are stored within the theory as $t\dtt simps$ and
3.1771 +$t\dtt iffs$, respectively. In some situations it might be appropriate to
3.1772 +expand the definitions of updates: $t\dtt updates$. Following a new trend in
3.1773 +Isabelle system architecture, these names are \emph{not} bound at the {\ML}
3.1774 +level, though.
3.1775 +
3.1776 +\medskip
3.1777 +
3.1778 +The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
3.1779 +concerning records. The basic idea is to make \ttindex{record_split_tac}
3.1780 +expand quantified record variables and then simplify by the conversion rules.
3.1781 +By using a combination of the simplifier and classical prover together with
3.1782 +the default simpset and claset, record problems should be solved with a single
3.1783 +stroke of \texttt{Auto_tac} or \texttt{Force_tac}.
3.1784 +
3.1785 +
3.1786 +\section{Datatype definitions}
3.1787 +\label{sec:HOL:datatype}
3.1788 +\index{*datatype|(}
3.1789 +
3.1790 +Inductive datatypes, similar to those of \ML, frequently appear in
3.1791 +applications of Isabelle/HOL. In principle, such types could be defined by
3.1792 +hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
3.1793 +tedious. The \ttindex{datatype} definition package of \HOL\ automates such
3.1794 +chores. It generates an appropriate \texttt{typedef} based on a least
3.1795 +fixed-point construction, and proves freeness theorems and induction rules, as
3.1796 +well as theorems for recursion and case combinators. The user just has to
3.1797 +give a simple specification of new inductive types using a notation similar to
3.1798 +{\ML} or Haskell.
3.1799 +
3.1800 +The current datatype package can handle both mutual and indirect recursion.
3.1801 +It also offers to represent existing types as datatypes giving the advantage
3.1802 +of a more uniform view on standard theories.
3.1803 +
3.1804 +
3.1805 +\subsection{Basics}
3.1806 +\label{subsec:datatype:basics}
3.1807 +
3.1808 +A general \texttt{datatype} definition is of the following form:
3.1809 +\[
3.1810 +\begin{array}{llcl}
3.1811 +\mathtt{datatype} & (\alpha@1,\ldots,\alpha@h)t@1 & = &
3.1812 + C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~
3.1813 + C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\
3.1814 + & & \vdots \\
3.1815 +\mathtt{and} & (\alpha@1,\ldots,\alpha@h)t@n & = &
3.1816 + C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~
3.1817 + C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}
3.1818 +\end{array}
3.1819 +\]
3.1820 +where $\alpha@i$ are type variables, $C^j@i$ are distinct constructor
3.1821 +names and $\tau^j@{i,i'}$ are {\em admissible} types containing at
3.1822 +most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$
3.1823 +occurring in a \texttt{datatype} definition is {\em admissible} iff
3.1824 +\begin{itemize}
3.1825 +\item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
3.1826 +newly defined type constructors $t@1,\ldots,t@n$, or
3.1827 +\item $\tau = (\alpha@1,\ldots,\alpha@h)t@{j'}$ where $1 \leq j' \leq n$, or
3.1828 +\item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
3.1829 +the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
3.1830 +are admissible types.
3.1831 +\end{itemize}
3.1832 +If some $(\alpha@1,\ldots,\alpha@h)t@{j'}$ occurs in a type $\tau^j@{i,i'}$
3.1833 +of the form
3.1834 +\[
3.1835 +(\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t'
3.1836 +\]
3.1837 +this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
3.1838 +example of a datatype is the type \texttt{list}, which can be defined by
3.1839 +\begin{ttbox}
3.1840 +datatype 'a list = Nil
3.1841 + | Cons 'a ('a list)
3.1842 +\end{ttbox}
3.1843 +Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled
3.1844 +by the mutually recursive datatype definition
3.1845 +\begin{ttbox}
3.1846 +datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
3.1847 + | Sum ('a aexp) ('a aexp)
3.1848 + | Diff ('a aexp) ('a aexp)
3.1849 + | Var 'a
3.1850 + | Num nat
3.1851 +and 'a bexp = Less ('a aexp) ('a aexp)
3.1852 + | And ('a bexp) ('a bexp)
3.1853 + | Or ('a bexp) ('a bexp)
3.1854 +\end{ttbox}
3.1855 +The datatype \texttt{term}, which is defined by
3.1856 +\begin{ttbox}
3.1857 +datatype ('a, 'b) term = Var 'a
3.1858 + | App 'b ((('a, 'b) term) list)
3.1859 +\end{ttbox}
3.1860 +is an example for a datatype with nested recursion.
3.1861 +
3.1862 +\medskip
3.1863 +
3.1864 +Types in HOL must be non-empty. Each of the new datatypes
3.1865 +$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is non-empty iff it has a
3.1866 +constructor $C^j@i$ with the following property: for all argument types
3.1867 +$\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype
3.1868 +$(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty.
3.1869 +
3.1870 +If there are no nested occurrences of the newly defined datatypes, obviously
3.1871 +at least one of the newly defined datatypes $(\alpha@1,\ldots,\alpha@h)t@j$
3.1872 +must have a constructor $C^j@i$ without recursive arguments, a \emph{base
3.1873 + case}, to ensure that the new types are non-empty. If there are nested
3.1874 +occurrences, a datatype can even be non-empty without having a base case
3.1875 +itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
3.1876 + list)} is non-empty as well.
3.1877 +
3.1878 +
3.1879 +\subsubsection{Freeness of the constructors}
3.1880 +
3.1881 +The datatype constructors are automatically defined as functions of their
3.1882 +respective type:
3.1883 +\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
3.1884 +These functions have certain {\em freeness} properties. They construct
3.1885 +distinct values:
3.1886 +\[
3.1887 +C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
3.1888 +\mbox{for all}~ i \neq i'.
3.1889 +\]
3.1890 +The constructor functions are injective:
3.1891 +\[
3.1892 +(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
3.1893 +(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
3.1894 +\]
3.1895 +Because the number of distinctness inequalities is quadratic in the number of
3.1896 +constructors, a different representation is used if there are $7$ or more of
3.1897 +them. In that case every constructor term is mapped to a natural number:
3.1898 +\[
3.1899 +t@j_ord \, (C^j@i \, x@1 \, \dots \, x@{m^j@i}) = i - 1
3.1900 +\]
3.1901 +Then distinctness of constructor terms is expressed by:
3.1902 +\[
3.1903 +t@j_ord \, x \neq t@j_ord \, y \Imp x \neq y.
3.1904 +\]
3.1905 +
3.1906 +\subsubsection{Structural induction}
3.1907 +
3.1908 +The datatype package also provides structural induction rules. For
3.1909 +datatypes without nested recursion, this is of the following form:
3.1910 +\[
3.1911 +\infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
3.1912 + {\begin{array}{lcl}
3.1913 + \Forall x@1 \dots x@{m^1@1}.
3.1914 + \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
3.1915 + P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &
3.1916 + P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\
3.1917 + & \vdots \\
3.1918 + \Forall x@1 \dots x@{m^1@{k@1}}.
3.1919 + \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;
3.1920 + P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &
3.1921 + P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\
3.1922 + & \vdots \\
3.1923 + \Forall x@1 \dots x@{m^n@1}.
3.1924 + \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;
3.1925 + P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &
3.1926 + P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\
3.1927 + & \vdots \\
3.1928 + \Forall x@1 \dots x@{m^n@{k@n}}.
3.1929 + \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots
3.1930 + P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &
3.1931 + P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)
3.1932 + \end{array}}
3.1933 +\]
3.1934 +where
3.1935 +\[
3.1936 +\begin{array}{rcl}
3.1937 +Rec^j@i & := &
3.1938 + \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
3.1939 + \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
3.1940 +&& \left\{(i',i'')~\left|~
3.1941 + 1\leq i' \leq m^j@i \wedge 1 \leq i'' \leq n \wedge
3.1942 + \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
3.1943 +\end{array}
3.1944 +\]
3.1945 +i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
3.1946 +
3.1947 +For datatypes with nested recursion, such as the \texttt{term} example from
3.1948 +above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds
3.1949 +a definition like
3.1950 +\begin{ttbox}
3.1951 +datatype ('a, 'b) term = Var 'a
3.1952 + | App 'b ((('a, 'b) term) list)
3.1953 +\end{ttbox}
3.1954 +to an equivalent definition without nesting:
3.1955 +\begin{ttbox}
3.1956 +datatype ('a, 'b) term = Var
3.1957 + | App 'b (('a, 'b) term_list)
3.1958 +and ('a, 'b) term_list = Nil'
3.1959 + | Cons' (('a,'b) term) (('a,'b) term_list)
3.1960 +\end{ttbox}
3.1961 +Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
3.1962 + Nil'} and \texttt{Cons'} are not really introduced. One can directly work with
3.1963 +the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
3.1964 +constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
3.1965 +\texttt{term} gets the form
3.1966 +\[
3.1967 +\infer{P@1~x@1 \wedge P@2~x@2}
3.1968 + {\begin{array}{l}
3.1969 + \Forall x.~P@1~(\mathtt{Var}~x) \\
3.1970 + \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
3.1971 + P@2~\mathtt{Nil} \\
3.1972 + \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)
3.1973 + \end{array}}
3.1974 +\]
3.1975 +Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
3.1976 +and one for the type \texttt{(('a, 'b) term) list}.
3.1977 +
3.1978 +\medskip In principle, inductive types are already fully determined by
3.1979 +freeness and structural induction. For convenience in applications,
3.1980 +the following derived constructions are automatically provided for any
3.1981 +datatype.
3.1982 +
3.1983 +\subsubsection{The \sdx{case} construct}
3.1984 +
3.1985 +The type comes with an \ML-like \texttt{case}-construct:
3.1986 +\[
3.1987 +\begin{array}{rrcl}
3.1988 +\mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\
3.1989 + \vdots \\
3.1990 + \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}
3.1991 +\end{array}
3.1992 +\]
3.1993 +where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
3.1994 +\S\ref{subsec:prod-sum}.
3.1995 +\begin{warn}
3.1996 + All constructors must be present, their order is fixed, and nested patterns
3.1997 + are not supported (with the exception of tuples). Violating this
3.1998 + restriction results in strange error messages.
3.1999 +\end{warn}
3.2000 +
3.2001 +To perform case distinction on a goal containing a \texttt{case}-construct,
3.2002 +the theorem $t@j.$\texttt{split} is provided:
3.2003 +\[
3.2004 +\begin{array}{@{}rcl@{}}
3.2005 +P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&
3.2006 +\!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to
3.2007 + P(f@1~x@1\dots x@{m^j@1})) \\
3.2008 +&&\!\!\! ~\land~ \dots ~\land \\
3.2009 +&&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to
3.2010 + P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))
3.2011 +\end{array}
3.2012 +\]
3.2013 +where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
3.2014 +This theorem can be added to a simpset via \ttindex{addsplits}
3.2015 +(see~\S\ref{subsec:HOL:case:splitting}).
3.2016 +
3.2017 +\subsubsection{The function \cdx{size}}\label{sec:HOL:size}
3.2018 +
3.2019 +Theory \texttt{Arith} declares a generic function \texttt{size} of type
3.2020 +$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
3.2021 +by overloading according to the following scheme:
3.2022 +%%% FIXME: This formula is too big and is completely unreadable
3.2023 +\[
3.2024 +size(C^j@i~x@1~\dots~x@{m^j@i}) = \!
3.2025 +\left\{
3.2026 +\begin{array}{ll}
3.2027 +0 & \!\mbox{if $Rec^j@i = \emptyset$} \\
3.2028 +\!\!\begin{array}{l}
3.2029 +size~x@{r^j@{i,1}} + \cdots \\
3.2030 +\cdots + size~x@{r^j@{i,l^j@i}} + 1
3.2031 +\end{array} &
3.2032 + \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
3.2033 + \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$}
3.2034 +\end{array}
3.2035 +\right.
3.2036 +\]
3.2037 +where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the
3.2038 +size of a leaf is 0 and the size of a node is the sum of the sizes of its
3.2039 +subtrees ${}+1$.
3.2040 +
3.2041 +\subsection{Defining datatypes}
3.2042 +
3.2043 +The theory syntax for datatype definitions is shown in
3.2044 +Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
3.2045 +definition has to obey the rules stated in the previous section. As a result
3.2046 +the theory is extended with the new types, the constructors, and the theorems
3.2047 +listed in the previous section.
3.2048 +
3.2049 +\begin{figure}
3.2050 +\begin{rail}
3.2051 +datatype : 'datatype' typedecls;
3.2052 +
3.2053 +typedecls: ( newtype '=' (cons + '|') ) + 'and'
3.2054 + ;
3.2055 +newtype : typevarlist id ( () | '(' infix ')' )
3.2056 + ;
3.2057 +cons : name (argtype *) ( () | ( '(' mixfix ')' ) )
3.2058 + ;
3.2059 +argtype : id | tid | ('(' typevarlist id ')')
3.2060 + ;
3.2061 +\end{rail}
3.2062 +\caption{Syntax of datatype declarations}
3.2063 +\label{datatype-grammar}
3.2064 +\end{figure}
3.2065 +
3.2066 +Most of the theorems about datatypes become part of the default simpset and
3.2067 +you never need to see them again because the simplifier applies them
3.2068 +automatically. Only induction or exhaustion are usually invoked by hand.
3.2069 +\begin{ttdescription}
3.2070 +\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
3.2071 + applies structural induction on variable $x$ to subgoal $i$, provided the
3.2072 + type of $x$ is a datatype.
3.2073 +\item[\ttindexbold{mutual_induct_tac}
3.2074 + {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous
3.2075 + structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This
3.2076 + is the canonical way to prove properties of mutually recursive datatypes
3.2077 + such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as
3.2078 + \texttt{term}.
3.2079 +\end{ttdescription}
3.2080 +In some cases, induction is overkill and a case distinction over all
3.2081 +constructors of the datatype suffices.
3.2082 +\begin{ttdescription}
3.2083 +\item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$]
3.2084 + performs an exhaustive case analysis for the term $u$ whose type
3.2085 + must be a datatype. If the datatype has $k@j$ constructors
3.2086 + $C^j@1$, \dots $C^j@{k@j}$, subgoal $i$ is replaced by $k@j$ new subgoals which
3.2087 + contain the additional assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for
3.2088 + $i'=1$, $\dots$,~$k@j$.
3.2089 +\end{ttdescription}
3.2090 +
3.2091 +Note that induction is only allowed on free variables that should not occur
3.2092 +among the premises of the subgoal. Exhaustion applies to arbitrary terms.
3.2093 +
3.2094 +\bigskip
3.2095 +
3.2096 +
3.2097 +For the technically minded, we exhibit some more details. Processing the
3.2098 +theory file produces an \ML\ structure which, in addition to the usual
3.2099 +components, contains a structure named $t$ for each datatype $t$ defined in
3.2100 +the file. Each structure $t$ contains the following elements:
3.2101 +\begin{ttbox}
3.2102 +val distinct : thm list
3.2103 +val inject : thm list
3.2104 +val induct : thm
3.2105 +val exhaust : thm
3.2106 +val cases : thm list
3.2107 +val split : thm
3.2108 +val split_asm : thm
3.2109 +val recs : thm list
3.2110 +val size : thm list
3.2111 +val simps : thm list
3.2112 +\end{ttbox}
3.2113 +\texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}
3.2114 +and \texttt{split} contain the theorems
3.2115 +described above. For user convenience, \texttt{distinct} contains
3.2116 +inequalities in both directions. The reduction rules of the {\tt
3.2117 + case}-construct are in \texttt{cases}. All theorems from {\tt
3.2118 + distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.
3.2119 +In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
3.2120 +and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
3.2121 +
3.2122 +
3.2123 +\subsection{Representing existing types as datatypes}
3.2124 +
3.2125 +For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
3.2126 + +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
3.2127 +but by more primitive means using \texttt{typedef}. To be able to use the
3.2128 +tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by
3.2129 +primitive recursion on these types, such types may be represented as actual
3.2130 +datatypes. This is done by specifying an induction rule, as well as theorems
3.2131 +stating the distinctness and injectivity of constructors in a {\tt
3.2132 + rep_datatype} section. For type \texttt{nat} this works as follows:
3.2133 +\begin{ttbox}
3.2134 +rep_datatype nat
3.2135 + distinct Suc_not_Zero, Zero_not_Suc
3.2136 + inject Suc_Suc_eq
3.2137 + induct nat_induct
3.2138 +\end{ttbox}
3.2139 +The datatype package automatically derives additional theorems for recursion
3.2140 +and case combinators from these rules. Any of the basic HOL types mentioned
3.2141 +above are represented as datatypes. Try an induction on \texttt{bool}
3.2142 +today.
3.2143 +
3.2144 +
3.2145 +\subsection{Examples}
3.2146 +
3.2147 +\subsubsection{The datatype $\alpha~mylist$}
3.2148 +
3.2149 +We want to define a type $\alpha~mylist$. To do this we have to build a new
3.2150 +theory that contains the type definition. We start from the theory
3.2151 +\texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the
3.2152 +\texttt{List} theory of Isabelle/HOL.
3.2153 +\begin{ttbox}
3.2154 +MyList = Datatype +
3.2155 + datatype 'a mylist = Nil | Cons 'a ('a mylist)
3.2156 +end
3.2157 +\end{ttbox}
3.2158 +After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To
3.2159 +ease the induction applied below, we state the goal with $x$ quantified at the
3.2160 +object-level. This will be stripped later using \ttindex{qed_spec_mp}.
3.2161 +\begin{ttbox}
3.2162 +Goal "!x. Cons x xs ~= xs";
3.2163 +{\out Level 0}
3.2164 +{\out ! x. Cons x xs ~= xs}
3.2165 +{\out 1. ! x. Cons x xs ~= xs}
3.2166 +\end{ttbox}
3.2167 +This can be proved by the structural induction tactic:
3.2168 +\begin{ttbox}
3.2169 +by (induct_tac "xs" 1);
3.2170 +{\out Level 1}
3.2171 +{\out ! x. Cons x xs ~= xs}
3.2172 +{\out 1. ! x. Cons x Nil ~= Nil}
3.2173 +{\out 2. !!a mylist.}
3.2174 +{\out ! x. Cons x mylist ~= mylist ==>}
3.2175 +{\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
3.2176 +\end{ttbox}
3.2177 +The first subgoal can be proved using the simplifier. Isabelle/HOL has
3.2178 +already added the freeness properties of lists to the default simplification
3.2179 +set.
3.2180 +\begin{ttbox}
3.2181 +by (Simp_tac 1);
3.2182 +{\out Level 2}
3.2183 +{\out ! x. Cons x xs ~= xs}
3.2184 +{\out 1. !!a mylist.}
3.2185 +{\out ! x. Cons x mylist ~= mylist ==>}
3.2186 +{\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
3.2187 +\end{ttbox}
3.2188 +Similarly, we prove the remaining goal.
3.2189 +\begin{ttbox}
3.2190 +by (Asm_simp_tac 1);
3.2191 +{\out Level 3}
3.2192 +{\out ! x. Cons x xs ~= xs}
3.2193 +{\out No subgoals!}
3.2194 +\ttbreak
3.2195 +qed_spec_mp "not_Cons_self";
3.2196 +{\out val not_Cons_self = "Cons x xs ~= xs" : thm}
3.2197 +\end{ttbox}
3.2198 +Because both subgoals could have been proved by \texttt{Asm_simp_tac}
3.2199 +we could have done that in one step:
3.2200 +\begin{ttbox}
3.2201 +by (ALLGOALS Asm_simp_tac);
3.2202 +\end{ttbox}
3.2203 +
3.2204 +
3.2205 +\subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}
3.2206 +
3.2207 +In this example we define the type $\alpha~mylist$ again but this time
3.2208 +we want to write \texttt{[]} for \texttt{Nil} and we want to use infix
3.2209 +notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix
3.2210 +annotations after the constructor declarations as follows:
3.2211 +\begin{ttbox}
3.2212 +MyList = Datatype +
3.2213 + datatype 'a mylist =
3.2214 + Nil ("[]") |
3.2215 + Cons 'a ('a mylist) (infixr "#" 70)
3.2216 +end
3.2217 +\end{ttbox}
3.2218 +Now the theorem in the previous example can be written \verb|x#xs ~= xs|.
3.2219 +
3.2220 +
3.2221 +\subsubsection{A datatype for weekdays}
3.2222 +
3.2223 +This example shows a datatype that consists of 7 constructors:
3.2224 +\begin{ttbox}
3.2225 +Days = Main +
3.2226 + datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
3.2227 +end
3.2228 +\end{ttbox}
3.2229 +Because there are more than 6 constructors, inequality is expressed via a function
3.2230 +\verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly
3.2231 +contained among the distinctness theorems, but the simplifier can
3.2232 +prove it thanks to rewrite rules inherited from theory \texttt{Arith}:
3.2233 +\begin{ttbox}
3.2234 +Goal "Mon ~= Tue";
3.2235 +by (Simp_tac 1);
3.2236 +\end{ttbox}
3.2237 +You need not derive such inequalities explicitly: the simplifier will dispose
3.2238 +of them automatically.
3.2239 +\index{*datatype|)}
3.2240 +
3.2241 +
3.2242 +\section{Recursive function definitions}\label{sec:HOL:recursive}
3.2243 +\index{recursive functions|see{recursion}}
3.2244 +
3.2245 +Isabelle/HOL provides two main mechanisms of defining recursive functions.
3.2246 +\begin{enumerate}
3.2247 +\item \textbf{Primitive recursion} is available only for datatypes, and it is
3.2248 + somewhat restrictive. Recursive calls are only allowed on the argument's
3.2249 + immediate constituents. On the other hand, it is the form of recursion most
3.2250 + often wanted, and it is easy to use.
3.2251 +
3.2252 +\item \textbf{Well-founded recursion} requires that you supply a well-founded
3.2253 + relation that governs the recursion. Recursive calls are only allowed if
3.2254 + they make the argument decrease under the relation. Complicated recursion
3.2255 + forms, such as nested recursion, can be dealt with. Termination can even be
3.2256 + proved at a later time, though having unsolved termination conditions around
3.2257 + can make work difficult.%
3.2258 + \footnote{This facility is based on Konrad Slind's TFL
3.2259 + package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
3.2260 + and assisting with its installation.}
3.2261 +\end{enumerate}
3.2262 +
3.2263 +Following good HOL tradition, these declarations do not assert arbitrary
3.2264 +axioms. Instead, they define the function using a recursion operator. Both
3.2265 +HOL and ZF derive the theory of well-founded recursion from first
3.2266 +principles~\cite{paulson-set-II}. Primitive recursion over some datatype
3.2267 +relies on the recursion operator provided by the datatype package. With
3.2268 +either form of function definition, Isabelle proves the desired recursion
3.2269 +equations as theorems.
3.2270 +
3.2271 +
3.2272 +\subsection{Primitive recursive functions}
3.2273 +\label{sec:HOL:primrec}
3.2274 +\index{recursion!primitive|(}
3.2275 +\index{*primrec|(}
3.2276 +
3.2277 +Datatypes come with a uniform way of defining functions, {\bf primitive
3.2278 + recursion}. In principle, one could introduce primitive recursive functions
3.2279 +by asserting their reduction rules as new axioms, but this is not recommended:
3.2280 +\begin{ttbox}\slshape
3.2281 +Append = Main +
3.2282 +consts app :: ['a list, 'a list] => 'a list
3.2283 +rules
3.2284 + app_Nil "app [] ys = ys"
3.2285 + app_Cons "app (x#xs) ys = x#app xs ys"
3.2286 +end
3.2287 +\end{ttbox}
3.2288 +Asserting axioms brings the danger of accidentally asserting nonsense, as
3.2289 +in \verb$app [] ys = us$.
3.2290 +
3.2291 +The \ttindex{primrec} declaration is a safe means of defining primitive
3.2292 +recursive functions on datatypes:
3.2293 +\begin{ttbox}
3.2294 +Append = Main +
3.2295 +consts app :: ['a list, 'a list] => 'a list
3.2296 +primrec
3.2297 + "app [] ys = ys"
3.2298 + "app (x#xs) ys = x#app xs ys"
3.2299 +end
3.2300 +\end{ttbox}
3.2301 +Isabelle will now check that the two rules do indeed form a primitive
3.2302 +recursive definition. For example
3.2303 +\begin{ttbox}
3.2304 +primrec
3.2305 + "app [] ys = us"
3.2306 +\end{ttbox}
3.2307 +is rejected with an error message ``\texttt{Extra variables on rhs}''.
3.2308 +
3.2309 +\bigskip
3.2310 +
3.2311 +The general form of a primitive recursive definition is
3.2312 +\begin{ttbox}
3.2313 +primrec
3.2314 + {\it reduction rules}
3.2315 +\end{ttbox}
3.2316 +where \textit{reduction rules} specify one or more equations of the form
3.2317 +\[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
3.2318 +\dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
3.2319 +contains only the free variables on the left-hand side, and all recursive
3.2320 +calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
3.2321 +must be at most one reduction rule for each constructor. The order is
3.2322 +immaterial. For missing constructors, the function is defined to return a
3.2323 +default value.
3.2324 +
3.2325 +If you would like to refer to some rule by name, then you must prefix
3.2326 +the rule with an identifier. These identifiers, like those in the
3.2327 +\texttt{rules} section of a theory, will be visible at the \ML\ level.
3.2328 +
3.2329 +The primitive recursive function can have infix or mixfix syntax:
3.2330 +\begin{ttbox}\underscoreon
3.2331 +consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
3.2332 +primrec
3.2333 + "[] @ ys = ys"
3.2334 + "(x#xs) @ ys = x#(xs @ ys)"
3.2335 +\end{ttbox}
3.2336 +
3.2337 +The reduction rules become part of the default simpset, which
3.2338 +leads to short proof scripts:
3.2339 +\begin{ttbox}\underscoreon
3.2340 +Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
3.2341 +by (induct\_tac "xs" 1);
3.2342 +by (ALLGOALS Asm\_simp\_tac);
3.2343 +\end{ttbox}
3.2344 +
3.2345 +\subsubsection{Example: Evaluation of expressions}
3.2346 +Using mutual primitive recursion, we can define evaluation functions \texttt{eval_aexp}
3.2347 +and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
3.2348 +\S\ref{subsec:datatype:basics}:
3.2349 +\begin{ttbox}
3.2350 +consts
3.2351 + eval_aexp :: "['a => nat, 'a aexp] => nat"
3.2352 + eval_bexp :: "['a => nat, 'a bexp] => bool"
3.2353 +
3.2354 +primrec
3.2355 + "eval_aexp env (If_then_else b a1 a2) =
3.2356 + (if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)"
3.2357 + "eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2"
3.2358 + "eval_aexp env (Diff a1 a2) = eval_aexp env a1 - eval_aexp env a2"
3.2359 + "eval_aexp env (Var v) = env v"
3.2360 + "eval_aexp env (Num n) = n"
3.2361 +
3.2362 + "eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)"
3.2363 + "eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
3.2364 + "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
3.2365 +\end{ttbox}
3.2366 +Since the value of an expression depends on the value of its variables,
3.2367 +the functions \texttt{eval_aexp} and \texttt{eval_bexp} take an additional
3.2368 +parameter, an {\em environment} of type \texttt{'a => nat}, which maps
3.2369 +variables to their values.
3.2370 +
3.2371 +Similarly, we may define substitution functions \texttt{subst_aexp}
3.2372 +and \texttt{subst_bexp} for expressions: The mapping \texttt{f} of type
3.2373 +\texttt{'a => 'a aexp} given as a parameter is lifted canonically
3.2374 +on the types {'a aexp} and {'a bexp}:
3.2375 +\begin{ttbox}
3.2376 +consts
3.2377 + subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp"
3.2378 + subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp"
3.2379 +
3.2380 +primrec
3.2381 + "subst_aexp f (If_then_else b a1 a2) =
3.2382 + If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)"
3.2383 + "subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)"
3.2384 + "subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)"
3.2385 + "subst_aexp f (Var v) = f v"
3.2386 + "subst_aexp f (Num n) = Num n"
3.2387 +
3.2388 + "subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)"
3.2389 + "subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)"
3.2390 + "subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)"
3.2391 +\end{ttbox}
3.2392 +In textbooks about semantics one often finds {\em substitution theorems},
3.2393 +which express the relationship between substitution and evaluation. For
3.2394 +\texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
3.2395 +induction, followed by simplification:
3.2396 +\begin{ttbox}
3.2397 +Goal
3.2398 + "eval_aexp env (subst_aexp (Var(v := a')) a) =
3.2399 + eval_aexp (env(v := eval_aexp env a')) a &
3.2400 + eval_bexp env (subst_bexp (Var(v := a')) b) =
3.2401 + eval_bexp (env(v := eval_aexp env a')) b";
3.2402 +by (mutual_induct_tac ["a","b"] 1);
3.2403 +by (ALLGOALS Asm_full_simp_tac);
3.2404 +\end{ttbox}
3.2405 +
3.2406 +\subsubsection{Example: A substitution function for terms}
3.2407 +Functions on datatypes with nested recursion, such as the type
3.2408 +\texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are
3.2409 +also defined by mutual primitive recursion. A substitution
3.2410 +function \texttt{subst_term} on type \texttt{term}, similar to the functions
3.2411 +\texttt{subst_aexp} and \texttt{subst_bexp} described above, can
3.2412 +be defined as follows:
3.2413 +\begin{ttbox}
3.2414 +consts
3.2415 + subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
3.2416 + subst_term_list ::
3.2417 + "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
3.2418 +
3.2419 +primrec
3.2420 + "subst_term f (Var a) = f a"
3.2421 + "subst_term f (App b ts) = App b (subst_term_list f ts)"
3.2422 +
3.2423 + "subst_term_list f [] = []"
3.2424 + "subst_term_list f (t # ts) =
3.2425 + subst_term f t # subst_term_list f ts"
3.2426 +\end{ttbox}
3.2427 +The recursion scheme follows the structure of the unfolded definition of type
3.2428 +\texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
3.2429 +this substitution function, mutual induction is needed:
3.2430 +\begin{ttbox}
3.2431 +Goal
3.2432 + "(subst_term ((subst_term f1) o f2) t) =
3.2433 + (subst_term f1 (subst_term f2 t)) &
3.2434 + (subst_term_list ((subst_term f1) o f2) ts) =
3.2435 + (subst_term_list f1 (subst_term_list f2 ts))";
3.2436 +by (mutual_induct_tac ["t", "ts"] 1);
3.2437 +by (ALLGOALS Asm_full_simp_tac);
3.2438 +\end{ttbox}
3.2439 +
3.2440 +\index{recursion!primitive|)}
3.2441 +\index{*primrec|)}
3.2442 +
3.2443 +
3.2444 +\subsection{General recursive functions}
3.2445 +\label{sec:HOL:recdef}
3.2446 +\index{recursion!general|(}
3.2447 +\index{*recdef|(}
3.2448 +
3.2449 +Using \texttt{recdef}, you can declare functions involving nested recursion
3.2450 +and pattern-matching. Recursion need not involve datatypes and there are few
3.2451 +syntactic restrictions. Termination is proved by showing that each recursive
3.2452 +call makes the argument smaller in a suitable sense, which you specify by
3.2453 +supplying a well-founded relation.
3.2454 +
3.2455 +Here is a simple example, the Fibonacci function. The first line declares
3.2456 +\texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on
3.2457 +the natural numbers). Pattern-matching is used here: \texttt{1} is a
3.2458 +macro for \texttt{Suc~0}.
3.2459 +\begin{ttbox}
3.2460 +consts fib :: "nat => nat"
3.2461 +recdef fib "less_than"
3.2462 + "fib 0 = 0"
3.2463 + "fib 1 = 1"
3.2464 + "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
3.2465 +\end{ttbox}
3.2466 +
3.2467 +With \texttt{recdef}, function definitions may be incomplete, and patterns may
3.2468 +overlap, as in functional programming. The \texttt{recdef} package
3.2469 +disambiguates overlapping patterns by taking the order of rules into account.
3.2470 +For missing patterns, the function is defined to return a default value.
3.2471 +
3.2472 +%For example, here is a declaration of the list function \cdx{hd}:
3.2473 +%\begin{ttbox}
3.2474 +%consts hd :: 'a list => 'a
3.2475 +%recdef hd "\{\}"
3.2476 +% "hd (x#l) = x"
3.2477 +%\end{ttbox}
3.2478 +%Because this function is not recursive, we may supply the empty well-founded
3.2479 +%relation, $\{\}$.
3.2480 +
3.2481 +The well-founded relation defines a notion of ``smaller'' for the function's
3.2482 +argument type. The relation $\prec$ is \textbf{well-founded} provided it
3.2483 +admits no infinitely decreasing chains
3.2484 +\[ \cdots\prec x@n\prec\cdots\prec x@1. \]
3.2485 +If the function's argument has type~$\tau$, then $\prec$ has to be a relation
3.2486 +over~$\tau$: it must have type $(\tau\times\tau)set$.
3.2487 +
3.2488 +Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection
3.2489 +of operators for building well-founded relations. The package recognises
3.2490 +these operators and automatically proves that the constructed relation is
3.2491 +well-founded. Here are those operators, in order of importance:
3.2492 +\begin{itemize}
3.2493 +\item \texttt{less_than} is ``less than'' on the natural numbers.
3.2494 + (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.
3.2495 +
3.2496 +\item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the
3.2497 + relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$.
3.2498 + Typically, $f$ takes the recursive function's arguments (as a tuple) and
3.2499 + returns a result expressed in terms of the function \texttt{size}. It is
3.2500 + called a \textbf{measure function}. Recall that \texttt{size} is overloaded
3.2501 + and is defined on all datatypes (see \S\ref{sec:HOL:size}).
3.2502 +
3.2503 +\item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
3.2504 + \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$
3.2505 + is less than $f(y)$ according to~$R$, which must itself be a well-founded
3.2506 + relation.
3.2507 +
3.2508 +\item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It
3.2509 + is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$
3.2510 + is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$
3.2511 + is less than $y@2$ according to~$R@2$.
3.2512 +
3.2513 +\item \texttt{finite_psubset} is the proper subset relation on finite sets.
3.2514 +\end{itemize}
3.2515 +
3.2516 +We can use \texttt{measure} to declare Euclid's algorithm for the greatest
3.2517 +common divisor. The measure function, $\lambda(m,n). n$, specifies that the
3.2518 +recursion terminates because argument~$n$ decreases.
3.2519 +\begin{ttbox}
3.2520 +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
3.2521 + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
3.2522 +\end{ttbox}
3.2523 +
3.2524 +The general form of a well-founded recursive definition is
3.2525 +\begin{ttbox}
3.2526 +recdef {\it function} {\it rel}
3.2527 + congs {\it congruence rules} {\bf(optional)}
3.2528 + simpset {\it simplification set} {\bf(optional)}
3.2529 + {\it reduction rules}
3.2530 +\end{ttbox}
3.2531 +where
3.2532 +\begin{itemize}
3.2533 +\item \textit{function} is the name of the function, either as an \textit{id}
3.2534 + or a \textit{string}.
3.2535 +
3.2536 +\item \textit{rel} is a {\HOL} expression for the well-founded termination
3.2537 + relation.
3.2538 +
3.2539 +\item \textit{congruence rules} are required only in highly exceptional
3.2540 + circumstances.
3.2541 +
3.2542 +\item The \textit{simplification set} is used to prove that the supplied
3.2543 + relation is well-founded. It is also used to prove the \textbf{termination
3.2544 + conditions}: assertions that arguments of recursive calls decrease under
3.2545 + \textit{rel}. By default, simplification uses \texttt{simpset()}, which
3.2546 + is sufficient to prove well-foundedness for the built-in relations listed
3.2547 + above.
3.2548 +
3.2549 +\item \textit{reduction rules} specify one or more recursion equations. Each
3.2550 + left-hand side must have the form $f\,t$, where $f$ is the function and $t$
3.2551 + is a tuple of distinct variables. If more than one equation is present then
3.2552 + $f$ is defined by pattern-matching on components of its argument whose type
3.2553 + is a \texttt{datatype}.
3.2554 +
3.2555 + Unlike with \texttt{primrec}, the reduction rules are not added to the
3.2556 + default simpset, and individual rules may not be labelled with identifiers.
3.2557 + However, the identifier $f$\texttt{.rules} is visible at the \ML\ level
3.2558 + as a list of theorems.
3.2559 +\end{itemize}
3.2560 +
3.2561 +With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
3.2562 +prove one termination condition. It remains as a precondition of the
3.2563 +recursion theorems.
3.2564 +\begin{ttbox}
3.2565 +gcd.rules;
3.2566 +{\out ["! m n. n ~= 0 --> m mod n < n}
3.2567 +{\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] }
3.2568 +{\out : thm list}
3.2569 +\end{ttbox}
3.2570 +The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
3.2571 +conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard
3.2572 +function \texttt{goalw}, which sets up a goal to prove, but its argument
3.2573 +should be the identifier $f$\texttt{.rules} and its effect is to set up a
3.2574 +proof of the termination conditions:
3.2575 +\begin{ttbox}
3.2576 +Tfl.tgoalw thy [] gcd.rules;
3.2577 +{\out Level 0}
3.2578 +{\out ! m n. n ~= 0 --> m mod n < n}
3.2579 +{\out 1. ! m n. n ~= 0 --> m mod n < n}
3.2580 +\end{ttbox}
3.2581 +This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem
3.2582 +is proved, it can be used to eliminate the termination conditions from
3.2583 +elements of \texttt{gcd.rules}. Theory \texttt{HOL/Subst/Unify} is a much
3.2584 +more complicated example of this process, where the termination conditions can
3.2585 +only be proved by complicated reasoning involving the recursive function
3.2586 +itself.
3.2587 +
3.2588 +Isabelle/HOL can prove the \texttt{gcd} function's termination condition
3.2589 +automatically if supplied with the right simpset.
3.2590 +\begin{ttbox}
3.2591 +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
3.2592 + simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"
3.2593 + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
3.2594 +\end{ttbox}
3.2595 +
3.2596 +A \texttt{recdef} definition also returns an induction rule specialised for
3.2597 +the recursive function. For the \texttt{gcd} function above, the induction
3.2598 +rule is
3.2599 +\begin{ttbox}
3.2600 +gcd.induct;
3.2601 +{\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}
3.2602 +\end{ttbox}
3.2603 +This rule should be used to reason inductively about the \texttt{gcd}
3.2604 +function. It usually makes the induction hypothesis available at all
3.2605 +recursive calls, leading to very direct proofs. If any termination conditions
3.2606 +remain unproved, they will become additional premises of this rule.
3.2607 +
3.2608 +\index{recursion!general|)}
3.2609 +\index{*recdef|)}
3.2610 +
3.2611 +
3.2612 +\section{Inductive and coinductive definitions}
3.2613 +\index{*inductive|(}
3.2614 +\index{*coinductive|(}
3.2615 +
3.2616 +An {\bf inductive definition} specifies the least set~$R$ closed under given
3.2617 +rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For
3.2618 +example, a structural operational semantics is an inductive definition of an
3.2619 +evaluation relation. Dually, a {\bf coinductive definition} specifies the
3.2620 +greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
3.2621 +seen as arising by applying a rule to elements of~$R$.) An important example
3.2622 +is using bisimulation relations to formalise equivalence of processes and
3.2623 +infinite data structures.
3.2624 +
3.2625 +A theory file may contain any number of inductive and coinductive
3.2626 +definitions. They may be intermixed with other declarations; in
3.2627 +particular, the (co)inductive sets {\bf must} be declared separately as
3.2628 +constants, and may have mixfix syntax or be subject to syntax translations.
3.2629 +
3.2630 +Each (co)inductive definition adds definitions to the theory and also
3.2631 +proves some theorems. Each definition creates an \ML\ structure, which is a
3.2632 +substructure of the main theory structure.
3.2633 +
3.2634 +This package is related to the \ZF\ one, described in a separate
3.2635 +paper,%
3.2636 +\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
3.2637 + distributed with Isabelle.} %
3.2638 +which you should refer to in case of difficulties. The package is simpler
3.2639 +than \ZF's thanks to \HOL's extra-logical automatic type-checking. The types
3.2640 +of the (co)inductive sets determine the domain of the fixedpoint definition,
3.2641 +and the package does not have to use inference rules for type-checking.
3.2642 +
3.2643 +
3.2644 +\subsection{The result structure}
3.2645 +Many of the result structure's components have been discussed in the paper;
3.2646 +others are self-explanatory.
3.2647 +\begin{description}
3.2648 +\item[\tt defs] is the list of definitions of the recursive sets.
3.2649 +
3.2650 +\item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
3.2651 +
3.2652 +\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
3.2653 +the recursive sets, in the case of mutual recursion).
3.2654 +
3.2655 +\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
3.2656 +the recursive sets. The rules are also available individually, using the
3.2657 +names given them in the theory file.
3.2658 +
3.2659 +\item[\tt elims] is the list of elimination rule.
3.2660 +
3.2661 +\item[\tt elim] is the head of the list \texttt{elims}.
3.2662 +
3.2663 +\item[\tt mk_cases] is a function to create simplified instances of {\tt
3.2664 +elim} using freeness reasoning on underlying datatypes.
3.2665 +\end{description}
3.2666 +
3.2667 +For an inductive definition, the result structure contains the
3.2668 +rule \texttt{induct}. For a
3.2669 +coinductive definition, it contains the rule \verb|coinduct|.
3.2670 +
3.2671 +Figure~\ref{def-result-fig} summarises the two result signatures,
3.2672 +specifying the types of all these components.
3.2673 +
3.2674 +\begin{figure}
3.2675 +\begin{ttbox}
3.2676 +sig
3.2677 +val defs : thm list
3.2678 +val mono : thm
3.2679 +val unfold : thm
3.2680 +val intrs : thm list
3.2681 +val elims : thm list
3.2682 +val elim : thm
3.2683 +val mk_cases : string -> thm
3.2684 +{\it(Inductive definitions only)}
3.2685 +val induct : thm
3.2686 +{\it(coinductive definitions only)}
3.2687 +val coinduct : thm
3.2688 +end
3.2689 +\end{ttbox}
3.2690 +\hrule
3.2691 +\caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}
3.2692 +\end{figure}
3.2693 +
3.2694 +\subsection{The syntax of a (co)inductive definition}
3.2695 +An inductive definition has the form
3.2696 +\begin{ttbox}
3.2697 +inductive {\it inductive sets}
3.2698 + intrs {\it introduction rules}
3.2699 + monos {\it monotonicity theorems}
3.2700 + con_defs {\it constructor definitions}
3.2701 +\end{ttbox}
3.2702 +A coinductive definition is identical, except that it starts with the keyword
3.2703 +\texttt{coinductive}.
3.2704 +
3.2705 +The \texttt{monos} and \texttt{con_defs} sections are optional. If present,
3.2706 +each is specified by a list of identifiers.
3.2707 +
3.2708 +\begin{itemize}
3.2709 +\item The \textit{inductive sets} are specified by one or more strings.
3.2710 +
3.2711 +\item The \textit{introduction rules} specify one or more introduction rules in
3.2712 + the form \textit{ident\/}~\textit{string}, where the identifier gives the name of
3.2713 + the rule in the result structure.
3.2714 +
3.2715 +\item The \textit{monotonicity theorems} are required for each operator
3.2716 + applied to a recursive set in the introduction rules. There {\bf must}
3.2717 + be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
3.2718 + premise $t\in M(R@i)$ in an introduction rule!
3.2719 +
3.2720 +\item The \textit{constructor definitions} contain definitions of constants
3.2721 + appearing in the introduction rules. In most cases it can be omitted.
3.2722 +\end{itemize}
3.2723 +
3.2724 +
3.2725 +\subsection{Example of an inductive definition}
3.2726 +Two declarations, included in a theory file, define the finite powerset
3.2727 +operator. First we declare the constant~\texttt{Fin}. Then we declare it
3.2728 +inductively, with two introduction rules:
3.2729 +\begin{ttbox}
3.2730 +consts Fin :: 'a set => 'a set set
3.2731 +inductive "Fin A"
3.2732 + intrs
3.2733 + emptyI "{\ttlbrace}{\ttrbrace} : Fin A"
3.2734 + insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A"
3.2735 +\end{ttbox}
3.2736 +The resulting theory structure contains a substructure, called~\texttt{Fin}.
3.2737 +It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
3.2738 +and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction
3.2739 +rule is \texttt{Fin.induct}.
3.2740 +
3.2741 +For another example, here is a theory file defining the accessible
3.2742 +part of a relation. The main thing to note is the use of~\texttt{Pow} in
3.2743 +the sole introduction rule, and the corresponding mention of the rule
3.2744 +\verb|Pow_mono| in the \texttt{monos} list. The paper
3.2745 +\cite{paulson-CADE} discusses a \ZF\ version of this example in more
3.2746 +detail.
3.2747 +\begin{ttbox}
3.2748 +Acc = WF +
3.2749 +consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
3.2750 + acc :: "('a * 'a)set => 'a set" (*Accessible part*)
3.2751 +defs pred_def "pred x r == {y. (y,x):r}"
3.2752 +inductive "acc r"
3.2753 + intrs
3.2754 + pred "pred a r: Pow(acc r) ==> a: acc r"
3.2755 + monos Pow_mono
3.2756 +end
3.2757 +\end{ttbox}
3.2758 +The Isabelle distribution contains many other inductive definitions. Simple
3.2759 +examples are collected on subdirectory \texttt{HOL/Induct}. The theory
3.2760 +\texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples
3.2761 +may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP},
3.2762 +\texttt{Lambda} and \texttt{Auth}.
3.2763 +
3.2764 +\index{*coinductive|)} \index{*inductive|)}
3.2765 +
3.2766 +
3.2767 +\section{The examples directories}
3.2768 +
3.2769 +Directory \texttt{HOL/Auth} contains theories for proving the correctness of
3.2770 +cryptographic protocols. The approach is based upon operational
3.2771 +semantics~\cite{paulson-security} rather than the more usual belief logics.
3.2772 +On the same directory are proofs for some standard examples, such as the
3.2773 +Needham-Schroeder public-key authentication protocol~\cite{paulson-ns}
3.2774 +and the Otway-Rees protocol.
3.2775 +
3.2776 +Directory \texttt{HOL/IMP} contains a formalization of various denotational,
3.2777 +operational and axiomatic semantics of a simple while-language, the necessary
3.2778 +equivalence proofs, soundness and completeness of the Hoare rules with respect
3.2779 +to the
3.2780 +denotational semantics, and soundness and completeness of a verification
3.2781 +condition generator. Much of development is taken from
3.2782 +Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
3.2783 +
3.2784 +Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
3.2785 +logic, including a tactic for generating verification-conditions.
3.2786 +
3.2787 +Directory \texttt{HOL/MiniML} contains a formalization of the type system of the
3.2788 +core functional language Mini-ML and a correctness proof for its type
3.2789 +inference algorithm $\cal W$~\cite{milner78,nazareth-nipkow}.
3.2790 +
3.2791 +Directory \texttt{HOL/Lambda} contains a formalization of untyped
3.2792 +$\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
3.2793 +and $\eta$ reduction~\cite{Nipkow-CR}.
3.2794 +
3.2795 +Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of
3.2796 +substitutions and unifiers. It is based on Paulson's previous
3.2797 +mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
3.2798 +theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef},
3.2799 +with nested recursion.
3.2800 +
3.2801 +Directory \texttt{HOL/Induct} presents simple examples of (co)inductive
3.2802 +definitions and datatypes.
3.2803 +\begin{itemize}
3.2804 +\item Theory \texttt{PropLog} proves the soundness and completeness of
3.2805 + classical propositional logic, given a truth table semantics. The only
3.2806 + connective is $\imp$. A Hilbert-style axiom system is specified, and its
3.2807 + set of theorems defined inductively. A similar proof in \ZF{} is
3.2808 + described elsewhere~\cite{paulson-set-II}.
3.2809 +
3.2810 +\item Theory \texttt{Term} defines the datatype \texttt{term}.
3.2811 +
3.2812 +\item Theory \texttt{ABexp} defines arithmetic and boolean expressions
3.2813 + as mutually recursive datatypes.
3.2814 +
3.2815 +\item The definition of lazy lists demonstrates methods for handling
3.2816 + infinite data structures and coinduction in higher-order
3.2817 + logic~\cite{paulson-coind}.%
3.2818 +\footnote{To be precise, these lists are \emph{potentially infinite} rather
3.2819 + than lazy. Lazy implies a particular operational semantics.}
3.2820 + Theory \thydx{LList} defines an operator for
3.2821 + corecursion on lazy lists, which is used to define a few simple functions
3.2822 + such as map and append. A coinduction principle is defined
3.2823 + for proving equations on lazy lists.
3.2824 +
3.2825 +\item Theory \thydx{LFilter} defines the filter functional for lazy lists.
3.2826 + This functional is notoriously difficult to define because finding the next
3.2827 + element meeting the predicate requires possibly unlimited search. It is not
3.2828 + computable, but can be expressed using a combination of induction and
3.2829 + corecursion.
3.2830 +
3.2831 +\item Theory \thydx{Exp} illustrates the use of iterated inductive definitions
3.2832 + to express a programming language semantics that appears to require mutual
3.2833 + induction. Iterated induction allows greater modularity.
3.2834 +\end{itemize}
3.2835 +
3.2836 +Directory \texttt{HOL/ex} contains other examples and experimental proofs in
3.2837 +{\HOL}.
3.2838 +\begin{itemize}
3.2839 +\item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}
3.2840 + to define recursive functions. Another example is \texttt{Fib}, which
3.2841 + defines the Fibonacci function.
3.2842 +
3.2843 +\item Theory \texttt{Primes} defines the Greatest Common Divisor of two
3.2844 + natural numbers and proves a key lemma of the Fundamental Theorem of
3.2845 + Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$
3.2846 + or $p$ divides~$n$.
3.2847 +
3.2848 +\item Theory \texttt{Primrec} develops some computation theory. It
3.2849 + inductively defines the set of primitive recursive functions and presents a
3.2850 + proof that Ackermann's function is not primitive recursive.
3.2851 +
3.2852 +\item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty
3.2853 + predicate calculus theorems, ranging from simple tautologies to
3.2854 + moderately difficult problems involving equality and quantifiers.
3.2855 +
3.2856 +\item File \texttt{meson.ML} contains an experimental implementation of the {\sc
3.2857 + meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
3.2858 + much more powerful than Isabelle's classical reasoner. But it is less
3.2859 + useful in practice because it works only for pure logic; it does not
3.2860 + accept derived rules for the set theory primitives, for example.
3.2861 +
3.2862 +\item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof
3.2863 + procedure. These are mostly taken from Pelletier \cite{pelletier86}.
3.2864 +
3.2865 +\item File \texttt{set.ML} proves Cantor's Theorem, which is presented in
3.2866 + \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
3.2867 +
3.2868 +\item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of
3.2869 + Milner and Tofte's coinduction example~\cite{milner-coind}. This
3.2870 + substantial proof concerns the soundness of a type system for a simple
3.2871 + functional language. The semantics of recursion is given by a cyclic
3.2872 + environment, which makes a coinductive argument appropriate.
3.2873 +\end{itemize}
3.2874 +
3.2875 +
3.2876 +\goodbreak
3.2877 +\section{Example: Cantor's Theorem}\label{sec:hol-cantor}
3.2878 +Cantor's Theorem states that every set has more subsets than it has
3.2879 +elements. It has become a favourite example in higher-order logic since
3.2880 +it is so easily expressed:
3.2881 +\[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.
3.2882 + \forall x::\alpha. f~x \not= S
3.2883 +\]
3.2884 +%
3.2885 +Viewing types as sets, $\alpha\To bool$ represents the powerset
3.2886 +of~$\alpha$. This version states that for every function from $\alpha$ to
3.2887 +its powerset, some subset is outside its range.
3.2888 +
3.2889 +The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
3.2890 +the operator \cdx{range}.
3.2891 +\begin{ttbox}
3.2892 +context Set.thy;
3.2893 +\end{ttbox}
3.2894 +The set~$S$ is given as an unknown instead of a
3.2895 +quantified variable so that we may inspect the subset found by the proof.
3.2896 +\begin{ttbox}
3.2897 +Goal "?S ~: range\thinspace(f :: 'a=>'a set)";
3.2898 +{\out Level 0}
3.2899 +{\out ?S ~: range f}
3.2900 +{\out 1. ?S ~: range f}
3.2901 +\end{ttbox}
3.2902 +The first two steps are routine. The rule \tdx{rangeE} replaces
3.2903 +$\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$.
3.2904 +\begin{ttbox}
3.2905 +by (resolve_tac [notI] 1);
3.2906 +{\out Level 1}
3.2907 +{\out ?S ~: range f}
3.2908 +{\out 1. ?S : range f ==> False}
3.2909 +\ttbreak
3.2910 +by (eresolve_tac [rangeE] 1);
3.2911 +{\out Level 2}
3.2912 +{\out ?S ~: range f}
3.2913 +{\out 1. !!x. ?S = f x ==> False}
3.2914 +\end{ttbox}
3.2915 +Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,
3.2916 +we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for
3.2917 +any~$\Var{c}$.
3.2918 +\begin{ttbox}
3.2919 +by (eresolve_tac [equalityCE] 1);
3.2920 +{\out Level 3}
3.2921 +{\out ?S ~: range f}
3.2922 +{\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}
3.2923 +{\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}
3.2924 +\end{ttbox}
3.2925 +Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
3.2926 +comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies
3.2927 +$\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD}
3.2928 +instantiates~$\Var{S}$ and creates the new assumption.
3.2929 +\begin{ttbox}
3.2930 +by (dresolve_tac [CollectD] 1);
3.2931 +{\out Level 4}
3.2932 +{\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}
3.2933 +{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}
3.2934 +{\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}
3.2935 +\end{ttbox}
3.2936 +Forcing a contradiction between the two assumptions of subgoal~1
3.2937 +completes the instantiation of~$S$. It is now the set $\{x. x\not\in
3.2938 +f~x\}$, which is the standard diagonal construction.
3.2939 +\begin{ttbox}
3.2940 +by (contr_tac 1);
3.2941 +{\out Level 5}
3.2942 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3.2943 +{\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}
3.2944 +\end{ttbox}
3.2945 +The rest should be easy. To apply \tdx{CollectI} to the negated
3.2946 +assumption, we employ \ttindex{swap_res_tac}:
3.2947 +\begin{ttbox}
3.2948 +by (swap_res_tac [CollectI] 1);
3.2949 +{\out Level 6}
3.2950 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3.2951 +{\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}
3.2952 +\ttbreak
3.2953 +by (assume_tac 1);
3.2954 +{\out Level 7}
3.2955 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3.2956 +{\out No subgoals!}
3.2957 +\end{ttbox}
3.2958 +How much creativity is required? As it happens, Isabelle can prove this
3.2959 +theorem automatically. The default classical set \texttt{claset()} contains rules
3.2960 +for most of the constructs of \HOL's set theory. We must augment it with
3.2961 +\tdx{equalityCE} to break up set equalities, and then apply best-first
3.2962 +search. Depth-first search would diverge, but best-first search
3.2963 +successfully navigates through the large search space.
3.2964 +\index{search!best-first}
3.2965 +\begin{ttbox}
3.2966 +choplev 0;
3.2967 +{\out Level 0}
3.2968 +{\out ?S ~: range f}
3.2969 +{\out 1. ?S ~: range f}
3.2970 +\ttbreak
3.2971 +by (best_tac (claset() addSEs [equalityCE]) 1);
3.2972 +{\out Level 1}
3.2973 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
3.2974 +{\out No subgoals!}
3.2975 +\end{ttbox}
3.2976 +If you run this example interactively, make sure your current theory contains
3.2977 +theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.
3.2978 +Otherwise the default claset may not contain the rules for set theory.
3.2979 +\index{higher-order logic|)}
3.2980 +
3.2981 +%%% Local Variables:
3.2982 +%%% mode: latex
3.2983 +%%% TeX-master: "logics"
3.2984 +%%% End:
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/HOL/Makefile Tue May 04 18:03:56 1999 +0200
4.3 @@ -0,0 +1,34 @@
4.4 +# $Id$
4.5 +#########################################################################
4.6 +# #
4.7 +# Makefile for the report "Isabelle's Logics: HOL" #
4.8 +# #
4.9 +#########################################################################
4.10 +
4.11 +
4.12 +FILES = logics-HOL.tex ../Logics/syntax.tex FOL.tex HOL.tex\
4.13 + ../rail.sty ../proof.sty ../iman.sty ../extra.sty
4.14 +
4.15 +logics-HOL.dvi.gz: $(FILES)
4.16 + test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
4.17 + -rm logics-HOL.dvi*
4.18 + latex logics-HOL
4.19 + rail logics-HOL
4.20 + bibtex logics-HOL
4.21 + latex logics-HOL
4.22 + latex logics-HOL
4.23 + ../sedindex logics-HOL
4.24 + latex logics-HOL
4.25 + gzip -f logics-HOL.dvi
4.26 +
4.27 +dist: $(FILES)
4.28 + test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
4.29 + -rm logics-HOL.dvi*
4.30 + latex logics-HOL
4.31 + latex logics-HOL
4.32 + ../sedindex logics-HOL
4.33 + latex logics-HOL
4.34 +
4.35 +clean:
4.36 + @rm *.aux *.log *.toc *.idx *.rai
4.37 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/HOL/logics-HOL.ind Tue May 04 18:03:56 1999 +0200
5.3 @@ -0,0 +1,439 @@
5.4 +\begin{theindex}
5.5 +
5.6 + \item {\tt !} symbol, 4, 6, 13, 14, 26
5.7 + \item {\tt[]} symbol, 26
5.8 + \item {\tt\#} symbol, 26
5.9 + \item {\tt\&} symbol, 4
5.10 + \item {\tt *} symbol, 5, 23
5.11 + \item {\tt *} type, 21
5.12 + \item {\tt +} symbol, 5, 23
5.13 + \item {\tt +} type, 21
5.14 + \item {\tt -} symbol, 5, 23
5.15 + \item {\tt -->} symbol, 4
5.16 + \item {\tt :} symbol, 12
5.17 + \item {\tt <} constant, 24
5.18 + \item {\tt <} symbol, 23
5.19 + \item {\tt <=} constant, 24
5.20 + \item {\tt <=} symbol, 12
5.21 + \item {\tt =} symbol, 4
5.22 + \item {\tt ?} symbol, 4, 6, 13, 14
5.23 + \item {\tt ?!} symbol, 4
5.24 + \item {\tt\at} symbol, 4, 26
5.25 + \item {\tt ``} symbol, 12
5.26 + \item \verb'{}' symbol, 12
5.27 + \item {\tt |} symbol, 4
5.28 +
5.29 + \indexspace
5.30 +
5.31 + \item {\tt 0} constant, 23
5.32 +
5.33 + \indexspace
5.34 +
5.35 + \item {\tt Addsplits}, \bold{20}
5.36 + \item {\tt addsplits}, \bold{20}, 25, 37
5.37 + \item {\tt ALL} symbol, 4, 6, 13, 14
5.38 + \item {\tt All} constant, 4
5.39 + \item {\tt All_def} theorem, 8
5.40 + \item {\tt all_dupE} theorem, 10
5.41 + \item {\tt allE} theorem, 10
5.42 + \item {\tt allI} theorem, 10
5.43 + \item {\tt and_def} theorem, 8
5.44 + \item {\tt arg_cong} theorem, 9
5.45 + \item {\tt Arith} theory, 24
5.46 + \item {\tt arith_tac}, 25
5.47 +
5.48 + \indexspace
5.49 +
5.50 + \item {\tt Ball} constant, 12, 14
5.51 + \item {\tt Ball_def} theorem, 15
5.52 + \item {\tt ballE} theorem, 16
5.53 + \item {\tt ballI} theorem, 16
5.54 + \item {\tt Bex} constant, 12, 14
5.55 + \item {\tt Bex_def} theorem, 15
5.56 + \item {\tt bexCI} theorem, 14, 16
5.57 + \item {\tt bexE} theorem, 16
5.58 + \item {\tt bexI} theorem, 14, 16
5.59 + \item {\textit {bool}} type, 5
5.60 + \item {\tt box_equals} theorem, 9, 11
5.61 + \item {\tt bspec} theorem, 16
5.62 + \item {\tt butlast} constant, 26
5.63 +
5.64 + \indexspace
5.65 +
5.66 + \item {\tt case} symbol, 7, 24, 25, 37
5.67 + \item {\tt case_tac}, \bold{11}
5.68 + \item {\tt ccontr} theorem, 10
5.69 + \item {\tt classical} theorem, 10
5.70 + \item {\tt coinductive}, 49--51
5.71 + \item {\tt Collect} constant, 12, 14
5.72 + \item {\tt Collect_mem_eq} theorem, 14, 15
5.73 + \item {\tt CollectD} theorem, 16, 54
5.74 + \item {\tt CollectE} theorem, 16
5.75 + \item {\tt CollectI} theorem, 16, 55
5.76 + \item {\tt Compl} constant, 12
5.77 + \item {\tt Compl_def} theorem, 15
5.78 + \item {\tt Compl_disjoint} theorem, 18
5.79 + \item {\tt Compl_Int} theorem, 18
5.80 + \item {\tt Compl_partition} theorem, 18
5.81 + \item {\tt Compl_Un} theorem, 18
5.82 + \item {\tt ComplD} theorem, 17
5.83 + \item {\tt ComplI} theorem, 17
5.84 + \item {\tt concat} constant, 26
5.85 + \item {\tt cong} theorem, 9
5.86 + \item {\tt conj_cong}, 19
5.87 + \item {\tt conjE} theorem, 9
5.88 + \item {\tt conjI} theorem, 9
5.89 + \item {\tt conjunct1} theorem, 9
5.90 + \item {\tt conjunct2} theorem, 9
5.91 + \item {\tt context}, 55
5.92 +
5.93 + \indexspace
5.94 +
5.95 + \item {\tt datatype}, 34--42
5.96 + \item {\tt Delsplits}, \bold{20}
5.97 + \item {\tt delsplits}, \bold{20}
5.98 + \item {\tt disjCI} theorem, 10
5.99 + \item {\tt disjE} theorem, 9
5.100 + \item {\tt disjI1} theorem, 9
5.101 + \item {\tt disjI2} theorem, 9
5.102 + \item {\tt div} symbol, 23
5.103 + \item {\tt div_geq} theorem, 24
5.104 + \item {\tt div_less} theorem, 24
5.105 + \item {\tt Divides} theory, 24
5.106 + \item {\tt double_complement} theorem, 18
5.107 + \item {\tt drop} constant, 26
5.108 + \item {\tt dropWhile} constant, 26
5.109 +
5.110 + \indexspace
5.111 +
5.112 + \item {\tt empty_def} theorem, 15
5.113 + \item {\tt emptyE} theorem, 17
5.114 + \item {\tt Eps} constant, 4, 6
5.115 + \item {\tt equalityCE} theorem, 14, 16, 54, 55
5.116 + \item {\tt equalityD1} theorem, 16
5.117 + \item {\tt equalityD2} theorem, 16
5.118 + \item {\tt equalityE} theorem, 16
5.119 + \item {\tt equalityI} theorem, 16
5.120 + \item {\tt EX} symbol, 4, 6, 13, 14
5.121 + \item {\tt Ex} constant, 4
5.122 + \item {\tt EX!} symbol, 4
5.123 + \item {\tt Ex1} constant, 4
5.124 + \item {\tt Ex1_def} theorem, 8
5.125 + \item {\tt ex1E} theorem, 10
5.126 + \item {\tt ex1I} theorem, 10
5.127 + \item {\tt Ex_def} theorem, 8
5.128 + \item {\tt exCI} theorem, 10
5.129 + \item {\tt excluded_middle} theorem, 10
5.130 + \item {\tt exE} theorem, 10
5.131 + \item {\tt exhaust_tac}, \bold{38}
5.132 + \item {\tt exI} theorem, 10
5.133 + \item {\tt Exp} theory, 53
5.134 + \item {\tt ext} theorem, 7, 8
5.135 +
5.136 + \indexspace
5.137 +
5.138 + \item {\tt False} constant, 4
5.139 + \item {\tt False_def} theorem, 8
5.140 + \item {\tt FalseE} theorem, 9
5.141 + \item {\tt filter} constant, 26
5.142 + \item {\tt foldl} constant, 26
5.143 + \item {\tt fst} constant, 21
5.144 + \item {\tt fst_conv} theorem, 21
5.145 + \item {\tt Fun} theory, 19
5.146 + \item {\textit {fun}} type, 5
5.147 + \item {\tt fun_cong} theorem, 9
5.148 +
5.149 + \indexspace
5.150 +
5.151 + \item {\tt hd} constant, 26
5.152 + \item higher-order logic, 3--55
5.153 + \item {\tt HOL} theory, 3
5.154 + \item {\sc hol} system, 3, 6
5.155 + \item {\tt HOL_basic_ss}, \bold{19}
5.156 + \item {\tt HOL_cs}, \bold{20}
5.157 + \item {\tt HOL_quantifiers}, \bold{6}, 14
5.158 + \item {\tt HOL_ss}, \bold{19}
5.159 + \item {\tt hyp_subst_tac}, 19
5.160 +
5.161 + \indexspace
5.162 +
5.163 + \item {\tt If} constant, 4
5.164 + \item {\tt if_def} theorem, 8
5.165 + \item {\tt if_not_P} theorem, 10
5.166 + \item {\tt if_P} theorem, 10
5.167 + \item {\tt iff} theorem, 7, 8
5.168 + \item {\tt iffCE} theorem, 10, 14
5.169 + \item {\tt iffD1} theorem, 9
5.170 + \item {\tt iffD2} theorem, 9
5.171 + \item {\tt iffE} theorem, 9
5.172 + \item {\tt iffI} theorem, 9
5.173 + \item {\tt image_def} theorem, 15
5.174 + \item {\tt imageE} theorem, 17
5.175 + \item {\tt imageI} theorem, 17
5.176 + \item {\tt impCE} theorem, 10
5.177 + \item {\tt impE} theorem, 9
5.178 + \item {\tt impI} theorem, 7
5.179 + \item {\tt in} symbol, 5
5.180 + \item {\textit {ind}} type, 22
5.181 + \item {\tt induct_tac}, 24, \bold{38}
5.182 + \item {\tt inductive}, 49--51
5.183 + \item {\tt inj} constant, 19
5.184 + \item {\tt inj_def} theorem, 19
5.185 + \item {\tt inj_Inl} theorem, 23
5.186 + \item {\tt inj_Inr} theorem, 23
5.187 + \item {\tt inj_on} constant, 19
5.188 + \item {\tt inj_on_def} theorem, 19
5.189 + \item {\tt inj_Suc} theorem, 23
5.190 + \item {\tt Inl} constant, 23
5.191 + \item {\tt Inl_not_Inr} theorem, 23
5.192 + \item {\tt Inr} constant, 23
5.193 + \item {\tt insert} constant, 12
5.194 + \item {\tt insert_def} theorem, 15
5.195 + \item {\tt insertE} theorem, 17
5.196 + \item {\tt insertI1} theorem, 17
5.197 + \item {\tt insertI2} theorem, 17
5.198 + \item {\tt INT} symbol, 12--14
5.199 + \item {\tt Int} symbol, 12
5.200 + \item {\tt Int_absorb} theorem, 18
5.201 + \item {\tt Int_assoc} theorem, 18
5.202 + \item {\tt Int_commute} theorem, 18
5.203 + \item {\tt INT_D} theorem, 17
5.204 + \item {\tt Int_def} theorem, 15
5.205 + \item {\tt INT_E} theorem, 17
5.206 + \item {\tt Int_greatest} theorem, 18
5.207 + \item {\tt INT_I} theorem, 17
5.208 + \item {\tt Int_Inter_image} theorem, 18
5.209 + \item {\tt Int_lower1} theorem, 18
5.210 + \item {\tt Int_lower2} theorem, 18
5.211 + \item {\tt Int_Un_distrib} theorem, 18
5.212 + \item {\tt Int_Union} theorem, 18
5.213 + \item {\tt IntD1} theorem, 17
5.214 + \item {\tt IntD2} theorem, 17
5.215 + \item {\tt IntE} theorem, 17
5.216 + \item {\tt INTER} constant, 12
5.217 + \item {\tt Inter} constant, 12
5.218 + \item {\tt INTER1} constant, 12
5.219 + \item {\tt INTER1_def} theorem, 15
5.220 + \item {\tt INTER_def} theorem, 15
5.221 + \item {\tt Inter_def} theorem, 15
5.222 + \item {\tt Inter_greatest} theorem, 18
5.223 + \item {\tt Inter_lower} theorem, 18
5.224 + \item {\tt Inter_Un_distrib} theorem, 18
5.225 + \item {\tt InterD} theorem, 17
5.226 + \item {\tt InterE} theorem, 17
5.227 + \item {\tt InterI} theorem, 17
5.228 + \item {\tt IntI} theorem, 17
5.229 + \item {\tt inv} constant, 19
5.230 + \item {\tt inv_def} theorem, 19
5.231 +
5.232 + \indexspace
5.233 +
5.234 + \item {\tt last} constant, 26
5.235 + \item {\tt LEAST} constant, 5, 6, 24
5.236 + \item {\tt Least} constant, 4
5.237 + \item {\tt Least_def} theorem, 8
5.238 + \item {\tt length} constant, 26
5.239 + \item {\tt less_induct} theorem, 25
5.240 + \item {\tt Let} constant, 4, 7
5.241 + \item {\tt let} symbol, 5, 7
5.242 + \item {\tt Let_def} theorem, 7, 8
5.243 + \item {\tt LFilter} theory, 53
5.244 + \item {\tt List} theory, 25, 26
5.245 + \item {\textit{list}} type, 25
5.246 + \item {\tt LList} theory, 52
5.247 +
5.248 + \indexspace
5.249 +
5.250 + \item {\tt map} constant, 26
5.251 + \item {\tt max} constant, 5, 24
5.252 + \item {\tt mem} symbol, 26
5.253 + \item {\tt mem_Collect_eq} theorem, 14, 15
5.254 + \item {\tt min} constant, 5, 24
5.255 + \item {\tt minus} class, 5
5.256 + \item {\tt mod} symbol, 23
5.257 + \item {\tt mod_geq} theorem, 24
5.258 + \item {\tt mod_less} theorem, 24
5.259 + \item {\tt mono} constant, 5
5.260 + \item {\tt mp} theorem, 7
5.261 + \item {\tt mutual_induct_tac}, \bold{38}
5.262 +
5.263 + \indexspace
5.264 +
5.265 + \item {\tt n_not_Suc_n} theorem, 23
5.266 + \item {\tt Nat} theory, 24
5.267 + \item {\textit {nat}} type, 23, 24
5.268 + \item {\textit{nat}} type, 22--25
5.269 + \item {\tt nat_induct} theorem, 23
5.270 + \item {\tt nat_rec} constant, 24
5.271 + \item {\tt NatDef} theory, 22
5.272 + \item {\tt Not} constant, 4
5.273 + \item {\tt not_def} theorem, 8
5.274 + \item {\tt not_sym} theorem, 9
5.275 + \item {\tt notE} theorem, 9
5.276 + \item {\tt notI} theorem, 9
5.277 + \item {\tt notnotD} theorem, 10
5.278 + \item {\tt null} constant, 26
5.279 +
5.280 + \indexspace
5.281 +
5.282 + \item {\tt o} symbol, 4, 15
5.283 + \item {\tt o_def} theorem, 8
5.284 + \item {\tt of} symbol, 7
5.285 + \item {\tt or_def} theorem, 8
5.286 + \item {\tt Ord} theory, 5
5.287 + \item {\tt ord} class, 5, 6, 24
5.288 + \item {\tt order} class, 5, 24
5.289 +
5.290 + \indexspace
5.291 +
5.292 + \item {\tt Pair} constant, 21
5.293 + \item {\tt Pair_eq} theorem, 21
5.294 + \item {\tt Pair_inject} theorem, 21
5.295 + \item {\tt PairE} theorem, 21
5.296 + \item {\tt plus} class, 5
5.297 + \item {\tt Pow} constant, 12
5.298 + \item {\tt Pow_def} theorem, 15
5.299 + \item {\tt PowD} theorem, 17
5.300 + \item {\tt PowI} theorem, 17
5.301 + \item {\tt primrec}, 43--46
5.302 + \item {\tt primrec} symbol, 24
5.303 + \item priorities, 1
5.304 + \item {\tt Prod} theory, 21
5.305 + \item {\tt prop_cs}, \bold{20}
5.306 +
5.307 + \indexspace
5.308 +
5.309 + \item {\tt qed_spec_mp}, 41
5.310 +
5.311 + \indexspace
5.312 +
5.313 + \item {\tt range} constant, 12, 54
5.314 + \item {\tt range_def} theorem, 15
5.315 + \item {\tt rangeE} theorem, 17, 54
5.316 + \item {\tt rangeI} theorem, 17
5.317 + \item {\tt recdef}, 46--49
5.318 + \item {\tt record}, 31
5.319 + \item {\tt record_split_tac}, 33, 34
5.320 + \item recursion
5.321 + \subitem general, 46--49
5.322 + \subitem primitive, 43--46
5.323 + \item recursive functions, \see{recursion}{42}
5.324 + \item {\tt refl} theorem, 7
5.325 + \item {\tt res_inst_tac}, 6
5.326 + \item {\tt rev} constant, 26
5.327 +
5.328 + \indexspace
5.329 +
5.330 + \item search
5.331 + \subitem best-first, 55
5.332 + \item {\tt select_equality} theorem, 8, 10
5.333 + \item {\tt selectI} theorem, 7, 8
5.334 + \item {\tt Set} theory, 11, 14
5.335 + \item {\tt set} constant, 26
5.336 + \item {\tt set} type, 11
5.337 + \item {\tt set_diff_def} theorem, 15
5.338 + \item {\tt show_sorts}, 6
5.339 + \item {\tt show_types}, 6
5.340 + \item {\tt Sigma} constant, 21
5.341 + \item {\tt Sigma_def} theorem, 21
5.342 + \item {\tt SigmaE} theorem, 21
5.343 + \item {\tt SigmaI} theorem, 21
5.344 + \item simplification
5.345 + \subitem of conjunctions, 19
5.346 + \item {\tt size} constant, 38
5.347 + \item {\tt snd} constant, 21
5.348 + \item {\tt snd_conv} theorem, 21
5.349 + \item {\tt spec} theorem, 10
5.350 + \item {\tt split} constant, 21
5.351 + \item {\tt split} theorem, 21
5.352 + \item {\tt split_all_tac}, \bold{22}
5.353 + \item {\tt split_if} theorem, 10, 20
5.354 + \item {\tt split_list_case} theorem, 25
5.355 + \item {\tt split_split} theorem, 21
5.356 + \item {\tt split_sum_case} theorem, 23
5.357 + \item {\tt ssubst} theorem, 9, 11
5.358 + \item {\tt stac}, \bold{19}
5.359 + \item {\tt strip_tac}, \bold{11}
5.360 + \item {\tt subset_def} theorem, 15
5.361 + \item {\tt subset_refl} theorem, 16
5.362 + \item {\tt subset_trans} theorem, 16
5.363 + \item {\tt subsetCE} theorem, 14, 16
5.364 + \item {\tt subsetD} theorem, 14, 16
5.365 + \item {\tt subsetI} theorem, 16
5.366 + \item {\tt subst} theorem, 7
5.367 + \item {\tt Suc} constant, 23
5.368 + \item {\tt Suc_not_Zero} theorem, 23
5.369 + \item {\tt Sum} theory, 22
5.370 + \item {\tt sum_case} constant, 23
5.371 + \item {\tt sum_case_Inl} theorem, 23
5.372 + \item {\tt sum_case_Inr} theorem, 23
5.373 + \item {\tt sumE} theorem, 23
5.374 + \item {\tt surj} constant, 15, 19
5.375 + \item {\tt surj_def} theorem, 19
5.376 + \item {\tt surjective_pairing} theorem, 21
5.377 + \item {\tt surjective_sum} theorem, 23
5.378 + \item {\tt swap} theorem, 10
5.379 + \item {\tt swap_res_tac}, 55
5.380 + \item {\tt sym} theorem, 9
5.381 +
5.382 + \indexspace
5.383 +
5.384 + \item {\tt take} constant, 26
5.385 + \item {\tt takeWhile} constant, 26
5.386 + \item {\tt term} class, 5
5.387 + \item {\tt times} class, 5
5.388 + \item {\tt tl} constant, 26
5.389 + \item tracing
5.390 + \subitem of unification, 6
5.391 + \item {\tt trans} theorem, 9
5.392 + \item {\tt True} constant, 4
5.393 + \item {\tt True_def} theorem, 8
5.394 + \item {\tt True_or_False} theorem, 7, 8
5.395 + \item {\tt TrueI} theorem, 9
5.396 + \item {\tt Trueprop} constant, 4
5.397 + \item type definition, \bold{28}
5.398 + \item {\tt typedef}, 25
5.399 +
5.400 + \indexspace
5.401 +
5.402 + \item {\tt UN} symbol, 12--14
5.403 + \item {\tt Un} symbol, 12
5.404 + \item {\tt Un1} theorem, 14
5.405 + \item {\tt Un2} theorem, 14
5.406 + \item {\tt Un_absorb} theorem, 18
5.407 + \item {\tt Un_assoc} theorem, 18
5.408 + \item {\tt Un_commute} theorem, 18
5.409 + \item {\tt Un_def} theorem, 15
5.410 + \item {\tt UN_E} theorem, 17
5.411 + \item {\tt UN_I} theorem, 17
5.412 + \item {\tt Un_Int_distrib} theorem, 18
5.413 + \item {\tt Un_Inter} theorem, 18
5.414 + \item {\tt Un_least} theorem, 18
5.415 + \item {\tt Un_Union_image} theorem, 18
5.416 + \item {\tt Un_upper1} theorem, 18
5.417 + \item {\tt Un_upper2} theorem, 18
5.418 + \item {\tt UnCI} theorem, 14, 17
5.419 + \item {\tt UnE} theorem, 17
5.420 + \item {\tt UnI1} theorem, 17
5.421 + \item {\tt UnI2} theorem, 17
5.422 + \item unification
5.423 + \subitem incompleteness of, 6
5.424 + \item {\tt Unify.trace_types}, 6
5.425 + \item {\tt UNION} constant, 12
5.426 + \item {\tt Union} constant, 12
5.427 + \item {\tt UNION1} constant, 12
5.428 + \item {\tt UNION1_def} theorem, 15
5.429 + \item {\tt UNION_def} theorem, 15
5.430 + \item {\tt Union_def} theorem, 15
5.431 + \item {\tt Union_least} theorem, 18
5.432 + \item {\tt Union_Un_distrib} theorem, 18
5.433 + \item {\tt Union_upper} theorem, 18
5.434 + \item {\tt UnionE} theorem, 17
5.435 + \item {\tt UnionI} theorem, 17
5.436 + \item {\tt unit_eq} theorem, 22
5.437 +
5.438 + \indexspace
5.439 +
5.440 + \item {\tt ZF} theory, 3
5.441 +
5.442 +\end{theindex}
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/HOL/logics-HOL.rao Tue May 04 18:03:56 1999 +0200
6.3 @@ -0,0 +1,122 @@
6.4 +% This file was generated by 'rail' from 'logics-HOL.rai'
6.5 +\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
6.6 +\rail@o {1}{
6.7 +\rail@begin{2}{typedef}
6.8 +\rail@term{typedef}[]
6.9 +\rail@bar
6.10 +\rail@nextbar{1}
6.11 +\rail@term{(}[]
6.12 +\rail@nont{name}[]
6.13 +\rail@term{)}[]
6.14 +\rail@endbar
6.15 +\rail@nont{type}[]
6.16 +\rail@term{=}[]
6.17 +\rail@nont{set}[]
6.18 +\rail@nont{witness}[]
6.19 +\rail@end
6.20 +\rail@begin{2}{type}
6.21 +\rail@nont{typevarlist}[]
6.22 +\rail@nont{name}[]
6.23 +\rail@bar
6.24 +\rail@nextbar{1}
6.25 +\rail@term{(}[]
6.26 +\rail@nont{infix}[]
6.27 +\rail@term{)}[]
6.28 +\rail@endbar
6.29 +\rail@end
6.30 +\rail@begin{1}{set}
6.31 +\rail@nont{string}[]
6.32 +\rail@end
6.33 +\rail@begin{2}{witness}
6.34 +\rail@bar
6.35 +\rail@nextbar{1}
6.36 +\rail@term{(}[]
6.37 +\rail@nont{id}[]
6.38 +\rail@term{)}[]
6.39 +\rail@endbar
6.40 +\rail@end
6.41 +}
6.42 +\rail@i {2}{ record : 'record' typevarlist name '=' parent (field +); \par parent : ( () | type '+'); field : name '::' type; }
6.43 +\rail@o {2}{
6.44 +\rail@begin{2}{record}
6.45 +\rail@term{record}[]
6.46 +\rail@nont{typevarlist}[]
6.47 +\rail@nont{name}[]
6.48 +\rail@term{=}[]
6.49 +\rail@nont{parent}[]
6.50 +\rail@plus
6.51 +\rail@nont{field}[]
6.52 +\rail@nextplus{1}
6.53 +\rail@endplus
6.54 +\rail@end
6.55 +\rail@begin{2}{parent}
6.56 +\rail@bar
6.57 +\rail@nextbar{1}
6.58 +\rail@nont{type}[]
6.59 +\rail@term{+}[]
6.60 +\rail@endbar
6.61 +\rail@end
6.62 +\rail@begin{1}{field}
6.63 +\rail@nont{name}[]
6.64 +\rail@term{::}[]
6.65 +\rail@nont{type}[]
6.66 +\rail@end
6.67 +}
6.68 +\rail@i {3}{ datatype : 'datatype' typedecls; \par typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
6.69 +\rail@o {3}{
6.70 +\rail@begin{1}{datatype}
6.71 +\rail@term{datatype}[]
6.72 +\rail@nont{typedecls}[]
6.73 +\rail@end
6.74 +\rail@begin{3}{typedecls}
6.75 +\rail@plus
6.76 +\rail@nont{newtype}[]
6.77 +\rail@term{=}[]
6.78 +\rail@plus
6.79 +\rail@nont{cons}[]
6.80 +\rail@nextplus{1}
6.81 +\rail@cterm{|}[]
6.82 +\rail@endplus
6.83 +\rail@nextplus{2}
6.84 +\rail@cterm{and}[]
6.85 +\rail@endplus
6.86 +\rail@end
6.87 +\rail@begin{2}{newtype}
6.88 +\rail@nont{typevarlist}[]
6.89 +\rail@nont{id}[]
6.90 +\rail@bar
6.91 +\rail@nextbar{1}
6.92 +\rail@term{(}[]
6.93 +\rail@nont{infix}[]
6.94 +\rail@term{)}[]
6.95 +\rail@endbar
6.96 +\rail@end
6.97 +\rail@begin{3}{cons}
6.98 +\rail@nont{name}[]
6.99 +\rail@bar
6.100 +\rail@nextbar{1}
6.101 +\rail@plus
6.102 +\rail@nont{argtype}[]
6.103 +\rail@nextplus{2}
6.104 +\rail@endplus
6.105 +\rail@endbar
6.106 +\rail@bar
6.107 +\rail@nextbar{1}
6.108 +\rail@term{(}[]
6.109 +\rail@nont{mixfix}[]
6.110 +\rail@term{)}[]
6.111 +\rail@endbar
6.112 +\rail@end
6.113 +\rail@begin{3}{argtype}
6.114 +\rail@bar
6.115 +\rail@nont{id}[]
6.116 +\rail@nextbar{1}
6.117 +\rail@nont{tid}[]
6.118 +\rail@nextbar{2}
6.119 +\rail@term{(}[]
6.120 +\rail@nont{typevarlist}[]
6.121 +\rail@nont{id}[]
6.122 +\rail@term{)}[]
6.123 +\rail@endbar
6.124 +\rail@end
6.125 +}
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/doc-src/HOL/logics-HOL.tex Tue May 04 18:03:56 1999 +0200
7.3 @@ -0,0 +1,61 @@
7.4 +%% $Id$
7.5 +\documentclass[12pt]{report}
7.6 +\usepackage{graphicx,a4,latexsym,../pdfsetup}
7.7 +
7.8 +\makeatletter
7.9 +\input{../proof.sty}
7.10 +\input{../rail.sty}
7.11 +\input{../iman.sty}
7.12 +\input{../extra.sty}
7.13 +\makeatother
7.14 +
7.15 +%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
7.16 +%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
7.17 +%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
7.18 +%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
7.19 +
7.20 +\title{\includegraphics[scale=0.5]{isabelle_hol.eps} \\[4ex]
7.21 + Isabelle's Logics: HOL}
7.22 +
7.23 +\author{{\em Lawrence C. Paulson}\\
7.24 + Computer Laboratory \\ University of Cambridge \\
7.25 + \texttt{lcp@cl.cam.ac.uk}\\[3ex]
7.26 + With Contributions by Tobias Nipkow and Markus Wenzel%
7.27 + \thanks{Tobias Nipkow developed~\HOL{}. Markus Wenzel made numerous
7.28 + improvements. The research has been funded by the EPSRC (grants
7.29 + GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project
7.30 + 6453: Types.}}
7.31 +
7.32 +\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
7.33 + \hrule\bigskip}
7.34 +\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
7.35 +
7.36 +\makeindex
7.37 +
7.38 +\underscoreoff
7.39 +
7.40 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
7.41 +
7.42 +\pagestyle{headings}
7.43 +\sloppy
7.44 +\binperiod %%%treat . like a binary operator
7.45 +
7.46 +\begin{document}
7.47 +\maketitle
7.48 +
7.49 +\begin{abstract}
7.50 + This manual describes Isabelle's formalization of Higher-Order Logic, a
7.51 + polymorphic version of Church's Simple Theory of Types. HOL can be best
7.52 + understood as a simply-typed version of classical set theory. See also
7.53 + \emph{Isabelle/HOL --- The Tutorial} for a gentle introduction on using
7.54 + Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle
7.55 + commands.
7.56 +\end{abstract}
7.57 +
7.58 +\pagenumbering{roman} \tableofcontents \clearfirst
7.59 +\include{../Logics/syntax}
7.60 +\include{HOL}
7.61 +\bibliographystyle{plain}
7.62 +\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
7.63 +\input{logics-HOL.ind}
7.64 +\end{document}