15647

1 
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)


2 

17566

3 
theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin

14516

4 


5 
;setup_theory bool


6 


7 
constdefs


8 
ARB :: "'a"


9 
"ARB == SOME x. True"


10 


11 
lemma ARB_DEF: "ARB = (SOME x. True)"


12 
by (import bool ARB_DEF)


13 


14 
constdefs


15 
IN :: "'a => ('a => bool) => bool"


16 
"IN == %x f. f x"


17 


18 
lemma IN_DEF: "IN = (%x f. f x)"


19 
by (import bool IN_DEF)


20 


21 
constdefs


22 
RES_FORALL :: "('a => bool) => ('a => bool) => bool"


23 
"RES_FORALL == %p m. ALL x. IN x p > m x"


24 


25 
lemma RES_FORALL_DEF: "RES_FORALL = (%p m. ALL x. IN x p > m x)"


26 
by (import bool RES_FORALL_DEF)


27 


28 
constdefs


29 
RES_EXISTS :: "('a => bool) => ('a => bool) => bool"


30 
"RES_EXISTS == %p m. EX x. IN x p & m x"


31 


32 
lemma RES_EXISTS_DEF: "RES_EXISTS = (%p m. EX x. IN x p & m x)"


33 
by (import bool RES_EXISTS_DEF)


34 


35 
constdefs


36 
RES_EXISTS_UNIQUE :: "('a => bool) => ('a => bool) => bool"


37 
"RES_EXISTS_UNIQUE ==


38 
%p m. RES_EXISTS p m &


39 
RES_FORALL p (%x. RES_FORALL p (%y. m x & m y > x = y))"


40 


41 
lemma RES_EXISTS_UNIQUE_DEF: "RES_EXISTS_UNIQUE =


42 
(%p m. RES_EXISTS p m &


43 
RES_FORALL p (%x. RES_FORALL p (%y. m x & m y > x = y)))"


44 
by (import bool RES_EXISTS_UNIQUE_DEF)


45 


46 
constdefs


47 
RES_SELECT :: "('a => bool) => ('a => bool) => 'a"


48 
"RES_SELECT == %p m. SOME x. IN x p & m x"


49 


50 
lemma RES_SELECT_DEF: "RES_SELECT = (%p m. SOME x. IN x p & m x)"


51 
by (import bool RES_SELECT_DEF)


52 


53 
lemma EXCLUDED_MIDDLE: "ALL t. t  ~ t"


54 
by (import bool EXCLUDED_MIDDLE)


55 


56 
lemma FORALL_THM: "All f = All f"


57 
by (import bool FORALL_THM)


58 


59 
lemma EXISTS_THM: "Ex f = Ex f"


60 
by (import bool EXISTS_THM)


61 


62 
lemma F_IMP: "ALL t. ~ t > t > False"


63 
by (import bool F_IMP)


64 


65 
lemma NOT_AND: "~ (t & ~ t)"


66 
by (import bool NOT_AND)


67 


68 
lemma AND_CLAUSES: "ALL t.


69 
(True & t) = t &


70 
(t & True) = t & (False & t) = False & (t & False) = False & (t & t) = t"


71 
by (import bool AND_CLAUSES)


72 


73 
lemma OR_CLAUSES: "ALL t.


74 
(True  t) = True &


75 
(t  True) = True & (False  t) = t & (t  False) = t & (t  t) = t"


76 
by (import bool OR_CLAUSES)


77 


78 
lemma IMP_CLAUSES: "ALL t.


79 
(True > t) = t &


80 
(t > True) = True &


81 
(False > t) = True & (t > t) = True & (t > False) = (~ t)"


82 
by (import bool IMP_CLAUSES)


83 


84 
lemma NOT_CLAUSES: "(ALL t. (~ ~ t) = t) & (~ True) = False & (~ False) = True"


85 
by (import bool NOT_CLAUSES)


86 


87 
lemma BOOL_EQ_DISTINCT: "True ~= False & False ~= True"


88 
by (import bool BOOL_EQ_DISTINCT)


89 


90 
lemma EQ_CLAUSES: "ALL t.


91 
(True = t) = t &


92 
(t = True) = t & (False = t) = (~ t) & (t = False) = (~ t)"


93 
by (import bool EQ_CLAUSES)


94 


95 
lemma COND_CLAUSES: "ALL t1 t2. (if True then t1 else t2) = t1 & (if False then t1 else t2) = t2"


96 
by (import bool COND_CLAUSES)


97 


98 
lemma SELECT_UNIQUE: "ALL P x. (ALL y. P y = (y = x)) > Eps P = x"


99 
by (import bool SELECT_UNIQUE)


100 


101 
lemma BOTH_EXISTS_AND_THM: "ALL (P::bool) Q::bool. (EX x::'a. P & Q) = ((EX x::'a. P) & (EX x::'a. Q))"


102 
by (import bool BOTH_EXISTS_AND_THM)


103 


104 
lemma BOTH_FORALL_OR_THM: "ALL (P::bool) Q::bool.


105 
(ALL x::'a. P  Q) = ((ALL x::'a. P)  (ALL x::'a. Q))"


106 
by (import bool BOTH_FORALL_OR_THM)


107 


108 
lemma BOTH_FORALL_IMP_THM: "ALL (P::bool) Q::bool.


109 
(ALL x::'a. P > Q) = ((EX x::'a. P) > (ALL x::'a. Q))"


110 
by (import bool BOTH_FORALL_IMP_THM)


111 


112 
lemma BOTH_EXISTS_IMP_THM: "ALL (P::bool) Q::bool.


113 
(EX x::'a. P > Q) = ((ALL x::'a. P) > (EX x::'a. Q))"


114 
by (import bool BOTH_EXISTS_IMP_THM)


115 


116 
lemma OR_IMP_THM: "ALL A B. (A = (B  A)) = (B > A)"


117 
by (import bool OR_IMP_THM)


118 


119 
lemma DE_MORGAN_THM: "ALL A B. (~ (A & B)) = (~ A  ~ B) & (~ (A  B)) = (~ A & ~ B)"


120 
by (import bool DE_MORGAN_THM)


121 


122 
lemma IMP_F_EQ_F: "ALL t. (t > False) = (t = False)"


123 
by (import bool IMP_F_EQ_F)


124 


125 
lemma EQ_EXPAND: "ALL t1 t2. (t1 = t2) = (t1 & t2  ~ t1 & ~ t2)"


126 
by (import bool EQ_EXPAND)


127 


128 
lemma COND_RATOR: "ALL b f g x. (if b then f else g) x = (if b then f x else g x)"


129 
by (import bool COND_RATOR)


130 


131 
lemma COND_ABS: "ALL b f g. (%x. if b then f x else g x) = (if b then f else g)"


132 
by (import bool COND_ABS)


133 


134 
lemma COND_EXPAND: "ALL b t1 t2. (if b then t1 else t2) = ((~ b  t1) & (b  t2))"


135 
by (import bool COND_EXPAND)


136 


137 
lemma ONE_ONE_THM: "ALL f. inj f = (ALL x1 x2. f x1 = f x2 > x1 = x2)"


138 
by (import bool ONE_ONE_THM)


139 


140 
lemma ABS_REP_THM: "(All::(('a => bool) => bool) => bool)


141 
(%P::'a => bool.


142 
(op >::bool => bool => bool)


143 
((Ex::(('b => 'a) => bool) => bool)


144 
((TYPE_DEFINITION::('a => bool) => ('b => 'a) => bool) P))


145 
((Ex::(('b => 'a) => bool) => bool)


146 
(%x::'b => 'a.


147 
(Ex::(('a => 'b) => bool) => bool)


148 
(%abs::'a => 'b.


149 
(op &::bool => bool => bool)


150 
((All::('b => bool) => bool)


151 
(%a::'b. (op =::'b => 'b => bool) (abs (x a)) a))


152 
((All::('a => bool) => bool)


153 
(%r::'a.


154 
(op =::bool => bool => bool) (P r)


155 
((op =::'a => 'a => bool) (x (abs r)) r)))))))"


156 
by (import bool ABS_REP_THM)


157 


158 
lemma LET_RAND: "(P::'b => bool) (Let (M::'a) (N::'a => 'b)) = (let x::'a = M in P (N x))"


159 
by (import bool LET_RAND)


160 


161 
lemma LET_RATOR: "Let (M::'a) (N::'a => 'b => 'c) (b::'b) = (let x::'a = M in N x b)"


162 
by (import bool LET_RATOR)


163 


164 
lemma SWAP_FORALL_THM: "ALL P. (ALL x. All (P x)) = (ALL y x. P x y)"


165 
by (import bool SWAP_FORALL_THM)


166 


167 
lemma SWAP_EXISTS_THM: "ALL P. (EX x. Ex (P x)) = (EX y x. P x y)"


168 
by (import bool SWAP_EXISTS_THM)


169 


170 
lemma AND_CONG: "ALL P P' Q Q'. (Q > P = P') & (P' > Q = Q') > (P & Q) = (P' & Q')"


171 
by (import bool AND_CONG)


172 


173 
lemma OR_CONG: "ALL P P' Q Q'. (~ Q > P = P') & (~ P' > Q = Q') > (P  Q) = (P'  Q')"


174 
by (import bool OR_CONG)


175 


176 
lemma COND_CONG: "ALL P Q x x' y y'.


177 
P = Q & (Q > x = x') & (~ Q > y = y') >


178 
(if P then x else y) = (if Q then x' else y')"


179 
by (import bool COND_CONG)


180 


181 
lemma MONO_COND: "(x > y) > (z > w) > (if b then x else z) > (if b then y else w)"


182 
by (import bool MONO_COND)


183 


184 
lemma SKOLEM_THM: "ALL P. (ALL x. Ex (P x)) = (EX f. ALL x. P x (f x))"


185 
by (import bool SKOLEM_THM)


186 


187 
lemma bool_case_thm: "(ALL (e0::'a) e1::'a. (case True of True => e0  False => e1) = e0) &


188 
(ALL (e0::'a) e1::'a. (case False of True => e0  False => e1) = e1)"


189 
by (import bool bool_case_thm)


190 

14847

191 
lemma bool_case_ID: "ALL x b. (case b of True => x  _ => x) = x"

14516

192 
by (import bool bool_case_ID)


193 


194 
lemma boolAxiom: "ALL e0 e1. EX x. x True = e0 & x False = e1"


195 
by (import bool boolAxiom)


196 


197 
lemma UEXISTS_OR_THM: "ALL P Q. (EX! x. P x  Q x) > Ex1 P  Ex1 Q"


198 
by (import bool UEXISTS_OR_THM)


199 


200 
lemma UEXISTS_SIMP: "(EX! x::'a. (t::bool)) = (t & (ALL x::'a. All (op = x)))"


201 
by (import bool UEXISTS_SIMP)


202 


203 
consts


204 
RES_ABSTRACT :: "('a => bool) => ('a => 'b) => 'a => 'b"


205 


206 
specification (RES_ABSTRACT) RES_ABSTRACT_DEF: "(ALL (p::'a => bool) (m::'a => 'b) x::'a.


207 
IN x p > RES_ABSTRACT p m x = m x) &


208 
(ALL (p::'a => bool) (m1::'a => 'b) m2::'a => 'b.


209 
(ALL x::'a. IN x p > m1 x = m2 x) >


210 
RES_ABSTRACT p m1 = RES_ABSTRACT p m2)"


211 
by (import bool RES_ABSTRACT_DEF)


212 


213 
lemma BOOL_FUN_CASES_THM: "ALL f. f = (%b. True)  f = (%b. False)  f = (%b. b)  f = Not"


214 
by (import bool BOOL_FUN_CASES_THM)


215 


216 
lemma BOOL_FUN_INDUCT: "ALL P. P (%b. True) & P (%b. False) & P (%b. b) & P Not > All P"


217 
by (import bool BOOL_FUN_INDUCT)


218 


219 
;end_setup


220 


221 
;setup_theory combin


222 


223 
constdefs


224 
K :: "'a => 'b => 'a"


225 
"K == %x y. x"


226 


227 
lemma K_DEF: "K = (%x y. x)"


228 
by (import combin K_DEF)


229 


230 
constdefs


231 
S :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"


232 
"S == %f g x. f x (g x)"


233 


234 
lemma S_DEF: "S = (%f g x. f x (g x))"


235 
by (import combin S_DEF)


236 


237 
constdefs


238 
I :: "'a => 'a"


239 
"(op ==::('a => 'a) => ('a => 'a) => prop) (I::'a => 'a)


240 
((S::('a => ('a => 'a) => 'a) => ('a => 'a => 'a) => 'a => 'a)


241 
(K::'a => ('a => 'a) => 'a) (K::'a => 'a => 'a))"


242 


243 
lemma I_DEF: "(op =::('a => 'a) => ('a => 'a) => bool) (I::'a => 'a)


244 
((S::('a => ('a => 'a) => 'a) => ('a => 'a => 'a) => 'a => 'a)


245 
(K::'a => ('a => 'a) => 'a) (K::'a => 'a => 'a))"


246 
by (import combin I_DEF)


247 


248 
constdefs


249 
C :: "('a => 'b => 'c) => 'b => 'a => 'c"


250 
"C == %f x y. f y x"


251 


252 
lemma C_DEF: "C = (%f x y. f y x)"


253 
by (import combin C_DEF)


254 


255 
constdefs


256 
W :: "('a => 'a => 'b) => 'a => 'b"


257 
"W == %f x. f x x"


258 


259 
lemma W_DEF: "W = (%f x. f x x)"


260 
by (import combin W_DEF)


261 


262 
lemma I_THM: "ALL x. I x = x"


263 
by (import combin I_THM)


264 


265 
lemma I_o_ID: "ALL f. I o f = f & f o I = f"


266 
by (import combin I_o_ID)


267 


268 
;end_setup


269 


270 
;setup_theory sum


271 


272 
lemma ISL_OR_ISR: "ALL x. ISL x  ISR x"


273 
by (import sum ISL_OR_ISR)


274 


275 
lemma INL: "ALL x. ISL x > Inl (OUTL x) = x"


276 
by (import sum INL)


277 


278 
lemma INR: "ALL x. ISR x > Inr (OUTR x) = x"


279 
by (import sum INR)


280 


281 
lemma sum_case_cong: "ALL (M::'b + 'c) (M'::'b + 'c) (f::'b => 'a) g::'c => 'a.


282 
M = M' &


283 
(ALL x::'b. M' = Inl x > f x = (f'::'b => 'a) x) &


284 
(ALL y::'c. M' = Inr y > g y = (g'::'c => 'a) y) >


285 
sum_case f g M = sum_case f' g' M'"


286 
by (import sum sum_case_cong)


287 


288 
;end_setup


289 


290 
;setup_theory one


291 


292 
;end_setup


293 


294 
;setup_theory option


295 


296 
lemma option_CLAUSES: "(op &::bool => bool => bool)


297 
((All::('a => bool) => bool)


298 
(%x::'a.


299 
(All::('a => bool) => bool)


300 
(%y::'a.


301 
(op =::bool => bool => bool)


302 
((op =::'a option => 'a option => bool) ((Some::'a ~=> 'a) x)


303 
((Some::'a ~=> 'a) y))


304 
((op =::'a => 'a => bool) x y))))


305 
((op &::bool => bool => bool)


306 
((All::('a => bool) => bool)


307 
(%x::'a.


308 
(op =::'a => 'a => bool)


309 
((the::'a option => 'a) ((Some::'a ~=> 'a) x)) x))


310 
((op &::bool => bool => bool)


311 
((All::('a => bool) => bool)


312 
(%x::'a.


313 
(Not::bool => bool)


314 
((op =::'a option => 'a option => bool) (None::'a option)


315 
((Some::'a ~=> 'a) x))))


316 
((op &::bool => bool => bool)


317 
((All::('a => bool) => bool)


318 
(%x::'a.


319 
(Not::bool => bool)


320 
((op =::'a option => 'a option => bool) ((Some::'a ~=> 'a) x)


321 
(None::'a option))))


322 
((op &::bool => bool => bool)


323 
((All::('a => bool) => bool)


324 
(%x::'a.


325 
(op =::bool => bool => bool)


326 
((IS_SOME::'a option => bool) ((Some::'a ~=> 'a) x))


327 
(True::bool)))


328 
((op &::bool => bool => bool)


329 
((op =::bool => bool => bool)


330 
((IS_SOME::'a option => bool) (None::'a option)) (False::bool))


331 
((op &::bool => bool => bool)


332 
((All::('a option => bool) => bool)


333 
(%x::'a option.


334 
(op =::bool => bool => bool)


335 
((IS_NONE::'a option => bool) x)


336 
((op =::'a option => 'a option => bool) x


337 
(None::'a option))))


338 
((op &::bool => bool => bool)


339 
((All::('a option => bool) => bool)


340 
(%x::'a option.


341 
(op =::bool => bool => bool)


342 
((Not::bool => bool) ((IS_SOME::'a option => bool) x))


343 
((op =::'a option => 'a option => bool) x


344 
(None::'a option))))


345 
((op &::bool => bool => bool)


346 
((All::('a option => bool) => bool)


347 
(%x::'a option.


348 
(op >::bool => bool => bool)


349 
((IS_SOME::'a option => bool) x)


350 
((op =::'a option => 'a option => bool)


351 
((Some::'a ~=> 'a) ((the::'a option => 'a) x))


352 
x)))


353 
((op &::bool => bool => bool)


354 
((All::('a option => bool) => bool)


355 
(%x::'a option.


356 
(op =::'a option => 'a option => bool)


357 
((option_case::'a option


358 
=> ('a ~=> 'a) => 'a option ~=> 'a)


359 
(None::'a option) (Some::'a ~=> 'a) x)


360 
x))


361 
((op &::bool => bool => bool)


362 
((All::('a option => bool) => bool)


363 
(%x::'a option.


364 
(op =::'a option => 'a option => bool)


365 
((option_case::'a option


366 
=> ('a ~=> 'a) => 'a option ~=> 'a)


367 
x (Some::'a ~=> 'a) x)


368 
x))


369 
((op &::bool => bool => bool)


370 
((All::('a option => bool) => bool)


371 
(%x::'a option.


372 
(op >::bool => bool => bool)


373 
((IS_NONE::'a option => bool) x)


374 
((op =::'b => 'b => bool)


375 
((option_case::'b


376 
=> ('a => 'b) => 'a option => 'b)


377 
(e::'b) (f::'a => 'b) x)


378 
e)))


379 
((op &::bool => bool => bool)


380 
((All::('a option => bool) => bool)


381 
(%x::'a option.


382 
(op >::bool => bool => bool)


383 
((IS_SOME::'a option => bool) x)


384 
((op =::'b => 'b => bool)


385 
((option_case::'b


386 
=> ('a => 'b) => 'a option => 'b)


387 
e f x)


388 
(f ((the::'a option => 'a) x)))))


389 
((op &::bool => bool => bool)


390 
((All::('a option => bool) => bool)


391 
(%x::'a option.


392 
(op >::bool => bool => bool)


393 
((IS_SOME::'a option => bool) x)


394 
((op =::'a option => 'a option => bool)


395 
((option_case::'a option


396 
=> ('a ~=> 'a) => 'a option ~=> 'a)


397 
(ea::'a option) (Some::'a ~=> 'a) x)


398 
x)))


399 
((op &::bool => bool => bool)


400 
((All::('b => bool) => bool)


401 
(%u::'b.


402 
(All::(('a => 'b) => bool) => bool)


403 
(%f::'a => 'b.


404 
(op =::'b => 'b => bool)


405 
((option_case::'b => ('a => 'b) => 'a option => 'b) u f


406 
(None::'a option))


407 
u)))


408 
((op &::bool => bool => bool)


409 
((All::('b => bool) => bool)


410 
(%u::'b.


411 
(All::(('a => 'b) => bool) => bool)


412 
(%f::'a => 'b.


413 
(All::('a => bool) => bool)


414 
(%x::'a.


415 
(op =::'b => 'b => bool)


416 
((option_case::'b => ('a => 'b) => 'a option => 'b) u f


417 
((Some::'a ~=> 'a) x))


418 
(f x)))))


419 
((op &::bool => bool => bool)


420 
((All::(('a => 'b) => bool) => bool)


421 
(%f::'a => 'b.


422 
(All::('a => bool) => bool)


423 
(%x::'a.


424 
(op =::'b option => 'b option => bool)


425 
((option_map::('a => 'b) => 'a option ~=> 'b) f


426 
((Some::'a ~=> 'a) x))


427 
((Some::'b ~=> 'b) (f x)))))


428 
((op &::bool => bool => bool)


429 
((All::(('a => 'b) => bool) => bool)


430 
(%f::'a => 'b.


431 
(op =::'b option => 'b option => bool)


432 
((option_map::('a => 'b) => 'a option ~=> 'b) f (None::'a option))


433 
(None::'b option)))


434 
((op &::bool => bool => bool)


435 
((op =::'a option => 'a option => bool)


436 
((OPTION_JOIN::'a option option ~=> 'a) (None::'a option option))


437 
(None::'a option))


438 
((All::('a option => bool) => bool)


439 
(%x::'a option.


440 
(op =::'a option => 'a option => bool)


441 
((OPTION_JOIN::'a option option ~=> 'a)


442 
((Some::'a option ~=> 'a option) x))


443 
x))))))))))))))))))))"


444 
by (import option option_CLAUSES)


445 


446 
lemma option_case_compute: "option_case (e::'b) (f::'a => 'b) (x::'a option) =


447 
(if IS_SOME x then f (the x) else e)"


448 
by (import option option_case_compute)


449 


450 
lemma OPTION_MAP_EQ_SOME: "ALL f x y. (option_map f x = Some y) = (EX z. x = Some z & y = f z)"


451 
by (import option OPTION_MAP_EQ_SOME)


452 


453 
lemma OPTION_JOIN_EQ_SOME: "ALL x xa. (OPTION_JOIN x = Some xa) = (x = Some (Some xa))"


454 
by (import option OPTION_JOIN_EQ_SOME)


455 


456 
lemma option_case_cong: "ALL M M' u f.


457 
M = M' & (M' = None > u = u') & (ALL x. M' = Some x > f x = f' x) >


458 
option_case u f M = option_case u' f' M'"


459 
by (import option option_case_cong)


460 


461 
;end_setup


462 


463 
;setup_theory marker


464 


465 
consts


466 
stmarker :: "'a => 'a"


467 


468 
defs


469 
stmarker_primdef: "stmarker == %x. x"


470 


471 
lemma stmarker_def: "ALL x. stmarker x = x"


472 
by (import marker stmarker_def)


473 


474 
lemma move_left_conj: "ALL x xa xb.


475 
(x & stmarker xb) = (stmarker xb & x) &


476 
((stmarker xb & x) & xa) = (stmarker xb & x & xa) &


477 
(x & stmarker xb & xa) = (stmarker xb & x & xa)"


478 
by (import marker move_left_conj)


479 


480 
lemma move_right_conj: "ALL x xa xb.


481 
(stmarker xb & x) = (x & stmarker xb) &


482 
(x & xa & stmarker xb) = ((x & xa) & stmarker xb) &


483 
((x & stmarker xb) & xa) = ((x & xa) & stmarker xb)"


484 
by (import marker move_right_conj)


485 


486 
lemma move_left_disj: "ALL x xa xb.


487 
(x  stmarker xb) = (stmarker xb  x) &


488 
((stmarker xb  x)  xa) = (stmarker xb  x  xa) &


489 
(x  stmarker xb  xa) = (stmarker xb  x  xa)"


490 
by (import marker move_left_disj)


491 


492 
lemma move_right_disj: "ALL x xa xb.


493 
(stmarker xb  x) = (x  stmarker xb) &


494 
(x  xa  stmarker xb) = ((x  xa)  stmarker xb) &


495 
((x  stmarker xb)  xa) = ((x  xa)  stmarker xb)"


496 
by (import marker move_right_disj)


497 


498 
;end_setup


499 


500 
;setup_theory relation


501 


502 
constdefs


503 
TC :: "('a => 'a => bool) => 'a => 'a => bool"


504 
"TC ==


505 
%R a b.


506 
ALL P.


507 
(ALL x y. R x y > P x y) & (ALL x y z. P x y & P y z > P x z) >


508 
P a b"


509 


510 
lemma TC_DEF: "ALL R a b.


511 
TC R a b =


512 
(ALL P.


513 
(ALL x y. R x y > P x y) & (ALL x y z. P x y & P y z > P x z) >


514 
P a b)"


515 
by (import relation TC_DEF)


516 


517 
constdefs


518 
RTC :: "('a => 'a => bool) => 'a => 'a => bool"


519 
"RTC ==


520 
%R a b.


521 
ALL P. (ALL x. P x x) & (ALL x y z. R x y & P y z > P x z) > P a b"


522 


523 
lemma RTC_DEF: "ALL R a b.


524 
RTC R a b =


525 
(ALL P. (ALL x. P x x) & (ALL x y z. R x y & P y z > P x z) > P a b)"


526 
by (import relation RTC_DEF)


527 


528 
consts


529 
RC :: "('a => 'a => bool) => 'a => 'a => bool"


530 


531 
defs


532 
RC_primdef: "RC == %R x y. x = y  R x y"


533 


534 
lemma RC_def: "ALL R x y. RC R x y = (x = y  R x y)"


535 
by (import relation RC_def)


536 


537 
consts


538 
transitive :: "('a => 'a => bool) => bool"


539 


540 
defs


541 
transitive_primdef: "transitive == %R. ALL x y z. R x y & R y z > R x z"


542 


543 
lemma transitive_def: "ALL R. transitive R = (ALL x y z. R x y & R y z > R x z)"


544 
by (import relation transitive_def)


545 


546 
constdefs


547 
pred_reflexive :: "('a => 'a => bool) => bool"


548 
"pred_reflexive == %R. ALL x. R x x"


549 


550 
lemma reflexive_def: "ALL R. pred_reflexive R = (ALL x. R x x)"


551 
by (import relation reflexive_def)


552 


553 
lemma TC_TRANSITIVE: "ALL x. transitive (TC x)"


554 
by (import relation TC_TRANSITIVE)


555 


556 
lemma RTC_INDUCT: "ALL x xa.


557 
(ALL x. xa x x) & (ALL xb y z. x xb y & xa y z > xa xb z) >


558 
(ALL xb xc. RTC x xb xc > xa xb xc)"


559 
by (import relation RTC_INDUCT)


560 


561 
lemma TC_RULES: "ALL x.


562 
(ALL xa xb. x xa xb > TC x xa xb) &


563 
(ALL xa xb xc. TC x xa xb & TC x xb xc > TC x xa xc)"


564 
by (import relation TC_RULES)


565 


566 
lemma RTC_RULES: "ALL x.


567 
(ALL xa. RTC x xa xa) &


568 
(ALL xa xb xc. x xa xb & RTC x xb xc > RTC x xa xc)"


569 
by (import relation RTC_RULES)


570 


571 
lemma RTC_STRONG_INDUCT: "ALL R P.


572 
(ALL x. P x x) & (ALL x y z. R x y & RTC R y z & P y z > P x z) >


573 
(ALL x y. RTC R x y > P x y)"


574 
by (import relation RTC_STRONG_INDUCT)


575 


576 
lemma RTC_RTC: "ALL R x y. RTC R x y > (ALL z. RTC R y z > RTC R x z)"


577 
by (import relation RTC_RTC)


578 


579 
lemma RTC_TRANSITIVE: "ALL x. transitive (RTC x)"


580 
by (import relation RTC_TRANSITIVE)


581 


582 
lemma RTC_REFLEXIVE: "ALL R. pred_reflexive (RTC R)"


583 
by (import relation RTC_REFLEXIVE)


584 


585 
lemma RC_REFLEXIVE: "ALL R. pred_reflexive (RC R)"


586 
by (import relation RC_REFLEXIVE)


587 


588 
lemma TC_SUBSET: "ALL x xa xb. x xa xb > TC x xa xb"


589 
by (import relation TC_SUBSET)


590 


591 
lemma RTC_SUBSET: "ALL R x y. R x y > RTC R x y"


592 
by (import relation RTC_SUBSET)


593 


594 
lemma RC_SUBSET: "ALL R x y. R x y > RC R x y"


595 
by (import relation RC_SUBSET)


596 


597 
lemma RC_RTC: "ALL R x y. RC R x y > RTC R x y"


598 
by (import relation RC_RTC)


599 


600 
lemma TC_INDUCT: "ALL x xa.


601 
(ALL xb y. x xb y > xa xb y) &


602 
(ALL x y z. xa x y & xa y z > xa x z) >


603 
(ALL xb xc. TC x xb xc > xa xb xc)"


604 
by (import relation TC_INDUCT)


605 


606 
lemma TC_INDUCT_LEFT1: "ALL x xa.


607 
(ALL xb y. x xb y > xa xb y) &


608 
(ALL xb y z. x xb y & xa y z > xa xb z) >


609 
(ALL xb xc. TC x xb xc > xa xb xc)"


610 
by (import relation TC_INDUCT_LEFT1)


611 


612 
lemma TC_STRONG_INDUCT: "ALL R P.


613 
(ALL x y. R x y > P x y) &


614 
(ALL x y z. P x y & P y z & TC R x y & TC R y z > P x z) >


615 
(ALL u v. TC R u v > P u v)"


616 
by (import relation TC_STRONG_INDUCT)


617 


618 
lemma TC_STRONG_INDUCT_LEFT1: "ALL R P.


619 
(ALL x y. R x y > P x y) &


620 
(ALL x y z. R x y & P y z & TC R y z > P x z) >


621 
(ALL u v. TC R u v > P u v)"


622 
by (import relation TC_STRONG_INDUCT_LEFT1)


623 


624 
lemma TC_RTC: "ALL R x y. TC R x y > RTC R x y"


625 
by (import relation TC_RTC)


626 


627 
lemma RTC_TC_RC: "ALL R x y. RTC R x y > RC R x y  TC R x y"


628 
by (import relation RTC_TC_RC)


629 


630 
lemma TC_RC_EQNS: "ALL R. RC (TC R) = RTC R & TC (RC R) = RTC R"


631 
by (import relation TC_RC_EQNS)


632 


633 
lemma RC_IDEM: "ALL R. RC (RC R) = RC R"


634 
by (import relation RC_IDEM)


635 


636 
lemma TC_IDEM: "ALL R. TC (TC R) = TC R"


637 
by (import relation TC_IDEM)


638 


639 
lemma RTC_IDEM: "ALL R. RTC (RTC R) = RTC R"


640 
by (import relation RTC_IDEM)


641 


642 
lemma RTC_CASES1: "ALL x xa xb. RTC x xa xb = (xa = xb  (EX u. x xa u & RTC x u xb))"


643 
by (import relation RTC_CASES1)


644 


645 
lemma RTC_CASES2: "ALL x xa xb. RTC x xa xb = (xa = xb  (EX u. RTC x xa u & x u xb))"


646 
by (import relation RTC_CASES2)


647 


648 
lemma RTC_CASES_RTC_TWICE: "ALL x xa xb. RTC x xa xb = (EX u. RTC x xa u & RTC x u xb)"


649 
by (import relation RTC_CASES_RTC_TWICE)


650 


651 
lemma TC_CASES1: "ALL R x z. TC R x z > R x z  (EX y. R x y & TC R y z)"


652 
by (import relation TC_CASES1)


653 


654 
lemma TC_CASES2: "ALL R x z. TC R x z > R x z  (EX y. TC R x y & R y z)"


655 
by (import relation TC_CASES2)


656 


657 
lemma TC_MONOTONE: "ALL R Q. (ALL x y. R x y > Q x y) > (ALL x y. TC R x y > TC Q x y)"


658 
by (import relation TC_MONOTONE)


659 


660 
lemma RTC_MONOTONE: "ALL R Q. (ALL x y. R x y > Q x y) > (ALL x y. RTC R x y > RTC Q x y)"


661 
by (import relation RTC_MONOTONE)


662 


663 
constdefs


664 
WF :: "('a => 'a => bool) => bool"


665 
"WF == %R. ALL B. Ex B > (EX min. B min & (ALL b. R b min > ~ B b))"


666 


667 
lemma WF_DEF: "ALL R. WF R = (ALL B. Ex B > (EX min. B min & (ALL b. R b min > ~ B b)))"


668 
by (import relation WF_DEF)


669 


670 
lemma WF_INDUCTION_THM: "ALL R. WF R > (ALL P. (ALL x. (ALL y. R y x > P y) > P x) > All P)"


671 
by (import relation WF_INDUCTION_THM)


672 


673 
lemma WF_NOT_REFL: "ALL x xa xb. WF x > x xa xb > xa ~= xb"


674 
by (import relation WF_NOT_REFL)


675 


676 
constdefs


677 
EMPTY_REL :: "'a => 'a => bool"


678 
"EMPTY_REL == %x y. False"


679 


680 
lemma EMPTY_REL_DEF: "ALL x y. EMPTY_REL x y = False"


681 
by (import relation EMPTY_REL_DEF)


682 


683 
lemma WF_EMPTY_REL: "WF EMPTY_REL"


684 
by (import relation WF_EMPTY_REL)


685 


686 
lemma WF_SUBSET: "ALL x xa. WF x & (ALL xb y. xa xb y > x xb y) > WF xa"


687 
by (import relation WF_SUBSET)


688 


689 
lemma WF_TC: "ALL R. WF R > WF (TC R)"


690 
by (import relation WF_TC)


691 


692 
consts


693 
inv_image :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool"


694 


695 
defs


696 
inv_image_primdef: "relation.inv_image ==


697 
%(R::'b => 'b => bool) (f::'a => 'b) (x::'a) y::'a. R (f x) (f y)"


698 


699 
lemma inv_image_def: "ALL (R::'b => 'b => bool) f::'a => 'b.


700 
relation.inv_image R f = (%(x::'a) y::'a. R (f x) (f y))"


701 
by (import relation inv_image_def)


702 


703 
lemma WF_inv_image: "ALL (R::'b => 'b => bool) f::'a => 'b. WF R > WF (relation.inv_image R f)"


704 
by (import relation WF_inv_image)


705 


706 
constdefs


707 
RESTRICT :: "('a => 'b) => ('a => 'a => bool) => 'a => 'a => 'b"


708 
"RESTRICT == %f R x y. if R y x then f y else ARB"


709 


710 
lemma RESTRICT_DEF: "ALL f R x. RESTRICT f R x = (%y. if R y x then f y else ARB)"


711 
by (import relation RESTRICT_DEF)


712 


713 
lemma RESTRICT_LEMMA: "ALL x xa xb xc. xa xb xc > RESTRICT x xa xc xb = x xb"


714 
by (import relation RESTRICT_LEMMA)


715 


716 
consts


717 
approx :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => ('a => 'b) => bool"


718 


719 
defs


720 
approx_primdef: "approx == %R M x f. f = RESTRICT (%y. M (RESTRICT f R y) y) R x"


721 


722 
lemma approx_def: "ALL R M x f. approx R M x f = (f = RESTRICT (%y. M (RESTRICT f R y) y) R x)"


723 
by (import relation approx_def)


724 


725 
consts


726 
the_fun :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'a => 'b"


727 


728 
defs


729 
the_fun_primdef: "the_fun == %R M x. Eps (approx R M x)"


730 


731 
lemma the_fun_def: "ALL R M x. the_fun R M x = Eps (approx R M x)"


732 
by (import relation the_fun_def)


733 


734 
constdefs


735 
WFREC :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'b"


736 
"WFREC ==


737 
%R M x. M (RESTRICT (the_fun (TC R) (%f v. M (RESTRICT f R v) v) x) R x) x"


738 


739 
lemma WFREC_DEF: "ALL R M.


740 
WFREC R M =


741 
(%x. M (RESTRICT (the_fun (TC R) (%f v. M (RESTRICT f R v) v) x) R x) x)"


742 
by (import relation WFREC_DEF)


743 


744 
lemma WFREC_THM: "ALL R M. WF R > (ALL x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x)"


745 
by (import relation WFREC_THM)


746 


747 
lemma WFREC_COROLLARY: "ALL M R f. f = WFREC R M > WF R > (ALL x. f x = M (RESTRICT f R x) x)"


748 
by (import relation WFREC_COROLLARY)


749 


750 
lemma WF_RECURSION_THM: "ALL R. WF R > (ALL M. EX! f. ALL x. f x = M (RESTRICT f R x) x)"


751 
by (import relation WF_RECURSION_THM)


752 


753 
;end_setup


754 


755 
;setup_theory pair


756 


757 
lemma CURRY_ONE_ONE_THM: "(curry f = curry g) = (f = g)"


758 
by (import pair CURRY_ONE_ONE_THM)


759 

15647

760 
lemma UNCURRY_ONE_ONE_THM: "(op =::bool => bool => bool)


761 
((op =::('a * 'b => 'c) => ('a * 'b => 'c) => bool)


762 
((split::('a => 'b => 'c) => 'a * 'b => 'c) (f::'a => 'b => 'c))


763 
((split::('a => 'b => 'c) => 'a * 'b => 'c) (g::'a => 'b => 'c)))


764 
((op =::('a => 'b => 'c) => ('a => 'b => 'c) => bool) f g)"

14516

765 
by (import pair UNCURRY_ONE_ONE_THM)


766 


767 
lemma pair_Axiom: "ALL f. EX x. ALL xa y. x (xa, y) = f xa y"


768 
by (import pair pair_Axiom)


769 


770 
lemma UNCURRY_CONG: "ALL M M' f.


771 
M = M' & (ALL x y. M' = (x, y) > f x y = f' x y) >


772 
split f M = split f' M'"


773 
by (import pair UNCURRY_CONG)


774 


775 
lemma ELIM_PEXISTS: "(EX p. P (fst p) (snd p)) = (EX p1. Ex (P p1))"


776 
by (import pair ELIM_PEXISTS)


777 


778 
lemma ELIM_PFORALL: "(ALL p. P (fst p) (snd p)) = (ALL p1. All (P p1))"


779 
by (import pair ELIM_PFORALL)


780 

15647

781 
lemma PFORALL_THM: "(All::(('a => 'b => bool) => bool) => bool)


782 
(%x::'a => 'b => bool.


783 
(op =::bool => bool => bool)


784 
((All::('a => bool) => bool)


785 
(%xa::'a. (All::('b => bool) => bool) (x xa)))


786 
((All::('a * 'b => bool) => bool)


787 
((split::('a => 'b => bool) => 'a * 'b => bool) x)))"

14516

788 
by (import pair PFORALL_THM)


789 

15647

790 
lemma PEXISTS_THM: "(All::(('a => 'b => bool) => bool) => bool)


791 
(%x::'a => 'b => bool.


792 
(op =::bool => bool => bool)


793 
((Ex::('a => bool) => bool)


794 
(%xa::'a. (Ex::('b => bool) => bool) (x xa)))


795 
((Ex::('a * 'b => bool) => bool)


796 
((split::('a => 'b => bool) => 'a * 'b => bool) x)))"

14516

797 
by (import pair PEXISTS_THM)


798 

15647

799 
lemma LET2_RAND: "(All::(('c => 'd) => bool) => bool)


800 
(%x::'c => 'd.


801 
(All::('a * 'b => bool) => bool)


802 
(%xa::'a * 'b.


803 
(All::(('a => 'b => 'c) => bool) => bool)


804 
(%xb::'a => 'b => 'c.


805 
(op =::'d => 'd => bool)


806 
(x ((Let::'a * 'b => ('a * 'b => 'c) => 'c) xa


807 
((split::('a => 'b => 'c) => 'a * 'b => 'c) xb)))


808 
((Let::'a * 'b => ('a * 'b => 'd) => 'd) xa


809 
((split::('a => 'b => 'd) => 'a * 'b => 'd)


810 
(%(xa::'a) y::'b. x (xb xa y)))))))"

14516

811 
by (import pair LET2_RAND)


812 

15647

813 
lemma LET2_RATOR: "(All::('a1 * 'a2 => bool) => bool)


814 
(%x::'a1 * 'a2.


815 
(All::(('a1 => 'a2 => 'b => 'c) => bool) => bool)


816 
(%xa::'a1 => 'a2 => 'b => 'c.


817 
(All::('b => bool) => bool)


818 
(%xb::'b.


819 
(op =::'c => 'c => bool)


820 
((Let::'a1 * 'a2 => ('a1 * 'a2 => 'b => 'c) => 'b => 'c) x


821 
((split::('a1 => 'a2 => 'b => 'c)


822 
=> 'a1 * 'a2 => 'b => 'c)


823 
xa)


824 
xb)


825 
((Let::'a1 * 'a2 => ('a1 * 'a2 => 'c) => 'c) x


826 
((split::('a1 => 'a2 => 'c) => 'a1 * 'a2 => 'c)


827 
(%(x::'a1) y::'a2. xa x y xb))))))"

14516

828 
by (import pair LET2_RATOR)


829 


830 
lemma pair_case_cong: "ALL x xa xb.


831 
x = xa & (ALL x y. xa = (x, y) > xb x y = f' x y) >


832 
split xb x = split f' xa"


833 
by (import pair pair_case_cong)


834 


835 
constdefs


836 
LEX :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool"


837 
"LEX == %R1 R2 (s, t) (u, v). R1 s u  s = u & R2 t v"


838 


839 
lemma LEX_DEF: "ALL R1 R2. LEX R1 R2 = (%(s, t) (u, v). R1 s u  s = u & R2 t v)"


840 
by (import pair LEX_DEF)


841 


842 
lemma WF_LEX: "ALL x xa. WF x & WF xa > WF (LEX x xa)"


843 
by (import pair WF_LEX)


844 


845 
constdefs


846 
RPROD :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool"


847 
"RPROD == %R1 R2 (s, t) (u, v). R1 s u & R2 t v"


848 


849 
lemma RPROD_DEF: "ALL R1 R2. RPROD R1 R2 = (%(s, t) (u, v). R1 s u & R2 t v)"


850 
by (import pair RPROD_DEF)


851 


852 
lemma WF_RPROD: "ALL R Q. WF R & WF Q > WF (RPROD R Q)"


853 
by (import pair WF_RPROD)


854 


855 
;end_setup


856 


857 
;setup_theory num


858 


859 
;end_setup


860 


861 
;setup_theory prim_rec


862 


863 
lemma LESS_0_0: "0 < Suc 0"


864 
by (import prim_rec LESS_0_0)


865 


866 
lemma LESS_LEMMA1: "ALL x xa. x < Suc xa > x = xa  x < xa"


867 
by (import prim_rec LESS_LEMMA1)


868 


869 
lemma LESS_LEMMA2: "ALL m n. m = n  m < n > m < Suc n"


870 
by (import prim_rec LESS_LEMMA2)


871 


872 
lemma LESS_THM: "ALL m n. (m < Suc n) = (m = n  m < n)"


873 
by (import prim_rec LESS_THM)


874 


875 
lemma LESS_SUC_IMP: "ALL x xa. x < Suc xa > x ~= xa > x < xa"


876 
by (import prim_rec LESS_SUC_IMP)


877 


878 
lemma EQ_LESS: "ALL n. Suc m = n > m < n"


879 
by (import prim_rec EQ_LESS)


880 


881 
lemma NOT_LESS_EQ: "ALL (m::nat) n::nat. m = n > ~ m < n"


882 
by (import prim_rec NOT_LESS_EQ)


883 


884 
constdefs


885 
SIMP_REC_REL :: "(nat => 'a) => 'a => ('a => 'a) => nat => bool"

14847

886 
"(op ==::((nat => 'a) => 'a => ('a => 'a) => nat => bool)


887 
=> ((nat => 'a) => 'a => ('a => 'a) => nat => bool) => prop)


888 
(SIMP_REC_REL::(nat => 'a) => 'a => ('a => 'a) => nat => bool)


889 
(%(fun::nat => 'a) (x::'a) (f::'a => 'a) n::nat.


890 
(op &::bool => bool => bool)


891 
((op =::'a => 'a => bool) (fun (0::nat)) x)


892 
((All::(nat => bool) => bool)


893 
(%m::nat.


894 
(op >::bool => bool => bool) ((op <::nat => nat => bool) m n)


895 
((op =::'a => 'a => bool) (fun ((Suc::nat => nat) m))


896 
(f (fun m))))))"


897 


898 
lemma SIMP_REC_REL: "(All::((nat => 'a) => bool) => bool)


899 
(%fun::nat => 'a.


900 
(All::('a => bool) => bool)


901 
(%x::'a.


902 
(All::(('a => 'a) => bool) => bool)


903 
(%f::'a => 'a.


904 
(All::(nat => bool) => bool)


905 
(%n::nat.


906 
(op =::bool => bool => bool)


907 
((SIMP_REC_REL::(nat => 'a)


908 
=> 'a => ('a => 'a) => nat => bool)


909 
fun x f n)


910 
((op &::bool => bool => bool)


911 
((op =::'a => 'a => bool) (fun (0::nat)) x)


912 
((All::(nat => bool) => bool)


913 
(%m::nat.


914 
(op >::bool => bool => bool)


915 
((op <::nat => nat => bool) m n)


916 
((op =::'a => 'a => bool)


917 
(fun ((Suc::nat => nat) m))


918 
(f (fun m))))))))))"

14516

919 
by (import prim_rec SIMP_REC_REL)


920 


921 
lemma SIMP_REC_EXISTS: "ALL x f n. EX fun. SIMP_REC_REL fun x f n"


922 
by (import prim_rec SIMP_REC_EXISTS)


923 


924 
lemma SIMP_REC_REL_UNIQUE: "ALL x xa xb xc xd xe.


925 
SIMP_REC_REL xb x xa xd & SIMP_REC_REL xc x xa xe >


926 
(ALL n. n < xd & n < xe > xb n = xc n)"


927 
by (import prim_rec SIMP_REC_REL_UNIQUE)


928 


929 
lemma SIMP_REC_REL_UNIQUE_RESULT: "ALL x f n. EX! y. EX g. SIMP_REC_REL g x f (Suc n) & y = g n"


930 
by (import prim_rec SIMP_REC_REL_UNIQUE_RESULT)


931 


932 
consts


933 
SIMP_REC :: "'a => ('a => 'a) => nat => 'a"


934 


935 
specification (SIMP_REC) SIMP_REC: "ALL x f' n. EX g. SIMP_REC_REL g x f' (Suc n) & SIMP_REC x f' n = g n"


936 
by (import prim_rec SIMP_REC)


937 


938 
lemma LESS_SUC_SUC: "ALL m. m < Suc m & m < Suc (Suc m)"


939 
by (import prim_rec LESS_SUC_SUC)


940 


941 
lemma SIMP_REC_THM: "ALL x f.


942 
SIMP_REC x f 0 = x & (ALL m. SIMP_REC x f (Suc m) = f (SIMP_REC x f m))"


943 
by (import prim_rec SIMP_REC_THM)


944 


945 
constdefs


946 
PRE :: "nat => nat"


947 
"PRE == %m. if m = 0 then 0 else SOME n. m = Suc n"


948 


949 
lemma PRE_DEF: "ALL m. PRE m = (if m = 0 then 0 else SOME n. m = Suc n)"


950 
by (import prim_rec PRE_DEF)


951 


952 
lemma PRE: "PRE 0 = 0 & (ALL m. PRE (Suc m) = m)"


953 
by (import prim_rec PRE)


954 


955 
constdefs


956 
PRIM_REC_FUN :: "'a => ('a => nat => 'a) => nat => nat => 'a"


957 
"PRIM_REC_FUN == %x f. SIMP_REC (%n. x) (%fun n. f (fun (PRE n)) n)"


958 


959 
lemma PRIM_REC_FUN: "ALL x f. PRIM_REC_FUN x f = SIMP_REC (%n. x) (%fun n. f (fun (PRE n)) n)"


960 
by (import prim_rec PRIM_REC_FUN)


961 


962 
lemma PRIM_REC_EQN: "ALL x f.


963 
(ALL n. PRIM_REC_FUN x f 0 n = x) &


964 
(ALL m n. PRIM_REC_FUN x f (Suc m) n = f (PRIM_REC_FUN x f m (PRE n)) n)"


965 
by (import prim_rec PRIM_REC_EQN)


966 


967 
constdefs


968 
PRIM_REC :: "'a => ('a => nat => 'a) => nat => 'a"


969 
"PRIM_REC == %x f m. PRIM_REC_FUN x f m (PRE m)"


970 


971 
lemma PRIM_REC: "ALL x f m. PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)"


972 
by (import prim_rec PRIM_REC)


973 


974 
lemma PRIM_REC_THM: "ALL x f.


975 
PRIM_REC x f 0 = x & (ALL m. PRIM_REC x f (Suc m) = f (PRIM_REC x f m) m)"


976 
by (import prim_rec PRIM_REC_THM)


977 


978 
lemma DC: "ALL P R a.


979 
P a & (ALL x. P x > (EX y. P y & R x y)) >


980 
(EX x. x 0 = a & (ALL n. P (x n) & R (x n) (x (Suc n))))"


981 
by (import prim_rec DC)


982 


983 
lemma num_Axiom_old: "ALL e f. EX! fn1. fn1 0 = e & (ALL n. fn1 (Suc n) = f (fn1 n) n)"


984 
by (import prim_rec num_Axiom_old)


985 


986 
lemma num_Axiom: "ALL e f. EX x. x 0 = e & (ALL n. x (Suc n) = f n (x n))"


987 
by (import prim_rec num_Axiom)


988 


989 
consts


990 
wellfounded :: "('a => 'a => bool) => bool"


991 


992 
defs


993 
wellfounded_primdef: "wellfounded == %R. ~ (EX f. ALL n. R (f (Suc n)) (f n))"


994 


995 
lemma wellfounded_def: "ALL R. wellfounded R = (~ (EX f. ALL n. R (f (Suc n)) (f n)))"


996 
by (import prim_rec wellfounded_def)


997 


998 
lemma WF_IFF_WELLFOUNDED: "ALL R. WF R = wellfounded R"


999 
by (import prim_rec WF_IFF_WELLFOUNDED)


1000 


1001 
lemma WF_PRED: "WF (%x y. y = Suc x)"


1002 
by (import prim_rec WF_PRED)


1003 


1004 
lemma WF_LESS: "(WF::(nat => nat => bool) => bool) (op <::nat => nat => bool)"


1005 
by (import prim_rec WF_LESS)


1006 


1007 
consts


1008 
measure :: "('a => nat) => 'a => 'a => bool"


1009 


1010 
defs


1011 
measure_primdef: "prim_rec.measure == relation.inv_image op <"


1012 


1013 
lemma measure_def: "prim_rec.measure = relation.inv_image op <"


1014 
by (import prim_rec measure_def)


1015 


1016 
lemma WF_measure: "ALL x. WF (prim_rec.measure x)"


1017 
by (import prim_rec WF_measure)


1018 


1019 
lemma measure_thm: "ALL x xa xb. prim_rec.measure x xa xb = (x xa < x xb)"


1020 
by (import prim_rec measure_thm)


1021 


1022 
;end_setup


1023 


1024 
;setup_theory arithmetic


1025 


1026 
constdefs


1027 
nat_elim__magic :: "nat => nat"


1028 
"nat_elim__magic == %n. n"


1029 


1030 
lemma nat_elim__magic: "ALL n. nat_elim__magic n = n"


1031 
by (import arithmetic nat_elim__magic)


1032 


1033 
consts


1034 
EVEN :: "nat => bool"


1035 


1036 
specification (EVEN) EVEN: "EVEN 0 = True & (ALL n. EVEN (Suc n) = (~ EVEN n))"


1037 
by (import arithmetic EVEN)


1038 


1039 
consts


1040 
ODD :: "nat => bool"


1041 


1042 
specification (ODD) ODD: "ODD 0 = False & (ALL n. ODD (Suc n) = (~ ODD n))"


1043 
by (import arithmetic ODD)


1044 


1045 
lemma TWO: "2 = Suc 1"


1046 
by (import arithmetic TWO)


1047 


1048 
lemma NORM_0: "(0::nat) = (0::nat)"


1049 
by (import arithmetic NORM_0)


1050 


1051 
lemma num_case_compute: "ALL n. nat_case f g n = (if n = 0 then f else g (PRE n))"


1052 
by (import arithmetic num_case_compute)


1053 


1054 
lemma ADD_CLAUSES: "0 + m = m & m + 0 = m & Suc m + n = Suc (m + n) & m + Suc n = Suc (m + n)"


1055 
by (import arithmetic ADD_CLAUSES)


1056 


1057 
lemma LESS_ADD: "ALL (m::nat) n::nat. n < m > (EX p::nat. p + n = m)"


1058 
by (import arithmetic LESS_ADD)


1059 


1060 
lemma LESS_ANTISYM: "ALL (m::nat) n::nat. ~ (m < n & n < m)"


1061 
by (import arithmetic LESS_ANTISYM)


1062 


1063 
lemma LESS_LESS_SUC: "ALL x xa. ~ (x < xa & xa < Suc x)"


1064 
by (import arithmetic LESS_LESS_SUC)


1065 


1066 
lemma FUN_EQ_LEMMA: "ALL f x1 x2. f x1 & ~ f x2 > x1 ~= x2"


1067 
by (import arithmetic FUN_EQ_LEMMA)


1068 


1069 
lemma LESS_NOT_SUC: "ALL m n. m < n & n ~= Suc m > Suc m < n"


1070 
by (import arithmetic LESS_NOT_SUC)


1071 


1072 
lemma LESS_0_CASES: "ALL m::nat. (0::nat) = m  (0::nat) < m"


1073 
by (import arithmetic LESS_0_CASES)


1074 


1075 
lemma LESS_CASES_IMP: "ALL (m::nat) n::nat. ~ m < n & m ~= n > n < m"


1076 
by (import arithmetic LESS_CASES_IMP)


1077 


1078 
lemma LESS_CASES: "ALL (m::nat) n::nat. m < n  n <= m"


1079 
by (import arithmetic LESS_CASES)


1080 


1081 
lemma LESS_EQ_SUC_REFL: "ALL m. m <= Suc m"


1082 
by (import arithmetic LESS_EQ_SUC_REFL)


1083 


1084 
lemma LESS_ADD_NONZERO: "ALL (m::nat) n::nat. n ~= (0::nat) > m < m + n"


1085 
by (import arithmetic LESS_ADD_NONZERO)


1086 


1087 
lemma LESS_EQ_ANTISYM: "ALL (x::nat) xa::nat. ~ (x < xa & xa <= x)"


1088 
by (import arithmetic LESS_EQ_ANTISYM)


1089 


1090 
lemma SUB_0: "ALL m::nat. (0::nat)  m = (0::nat) & m  (0::nat) = m"


1091 
by (import arithmetic SUB_0)


1092 


1093 
lemma SUC_SUB1: "ALL m. Suc m  1 = m"


1094 
by (import arithmetic SUC_SUB1)


1095 


1096 
lemma PRE_SUB1: "ALL m. PRE m = m  1"


1097 
by (import arithmetic PRE_SUB1)


1098 


1099 
lemma MULT_CLAUSES: "ALL x xa.


1100 
0 * x = 0 &


1101 
x * 0 = 0 &


1102 
1 * x = x &


1103 
x * 1 = x & Suc x * xa = x * xa + xa & x * Suc xa = x + x * xa"


1104 
by (import arithmetic MULT_CLAUSES)


1105 


1106 
lemma PRE_SUB: "ALL m n. PRE (m  n) = PRE m  n"


1107 
by (import arithmetic PRE_SUB)


1108 


1109 
lemma ADD_EQ_1: "ALL (m::nat) n::nat.


1110 
(m + n = (1::nat)) =


1111 
(m = (1::nat) & n = (0::nat)  m = (0::nat) & n = (1::nat))"


1112 
by (import arithmetic ADD_EQ_1)


1113 


1114 
lemma ADD_INV_0_EQ: "ALL (m::nat) n::nat. (m + n = m) = (n = (0::nat))"


1115 
by (import arithmetic ADD_INV_0_EQ)


1116 


1117 
lemma PRE_SUC_EQ: "ALL m n. 0 < n > (m = PRE n) = (Suc m = n)"


1118 
by (import arithmetic PRE_SUC_EQ)


1119 


1120 
lemma INV_PRE_EQ: "ALL m n. 0 < m & 0 < n > (PRE m = PRE n) = (m = n)"


1121 
by (import arithmetic INV_PRE_EQ)


1122 


1123 
lemma LESS_SUC_NOT: "ALL m n. m < n > ~ n < Suc m"


1124 
by (import arithmetic LESS_SUC_NOT)


1125 


1126 
lemma ADD_EQ_SUB: "ALL (m::nat) (n::nat) p::nat. n <= p > (m + n = p) = (m = p  n)"


1127 
by (import arithmetic ADD_EQ_SUB)


1128 


1129 
lemma LESS_ADD_1: "ALL (x::nat) xa::nat. xa < x > (EX xb::nat. x = xa + (xb + (1::nat)))"


1130 
by (import arithmetic LESS_ADD_1)


1131 


1132 
lemma NOT_ODD_EQ_EVEN: "ALL n m. Suc (n + n) ~= m + m"


1133 
by (import arithmetic NOT_ODD_EQ_EVEN)


1134 


1135 
lemma MULT_SUC_EQ: "ALL p m n. (n * Suc p = m * Suc p) = (n = m)"


1136 
by (import arithmetic MULT_SUC_EQ)


1137 


1138 
lemma MULT_EXP_MONO: "ALL p q n m. (n * Suc q ^ p = m * Suc q ^ p) = (n = m)"


1139 
by (import arithmetic MULT_EXP_MONO)


1140 


1141 
lemma LESS_ADD_SUC: "ALL m n. m < m + Suc n"


1142 
by (import arithmetic LESS_ADD_SUC)


1143 


1144 
lemma LESS_OR_EQ_ADD: "ALL (n::nat) m::nat. n < m  (EX p::nat. n = p + m)"


1145 
by (import arithmetic LESS_OR_EQ_ADD)


1146 

14847

1147 
lemma WOP: "(All::((nat => bool) => bool) => bool)


1148 
(%P::nat => bool.


1149 
(op >::bool => bool => bool) ((Ex::(nat => bool) => bool) P)


1150 
((Ex::(nat => bool) => bool)


1151 
(%n::nat.


1152 
(op &::bool => bool => bool) (P n)


1153 
((All::(nat => bool) => bool)


1154 
(%m::nat.


1155 
(op >::bool => bool => bool)


1156 
((op <::nat => nat => bool) m n)


1157 
((Not::bool => bool) (P m)))))))"

14516

1158 
by (import arithmetic WOP)


1159 

15647

1160 
lemma INV_PRE_LESS: "ALL m>0. ALL n. (PRE m < PRE n) = (m < n)"

14516

1161 
by (import arithmetic INV_PRE_LESS)


1162 

15647

1163 
lemma INV_PRE_LESS_EQ: "ALL n>0. ALL m. (PRE m <= PRE n) = (m <= n)"

14516

1164 
by (import arithmetic INV_PRE_LESS_EQ)


1165 


1166 
lemma SUB_EQ_EQ_0: "ALL (m::nat) n::nat. (m  n = m) = (m = (0::nat)  n = (0::nat))"


1167 
by (import arithmetic SUB_EQ_EQ_0)


1168 


1169 
lemma SUB_LESS_OR: "ALL (m::nat) n::nat. n < m > n <= m  (1::nat)"


1170 
by (import arithmetic SUB_LESS_OR)


1171 


1172 
lemma LESS_SUB_ADD_LESS: "ALL (n::nat) (m::nat) i::nat. i < n  m > i + m < n"


1173 
by (import arithmetic LESS_SUB_ADD_LESS)


1174 


1175 
lemma LESS_EQ_SUB_LESS: "ALL (x::nat) xa::nat. xa <= x > (ALL c::nat. (x  xa < c) = (x < xa + c))"


1176 
by (import arithmetic LESS_EQ_SUB_LESS)


1177 


1178 
lemma NOT_SUC_LESS_EQ: "ALL x xa. (~ Suc x <= xa) = (xa <= x)"


1179 
by (import arithmetic NOT_SUC_LESS_EQ)


1180 


1181 
lemma SUB_LESS_EQ_ADD: "ALL (m::nat) p::nat. m <= p > (ALL n::nat. (p  m <= n) = (p <= m + n))"


1182 
by (import arithmetic SUB_LESS_EQ_ADD)


1183 


1184 
lemma SUB_CANCEL: "ALL (x::nat) (xa::nat) xb::nat.


1185 
xa <= x & xb <= x > (x  xa = x  xb) = (xa = xb)"


1186 
by (import arithmetic SUB_CANCEL)


1187 


1188 
lemma NOT_EXP_0: "ALL m n. Suc n ^ m ~= 0"


1189 
by (import arithmetic NOT_EXP_0)


1190 


1191 
lemma ZERO_LESS_EXP: "ALL m n. 0 < Suc n ^ m"


1192 
by (import arithmetic ZERO_LESS_EXP)


1193 


1194 
lemma ODD_OR_EVEN: "ALL x. EX xa. x = Suc (Suc 0) * xa  x = Suc (Suc 0) * xa + 1"


1195 
by (import arithmetic ODD_OR_EVEN)


1196 


1197 
lemma LESS_EXP_SUC_MONO: "ALL n m. Suc (Suc m) ^ n < Suc (Suc m) ^ Suc n"


1198 
by (import arithmetic LESS_EXP_SUC_MONO)


1199 


1200 
lemma LESS_LESS_CASES: "ALL (m::nat) n::nat. m = n  m < n  n < m"


1201 
by (import arithmetic LESS_LESS_CASES)


1202 


1203 
lemma LESS_EQUAL_ADD: "ALL (m::nat) n::nat. m <= n > (EX p::nat. n = m + p)"


1204 
by (import arithmetic LESS_EQUAL_ADD)


1205 


1206 
lemma LESS_EQ_EXISTS: "ALL (m::nat) n::nat. (m <= n) = (EX p::nat. n = m + p)"


1207 
by (import arithmetic LESS_EQ_EXISTS)


1208 


1209 
lemma MULT_EQ_1: "ALL (x::nat) y::nat. (x * y = (1::nat)) = (x = (1::nat) & y = (1::nat))"


1210 
by (import arithmetic MULT_EQ_1)


1211 


1212 
consts


1213 
FACT :: "nat => nat"


1214 


1215 
specification (FACT) FACT: "FACT 0 = 1 & (ALL n. FACT (Suc n) = Suc n * FACT n)"


1216 
by (import arithmetic FACT)


1217 


1218 
lemma FACT_LESS: "ALL n. 0 < FACT n"


1219 
by (import arithmetic FACT_LESS)


1220 


1221 
lemma EVEN_ODD: "ALL n. EVEN n = (~ ODD n)"


1222 
by (import arithmetic EVEN_ODD)


1223 


1224 
lemma ODD_EVEN: "ALL x. ODD x = (~ EVEN x)"


1225 
by (import arithmetic ODD_EVEN)


1226 


1227 
lemma EVEN_OR_ODD: "ALL x. EVEN x  ODD x"


1228 
by (import arithmetic EVEN_OR_ODD)


1229 


1230 
lemma EVEN_AND_ODD: "ALL x. ~ (EVEN x & ODD x)"


1231 
by (import arithmetic EVEN_AND_ODD)


1232 


1233 
lemma EVEN_ADD: "ALL m n. EVEN (m + n) = (EVEN m = EVEN n)"


1234 
by (import arithmetic EVEN_ADD)


1235 


1236 
lemma EVEN_MULT: "ALL m n. EVEN (m * n) = (EVEN m  EVEN n)"


1237 
by (import arithmetic EVEN_MULT)


1238 


1239 
lemma ODD_ADD: "ALL m n. ODD (m + n) = (ODD m ~= ODD n)"


1240 
by (import arithmetic ODD_ADD)


1241 


1242 
lemma ODD_MULT: "ALL m n. ODD (m * n) = (ODD m & ODD n)"


1243 
by (import arithmetic ODD_MULT)


1244 


1245 
lemma EVEN_DOUBLE: "ALL n. EVEN (2 * n)"


1246 
by (import arithmetic EVEN_DOUBLE)


1247 


1248 
lemma ODD_DOUBLE: "ALL x. ODD (Suc (2 * x))"


1249 
by (import arithmetic ODD_DOUBLE)


1250 


1251 
lemma EVEN_ODD_EXISTS: "ALL x. (EVEN x > (EX m. x = 2 * m)) & (ODD x > (EX m. x = Suc (2 * m)))"


1252 
by (import arithmetic EVEN_ODD_EXISTS)


1253 


1254 
lemma EVEN_EXISTS: "ALL n. EVEN n = (EX m. n = 2 * m)"


1255 
by (import arithmetic EVEN_EXISTS)


1256 


1257 
lemma ODD_EXISTS: "ALL n. ODD n = (EX m. n = Suc (2 * m))"


1258 
by (import arithmetic ODD_EXISTS)


1259 


1260 
lemma NOT_SUC_LESS_EQ_0: "ALL x. ~ Suc x <= 0"


1261 
by (import arithmetic NOT_SUC_LESS_EQ_0)


1262 


1263 
lemma NOT_LEQ: "ALL x xa. (~ x <= xa) = (Suc xa <= x)"


1264 
by (import arithmetic NOT_LEQ)


1265 


1266 
lemma NOT_NUM_EQ: "ALL x xa. (x ~= xa) = (Suc x <= xa  Suc xa <= x)"


1267 
by (import arithmetic NOT_NUM_EQ)


1268 


1269 
lemma NOT_GREATER_EQ: "ALL x xa. (~ xa <= x) = (Suc x <= xa)"


1270 
by (import arithmetic NOT_GREATER_EQ)


1271 


1272 
lemma SUC_ADD_SYM: "ALL m n. Suc (m + n) = Suc n + m"


1273 
by (import arithmetic SUC_ADD_SYM)


1274 


1275 
lemma NOT_SUC_ADD_LESS_EQ: "ALL m n. ~ Suc (m + n) <= m"


1276 
by (import arithmetic NOT_SUC_ADD_LESS_EQ)


1277 


1278 
lemma SUB_LEFT_ADD: "ALL (m::nat) (n::nat) p::nat.


1279 
m + (n  p) = (if n <= p then m else m + n  p)"


1280 
by (import arithmetic SUB_LEFT_ADD)


1281 


1282 
lemma SUB_RIGHT_ADD: "ALL (m::nat) (n::nat) p::nat. m  n + p = (if m <= n then p else m + p  n)"


1283 
by (import arithmetic SUB_RIGHT_ADD)


1284 


1285 
lemma SUB_LEFT_SUB: "ALL (m::nat) (n::nat) p::nat.


1286 
m  (n  p) = (if n <= p then m else m + p  n)"


1287 
by (import arithmetic SUB_LEFT_SUB)


1288 


1289 
lemma SUB_LEFT_SUC: "ALL m n. Suc (m  n) = (if m <= n then Suc 0 else Suc m  n)"


1290 
by (import arithmetic SUB_LEFT_SUC)


1291 


1292 
lemma SUB_LEFT_LESS_EQ: "ALL (m::nat) (n::nat) p::nat. (m <= n  p) = (m + p <= n  m <= (0::nat))"


1293 
by (import arithmetic SUB_LEFT_LESS_EQ)


1294 


1295 
lemma SUB_RIGHT_LESS_EQ: "ALL (m::nat) (n::nat) p::nat. (m  n <= p) = (m <= n + p)"


1296 
by (import arithmetic SUB_RIGHT_LESS_EQ)


1297 


1298 
lemma SUB_RIGHT_LESS: "ALL (m::nat) (n::nat) p::nat. (m  n < p) = (m < n + p & (0::nat) < p)"


1299 
by (import arithmetic SUB_RIGHT_LESS)


1300 


1301 
lemma SUB_RIGHT_GREATER_EQ: "ALL (m::nat) (n::nat) p::nat. (p <= m  n) = (n + p <= m  p <= (0::nat))"


1302 
by (import arithmetic SUB_RIGHT_GREATER_EQ)


1303 


1304 
lemma SUB_LEFT_GREATER: "ALL (m::nat) (n::nat) p::nat. (n  p < m) = (n < m + p & (0::nat) < m)"


1305 
by (import arithmetic SUB_LEFT_GREATER)


1306 


1307 
lemma SUB_RIGHT_GREATER: "ALL (m::nat) (n::nat) p::nat. (p < m  n) = (n + p < m)"


1308 
by (import arithmetic SUB_RIGHT_GREATER)


1309 


1310 
lemma SUB_LEFT_EQ: "ALL (m::nat) (n::nat) p::nat.


1311 
(m = n  p) = (m + p = n  m <= (0::nat) & n <= p)"


1312 
by (import arithmetic SUB_LEFT_EQ)


1313 


1314 
lemma SUB_RIGHT_EQ: "ALL (m::nat) (n::nat) p::nat.


1315 
(m  n = p) = (m = n + p  m <= n & p <= (0::nat))"


1316 
by (import arithmetic SUB_RIGHT_EQ)


1317 


1318 
lemma LE: "(ALL n::nat. (n <= (0::nat)) = (n = (0::nat))) &


1319 
(ALL (m::nat) n::nat. (m <= Suc n) = (m = Suc n  m <= n))"


1320 
by (import arithmetic LE)


1321 


1322 
lemma DA: "ALL (k::nat) n::nat.


1323 
(0::nat) < n > (EX (x::nat) q::nat. k = q * n + x & x < n)"


1324 
by (import arithmetic DA)


1325 

15647

1326 
lemma DIV_LESS_EQ: "ALL n>0::nat. ALL k::nat. k div n <= k"

14516

1327 
by (import arithmetic DIV_LESS_EQ)


1328 


1329 
lemma DIV_UNIQUE: "ALL (n::nat) (k::nat) q::nat.


1330 
(EX r::nat. k = q * n + r & r < n) > k div n = q"


1331 
by (import arithmetic DIV_UNIQUE)


1332 


1333 
lemma MOD_UNIQUE: "ALL (n::nat) (k::nat) r::nat.


1334 
(EX q::nat. k = q * n + r & r < n) > k mod n = r"


1335 
by (import arithmetic MOD_UNIQUE)


1336 


1337 
lemma DIV_MULT: "ALL (n::nat) r::nat. r < n > (ALL q::nat. (q * n + r) div n = q)"


1338 
by (import arithmetic DIV_MULT)


1339 

15647

1340 
lemma MOD_EQ_0: "ALL n>0::nat. ALL k::nat. k * n mod n = (0::nat)"

14516

1341 
by (import arithmetic MOD_EQ_0)


1342 

15647

1343 
lemma ZERO_MOD: "ALL n>0::nat. (0::nat) mod n = (0::nat)"

14516

1344 
by (import arithmetic ZERO_MOD)


1345 

15647

1346 
lemma ZERO_DIV: "ALL n>0::nat. (0::nat) div n = (0::nat)"

14516

1347 
by (import arithmetic ZERO_DIV)


1348 


1349 
lemma MOD_MULT: "ALL (n::nat) r::nat. r < n > (ALL q::nat. (q * n + r) mod n = r)"


1350 
by (import arithmetic MOD_MULT)


1351 

15647

1352 
lemma MOD_TIMES: "ALL n>0::nat. ALL (q::nat) r::nat. (q * n + r) mod n = r mod n"

14516

1353 
by (import arithmetic MOD_TIMES)


1354 

15647

1355 
lemma MOD_PLUS: "ALL n>0::nat. ALL (j::nat) k::nat. (j mod n + k mod n) mod n = (j + k) mod n"

14516

1356 
by (import arithmetic MOD_PLUS)


1357 

15647

1358 
lemma MOD_MOD: "ALL n>0::nat. ALL k::nat. k mod n mod n = k mod n"

14516

1359 
by (import arithmetic MOD_MOD)


1360 

15647

1361 
lemma ADD_DIV_ADD_DIV: "ALL x>0::nat. ALL (xa::nat) r::nat. (xa * x + r) div x = xa + r div x"

14516

1362 
by (import arithmetic ADD_DIV_ADD_DIV)


1363 


1364 
lemma MOD_MULT_MOD: "ALL (m::nat) n::nat.


1365 
(0::nat) < n & (0::nat) < m >


1366 
(ALL x::nat. x mod (n * m) mod n = x mod n)"


1367 
by (import arithmetic MOD_MULT_MOD)


1368 

15647

1369 
lemma DIVMOD_ID: "ALL n>0::nat. n div n = (1::nat) & n mod n = (0::nat)"

14516

1370 
by (import arithmetic DIVMOD_ID)


1371 


1372 
lemma DIV_DIV_DIV_MULT: "ALL (x::nat) xa::nat.


1373 
(0::nat) < x & (0::nat) < xa >


1374 
(ALL xb::nat. xb div x div xa = xb div (x * xa))"


1375 
by (import arithmetic DIV_DIV_DIV_MULT)


1376 


1377 
lemma DIV_P: "ALL (P::nat => bool) (p::nat) q::nat.


1378 
(0::nat) < q >


1379 
P (p div q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P k)"


1380 
by (import arithmetic DIV_P)


1381 


1382 
lemma MOD_P: "ALL (P::nat => bool) (p::nat) q::nat.


1383 
(0::nat) < q >


1384 
P (p mod q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P r)"


1385 
by (import arithmetic MOD_P)


1386 

15647

1387 
lemma MOD_TIMES2: "ALL n>0::nat. ALL (j::nat) k::nat. j mod n * (k mod n) mod n = j * k mod n"

14516

1388 
by (import arithmetic MOD_TIMES2)


1389 


1390 
lemma MOD_COMMON_FACTOR: "ALL (n::nat) (p::nat) q::nat.


1391 
(0::nat) < n & (0::nat) < q > n * (p mod q) = n * p mod (n * q)"


1392 
by (import arithmetic MOD_COMMON_FACTOR)


1393 


1394 
lemma num_case_cong: "ALL M M' b f.


1395 
M = M' & (M' = 0 > b = b') & (ALL n. M' = Suc n > f n = f' n) >


1396 
nat_case b f M = nat_case b' f' M'"


1397 
by (import arithmetic num_case_cong)


1398 

15647

1399 
lemma SUC_ELIM_THM: "ALL P. (ALL n. P (Suc n) n) = (ALL n>0. P n (n  1))"

14516

1400 
by (import arithmetic SUC_ELIM_THM)


1401 


1402 
lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat)  (b::nat)) =


1403 
(ALL x::nat. (b = a + x > P (0::nat)) & (a = b + x > P x))"


1404 
by (import arithmetic SUB_ELIM_THM)


1405 


1406 
lemma PRE_ELIM_THM: "P (PRE n) = (ALL m. (n = 0 > P 0) & (n = Suc m > P m))"


1407 
by (import arithmetic PRE_ELIM_THM)


1408 


1409 
lemma MULT_INCREASES: "ALL m n. 1 < m & 0 < n > Suc n <= m * n"


1410 
by (import arithmetic MULT_INCREASES)


1411 

15647

1412 
lemma EXP_ALWAYS_BIG_ENOUGH: "ALL b>1::nat. ALL n::nat. EX m::nat. n <= b ^ m"

14516

1413 
by (import arithmetic EXP_ALWAYS_BIG_ENOUGH)


1414 


1415 
lemma EXP_EQ_0: "ALL (n::nat) m::nat. (n ^ m = (0::nat)) = (n = (0::nat) & (0::nat) < m)"


1416 
by (import arithmetic EXP_EQ_0)


1417 


1418 
lemma EXP_1: "ALL x::nat. (1::nat) ^ x = (1::nat) & x ^ (1::nat) = x"


1419 
by (import arithmetic EXP_1)


1420 


1421 
lemma EXP_EQ_1: "ALL (n::nat) m::nat. (n ^ m = (1::nat)) = (n = (1::nat)  m = (0::nat))"


1422 
by (import arithmetic EXP_EQ_1)


1423 


1424 
lemma MIN_MAX_EQ: "ALL (x::nat) xa::nat. (min x xa = max x xa) = (x = xa)"


1425 
by (import arithmetic MIN_MAX_EQ)


1426 


1427 
lemma MIN_MAX_LT: "ALL (x::nat) xa::nat. (min x xa < max x xa) = (x ~= xa)"


1428 
by (import arithmetic MIN_MAX_LT)


1429 


1430 
lemma MIN_MAX_PRED: "ALL (P::nat => bool) (m::nat) n::nat.


1431 
P m & P n > P (min m n) & P (max m n)"


1432 
by (import arithmetic MIN_MAX_PRED)


1433 


1434 
lemma MIN_LT: "ALL (x::nat) xa::nat.


1435 
(min xa x < xa) = (xa ~= x & min xa x = x) &


1436 
(min xa x < x) = (xa ~= x & min xa x = xa) &


1437 
(xa < min xa x) = False & (x < min xa x) = False"


1438 
by (import arithmetic MIN_LT)


1439 


1440 
lemma MAX_LT: "ALL (x::nat) xa::nat.


1441 
(xa < max xa x) = (xa ~= x & max xa x = x) &


1442 
(x < max xa x) = (xa ~= x & max xa x = xa) &


1443 
(max xa x < xa) = False & (max xa x < x) = False"


1444 
by (import arithmetic MAX_LT)


1445 


1446 
lemma MIN_LE: "ALL (x::nat) xa::nat. min xa x <= xa & min xa x <= x"


1447 
by (import arithmetic MIN_LE)


1448 


1449 
lemma MAX_LE: "ALL (x::nat) xa::nat. xa <= max xa x & x <= max xa x"


1450 
by (import arithmetic MAX_LE)


1451 


1452 
lemma MIN_0: "ALL x::nat. min x (0::nat) = (0::nat) & min (0::nat) x = (0::nat)"


1453 
by (import arithmetic MIN_0)


1454 


1455 
lemma MAX_0: "ALL x::nat. max x (0::nat) = x & max (0::nat) x = x"


1456 
by (import arithmetic MAX_0)


1457 


1458 
lemma EXISTS_GREATEST: "ALL P::nat => bool.


1459 
(Ex P & (EX x::nat. ALL y::nat. x < y > ~ P y)) =


1460 
(EX x::nat. P x & (ALL y::nat. x < y > ~ P y))"


1461 
by (import arithmetic EXISTS_GREATEST)


1462 


1463 
;end_setup


1464 


1465 
;setup_theory hrat


1466 


1467 
constdefs


1468 
trat_1 :: "nat * nat"


1469 
"trat_1 == (0, 0)"


1470 


1471 
lemma trat_1: "trat_1 = (0, 0)"


1472 
by (import hrat trat_1)


1473 


1474 
constdefs
