1.1 --- a/doc-src/Logics/HOL-eg.txt Tue May 04 18:04:45 1999 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,151 +0,0 @@
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 --- a/doc-src/Logics/HOL-rules.txt Tue May 04 18:04:45 1999 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,403 +0,0 @@
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 --- a/doc-src/Logics/HOL.tex Tue May 04 18:04:45 1999 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,2981 +0,0 @@
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 --- a/doc-src/Logics/logics.ind Tue May 04 18:04:45 1999 +0200
4.2 +++ b/doc-src/Logics/logics.ind Tue May 04 18:05:34 1999 +0200
4.3 @@ -1,659 +1,307 @@
4.4 \begin{theindex}
4.5
4.6 - \item {\tt !} symbol, 6, 8, 15, 16, 28
4.7 - \item {\tt[]} symbol, 28
4.8 - \item {\tt\#} symbol, 28
4.9 - \item {\tt\#*} symbol, 83
4.10 - \item {\tt\#+} symbol, 83
4.11 - \item {\tt\&} symbol, 6, 59
4.12 - \item {\tt *} symbol, 7, 25, 74
4.13 - \item {\tt *} type, 23
4.14 - \item {\tt +} symbol, 7, 25, 74
4.15 - \item {\tt +} type, 23
4.16 - \item {\tt -} symbol, 7, 25, 83
4.17 - \item {\tt -->} symbol, 6, 59, 74
4.18 - \item {\tt :} symbol, 14
4.19 - \item {\tt <} constant, 26
4.20 - \item {\tt <} symbol, 25
4.21 - \item {\tt <->} symbol, 59
4.22 - \item {\tt <=} constant, 26
4.23 - \item {\tt <=} symbol, 14
4.24 - \item {\tt =} symbol, 6, 59, 74
4.25 - \item {\tt ?} symbol, 6, 8, 15, 16
4.26 - \item {\tt ?!} symbol, 6
4.27 - \item {\tt\at} symbol, 6, 28
4.28 - \item {\tt `} symbol, 74
4.29 - \item {\tt ``} symbol, 14
4.30 - \item \verb'{}' symbol, 14
4.31 - \item {\tt |} symbol, 6, 59
4.32 - \item {\tt |-|} symbol, 83
4.33 + \item {\tt\#*} symbol, 30
4.34 + \item {\tt\#+} symbol, 30
4.35 + \item {\tt\&} symbol, 6
4.36 + \item {\tt *} symbol, 21
4.37 + \item {\tt +} symbol, 21
4.38 + \item {\tt -} symbol, 30
4.39 + \item {\tt -->} symbol, 6, 21
4.40 + \item {\tt <->} symbol, 6
4.41 + \item {\tt =} symbol, 6, 21
4.42 + \item {\tt `} symbol, 21
4.43 + \item {\tt |} symbol, 6
4.44 + \item {\tt |-|} symbol, 30
4.45
4.46 \indexspace
4.47
4.48 - \item {\tt 0} constant, 25, 72
4.49 + \item {\tt 0} constant, 19
4.50
4.51 \indexspace
4.52
4.53 - \item {\tt absdiff_def} theorem, 83
4.54 - \item {\tt add_assoc} theorem, 83
4.55 - \item {\tt add_commute} theorem, 83
4.56 - \item {\tt add_def} theorem, 83
4.57 - \item {\tt add_inverse_diff} theorem, 83
4.58 - \item {\tt add_mp_tac}, \bold{81}
4.59 - \item {\tt add_mult_dist} theorem, 83
4.60 - \item {\tt add_safes}, \bold{65}
4.61 - \item {\tt add_typing} theorem, 83
4.62 - \item {\tt add_unsafes}, \bold{65}
4.63 - \item {\tt addC0} theorem, 83
4.64 - \item {\tt addC_succ} theorem, 83
4.65 - \item {\tt Addsplits}, \bold{22}
4.66 - \item {\tt addsplits}, \bold{22}, 27, 39
4.67 - \item {\tt ALL} symbol, 6, 8, 15, 16, 59
4.68 - \item {\tt All} constant, 6, 59
4.69 - \item {\tt All_def} theorem, 10
4.70 - \item {\tt all_dupE} theorem, 12
4.71 - \item {\tt allE} theorem, 12
4.72 - \item {\tt allI} theorem, 12
4.73 - \item {\tt allL} theorem, 61, 65
4.74 - \item {\tt allL_thin} theorem, 62
4.75 - \item {\tt allR} theorem, 61
4.76 - \item {\tt and_def} theorem, 10
4.77 - \item {\tt arg_cong} theorem, 11
4.78 - \item {\tt Arith} theory, 26, 82
4.79 - \item {\tt arith_tac}, 27
4.80 + \item {\tt absdiff_def} theorem, 30
4.81 + \item {\tt add_assoc} theorem, 30
4.82 + \item {\tt add_commute} theorem, 30
4.83 + \item {\tt add_def} theorem, 30
4.84 + \item {\tt add_inverse_diff} theorem, 30
4.85 + \item {\tt add_mp_tac}, \bold{28}
4.86 + \item {\tt add_mult_dist} theorem, 30
4.87 + \item {\tt add_safes}, \bold{12}
4.88 + \item {\tt add_typing} theorem, 30
4.89 + \item {\tt add_unsafes}, \bold{12}
4.90 + \item {\tt addC0} theorem, 30
4.91 + \item {\tt addC_succ} theorem, 30
4.92 + \item {\tt ALL} symbol, 6
4.93 + \item {\tt All} constant, 6
4.94 + \item {\tt allL} theorem, 8, 12
4.95 + \item {\tt allL_thin} theorem, 9
4.96 + \item {\tt allR} theorem, 8
4.97 + \item {\tt Arith} theory, 29
4.98 \item assumptions
4.99 - \subitem in {\CTT}, 71, 81
4.100 + \subitem in {\CTT}, 18, 28
4.101
4.102 \indexspace
4.103
4.104 - \item {\tt Ball} constant, 14, 16
4.105 - \item {\tt Ball_def} theorem, 17
4.106 - \item {\tt ballE} theorem, 18
4.107 - \item {\tt ballI} theorem, 18
4.108 - \item {\tt basic} theorem, 61
4.109 - \item {\tt basic_defs}, \bold{79}
4.110 - \item {\tt best_tac}, \bold{66}
4.111 - \item {\tt Bex} constant, 14, 16
4.112 - \item {\tt Bex_def} theorem, 17
4.113 - \item {\tt bexCI} theorem, 16, 18
4.114 - \item {\tt bexE} theorem, 18
4.115 - \item {\tt bexI} theorem, 16, 18
4.116 - \item {\textit {bool}} type, 7
4.117 - \item {\tt box_equals} theorem, 11, 13
4.118 - \item {\tt bspec} theorem, 18
4.119 - \item {\tt butlast} constant, 28
4.120 + \item {\tt basic} theorem, 8
4.121 + \item {\tt basic_defs}, \bold{26}
4.122 + \item {\tt best_tac}, \bold{13}
4.123
4.124 \indexspace
4.125
4.126 - \item {\tt case} symbol, 9, 26, 27, 39
4.127 - \item {\tt case_tac}, \bold{13}
4.128 \item {\tt CCL} theory, 1
4.129 - \item {\tt ccontr} theorem, 12
4.130 - \item {\tt classical} theorem, 12
4.131 - \item {\tt coinductive}, 51--53
4.132 - \item {\tt Collect} constant, 14, 16
4.133 - \item {\tt Collect_mem_eq} theorem, 16, 17
4.134 - \item {\tt CollectD} theorem, 18, 56
4.135 - \item {\tt CollectE} theorem, 18
4.136 - \item {\tt CollectI} theorem, 18, 57
4.137 - \item {\tt comp_rls}, \bold{79}
4.138 - \item {\tt Compl} constant, 14
4.139 - \item {\tt Compl_def} theorem, 17
4.140 - \item {\tt Compl_disjoint} theorem, 20
4.141 - \item {\tt Compl_Int} theorem, 20
4.142 - \item {\tt Compl_partition} theorem, 20
4.143 - \item {\tt Compl_Un} theorem, 20
4.144 - \item {\tt ComplD} theorem, 19
4.145 - \item {\tt ComplI} theorem, 19
4.146 - \item {\tt concat} constant, 28
4.147 - \item {\tt cong} theorem, 11
4.148 - \item {\tt conj_cong}, 21
4.149 - \item {\tt conjE} theorem, 11
4.150 - \item {\tt conjI} theorem, 11
4.151 - \item {\tt conjL} theorem, 61
4.152 - \item {\tt conjR} theorem, 61
4.153 - \item {\tt conjunct1} theorem, 11
4.154 - \item {\tt conjunct2} theorem, 11
4.155 - \item {\tt conL} theorem, 62
4.156 - \item {\tt conR} theorem, 62
4.157 - \item Constructive Type Theory, 71--93
4.158 - \item {\tt context}, 57
4.159 - \item {\tt contr} constant, 72
4.160 - \item {\tt could_res}, \bold{64}
4.161 - \item {\tt could_resolve_seq}, \bold{64}
4.162 - \item {\tt CTT} theory, 1, 71
4.163 + \item {\tt comp_rls}, \bold{26}
4.164 + \item {\tt conjL} theorem, 8
4.165 + \item {\tt conjR} theorem, 8
4.166 + \item {\tt conL} theorem, 9
4.167 + \item {\tt conR} theorem, 9
4.168 + \item Constructive Type Theory, 18--40
4.169 + \item {\tt contr} constant, 19
4.170 + \item {\tt could_res}, \bold{11}
4.171 + \item {\tt could_resolve_seq}, \bold{11}
4.172 + \item {\tt CTT} theory, 1, 18
4.173 \item {\tt Cube} theory, 1
4.174 - \item {\tt cut} theorem, 61
4.175 - \item {\tt cutL_tac}, \bold{63}
4.176 - \item {\tt cutR_tac}, \bold{63}
4.177 + \item {\tt cut} theorem, 8
4.178 + \item {\tt cutL_tac}, \bold{10}
4.179 + \item {\tt cutR_tac}, \bold{10}
4.180
4.181 \indexspace
4.182
4.183 - \item {\tt datatype}, 36--44
4.184 - \item {\tt Delsplits}, \bold{22}
4.185 - \item {\tt delsplits}, \bold{22}
4.186 - \item {\tt diff_0_eq_0} theorem, 83
4.187 - \item {\tt diff_def} theorem, 83
4.188 - \item {\tt diff_self_eq_0} theorem, 83
4.189 - \item {\tt diff_succ_succ} theorem, 83
4.190 - \item {\tt diff_typing} theorem, 83
4.191 - \item {\tt diffC0} theorem, 83
4.192 - \item {\tt disjCI} theorem, 12
4.193 - \item {\tt disjE} theorem, 11
4.194 - \item {\tt disjI1} theorem, 11
4.195 - \item {\tt disjI2} theorem, 11
4.196 - \item {\tt disjL} theorem, 61
4.197 - \item {\tt disjR} theorem, 61
4.198 - \item {\tt div} symbol, 25, 83
4.199 - \item {\tt div_def} theorem, 83
4.200 - \item {\tt div_geq} theorem, 26
4.201 - \item {\tt div_less} theorem, 26
4.202 - \item {\tt Divides} theory, 26
4.203 - \item {\tt double_complement} theorem, 20
4.204 - \item {\tt drop} constant, 28
4.205 - \item {\tt dropWhile} constant, 28
4.206 + \item {\tt diff_0_eq_0} theorem, 30
4.207 + \item {\tt diff_def} theorem, 30
4.208 + \item {\tt diff_self_eq_0} theorem, 30
4.209 + \item {\tt diff_succ_succ} theorem, 30
4.210 + \item {\tt diff_typing} theorem, 30
4.211 + \item {\tt diffC0} theorem, 30
4.212 + \item {\tt disjL} theorem, 8
4.213 + \item {\tt disjR} theorem, 8
4.214 + \item {\tt div} symbol, 30
4.215 + \item {\tt div_def} theorem, 30
4.216
4.217 \indexspace
4.218
4.219 - \item {\tt Elem} constant, 72
4.220 - \item {\tt elim_rls}, \bold{79}
4.221 - \item {\tt elimL_rls}, \bold{79}
4.222 - \item {\tt empty_def} theorem, 17
4.223 - \item {\tt empty_pack}, \bold{65}
4.224 - \item {\tt emptyE} theorem, 19
4.225 - \item {\tt Eps} constant, 6, 8
4.226 - \item {\tt Eq} constant, 72
4.227 - \item {\tt eq} constant, 72, 77
4.228 - \item {\tt EqC} theorem, 78
4.229 - \item {\tt EqE} theorem, 78
4.230 - \item {\tt Eqelem} constant, 72
4.231 - \item {\tt EqF} theorem, 78
4.232 - \item {\tt EqFL} theorem, 78
4.233 - \item {\tt EqI} theorem, 78
4.234 - \item {\tt Eqtype} constant, 72
4.235 - \item {\tt equal_tac}, \bold{80}
4.236 - \item {\tt equal_types} theorem, 75
4.237 - \item {\tt equal_typesL} theorem, 75
4.238 - \item {\tt equalityCE} theorem, 16, 18, 56, 57
4.239 - \item {\tt equalityD1} theorem, 18
4.240 - \item {\tt equalityD2} theorem, 18
4.241 - \item {\tt equalityE} theorem, 18
4.242 - \item {\tt equalityI} theorem, 18
4.243 - \item {\tt EX} symbol, 6, 8, 15, 16, 59
4.244 - \item {\tt Ex} constant, 6, 59
4.245 - \item {\tt EX!} symbol, 6
4.246 - \item {\tt Ex1} constant, 6
4.247 - \item {\tt Ex1_def} theorem, 10
4.248 - \item {\tt ex1E} theorem, 12
4.249 - \item {\tt ex1I} theorem, 12
4.250 - \item {\tt Ex_def} theorem, 10
4.251 - \item {\tt exCI} theorem, 12
4.252 - \item {\tt excluded_middle} theorem, 12
4.253 - \item {\tt exE} theorem, 12
4.254 - \item {\tt exhaust_tac}, \bold{40}
4.255 - \item {\tt exI} theorem, 12
4.256 - \item {\tt exL} theorem, 61
4.257 - \item {\tt Exp} theory, 55
4.258 - \item {\tt exR} theorem, 61, 65, 67
4.259 - \item {\tt exR_thin} theorem, 62, 67, 68
4.260 - \item {\tt ext} theorem, 9, 10
4.261 + \item {\tt Elem} constant, 19
4.262 + \item {\tt elim_rls}, \bold{26}
4.263 + \item {\tt elimL_rls}, \bold{26}
4.264 + \item {\tt empty_pack}, \bold{12}
4.265 + \item {\tt Eq} constant, 19
4.266 + \item {\tt eq} constant, 19, 24
4.267 + \item {\tt EqC} theorem, 25
4.268 + \item {\tt EqE} theorem, 25
4.269 + \item {\tt Eqelem} constant, 19
4.270 + \item {\tt EqF} theorem, 25
4.271 + \item {\tt EqFL} theorem, 25
4.272 + \item {\tt EqI} theorem, 25
4.273 + \item {\tt Eqtype} constant, 19
4.274 + \item {\tt equal_tac}, \bold{27}
4.275 + \item {\tt equal_types} theorem, 22
4.276 + \item {\tt equal_typesL} theorem, 22
4.277 + \item {\tt EX} symbol, 6
4.278 + \item {\tt Ex} constant, 6
4.279 + \item {\tt exL} theorem, 8
4.280 + \item {\tt exR} theorem, 8, 12, 14
4.281 + \item {\tt exR_thin} theorem, 9, 14, 15
4.282
4.283 \indexspace
4.284
4.285 - \item {\tt F} constant, 72
4.286 - \item {\tt False} constant, 6, 59
4.287 - \item {\tt False_def} theorem, 10
4.288 - \item {\tt FalseE} theorem, 11
4.289 - \item {\tt FalseL} theorem, 61
4.290 - \item {\tt fast_tac}, \bold{66}
4.291 - \item {\tt FE} theorem, 78, 82
4.292 - \item {\tt FEL} theorem, 78
4.293 - \item {\tt FF} theorem, 78
4.294 - \item {\tt filseq_resolve_tac}, \bold{64}
4.295 - \item {\tt filt_resolve_tac}, 64, 80
4.296 - \item {\tt filter} constant, 28
4.297 - \item flex-flex constraints, 60
4.298 - \item {\tt FOL} theory, 81
4.299 - \item {\tt foldl} constant, 28
4.300 - \item {\tt form_rls}, \bold{79}
4.301 - \item {\tt formL_rls}, \bold{79}
4.302 - \item {\tt forms_of_seq}, \bold{63}
4.303 - \item {\tt fst} constant, 23, 72, 77
4.304 - \item {\tt fst_conv} theorem, 23
4.305 - \item {\tt fst_def} theorem, 77
4.306 - \item {\tt Fun} theory, 21
4.307 - \item {\textit {fun}} type, 7
4.308 - \item {\tt fun_cong} theorem, 11
4.309 + \item {\tt F} constant, 19
4.310 + \item {\tt False} constant, 6
4.311 + \item {\tt FalseL} theorem, 8
4.312 + \item {\tt fast_tac}, \bold{13}
4.313 + \item {\tt FE} theorem, 25, 29
4.314 + \item {\tt FEL} theorem, 25
4.315 + \item {\tt FF} theorem, 25
4.316 + \item {\tt filseq_resolve_tac}, \bold{11}
4.317 + \item {\tt filt_resolve_tac}, 11, 27
4.318 + \item flex-flex constraints, 7
4.319 + \item {\tt FOL} theory, 28
4.320 + \item {\tt form_rls}, \bold{26}
4.321 + \item {\tt formL_rls}, \bold{26}
4.322 + \item {\tt forms_of_seq}, \bold{10}
4.323 + \item {\tt fst} constant, 19, 24
4.324 + \item {\tt fst_def} theorem, 24
4.325 \item function applications
4.326 - \subitem in \CTT, 74
4.327 + \subitem in \CTT, 21
4.328
4.329 \indexspace
4.330
4.331 - \item {\tt hd} constant, 28
4.332 - \item higher-order logic, 5--57
4.333 - \item {\tt HOL} theory, 1, 5
4.334 - \item {\sc hol} system, 5, 8
4.335 - \item {\tt HOL_basic_ss}, \bold{21}
4.336 - \item {\tt HOL_cs}, \bold{22}
4.337 - \item {\tt HOL_quantifiers}, \bold{8}, 16
4.338 - \item {\tt HOL_ss}, \bold{21}
4.339 + \item {\tt HOL} theory, 1
4.340 \item {\tt HOLCF} theory, 1
4.341 - \item {\tt hyp_rew_tac}, \bold{81}
4.342 - \item {\tt hyp_subst_tac}, 21
4.343 + \item {\tt hyp_rew_tac}, \bold{28}
4.344
4.345 \indexspace
4.346
4.347 - \item {\textit {i}} type, 71
4.348 - \item {\tt If} constant, 6
4.349 - \item {\tt if_def} theorem, 10
4.350 - \item {\tt if_not_P} theorem, 12
4.351 - \item {\tt if_P} theorem, 12
4.352 - \item {\tt iff} theorem, 9, 10
4.353 - \item {\tt iff_def} theorem, 61
4.354 - \item {\tt iffCE} theorem, 12, 16
4.355 - \item {\tt iffD1} theorem, 11
4.356 - \item {\tt iffD2} theorem, 11
4.357 - \item {\tt iffE} theorem, 11
4.358 - \item {\tt iffI} theorem, 11
4.359 - \item {\tt iffL} theorem, 62, 69
4.360 - \item {\tt iffR} theorem, 62
4.361 + \item {\textit {i}} type, 18
4.362 + \item {\tt iff_def} theorem, 8
4.363 + \item {\tt iffL} theorem, 9, 16
4.364 + \item {\tt iffR} theorem, 9
4.365 \item {\tt ILL} theory, 1
4.366 - \item {\tt image_def} theorem, 17
4.367 - \item {\tt imageE} theorem, 19
4.368 - \item {\tt imageI} theorem, 19
4.369 - \item {\tt impCE} theorem, 12
4.370 - \item {\tt impE} theorem, 11
4.371 - \item {\tt impI} theorem, 9
4.372 - \item {\tt impL} theorem, 61
4.373 - \item {\tt impR} theorem, 61
4.374 - \item {\tt in} symbol, 7
4.375 - \item {\textit {ind}} type, 24
4.376 - \item {\tt induct_tac}, 26, \bold{40}
4.377 - \item {\tt inductive}, 51--53
4.378 - \item {\tt inj} constant, 21
4.379 - \item {\tt inj_def} theorem, 21
4.380 - \item {\tt inj_Inl} theorem, 25
4.381 - \item {\tt inj_Inr} theorem, 25
4.382 - \item {\tt inj_on} constant, 21
4.383 - \item {\tt inj_on_def} theorem, 21
4.384 - \item {\tt inj_Suc} theorem, 25
4.385 - \item {\tt Inl} constant, 25
4.386 - \item {\tt inl} constant, 72, 77, 87
4.387 - \item {\tt Inl_not_Inr} theorem, 25
4.388 - \item {\tt Inr} constant, 25
4.389 - \item {\tt inr} constant, 72, 77
4.390 - \item {\tt insert} constant, 14
4.391 - \item {\tt insert_def} theorem, 17
4.392 - \item {\tt insertE} theorem, 19
4.393 - \item {\tt insertI1} theorem, 19
4.394 - \item {\tt insertI2} theorem, 19
4.395 - \item {\tt INT} symbol, 14--16
4.396 - \item {\tt Int} symbol, 14
4.397 - \item {\tt Int_absorb} theorem, 20
4.398 - \item {\tt Int_assoc} theorem, 20
4.399 - \item {\tt Int_commute} theorem, 20
4.400 - \item {\tt INT_D} theorem, 19
4.401 - \item {\tt Int_def} theorem, 17
4.402 - \item {\tt INT_E} theorem, 19
4.403 - \item {\tt Int_greatest} theorem, 20
4.404 - \item {\tt INT_I} theorem, 19
4.405 - \item {\tt Int_Inter_image} theorem, 20
4.406 - \item {\tt Int_lower1} theorem, 20
4.407 - \item {\tt Int_lower2} theorem, 20
4.408 - \item {\tt Int_Un_distrib} theorem, 20
4.409 - \item {\tt Int_Union} theorem, 20
4.410 - \item {\tt IntD1} theorem, 19
4.411 - \item {\tt IntD2} theorem, 19
4.412 - \item {\tt IntE} theorem, 19
4.413 - \item {\tt INTER} constant, 14
4.414 - \item {\tt Inter} constant, 14
4.415 - \item {\tt INTER1} constant, 14
4.416 - \item {\tt INTER1_def} theorem, 17
4.417 - \item {\tt INTER_def} theorem, 17
4.418 - \item {\tt Inter_def} theorem, 17
4.419 - \item {\tt Inter_greatest} theorem, 20
4.420 - \item {\tt Inter_lower} theorem, 20
4.421 - \item {\tt Inter_Un_distrib} theorem, 20
4.422 - \item {\tt InterD} theorem, 19
4.423 - \item {\tt InterE} theorem, 19
4.424 - \item {\tt InterI} theorem, 19
4.425 - \item {\tt IntI} theorem, 19
4.426 - \item {\tt intr_rls}, \bold{79}
4.427 - \item {\tt intr_tac}, \bold{80}, 89, 90
4.428 - \item {\tt intrL_rls}, \bold{79}
4.429 - \item {\tt inv} constant, 21
4.430 - \item {\tt inv_def} theorem, 21
4.431 + \item {\tt impL} theorem, 8
4.432 + \item {\tt impR} theorem, 8
4.433 + \item {\tt inl} constant, 19, 24, 34
4.434 + \item {\tt inr} constant, 19, 24
4.435 + \item {\tt intr_rls}, \bold{26}
4.436 + \item {\tt intr_tac}, \bold{27}, 36, 37
4.437 + \item {\tt intrL_rls}, \bold{26}
4.438
4.439 \indexspace
4.440
4.441 - \item {\tt lam} symbol, 74
4.442 - \item {\tt lambda} constant, 72, 74
4.443 + \item {\tt lam} symbol, 21
4.444 + \item {\tt lambda} constant, 19, 21
4.445 \item $\lambda$-abstractions
4.446 - \subitem in \CTT, 74
4.447 - \item {\tt last} constant, 28
4.448 + \subitem in \CTT, 21
4.449 \item {\tt LCF} theory, 1
4.450 - \item {\tt LEAST} constant, 7, 8, 26
4.451 - \item {\tt Least} constant, 6
4.452 - \item {\tt Least_def} theorem, 10
4.453 - \item {\tt length} constant, 28
4.454 - \item {\tt less_induct} theorem, 27
4.455 - \item {\tt Let} constant, 6, 9
4.456 - \item {\tt let} symbol, 7, 9
4.457 - \item {\tt Let_def} theorem, 9, 10
4.458 - \item {\tt LFilter} theory, 55
4.459 - \item {\tt List} theory, 27, 28
4.460 - \item {\textit{list}} type, 27
4.461 - \item {\tt LK} theory, 1, 58, 62
4.462 - \item {\tt LK_dup_pack}, \bold{65}, 66
4.463 - \item {\tt LK_pack}, \bold{65}
4.464 - \item {\tt LList} theory, 54
4.465 + \item {\tt LK} theory, 1, 5, 9
4.466 + \item {\tt LK_dup_pack}, \bold{12}, 13
4.467 + \item {\tt LK_pack}, \bold{12}
4.468
4.469 \indexspace
4.470
4.471 - \item {\tt map} constant, 28
4.472 - \item {\tt max} constant, 7, 26
4.473 - \item {\tt mem} symbol, 28
4.474 - \item {\tt mem_Collect_eq} theorem, 16, 17
4.475 - \item {\tt min} constant, 7, 26
4.476 - \item {\tt minus} class, 7
4.477 - \item {\tt mod} symbol, 25, 83
4.478 - \item {\tt mod_def} theorem, 83
4.479 - \item {\tt mod_geq} theorem, 26
4.480 - \item {\tt mod_less} theorem, 26
4.481 + \item {\tt mod} symbol, 30
4.482 + \item {\tt mod_def} theorem, 30
4.483 \item {\tt Modal} theory, 1
4.484 - \item {\tt mono} constant, 7
4.485 - \item {\tt mp} theorem, 9
4.486 - \item {\tt mp_tac}, \bold{81}
4.487 - \item {\tt mult_assoc} theorem, 83
4.488 - \item {\tt mult_commute} theorem, 83
4.489 - \item {\tt mult_def} theorem, 83
4.490 - \item {\tt mult_typing} theorem, 83
4.491 - \item {\tt multC0} theorem, 83
4.492 - \item {\tt multC_succ} theorem, 83
4.493 - \item {\tt mutual_induct_tac}, \bold{40}
4.494 + \item {\tt mp_tac}, \bold{28}
4.495 + \item {\tt mult_assoc} theorem, 30
4.496 + \item {\tt mult_commute} theorem, 30
4.497 + \item {\tt mult_def} theorem, 30
4.498 + \item {\tt mult_typing} theorem, 30
4.499 + \item {\tt multC0} theorem, 30
4.500 + \item {\tt multC_succ} theorem, 30
4.501
4.502 \indexspace
4.503
4.504 - \item {\tt N} constant, 72
4.505 - \item {\tt n_not_Suc_n} theorem, 25
4.506 - \item {\tt Nat} theory, 26
4.507 - \item {\textit {nat}} type, 25, 26
4.508 - \item {\textit{nat}} type, 24--27
4.509 - \item {\tt nat_induct} theorem, 25
4.510 - \item {\tt nat_rec} constant, 26
4.511 - \item {\tt NatDef} theory, 24
4.512 - \item {\tt NC0} theorem, 76
4.513 - \item {\tt NC_succ} theorem, 76
4.514 - \item {\tt NE} theorem, 75, 76, 84
4.515 - \item {\tt NEL} theorem, 76
4.516 - \item {\tt NF} theorem, 76, 85
4.517 - \item {\tt NI0} theorem, 76
4.518 - \item {\tt NI_succ} theorem, 76
4.519 - \item {\tt NI_succL} theorem, 76
4.520 - \item {\tt NIO} theorem, 84
4.521 - \item {\tt Not} constant, 6, 59
4.522 - \item {\tt not_def} theorem, 10
4.523 - \item {\tt not_sym} theorem, 11
4.524 - \item {\tt notE} theorem, 11
4.525 - \item {\tt notI} theorem, 11
4.526 - \item {\tt notL} theorem, 61
4.527 - \item {\tt notnotD} theorem, 12
4.528 - \item {\tt notR} theorem, 61
4.529 - \item {\tt null} constant, 28
4.530 + \item {\tt N} constant, 19
4.531 + \item {\tt NC0} theorem, 23
4.532 + \item {\tt NC_succ} theorem, 23
4.533 + \item {\tt NE} theorem, 22, 23, 31
4.534 + \item {\tt NEL} theorem, 23
4.535 + \item {\tt NF} theorem, 23, 32
4.536 + \item {\tt NI0} theorem, 23
4.537 + \item {\tt NI_succ} theorem, 23
4.538 + \item {\tt NI_succL} theorem, 23
4.539 + \item {\tt NIO} theorem, 31
4.540 + \item {\tt Not} constant, 6
4.541 + \item {\tt notL} theorem, 8
4.542 + \item {\tt notR} theorem, 8
4.543
4.544 \indexspace
4.545
4.546 - \item {\textit {o}} type, 58
4.547 - \item {\tt o} symbol, 6, 17
4.548 - \item {\tt o_def} theorem, 10
4.549 - \item {\tt of} symbol, 9
4.550 - \item {\tt or_def} theorem, 10
4.551 - \item {\tt Ord} theory, 7
4.552 - \item {\tt ord} class, 7, 8, 26
4.553 - \item {\tt order} class, 7, 26
4.554 + \item {\textit {o}} type, 5
4.555
4.556 \indexspace
4.557
4.558 - \item {\tt pack} ML type, 64
4.559 - \item {\tt Pair} constant, 23
4.560 - \item {\tt pair} constant, 72
4.561 - \item {\tt Pair_eq} theorem, 23
4.562 - \item {\tt Pair_inject} theorem, 23
4.563 - \item {\tt PairE} theorem, 23
4.564 - \item {\tt pc_tac}, \bold{66}, \bold{82}, 88, 89
4.565 - \item {\tt plus} class, 7
4.566 - \item {\tt PlusC_inl} theorem, 78
4.567 - \item {\tt PlusC_inr} theorem, 78
4.568 - \item {\tt PlusE} theorem, 78, 82, 86
4.569 - \item {\tt PlusEL} theorem, 78
4.570 - \item {\tt PlusF} theorem, 78
4.571 - \item {\tt PlusFL} theorem, 78
4.572 - \item {\tt PlusI_inl} theorem, 78, 87
4.573 - \item {\tt PlusI_inlL} theorem, 78
4.574 - \item {\tt PlusI_inr} theorem, 78
4.575 - \item {\tt PlusI_inrL} theorem, 78
4.576 - \item {\tt Pow} constant, 14
4.577 - \item {\tt Pow_def} theorem, 17
4.578 - \item {\tt PowD} theorem, 19
4.579 - \item {\tt PowI} theorem, 19
4.580 - \item {\tt primrec}, 45--48
4.581 - \item {\tt primrec} symbol, 26
4.582 + \item {\tt pack} ML type, 11
4.583 + \item {\tt pair} constant, 19
4.584 + \item {\tt pc_tac}, \bold{13}, \bold{29}, 35, 36
4.585 + \item {\tt PlusC_inl} theorem, 25
4.586 + \item {\tt PlusC_inr} theorem, 25
4.587 + \item {\tt PlusE} theorem, 25, 29, 33
4.588 + \item {\tt PlusEL} theorem, 25
4.589 + \item {\tt PlusF} theorem, 25
4.590 + \item {\tt PlusFL} theorem, 25
4.591 + \item {\tt PlusI_inl} theorem, 25, 34
4.592 + \item {\tt PlusI_inlL} theorem, 25
4.593 + \item {\tt PlusI_inr} theorem, 25
4.594 + \item {\tt PlusI_inrL} theorem, 25
4.595 \item priorities, 3
4.596 - \item {\tt PROD} symbol, 73, 74
4.597 - \item {\tt Prod} constant, 72
4.598 - \item {\tt Prod} theory, 23
4.599 - \item {\tt ProdC} theorem, 76, 92
4.600 - \item {\tt ProdC2} theorem, 76
4.601 - \item {\tt ProdE} theorem, 76, 89, 91, 93
4.602 - \item {\tt ProdEL} theorem, 76
4.603 - \item {\tt ProdF} theorem, 76
4.604 - \item {\tt ProdFL} theorem, 76
4.605 - \item {\tt ProdI} theorem, 76, 82, 84
4.606 - \item {\tt ProdIL} theorem, 76
4.607 - \item {\tt prop_cs}, \bold{22}
4.608 - \item {\tt prop_pack}, \bold{65}
4.609 + \item {\tt PROD} symbol, 20, 21
4.610 + \item {\tt Prod} constant, 19
4.611 + \item {\tt ProdC} theorem, 23, 39
4.612 + \item {\tt ProdC2} theorem, 23
4.613 + \item {\tt ProdE} theorem, 23, 36, 38, 40
4.614 + \item {\tt ProdEL} theorem, 23
4.615 + \item {\tt ProdF} theorem, 23
4.616 + \item {\tt ProdFL} theorem, 23
4.617 + \item {\tt ProdI} theorem, 23, 29, 31
4.618 + \item {\tt ProdIL} theorem, 23
4.619 + \item {\tt prop_pack}, \bold{12}
4.620
4.621 \indexspace
4.622
4.623 - \item {\tt qed_spec_mp}, 43
4.624 + \item {\tt rec} constant, 19, 22
4.625 + \item {\tt red_if_equal} theorem, 22
4.626 + \item {\tt Reduce} constant, 19, 22, 28
4.627 + \item {\tt refl} theorem, 8
4.628 + \item {\tt refl_elem} theorem, 22, 26
4.629 + \item {\tt refl_red} theorem, 22
4.630 + \item {\tt refl_type} theorem, 22, 26
4.631 + \item {\tt REPEAT_FIRST}, 27
4.632 + \item {\tt repeat_goal_tac}, \bold{13}
4.633 + \item {\tt replace_type} theorem, 26, 38
4.634 + \item {\tt reresolve_tac}, \bold{13}
4.635 + \item {\tt rew_tac}, \bold{28}
4.636 + \item {\tt RL}, 33
4.637 + \item {\tt RS}, 38, 40
4.638
4.639 \indexspace
4.640
4.641 - \item {\tt range} constant, 14, 56
4.642 - \item {\tt range_def} theorem, 17
4.643 - \item {\tt rangeE} theorem, 19, 56
4.644 - \item {\tt rangeI} theorem, 19
4.645 - \item {\tt rec} constant, 72, 75
4.646 - \item {\tt recdef}, 48--51
4.647 - \item {\tt record}, 33
4.648 - \item {\tt record_split_tac}, 35, 36
4.649 - \item recursion
4.650 - \subitem general, 48--51
4.651 - \subitem primitive, 45--48
4.652 - \item recursive functions, \see{recursion}{44}
4.653 - \item {\tt red_if_equal} theorem, 75
4.654 - \item {\tt Reduce} constant, 72, 75, 81
4.655 - \item {\tt refl} theorem, 9, 61
4.656 - \item {\tt refl_elem} theorem, 75, 79
4.657 - \item {\tt refl_red} theorem, 75
4.658 - \item {\tt refl_type} theorem, 75, 79
4.659 - \item {\tt REPEAT_FIRST}, 80
4.660 - \item {\tt repeat_goal_tac}, \bold{66}
4.661 - \item {\tt replace_type} theorem, 79, 91
4.662 - \item {\tt reresolve_tac}, \bold{66}
4.663 - \item {\tt res_inst_tac}, 8
4.664 - \item {\tt rev} constant, 28
4.665 - \item {\tt rew_tac}, \bold{81}
4.666 - \item {\tt RL}, 86
4.667 - \item {\tt RS}, 91, 93
4.668 + \item {\tt safe_goal_tac}, \bold{13}
4.669 + \item {\tt safe_tac}, \bold{29}
4.670 + \item {\tt safestep_tac}, \bold{29}
4.671 + \item {\tt Seqof} constant, 6
4.672 + \item sequent calculus, 5--17
4.673 + \item {\tt snd} constant, 19, 24
4.674 + \item {\tt snd_def} theorem, 24
4.675 + \item {\tt sobj} type, 9
4.676 + \item {\tt split} constant, 19, 33
4.677 + \item {\tt step_tac}, \bold{13}, \bold{29}
4.678 + \item {\tt subst_elem} theorem, 22
4.679 + \item {\tt subst_elemL} theorem, 22
4.680 + \item {\tt subst_eqtyparg} theorem, 26, 38
4.681 + \item {\tt subst_prodE} theorem, 24, 26
4.682 + \item {\tt subst_type} theorem, 22
4.683 + \item {\tt subst_typeL} theorem, 22
4.684 + \item {\tt succ} constant, 19
4.685 + \item {\tt SUM} symbol, 20, 21
4.686 + \item {\tt Sum} constant, 19
4.687 + \item {\tt SumC} theorem, 24
4.688 + \item {\tt SumE} theorem, 24, 29, 33
4.689 + \item {\tt SumE_fst} theorem, 24, 26, 38, 39
4.690 + \item {\tt SumE_snd} theorem, 24, 26, 40
4.691 + \item {\tt SumEL} theorem, 24
4.692 + \item {\tt SumF} theorem, 24
4.693 + \item {\tt SumFL} theorem, 24
4.694 + \item {\tt SumI} theorem, 24, 34
4.695 + \item {\tt SumIL} theorem, 24
4.696 + \item {\tt SumIL2} theorem, 26
4.697 + \item {\tt sym} theorem, 8
4.698 + \item {\tt sym_elem} theorem, 22
4.699 + \item {\tt sym_type} theorem, 22
4.700 + \item {\tt symL} theorem, 9
4.701
4.702 \indexspace
4.703
4.704 - \item {\tt safe_goal_tac}, \bold{66}
4.705 - \item {\tt safe_tac}, \bold{82}
4.706 - \item {\tt safestep_tac}, \bold{82}
4.707 - \item search
4.708 - \subitem best-first, 57
4.709 - \item {\tt select_equality} theorem, 10, 12
4.710 - \item {\tt selectI} theorem, 9, 10
4.711 - \item {\tt Seqof} constant, 59
4.712 - \item sequent calculus, 58--70
4.713 - \item {\tt Set} theory, 13, 16
4.714 - \item {\tt set} constant, 28
4.715 - \item {\tt set} type, 13
4.716 - \item {\tt set_diff_def} theorem, 17
4.717 - \item {\tt show_sorts}, 8
4.718 - \item {\tt show_types}, 8
4.719 - \item {\tt Sigma} constant, 23
4.720 - \item {\tt Sigma_def} theorem, 23
4.721 - \item {\tt SigmaE} theorem, 23
4.722 - \item {\tt SigmaI} theorem, 23
4.723 - \item simplification
4.724 - \subitem of conjunctions, 21
4.725 - \item {\tt size} constant, 40
4.726 - \item {\tt snd} constant, 23, 72, 77
4.727 - \item {\tt snd_conv} theorem, 23
4.728 - \item {\tt snd_def} theorem, 77
4.729 - \item {\tt sobj} type, 62
4.730 - \item {\tt spec} theorem, 12
4.731 - \item {\tt split} constant, 23, 72, 86
4.732 - \item {\tt split} theorem, 23
4.733 - \item {\tt split_all_tac}, \bold{24}
4.734 - \item {\tt split_if} theorem, 12, 22
4.735 - \item {\tt split_list_case} theorem, 27
4.736 - \item {\tt split_split} theorem, 23
4.737 - \item {\tt split_sum_case} theorem, 25
4.738 - \item {\tt ssubst} theorem, 11, 13
4.739 - \item {\tt stac}, \bold{21}
4.740 - \item {\tt step_tac}, \bold{66}, \bold{82}
4.741 - \item {\tt strip_tac}, \bold{13}
4.742 - \item {\tt subset_def} theorem, 17
4.743 - \item {\tt subset_refl} theorem, 18
4.744 - \item {\tt subset_trans} theorem, 18
4.745 - \item {\tt subsetCE} theorem, 16, 18
4.746 - \item {\tt subsetD} theorem, 16, 18
4.747 - \item {\tt subsetI} theorem, 18
4.748 - \item {\tt subst} theorem, 9
4.749 - \item {\tt subst_elem} theorem, 75
4.750 - \item {\tt subst_elemL} theorem, 75
4.751 - \item {\tt subst_eqtyparg} theorem, 79, 91
4.752 - \item {\tt subst_prodE} theorem, 77, 79
4.753 - \item {\tt subst_type} theorem, 75
4.754 - \item {\tt subst_typeL} theorem, 75
4.755 - \item {\tt Suc} constant, 25
4.756 - \item {\tt Suc_not_Zero} theorem, 25
4.757 - \item {\tt succ} constant, 72
4.758 - \item {\tt SUM} symbol, 73, 74
4.759 - \item {\tt Sum} constant, 72
4.760 - \item {\tt Sum} theory, 24
4.761 - \item {\tt sum_case} constant, 25
4.762 - \item {\tt sum_case_Inl} theorem, 25
4.763 - \item {\tt sum_case_Inr} theorem, 25
4.764 - \item {\tt SumC} theorem, 77
4.765 - \item {\tt SumE} theorem, 77, 82, 86
4.766 - \item {\tt sumE} theorem, 25
4.767 - \item {\tt SumE_fst} theorem, 77, 79, 91, 92
4.768 - \item {\tt SumE_snd} theorem, 77, 79, 93
4.769 - \item {\tt SumEL} theorem, 77
4.770 - \item {\tt SumF} theorem, 77
4.771 - \item {\tt SumFL} theorem, 77
4.772 - \item {\tt SumI} theorem, 77, 87
4.773 - \item {\tt SumIL} theorem, 77
4.774 - \item {\tt SumIL2} theorem, 79
4.775 - \item {\tt surj} constant, 17, 21
4.776 - \item {\tt surj_def} theorem, 21
4.777 - \item {\tt surjective_pairing} theorem, 23
4.778 - \item {\tt surjective_sum} theorem, 25
4.779 - \item {\tt swap} theorem, 12
4.780 - \item {\tt swap_res_tac}, 57
4.781 - \item {\tt sym} theorem, 11, 61
4.782 - \item {\tt sym_elem} theorem, 75
4.783 - \item {\tt sym_type} theorem, 75
4.784 - \item {\tt symL} theorem, 62
4.785 + \item {\tt T} constant, 19
4.786 + \item {\textit {t}} type, 18
4.787 + \item {\tt TC} theorem, 25
4.788 + \item {\tt TE} theorem, 25
4.789 + \item {\tt TEL} theorem, 25
4.790 + \item {\tt term} class, 5
4.791 + \item {\tt test_assume_tac}, \bold{27}
4.792 + \item {\tt TF} theorem, 25
4.793 + \item {\tt THE} symbol, 6
4.794 + \item {\tt The} constant, 6
4.795 + \item {\tt The} theorem, 8
4.796 + \item {\tt thinL} theorem, 8
4.797 + \item {\tt thinR} theorem, 8
4.798 + \item {\tt TI} theorem, 25
4.799 + \item {\tt trans} theorem, 8
4.800 + \item {\tt trans_elem} theorem, 22
4.801 + \item {\tt trans_red} theorem, 22
4.802 + \item {\tt trans_type} theorem, 22
4.803 + \item {\tt True} constant, 6
4.804 + \item {\tt True_def} theorem, 8
4.805 + \item {\tt Trueprop} constant, 6
4.806 + \item {\tt TrueR} theorem, 9
4.807 + \item {\tt tt} constant, 19
4.808 + \item {\tt Type} constant, 19
4.809 + \item {\tt typechk_tac}, \bold{27}, 32, 35, 39, 40
4.810
4.811 \indexspace
4.812
4.813 - \item {\tt T} constant, 72
4.814 - \item {\textit {t}} type, 71
4.815 - \item {\tt take} constant, 28
4.816 - \item {\tt takeWhile} constant, 28
4.817 - \item {\tt TC} theorem, 78
4.818 - \item {\tt TE} theorem, 78
4.819 - \item {\tt TEL} theorem, 78
4.820 - \item {\tt term} class, 7, 58
4.821 - \item {\tt test_assume_tac}, \bold{80}
4.822 - \item {\tt TF} theorem, 78
4.823 - \item {\tt THE} symbol, 59
4.824 - \item {\tt The} constant, 59
4.825 - \item {\tt The} theorem, 61
4.826 - \item {\tt thinL} theorem, 61
4.827 - \item {\tt thinR} theorem, 61
4.828 - \item {\tt TI} theorem, 78
4.829 - \item {\tt times} class, 7
4.830 - \item {\tt tl} constant, 28
4.831 - \item tracing
4.832 - \subitem of unification, 8
4.833 - \item {\tt trans} theorem, 11, 61
4.834 - \item {\tt trans_elem} theorem, 75
4.835 - \item {\tt trans_red} theorem, 75
4.836 - \item {\tt trans_type} theorem, 75
4.837 - \item {\tt True} constant, 6, 59
4.838 - \item {\tt True_def} theorem, 10, 61
4.839 - \item {\tt True_or_False} theorem, 9, 10
4.840 - \item {\tt TrueI} theorem, 11
4.841 - \item {\tt Trueprop} constant, 6, 59
4.842 - \item {\tt TrueR} theorem, 62
4.843 - \item {\tt tt} constant, 72
4.844 - \item {\tt Type} constant, 72
4.845 - \item type definition, \bold{30}
4.846 - \item {\tt typechk_tac}, \bold{80}, 85, 88, 92, 93
4.847 - \item {\tt typedef}, 27
4.848 + \item {\tt when} constant, 19, 24, 33
4.849
4.850 \indexspace
4.851
4.852 - \item {\tt UN} symbol, 14--16
4.853 - \item {\tt Un} symbol, 14
4.854 - \item {\tt Un1} theorem, 16
4.855 - \item {\tt Un2} theorem, 16
4.856 - \item {\tt Un_absorb} theorem, 20
4.857 - \item {\tt Un_assoc} theorem, 20
4.858 - \item {\tt Un_commute} theorem, 20
4.859 - \item {\tt Un_def} theorem, 17
4.860 - \item {\tt UN_E} theorem, 19
4.861 - \item {\tt UN_I} theorem, 19
4.862 - \item {\tt Un_Int_distrib} theorem, 20
4.863 - \item {\tt Un_Inter} theorem, 20
4.864 - \item {\tt Un_least} theorem, 20
4.865 - \item {\tt Un_Union_image} theorem, 20
4.866 - \item {\tt Un_upper1} theorem, 20
4.867 - \item {\tt Un_upper2} theorem, 20
4.868 - \item {\tt UnCI} theorem, 16, 19
4.869 - \item {\tt UnE} theorem, 19
4.870 - \item {\tt UnI1} theorem, 19
4.871 - \item {\tt UnI2} theorem, 19
4.872 - \item unification
4.873 - \subitem incompleteness of, 8
4.874 - \item {\tt Unify.trace_types}, 8
4.875 - \item {\tt UNION} constant, 14
4.876 - \item {\tt Union} constant, 14
4.877 - \item {\tt UNION1} constant, 14
4.878 - \item {\tt UNION1_def} theorem, 17
4.879 - \item {\tt UNION_def} theorem, 17
4.880 - \item {\tt Union_def} theorem, 17
4.881 - \item {\tt Union_least} theorem, 20
4.882 - \item {\tt Union_Un_distrib} theorem, 20
4.883 - \item {\tt Union_upper} theorem, 20
4.884 - \item {\tt UnionE} theorem, 19
4.885 - \item {\tt UnionI} theorem, 19
4.886 - \item {\tt unit_eq} theorem, 24
4.887 -
4.888 - \indexspace
4.889 -
4.890 - \item {\tt when} constant, 72, 77, 86
4.891 -
4.892 - \indexspace
4.893 -
4.894 - \item {\tt zero_ne_succ} theorem, 75, 76
4.895 - \item {\tt ZF} theory, 5
4.896 + \item {\tt zero_ne_succ} theorem, 22, 23
4.897
4.898 \end{theindex}
5.1 --- a/doc-src/Logics/logics.tex Tue May 04 18:04:45 1999 +0200
5.2 +++ b/doc-src/Logics/logics.tex Tue May 04 18:05:34 1999 +0200
5.3 @@ -21,15 +21,12 @@
5.4 Computer Laboratory \\ University of Cambridge \\
5.5 \texttt{lcp@cl.cam.ac.uk}\\[3ex]
5.6 With Contributions by Tobias Nipkow and Markus Wenzel%
5.7 -\thanks{Tobias Nipkow revised and extended
5.8 - the chapter on \HOL. Markus Wenzel made numerous improvements.
5.9 - Philippe de Groote wrote the
5.10 - first version of the logic~\LK{}. Tobias
5.11 - Nipkow developed~\HOL{}, \LCF{} and~\Cube{}. Martin Coen
5.12 - developed~\Modal{} with assistance from Rajeev Gor\'e. The research has
5.13 - been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
5.14 - GR/K77051) and by ESPRIT project 6453: Types.}
5.15 -}
5.16 + \thanks{Markus Wenzel made numerous improvements. Philippe de Groote
5.17 + wrote the first version of the logic~\LK{}. Tobias Nipkow developed
5.18 + \LCF{} and~\Cube{}. Martin Coen developed~\Modal{} with assistance
5.19 + from Rajeev Gor\'e. The research has been funded by the EPSRC
5.20 + (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT
5.21 + project 6453: Types.} }
5.22
5.23 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
5.24 \hrule\bigskip}
5.25 @@ -50,13 +47,12 @@
5.26 \pagenumbering{roman} \tableofcontents \clearfirst
5.27 \include{preface}
5.28 \include{syntax}
5.29 -\include{HOL}
5.30 \include{LK}
5.31 %%\include{Modal}
5.32 \include{CTT}
5.33 %%\include{Cube}
5.34 %%\include{LCF}
5.35 \bibliographystyle{plain}
5.36 -\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref}
5.37 +\bibliography{bib,string,general,atp,theory,funprog,logicprog,isabelle,crossref}
5.38 \input{logics.ind}
5.39 \end{document}
6.1 --- a/doc-src/Logics/preface.tex Tue May 04 18:04:45 1999 +0200
6.2 +++ b/doc-src/Logics/preface.tex Tue May 04 18:05:34 1999 +0200
6.3 @@ -5,10 +5,21 @@
6.4 starting points for defining new logics. Each logic is distributed with
6.5 sample proofs, some of which are described in this document.
6.6
6.7 -The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set
6.8 -theory) are described in a separate manual~\cite{isabelle-ZF}. Here are the
6.9 -others:
6.10 +\texttt{HOL} is currently the best developed Isabelle object-logic, including
6.11 +an extensive library of (concrete) mathematics, and various packages for
6.12 +advanced definitional concepts (like (co-)inductive sets and types,
6.13 +well-founded recursion etc.). The distribution also includes some large
6.14 +applications. See the separate manual \emph{Isabelle's Logics: HOL}. There
6.15 +is also a comprehensive tutorial on Isabelle/HOL available.
6.16
6.17 +\texttt{ZF} provides another starting point for applications, with a slightly
6.18 +less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages
6.19 +are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides
6.20 +more advanced constructions for sets than simply-typed \texttt{HOL}.
6.21 +\texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
6.22 +in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.
6.23 +
6.24 +\medskip There are some further logics distributed with Isabelle:
6.25 \begin{ttdescription}
6.26 \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
6.27 which is the basis of a preliminary method for deriving programs from
6.28 @@ -17,14 +28,9 @@
6.29 \item[\thydx{LCF}] is a version of Scott's Logic for Computable
6.30 Functions, which is also implemented by the~{\sc lcf}
6.31 system~\cite{paulson87}. It is built upon classical~\FOL{}.
6.32 -
6.33 -\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
6.34 -which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
6.35 -This object-logic should not be confused with Isabelle's meta-logic, which is
6.36 -also a form of higher-order logic.
6.37 -
6.38 -\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an
6.39 - extension of \texttt{HOL}\@.
6.40 +
6.41 +\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
6.42 + \texttt{HOL}\@. %FIXME See \cite{MNOS98} for more details on \texttt{HOLCF}.
6.43
6.44 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
6.45 Theory~\cite{nordstrom90}, with extensional equality. Universes are not
6.46 @@ -44,19 +50,20 @@
6.47 \item[\thydx{ILL}] implements intuitionistic linear logic.
6.48 \end{ttdescription}
6.49
6.50 -The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt
6.51 - Cube} are undocumented. All object-logics' sources are
6.52 -distributed with Isabelle (see the directory \texttt{src}). They are
6.53 -also available for browsing on the WWW at
6.54 +The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt
6.55 + Cube} are undocumented. All object-logics' sources are distributed with
6.56 +Isabelle (see the directory \texttt{src}). They are also available for
6.57 +browsing on the WWW at
6.58 \begin{ttbox}
6.59 http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/
6.60 http://isabelle.in.tum.de/library/
6.61 \end{ttbox}
6.62 Note that this is not necessarily consistent with your local sources!
6.63
6.64 -\medskip Do not read this manual before reading \emph{Introduction to
6.65 - Isabelle} and performing some Isabelle proofs. Consult the {\em Reference
6.66 - Manual} for more information on tactics, packages, etc.
6.67 +\medskip Do not read the \emph{Isabelle's Logics} manuals before reading
6.68 +\emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and
6.69 +performing some Isabelle proofs. Consult the {\em Reference Manual} for more
6.70 +information on tactics, packages, etc.
6.71
6.72
6.73 %%% Local Variables: