104

1 
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 



3 
ruleshell.ML


4 


5 
\idx{refl} t = t::'a


6 
\idx{subst} [ s = t; P(s) ] ==> P(t::'a)


7 
\idx{abs},!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x)))


8 
\idx{disch} (P ==> Q) ==> P>Q


9 
\idx{mp} [ P>Q; P ] ==> Q


10 


11 
\idx{True_def} True = ((%x.x)=(%x.x))


12 
\idx{All_def} All = (%P. P = (%x.True))


13 
\idx{Ex_def} Ex = (%P. P(Eps(P)))


14 
\idx{False_def} False = (!P.P)


15 
\idx{not_def} not = (%P. P>False)


16 
\idx{and_def} op & = (%P Q. !R. (P>Q>R) > R)


17 
\idx{or_def} op  = (%P Q. !R. (P>R) > (Q>R) > R)


18 
\idx{Ex1_def} Ex1 == (%P. ? x. P(x) & (! y. P(y) > y=x))


19 


20 
\idx{iff} (P>Q) > (Q>P) > (P=Q)


21 
\idx{True_or_False} (P=True)  (P=False)


22 
\idx{select} P(x::'a) > P(Eps(P))


23 


24 
\idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y)


25 
\idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x)))


26 
\idx{Cond_def} Cond = (%P x y.@z::'a. (P=True > z=x) & (P=False > z=y))


27 


28 



29 
lemmas.ML


30 


31 
\idx{sym} s=t ==> t=s


32 
\idx{trans} [ r=s; s=t ] ==> r=t


33 
\idx{box_equals}


34 
[ a=b; a=c; b=d ] ==> c=d


35 
\idx{ap_term} s=t ==> f(s)=f(t)


36 
\idx{ap_thm} s::'a=>'b = t ==> s(x)=t(x)


37 
\idx{cong}


38 
[ f = g; x::'a = y ] ==> f(x) = g(y)


39 
\idx{iffI}


40 
[ P ==> Q; Q ==> P ] ==> P=Q


41 
\idx{iffD1} [ P=Q; Q ] ==> P


42 
\idx{iffE}


43 
[ P=Q; [ P > Q; Q > P ] ==> R ] ==> R


44 
\idx{eqTrueI} P ==> P=True


45 
\idx{eqTrueE} P=True ==> P


46 
\idx{allI} (!!x::'a. P(x)) ==> !x. P(x)


47 
\idx{spec} !x::'a.P(x) ==> P(x)


48 
\idx{allE} [ !x.P(x); P(x) ==> R ] ==> R


49 
\idx{all_dupE}


50 
[ ! x.P(x); [ P(x); ! x.P(x) ] ==> R


51 
] ==> R


52 
\idx{FalseE} False ==> P


53 
\idx{False_neq_True} False=True ==> P


54 
\idx{notI} (P ==> False) ==> ~P


55 
\idx{notE} [ ~P; P ] ==> R


56 
\idx{impE} [ P>Q; P; Q ==> R ] ==> R


57 
\idx{rev_mp} [ P; P > Q ] ==> Q


58 
\idx{contrapos} [ ~Q; P==>Q ] ==> ~P


59 
\idx{exI} P(x) ==> ? x::'a.P(x)


60 
\idx{exE} [ ? x::'a.P(x); !!x. P(x) ==> Q ] ==> Q


61 


62 
\idx{conjI} [ P; Q ] ==> P&Q


63 
\idx{conjunct1} [ P & Q ] ==> P


64 
\idx{conjunct2} [ P & Q ] ==> Q


65 
\idx{conjE} [ P&Q; [ P; Q ] ==> R ] ==> R


66 
\idx{disjI1} P ==> PQ


67 
\idx{disjI2} Q ==> PQ


68 
\idx{disjE} [ P  Q; P ==> R; Q ==> R ] ==> R


69 
\idx{ccontr} (~P ==> False) ==> P


70 
\idx{classical} (~P ==> P) ==> P


71 
\idx{notnotD} ~~P ==> P


72 
\idx{ex1I}


73 
[ P(a); !!x. P(x) ==> x=a ] ==> ?! x. P(x)


74 
\idx{ex1E}


75 
[ ?! x.P(x); !!x. [ P(x); ! y. P(y) > y=x ] ==> R ] ==> R


76 
\idx{select_equality}


77 
[ P(a); !!x. P(x) ==> x=a ] ==> (@x.P(x)) = a


78 
\idx{disjCI} (~Q ==> P) ==> PQ


79 
\idx{excluded_middle} ~P  P


80 
\idx{impCE} [ P>Q; ~P ==> R; Q ==> R ] ==> R


81 
\idx{iffCE}


82 
[ P=Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R


83 
\idx{exCI} (! x. ~P(x) ==> P(a)) ==> ? x.P(x)


84 
\idx{swap} ~P ==> (~Q ==> P) ==> Q


85 


86 



87 
simpdata.ML


88 


89 
\idx{if_True} Cond(True,x,y) = x


90 
\idx{if_False} Cond(False,x,y) = y


91 
\idx{if_P} P ==> Cond(P,x,y) = x


92 
\idx{if_not_P} ~P ==> Cond(P,x,y) = y


93 
\idx{expand_if}


94 
P(Cond(Q,x,y)) = ((Q > P(x)) & (~Q > P(y)))


95 


96 



97 
\idx{set.ML}


98 


99 
\idx{CollectI} [ P(a) ] ==> a : \{x.P(x)\}


100 
\idx{CollectD} [ a : \{x.P(x)\} ] ==> P(a)


101 
\idx{set_ext} [ !!x. (x:A) = (x:B) ] ==> A = B


102 


103 
\idx{Ball_def} Ball(A,P) == ! x. x:A > P(x)


104 
\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)


105 
\idx{subset_def} A <= B == ! x:A. x:B


106 
\idx{Un_def} A Un B == \{x.x:A  x:B\}


107 
\idx{Int_def} A Int B == \{x.x:A & x:B\}


108 
\idx{Compl_def} Compl(A) == \{x. ~x:A\}


109 
\idx{Inter_def} Inter(S) == \{x. ! A:S. x:A\}


110 
\idx{Union_def} Union(S) == \{x. ? A:S. x:A\}


111 
\idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}


112 
\idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}


113 
\idx{mono_def} mono(f) == (!A B. A <= B > f(A) <= f(B))


114 
\idx{image_def} f``A == \{y. ? x:A. y=f(x)\}


115 
\idx{singleton_def} \{a\} == \{x.x=a\}


116 
\idx{range_def} range(f) == \{y. ? x. y=f(x)\}


117 
\idx{One_One_def} One_One(f) == ! x y. f(x)=f(y) > x=y


118 
\idx{One_One_on_def} One_One_on(f,A) == !x y. x:A > y:A > f(x)=f(y) > x=y


119 
\idx{Onto_def} Onto(f) == ! y. ? x. y=f(x)


120 


121 


122 
\idx{Collect_cong} [ !!x. P(x)=Q(x) ] ==> \{x. P(x)\} = \{x. Q(x)\}


123 


124 
\idx{ballI} [ !!x. x:A ==> P(x) ] ==> ! x:A. P(x)


125 
\idx{bspec} [ ! x:A. P(x); x:A ] ==> P(x)


126 
\idx{ballE} [ ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q ] ==> Q


127 


128 
\idx{bexI} [ P(x); x:A ] ==> ? x:A. P(x)


129 
\idx{bexCI} [ ! x:A. ~P(x) ==> P(a); a:A ] ==> ? x:A.P(x)


130 
\idx{bexE} [ ? x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q


131 


132 
\idx{ball_cong}


133 
[ A=A'; !!x. x:A' ==> P(x) = P'(x) ] ==>


134 
(! x:A. P(x)) = (! x:A'. P'(x))


135 


136 
\idx{bex_cong}


137 
[ A=A'; !!x. x:A' ==> P(x) = P'(x) ] ==>


138 
(? x:A. P(x)) = (? x:A'. P'(x))


139 


140 
\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B


141 
\idx{subsetD} [ A <= B; c:A ] ==> c:B


142 
\idx{subsetCE} [ A <= B; ~(c:A) ==> P; c:B ==> P ] ==> P


143 


144 
\idx{subset_refl} A <= A


145 
\idx{subset_antisym} [ A <= B; B <= A ] ==> A = B


146 
\idx{subset_trans} [ A<=B; B<=C ] ==> A<=C


147 


148 
\idx{equalityD1} A = B ==> A<=B


149 
\idx{equalityD2} A = B ==> B<=A


150 
\idx{equalityE} [ A = B; [ A<=B; B<=A ] ==> P ] ==> P


151 


152 
\idx{singletonI} a : \{a\}


153 
\idx{singletonD} b : \{a\} ==> b=a


154 


155 
\idx{imageI} [ x:A ] ==> f(x) : f``A


156 
\idx{imageE} [ b : f``A; !!x.[ b=f(x); x:A ] ==> P ] ==> P


157 


158 
\idx{rangeI} f(x) : range(f)


159 
\idx{rangeE} [ b : range(f); !!x.[ b=f(x) ] ==> P ] ==> P


160 


161 
\idx{UnionI} [ X:C; A:X ] ==> A : Union(C)


162 
\idx{UnionE} [ A : Union(C); !!X.[ A:X; X:C ] ==> R ] ==> R


163 


164 
\idx{InterI} [ !!X. X:C ==> A:X ] ==> A : Inter(C)


165 
\idx{InterD} [ A : Inter(C); X:C ] ==> A:X


166 
\idx{InterE} [ A : Inter(C); A:X ==> R; ~ X:C ==> R ] ==> R


167 


168 
\idx{UN_I} [ a:A; b: B(a) ] ==> b: (UN x:A. B(x))


169 
\idx{UN_E} [ b : (UN x:A. B(x)); !!x.[ x:A; b: B(x) ] ==> R ] ==> R


170 


171 
\idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))


172 
\idx{INT_D} [ b : (INT x:A. B(x)); a:A ] ==> b: B(a)


173 
\idx{INT_E} [ b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R ] ==> R


174 


175 
\idx{UnI1} c:A ==> c : A Un B


176 
\idx{UnI2} c:B ==> c : A Un B


177 
\idx{UnCI} (~c:B ==> c:A) ==> c : A Un B


178 
\idx{UnE} [ c : A Un B; c:A ==> P; c:B ==> P ] ==> P


179 


180 
\idx{IntI} [ c:A; c:B ] ==> c : A Int B


181 
\idx{IntD1} c : A Int B ==> c:A


182 
\idx{IntD2} c : A Int B ==> c:B


183 
\idx{IntE} [ c : A Int B; [ c:A; c:B ] ==> P ] ==> P


184 


185 
\idx{ComplI} [ c:A ==> False ] ==> c : Compl(A)


186 
\idx{ComplD} [ c : Compl(A) ] ==> ~c:A


187 


188 
\idx{monoI} [ !!A B. A <= B ==> f(A) <= f(B) ] ==> mono(f)


189 
\idx{monoD} [ mono(f); A <= B ] ==> f(A) <= f(B)


190 


191 


192 



193 
\idx{fun.ML}


194 


195 
\idx{One_OneI} [ !! x y. f(x) = f(y) ==> x=y ] ==> One_One(f)


196 
\idx{One_One_inverseI} (!!x. g(f(x)) = x) ==> One_One(f)


197 
\idx{One_OneD} [ One_One(f); f(x) = f(y) ] ==> x=y


198 


199 
\idx{Inv_f_f} One_One(f) ==> Inv(f,f(x)) = x


200 
\idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y


201 


202 
\idx{Inv_injective}


203 
[ Inv(f,x)=Inv(f,y); x: range(f); y: range(f) ] ==> x=y


204 


205 
\idx{One_One_onI}


206 
(!! x y. [ f(x) = f(y); x:A; y:A ] ==> x=y) ==> One_One_on(f,A)


207 


208 
\idx{One_One_on_inverseI}


209 
(!!x. x:A ==> g(f(x)) = x) ==> One_One_on(f,A)


210 


211 
\idx{One_One_onD}


212 
[ One_One_on(f,A); f(x)=f(y); x:A; y:A ] ==> x=y


213 


214 
\idx{One_One_on_contraD}


215 
[ One_One_on(f,A); ~x=y; x:A; y:A ] ==> ~ f(x)=f(y)


216 


217 


218 



219 
\idx{subset.ML}


220 


221 
\idx{Union_upper} B:A ==> B <= Union(A)


222 
\idx{Union_least} [ !!X. X:A ==> X<=C ] ==> Union(A) <= C


223 


224 
\idx{Inter_lower} B:A ==> Inter(A) <= B


225 
\idx{Inter_greatest} [ !!X. X:A ==> C<=X ] ==> C <= Inter(A)


226 


227 
\idx{Un_upper1} A <= A Un B


228 
\idx{Un_upper2} B <= A Un B


229 
\idx{Un_least} [ A<=C; B<=C ] ==> A Un B <= C


230 


231 
\idx{Int_lower1} A Int B <= A


232 
\idx{Int_lower2} A Int B <= B


233 
\idx{Int_greatest} [ C<=A; C<=B ] ==> C <= A Int B


234 


235 


236 



237 
\idx{equalities.ML}


238 


239 
\idx{Int_absorb} A Int A = A


240 
\idx{Int_commute} A Int B = B Int A


241 
\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)


242 
\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)


243 


244 
\idx{Un_absorb} A Un A = A


245 
\idx{Un_commute} A Un B = B Un A


246 
\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)


247 
\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)


248 


249 
\idx{Compl_disjoint} A Int Compl(A) = \{x.False\}


250 
\idx{Compl_partition A Un Compl(A) = \{x.True\}


251 
\idx{double_complement} Compl(Compl(A)) = A


252 


253 


254 
\idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)


255 
\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)


256 


257 
\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)


258 
\idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C)


259 
\idx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)


260 


261 
\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)


262 
\idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C)


263 
\idx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)


264 


265 


266 



267 
prod.ML


268 


269 
mixfix = [ Delimfix((1<_,/_>), ['a,'b] => ('a,'b)prod, Pair),


270 
TInfixl(*, prod, 20) ],


271 
thy = extend_theory Set.thy Prod


272 
[([prod],([[term],[term]],term))],


273 
([fst], 'a * 'b => 'a),


274 
([snd], 'a * 'b => 'b),


275 
([split], ['a * 'b, ['a,'b]=>'c] => 'c)],


276 
\idx{fst_def} fst(p) == @a. ? b. p = <a,b>),


277 
\idx{snd_def} snd(p) == @b. ? a. p = <a,b>),


278 
\idx{split_def} split(p,c) == c(fst(p),snd(p)))


279 


280 
\idx{Pair_inject} [ <a, b> = <a',b'>; [ a=a'; b=b' ] ==> R ] ==> R


281 


282 
\idx{fst_conv} fst(<a,b>) = a


283 
\idx{snd_conv} snd(<a,b>) = b


284 
\idx{split_conv} split(<a,b>, c) = c(a,b)


285 


286 
\idx{surjective_pairing} p = <fst(p),snd(p)>


287 


288 



289 
sum.ML


290 


291 
mixfix = [TInfixl(+, sum, 10)],


292 
thy = extend_theory Prod.thy sum


293 
[([sum], ([[term],[term]],term))],


294 
[Inl], 'a => 'a+'b),


295 
[Inr], 'b => 'a+'b),


296 
[when], ['a+'b, 'a=>'c, 'b=>'c] =>'c)],


297 
\idx{when_def} when == (%p f g. @z. (!x. p=Inl(x) > z=f(x))


298 
& (!y. p=Inr(y) > z=g(y))))


299 


300 
\idx{Inl_not_Inr} ~ (Inl(a) = Inr(b))


301 


302 
\idx{One_One_Inl} One_One(Inl)


303 


304 
\idx{One_One_Inr} One_One(Inr)


305 


306 
\idx{when_Inl_conv} when(Inl(x), f, g) = f(x)


307 


308 
\idx{when_Inr_conv} when(Inr(x), f, g) = g(x)


309 


310 
\idx{sumE}


311 
[ !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y))


312 
] ==> P(s)


313 


314 
\idx{surjective_sum} when(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)


315 


316 


317 
????????????????????????????????????????????????????????????????


318 
trancl?


319 


320 



321 
nat.ML


322 


323 
Sext\{mixfix=[Delimfix(0, nat, 0),


324 
Infixl(<,[nat,nat] => bool,50)],


325 
thy = extend_theory Trancl.thy Nat


326 
[nat], ([],term))


327 
[nat_case], [nat, 'a, nat=>'a] =>'a),


328 
[pred_nat],nat*nat) set),


329 
[nat_rec], [nat, 'a, [nat, 'a]=>'a] => 'a)


330 


331 
\idx{nat_case_def} nat_case == (%n a f. @z. (n=0 > z=a)


332 
& (!x. n=Suc(x) > z=f(x)))),


333 
\idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\} ),


334 
\idx{less_def} m<n == <m,n>:trancl(pred_nat)),


335 
\idx{nat_rec_def}


336 
nat_rec(n,c,d) == wfrec(trancl(pred_nat),


337 
%rec l. nat_case(l, c, %m. d(m,rec(m))),


338 
n) )


339 


340 
\idx{nat_induct} [ P(0); !!k. [ P(k) ] ==> P(Suc(k)) ] ==> P(n)


341 


342 


343 
\idx{Suc_not_Zero} ~ (Suc(m) = 0)


344 
\idx{One_One_Suc} One_One(Suc)


345 
\idx{n_not_Suc_n} ~(n=Suc(n))


346 


347 
\idx{nat_case_0_conv} nat_case(0, a, f) = a


348 


349 
\idx{nat_case_Suc_conv} nat_case(Suc(k), a, f) = f(k)


350 


351 
\idx{pred_natI} <n, Suc(n)> : pred_nat


352 
\idx{pred_natE}


353 
[ p : pred_nat; !!x n. [ p = <n, Suc(n)> ] ==> R


354 
] ==> R


355 


356 
\idx{wf_pred_nat} wf(pred_nat)


357 


358 
\idx{nat_rec_0_conv} nat_rec(0,c,h) = c


359 


360 
\idx{nat_rec_Suc_conv} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))


361 


362 


363 
(*** Basic properties of less than ***)


364 
\idx{less_trans} [ i<j; j<k ] ==> i<k


365 
\idx{lessI} n < Suc(n)


366 
\idx{zero_less_Suc} 0 < Suc(n)


367 


368 
\idx{less_not_sym} n<m > ~m<n


369 
\idx{less_not_refl} ~ (n<n)


370 
\idx{not_less0} ~ (n<0)


371 


372 
\idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)


373 
\idx{less_induct} [ !!n. [ ! m. m<n > P(m) ] ==> P(n) ] ==> P(n)


374 


375 
\idx{less_linear} m<n  m=n  n<m


376 


377 


378 



379 
list.ML


380 


381 
[([list], ([[term]],term))],


382 
([Nil], 'a list),


383 
([Cons], ['a, 'a list] => 'a list),


384 
([list_rec], ['a list, 'b, ['a ,'a list, 'b]=>'b] => 'b),


385 
([list_all], ('a => bool) => ('a list => bool)),


386 
([map], ('a=>'b) => ('a list => 'b list))


387 


388 
\idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r)) )


389 


390 
\idx{list_induct}


391 
[ P(Nil);


392 
!!x xs. [ P(xs) ] ==> P(Cons(x,xs)) ] ==> P(l)


393 


394 
\idx{Cons_not_Nil} ~ Cons(x,xs) = Nil


395 
\idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)


396 


397 
\idx{list_rec_Nil_conv} list_rec(Nil,c,h) = c


398 
\idx{list_rec_Cons_conv} list_rec(Cons(a,l), c, h) =


399 
h(a, l, list_rec(l,c,h))


400 


401 
\idx{map_Nil_conv} map(f,Nil) = Nil


402 
\idx{map_Cons_conv} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))


403 
