--- a/src/HOL/Import/HOL4/Generated/HOL4Base.thy Sun Apr 01 14:50:47 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4501 +0,0 @@
-(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
-
-theory HOL4Base
-imports "../../Importer" "../Compatibility"
-begin
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" bool
-
-definition
- ARB :: "'a" where
- "ARB == SOME x. True"
-
-lemma ARB_DEF: "ARB = (SOME x. True)"
- sorry
-
-definition
- IN :: "'a => ('a => bool) => bool" where
- "IN == %x f. f x"
-
-lemma IN_DEF: "IN = (%x f. f x)"
- sorry
-
-definition
- RES_FORALL :: "('a => bool) => ('a => bool) => bool" where
- "RES_FORALL == %p m. ALL x. IN x p --> m x"
-
-lemma RES_FORALL_DEF: "RES_FORALL = (%p m. ALL x. IN x p --> m x)"
- sorry
-
-definition
- RES_EXISTS :: "('a => bool) => ('a => bool) => bool" where
- "RES_EXISTS == %p m. EX x. IN x p & m x"
-
-lemma RES_EXISTS_DEF: "RES_EXISTS = (%p m. EX x. IN x p & m x)"
- sorry
-
-definition
- RES_EXISTS_UNIQUE :: "('a => bool) => ('a => bool) => bool" where
- "RES_EXISTS_UNIQUE ==
-%p m. RES_EXISTS p m &
- RES_FORALL p (%x. RES_FORALL p (%y. m x & m y --> x = y))"
-
-lemma RES_EXISTS_UNIQUE_DEF: "RES_EXISTS_UNIQUE =
-(%p m. RES_EXISTS p m &
- RES_FORALL p (%x. RES_FORALL p (%y. m x & m y --> x = y)))"
- sorry
-
-definition
- RES_SELECT :: "('a => bool) => ('a => bool) => 'a" where
- "RES_SELECT == %p m. SOME x. IN x p & m x"
-
-lemma RES_SELECT_DEF: "RES_SELECT = (%p m. SOME x. IN x p & m x)"
- sorry
-
-lemma EXCLUDED_MIDDLE: "t | ~ t"
- sorry
-
-lemma FORALL_THM: "All f = All f"
- sorry
-
-lemma EXISTS_THM: "Ex f = Ex f"
- sorry
-
-lemma F_IMP: "[| ~ t; t |] ==> False"
- sorry
-
-lemma NOT_AND: "~ (t & ~ t)"
- sorry
-
-lemma AND_CLAUSES: "(True & t) = t &
-(t & True) = t & (False & t) = False & (t & False) = False & (t & t) = t"
- sorry
-
-lemma OR_CLAUSES: "(True | t) = True &
-(t | True) = True & (False | t) = t & (t | False) = t & (t | t) = t"
- sorry
-
-lemma IMP_CLAUSES: "(True --> t) = t &
-(t --> True) = True &
-(False --> t) = True & (t --> t) = True & (t --> False) = (~ t)"
- sorry
-
-lemma NOT_CLAUSES: "(ALL t. (~ ~ t) = t) & (~ True) = False & (~ False) = True"
- sorry
-
-lemma BOOL_EQ_DISTINCT: "True ~= False & False ~= True"
- sorry
-
-lemma EQ_CLAUSES: "(True = t) = t & (t = True) = t & (False = t) = (~ t) & (t = False) = (~ t)"
- sorry
-
-lemma COND_CLAUSES: "(if True then t1 else t2) = t1 & (if False then t1 else t2) = t2"
- sorry
-
-lemma SELECT_UNIQUE: "(!!y. P y = (y = x)) ==> Eps P = x"
- sorry
-
-lemma BOTH_EXISTS_AND_THM: "(EX x::'a. (P::bool) & (Q::bool)) = ((EX x::'a. P) & (EX x::'a. Q))"
- sorry
-
-lemma BOTH_FORALL_OR_THM: "(ALL x::'a. (P::bool) | (Q::bool)) = ((ALL x::'a. P) | (ALL x::'a. Q))"
- sorry
-
-lemma BOTH_FORALL_IMP_THM: "(ALL x::'a. (P::bool) --> (Q::bool)) = ((EX x::'a. P) --> (ALL x::'a. Q))"
- sorry
-
-lemma BOTH_EXISTS_IMP_THM: "(EX x::'a. (P::bool) --> (Q::bool)) = ((ALL x::'a. P) --> (EX x::'a. Q))"
- sorry
-
-lemma OR_IMP_THM: "(A = (B | A)) = (B --> A)"
- sorry
-
-lemma DE_MORGAN_THM: "(~ (A & B)) = (~ A | ~ B) & (~ (A | B)) = (~ A & ~ B)"
- sorry
-
-lemma IMP_F_EQ_F: "(t --> False) = (t = False)"
- sorry
-
-lemma COND_RATOR: "(if b::bool then f::'a => 'b else (g::'a => 'b)) (x::'a) =
-(if b then f x else g x)"
- sorry
-
-lemma COND_ABS: "(%x. if b then f x else g x) = (if b then f else g)"
- sorry
-
-lemma COND_EXPAND: "(if b then t1 else t2) = ((~ b | t1) & (b | t2))"
- sorry
-
-lemma ONE_ONE_THM: "inj f = (ALL x1 x2. f x1 = f x2 --> x1 = x2)"
- sorry
-
-lemma ABS_REP_THM: "(op ==>::prop => prop => prop)
- ((Trueprop::bool => prop)
- ((Ex::(('b::type => 'a::type) => bool) => bool)
- ((TYPE_DEFINITION::('a::type => bool)
- => ('b::type => 'a::type) => bool)
- (P::'a::type => bool))))
- ((Trueprop::bool => prop)
- ((Ex::(('b::type => 'a::type) => bool) => bool)
- (%x::'b::type => 'a::type.
- (Ex::(('a::type => 'b::type) => bool) => bool)
- (%abs::'a::type => 'b::type.
- (op &::bool => bool => bool)
- ((All::('b::type => bool) => bool)
- (%a::'b::type.
- (op =::'b::type => 'b::type => bool) (abs (x a)) a))
- ((All::('a::type => bool) => bool)
- (%r::'a::type.
- (op =::bool => bool => bool) (P r)
- ((op =::'a::type => 'a::type => bool) (x (abs r))
- r)))))))"
- sorry
-
-lemma LET_RAND: "(P::'b => bool) (Let (M::'a) (N::'a => 'b)) = (let x::'a = M in P (N x))"
- sorry
-
-lemma LET_RATOR: "Let (M::'a) (N::'a => 'b => 'c) (b::'b) = (let x::'a = M in N x b)"
- sorry
-
-lemma AND_CONG: "(Q --> P = P') & (P' --> Q = Q') ==> (P & Q) = (P' & Q')"
- sorry
-
-lemma OR_CONG: "(~ Q --> P = P') & (~ P' --> Q = Q') ==> (P | Q) = (P' | Q')"
- sorry
-
-lemma COND_CONG: "P = Q & (Q --> x = x') & (~ Q --> y = y')
-==> (if P then x else y) = (if Q then x' else y')"
- sorry
-
-lemma MONO_COND: "[| x ==> y; z ==> w; if b then x else z |] ==> if b then y else w"
- sorry
-
-lemma SKOLEM_THM: "(ALL x. Ex (P x)) = (EX f. ALL x. P x (f x))"
- sorry
-
-lemma bool_case_thm: "(ALL (e0::'a) e1::'a. (case True of True => e0 | False => e1) = e0) &
-(ALL (e0::'a) e1::'a. (case False of True => e0 | False => e1) = e1)"
- sorry
-
-lemma bool_case_ID: "(case b of True => x | _ => x) = x"
- sorry
-
-lemma boolAxiom: "EX x. x True = e0 & x False = e1"
- sorry
-
-lemma UEXISTS_OR_THM: "EX! x. P x | Q x ==> Ex1 P | Ex1 Q"
- sorry
-
-lemma UEXISTS_SIMP: "(EX! x::'a. (t::bool)) = (t & (ALL x::'a. All (op = x)))"
- sorry
-
-consts
- RES_ABSTRACT :: "('a => bool) => ('a => 'b) => 'a => 'b"
-
-specification (RES_ABSTRACT) RES_ABSTRACT_DEF: "(ALL (p::'a => bool) (m::'a => 'b) x::'a.
- IN x p --> RES_ABSTRACT p m x = m x) &
-(ALL (p::'a => bool) (m1::'a => 'b) m2::'a => 'b.
- (ALL x::'a. IN x p --> m1 x = m2 x) -->
- RES_ABSTRACT p m1 = RES_ABSTRACT p m2)"
- sorry
-
-lemma BOOL_FUN_CASES_THM: "f = (%b. True) | f = (%b. False) | f = (%b. b) | f = Not"
- sorry
-
-lemma BOOL_FUN_INDUCT: "P (%b. True) & P (%b. False) & P (%b. b) & P Not ==> P x"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" combin
-
-definition
- K :: "'a => 'b => 'a" where
- "K == %x y. x"
-
-lemma K_DEF: "K = (%x y. x)"
- sorry
-
-definition
- S :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" where
- "S == %f g x. f x (g x)"
-
-lemma S_DEF: "S = (%f g x. f x (g x))"
- sorry
-
-definition
- I :: "'a => 'a" where
- "(op ==::('a::type => 'a::type) => ('a::type => 'a::type) => prop)
- (I::'a::type => 'a::type)
- ((S::('a::type => ('a::type => 'a::type) => 'a::type)
- => ('a::type => 'a::type => 'a::type) => 'a::type => 'a::type)
- (K::'a::type => ('a::type => 'a::type) => 'a::type)
- (K::'a::type => 'a::type => 'a::type))"
-
-lemma I_DEF: "(op =::('a::type => 'a::type) => ('a::type => 'a::type) => bool)
- (I::'a::type => 'a::type)
- ((S::('a::type => ('a::type => 'a::type) => 'a::type)
- => ('a::type => 'a::type => 'a::type) => 'a::type => 'a::type)
- (K::'a::type => ('a::type => 'a::type) => 'a::type)
- (K::'a::type => 'a::type => 'a::type))"
- sorry
-
-definition
- C :: "('a => 'b => 'c) => 'b => 'a => 'c" where
- "C == %f x y. f y x"
-
-lemma C_DEF: "C = (%f x y. f y x)"
- sorry
-
-definition
- W :: "('a => 'a => 'b) => 'a => 'b" where
- "W == %f x. f x x"
-
-lemma W_DEF: "W = (%f x. f x x)"
- sorry
-
-lemma I_THM: "I x = x"
- sorry
-
-lemma I_o_ID: "I o f = f & f o I = f"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" sum
-
-lemma ISL_OR_ISR: "ISL x | ISR x"
- sorry
-
-lemma INL: "ISL x ==> Inl (OUTL x) = x"
- sorry
-
-lemma INR: "ISR x ==> Inr (OUTR x) = x"
- sorry
-
-lemma sum_case_cong: "(M::'b + 'c) = (M'::'b + 'c) &
-(ALL x::'b. M' = Inl x --> (f::'b => 'a) x = (f'::'b => 'a) x) &
-(ALL y::'c. M' = Inr y --> (g::'c => 'a) y = (g'::'c => 'a) y)
-==> sum_case f g M = sum_case f' g' M'"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" one
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" option
-
-lemma option_CLAUSES: "(op &::bool => bool => bool)
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (All::('a::type => bool) => bool)
- (%y::'a::type.
- (op =::bool => bool => bool)
- ((op =::'a::type option => 'a::type option => bool)
- ((Some::'a::type => 'a::type option) x)
- ((Some::'a::type => 'a::type option) y))
- ((op =::'a::type => 'a::type => bool) x y))))
- ((op &::bool => bool => bool)
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (op =::'a::type => 'a::type => bool)
- ((the::'a::type option => 'a::type)
- ((Some::'a::type => 'a::type option) x))
- x))
- ((op &::bool => bool => bool)
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (op ~=::'a::type option => 'a::type option => bool)
- (None::'a::type option)
- ((Some::'a::type => 'a::type option) x)))
- ((op &::bool => bool => bool)
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (op ~=::'a::type option => 'a::type option => bool)
- ((Some::'a::type => 'a::type option) x)
- (None::'a::type option)))
- ((op &::bool => bool => bool)
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (op =::bool => bool => bool)
- ((IS_SOME::'a::type option => bool)
- ((Some::'a::type => 'a::type option) x))
- (True::bool)))
- ((op &::bool => bool => bool)
- ((op =::bool => bool => bool)
- ((IS_SOME::'a::type option => bool) (None::'a::type option))
- (False::bool))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op =::bool => bool => bool)
- ((IS_NONE::'a::type option => bool) x)
- ((op =::'a::type option => 'a::type option => bool) x
- (None::'a::type option))))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op =::bool => bool => bool)
- ((Not::bool => bool)
- ((IS_SOME::'a::type option => bool) x))
- ((op =::'a::type option => 'a::type option => bool) x
- (None::'a::type option))))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op -->::bool => bool => bool)
- ((IS_SOME::'a::type option => bool) x)
- ((op =::'a::type option => 'a::type option => bool)
- ((Some::'a::type => 'a::type option)
- ((the::'a::type option => 'a::type) x))
- x)))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op =::'a::type option => 'a::type option => bool)
- ((option_case::'a::type option
- => ('a::type => 'a::type option) => 'a::type option => 'a::type option)
- (None::'a::type option)
- (Some::'a::type => 'a::type option) x)
- x))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op =::'a::type option
- => 'a::type option => bool)
- ((option_case::'a::type option
- => ('a::type => 'a::type option) => 'a::type option => 'a::type option)
- x (Some::'a::type => 'a::type option) x)
- x))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op -->::bool => bool => bool)
- ((IS_NONE::'a::type option => bool) x)
- ((op =::'b::type => 'b::type => bool)
- ((option_case::'b::type
- => ('a::type => 'b::type) => 'a::type option => 'b::type)
- (e::'b::type) (f::'a::type => 'b::type) x)
- e)))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op -->::bool => bool => bool)
- ((IS_SOME::'a::type option => bool) x)
- ((op =::'b::type => 'b::type => bool)
- ((option_case::'b::type
- => ('a::type => 'b::type) => 'a::type option => 'b::type)
- e f x)
- (f ((the::'a::type option => 'a::type)
- x)))))
- ((op &::bool => bool => bool)
- ((All::('a::type option => bool) => bool)
- (%x::'a::type option.
- (op -->::bool => bool => bool)
- ((IS_SOME::'a::type option => bool) x)
- ((op =::'a::type option
- => 'a::type option => bool)
- ((option_case::'a::type option
- => ('a::type => 'a::type option)
- => 'a::type option => 'a::type option)
-(ea::'a::type option) (Some::'a::type => 'a::type option) x)
- x)))
- ((op &::bool => bool => bool)
- ((All::('b::type => bool) => bool)
- (%u::'b::type.
- (All::(('a::type => 'b::type) => bool)
- => bool)
- (%f::'a::type => 'b::type.
- (op =::'b::type => 'b::type => bool)
- ((option_case::'b::type
- => ('a::type => 'b::type) => 'a::type option => 'b::type)
- u f (None::'a::type option))
- u)))
- ((op &::bool => bool => bool)
- ((All::('b::type => bool) => bool)
- (%u::'b::type.
- (All::(('a::type => 'b::type) => bool)
- => bool)
-(%f::'a::type => 'b::type.
- (All::('a::type => bool) => bool)
- (%x::'a::type.
- (op =::'b::type => 'b::type => bool)
- ((option_case::'b::type
- => ('a::type => 'b::type)
- => 'a::type option => 'b::type)
- u f ((Some::'a::type => 'a::type option) x))
- (f x)))))
- ((op &::bool => bool => bool)
- ((All::(('a::type => 'b::type) => bool)
- => bool)
- (%f::'a::type => 'b::type.
- (All::('a::type => bool) => bool)
- (%x::'a::type.
- (op =::'b::type option => 'b::type option => bool)
- ((Option.map::('a::type => 'b::type)
- => 'a::type option => 'b::type option)
- f ((Some::'a::type => 'a::type option) x))
- ((Some::'b::type => 'b::type option) (f x)))))
- ((op &::bool => bool => bool)
- ((All::(('a::type => 'b::type) => bool)
- => bool)
- (%f::'a::type => 'b::type.
- (op =::'b::type option => 'b::type option => bool)
- ((Option.map::('a::type => 'b::type)
- => 'a::type option => 'b::type option)
- f (None::'a::type option))
- (None::'b::type option)))
- ((op &::bool => bool => bool)
- ((op =::'a::type option
- => 'a::type option => bool)
- ((OPTION_JOIN::'a::type option option => 'a::type option)
- (None::'a::type option option))
- (None::'a::type option))
- ((All::('a::type option => bool)
- => bool)
- (%x::'a::type option.
- (op =::'a::type option => 'a::type option => bool)
- ((OPTION_JOIN::'a::type option option => 'a::type option)
- ((Some::'a::type option => 'a::type option option) x))
- x))))))))))))))))))))"
- sorry
-
-lemma option_case_compute: "option_case (e::'b) (f::'a => 'b) (x::'a option) =
-(if IS_SOME x then f (the x) else e)"
- sorry
-
-lemma OPTION_MAP_EQ_SOME: "(Option.map (f::'a => 'b) (x::'a option) = Some (y::'b)) =
-(EX z::'a. x = Some z & y = f z)"
- sorry
-
-lemma OPTION_JOIN_EQ_SOME: "(OPTION_JOIN x = Some xa) = (x = Some (Some xa))"
- sorry
-
-lemma option_case_cong: "M = M' & (M' = None --> u = u') & (ALL x. M' = Some x --> f x = f' x)
-==> option_case u f M = option_case u' f' M'"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" marker
-
-consts
- stmarker :: "'a => 'a"
-
-defs
- stmarker_primdef: "stmarker == %x. x"
-
-lemma stmarker_def: "stmarker x = x"
- sorry
-
-lemma move_left_conj: "(x & stmarker xb) = (stmarker xb & x) &
-((stmarker xb & x) & xa) = (stmarker xb & x & xa) &
-(x & stmarker xb & xa) = (stmarker xb & x & xa)"
- sorry
-
-lemma move_right_conj: "(stmarker xb & x) = (x & stmarker xb) &
-(x & xa & stmarker xb) = ((x & xa) & stmarker xb) &
-((x & stmarker xb) & xa) = ((x & xa) & stmarker xb)"
- sorry
-
-lemma move_left_disj: "(x | stmarker xb) = (stmarker xb | x) &
-((stmarker xb | x) | xa) = (stmarker xb | x | xa) &
-(x | stmarker xb | xa) = (stmarker xb | x | xa)"
- sorry
-
-lemma move_right_disj: "(stmarker xb | x) = (x | stmarker xb) &
-(x | xa | stmarker xb) = ((x | xa) | stmarker xb) &
-((x | stmarker xb) | xa) = ((x | xa) | stmarker xb)"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" relation
-
-definition
- TC :: "('a => 'a => bool) => 'a => 'a => bool" where
- "TC ==
-%R a b.
- ALL P.
- (ALL x y. R x y --> P x y) & (ALL x y z. P x y & P y z --> P x z) -->
- P a b"
-
-lemma TC_DEF: "TC R a b =
-(ALL P.
- (ALL x y. R x y --> P x y) & (ALL x y z. P x y & P y z --> P x z) -->
- P a b)"
- sorry
-
-definition
- RTC :: "('a => 'a => bool) => 'a => 'a => bool" where
- "RTC ==
-%R a b.
- ALL P. (ALL x. P x x) & (ALL x y z. R x y & P y z --> P x z) --> P a b"
-
-lemma RTC_DEF: "RTC R a b =
-(ALL P. (ALL x. P x x) & (ALL x y z. R x y & P y z --> P x z) --> P a b)"
- sorry
-
-consts
- RC :: "('a => 'a => bool) => 'a => 'a => bool"
-
-defs
- RC_primdef: "RC == %R x y. x = y | R x y"
-
-lemma RC_def: "RC R x y = (x = y | R x y)"
- sorry
-
-consts
- transitive :: "('a => 'a => bool) => bool"
-
-defs
- transitive_primdef: "transitive == %R. ALL x y z. R x y & R y z --> R x z"
-
-lemma transitive_def: "transitive R = (ALL x y z. R x y & R y z --> R x z)"
- sorry
-
-definition
- pred_reflexive :: "('a => 'a => bool) => bool" where
- "pred_reflexive == %R. ALL x. R x x"
-
-lemma reflexive_def: "pred_reflexive R = (ALL x. R x x)"
- sorry
-
-lemma TC_TRANSITIVE: "transitive (TC x)"
- sorry
-
-lemma RTC_INDUCT: "[| (ALL x. xa x x) & (ALL xb y z. x xb y & xa y z --> xa xb z);
- RTC x xb xc |]
-==> xa xb xc"
- sorry
-
-lemma TC_RULES: "(ALL xa xb. x xa xb --> TC x xa xb) &
-(ALL xa xb xc. TC x xa xb & TC x xb xc --> TC x xa xc)"
- sorry
-
-lemma RTC_RULES: "(ALL xa. RTC x xa xa) &
-(ALL xa xb xc. x xa xb & RTC x xb xc --> RTC x xa xc)"
- sorry
-
-lemma RTC_STRONG_INDUCT: "[| (ALL x. P x x) & (ALL x y z. R x y & RTC R y z & P y z --> P x z);
- RTC R x y |]
-==> P x y"
- sorry
-
-lemma RTC_RTC: "[| RTC R x y; RTC R y z |] ==> RTC R x z"
- sorry
-
-lemma RTC_TRANSITIVE: "transitive (RTC x)"
- sorry
-
-lemma RTC_REFLEXIVE: "pred_reflexive (RTC R)"
- sorry
-
-lemma RC_REFLEXIVE: "pred_reflexive (RC R)"
- sorry
-
-lemma TC_SUBSET: "x xa xb ==> TC x xa xb"
- sorry
-
-lemma RTC_SUBSET: "R x y ==> RTC R x y"
- sorry
-
-lemma RC_SUBSET: "R x y ==> RC R x y"
- sorry
-
-lemma RC_RTC: "RC R x y ==> RTC R x y"
- sorry
-
-lemma TC_INDUCT: "[| (ALL xb y. x xb y --> xa xb y) & (ALL x y z. xa x y & xa y z --> xa x z);
- TC x xb xc |]
-==> xa xb xc"
- sorry
-
-lemma TC_INDUCT_LEFT1: "[| (ALL xb y. x xb y --> xa xb y) &
- (ALL xb y z. x xb y & xa y z --> xa xb z);
- TC x xb xc |]
-==> xa xb xc"
- sorry
-
-lemma TC_STRONG_INDUCT: "[| (ALL x y. R x y --> P x y) &
- (ALL x y z. P x y & P y z & TC R x y & TC R y z --> P x z);
- TC R u v |]
-==> P u v"
- sorry
-
-lemma TC_STRONG_INDUCT_LEFT1: "[| (ALL x y. R x y --> P x y) &
- (ALL x y z. R x y & P y z & TC R y z --> P x z);
- TC R u v |]
-==> P u v"
- sorry
-
-lemma TC_RTC: "TC R x y ==> RTC R x y"
- sorry
-
-lemma RTC_TC_RC: "RTC R x y ==> RC R x y | TC R x y"
- sorry
-
-lemma TC_RC_EQNS: "RC (TC R) = RTC R & TC (RC R) = RTC R"
- sorry
-
-lemma RC_IDEM: "RC (RC R) = RC R"
- sorry
-
-lemma TC_IDEM: "TC (TC R) = TC R"
- sorry
-
-lemma RTC_IDEM: "RTC (RTC R) = RTC R"
- sorry
-
-lemma RTC_CASES1: "RTC x xa xb = (xa = xb | (EX u. x xa u & RTC x u xb))"
- sorry
-
-lemma RTC_CASES2: "RTC x xa xb = (xa = xb | (EX u. RTC x xa u & x u xb))"
- sorry
-
-lemma RTC_CASES_RTC_TWICE: "RTC x xa xb = (EX u. RTC x xa u & RTC x u xb)"
- sorry
-
-lemma TC_CASES1: "TC R x z ==> R x z | (EX y. R x y & TC R y z)"
- sorry
-
-lemma TC_CASES2: "TC R x z ==> R x z | (EX y. TC R x y & R y z)"
- sorry
-
-lemma TC_MONOTONE: "[| !!x y. R x y ==> Q x y; TC R x y |] ==> TC Q x y"
- sorry
-
-lemma RTC_MONOTONE: "[| !!x y. R x y ==> Q x y; RTC R x y |] ==> RTC Q x y"
- sorry
-
-definition
- WF :: "('a => 'a => bool) => bool" where
- "WF == %R. ALL B. Ex B --> (EX min. B min & (ALL b. R b min --> ~ B b))"
-
-lemma WF_DEF: "WF R = (ALL B. Ex B --> (EX min. B min & (ALL b. R b min --> ~ B b)))"
- sorry
-
-lemma WF_INDUCTION_THM: "[| WF R; !!x. (!!y. R y x ==> P y) ==> P x |] ==> P x"
- sorry
-
-lemma WF_NOT_REFL: "[| WF x; x xa xb |] ==> xa ~= xb"
- sorry
-
-definition
- EMPTY_REL :: "'a => 'a => bool" where
- "EMPTY_REL == %x y. False"
-
-lemma EMPTY_REL_DEF: "EMPTY_REL x y = False"
- sorry
-
-lemma WF_EMPTY_REL: "WF EMPTY_REL"
- sorry
-
-lemma WF_SUBSET: "WF x & (ALL xb y. xa xb y --> x xb y) ==> WF xa"
- sorry
-
-lemma WF_TC: "WF R ==> WF (TC R)"
- sorry
-
-consts
- inv_image :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool"
-
-defs
- inv_image_primdef: "relation.inv_image ==
-%(R::'b => 'b => bool) (f::'a => 'b) (x::'a) y::'a. R (f x) (f y)"
-
-lemma inv_image_def: "relation.inv_image R f = (%x y. R (f x) (f y))"
- sorry
-
-lemma WF_inv_image: "WF (R::'b => 'b => bool) ==> WF (relation.inv_image R (f::'a => 'b))"
- sorry
-
-definition
- RESTRICT :: "('a => 'b) => ('a => 'a => bool) => 'a => 'a => 'b" where
- "RESTRICT == %f R x y. if R y x then f y else ARB"
-
-lemma RESTRICT_DEF: "RESTRICT f R x = (%y. if R y x then f y else ARB)"
- sorry
-
-lemma RESTRICT_LEMMA: "xa xb xc ==> RESTRICT x xa xc xb = x xb"
- sorry
-
-consts
- approx :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => ('a => 'b) => bool"
-
-defs
- approx_primdef: "approx == %R M x f. f = RESTRICT (%y. M (RESTRICT f R y) y) R x"
-
-lemma approx_def: "approx R M x f = (f = RESTRICT (%y. M (RESTRICT f R y) y) R x)"
- sorry
-
-consts
- the_fun :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'a => 'b"
-
-defs
- the_fun_primdef: "the_fun == %R M x. Eps (approx R M x)"
-
-lemma the_fun_def: "the_fun R M x = Eps (approx R M x)"
- sorry
-
-definition
- WFREC :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'b" where
- "WFREC ==
-%R M x. M (RESTRICT (the_fun (TC R) (%f v. M (RESTRICT f R v) v) x) R x) x"
-
-lemma WFREC_DEF: "WFREC R M =
-(%x. M (RESTRICT (the_fun (TC R) (%f v. M (RESTRICT f R v) v) x) R x) x)"
- sorry
-
-lemma WFREC_THM: "WF R ==> WFREC R M x = M (RESTRICT (WFREC R M) R x) x"
- sorry
-
-lemma WFREC_COROLLARY: "[| f = WFREC R M; WF R |] ==> f x = M (RESTRICT f R x) x"
- sorry
-
-lemma WF_RECURSION_THM: "WF R ==> EX! f. ALL x. f x = M (RESTRICT f R x) x"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" pair
-
-lemma CURRY_ONE_ONE_THM: "(curry f = curry g) = (f = g)"
- sorry
-
-lemma UNCURRY_ONE_ONE_THM: "((%(x, y). f x y) = (%(x, y). g x y)) = (f = g)"
- sorry
-
-lemma pair_Axiom: "EX x. ALL xa y. x (xa, y) = f xa y"
- sorry
-
-lemma UNCURRY_CONG: "M = M' & (ALL x y. M' = (x, y) --> f x y = f' x y)
-==> prod_case f M = prod_case f' M'"
- sorry
-
-lemma ELIM_PEXISTS: "(EX p. P (fst p) (snd p)) = (EX p1. Ex (P p1))"
- sorry
-
-lemma ELIM_PFORALL: "(ALL p. P (fst p) (snd p)) = (ALL p1. All (P p1))"
- sorry
-
-lemma PFORALL_THM: "(ALL xa. All (x xa)) = All (%(xa, y). x xa y)"
- sorry
-
-lemma PEXISTS_THM: "(EX xa. Ex (x xa)) = Ex (%(xa, y). x xa y)"
- sorry
-
-lemma LET2_RAND: "(x::'c => 'd)
- (let (x::'a, y::'b) = xa::'a * 'b in (xb::'a => 'b => 'c) x y) =
-(let (xa::'a, y::'b) = xa in x (xb xa y))"
- sorry
-
-lemma LET2_RATOR: "(let (x::'a1, y::'a2) = x::'a1 * 'a2 in (xa::'a1 => 'a2 => 'b => 'c) x y)
- (xb::'b) =
-(let (x::'a1, y::'a2) = x in xa x y xb)"
- sorry
-
-lemma pair_case_cong: "x = xa & (ALL x y. xa = (x, y) --> xb x y = f' x y)
-==> prod_case xb x = prod_case f' xa"
- sorry
-
-definition
- LEX :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" where
- "LEX == %R1 R2 (s, t) (u, v). R1 s u | s = u & R2 t v"
-
-lemma LEX_DEF: "LEX R1 R2 = (%(s, t) (u, v). R1 s u | s = u & R2 t v)"
- sorry
-
-lemma WF_LEX: "WF x & WF xa ==> WF (LEX x xa)"
- sorry
-
-definition
- RPROD :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" where
- "RPROD == %R1 R2 (s, t) (u, v). R1 s u & R2 t v"
-
-lemma RPROD_DEF: "RPROD R1 R2 = (%(s, t) (u, v). R1 s u & R2 t v)"
- sorry
-
-lemma WF_RPROD: "WF R & WF Q ==> WF (RPROD R Q)"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" num
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" prim_rec
-
-lemma LESS_0_0: "0 < Suc 0"
- sorry
-
-lemma LESS_LEMMA1: "x < Suc xa ==> x = xa | x < xa"
- sorry
-
-lemma LESS_LEMMA2: "m = n | m < n ==> m < Suc n"
- sorry
-
-lemma LESS_THM: "(m < Suc n) = (m = n | m < n)"
- sorry
-
-lemma LESS_SUC_IMP: "[| x < Suc xa; x ~= xa |] ==> x < xa"
- sorry
-
-lemma EQ_LESS: "Suc m = n ==> m < n"
- sorry
-
-lemma NOT_LESS_EQ: "(m::nat) = (n::nat) ==> ~ m < n"
- sorry
-
-definition
- SIMP_REC_REL :: "(nat => 'a) => 'a => ('a => 'a) => nat => bool" where
- "SIMP_REC_REL == %fun x f n. fun 0 = x & (ALL m<n. fun (Suc m) = f (fun m))"
-
-lemma SIMP_REC_REL: "SIMP_REC_REL fun x f n = (fun 0 = x & (ALL m<n. fun (Suc m) = f (fun m)))"
- sorry
-
-lemma SIMP_REC_EXISTS: "EX fun. SIMP_REC_REL fun x f n"
- sorry
-
-lemma SIMP_REC_REL_UNIQUE: "[| SIMP_REC_REL xb x xa xd & SIMP_REC_REL xc x xa xe; n < xd & n < xe |]
-==> xb n = xc n"
- sorry
-
-lemma SIMP_REC_REL_UNIQUE_RESULT: "EX! y. EX g. SIMP_REC_REL g x f (Suc n) & y = g n"
- sorry
-
-consts
- SIMP_REC :: "'a => ('a => 'a) => nat => 'a"
-
-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"
- sorry
-
-lemma LESS_SUC_SUC: "m < Suc m & m < Suc (Suc m)"
- sorry
-
-lemma SIMP_REC_THM: "SIMP_REC x f 0 = x & (ALL m. SIMP_REC x f (Suc m) = f (SIMP_REC x f m))"
- sorry
-
-definition
- PRE :: "nat => nat" where
- "PRE == %m. if m = 0 then 0 else SOME n. m = Suc n"
-
-lemma PRE_DEF: "PRE m = (if m = 0 then 0 else SOME n. m = Suc n)"
- sorry
-
-lemma PRE: "PRE 0 = 0 & (ALL m. PRE (Suc m) = m)"
- sorry
-
-definition
- PRIM_REC_FUN :: "'a => ('a => nat => 'a) => nat => nat => 'a" where
- "PRIM_REC_FUN == %x f. SIMP_REC (%n. x) (%fun n. f (fun (PRE n)) n)"
-
-lemma PRIM_REC_FUN: "PRIM_REC_FUN x f = SIMP_REC (%n. x) (%fun n. f (fun (PRE n)) n)"
- sorry
-
-lemma PRIM_REC_EQN: "(ALL n. PRIM_REC_FUN x f 0 n = x) &
-(ALL m n. PRIM_REC_FUN x f (Suc m) n = f (PRIM_REC_FUN x f m (PRE n)) n)"
- sorry
-
-definition
- PRIM_REC :: "'a => ('a => nat => 'a) => nat => 'a" where
- "PRIM_REC == %x f m. PRIM_REC_FUN x f m (PRE m)"
-
-lemma PRIM_REC: "PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)"
- sorry
-
-lemma PRIM_REC_THM: "PRIM_REC x f 0 = x & (ALL m. PRIM_REC x f (Suc m) = f (PRIM_REC x f m) m)"
- sorry
-
-lemma DC: "P a & (ALL x. P x --> (EX y. P y & R x y))
-==> EX x. x 0 = a & (ALL n. P (x n) & R (x n) (x (Suc n)))"
- sorry
-
-lemma num_Axiom_old: "EX! fn1. fn1 0 = e & (ALL n. fn1 (Suc n) = f (fn1 n) n)"
- sorry
-
-lemma num_Axiom: "EX x. x 0 = e & (ALL n. x (Suc n) = f n (x n))"
- sorry
-
-consts
- wellfounded :: "('a => 'a => bool) => bool"
-
-defs
- wellfounded_primdef: "wellfounded == %R. ~ (EX f. ALL n. R (f (Suc n)) (f n))"
-
-lemma wellfounded_def: "wellfounded R = (~ (EX f. ALL n. R (f (Suc n)) (f n)))"
- sorry
-
-lemma WF_IFF_WELLFOUNDED: "WF R = wellfounded R"
- sorry
-
-lemma WF_PRED: "WF (%x y. y = Suc x)"
- sorry
-
-lemma WF_LESS: "(WF::(nat => nat => bool) => bool) (op <::nat => nat => bool)"
- sorry
-
-consts
- measure :: "('a => nat) => 'a => 'a => bool"
-
-defs
- measure_primdef: "prim_rec.measure == relation.inv_image op <"
-
-lemma measure_def: "prim_rec.measure = relation.inv_image op <"
- sorry
-
-lemma WF_measure: "WF (prim_rec.measure x)"
- sorry
-
-lemma measure_thm: "prim_rec.measure x xa xb = (x xa < x xb)"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" arithmetic
-
-definition
- nat_elim__magic :: "nat => nat" where
- "nat_elim__magic == %n. n"
-
-lemma nat_elim__magic: "nat_elim__magic n = n"
- sorry
-
-consts
- EVEN :: "nat => bool"
-
-specification (EVEN) EVEN: "EVEN 0 = True & (ALL n. EVEN (Suc n) = (~ EVEN n))"
- sorry
-
-consts
- ODD :: "nat => bool"
-
-specification (ODD) ODD: "ODD 0 = False & (ALL n. ODD (Suc n) = (~ ODD n))"
- sorry
-
-lemma TWO: "2 = Suc 1"
- sorry
-
-lemma NORM_0: "(0::nat) = (0::nat)"
- sorry
-
-lemma num_case_compute: "nat_case f g n = (if n = 0 then f else g (PRE n))"
- sorry
-
-lemma ADD_CLAUSES: "0 + m = m & m + 0 = m & Suc m + n = Suc (m + n) & m + Suc n = Suc (m + n)"
- sorry
-
-lemma LESS_ADD: "(n::nat) < (m::nat) ==> EX p::nat. p + n = m"
- sorry
-
-lemma LESS_ANTISYM: "~ ((m::nat) < (n::nat) & n < m)"
- sorry
-
-lemma LESS_LESS_SUC: "~ (x < xa & xa < Suc x)"
- sorry
-
-lemma FUN_EQ_LEMMA: "f x1 & ~ f x2 ==> x1 ~= x2"
- sorry
-
-lemma LESS_NOT_SUC: "m < n & n ~= Suc m ==> Suc m < n"
- sorry
-
-lemma LESS_0_CASES: "(0::nat) = (m::nat) | (0::nat) < m"
- sorry
-
-lemma LESS_CASES_IMP: "~ (m::nat) < (n::nat) & m ~= n ==> n < m"
- sorry
-
-lemma LESS_CASES: "(m::nat) < (n::nat) | n <= m"
- sorry
-
-lemma LESS_EQ_SUC_REFL: "m <= Suc m"
- sorry
-
-lemma LESS_ADD_NONZERO: "(n::nat) ~= (0::nat) ==> (m::nat) < m + n"
- sorry
-
-lemma LESS_EQ_ANTISYM: "~ ((x::nat) < (xa::nat) & xa <= x)"
- sorry
-
-lemma SUB_0: "(0::nat) - (m::nat) = (0::nat) & m - (0::nat) = m"
- sorry
-
-lemma PRE_SUB1: "PRE m = m - 1"
- sorry
-
-lemma MULT_CLAUSES: "0 * x = 0 &
-x * 0 = 0 &
-1 * x = x & x * 1 = x & Suc x * xa = x * xa + xa & x * Suc xa = x + x * xa"
- sorry
-
-lemma PRE_SUB: "PRE (m - n) = PRE m - n"
- sorry
-
-lemma ADD_EQ_1: "((m::nat) + (n::nat) = (1::nat)) =
-(m = (1::nat) & n = (0::nat) | m = (0::nat) & n = (1::nat))"
- sorry
-
-lemma ADD_INV_0_EQ: "((m::nat) + (n::nat) = m) = (n = (0::nat))"
- sorry
-
-lemma PRE_SUC_EQ: "0 < n ==> (m = PRE n) = (Suc m = n)"
- sorry
-
-lemma INV_PRE_EQ: "0 < m & 0 < n ==> (PRE m = PRE n) = (m = n)"
- sorry
-
-lemma LESS_SUC_NOT: "m < n ==> ~ n < Suc m"
- sorry
-
-lemma ADD_EQ_SUB: "(n::nat) <= (p::nat) ==> ((m::nat) + n = p) = (m = p - n)"
- sorry
-
-lemma LESS_ADD_1: "(xa::nat) < (x::nat) ==> EX xb::nat. x = xa + (xb + (1::nat))"
- sorry
-
-lemma NOT_ODD_EQ_EVEN: "Suc (n + n) ~= m + m"
- sorry
-
-lemma MULT_SUC_EQ: "(n * Suc p = m * Suc p) = (n = m)"
- sorry
-
-lemma MULT_EXP_MONO: "(n * Suc q ^ p = m * Suc q ^ p) = (n = m)"
- sorry
-
-lemma LESS_ADD_SUC: "m < m + Suc n"
- sorry
-
-lemma LESS_OR_EQ_ADD: "(n::nat) < (m::nat) | (EX p::nat. n = p + m)"
- sorry
-
-lemma WOP: "Ex (P::nat => bool) ==> EX n::nat. P n & (ALL m<n. ~ P m)"
- sorry
-
-lemma INV_PRE_LESS: "0 < m ==> (PRE m < PRE n) = (m < n)"
- sorry
-
-lemma INV_PRE_LESS_EQ: "0 < n ==> (PRE m <= PRE n) = (m <= n)"
- sorry
-
-lemma SUB_EQ_EQ_0: "((m::nat) - (n::nat) = m) = (m = (0::nat) | n = (0::nat))"
- sorry
-
-lemma SUB_LESS_OR: "(n::nat) < (m::nat) ==> n <= m - (1::nat)"
- sorry
-
-lemma LESS_SUB_ADD_LESS: "(i::nat) < (n::nat) - (m::nat) ==> i + m < n"
- sorry
-
-lemma LESS_EQ_SUB_LESS: "(xa::nat) <= (x::nat) ==> (x - xa < (c::nat)) = (x < xa + c)"
- sorry
-
-lemma NOT_SUC_LESS_EQ: "(~ Suc x <= xa) = (xa <= x)"
- sorry
-
-lemma SUB_LESS_EQ_ADD: "(m::nat) <= (p::nat) ==> (p - m <= (n::nat)) = (p <= m + n)"
- sorry
-
-lemma SUB_CANCEL: "(xa::nat) <= (x::nat) & (xb::nat) <= x ==> (x - xa = x - xb) = (xa = xb)"
- sorry
-
-lemma NOT_EXP_0: "Suc n ^ m ~= 0"
- sorry
-
-lemma ZERO_LESS_EXP: "0 < Suc n ^ m"
- sorry
-
-lemma ODD_OR_EVEN: "EX xa. x = Suc (Suc 0) * xa | x = Suc (Suc 0) * xa + 1"
- sorry
-
-lemma LESS_EXP_SUC_MONO: "Suc (Suc m) ^ n < Suc (Suc m) ^ Suc n"
- sorry
-
-lemma LESS_LESS_CASES: "(m::nat) = (n::nat) | m < n | n < m"
- sorry
-
-consts
- FACT :: "nat => nat"
-
-specification (FACT) FACT: "FACT 0 = 1 & (ALL n. FACT (Suc n) = Suc n * FACT n)"
- sorry
-
-lemma FACT_LESS: "0 < FACT n"
- sorry
-
-lemma EVEN_ODD: "EVEN n = (~ ODD n)"
- sorry
-
-lemma ODD_EVEN: "ODD x = (~ EVEN x)"
- sorry
-
-lemma EVEN_OR_ODD: "EVEN x | ODD x"
- sorry
-
-lemma EVEN_AND_ODD: "~ (EVEN x & ODD x)"
- sorry
-
-lemma EVEN_ADD: "EVEN (m + n) = (EVEN m = EVEN n)"
- sorry
-
-lemma EVEN_MULT: "EVEN (m * n) = (EVEN m | EVEN n)"
- sorry
-
-lemma ODD_ADD: "ODD (m + n) = (ODD m ~= ODD n)"
- sorry
-
-lemma ODD_MULT: "ODD (m * n) = (ODD m & ODD n)"
- sorry
-
-lemma EVEN_DOUBLE: "EVEN (2 * n)"
- sorry
-
-lemma ODD_DOUBLE: "ODD (Suc (2 * x))"
- sorry
-
-lemma EVEN_ODD_EXISTS: "(EVEN x --> (EX m. x = 2 * m)) & (ODD x --> (EX m. x = Suc (2 * m)))"
- sorry
-
-lemma EVEN_EXISTS: "EVEN n = (EX m. n = 2 * m)"
- sorry
-
-lemma ODD_EXISTS: "ODD n = (EX m. n = Suc (2 * m))"
- sorry
-
-lemma NOT_SUC_LESS_EQ_0: "~ Suc x <= 0"
- sorry
-
-lemma NOT_NUM_EQ: "(x ~= xa) = (Suc x <= xa | Suc xa <= x)"
- sorry
-
-lemma SUC_ADD_SYM: "Suc (m + n) = Suc n + m"
- sorry
-
-lemma NOT_SUC_ADD_LESS_EQ: "~ Suc (m + n) <= m"
- sorry
-
-lemma SUB_LEFT_ADD: "(m::nat) + ((n::nat) - (p::nat)) = (if n <= p then m else m + n - p)"
- sorry
-
-lemma SUB_RIGHT_ADD: "(m::nat) - (n::nat) + (p::nat) = (if m <= n then p else m + p - n)"
- sorry
-
-lemma SUB_LEFT_SUB: "(m::nat) - ((n::nat) - (p::nat)) = (if n <= p then m else m + p - n)"
- sorry
-
-lemma SUB_LEFT_SUC: "Suc (m - n) = (if m <= n then Suc 0 else Suc m - n)"
- sorry
-
-lemma SUB_LEFT_LESS_EQ: "((m::nat) <= (n::nat) - (p::nat)) = (m + p <= n | m <= (0::nat))"
- sorry
-
-lemma SUB_RIGHT_LESS_EQ: "((m::nat) - (n::nat) <= (p::nat)) = (m <= n + p)"
- sorry
-
-lemma SUB_RIGHT_LESS: "((m::nat) - (n::nat) < (p::nat)) = (m < n + p & (0::nat) < p)"
- sorry
-
-lemma SUB_RIGHT_GREATER_EQ: "((p::nat) <= (m::nat) - (n::nat)) = (n + p <= m | p <= (0::nat))"
- sorry
-
-lemma SUB_LEFT_GREATER: "((n::nat) - (p::nat) < (m::nat)) = (n < m + p & (0::nat) < m)"
- sorry
-
-lemma SUB_RIGHT_GREATER: "((p::nat) < (m::nat) - (n::nat)) = (n + p < m)"
- sorry
-
-lemma SUB_LEFT_EQ: "((m::nat) = (n::nat) - (p::nat)) = (m + p = n | m <= (0::nat) & n <= p)"
- sorry
-
-lemma SUB_RIGHT_EQ: "((m::nat) - (n::nat) = (p::nat)) = (m = n + p | m <= n & p <= (0::nat))"
- sorry
-
-lemma LE: "(ALL n::nat. (n <= (0::nat)) = (n = (0::nat))) &
-(ALL (m::nat) n::nat. (m <= Suc n) = (m = Suc n | m <= n))"
- sorry
-
-lemma DA: "(0::nat) < (n::nat) ==> EX (x::nat) q::nat. (k::nat) = q * n + x & x < n"
- sorry
-
-lemma DIV_LESS_EQ: "(0::nat) < (n::nat) ==> (k::nat) div n <= k"
- sorry
-
-lemma DIV_UNIQUE: "EX r::nat. (k::nat) = (q::nat) * (n::nat) + r & r < n ==> k div n = q"
- sorry
-
-lemma MOD_UNIQUE: "EX q::nat. (k::nat) = q * (n::nat) + (r::nat) & r < n ==> k mod n = r"
- sorry
-
-lemma DIV_MULT: "(r::nat) < (n::nat) ==> ((q::nat) * n + r) div n = q"
- sorry
-
-lemma MOD_EQ_0: "(0::nat) < (n::nat) ==> (k::nat) * n mod n = (0::nat)"
- sorry
-
-lemma ZERO_MOD: "(0::nat) < (n::nat) ==> (0::nat) mod n = (0::nat)"
- sorry
-
-lemma ZERO_DIV: "(0::nat) < (n::nat) ==> (0::nat) div n = (0::nat)"
- sorry
-
-lemma MOD_MULT: "(r::nat) < (n::nat) ==> ((q::nat) * n + r) mod n = r"
- sorry
-
-lemma MOD_TIMES: "(0::nat) < (n::nat) ==> ((q::nat) * n + (r::nat)) mod n = r mod n"
- sorry
-
-lemma MOD_PLUS: "(0::nat) < (n::nat)
-==> ((j::nat) mod n + (k::nat) mod n) mod n = (j + k) mod n"
- sorry
-
-lemma MOD_MOD: "(0::nat) < (n::nat) ==> (k::nat) mod n mod n = k mod n"
- sorry
-
-lemma ADD_DIV_ADD_DIV: "(0::nat) < (x::nat) ==> ((xa::nat) * x + (r::nat)) div x = xa + r div x"
- sorry
-
-lemma MOD_MULT_MOD: "(0::nat) < (n::nat) & (0::nat) < (m::nat)
-==> (x::nat) mod (n * m) mod n = x mod n"
- sorry
-
-lemma DIVMOD_ID: "(0::nat) < (n::nat) ==> n div n = (1::nat) & n mod n = (0::nat)"
- sorry
-
-lemma DIV_DIV_DIV_MULT: "(0::nat) < (x::nat) & (0::nat) < (xa::nat)
-==> (xb::nat) div x div xa = xb div (x * xa)"
- sorry
-
-lemma DIV_P: "(0::nat) < (q::nat)
-==> (P::nat => bool) ((p::nat) div q) =
- (EX (k::nat) r::nat. p = k * q + r & r < q & P k)"
- sorry
-
-lemma MOD_P: "(0::nat) < (q::nat)
-==> (P::nat => bool) ((p::nat) mod q) =
- (EX (k::nat) r::nat. p = k * q + r & r < q & P r)"
- sorry
-
-lemma MOD_TIMES2: "(0::nat) < (n::nat)
-==> (j::nat) mod n * ((k::nat) mod n) mod n = j * k mod n"
- sorry
-
-lemma MOD_COMMON_FACTOR: "(0::nat) < (n::nat) & (0::nat) < (q::nat)
-==> n * ((p::nat) mod q) = n * p mod (n * q)"
- sorry
-
-lemma num_case_cong: "M = M' & (M' = 0 --> b = b') & (ALL n. M' = Suc n --> f n = f' n)
-==> nat_case b f M = nat_case b' f' M'"
- sorry
-
-lemma SUC_ELIM_THM: "(ALL n. P (Suc n) n) = (ALL n>0. P n (n - 1))"
- sorry
-
-lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat) - (b::nat)) =
-(ALL x::nat. (b = a + x --> P (0::nat)) & (a = b + x --> P x))"
- sorry
-
-lemma PRE_ELIM_THM: "P (PRE n) = (ALL m. (n = 0 --> P 0) & (n = Suc m --> P m))"
- sorry
-
-lemma MULT_INCREASES: "1 < m & 0 < n ==> Suc n <= m * n"
- sorry
-
-lemma EXP_ALWAYS_BIG_ENOUGH: "(1::nat) < (b::nat) ==> EX m::nat. (n::nat) <= b ^ m"
- sorry
-
-lemma EXP_EQ_0: "((n::nat) ^ (m::nat) = (0::nat)) = (n = (0::nat) & (0::nat) < m)"
- sorry
-
-lemma EXP_1: "(1::nat) ^ (x::nat) = (1::nat) & x ^ (1::nat) = x"
- sorry
-
-lemma MIN_MAX_EQ: "(min (x::nat) (xa::nat) = max x xa) = (x = xa)"
- sorry
-
-lemma MIN_MAX_LT: "(min (x::nat) (xa::nat) < max x xa) = (x ~= xa)"
- sorry
-
-lemma MIN_MAX_PRED: "(P::nat => bool) (m::nat) & P (n::nat) ==> P (min m n) & P (max m n)"
- sorry
-
-lemma MIN_LT: "(min (xa::nat) (x::nat) < xa) = (xa ~= x & min xa x = x) &
-(min xa x < x) = (xa ~= x & min xa x = xa) &
-(xa < min xa x) = False & (x < min xa x) = False"
- sorry
-
-lemma MAX_LT: "((xa::nat) < max xa (x::nat)) = (xa ~= x & max xa x = x) &
-(x < max xa x) = (xa ~= x & max xa x = xa) &
-(max xa x < xa) = False & (max xa x < x) = False"
- sorry
-
-lemma MIN_LE: "min (xa::nat) (x::nat) <= xa & min xa x <= x"
- sorry
-
-lemma MAX_LE: "(xa::nat) <= max xa (x::nat) & x <= max xa x"
- sorry
-
-lemma MIN_0: "min (x::nat) (0::nat) = (0::nat) & min (0::nat) x = (0::nat)"
- sorry
-
-lemma MAX_0: "max (x::nat) (0::nat) = x & max (0::nat) x = x"
- sorry
-
-lemma EXISTS_GREATEST: "(Ex (P::nat => bool) & (EX x::nat. ALL y>x. ~ P y)) =
-(EX x::nat. P x & (ALL y>x. ~ P y))"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" hrat
-
-definition
- trat_1 :: "nat * nat" where
- "trat_1 == (0, 0)"
-
-lemma trat_1: "trat_1 = (0, 0)"
- sorry
-
-definition
- trat_inv :: "nat * nat => nat * nat" where
- "trat_inv == %(x, y). (y, x)"
-
-lemma trat_inv: "trat_inv (x, y) = (y, x)"
- sorry
-
-definition
- trat_add :: "nat * nat => nat * nat => nat * nat" where
- "trat_add ==
-%(x, y) (x', y').
- (PRE (Suc x * Suc y' + Suc x' * Suc y), PRE (Suc y * Suc y'))"
-
-lemma trat_add: "trat_add (x, y) (x', y') =
-(PRE (Suc x * Suc y' + Suc x' * Suc y), PRE (Suc y * Suc y'))"
- sorry
-
-definition
- trat_mul :: "nat * nat => nat * nat => nat * nat" where
- "trat_mul == %(x, y) (x', y'). (PRE (Suc x * Suc x'), PRE (Suc y * Suc y'))"
-
-lemma trat_mul: "trat_mul (x, y) (x', y') = (PRE (Suc x * Suc x'), PRE (Suc y * Suc y'))"
- sorry
-
-consts
- trat_sucint :: "nat => nat * nat"
-
-specification (trat_sucint) trat_sucint: "trat_sucint 0 = trat_1 &
-(ALL n. trat_sucint (Suc n) = trat_add (trat_sucint n) trat_1)"
- sorry
-
-definition
- trat_eq :: "nat * nat => nat * nat => bool" where
- "trat_eq == %(x, y) (x', y'). Suc x * Suc y' = Suc x' * Suc y"
-
-lemma trat_eq: "trat_eq (x, y) (x', y') = (Suc x * Suc y' = Suc x' * Suc y)"
- sorry
-
-lemma TRAT_EQ_REFL: "trat_eq p p"
- sorry
-
-lemma TRAT_EQ_SYM: "trat_eq p q = trat_eq q p"
- sorry
-
-lemma TRAT_EQ_TRANS: "trat_eq p q & trat_eq q r ==> trat_eq p r"
- sorry
-
-lemma TRAT_EQ_AP: "p = q ==> trat_eq p q"
- sorry
-
-lemma TRAT_ADD_SYM_EQ: "trat_add h i = trat_add i h"
- sorry
-
-lemma TRAT_MUL_SYM_EQ: "trat_mul h i = trat_mul i h"
- sorry
-
-lemma TRAT_INV_WELLDEFINED: "trat_eq p q ==> trat_eq (trat_inv p) (trat_inv q)"
- sorry
-
-lemma TRAT_ADD_WELLDEFINED: "trat_eq p q ==> trat_eq (trat_add p r) (trat_add q r)"
- sorry
-
-lemma TRAT_ADD_WELLDEFINED2: "trat_eq p1 p2 & trat_eq q1 q2 ==> trat_eq (trat_add p1 q1) (trat_add p2 q2)"
- sorry
-
-lemma TRAT_MUL_WELLDEFINED: "trat_eq p q ==> trat_eq (trat_mul p r) (trat_mul q r)"
- sorry
-
-lemma TRAT_MUL_WELLDEFINED2: "trat_eq p1 p2 & trat_eq q1 q2 ==> trat_eq (trat_mul p1 q1) (trat_mul p2 q2)"
- sorry
-
-lemma TRAT_ADD_SYM: "trat_eq (trat_add h i) (trat_add i h)"
- sorry
-
-lemma TRAT_ADD_ASSOC: "trat_eq (trat_add h (trat_add i j)) (trat_add (trat_add h i) j)"
- sorry
-
-lemma TRAT_MUL_SYM: "trat_eq (trat_mul h i) (trat_mul i h)"
- sorry
-
-lemma TRAT_MUL_ASSOC: "trat_eq (trat_mul h (trat_mul i j)) (trat_mul (trat_mul h i) j)"
- sorry
-
-lemma TRAT_LDISTRIB: "trat_eq (trat_mul h (trat_add i j)) (trat_add (trat_mul h i) (trat_mul h j))"
- sorry
-
-lemma TRAT_MUL_LID: "trat_eq (trat_mul trat_1 h) h"
- sorry
-
-lemma TRAT_MUL_LINV: "trat_eq (trat_mul (trat_inv h) h) trat_1"
- sorry
-
-lemma TRAT_NOZERO: "~ trat_eq (trat_add h i) h"
- sorry
-
-lemma TRAT_ADD_TOTAL: "trat_eq h i |
-(EX d. trat_eq h (trat_add i d)) | (EX d. trat_eq i (trat_add h d))"
- sorry
-
-lemma TRAT_SUCINT_0: "trat_eq (trat_sucint n) (n, 0)"
- sorry
-
-lemma TRAT_ARCH: "EX n d. trat_eq (trat_sucint n) (trat_add h d)"
- sorry
-
-lemma TRAT_SUCINT: "trat_eq (trat_sucint 0) trat_1 &
-(ALL n. trat_eq (trat_sucint (Suc n)) (trat_add (trat_sucint n) trat_1))"
- sorry
-
-lemma TRAT_EQ_EQUIV: "trat_eq p q = (trat_eq p = trat_eq q)"
- sorry
-
-typedef (open) hrat = "{x. EX xa. x = trat_eq xa}"
- sorry
-
-lemmas hrat_TY_DEF = typedef_hol2hol4 [OF type_definition_hrat]
-
-consts
- mk_hrat :: "(nat * nat => bool) => hrat"
- dest_hrat :: "hrat => nat * nat => bool"
-
-specification (dest_hrat mk_hrat) hrat_tybij: "(ALL a. mk_hrat (dest_hrat a) = a) &
-(ALL r. (EX x. r = trat_eq x) = (dest_hrat (mk_hrat r) = r))"
- sorry
-
-definition
- hrat_1 :: "hrat" where
- "hrat_1 == mk_hrat (trat_eq trat_1)"
-
-lemma hrat_1: "hrat_1 = mk_hrat (trat_eq trat_1)"
- sorry
-
-definition
- hrat_inv :: "hrat => hrat" where
- "hrat_inv == %T1. mk_hrat (trat_eq (trat_inv (Eps (dest_hrat T1))))"
-
-lemma hrat_inv: "hrat_inv T1 = mk_hrat (trat_eq (trat_inv (Eps (dest_hrat T1))))"
- sorry
-
-definition
- hrat_add :: "hrat => hrat => hrat" where
- "hrat_add ==
-%T1 T2.
- mk_hrat (trat_eq (trat_add (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
-
-lemma hrat_add: "hrat_add T1 T2 =
-mk_hrat (trat_eq (trat_add (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
- sorry
-
-definition
- hrat_mul :: "hrat => hrat => hrat" where
- "hrat_mul ==
-%T1 T2.
- mk_hrat (trat_eq (trat_mul (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
-
-lemma hrat_mul: "hrat_mul T1 T2 =
-mk_hrat (trat_eq (trat_mul (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
- sorry
-
-definition
- hrat_sucint :: "nat => hrat" where
- "hrat_sucint == %T1. mk_hrat (trat_eq (trat_sucint T1))"
-
-lemma hrat_sucint: "hrat_sucint T1 = mk_hrat (trat_eq (trat_sucint T1))"
- sorry
-
-lemma HRAT_ADD_SYM: "hrat_add h i = hrat_add i h"
- sorry
-
-lemma HRAT_ADD_ASSOC: "hrat_add h (hrat_add i j) = hrat_add (hrat_add h i) j"
- sorry
-
-lemma HRAT_MUL_SYM: "hrat_mul h i = hrat_mul i h"
- sorry
-
-lemma HRAT_MUL_ASSOC: "hrat_mul h (hrat_mul i j) = hrat_mul (hrat_mul h i) j"
- sorry
-
-lemma HRAT_LDISTRIB: "hrat_mul h (hrat_add i j) = hrat_add (hrat_mul h i) (hrat_mul h j)"
- sorry
-
-lemma HRAT_MUL_LID: "hrat_mul hrat_1 h = h"
- sorry
-
-lemma HRAT_MUL_LINV: "hrat_mul (hrat_inv h) h = hrat_1"
- sorry
-
-lemma HRAT_NOZERO: "hrat_add h i ~= h"
- sorry
-
-lemma HRAT_ADD_TOTAL: "h = i | (EX x. h = hrat_add i x) | (EX x. i = hrat_add h x)"
- sorry
-
-lemma HRAT_ARCH: "EX x xa. hrat_sucint x = hrat_add h xa"
- sorry
-
-lemma HRAT_SUCINT: "hrat_sucint 0 = hrat_1 &
-(ALL x. hrat_sucint (Suc x) = hrat_add (hrat_sucint x) hrat_1)"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" hreal
-
-definition
- hrat_lt :: "hrat => hrat => bool" where
- "hrat_lt == %x y. EX d. y = hrat_add x d"
-
-lemma hrat_lt: "hrat_lt x y = (EX d. y = hrat_add x d)"
- sorry
-
-lemma HRAT_LT_REFL: "~ hrat_lt x x"
- sorry
-
-lemma HRAT_LT_TRANS: "hrat_lt x y & hrat_lt y z ==> hrat_lt x z"
- sorry
-
-lemma HRAT_LT_ANTISYM: "~ (hrat_lt x y & hrat_lt y x)"
- sorry
-
-lemma HRAT_LT_TOTAL: "x = y | hrat_lt x y | hrat_lt y x"
- sorry
-
-lemma HRAT_MUL_RID: "hrat_mul x hrat_1 = x"
- sorry
-
-lemma HRAT_MUL_RINV: "hrat_mul x (hrat_inv x) = hrat_1"
- sorry
-
-lemma HRAT_RDISTRIB: "hrat_mul (hrat_add x y) z = hrat_add (hrat_mul x z) (hrat_mul y z)"
- sorry
-
-lemma HRAT_LT_ADDL: "hrat_lt x (hrat_add x y)"
- sorry
-
-lemma HRAT_LT_ADDR: "hrat_lt xa (hrat_add x xa)"
- sorry
-
-lemma HRAT_LT_GT: "hrat_lt x y ==> ~ hrat_lt y x"
- sorry
-
-lemma HRAT_LT_NE: "hrat_lt x y ==> x ~= y"
- sorry
-
-lemma HRAT_EQ_LADD: "(hrat_add x y = hrat_add x z) = (y = z)"
- sorry
-
-lemma HRAT_EQ_LMUL: "(hrat_mul x y = hrat_mul x z) = (y = z)"
- sorry
-
-lemma HRAT_LT_ADD2: "hrat_lt u x & hrat_lt v y ==> hrat_lt (hrat_add u v) (hrat_add x y)"
- sorry
-
-lemma HRAT_LT_LADD: "hrat_lt (hrat_add z x) (hrat_add z y) = hrat_lt x y"
- sorry
-
-lemma HRAT_LT_RADD: "hrat_lt (hrat_add x z) (hrat_add y z) = hrat_lt x y"
- sorry
-
-lemma HRAT_LT_MUL2: "hrat_lt u x & hrat_lt v y ==> hrat_lt (hrat_mul u v) (hrat_mul x y)"
- sorry
-
-lemma HRAT_LT_LMUL: "hrat_lt (hrat_mul z x) (hrat_mul z y) = hrat_lt x y"
- sorry
-
-lemma HRAT_LT_RMUL: "hrat_lt (hrat_mul x z) (hrat_mul y z) = hrat_lt x y"
- sorry
-
-lemma HRAT_LT_LMUL1: "hrat_lt (hrat_mul x y) y = hrat_lt x hrat_1"
- sorry
-
-lemma HRAT_LT_RMUL1: "hrat_lt (hrat_mul x y) x = hrat_lt y hrat_1"
- sorry
-
-lemma HRAT_GT_LMUL1: "hrat_lt y (hrat_mul x y) = hrat_lt hrat_1 x"
- sorry
-
-lemma HRAT_LT_L1: "hrat_lt (hrat_mul (hrat_inv x) y) hrat_1 = hrat_lt y x"
- sorry
-
-lemma HRAT_LT_R1: "hrat_lt (hrat_mul x (hrat_inv y)) hrat_1 = hrat_lt x y"
- sorry
-
-lemma HRAT_GT_L1: "hrat_lt hrat_1 (hrat_mul (hrat_inv x) y) = hrat_lt x y"
- sorry
-
-lemma HRAT_INV_MUL: "hrat_inv (hrat_mul x y) = hrat_mul (hrat_inv x) (hrat_inv y)"
- sorry
-
-lemma HRAT_UP: "Ex (hrat_lt x)"
- sorry
-
-lemma HRAT_DOWN: "EX xa. hrat_lt xa x"
- sorry
-
-lemma HRAT_DOWN2: "EX xa. hrat_lt xa x & hrat_lt xa y"
- sorry
-
-lemma HRAT_MEAN: "hrat_lt x y ==> EX xa. hrat_lt x xa & hrat_lt xa y"
- sorry
-
-definition
- isacut :: "(hrat => bool) => bool" where
- "isacut ==
-%C. Ex C &
- (EX x. ~ C x) &
- (ALL x y. C x & hrat_lt y x --> C y) &
- (ALL x. C x --> (EX y. C y & hrat_lt x y))"
-
-lemma isacut: "isacut (CC::hrat => bool) =
-(Ex CC &
- (EX x::hrat. ~ CC x) &
- (ALL (x::hrat) y::hrat. CC x & hrat_lt y x --> CC y) &
- (ALL x::hrat. CC x --> (EX y::hrat. CC y & hrat_lt x y)))"
- sorry
-
-definition
- cut_of_hrat :: "hrat => hrat => bool" where
- "cut_of_hrat == %x y. hrat_lt y x"
-
-lemma cut_of_hrat: "cut_of_hrat x = (%y. hrat_lt y x)"
- sorry
-
-lemma ISACUT_HRAT: "isacut (cut_of_hrat h)"
- sorry
-
-typedef (open) hreal = "Collect isacut"
- sorry
-
-lemmas hreal_TY_DEF = typedef_hol2hol4 [OF type_definition_hreal]
-
-consts
- hreal :: "(hrat => bool) => hreal"
- cut :: "hreal => hrat => bool"
-
-specification (cut hreal) hreal_tybij: "(ALL a. hreal (cut a) = a) & (ALL r. isacut r = (cut (hreal r) = r))"
- sorry
-
-lemma EQUAL_CUTS: "cut X = cut Y ==> X = Y"
- sorry
-
-lemma CUT_ISACUT: "isacut (cut x)"
- sorry
-
-lemma CUT_NONEMPTY: "Ex (cut x)"
- sorry
-
-lemma CUT_BOUNDED: "EX xa. ~ cut x xa"
- sorry
-
-lemma CUT_DOWN: "cut x xa & hrat_lt xb xa ==> cut x xb"
- sorry
-
-lemma CUT_UP: "cut x xa ==> EX y. cut x y & hrat_lt xa y"
- sorry
-
-lemma CUT_UBOUND: "~ cut x xa & hrat_lt xa xb ==> ~ cut x xb"
- sorry
-
-lemma CUT_STRADDLE: "cut X x & ~ cut X y ==> hrat_lt x y"
- sorry
-
-lemma CUT_NEARTOP_ADD: "EX x. cut X x & ~ cut X (hrat_add x e)"
- sorry
-
-lemma CUT_NEARTOP_MUL: "hrat_lt hrat_1 u ==> EX x. cut X x & ~ cut X (hrat_mul u x)"
- sorry
-
-definition
- hreal_1 :: "hreal" where
- "hreal_1 == hreal (cut_of_hrat hrat_1)"
-
-lemma hreal_1: "hreal_1 = hreal (cut_of_hrat hrat_1)"
- sorry
-
-definition
- hreal_add :: "hreal => hreal => hreal" where
- "hreal_add == %X Y. hreal (%w. EX x y. w = hrat_add x y & cut X x & cut Y y)"
-
-lemma hreal_add: "hreal_add X Y = hreal (%w. EX x y. w = hrat_add x y & cut X x & cut Y y)"
- sorry
-
-definition
- hreal_mul :: "hreal => hreal => hreal" where
- "hreal_mul == %X Y. hreal (%w. EX x y. w = hrat_mul x y & cut X x & cut Y y)"
-
-lemma hreal_mul: "hreal_mul X Y = hreal (%w. EX x y. w = hrat_mul x y & cut X x & cut Y y)"
- sorry
-
-definition
- hreal_inv :: "hreal => hreal" where
- "hreal_inv ==
-%X. hreal
- (%w. EX d. hrat_lt d hrat_1 &
- (ALL x. cut X x --> hrat_lt (hrat_mul w x) d))"
-
-lemma hreal_inv: "hreal_inv X =
-hreal
- (%w. EX d. hrat_lt d hrat_1 &
- (ALL x. cut X x --> hrat_lt (hrat_mul w x) d))"
- sorry
-
-definition
- hreal_sup :: "(hreal => bool) => hreal" where
- "hreal_sup == %P. hreal (%w. EX X. P X & cut X w)"
-
-lemma hreal_sup: "hreal_sup P = hreal (%w. EX X. P X & cut X w)"
- sorry
-
-definition
- hreal_lt :: "hreal => hreal => bool" where
- "hreal_lt == %X Y. X ~= Y & (ALL x. cut X x --> cut Y x)"
-
-lemma hreal_lt: "hreal_lt X Y = (X ~= Y & (ALL x. cut X x --> cut Y x))"
- sorry
-
-lemma HREAL_INV_ISACUT: "isacut
- (%w. EX d. hrat_lt d hrat_1 &
- (ALL x. cut X x --> hrat_lt (hrat_mul w x) d))"
- sorry
-
-lemma HREAL_ADD_ISACUT: "isacut (%w. EX x y. w = hrat_add x y & cut X x & cut Y y)"
- sorry
-
-lemma HREAL_MUL_ISACUT: "isacut (%w. EX x y. w = hrat_mul x y & cut X x & cut Y y)"
- sorry
-
-lemma HREAL_ADD_SYM: "hreal_add X Y = hreal_add Y X"
- sorry
-
-lemma HREAL_MUL_SYM: "hreal_mul X Y = hreal_mul Y X"
- sorry
-
-lemma HREAL_ADD_ASSOC: "hreal_add X (hreal_add Y Z) = hreal_add (hreal_add X Y) Z"
- sorry
-
-lemma HREAL_MUL_ASSOC: "hreal_mul X (hreal_mul Y Z) = hreal_mul (hreal_mul X Y) Z"
- sorry
-
-lemma HREAL_LDISTRIB: "hreal_mul X (hreal_add Y Z) = hreal_add (hreal_mul X Y) (hreal_mul X Z)"
- sorry
-
-lemma HREAL_MUL_LID: "hreal_mul hreal_1 X = X"
- sorry
-
-lemma HREAL_MUL_LINV: "hreal_mul (hreal_inv X) X = hreal_1"
- sorry
-
-lemma HREAL_NOZERO: "hreal_add X Y ~= X"
- sorry
-
-definition
- hreal_sub :: "hreal => hreal => hreal" where
- "hreal_sub == %Y X. hreal (%w. EX x. ~ cut X x & cut Y (hrat_add x w))"
-
-lemma hreal_sub: "hreal_sub Y X = hreal (%w. EX x. ~ cut X x & cut Y (hrat_add x w))"
- sorry
-
-lemma HREAL_LT_LEMMA: "hreal_lt X Y ==> EX x. ~ cut X x & cut Y x"
- sorry
-
-lemma HREAL_SUB_ISACUT: "hreal_lt X Y ==> isacut (%w. EX x. ~ cut X x & cut Y (hrat_add x w))"
- sorry
-
-lemma HREAL_SUB_ADD: "hreal_lt X Y ==> hreal_add (hreal_sub Y X) X = Y"
- sorry
-
-lemma HREAL_LT_TOTAL: "X = Y | hreal_lt X Y | hreal_lt Y X"
- sorry
-
-lemma HREAL_LT: "hreal_lt X Y = (EX D. Y = hreal_add X D)"
- sorry
-
-lemma HREAL_ADD_TOTAL: "X = Y | (EX D. Y = hreal_add X D) | (EX D. X = hreal_add Y D)"
- sorry
-
-lemma HREAL_SUP_ISACUT: "Ex P & (EX Y. ALL X. P X --> hreal_lt X Y)
-==> isacut (%w. EX X. P X & cut X w)"
- sorry
-
-lemma HREAL_SUP: "Ex P & (EX Y. ALL X. P X --> hreal_lt X Y)
-==> (EX X. P X & hreal_lt Y X) = hreal_lt Y (hreal_sup P)"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" numeral
-
-lemma numeral_suc: "Suc ALT_ZERO = NUMERAL_BIT1 ALT_ZERO &
-(ALL x. Suc (NUMERAL_BIT1 x) = NUMERAL_BIT2 x) &
-(ALL x. Suc (NUMERAL_BIT2 x) = NUMERAL_BIT1 (Suc x))"
- sorry
-
-definition
- iZ :: "nat => nat" where
- "iZ == %x. x"
-
-lemma iZ: "iZ x = x"
- sorry
-
-definition
- iiSUC :: "nat => nat" where
- "iiSUC == %n. Suc (Suc n)"
-
-lemma iiSUC: "iiSUC n = Suc (Suc n)"
- sorry
-
-lemma numeral_distrib: "(ALL x::nat. (0::nat) + x = x) &
-(ALL x::nat. x + (0::nat) = x) &
-(ALL (x::nat) xa::nat. NUMERAL x + NUMERAL xa = NUMERAL (iZ (x + xa))) &
-(ALL x::nat. (0::nat) * x = (0::nat)) &
-(ALL x::nat. x * (0::nat) = (0::nat)) &
-(ALL (x::nat) xa::nat. NUMERAL x * NUMERAL xa = NUMERAL (x * xa)) &
-(ALL x::nat. (0::nat) - x = (0::nat)) &
-(ALL x::nat. x - (0::nat) = x) &
-(ALL (x::nat) xa::nat. NUMERAL x - NUMERAL xa = NUMERAL (x - xa)) &
-(ALL x::nat. (0::nat) ^ NUMERAL (NUMERAL_BIT1 x) = (0::nat)) &
-(ALL x::nat. (0::nat) ^ NUMERAL (NUMERAL_BIT2 x) = (0::nat)) &
-(ALL x::nat. x ^ (0::nat) = (1::nat)) &
-(ALL (x::nat) xa::nat. NUMERAL x ^ NUMERAL xa = NUMERAL (x ^ xa)) &
-Suc (0::nat) = (1::nat) &
-(ALL x::nat. Suc (NUMERAL x) = NUMERAL (Suc x)) &
-PRE (0::nat) = (0::nat) &
-(ALL x::nat. PRE (NUMERAL x) = NUMERAL (PRE x)) &
-(ALL x::nat. (NUMERAL x = (0::nat)) = (x = ALT_ZERO)) &
-(ALL x::nat. ((0::nat) = NUMERAL x) = (x = ALT_ZERO)) &
-(ALL (x::nat) xa::nat. (NUMERAL x = NUMERAL xa) = (x = xa)) &
-(ALL x::nat. (x < (0::nat)) = False) &
-(ALL x::nat. ((0::nat) < NUMERAL x) = (ALT_ZERO < x)) &
-(ALL (x::nat) xa::nat. (NUMERAL x < NUMERAL xa) = (x < xa)) &
-(ALL x::nat. (x < (0::nat)) = False) &
-(ALL x::nat. ((0::nat) < NUMERAL x) = (ALT_ZERO < x)) &
-(ALL (x::nat) xa::nat. (NUMERAL xa < NUMERAL x) = (xa < x)) &
-(ALL x::nat. ((0::nat) <= x) = True) &
-(ALL x::nat. (NUMERAL x <= (0::nat)) = (x <= ALT_ZERO)) &
-(ALL (x::nat) xa::nat. (NUMERAL x <= NUMERAL xa) = (x <= xa)) &
-(ALL x::nat. ((0::nat) <= x) = True) &
-(ALL x::nat. (x <= (0::nat)) = (x = (0::nat))) &
-(ALL (x::nat) xa::nat. (NUMERAL xa <= NUMERAL x) = (xa <= x)) &
-(ALL x::nat. ODD (NUMERAL x) = ODD x) &
-(ALL x::nat. EVEN (NUMERAL x) = EVEN x) & ~ ODD (0::nat) & EVEN (0::nat)"
- sorry
-
-lemma numeral_iisuc: "iiSUC ALT_ZERO = NUMERAL_BIT2 ALT_ZERO &
-iiSUC (NUMERAL_BIT1 n) = NUMERAL_BIT1 (Suc n) &
-iiSUC (NUMERAL_BIT2 n) = NUMERAL_BIT2 (Suc n)"
- sorry
-
-lemma numeral_add: "iZ (ALT_ZERO + x) = x &
-iZ (x + ALT_ZERO) = x &
-iZ (NUMERAL_BIT1 x + NUMERAL_BIT1 xa) = NUMERAL_BIT2 (iZ (x + xa)) &
-iZ (NUMERAL_BIT1 x + NUMERAL_BIT2 xa) = NUMERAL_BIT1 (Suc (x + xa)) &
-iZ (NUMERAL_BIT2 x + NUMERAL_BIT1 xa) = NUMERAL_BIT1 (Suc (x + xa)) &
-iZ (NUMERAL_BIT2 x + NUMERAL_BIT2 xa) = NUMERAL_BIT2 (Suc (x + xa)) &
-Suc (ALT_ZERO + x) = Suc x &
-Suc (x + ALT_ZERO) = Suc x &
-Suc (NUMERAL_BIT1 x + NUMERAL_BIT1 xa) = NUMERAL_BIT1 (Suc (x + xa)) &
-Suc (NUMERAL_BIT1 x + NUMERAL_BIT2 xa) = NUMERAL_BIT2 (Suc (x + xa)) &
-Suc (NUMERAL_BIT2 x + NUMERAL_BIT1 xa) = NUMERAL_BIT2 (Suc (x + xa)) &
-Suc (NUMERAL_BIT2 x + NUMERAL_BIT2 xa) = NUMERAL_BIT1 (iiSUC (x + xa)) &
-iiSUC (ALT_ZERO + x) = iiSUC x &
-iiSUC (x + ALT_ZERO) = iiSUC x &
-iiSUC (NUMERAL_BIT1 x + NUMERAL_BIT1 xa) = NUMERAL_BIT2 (Suc (x + xa)) &
-iiSUC (NUMERAL_BIT1 x + NUMERAL_BIT2 xa) = NUMERAL_BIT1 (iiSUC (x + xa)) &
-iiSUC (NUMERAL_BIT2 x + NUMERAL_BIT1 xa) = NUMERAL_BIT1 (iiSUC (x + xa)) &
-iiSUC (NUMERAL_BIT2 x + NUMERAL_BIT2 xa) = NUMERAL_BIT2 (iiSUC (x + xa))"
- sorry
-
-lemma numeral_eq: "(ALT_ZERO = NUMERAL_BIT1 x) = False &
-(NUMERAL_BIT1 x = ALT_ZERO) = False &
-(ALT_ZERO = NUMERAL_BIT2 x) = False &
-(NUMERAL_BIT2 x = ALT_ZERO) = False &
-(NUMERAL_BIT1 x = NUMERAL_BIT2 xa) = False &
-(NUMERAL_BIT2 x = NUMERAL_BIT1 xa) = False &
-(NUMERAL_BIT1 x = NUMERAL_BIT1 xa) = (x = xa) &
-(NUMERAL_BIT2 x = NUMERAL_BIT2 xa) = (x = xa)"
- sorry
-
-lemma numeral_lt: "(ALT_ZERO < NUMERAL_BIT1 x) = True &
-(ALT_ZERO < NUMERAL_BIT2 x) = True &
-(x < ALT_ZERO) = False &
-(NUMERAL_BIT1 x < NUMERAL_BIT1 xa) = (x < xa) &
-(NUMERAL_BIT2 x < NUMERAL_BIT2 xa) = (x < xa) &
-(NUMERAL_BIT1 x < NUMERAL_BIT2 xa) = (~ xa < x) &
-(NUMERAL_BIT2 x < NUMERAL_BIT1 xa) = (x < xa)"
- sorry
-
-lemma numeral_lte: "(ALT_ZERO <= x) = True &
-(NUMERAL_BIT1 x <= ALT_ZERO) = False &
-(NUMERAL_BIT2 x <= ALT_ZERO) = False &
-(NUMERAL_BIT1 x <= NUMERAL_BIT1 xa) = (x <= xa) &
-(NUMERAL_BIT1 x <= NUMERAL_BIT2 xa) = (x <= xa) &
-(NUMERAL_BIT2 x <= NUMERAL_BIT1 xa) = (~ xa <= x) &
-(NUMERAL_BIT2 x <= NUMERAL_BIT2 xa) = (x <= xa)"
- sorry
-
-lemma numeral_pre: "PRE ALT_ZERO = ALT_ZERO &
-PRE (NUMERAL_BIT1 ALT_ZERO) = ALT_ZERO &
-(ALL x.
- PRE (NUMERAL_BIT1 (NUMERAL_BIT1 x)) =
- NUMERAL_BIT2 (PRE (NUMERAL_BIT1 x))) &
-(ALL x.
- PRE (NUMERAL_BIT1 (NUMERAL_BIT2 x)) = NUMERAL_BIT2 (NUMERAL_BIT1 x)) &
-(ALL x. PRE (NUMERAL_BIT2 x) = NUMERAL_BIT1 x)"
- sorry
-
-lemma bit_initiality: "EX x. x ALT_ZERO = zf &
- (ALL n. x (NUMERAL_BIT1 n) = b1f n (x n)) &
- (ALL n. x (NUMERAL_BIT2 n) = b2f n (x n))"
- sorry
-
-consts
- iBIT_cases :: "nat => 'a => (nat => 'a) => (nat => 'a) => 'a"
-
-specification (iBIT_cases) iBIT_cases: "(ALL (zf::'a) (bf1::nat => 'a) bf2::nat => 'a.
- iBIT_cases ALT_ZERO zf bf1 bf2 = zf) &
-(ALL (n::nat) (zf::'a) (bf1::nat => 'a) bf2::nat => 'a.
- iBIT_cases (NUMERAL_BIT1 n) zf bf1 bf2 = bf1 n) &
-(ALL (n::nat) (zf::'a) (bf1::nat => 'a) bf2::nat => 'a.
- iBIT_cases (NUMERAL_BIT2 n) zf bf1 bf2 = bf2 n)"
- sorry
-
-definition
- iDUB :: "nat => nat" where
- "iDUB == %x. x + x"
-
-lemma iDUB: "iDUB x = x + x"
- sorry
-
-consts
- iSUB :: "bool => nat => nat => nat"
-
-specification (iSUB) iSUB_DEF: "(ALL b x. iSUB b ALT_ZERO x = ALT_ZERO) &
-(ALL b n x.
- iSUB b (NUMERAL_BIT1 n) x =
- (if b
- then iBIT_cases x (NUMERAL_BIT1 n) (%m. iDUB (iSUB True n m))
- (%m. NUMERAL_BIT1 (iSUB False n m))
- else iBIT_cases x (iDUB n) (%m. NUMERAL_BIT1 (iSUB False n m))
- (%m. iDUB (iSUB False n m)))) &
-(ALL b n x.
- iSUB b (NUMERAL_BIT2 n) x =
- (if b
- then iBIT_cases x (NUMERAL_BIT2 n) (%m. NUMERAL_BIT1 (iSUB True n m))
- (%m. iDUB (iSUB True n m))
- else iBIT_cases x (NUMERAL_BIT1 n) (%m. iDUB (iSUB True n m))
- (%m. NUMERAL_BIT1 (iSUB False n m))))"
- sorry
-
-lemma bit_induction: "P ALT_ZERO &
-(ALL n. P n --> P (NUMERAL_BIT1 n)) & (ALL n. P n --> P (NUMERAL_BIT2 n))
-==> P x"
- sorry
-
-lemma iSUB_THM: "iSUB (x::bool) ALT_ZERO (xn::nat) = ALT_ZERO &
-iSUB True (xa::nat) ALT_ZERO = xa &
-iSUB False (NUMERAL_BIT1 xa) ALT_ZERO = iDUB xa &
-iSUB True (NUMERAL_BIT1 xa) (NUMERAL_BIT1 (xb::nat)) =
-iDUB (iSUB True xa xb) &
-iSUB False (NUMERAL_BIT1 xa) (NUMERAL_BIT1 xb) =
-NUMERAL_BIT1 (iSUB False xa xb) &
-iSUB True (NUMERAL_BIT1 xa) (NUMERAL_BIT2 xb) =
-NUMERAL_BIT1 (iSUB False xa xb) &
-iSUB False (NUMERAL_BIT1 xa) (NUMERAL_BIT2 xb) = iDUB (iSUB False xa xb) &
-iSUB False (NUMERAL_BIT2 xa) ALT_ZERO = NUMERAL_BIT1 xa &
-iSUB True (NUMERAL_BIT2 xa) (NUMERAL_BIT1 xb) =
-NUMERAL_BIT1 (iSUB True xa xb) &
-iSUB False (NUMERAL_BIT2 xa) (NUMERAL_BIT1 xb) = iDUB (iSUB True xa xb) &
-iSUB True (NUMERAL_BIT2 xa) (NUMERAL_BIT2 xb) = iDUB (iSUB True xa xb) &
-iSUB False (NUMERAL_BIT2 xa) (NUMERAL_BIT2 xb) =
-NUMERAL_BIT1 (iSUB False xa xb)"
- sorry
-
-lemma numeral_sub: "NUMERAL (x - xa) = (if xa < x then NUMERAL (iSUB True x xa) else 0)"
- sorry
-
-lemma iDUB_removal: "iDUB (NUMERAL_BIT1 x) = NUMERAL_BIT2 (iDUB x) &
-iDUB (NUMERAL_BIT2 x) = NUMERAL_BIT2 (NUMERAL_BIT1 x) &
-iDUB ALT_ZERO = ALT_ZERO"
- sorry
-
-lemma numeral_mult: "ALT_ZERO * x = ALT_ZERO &
-x * ALT_ZERO = ALT_ZERO &
-NUMERAL_BIT1 x * xa = iZ (iDUB (x * xa) + xa) &
-NUMERAL_BIT2 x * xa = iDUB (iZ (x * xa + xa))"
- sorry
-
-definition
- iSQR :: "nat => nat" where
- "iSQR == %x. x * x"
-
-lemma iSQR: "iSQR x = x * x"
- sorry
-
-lemma numeral_exp: "(ALL x. x ^ ALT_ZERO = NUMERAL_BIT1 ALT_ZERO) &
-(ALL x xa. x ^ NUMERAL_BIT1 xa = x * iSQR (x ^ xa)) &
-(ALL x xa. x ^ NUMERAL_BIT2 xa = iSQR x * iSQR (x ^ xa))"
- sorry
-
-lemma numeral_evenodd: "EVEN ALT_ZERO &
-EVEN (NUMERAL_BIT2 x) &
-~ EVEN (NUMERAL_BIT1 x) &
-~ ODD ALT_ZERO & ~ ODD (NUMERAL_BIT2 x) & ODD (NUMERAL_BIT1 x)"
- sorry
-
-lemma numeral_fact: "FACT n = (if n = 0 then 1 else n * FACT (PRE n))"
- sorry
-
-lemma numeral_funpow: "(f ^^ n) x = (if n = 0 then x else (f ^^ (n - 1)) (f x))"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" ind_type
-
-lemma INJ_INVERSE2: "(!!(x1::'A) (y1::'B) (x2::'A) y2::'B.
- ((P::'A => 'B => 'C) x1 y1 = P x2 y2) = (x1 = x2 & y1 = y2))
-==> EX (x::'C => 'A) Y::'C => 'B.
- ALL (xa::'A) y::'B. x (P xa y) = xa & Y (P xa y) = y"
- sorry
-
-definition
- NUMPAIR :: "nat => nat => nat" where
- "NUMPAIR == %x y. 2 ^ x * (2 * y + 1)"
-
-lemma NUMPAIR: "NUMPAIR x y = 2 ^ x * (2 * y + 1)"
- sorry
-
-lemma NUMPAIR_INJ_LEMMA: "NUMPAIR x xa = NUMPAIR xb xc ==> x = xb"
- sorry
-
-lemma NUMPAIR_INJ: "(NUMPAIR x1 y1 = NUMPAIR x2 y2) = (x1 = x2 & y1 = y2)"
- sorry
-
-consts
- NUMSND :: "nat => nat"
- NUMFST :: "nat => nat"
-
-specification (NUMFST NUMSND) NUMPAIR_DEST: "ALL x y. NUMFST (NUMPAIR x y) = x & NUMSND (NUMPAIR x y) = y"
- sorry
-
-definition
- NUMSUM :: "bool => nat => nat" where
- "NUMSUM == %b x. if b then Suc (2 * x) else 2 * x"
-
-lemma NUMSUM: "NUMSUM b x = (if b then Suc (2 * x) else 2 * x)"
- sorry
-
-lemma NUMSUM_INJ: "(NUMSUM b1 x1 = NUMSUM b2 x2) = (b1 = b2 & x1 = x2)"
- sorry
-
-consts
- NUMRIGHT :: "nat => nat"
- NUMLEFT :: "nat => bool"
-
-specification (NUMLEFT NUMRIGHT) NUMSUM_DEST: "ALL x y. NUMLEFT (NUMSUM x y) = x & NUMRIGHT (NUMSUM x y) = y"
- sorry
-
-definition
- INJN :: "nat => nat => 'a => bool" where
- "INJN == %m n a. n = m"
-
-lemma INJN: "INJN m = (%n a. n = m)"
- sorry
-
-lemma INJN_INJ: "(INJN n1 = INJN n2) = (n1 = n2)"
- sorry
-
-definition
- INJA :: "'a => nat => 'a => bool" where
- "INJA == %a n b. b = a"
-
-lemma INJA: "INJA a = (%n b. b = a)"
- sorry
-
-lemma INJA_INJ: "(INJA a1 = INJA a2) = (a1 = a2)"
- sorry
-
-definition
- INJF :: "(nat => nat => 'a => bool) => nat => 'a => bool" where
- "INJF == %f n. f (NUMFST n) (NUMSND n)"
-
-lemma INJF: "INJF f = (%n. f (NUMFST n) (NUMSND n))"
- sorry
-
-lemma INJF_INJ: "(INJF f1 = INJF f2) = (f1 = f2)"
- sorry
-
-definition
- INJP :: "(nat => 'a => bool) => (nat => 'a => bool) => nat => 'a => bool" where
- "INJP ==
-%f1 f2 n a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a"
-
-lemma INJP: "INJP f1 f2 =
-(%n a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a)"
- sorry
-
-lemma INJP_INJ: "(INJP f1 f2 = INJP f1' f2') = (f1 = f1' & f2 = f2')"
- sorry
-
-definition
- ZCONSTR :: "nat => 'a => (nat => nat => 'a => bool) => nat => 'a => bool" where
- "ZCONSTR == %c i r. INJP (INJN (Suc c)) (INJP (INJA i) (INJF r))"
-
-lemma ZCONSTR: "ZCONSTR c i r = INJP (INJN (Suc c)) (INJP (INJA i) (INJF r))"
- sorry
-
-definition
- ZBOT :: "nat => 'a => bool" where
- "ZBOT == INJP (INJN 0) (SOME z. True)"
-
-lemma ZBOT: "ZBOT = INJP (INJN 0) (SOME z. True)"
- sorry
-
-lemma ZCONSTR_ZBOT: "ZCONSTR x xa xb ~= ZBOT"
- sorry
-
-definition
- ZRECSPACE :: "(nat => 'a => bool) => bool" where
- "ZRECSPACE ==
-%a0. ALL ZRECSPACE'.
- (ALL a0.
- a0 = ZBOT |
- (EX c i r. a0 = ZCONSTR c i r & (ALL n. ZRECSPACE' (r n))) -->
- ZRECSPACE' a0) -->
- ZRECSPACE' a0"
-
-lemma ZRECSPACE: "ZRECSPACE =
-(%a0. ALL ZRECSPACE'.
- (ALL a0.
- a0 = ZBOT |
- (EX c i r. a0 = ZCONSTR c i r & (ALL n. ZRECSPACE' (r n))) -->
- ZRECSPACE' a0) -->
- ZRECSPACE' a0)"
- sorry
-
-lemma ZRECSPACE_rules: "(op &::bool => bool => bool)
- ((ZRECSPACE::(nat => 'a::type => bool) => bool)
- (ZBOT::nat => 'a::type => bool))
- ((All::(nat => bool) => bool)
- (%c::nat.
- (All::('a::type => bool) => bool)
- (%i::'a::type.
- (All::((nat => nat => 'a::type => bool) => bool) => bool)
- (%r::nat => nat => 'a::type => bool.
- (op -->::bool => bool => bool)
- ((All::(nat => bool) => bool)
- (%n::nat.
- (ZRECSPACE::(nat => 'a::type => bool) => bool)
- (r n)))
- ((ZRECSPACE::(nat => 'a::type => bool) => bool)
- ((ZCONSTR::nat
- => 'a::type
- => (nat => nat => 'a::type => bool)
- => nat => 'a::type => bool)
- c i r))))))"
- sorry
-
-lemma ZRECSPACE_ind: "[| x ZBOT & (ALL c i r. (ALL n. x (r n)) --> x (ZCONSTR c i r));
- ZRECSPACE a0 |]
-==> x a0"
- sorry
-
-lemma ZRECSPACE_cases: "ZRECSPACE a0 =
-(a0 = ZBOT | (EX c i r. a0 = ZCONSTR c i r & (ALL n. ZRECSPACE (r n))))"
- sorry
-
-typedef (open) ('a) recspace = "Collect ZRECSPACE :: (nat \<Rightarrow> 'a\<Colon>type \<Rightarrow> bool) set"
- sorry
-
-lemmas recspace_TY_DEF = typedef_hol2hol4 [OF type_definition_recspace]
-
-consts
- mk_rec :: "(nat => 'a => bool) => 'a recspace"
- dest_rec :: "'a recspace => nat => 'a => bool"
-
-specification (dest_rec mk_rec) recspace_repfns: "(ALL a::'a recspace. mk_rec (dest_rec a) = a) &
-(ALL r::nat => 'a => bool. ZRECSPACE r = (dest_rec (mk_rec r) = r))"
- sorry
-
-definition
- BOTTOM :: "'a recspace" where
- "BOTTOM == mk_rec ZBOT"
-
-lemma BOTTOM: "BOTTOM = mk_rec ZBOT"
- sorry
-
-definition
- CONSTR :: "nat => 'a => (nat => 'a recspace) => 'a recspace" where
- "CONSTR == %c i r. mk_rec (ZCONSTR c i (%n. dest_rec (r n)))"
-
-lemma CONSTR: "CONSTR c i r = mk_rec (ZCONSTR c i (%n. dest_rec (r n)))"
- sorry
-
-lemma MK_REC_INJ: "[| mk_rec x = mk_rec y; ZRECSPACE x & ZRECSPACE y |] ==> x = y"
- sorry
-
-lemma DEST_REC_INJ: "(dest_rec x = dest_rec y) = (x = y)"
- sorry
-
-lemma CONSTR_BOT: "CONSTR c i r ~= BOTTOM"
- sorry
-
-lemma CONSTR_INJ: "(CONSTR c1 i1 r1 = CONSTR c2 i2 r2) = (c1 = c2 & i1 = i2 & r1 = r2)"
- sorry
-
-lemma CONSTR_IND: "P BOTTOM & (ALL c i r. (ALL n. P (r n)) --> P (CONSTR c i r)) ==> P x"
- sorry
-
-lemma CONSTR_REC: "EX f. ALL c i r. f (CONSTR c i r) = Fn c i r (%n. f (r n))"
- sorry
-
-consts
- FCONS :: "'a => (nat => 'a) => nat => 'a"
-
-specification (FCONS) FCONS: "(ALL (a::'a) f::nat => 'a. FCONS a f (0::nat) = a) &
-(ALL (a::'a) (f::nat => 'a) n::nat. FCONS a f (Suc n) = f n)"
- sorry
-
-definition
- FNIL :: "nat => 'a" where
- "FNIL == %n. SOME x. True"
-
-lemma FNIL: "FNIL n = (SOME x. True)"
- sorry
-
-definition
- ISO :: "('a => 'b) => ('b => 'a) => bool" where
- "ISO == %f g. (ALL x. f (g x) = x) & (ALL y. g (f y) = y)"
-
-lemma ISO: "ISO f g = ((ALL x. f (g x) = x) & (ALL y. g (f y) = y))"
- sorry
-
-lemma ISO_REFL: "ISO (%x. x) (%x. x)"
- sorry
-
-lemma ISO_FUN: "ISO (f::'a => 'c) (f'::'c => 'a) & ISO (g::'b => 'd) (g'::'d => 'b)
-==> ISO (%(h::'a => 'b) a'::'c. g (h (f' a')))
- (%(h::'c => 'd) a::'a. g' (h (f a)))"
- sorry
-
-lemma ISO_USAGE: "ISO f g
-==> (ALL P. All P = (ALL x. P (g x))) &
- (ALL P. Ex P = (EX x. P (g x))) & (ALL a b. (a = g b) = (f a = b))"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" divides
-
-lemma DIVIDES_FACT: "0 < b ==> b dvd FACT b"
- sorry
-
-lemma DIVIDES_MULT_LEFT: "((x::nat) * (xa::nat) dvd xa) = (xa = (0::nat) | x = (1::nat))"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" prime
-
-consts
- prime :: "nat => bool"
-
-defs
- prime_primdef: "prime.prime == %a. a ~= 1 & (ALL b. b dvd a --> b = a | b = 1)"
-
-lemma prime_def: "prime.prime a = (a ~= 1 & (ALL b. b dvd a --> b = a | b = 1))"
- sorry
-
-lemma NOT_PRIME_0: "~ prime.prime 0"
- sorry
-
-lemma NOT_PRIME_1: "~ prime.prime 1"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" list
-
-consts
- EL :: "nat => 'a list => 'a"
-
-specification (EL) EL: "(ALL l::'a list. EL (0::nat) l = hd l) &
-(ALL (l::'a list) n::nat. EL (Suc n) l = EL n (tl l))"
- sorry
-
-lemma NULL: "(op &::bool => bool => bool)
- ((List.null::'a::type list => bool) ([]::'a::type list))
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (All::('a::type list => bool) => bool)
- (%xa::'a::type list.
- (Not::bool => bool)
- ((List.null::'a::type list => bool)
- ((op #::'a::type => 'a::type list => 'a::type list) x xa)))))"
- sorry
-
-lemma list_case_compute: "list_case (b::'b) (f::'a => 'a list => 'b) (l::'a list) =
-(if List.null l then b else f (hd l) (tl l))"
- sorry
-
-lemma LIST_NOT_EQ: "l1 ~= l2 ==> x # l1 ~= xa # l2"
- sorry
-
-lemma NOT_EQ_LIST: "h1 ~= h2 ==> h1 # x ~= h2 # xa"
- sorry
-
-lemma EQ_LIST: "[| h1 = h2; l1 = l2 |] ==> h1 # l1 = h2 # l2"
- sorry
-
-lemma CONS: "~ List.null l ==> hd l # tl l = l"
- sorry
-
-lemma MAP_EQ_NIL: "(map (f::'a => 'b) (l::'a list) = []) = (l = []) & ([] = map f l) = (l = [])"
- sorry
-
-lemma EVERY_EL: "list_all P l = (ALL n<length l. P (EL n l))"
- sorry
-
-lemma EVERY_CONJ: "list_all (%x. P x & Q x) l = (list_all P l & list_all Q l)"
- sorry
-
-lemma EVERY_MEM: "list_all P l = (ALL e. List.member l e --> P e)"
- sorry
-
-lemma EXISTS_MEM: "list_ex P l = (EX e. List.member l e & P e)"
- sorry
-
-lemma MEM_APPEND: "List.member (l1 @ l2) e = (List.member l1 e | List.member l2 e)"
- sorry
-
-lemma NOT_EVERY: "(~ list_all P l) = list_ex (Not o P) l"
- sorry
-
-lemma NOT_EXISTS: "(~ list_ex P l) = list_all (Not o P) l"
- sorry
-
-lemma MEM_MAP: "List.member (map (f::'a => 'b) (l::'a list)) (x::'b) =
-(EX y::'a. x = f y & List.member l y)"
- sorry
-
-lemma LENGTH_CONS: "(length l = Suc n) = (EX h l'. length l' = n & l = h # l')"
- sorry
-
-lemma LENGTH_EQ_CONS: "(ALL l. length l = Suc n --> P l) =
-(ALL l. length l = n --> (ALL x. P (x # l)))"
- sorry
-
-lemma LENGTH_EQ_NIL: "(ALL l. length l = 0 --> P l) = P []"
- sorry
-
-lemma CONS_ACYCLIC: "l ~= x # l & x # l ~= l"
- sorry
-
-lemma APPEND_eq_NIL: "(ALL (l1::'a list) l2::'a list. ([] = l1 @ l2) = (l1 = [] & l2 = [])) &
-(ALL (l1::'a list) l2::'a list. (l1 @ l2 = []) = (l1 = [] & l2 = []))"
- sorry
-
-lemma APPEND_11: "(ALL (l1::'a list) (l2::'a list) l3::'a list.
- (l1 @ l2 = l1 @ l3) = (l2 = l3)) &
-(ALL (l1::'a list) (l2::'a list) l3::'a list.
- (l2 @ l1 = l3 @ l1) = (l2 = l3))"
- sorry
-
-lemma EL_compute: "EL n l = (if n = 0 then hd l else EL (PRE n) (tl l))"
- sorry
-
-lemma WF_LIST_PRED: "WF (%L1 L2. EX h. L2 = h # L1)"
- sorry
-
-lemma list_size_cong: "M = N & (ALL x. List.member N x --> f x = f' x)
-==> Compatibility.list_size f M = Compatibility.list_size f' N"
- sorry
-
-lemma FOLDR_CONG: "l = l' & b = b' & (ALL x a. List.member l' x --> f x a = f' x a)
-==> foldr f l b = foldr f' l' b'"
- sorry
-
-lemma FOLDL_CONG: "l = l' & b = b' & (ALL x a. List.member l' x --> f a x = f' a x)
-==> foldl f b l = foldl f' b' l'"
- sorry
-
-lemma MAP_CONG: "l1 = l2 & (ALL x. List.member l2 x --> f x = f' x) ==> map f l1 = map f' l2"
- sorry
-
-lemma EXISTS_CONG: "l1 = l2 & (ALL x. List.member l2 x --> P x = P' x)
-==> list_ex P l1 = list_ex P' l2"
- sorry
-
-lemma EVERY_CONG: "l1 = l2 & (ALL x. List.member l2 x --> P x = P' x)
-==> list_all P l1 = list_all P' l2"
- sorry
-
-lemma EVERY_MONOTONIC: "[| !!x. P x ==> Q x; list_all P l |] ==> list_all Q l"
- sorry
-
-lemma LENGTH_ZIP: "length l1 = length l2
-==> length (zip l1 l2) = length l1 & length (zip l1 l2) = length l2"
- sorry
-
-lemma LENGTH_UNZIP: "length (fst (unzip pl)) = length pl & length (snd (unzip pl)) = length pl"
- sorry
-
-lemma ZIP_UNZIP: "ZIP (unzip l) = l"
- sorry
-
-lemma UNZIP_ZIP: "length l1 = length l2 ==> unzip (zip l1 l2) = (l1, l2)"
- sorry
-
-lemma ZIP_MAP: "length l1 = length l2
-==> zip (map f1 l1) l2 = map (%p. (f1 (fst p), snd p)) (zip l1 l2) &
- zip l1 (map f2 l2) = map (%p. (fst p, f2 (snd p))) (zip l1 l2)"
- sorry
-
-lemma MEM_ZIP: "length l1 = length l2
-==> List.member (zip l1 l2) p = (EX n<length l1. p = (EL n l1, EL n l2))"
- sorry
-
-lemma EL_ZIP: "length l1 = length l2 & n < length l1
-==> EL n (zip l1 l2) = (EL n l1, EL n l2)"
- sorry
-
-lemma MAP2_ZIP: "length l1 = length l2 ==> map2 f l1 l2 = map (%(x, y). f x y) (zip l1 l2)"
- sorry
-
-lemma MEM_EL: "List.member l x = (EX n<length l. x = EL n l)"
- sorry
-
-lemma LAST_CONS: "(ALL x::'a. last [x] = x) &
-(ALL (x::'a) (xa::'a) xb::'a list. last (x # xa # xb) = last (xa # xb))"
- sorry
-
-lemma FRONT_CONS: "(ALL x::'a. butlast [x] = []) &
-(ALL (x::'a) (xa::'a) xb::'a list.
- butlast (x # xa # xb) = x # butlast (xa # xb))"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" pred_set
-
-lemma EXTENSION: "(s = t) = (ALL x. IN x s = IN x t)"
- sorry
-
-lemma NOT_EQUAL_SETS: "(x ~= xa) = (EX xb. IN xb xa = (~ IN xb x))"
- sorry
-
-lemma NUM_SET_WOP: "(EX n::nat. IN n (s::nat => bool)) =
-(EX n::nat. IN n s & (ALL m::nat. IN m s --> n <= m))"
- sorry
-
-consts
- GSPEC :: "('b => 'a * bool) => 'a => bool"
-
-specification (GSPEC) GSPECIFICATION: "ALL (f::'b => 'a * bool) v::'a. IN v (GSPEC f) = (EX x::'b. (v, True) = f x)"
- sorry
-
-lemma SET_MINIMUM: "(EX x::'a. IN x (s::'a => bool)) =
-(EX x::'a. IN x s & (ALL y::'a. IN y s --> (M::'a => nat) x <= M y))"
- sorry
-
-definition
- EMPTY :: "'a => bool" where
- "EMPTY == %x. False"
-
-lemma EMPTY_DEF: "EMPTY = (%x. False)"
- sorry
-
-lemma NOT_IN_EMPTY: "~ IN x EMPTY"
- sorry
-
-lemma MEMBER_NOT_EMPTY: "(EX xa. IN xa x) = (x ~= EMPTY)"
- sorry
-
-definition
- UNIV :: "'a => bool" where
- "UNIV == %x. True"
-
-lemma UNIV_DEF: "pred_set.UNIV = (%x. True)"
- sorry
-
-lemma IN_UNIV: "IN x pred_set.UNIV"
- sorry
-
-lemma UNIV_NOT_EMPTY: "pred_set.UNIV ~= EMPTY"
- sorry
-
-lemma EMPTY_NOT_UNIV: "EMPTY ~= pred_set.UNIV"
- sorry
-
-lemma EQ_UNIV: "(ALL x. IN x s) = (s = pred_set.UNIV)"
- sorry
-
-definition
- SUBSET :: "('a => bool) => ('a => bool) => bool" where
- "SUBSET == %s t. ALL x. IN x s --> IN x t"
-
-lemma SUBSET_DEF: "SUBSET s t = (ALL x. IN x s --> IN x t)"
- sorry
-
-lemma SUBSET_TRANS: "SUBSET x xa & SUBSET xa xb ==> SUBSET x xb"
- sorry
-
-lemma SUBSET_REFL: "SUBSET x x"
- sorry
-
-lemma SUBSET_ANTISYM: "SUBSET x xa & SUBSET xa x ==> x = xa"
- sorry
-
-lemma EMPTY_SUBSET: "SUBSET EMPTY x"
- sorry
-
-lemma SUBSET_EMPTY: "SUBSET x EMPTY = (x = EMPTY)"
- sorry
-
-lemma SUBSET_UNIV: "SUBSET x pred_set.UNIV"
- sorry
-
-lemma UNIV_SUBSET: "SUBSET pred_set.UNIV x = (x = pred_set.UNIV)"
- sorry
-
-definition
- PSUBSET :: "('a => bool) => ('a => bool) => bool" where
- "PSUBSET == %s t. SUBSET s t & s ~= t"
-
-lemma PSUBSET_DEF: "PSUBSET s t = (SUBSET s t & s ~= t)"
- sorry
-
-lemma PSUBSET_TRANS: "PSUBSET x xa & PSUBSET xa xb ==> PSUBSET x xb"
- sorry
-
-lemma PSUBSET_IRREFL: "~ PSUBSET x x"
- sorry
-
-lemma NOT_PSUBSET_EMPTY: "~ PSUBSET x EMPTY"
- sorry
-
-lemma NOT_UNIV_PSUBSET: "~ PSUBSET pred_set.UNIV x"
- sorry
-
-lemma PSUBSET_UNIV: "PSUBSET x pred_set.UNIV = (EX xa. ~ IN xa x)"
- sorry
-
-definition
- UNION :: "('a => bool) => ('a => bool) => 'a => bool" where
- "UNION == %s t. GSPEC (%x. (x, IN x s | IN x t))"
-
-lemma UNION_DEF: "pred_set.UNION s t = GSPEC (%x. (x, IN x s | IN x t))"
- sorry
-
-lemma IN_UNION: "IN xb (pred_set.UNION x xa) = (IN xb x | IN xb xa)"
- sorry
-
-lemma UNION_ASSOC: "pred_set.UNION x (pred_set.UNION xa xb) =
-pred_set.UNION (pred_set.UNION x xa) xb"
- sorry
-
-lemma UNION_IDEMPOT: "pred_set.UNION x x = x"
- sorry
-
-lemma UNION_COMM: "pred_set.UNION x xa = pred_set.UNION xa x"
- sorry
-
-lemma SUBSET_UNION: "(ALL (x::'a => bool) xa::'a => bool. SUBSET x (pred_set.UNION x xa)) &
-(ALL (x::'a => bool) xa::'a => bool. SUBSET x (pred_set.UNION xa x))"
- sorry
-
-lemma UNION_SUBSET: "SUBSET (pred_set.UNION s t) u = (SUBSET s u & SUBSET t u)"
- sorry
-
-lemma SUBSET_UNION_ABSORPTION: "SUBSET x xa = (pred_set.UNION x xa = xa)"
- sorry
-
-lemma UNION_EMPTY: "(ALL x::'a => bool. pred_set.UNION EMPTY x = x) &
-(ALL x::'a => bool. pred_set.UNION x EMPTY = x)"
- sorry
-
-lemma UNION_UNIV: "(ALL x::'a => bool. pred_set.UNION pred_set.UNIV x = pred_set.UNIV) &
-(ALL x::'a => bool. pred_set.UNION x pred_set.UNIV = pred_set.UNIV)"
- sorry
-
-lemma EMPTY_UNION: "(pred_set.UNION x xa = EMPTY) = (x = EMPTY & xa = EMPTY)"
- sorry
-
-definition
- INTER :: "('a => bool) => ('a => bool) => 'a => bool" where
- "INTER == %s t. GSPEC (%x. (x, IN x s & IN x t))"
-
-lemma INTER_DEF: "pred_set.INTER s t = GSPEC (%x. (x, IN x s & IN x t))"
- sorry
-
-lemma IN_INTER: "IN xb (pred_set.INTER x xa) = (IN xb x & IN xb xa)"
- sorry
-
-lemma INTER_ASSOC: "pred_set.INTER x (pred_set.INTER xa xb) =
-pred_set.INTER (pred_set.INTER x xa) xb"
- sorry
-
-lemma INTER_IDEMPOT: "pred_set.INTER x x = x"
- sorry
-
-lemma INTER_COMM: "pred_set.INTER x xa = pred_set.INTER xa x"
- sorry
-
-lemma INTER_SUBSET: "(ALL (x::'a => bool) xa::'a => bool. SUBSET (pred_set.INTER x xa) x) &
-(ALL (x::'a => bool) xa::'a => bool. SUBSET (pred_set.INTER xa x) x)"
- sorry
-
-lemma SUBSET_INTER: "SUBSET s (pred_set.INTER t u) = (SUBSET s t & SUBSET s u)"
- sorry
-
-lemma SUBSET_INTER_ABSORPTION: "SUBSET x xa = (pred_set.INTER x xa = x)"
- sorry
-
-lemma INTER_EMPTY: "(ALL x::'a => bool. pred_set.INTER EMPTY x = EMPTY) &
-(ALL x::'a => bool. pred_set.INTER x EMPTY = EMPTY)"
- sorry
-
-lemma INTER_UNIV: "(ALL x::'a => bool. pred_set.INTER pred_set.UNIV x = x) &
-(ALL x::'a => bool. pred_set.INTER x pred_set.UNIV = x)"
- sorry
-
-lemma UNION_OVER_INTER: "pred_set.INTER x (pred_set.UNION xa xb) =
-pred_set.UNION (pred_set.INTER x xa) (pred_set.INTER x xb)"
- sorry
-
-lemma INTER_OVER_UNION: "pred_set.UNION x (pred_set.INTER xa xb) =
-pred_set.INTER (pred_set.UNION x xa) (pred_set.UNION x xb)"
- sorry
-
-definition
- DISJOINT :: "('a => bool) => ('a => bool) => bool" where
- "DISJOINT == %s t. pred_set.INTER s t = EMPTY"
-
-lemma DISJOINT_DEF: "DISJOINT s t = (pred_set.INTER s t = EMPTY)"
- sorry
-
-lemma IN_DISJOINT: "DISJOINT x xa = (~ (EX xb. IN xb x & IN xb xa))"
- sorry
-
-lemma DISJOINT_SYM: "DISJOINT x xa = DISJOINT xa x"
- sorry
-
-lemma DISJOINT_EMPTY: "DISJOINT EMPTY x & DISJOINT x EMPTY"
- sorry
-
-lemma DISJOINT_EMPTY_REFL: "(x = EMPTY) = DISJOINT x x"
- sorry
-
-lemma DISJOINT_UNION: "DISJOINT (pred_set.UNION x xa) xb = (DISJOINT x xb & DISJOINT xa xb)"
- sorry
-
-lemma DISJOINT_UNION_BOTH: "DISJOINT (pred_set.UNION s t) u = (DISJOINT s u & DISJOINT t u) &
-DISJOINT u (pred_set.UNION s t) = (DISJOINT s u & DISJOINT t u)"
- sorry
-
-definition
- DIFF :: "('a => bool) => ('a => bool) => 'a => bool" where
- "DIFF == %s t. GSPEC (%x. (x, IN x s & ~ IN x t))"
-
-lemma DIFF_DEF: "DIFF s t = GSPEC (%x. (x, IN x s & ~ IN x t))"
- sorry
-
-lemma IN_DIFF: "IN x (DIFF s t) = (IN x s & ~ IN x t)"
- sorry
-
-lemma DIFF_EMPTY: "DIFF s EMPTY = s"
- sorry
-
-lemma EMPTY_DIFF: "DIFF EMPTY s = EMPTY"
- sorry
-
-lemma DIFF_UNIV: "DIFF s pred_set.UNIV = EMPTY"
- sorry
-
-lemma DIFF_DIFF: "DIFF (DIFF x xa) xa = DIFF x xa"
- sorry
-
-lemma DIFF_EQ_EMPTY: "DIFF x x = EMPTY"
- sorry
-
-definition
- INSERT :: "'a => ('a => bool) => 'a => bool" where
- "INSERT == %x s. GSPEC (%y. (y, y = x | IN y s))"
-
-lemma INSERT_DEF: "INSERT x s = GSPEC (%y. (y, y = x | IN y s))"
- sorry
-
-lemma IN_INSERT: "IN x (INSERT xa xb) = (x = xa | IN x xb)"
- sorry
-
-lemma COMPONENT: "IN x (INSERT x xa)"
- sorry
-
-lemma SET_CASES: "x = EMPTY | (EX xa xb. x = INSERT xa xb & ~ IN xa xb)"
- sorry
-
-lemma DECOMPOSITION: "IN x s = (EX t. s = INSERT x t & ~ IN x t)"
- sorry
-
-lemma ABSORPTION: "IN x xa = (INSERT x xa = xa)"
- sorry
-
-lemma INSERT_INSERT: "INSERT x (INSERT x xa) = INSERT x xa"
- sorry
-
-lemma INSERT_COMM: "INSERT x (INSERT xa xb) = INSERT xa (INSERT x xb)"
- sorry
-
-lemma INSERT_UNIV: "INSERT x pred_set.UNIV = pred_set.UNIV"
- sorry
-
-lemma NOT_INSERT_EMPTY: "INSERT x xa ~= EMPTY"
- sorry
-
-lemma NOT_EMPTY_INSERT: "EMPTY ~= INSERT x xa"
- sorry
-
-lemma INSERT_UNION: "pred_set.UNION (INSERT x s) t =
-(if IN x t then pred_set.UNION s t else INSERT x (pred_set.UNION s t))"
- sorry
-
-lemma INSERT_UNION_EQ: "pred_set.UNION (INSERT x s) t = INSERT x (pred_set.UNION s t)"
- sorry
-
-lemma INSERT_INTER: "pred_set.INTER (INSERT x s) t =
-(if IN x t then INSERT x (pred_set.INTER s t) else pred_set.INTER s t)"
- sorry
-
-lemma DISJOINT_INSERT: "DISJOINT (INSERT x xa) xb = (DISJOINT xa xb & ~ IN x xb)"
- sorry
-
-lemma INSERT_SUBSET: "SUBSET (INSERT x xa) xb = (IN x xb & SUBSET xa xb)"
- sorry
-
-lemma SUBSET_INSERT: "~ IN x xa ==> SUBSET xa (INSERT x xb) = SUBSET xa xb"
- sorry
-
-lemma INSERT_DIFF: "DIFF (INSERT x s) t = (if IN x t then DIFF s t else INSERT x (DIFF s t))"
- sorry
-
-definition
- DELETE :: "('a => bool) => 'a => 'a => bool" where
- "DELETE == %s x. DIFF s (INSERT x EMPTY)"
-
-lemma DELETE_DEF: "DELETE s x = DIFF s (INSERT x EMPTY)"
- sorry
-
-lemma IN_DELETE: "IN xa (DELETE x xb) = (IN xa x & xa ~= xb)"
- sorry
-
-lemma DELETE_NON_ELEMENT: "(~ IN x xa) = (DELETE xa x = xa)"
- sorry
-
-lemma IN_DELETE_EQ: "(IN x s = IN x' s) = (IN x (DELETE s x') = IN x' (DELETE s x))"
- sorry
-
-lemma EMPTY_DELETE: "DELETE EMPTY x = EMPTY"
- sorry
-
-lemma DELETE_DELETE: "DELETE (DELETE xa x) x = DELETE xa x"
- sorry
-
-lemma DELETE_COMM: "DELETE (DELETE xb x) xa = DELETE (DELETE xb xa) x"
- sorry
-
-lemma DELETE_SUBSET: "SUBSET (DELETE xa x) xa"
- sorry
-
-lemma SUBSET_DELETE: "SUBSET xa (DELETE xb x) = (~ IN x xa & SUBSET xa xb)"
- sorry
-
-lemma SUBSET_INSERT_DELETE: "SUBSET s (INSERT x t) = SUBSET (DELETE s x) t"
- sorry
-
-lemma DIFF_INSERT: "DIFF x (INSERT xb xa) = DIFF (DELETE x xb) xa"
- sorry
-
-lemma PSUBSET_INSERT_SUBSET: "PSUBSET x xa = (EX xb. ~ IN xb x & SUBSET (INSERT xb x) xa)"
- sorry
-
-lemma PSUBSET_MEMBER: "PSUBSET s t = (SUBSET s t & (EX y. IN y t & ~ IN y s))"
- sorry
-
-lemma DELETE_INSERT: "DELETE (INSERT x xb) xa =
-(if x = xa then DELETE xb xa else INSERT x (DELETE xb xa))"
- sorry
-
-lemma INSERT_DELETE: "IN x xa ==> INSERT x (DELETE xa x) = xa"
- sorry
-
-lemma DELETE_INTER: "pred_set.INTER (DELETE x xb) xa = DELETE (pred_set.INTER x xa) xb"
- sorry
-
-lemma DISJOINT_DELETE_SYM: "DISJOINT (DELETE x xb) xa = DISJOINT (DELETE xa xb) x"
- sorry
-
-consts
- CHOICE :: "('a => bool) => 'a"
-
-specification (CHOICE) CHOICE_DEF: "ALL x. x ~= EMPTY --> IN (CHOICE x) x"
- sorry
-
-definition
- REST :: "('a => bool) => 'a => bool" where
- "REST == %s. DELETE s (CHOICE s)"
-
-lemma REST_DEF: "REST s = DELETE s (CHOICE s)"
- sorry
-
-lemma CHOICE_NOT_IN_REST: "~ IN (CHOICE x) (REST x)"
- sorry
-
-lemma CHOICE_INSERT_REST: "s ~= EMPTY ==> INSERT (CHOICE s) (REST s) = s"
- sorry
-
-lemma REST_SUBSET: "SUBSET (REST x) x"
- sorry
-
-lemma REST_PSUBSET: "x ~= EMPTY ==> PSUBSET (REST x) x"
- sorry
-
-definition
- SING :: "('a => bool) => bool" where
- "SING == %s. EX x. s = INSERT x EMPTY"
-
-lemma SING_DEF: "SING s = (EX x. s = INSERT x EMPTY)"
- sorry
-
-lemma SING: "SING (INSERT x EMPTY)"
- sorry
-
-lemma IN_SING: "IN x (INSERT xa EMPTY) = (x = xa)"
- sorry
-
-lemma NOT_SING_EMPTY: "INSERT x EMPTY ~= EMPTY"
- sorry
-
-lemma NOT_EMPTY_SING: "EMPTY ~= INSERT x EMPTY"
- sorry
-
-lemma EQUAL_SING: "(INSERT x EMPTY = INSERT xa EMPTY) = (x = xa)"
- sorry
-
-lemma DISJOINT_SING_EMPTY: "DISJOINT (INSERT x EMPTY) EMPTY"
- sorry
-
-lemma INSERT_SING_UNION: "INSERT xa x = pred_set.UNION (INSERT xa EMPTY) x"
- sorry
-
-lemma SING_DELETE: "DELETE (INSERT x EMPTY) x = EMPTY"
- sorry
-
-lemma DELETE_EQ_SING: "IN xa x ==> (DELETE x xa = EMPTY) = (x = INSERT xa EMPTY)"
- sorry
-
-lemma CHOICE_SING: "CHOICE (INSERT x EMPTY) = x"
- sorry
-
-lemma REST_SING: "REST (INSERT x EMPTY) = EMPTY"
- sorry
-
-lemma SING_IFF_EMPTY_REST: "SING x = (x ~= EMPTY & REST x = EMPTY)"
- sorry
-
-definition
- IMAGE :: "('a => 'b) => ('a => bool) => 'b => bool" where
- "IMAGE == %f s. GSPEC (%x. (f x, IN x s))"
-
-lemma IMAGE_DEF: "IMAGE (f::'a => 'b) (s::'a => bool) = GSPEC (%x::'a. (f x, IN x s))"
- sorry
-
-lemma IN_IMAGE: "IN (x::'b) (IMAGE (xb::'a => 'b) (xa::'a => bool)) =
-(EX xc::'a. x = xb xc & IN xc xa)"
- sorry
-
-lemma IMAGE_IN: "IN x xa ==> IN (xb x) (IMAGE xb xa)"
- sorry
-
-lemma IMAGE_EMPTY: "IMAGE (x::'a => 'b) EMPTY = EMPTY"
- sorry
-
-lemma IMAGE_ID: "IMAGE (%x. x) x = x"
- sorry
-
-lemma IMAGE_COMPOSE: "IMAGE ((x::'b => 'c) o (xa::'a => 'b)) (xb::'a => bool) =
-IMAGE x (IMAGE xa xb)"
- sorry
-
-lemma IMAGE_INSERT: "IMAGE (x::'a => 'b) (INSERT (xa::'a) (xb::'a => bool)) =
-INSERT (x xa) (IMAGE x xb)"
- sorry
-
-lemma IMAGE_EQ_EMPTY: "(IMAGE (x::'a => 'b) (s::'a => bool) = EMPTY) = (s = EMPTY)"
- sorry
-
-lemma IMAGE_DELETE: "~ IN x s ==> IMAGE f (DELETE s x) = IMAGE f s"
- sorry
-
-lemma IMAGE_UNION: "IMAGE (x::'a => 'b) (pred_set.UNION (xa::'a => bool) (xb::'a => bool)) =
-pred_set.UNION (IMAGE x xa) (IMAGE x xb)"
- sorry
-
-lemma IMAGE_SUBSET: "SUBSET x xa ==> SUBSET (IMAGE xb x) (IMAGE xb xa)"
- sorry
-
-lemma IMAGE_INTER: "SUBSET
- (IMAGE (f::'a => 'b) (pred_set.INTER (s::'a => bool) (t::'a => bool)))
- (pred_set.INTER (IMAGE f s) (IMAGE f t))"
- sorry
-
-definition
- INJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" where
- "INJ ==
-%f s t.
- (ALL x. IN x s --> IN (f x) t) &
- (ALL x y. IN x s & IN y s --> f x = f y --> x = y)"
-
-lemma INJ_DEF: "INJ f s t =
-((ALL x. IN x s --> IN (f x) t) &
- (ALL x y. IN x s & IN y s --> f x = f y --> x = y))"
- sorry
-
-lemma INJ_ID: "INJ (%x. x) x x"
- sorry
-
-lemma INJ_COMPOSE: "INJ x xb xc & INJ xa xc xd ==> INJ (xa o x) xb xd"
- sorry
-
-lemma INJ_EMPTY: "All (INJ (x::'a => 'b) EMPTY) &
-(ALL xa::'a => bool. INJ x xa EMPTY = (xa = EMPTY))"
- sorry
-
-definition
- SURJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" where
- "SURJ ==
-%f s t.
- (ALL x. IN x s --> IN (f x) t) &
- (ALL x. IN x t --> (EX y. IN y s & f y = x))"
-
-lemma SURJ_DEF: "SURJ f s t =
-((ALL x. IN x s --> IN (f x) t) &
- (ALL x. IN x t --> (EX y. IN y s & f y = x)))"
- sorry
-
-lemma SURJ_ID: "SURJ (%x. x) x x"
- sorry
-
-lemma SURJ_COMPOSE: "SURJ x xb xc & SURJ xa xc xd ==> SURJ (xa o x) xb xd"
- sorry
-
-lemma SURJ_EMPTY: "(ALL xa::'b => bool. SURJ (x::'a => 'b) EMPTY xa = (xa = EMPTY)) &
-(ALL xa::'a => bool. SURJ x xa EMPTY = (xa = EMPTY))"
- sorry
-
-lemma IMAGE_SURJ: "SURJ x xa xb = (IMAGE x xa = xb)"
- sorry
-
-definition
- BIJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" where
- "BIJ == %f s t. INJ f s t & SURJ f s t"
-
-lemma BIJ_DEF: "BIJ f s t = (INJ f s t & SURJ f s t)"
- sorry
-
-lemma BIJ_ID: "BIJ (%x. x) x x"
- sorry
-
-lemma BIJ_EMPTY: "(ALL xa::'b => bool. BIJ (x::'a => 'b) EMPTY xa = (xa = EMPTY)) &
-(ALL xa::'a => bool. BIJ x xa EMPTY = (xa = EMPTY))"
- sorry
-
-lemma BIJ_COMPOSE: "BIJ x xb xc & BIJ xa xc xd ==> BIJ (xa o x) xb xd"
- sorry
-
-consts
- LINV :: "('a => 'b) => ('a => bool) => 'b => 'a"
-
-specification (LINV) LINV_DEF: "ALL f s t. INJ f s t --> (ALL x. IN x s --> LINV f s (f x) = x)"
- sorry
-
-consts
- RINV :: "('a => 'b) => ('a => bool) => 'b => 'a"
-
-specification (RINV) RINV_DEF: "ALL f s t. SURJ f s t --> (ALL x. IN x t --> f (RINV f s x) = x)"
- sorry
-
-definition
- FINITE :: "('a => bool) => bool" where
- "FINITE ==
-%s. ALL P. P EMPTY & (ALL s. P s --> (ALL e. P (INSERT e s))) --> P s"
-
-lemma FINITE_DEF: "FINITE s =
-(ALL P. P EMPTY & (ALL s. P s --> (ALL e. P (INSERT e s))) --> P s)"
- sorry
-
-lemma FINITE_EMPTY: "FINITE EMPTY"
- sorry
-
-lemma FINITE_INDUCT: "[| P EMPTY &
- (ALL s. FINITE s & P s --> (ALL e. ~ IN e s --> P (INSERT e s)));
- FINITE s |]
-==> P s"
- sorry
-
-lemma FINITE_INSERT: "FINITE (INSERT x s) = FINITE s"
- sorry
-
-lemma FINITE_DELETE: "FINITE (DELETE s x) = FINITE s"
- sorry
-
-lemma FINITE_UNION: "FINITE (pred_set.UNION s t) = (FINITE s & FINITE t)"
- sorry
-
-lemma INTER_FINITE: "FINITE s ==> FINITE (pred_set.INTER s t)"
- sorry
-
-lemma SUBSET_FINITE: "[| FINITE s; SUBSET t s |] ==> FINITE t"
- sorry
-
-lemma PSUBSET_FINITE: "[| FINITE x; PSUBSET xa x |] ==> FINITE xa"
- sorry
-
-lemma FINITE_DIFF: "FINITE s ==> FINITE (DIFF s t)"
- sorry
-
-lemma FINITE_SING: "FINITE (INSERT x EMPTY)"
- sorry
-
-lemma SING_FINITE: "SING x ==> FINITE x"
- sorry
-
-lemma IMAGE_FINITE: "FINITE s ==> FINITE (IMAGE f s)"
- sorry
-
-consts
- CARD :: "('a => bool) => nat"
-
-specification (CARD) CARD_DEF: "(op &::bool => bool => bool)
- ((op =::nat => nat => bool)
- ((CARD::('a::type => bool) => nat) (EMPTY::'a::type => bool)) (0::nat))
- ((All::(('a::type => bool) => bool) => bool)
- (%s::'a::type => bool.
- (op -->::bool => bool => bool)
- ((FINITE::('a::type => bool) => bool) s)
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (op =::nat => nat => bool)
- ((CARD::('a::type => bool) => nat)
- ((INSERT::'a::type
- => ('a::type => bool) => 'a::type => bool)
- x s))
- ((If::bool => nat => nat => nat)
- ((IN::'a::type => ('a::type => bool) => bool) x s)
- ((CARD::('a::type => bool) => nat) s)
- ((Suc::nat => nat)
- ((CARD::('a::type => bool) => nat) s)))))))"
- sorry
-
-lemma CARD_EMPTY: "CARD EMPTY = 0"
- sorry
-
-lemma CARD_INSERT: "FINITE s ==> CARD (INSERT x s) = (if IN x s then CARD s else Suc (CARD s))"
- sorry
-
-lemma CARD_EQ_0: "FINITE s ==> (CARD s = 0) = (s = EMPTY)"
- sorry
-
-lemma CARD_DELETE: "FINITE s ==> CARD (DELETE s x) = (if IN x s then CARD s - 1 else CARD s)"
- sorry
-
-lemma CARD_INTER_LESS_EQ: "FINITE s ==> CARD (pred_set.INTER s t) <= CARD s"
- sorry
-
-lemma CARD_UNION: "[| FINITE s; FINITE t |]
-==> CARD (pred_set.UNION s t) + CARD (pred_set.INTER s t) = CARD s + CARD t"
- sorry
-
-lemma CARD_SUBSET: "[| FINITE s; SUBSET t s |] ==> CARD t <= CARD s"
- sorry
-
-lemma CARD_PSUBSET: "[| FINITE s; PSUBSET t s |] ==> CARD t < CARD s"
- sorry
-
-lemma CARD_SING: "CARD (INSERT x EMPTY) = 1"
- sorry
-
-lemma SING_IFF_CARD1: "SING x = (CARD x = 1 & FINITE x)"
- sorry
-
-lemma CARD_DIFF: "[| FINITE t; FINITE s |]
-==> CARD (DIFF s t) = CARD s - CARD (pred_set.INTER s t)"
- sorry
-
-lemma LESS_CARD_DIFF: "[| FINITE t; FINITE s; CARD t < CARD s |] ==> 0 < CARD (DIFF s t)"
- sorry
-
-lemma FINITE_COMPLETE_INDUCTION: "[| !!x. [| !!y. PSUBSET y x ==> P y; FINITE x |] ==> P x; FINITE x |]
-==> P x"
- sorry
-
-definition
- INFINITE :: "('a => bool) => bool" where
- "INFINITE == %s. ~ FINITE s"
-
-lemma INFINITE_DEF: "INFINITE s = (~ FINITE s)"
- sorry
-
-lemma NOT_IN_FINITE: "(op =::bool => bool => bool)
- ((INFINITE::('a::type => bool) => bool) (pred_set.UNIV::'a::type => bool))
- ((All::(('a::type => bool) => bool) => bool)
- (%s::'a::type => bool.
- (op -->::bool => bool => bool)
- ((FINITE::('a::type => bool) => bool) s)
- ((Ex::('a::type => bool) => bool)
- (%x::'a::type.
- (Not::bool => bool)
- ((IN::'a::type => ('a::type => bool) => bool) x s)))))"
- sorry
-
-lemma INFINITE_INHAB: "INFINITE x ==> EX xa. IN xa x"
- sorry
-
-lemma IMAGE_11_INFINITE: "[| !!x y. f x = f y ==> x = y; INFINITE s |] ==> INFINITE (IMAGE f s)"
- sorry
-
-lemma INFINITE_SUBSET: "[| INFINITE x; SUBSET x xa |] ==> INFINITE xa"
- sorry
-
-lemma IN_INFINITE_NOT_FINITE: "INFINITE x & FINITE xa ==> EX xb. IN xb x & ~ IN xb xa"
- sorry
-
-lemma INFINITE_UNIV: "(op =::bool => bool => bool)
- ((INFINITE::('a::type => bool) => bool) (pred_set.UNIV::'a::type => bool))
- ((Ex::(('a::type => 'a::type) => bool) => bool)
- (%f::'a::type => 'a::type.
- (op &::bool => bool => bool)
- ((All::('a::type => bool) => bool)
- (%x::'a::type.
- (All::('a::type => bool) => bool)
- (%y::'a::type.
- (op -->::bool => bool => bool)
- ((op =::'a::type => 'a::type => bool) (f x) (f y))
- ((op =::'a::type => 'a::type => bool) x y))))
- ((Ex::('a::type => bool) => bool)
- (%y::'a::type.
- (All::('a::type => bool) => bool)
- (%x::'a::type.
- (op ~=::'a::type => 'a::type => bool) (f x) y)))))"
- sorry
-
-lemma FINITE_PSUBSET_INFINITE: "INFINITE x = (ALL xa. FINITE xa --> SUBSET xa x --> PSUBSET xa x)"
- sorry
-
-lemma FINITE_PSUBSET_UNIV: "(op =::bool => bool => bool)
- ((INFINITE::('a::type => bool) => bool) (pred_set.UNIV::'a::type => bool))
- ((All::(('a::type => bool) => bool) => bool)
- (%s::'a::type => bool.
- (op -->::bool => bool => bool)
- ((FINITE::('a::type => bool) => bool) s)
- ((PSUBSET::('a::type => bool) => ('a::type => bool) => bool) s
- (pred_set.UNIV::'a::type => bool))))"
- sorry
-
-lemma INFINITE_DIFF_FINITE: "INFINITE s & FINITE t ==> DIFF s t ~= EMPTY"
- sorry
-
-lemma FINITE_ISO_NUM: "FINITE s
-==> EX f. (ALL n m. n < CARD s & m < CARD s --> f n = f m --> n = m) &
- s = GSPEC (%n. (f n, n < CARD s))"
- sorry
-
-lemma FINITE_WEAK_ENUMERATE: "FINITE (x::'a => bool) =
-(EX (f::nat => 'a) b::nat. ALL e::'a. IN e x = (EX n<b. e = f n))"
- sorry
-
-definition
- BIGUNION :: "(('a => bool) => bool) => 'a => bool" where
- "BIGUNION == %P. GSPEC (%x. (x, EX p. IN p P & IN x p))"
-
-lemma BIGUNION: "BIGUNION P = GSPEC (%x. (x, EX p. IN p P & IN x p))"
- sorry
-
-lemma IN_BIGUNION: "IN x (BIGUNION xa) = (EX s. IN x s & IN s xa)"
- sorry
-
-lemma BIGUNION_EMPTY: "BIGUNION EMPTY = EMPTY"
- sorry
-
-lemma BIGUNION_SING: "BIGUNION (INSERT x EMPTY) = x"
- sorry
-
-lemma BIGUNION_UNION: "BIGUNION (pred_set.UNION x xa) = pred_set.UNION (BIGUNION x) (BIGUNION xa)"
- sorry
-
-lemma DISJOINT_BIGUNION: "(ALL (s::('a => bool) => bool) t::'a => bool.
- DISJOINT (BIGUNION s) t =
- (ALL s'::'a => bool. IN s' s --> DISJOINT s' t)) &
-(ALL (x::('a => bool) => bool) xa::'a => bool.
- DISJOINT xa (BIGUNION x) =
- (ALL xb::'a => bool. IN xb x --> DISJOINT xa xb))"
- sorry
-
-lemma BIGUNION_INSERT: "BIGUNION (INSERT x xa) = pred_set.UNION x (BIGUNION xa)"
- sorry
-
-lemma BIGUNION_SUBSET: "SUBSET (BIGUNION P) X = (ALL Y. IN Y P --> SUBSET Y X)"
- sorry
-
-lemma FINITE_BIGUNION: "FINITE x & (ALL s. IN s x --> FINITE s) ==> FINITE (BIGUNION x)"
- sorry
-
-definition
- BIGINTER :: "(('a => bool) => bool) => 'a => bool" where
- "BIGINTER == %B. GSPEC (%x. (x, ALL P. IN P B --> IN x P))"
-
-lemma BIGINTER: "BIGINTER B = GSPEC (%x. (x, ALL P. IN P B --> IN x P))"
- sorry
-
-lemma IN_BIGINTER: "IN x (BIGINTER B) = (ALL P. IN P B --> IN x P)"
- sorry
-
-lemma BIGINTER_INSERT: "BIGINTER (INSERT P B) = pred_set.INTER P (BIGINTER B)"
- sorry
-
-lemma BIGINTER_EMPTY: "BIGINTER EMPTY = pred_set.UNIV"
- sorry
-
-lemma BIGINTER_INTER: "BIGINTER (INSERT x (INSERT xa EMPTY)) = pred_set.INTER x xa"
- sorry
-
-lemma BIGINTER_SING: "BIGINTER (INSERT x EMPTY) = x"
- sorry
-
-lemma SUBSET_BIGINTER: "SUBSET X (BIGINTER P) = (ALL x. IN x P --> SUBSET X x)"
- sorry
-
-lemma DISJOINT_BIGINTER: "IN xa xb & DISJOINT xa x
-==> DISJOINT x (BIGINTER xb) & DISJOINT (BIGINTER xb) x"
- sorry
-
-definition
- CROSS :: "('a => bool) => ('b => bool) => 'a * 'b => bool" where
- "CROSS == %P Q. GSPEC (%p. (p, IN (fst p) P & IN (snd p) Q))"
-
-lemma CROSS_DEF: "CROSS P Q = GSPEC (%p. (p, IN (fst p) P & IN (snd p) Q))"
- sorry
-
-lemma IN_CROSS: "IN xb (CROSS x xa) = (IN (fst xb) x & IN (snd xb) xa)"
- sorry
-
-lemma CROSS_EMPTY: "CROSS x EMPTY = EMPTY & CROSS EMPTY x = EMPTY"
- sorry
-
-lemma CROSS_INSERT_LEFT: "CROSS (INSERT xb x) xa =
-pred_set.UNION (CROSS (INSERT xb EMPTY) xa) (CROSS x xa)"
- sorry
-
-lemma CROSS_INSERT_RIGHT: "CROSS x (INSERT xb xa) =
-pred_set.UNION (CROSS x (INSERT xb EMPTY)) (CROSS x xa)"
- sorry
-
-lemma FINITE_CROSS: "FINITE x & FINITE xa ==> FINITE (CROSS x xa)"
- sorry
-
-lemma CROSS_SINGS: "CROSS (INSERT x EMPTY) (INSERT xa EMPTY) = INSERT (x, xa) EMPTY"
- sorry
-
-lemma CARD_SING_CROSS: "FINITE (s::'b => bool) ==> CARD (CROSS (INSERT (x::'a) EMPTY) s) = CARD s"
- sorry
-
-lemma CARD_CROSS: "FINITE x & FINITE xa ==> CARD (CROSS x xa) = CARD x * CARD xa"
- sorry
-
-lemma CROSS_SUBSET: "SUBSET (CROSS xb xc) (CROSS x xa) =
-(xb = EMPTY | xc = EMPTY | SUBSET xb x & SUBSET xc xa)"
- sorry
-
-lemma FINITE_CROSS_EQ: "FINITE (CROSS P Q) = (P = EMPTY | Q = EMPTY | FINITE P & FINITE Q)"
- sorry
-
-definition
- COMPL :: "('a => bool) => 'a => bool" where
- "COMPL == DIFF pred_set.UNIV"
-
-lemma COMPL_DEF: "COMPL P = DIFF pred_set.UNIV P"
- sorry
-
-lemma IN_COMPL: "IN x (COMPL xa) = (~ IN x xa)"
- sorry
-
-lemma COMPL_COMPL: "COMPL (COMPL x) = x"
- sorry
-
-lemma COMPL_CLAUSES: "pred_set.INTER (COMPL x) x = EMPTY &
-pred_set.UNION (COMPL x) x = pred_set.UNIV"
- sorry
-
-lemma COMPL_SPLITS: "pred_set.UNION (pred_set.INTER x xa) (pred_set.INTER (COMPL x) xa) = xa"
- sorry
-
-lemma INTER_UNION_COMPL: "pred_set.INTER x xa = COMPL (pred_set.UNION (COMPL x) (COMPL xa))"
- sorry
-
-lemma COMPL_EMPTY: "COMPL EMPTY = pred_set.UNIV"
- sorry
-
-consts
- count :: "nat => nat => bool"
-
-defs
- count_primdef: "count == %n. GSPEC (%m. (m, m < n))"
-
-lemma count_def: "count n = GSPEC (%m. (m, m < n))"
- sorry
-
-lemma IN_COUNT: "IN m (count n) = (m < n)"
- sorry
-
-lemma COUNT_ZERO: "count 0 = EMPTY"
- sorry
-
-lemma COUNT_SUC: "count (Suc n) = INSERT n (count n)"
- sorry
-
-lemma FINITE_COUNT: "FINITE (count n)"
- sorry
-
-lemma CARD_COUNT: "CARD (count n) = n"
- sorry
-
-definition
- ITSET_tupled :: "('a => 'b => 'b) => ('a => bool) * 'b => 'b" where
- "ITSET_tupled ==
-%f. WFREC
- (SOME R.
- WF R &
- (ALL b s.
- FINITE s & s ~= EMPTY --> R (REST s, f (CHOICE s) b) (s, b)))
- (%ITSET_tupled (v, v1).
- if FINITE v
- then if v = EMPTY then v1
- else ITSET_tupled (REST v, f (CHOICE v) v1)
- else ARB)"
-
-lemma ITSET_tupled_primitive_def: "ITSET_tupled f =
-WFREC
- (SOME R.
- WF R &
- (ALL b s. FINITE s & s ~= EMPTY --> R (REST s, f (CHOICE s) b) (s, b)))
- (%ITSET_tupled (v, v1).
- if FINITE v
- then if v = EMPTY then v1 else ITSET_tupled (REST v, f (CHOICE v) v1)
- else ARB)"
- sorry
-
-definition
- ITSET :: "('a => 'b => 'b) => ('a => bool) => 'b => 'b" where
- "ITSET == %f x x1. ITSET_tupled f (x, x1)"
-
-lemma ITSET_curried_def: "ITSET (f::'a => 'b => 'b) (x::'a => bool) (x1::'b) = ITSET_tupled f (x, x1)"
- sorry
-
-lemma ITSET_IND: "(!!(s::'a => bool) b::'b.
- (FINITE s & s ~= EMPTY
- ==> (P::('a => bool) => 'b => bool) (REST s)
- ((f::'a => 'b => 'b) (CHOICE s) b))
- ==> P s b)
-==> P (v::'a => bool) (x::'b)"
- sorry
-
-lemma ITSET_THM: "FINITE s
-==> ITSET f s b =
- (if s = EMPTY then b else ITSET f (REST s) (f (CHOICE s) b))"
- sorry
-
-lemma ITSET_EMPTY: "ITSET (x::'a => 'b => 'b) EMPTY (xa::'b) = xa"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" operator
-
-definition
- ASSOC :: "('a => 'a => 'a) => bool" where
- "ASSOC == %f. ALL x y z. f x (f y z) = f (f x y) z"
-
-lemma ASSOC_DEF: "ASSOC f = (ALL x y z. f x (f y z) = f (f x y) z)"
- sorry
-
-definition
- COMM :: "('a => 'a => 'b) => bool" where
- "COMM == %f. ALL x y. f x y = f y x"
-
-lemma COMM_DEF: "COMM f = (ALL x y. f x y = f y x)"
- sorry
-
-definition
- FCOMM :: "('a => 'b => 'a) => ('c => 'a => 'a) => bool" where
- "FCOMM == %f g. ALL x y z. g x (f y z) = f (g x y) z"
-
-lemma FCOMM_DEF: "FCOMM f g = (ALL x y z. g x (f y z) = f (g x y) z)"
- sorry
-
-definition
- RIGHT_ID :: "('a => 'b => 'a) => 'b => bool" where
- "RIGHT_ID == %f e. ALL x. f x e = x"
-
-lemma RIGHT_ID_DEF: "RIGHT_ID f e = (ALL x. f x e = x)"
- sorry
-
-definition
- LEFT_ID :: "('a => 'b => 'b) => 'a => bool" where
- "LEFT_ID == %f e. ALL x. f e x = x"
-
-lemma LEFT_ID_DEF: "LEFT_ID f e = (ALL x. f e x = x)"
- sorry
-
-definition
- MONOID :: "('a => 'a => 'a) => 'a => bool" where
- "MONOID == %f e. ASSOC f & RIGHT_ID f e & LEFT_ID f e"
-
-lemma MONOID_DEF: "MONOID f e = (ASSOC f & RIGHT_ID f e & LEFT_ID f e)"
- sorry
-
-lemma ASSOC_CONJ: "ASSOC op &"
- sorry
-
-lemma ASSOC_DISJ: "ASSOC op |"
- sorry
-
-lemma FCOMM_ASSOC: "FCOMM x x = ASSOC x"
- sorry
-
-lemma MONOID_CONJ_T: "MONOID op & True"
- sorry
-
-lemma MONOID_DISJ_F: "MONOID op | False"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" rich_list
-
-consts
- SNOC :: "'a => 'a list => 'a list"
-
-specification (SNOC) SNOC: "(ALL x::'a. SNOC x [] = [x]) &
-(ALL (x::'a) (x'::'a) l::'a list. SNOC x (x' # l) = x' # SNOC x l)"
- sorry
-
-consts
- SCANL :: "('b => 'a => 'b) => 'b => 'a list => 'b list"
-
-specification (SCANL) SCANL: "(ALL (f::'b => 'a => 'b) e::'b. SCANL f e [] = [e]) &
-(ALL (f::'b => 'a => 'b) (e::'b) (x::'a) l::'a list.
- SCANL f e (x # l) = e # SCANL f (f e x) l)"
- sorry
-
-consts
- SCANR :: "('a => 'b => 'b) => 'b => 'a list => 'b list"
-
-specification (SCANR) SCANR: "(ALL (f::'a => 'b => 'b) e::'b. SCANR f e [] = [e]) &
-(ALL (f::'a => 'b => 'b) (e::'b) (x::'a) l::'a list.
- SCANR f e (x # l) = f x (hd (SCANR f e l)) # SCANR f e l)"
- sorry
-
-lemma IS_EL_DEF: "List.member l x = list_ex (op = x) l"
- sorry
-
-definition
- AND_EL :: "bool list => bool" where
- "AND_EL == list_all I"
-
-lemma AND_EL_DEF: "AND_EL = list_all I"
- sorry
-
-definition
- OR_EL :: "bool list => bool" where
- "OR_EL == list_ex I"
-
-lemma OR_EL_DEF: "OR_EL = list_ex I"
- sorry
-
-consts
- FIRSTN :: "nat => 'a list => 'a list"
-
-specification (FIRSTN) FIRSTN: "(ALL l::'a list. FIRSTN (0::nat) l = []) &
-(ALL (n::nat) (x::'a) l::'a list. FIRSTN (Suc n) (x # l) = x # FIRSTN n l)"
- sorry
-
-consts
- BUTFIRSTN :: "nat => 'a list => 'a list"
-
-specification (BUTFIRSTN) BUTFIRSTN: "(ALL l::'a list. BUTFIRSTN (0::nat) l = l) &
-(ALL (n::nat) (x::'a) l::'a list. BUTFIRSTN (Suc n) (x # l) = BUTFIRSTN n l)"
- sorry
-
-consts
- SEG :: "nat => nat => 'a list => 'a list"
-
-specification (SEG) SEG: "(ALL (k::nat) l::'a list. SEG (0::nat) k l = []) &
-(ALL (m::nat) (x::'a) l::'a list.
- SEG (Suc m) (0::nat) (x # l) = x # SEG m (0::nat) l) &
-(ALL (m::nat) (k::nat) (x::'a) l::'a list.
- SEG (Suc m) (Suc k) (x # l) = SEG (Suc m) k l)"
- sorry
-
-lemma LAST: "last (SNOC x l) = x"
- sorry
-
-lemma BUTLAST: "butlast (SNOC x l) = l"
- sorry
-
-consts
- LASTN :: "nat => 'a list => 'a list"
-
-specification (LASTN) LASTN: "(ALL l::'a list. LASTN (0::nat) l = []) &
-(ALL (n::nat) (x::'a) l::'a list.
- LASTN (Suc n) (SNOC x l) = SNOC x (LASTN n l))"
- sorry
-
-consts
- BUTLASTN :: "nat => 'a list => 'a list"
-
-specification (BUTLASTN) BUTLASTN: "(ALL l::'a list. BUTLASTN (0::nat) l = l) &
-(ALL (n::nat) (x::'a) l::'a list.
- BUTLASTN (Suc n) (SNOC x l) = BUTLASTN n l)"
- sorry
-
-lemma EL: "(ALL x::'a list. EL (0::nat) x = hd x) &
-(ALL (x::nat) xa::'a list. EL (Suc x) xa = EL x (tl xa))"
- sorry
-
-consts
- ELL :: "nat => 'a list => 'a"
-
-specification (ELL) ELL: "(ALL l::'a list. ELL (0::nat) l = last l) &
-(ALL (n::nat) l::'a list. ELL (Suc n) l = ELL n (butlast l))"
- sorry
-
-consts
- IS_PREFIX :: "'a list => 'a list => bool"
-
-specification (IS_PREFIX) IS_PREFIX: "(ALL l::'a list. IS_PREFIX l [] = True) &
-(ALL (x::'a) l::'a list. IS_PREFIX [] (x # l) = False) &
-(ALL (x1::'a) (l1::'a list) (x2::'a) l2::'a list.
- IS_PREFIX (x1 # l1) (x2 # l2) = (x1 = x2 & IS_PREFIX l1 l2))"
- sorry
-
-lemma SNOC_APPEND: "SNOC x l = l @ [x]"
- sorry
-
-lemma REVERSE: "rev [] = [] & (ALL (x::'a) xa::'a list. rev (x # xa) = SNOC x (rev xa))"
- sorry
-
-lemma REVERSE_SNOC: "rev (SNOC x l) = x # rev l"
- sorry
-
-lemma SNOC_Axiom: "EX x. x [] = e & (ALL xa l. x (SNOC xa l) = f xa l (x l))"
- sorry
-
-consts
- IS_SUFFIX :: "'a list => 'a list => bool"
-
-specification (IS_SUFFIX) IS_SUFFIX: "(ALL l::'a list. IS_SUFFIX l [] = True) &
-(ALL (x::'a) l::'a list. IS_SUFFIX [] (SNOC x l) = False) &
-(ALL (x1::'a) (l1::'a list) (x2::'a) l2::'a list.
- IS_SUFFIX (SNOC x1 l1) (SNOC x2 l2) = (x1 = x2 & IS_SUFFIX l1 l2))"
- sorry
-
-consts
- IS_SUBLIST :: "'a list => 'a list => bool"
-
-specification (IS_SUBLIST) IS_SUBLIST: "(ALL l::'a list. IS_SUBLIST l [] = True) &
-(ALL (x::'a) l::'a list. IS_SUBLIST [] (x # l) = False) &
-(ALL (x1::'a) (l1::'a list) (x2::'a) l2::'a list.
- IS_SUBLIST (x1 # l1) (x2 # l2) =
- (x1 = x2 & IS_PREFIX l1 l2 | IS_SUBLIST l1 (x2 # l2)))"
- sorry
-
-consts
- SPLITP :: "('a => bool) => 'a list => 'a list * 'a list"
-
-specification (SPLITP) SPLITP: "(ALL P::'a => bool. SPLITP P [] = ([], [])) &
-(ALL (P::'a => bool) (x::'a) l::'a list.
- SPLITP P (x # l) =
- (if P x then ([], x # l) else (x # fst (SPLITP P l), snd (SPLITP P l))))"
- sorry
-
-definition
- PREFIX :: "('a => bool) => 'a list => 'a list" where
- "PREFIX == %P l. fst (SPLITP (Not o P) l)"
-
-lemma PREFIX_DEF: "PREFIX P l = fst (SPLITP (Not o P) l)"
- sorry
-
-definition
- SUFFIX :: "('a => bool) => 'a list => 'a list" where
- "SUFFIX == %P. foldl (%l' x. if P x then SNOC x l' else []) []"
-
-lemma SUFFIX_DEF: "SUFFIX P l = foldl (%l' x. if P x then SNOC x l' else []) [] l"
- sorry
-
-definition
- UNZIP_FST :: "('a * 'b) list => 'a list" where
- "UNZIP_FST == %l. fst (unzip l)"
-
-lemma UNZIP_FST_DEF: "UNZIP_FST l = fst (unzip l)"
- sorry
-
-definition
- UNZIP_SND :: "('a * 'b) list => 'b list" where
- "UNZIP_SND == %l. snd (unzip l)"
-
-lemma UNZIP_SND_DEF: "UNZIP_SND (l::('a * 'b) list) = snd (unzip l)"
- sorry
-
-consts
- GENLIST :: "(nat => 'a) => nat => 'a list"
-
-specification (GENLIST) GENLIST: "(ALL f::nat => 'a. GENLIST f (0::nat) = []) &
-(ALL (f::nat => 'a) n::nat. GENLIST f (Suc n) = SNOC (f n) (GENLIST f n))"
- sorry
-
-consts
- REPLICATE :: "nat => 'a => 'a list"
-
-specification (REPLICATE) REPLICATE: "(ALL x::'a. REPLICATE (0::nat) x = []) &
-(ALL (n::nat) x::'a. REPLICATE (Suc n) x = x # REPLICATE n x)"
- sorry
-
-lemma LENGTH_MAP2: "length l1 = length l2
-==> length (map2 f l1 l2) = length l1 & length (map2 f l1 l2) = length l2"
- sorry
-
-lemma LENGTH_EQ: "x = y ==> length x = length y"
- sorry
-
-lemma LENGTH_NOT_NULL: "(0 < length l) = (~ List.null l)"
- sorry
-
-lemma SNOC_INDUCT: "P [] & (ALL l. P l --> (ALL x. P (SNOC x l))) ==> P x"
- sorry
-
-lemma SNOC_CASES: "x' = [] | (EX x l. x' = SNOC x l)"
- sorry
-
-lemma LENGTH_SNOC: "length (SNOC x l) = Suc (length l)"
- sorry
-
-lemma NOT_NIL_SNOC: "[] ~= SNOC x xa"
- sorry
-
-lemma NOT_SNOC_NIL: "SNOC x xa ~= []"
- sorry
-
-lemma SNOC_11: "(SNOC x l = SNOC x' l') = (x = x' & l = l')"
- sorry
-
-lemma SNOC_EQ_LENGTH_EQ: "SNOC x1 l1 = SNOC x2 l2 ==> length l1 = length l2"
- sorry
-
-lemma SNOC_REVERSE_CONS: "SNOC x xa = rev (x # rev xa)"
- sorry
-
-lemma MAP_SNOC: "map (x::'a => 'b) (SNOC (xa::'a) (xb::'a list)) = SNOC (x xa) (map x xb)"
- sorry
-
-lemma FOLDR_SNOC: "foldr (f::'a => 'b => 'b) (SNOC (x::'a) (l::'a list)) (e::'b) =
-foldr f l (f x e)"
- sorry
-
-lemma FOLDL_SNOC: "foldl (f::'b => 'a => 'b) (e::'b) (SNOC (x::'a) (l::'a list)) =
-f (foldl f e l) x"
- sorry
-
-lemma FOLDR_FOLDL: "MONOID f e ==> foldr f l e = foldl f e l"
- sorry
-
-lemma LENGTH_FOLDR: "length l = foldr (%x. Suc) l 0"
- sorry
-
-lemma LENGTH_FOLDL: "length l = foldl (%l' x. Suc l') 0 l"
- sorry
-
-lemma MAP_FOLDR: "map (f::'a => 'b) (l::'a list) = foldr (%x::'a. op # (f x)) l []"
- sorry
-
-lemma MAP_FOLDL: "map (f::'a => 'b) (l::'a list) =
-foldl (%(l'::'b list) x::'a. SNOC (f x) l') [] l"
- sorry
-
-lemma FILTER_FOLDR: "filter P l = foldr (%x l'. if P x then x # l' else l') l []"
- sorry
-
-lemma FILTER_SNOC: "filter P (SNOC x l) = (if P x then SNOC x (filter P l) else filter P l)"
- sorry
-
-lemma FILTER_FOLDL: "filter P l = foldl (%l' x. if P x then SNOC x l' else l') [] l"
- sorry
-
-lemma FILTER_COMM: "filter f1 (filter f2 l) = filter f2 (filter f1 l)"
- sorry
-
-lemma FILTER_IDEM: "filter f (filter f l) = filter f l"
- sorry
-
-lemma LENGTH_SEG: "n + k <= length l ==> length (SEG n k l) = n"
- sorry
-
-lemma APPEND_NIL: "(ALL l::'a list. l @ [] = l) & (ALL x::'a list. [] @ x = x)"
- sorry
-
-lemma APPEND_SNOC: "l1 @ SNOC x l2 = SNOC x (l1 @ l2)"
- sorry
-
-lemma APPEND_FOLDR: "l1 @ l2 = foldr op # l1 l2"
- sorry
-
-lemma APPEND_FOLDL: "l1 @ l2 = foldl (%l' x. SNOC x l') l1 l2"
- sorry
-
-lemma CONS_APPEND: "x # l = [x] @ l"
- sorry
-
-lemma ASSOC_APPEND: "ASSOC op @"
- sorry
-
-lemma MONOID_APPEND_NIL: "MONOID op @ []"
- sorry
-
-lemma APPEND_LENGTH_EQ: "[| length l1 = length l1'; length l2 = length l2' |]
-==> (l1 @ l2 = l1' @ l2') = (l1 = l1' & l2 = l2')"
- sorry
-
-lemma FLAT_SNOC: "concat (SNOC x l) = concat l @ x"
- sorry
-
-lemma FLAT_FOLDR: "concat l = foldr op @ l []"
- sorry
-
-lemma LENGTH_FLAT: "length (concat l) = Compatibility.sum (map length l)"
- sorry
-
-lemma REVERSE_FOLDR: "rev l = foldr SNOC l []"
- sorry
-
-lemma ALL_EL_SNOC: "list_all P (SNOC x l) = (list_all P l & P x)"
- sorry
-
-lemma ALL_EL_MAP: "list_all (P::'b => bool) (map (f::'a => 'b) (l::'a list)) =
-list_all (P o f) l"
- sorry
-
-lemma SOME_EL_SNOC: "list_ex P (SNOC x l) = (P x | list_ex P l)"
- sorry
-
-lemma IS_EL_SNOC: "List.member (SNOC x l) y = (y = x | List.member l y)"
- sorry
-
-lemma SUM_SNOC: "Compatibility.sum (SNOC x l) = Compatibility.sum l + x"
- sorry
-
-lemma SUM_FOLDL: "Compatibility.sum l = foldl op + 0 l"
- sorry
-
-lemma IS_PREFIX_APPEND: "IS_PREFIX l1 l2 = (EX l. l1 = l2 @ l)"
- sorry
-
-lemma IS_SUFFIX_APPEND: "IS_SUFFIX l1 l2 = (EX l. l1 = l @ l2)"
- sorry
-
-lemma IS_SUBLIST_APPEND: "IS_SUBLIST l1 l2 = (EX l l'. l1 = l @ l2 @ l')"
- sorry
-
-lemma IS_PREFIX_IS_SUBLIST: "IS_PREFIX l1 l2 ==> IS_SUBLIST l1 l2"
- sorry
-
-lemma IS_SUFFIX_IS_SUBLIST: "IS_SUFFIX l1 l2 ==> IS_SUBLIST l1 l2"
- sorry
-
-lemma IS_PREFIX_REVERSE: "IS_PREFIX (rev l1) (rev l2) = IS_SUFFIX l1 l2"
- sorry
-
-lemma IS_SUFFIX_REVERSE: "IS_SUFFIX (rev l1) (rev l2) = IS_PREFIX l1 l2"
- sorry
-
-lemma IS_SUBLIST_REVERSE: "IS_SUBLIST (rev l1) (rev l2) = IS_SUBLIST l1 l2"
- sorry
-
-lemma PREFIX_FOLDR: "PREFIX P x = foldr (%x l'. if P x then x # l' else []) x []"
- sorry
-
-lemma PREFIX: "(ALL x::'a => bool. PREFIX x [] = []) &
-(ALL (x::'a => bool) (xa::'a) xb::'a list.
- PREFIX x (xa # xb) = (if x xa then xa # PREFIX x xb else []))"
- sorry
-
-lemma IS_PREFIX_PREFIX: "IS_PREFIX l (PREFIX P l)"
- sorry
-
-lemma LENGTH_SCANL: "length (SCANL (f::'b => 'a => 'b) (e::'b) (l::'a list)) = Suc (length l)"
- sorry
-
-lemma LENGTH_SCANR: "length (SCANR (f::'a => 'b => 'b) (e::'b) (l::'a list)) = Suc (length l)"
- sorry
-
-lemma COMM_MONOID_FOLDL: "[| COMM x; MONOID x xa |] ==> foldl x e l = x e (foldl x xa l)"
- sorry
-
-lemma COMM_MONOID_FOLDR: "[| COMM x; MONOID x xa |] ==> foldr x l e = x e (foldr x l xa)"
- sorry
-
-lemma FCOMM_FOLDR_APPEND: "[| FCOMM x xa; LEFT_ID x xb |]
-==> foldr xa (l1 @ l2) xb = x (foldr xa l1 xb) (foldr xa l2 xb)"
- sorry
-
-lemma FCOMM_FOLDL_APPEND: "[| FCOMM x xa; RIGHT_ID xa xb |]
-==> foldl x xb (l1 @ l2) = xa (foldl x xb l1) (foldl x xb l2)"
- sorry
-
-lemma FOLDL_SINGLE: "foldl x xa [xb] = x xa xb"
- sorry
-
-lemma FOLDR_SINGLE: "foldr (x::'a => 'b => 'b) [xb::'a] (xa::'b) = x xb xa"
- sorry
-
-lemma FOLDR_CONS_NIL: "foldr op # l [] = l"
- sorry
-
-lemma FOLDL_SNOC_NIL: "foldl (%xs x. SNOC x xs) [] l = l"
- sorry
-
-lemma FOLDR_REVERSE: "foldr (x::'a => 'b => 'b) (rev (xb::'a list)) (xa::'b) =
-foldl (%(xa::'b) y::'a. x y xa) xa xb"
- sorry
-
-lemma FOLDL_REVERSE: "foldl x xa (rev xb) = foldr (%xa y. x y xa) xb xa"
- sorry
-
-lemma FOLDR_MAP: "foldr (f::'a => 'a => 'a) (map (g::'b => 'a) (l::'b list)) (e::'a) =
-foldr (%x::'b. f (g x)) l e"
- sorry
-
-lemma ALL_EL_FOLDR: "list_all P l = foldr (%x. op & (P x)) l True"
- sorry
-
-lemma ALL_EL_FOLDL: "list_all P l = foldl (%l' x. l' & P x) True l"
- sorry
-
-lemma SOME_EL_FOLDR: "list_ex P l = foldr (%x. op | (P x)) l False"
- sorry
-
-lemma SOME_EL_FOLDL: "list_ex P l = foldl (%l' x. l' | P x) False l"
- sorry
-
-lemma ALL_EL_FOLDR_MAP: "list_all x xa = foldr op & (map x xa) True"
- sorry
-
-lemma ALL_EL_FOLDL_MAP: "list_all x xa = foldl op & True (map x xa)"
- sorry
-
-lemma SOME_EL_FOLDR_MAP: "list_ex x xa = foldr op | (map x xa) False"
- sorry
-
-lemma SOME_EL_FOLDL_MAP: "list_ex x xa = foldl op | False (map x xa)"
- sorry
-
-lemma FOLDR_FILTER: "foldr (f::'a => 'a => 'a) (filter (P::'a => bool) (l::'a list)) (e::'a) =
-foldr (%(x::'a) y::'a. if P x then f x y else y) l e"
- sorry
-
-lemma FOLDL_FILTER: "foldl (f::'a => 'a => 'a) (e::'a) (filter (P::'a => bool) (l::'a list)) =
-foldl (%(x::'a) y::'a. if P y then f x y else x) e l"
- sorry
-
-lemma ASSOC_FOLDR_FLAT: "[| ASSOC f; LEFT_ID f e |]
-==> foldr f (concat l) e = foldr f (map (FOLDR f e) l) e"
- sorry
-
-lemma ASSOC_FOLDL_FLAT: "[| ASSOC f; RIGHT_ID f e |]
-==> foldl f e (concat l) = foldl f e (map (foldl f e) l)"
- sorry
-
-lemma SOME_EL_MAP: "list_ex (P::'b => bool) (map (f::'a => 'b) (l::'a list)) = list_ex (P o f) l"
- sorry
-
-lemma SOME_EL_DISJ: "list_ex (%x. P x | Q x) l = (list_ex P l | list_ex Q l)"
- sorry
-
-lemma IS_EL_FOLDR: "List.member xa x = foldr (%xa. op | (x = xa)) xa False"
- sorry
-
-lemma IS_EL_FOLDL: "List.member xa x = foldl (%l' xa. l' | x = xa) False xa"
- sorry
-
-lemma NULL_FOLDR: "List.null l = foldr (%x l'. False) l True"
- sorry
-
-lemma NULL_FOLDL: "List.null l = foldl (%x l'. False) True l"
- sorry
-
-lemma SEG_LENGTH_ID: "SEG (length l) 0 l = l"
- sorry
-
-lemma SEG_SUC_CONS: "SEG m (Suc n) (x # l) = SEG m n l"
- sorry
-
-lemma SEG_0_SNOC: "m <= length l ==> SEG m 0 (SNOC x l) = SEG m 0 l"
- sorry
-
-lemma BUTLASTN_SEG: "n <= length l ==> BUTLASTN n l = SEG (length l - n) 0 l"
- sorry
-
-lemma LASTN_CONS: "n <= length l ==> LASTN n (x # l) = LASTN n l"
- sorry
-
-lemma LENGTH_LASTN: "n <= length l ==> length (LASTN n l) = n"
- sorry
-
-lemma LASTN_LENGTH_ID: "LASTN (length l) l = l"
- sorry
-
-lemma LASTN_LASTN: "[| m <= length l; n <= m |] ==> LASTN n (LASTN m l) = LASTN n l"
- sorry
-
-lemma FIRSTN_LENGTH_ID: "FIRSTN (length l) l = l"
- sorry
-
-lemma FIRSTN_SNOC: "n <= length l ==> FIRSTN n (SNOC x l) = FIRSTN n l"
- sorry
-
-lemma BUTLASTN_LENGTH_NIL: "BUTLASTN (length l) l = []"
- sorry
-
-lemma BUTLASTN_SUC_BUTLAST: "n < length l ==> BUTLASTN (Suc n) l = BUTLASTN n (butlast l)"
- sorry
-
-lemma BUTLASTN_BUTLAST: "n < length l ==> BUTLASTN n (butlast l) = butlast (BUTLASTN n l)"
- sorry
-
-lemma LENGTH_BUTLASTN: "n <= length l ==> length (BUTLASTN n l) = length l - n"
- sorry
-
-lemma BUTLASTN_BUTLASTN: "n + m <= length l ==> BUTLASTN n (BUTLASTN m l) = BUTLASTN (n + m) l"
- sorry
-
-lemma APPEND_BUTLASTN_LASTN: "n <= length l ==> BUTLASTN n l @ LASTN n l = l"
- sorry
-
-lemma APPEND_FIRSTN_LASTN: "m + n = length l ==> FIRSTN n l @ LASTN m l = l"
- sorry
-
-lemma BUTLASTN_APPEND2: "n <= length l2 ==> BUTLASTN n (l1 @ l2) = l1 @ BUTLASTN n l2"
- sorry
-
-lemma BUTLASTN_LENGTH_APPEND: "BUTLASTN (length l2) (l1 @ l2) = l1"
- sorry
-
-lemma LASTN_LENGTH_APPEND: "LASTN (length l2) (l1 @ l2) = l2"
- sorry
-
-lemma BUTLASTN_CONS: "n <= length l ==> BUTLASTN n (x # l) = x # BUTLASTN n l"
- sorry
-
-lemma BUTLASTN_LENGTH_CONS: "BUTLASTN (length l) (x # l) = [x]"
- sorry
-
-lemma LAST_LASTN_LAST: "[| n <= length l; 0 < n |] ==> last (LASTN n l) = last l"
- sorry
-
-lemma BUTLASTN_LASTN_NIL: "n <= length l ==> BUTLASTN n (LASTN n l) = []"
- sorry
-
-lemma LASTN_BUTLASTN: "n + m <= length l ==> LASTN n (BUTLASTN m l) = BUTLASTN m (LASTN (n + m) l)"
- sorry
-
-lemma BUTLASTN_LASTN: "m <= n & n <= length l
-==> BUTLASTN m (LASTN n l) = LASTN (n - m) (BUTLASTN m l)"
- sorry
-
-lemma LASTN_1: "l ~= [] ==> LASTN 1 l = [last l]"
- sorry
-
-lemma BUTLASTN_1: "l ~= [] ==> BUTLASTN 1 l = butlast l"
- sorry
-
-lemma BUTLASTN_APPEND1: "length l2 <= n ==> BUTLASTN n (l1 @ l2) = BUTLASTN (n - length l2) l1"
- sorry
-
-lemma LASTN_APPEND2: "n <= length l2 ==> LASTN n (l1 @ l2) = LASTN n l2"
- sorry
-
-lemma LASTN_APPEND1: "length l2 <= n ==> LASTN n (l1 @ l2) = LASTN (n - length l2) l1 @ l2"
- sorry
-
-lemma LASTN_MAP: "n <= length l ==> LASTN n (map f l) = map f (LASTN n l)"
- sorry
-
-lemma BUTLASTN_MAP: "n <= length l ==> BUTLASTN n (map f l) = map f (BUTLASTN n l)"
- sorry
-
-lemma ALL_EL_LASTN: "[| list_all P l; m <= length l |] ==> list_all P (LASTN m l)"
- sorry
-
-lemma ALL_EL_BUTLASTN: "[| list_all P l; m <= length l |] ==> list_all P (BUTLASTN m l)"
- sorry
-
-lemma LENGTH_FIRSTN: "n <= length l ==> length (FIRSTN n l) = n"
- sorry
-
-lemma FIRSTN_FIRSTN: "[| m <= length l; n <= m |] ==> FIRSTN n (FIRSTN m l) = FIRSTN n l"
- sorry
-
-lemma LENGTH_BUTFIRSTN: "n <= length l ==> length (BUTFIRSTN n l) = length l - n"
- sorry
-
-lemma BUTFIRSTN_LENGTH_NIL: "BUTFIRSTN (length l) l = []"
- sorry
-
-lemma BUTFIRSTN_APPEND1: "n <= length l1 ==> BUTFIRSTN n (l1 @ l2) = BUTFIRSTN n l1 @ l2"
- sorry
-
-lemma BUTFIRSTN_APPEND2: "length l1 <= n ==> BUTFIRSTN n (l1 @ l2) = BUTFIRSTN (n - length l1) l2"
- sorry
-
-lemma BUTFIRSTN_BUTFIRSTN: "n + m <= length l ==> BUTFIRSTN n (BUTFIRSTN m l) = BUTFIRSTN (n + m) l"
- sorry
-
-lemma APPEND_FIRSTN_BUTFIRSTN: "n <= length l ==> FIRSTN n l @ BUTFIRSTN n l = l"
- sorry
-
-lemma LASTN_SEG: "n <= length l ==> LASTN n l = SEG n (length l - n) l"
- sorry
-
-lemma FIRSTN_SEG: "n <= length l ==> FIRSTN n l = SEG n 0 l"
- sorry
-
-lemma BUTFIRSTN_SEG: "n <= length l ==> BUTFIRSTN n l = SEG (length l - n) n l"
- sorry
-
-lemma BUTFIRSTN_SNOC: "n <= length l ==> BUTFIRSTN n (SNOC x l) = SNOC x (BUTFIRSTN n l)"
- sorry
-
-lemma APPEND_BUTLASTN_BUTFIRSTN: "m + n = length l ==> BUTLASTN m l @ BUTFIRSTN n l = l"
- sorry
-
-lemma SEG_SEG: "n1 + m1 <= length l & n2 + m2 <= n1
-==> SEG n2 m2 (SEG n1 m1 l) = SEG n2 (m1 + m2) l"
- sorry
-
-lemma SEG_APPEND1: "n + m <= length l1 ==> SEG n m (l1 @ l2) = SEG n m l1"
- sorry
-
-lemma SEG_APPEND2: "length l1 <= m & n <= length l2
-==> SEG n m (l1 @ l2) = SEG n (m - length l1) l2"
- sorry
-
-lemma SEG_FIRSTN_BUTFISTN: "n + m <= length l ==> SEG n m l = FIRSTN n (BUTFIRSTN m l)"
- sorry
-
-lemma SEG_APPEND: "m < length l1 & length l1 <= n + m & n + m <= length l1 + length l2
-==> SEG n m (l1 @ l2) =
- SEG (length l1 - m) m l1 @ SEG (n + m - length l1) 0 l2"
- sorry
-
-lemma SEG_LENGTH_SNOC: "SEG 1 (length x) (SNOC xa x) = [xa]"
- sorry
-
-lemma SEG_SNOC: "n + m <= length l ==> SEG n m (SNOC x l) = SEG n m l"
- sorry
-
-lemma ELL_SEG: "n < length l ==> ELL n l = hd (SEG 1 (PRE (length l - n)) l)"
- sorry
-
-lemma SNOC_FOLDR: "SNOC x l = foldr op # l [x]"
- sorry
-
-lemma IS_EL_FOLDR_MAP: "List.member xa x = foldr op | (map (op = x) xa) False"
- sorry
-
-lemma IS_EL_FOLDL_MAP: "List.member xa x = foldl op | False (map (op = x) xa)"
- sorry
-
-lemma FILTER_FILTER: "filter P (filter Q l) = [x<-l. P x & Q x]"
- sorry
-
-lemma FCOMM_FOLDR_FLAT: "[| FCOMM g f; LEFT_ID g e |]
-==> foldr f (concat l) e = foldr g (map (FOLDR f e) l) e"
- sorry
-
-lemma FCOMM_FOLDL_FLAT: "[| FCOMM f g; RIGHT_ID g e |]
-==> foldl f e (concat l) = foldl g e (map (foldl f e) l)"
- sorry
-
-lemma FOLDR_MAP_REVERSE: "(!!(a::'a) (b::'a) c::'a. (f::'a => 'a => 'a) a (f b c) = f b (f a c))
-==> foldr f (map (g::'b => 'a) (rev (l::'b list))) (e::'a) =
- foldr f (map g l) e"
- sorry
-
-lemma FOLDR_FILTER_REVERSE: "(!!(a::'a) (b::'a) c::'a. (f::'a => 'a => 'a) a (f b c) = f b (f a c))
-==> foldr f (filter (P::'a => bool) (rev (l::'a list))) (e::'a) =
- foldr f (filter P l) e"
- sorry
-
-lemma COMM_ASSOC_FOLDR_REVERSE: "[| COMM f; ASSOC f |] ==> foldr f (rev l) e = foldr f l e"
- sorry
-
-lemma COMM_ASSOC_FOLDL_REVERSE: "[| COMM f; ASSOC f |] ==> foldl f e (rev l) = foldl f e l"
- sorry
-
-lemma ELL_LAST: "~ List.null l ==> ELL 0 l = last l"
- sorry
-
-lemma ELL_0_SNOC: "ELL 0 (SNOC x l) = x"
- sorry
-
-lemma ELL_SNOC: "0 < n ==> ELL n (SNOC x l) = ELL (PRE n) l"
- sorry
-
-lemma ELL_SUC_SNOC: "ELL (Suc n) (SNOC x xa) = ELL n xa"
- sorry
-
-lemma ELL_CONS: "n < length l ==> ELL n (x # l) = ELL n l"
- sorry
-
-lemma ELL_LENGTH_CONS: "ELL (length l) (x # l) = x"
- sorry
-
-lemma ELL_LENGTH_SNOC: "ELL (length l) (SNOC x l) = (if List.null l then x else hd l)"
- sorry
-
-lemma ELL_APPEND2: "n < length l2 ==> ELL n (l1 @ l2) = ELL n l2"
- sorry
-
-lemma ELL_APPEND1: "length l2 <= n ==> ELL n (l1 @ l2) = ELL (n - length l2) l1"
- sorry
-
-lemma ELL_PRE_LENGTH: "l ~= [] ==> ELL (PRE (length l)) l = hd l"
- sorry
-
-lemma EL_LENGTH_SNOC: "EL (length l) (SNOC x l) = x"
- sorry
-
-lemma EL_PRE_LENGTH: "l ~= [] ==> EL (PRE (length l)) l = last l"
- sorry
-
-lemma EL_SNOC: "n < length l ==> EL n (SNOC x l) = EL n l"
- sorry
-
-lemma EL_ELL: "n < length l ==> EL n l = ELL (PRE (length l - n)) l"
- sorry
-
-lemma EL_LENGTH_APPEND: "~ List.null l2 ==> EL (length l1) (l1 @ l2) = hd l2"
- sorry
-
-lemma ELL_EL: "n < length l ==> ELL n l = EL (PRE (length l - n)) l"
- sorry
-
-lemma ELL_MAP: "n < length l ==> ELL n (map f l) = f (ELL n l)"
- sorry
-
-lemma LENGTH_BUTLAST: "l ~= [] ==> length (butlast l) = PRE (length l)"
- sorry
-
-lemma BUTFIRSTN_LENGTH_APPEND: "BUTFIRSTN (length l1) (l1 @ l2) = l2"
- sorry
-
-lemma FIRSTN_APPEND1: "n <= length l1 ==> FIRSTN n (l1 @ l2) = FIRSTN n l1"
- sorry
-
-lemma FIRSTN_APPEND2: "length l1 <= n ==> FIRSTN n (l1 @ l2) = l1 @ FIRSTN (n - length l1) l2"
- sorry
-
-lemma FIRSTN_LENGTH_APPEND: "FIRSTN (length l1) (l1 @ l2) = l1"
- sorry
-
-lemma REVERSE_FLAT: "rev (concat l) = concat (rev (map rev l))"
- sorry
-
-lemma MAP_FILTER: "(!!x. P (f x) = P x) ==> map f (filter P l) = filter P (map f l)"
- sorry
-
-lemma FLAT_REVERSE: "concat (rev l) = rev (concat (map rev l))"
- sorry
-
-lemma FLAT_FLAT: "concat (concat l) = concat (map concat l)"
- sorry
-
-lemma ALL_EL_SEG: "[| list_all P l; m + k <= length l |] ==> list_all P (SEG m k l)"
- sorry
-
-lemma ALL_EL_FIRSTN: "[| list_all P l; m <= length l |] ==> list_all P (FIRSTN m l)"
- sorry
-
-lemma ALL_EL_BUTFIRSTN: "[| list_all P l; m <= length l |] ==> list_all P (BUTFIRSTN m l)"
- sorry
-
-lemma SOME_EL_SEG: "[| m + k <= length l; list_ex P (SEG m k l) |] ==> list_ex P l"
- sorry
-
-lemma SOME_EL_FIRSTN: "[| m <= length l; list_ex P (FIRSTN m l) |] ==> list_ex P l"
- sorry
-
-lemma SOME_EL_BUTFIRSTN: "[| m <= length l; list_ex P (BUTFIRSTN m l) |] ==> list_ex P l"
- sorry
-
-lemma SOME_EL_LASTN: "[| m <= length l; list_ex P (LASTN m l) |] ==> list_ex P l"
- sorry
-
-lemma SOME_EL_BUTLASTN: "[| m <= length l; list_ex P (BUTLASTN m l) |] ==> list_ex P l"
- sorry
-
-lemma IS_EL_REVERSE: "List.member (rev l) x = List.member l x"
- sorry
-
-lemma IS_EL_FILTER: "P x ==> List.member (filter P l) x = List.member l x"
- sorry
-
-lemma IS_EL_SEG: "[| n + m <= length l; List.member (SEG n m l) x |] ==> List.member l x"
- sorry
-
-lemma IS_EL_SOME_EL: "List.member l x = list_ex (op = x) l"
- sorry
-
-lemma IS_EL_FIRSTN: "[| x <= length xa; List.member (FIRSTN x xa) xb |] ==> List.member xa xb"
- sorry
-
-lemma IS_EL_BUTFIRSTN: "[| x <= length xa; List.member (BUTFIRSTN x xa) xb |] ==> List.member xa xb"
- sorry
-
-lemma IS_EL_BUTLASTN: "[| x <= length xa; List.member (BUTLASTN x xa) xb |] ==> List.member xa xb"
- sorry
-
-lemma IS_EL_LASTN: "[| x <= length xa; List.member (LASTN x xa) xb |] ==> List.member xa xb"
- sorry
-
-lemma ZIP_SNOC: "length l1 = length l2
-==> zip (SNOC x1 l1) (SNOC x2 l2) = SNOC (x1, x2) (zip l1 l2)"
- sorry
-
-lemma UNZIP_SNOC: "unzip (SNOC x l) =
-(SNOC (fst x) (fst (unzip l)), SNOC (snd x) (snd (unzip l)))"
- sorry
-
-lemma LENGTH_UNZIP_FST: "length (UNZIP_FST x) = length x"
- sorry
-
-lemma LENGTH_UNZIP_SND: "length (UNZIP_SND (x::('a * 'b) list)) = length x"
- sorry
-
-lemma SUM_APPEND: "Compatibility.sum (l1 @ l2) = Compatibility.sum l1 + Compatibility.sum l2"
- sorry
-
-lemma SUM_REVERSE: "Compatibility.sum (rev l) = Compatibility.sum l"
- sorry
-
-lemma SUM_FLAT: "Compatibility.sum (concat l) = Compatibility.sum (map Compatibility.sum l)"
- sorry
-
-lemma EL_APPEND1: "n < length l1 ==> EL n (l1 @ l2) = EL n l1"
- sorry
-
-lemma EL_APPEND2: "length l1 <= n ==> EL n (l1 @ l2) = EL (n - length l1) l2"
- sorry
-
-lemma EL_MAP: "n < length l ==> EL n (map f l) = f (EL n l)"
- sorry
-
-lemma EL_CONS: "0 < n ==> EL n (x # l) = EL (PRE n) l"
- sorry
-
-lemma EL_SEG: "n < length l ==> EL n l = hd (SEG 1 n l)"
- sorry
-
-lemma EL_IS_EL: "n < length l ==> List.member l (EL n l)"
- sorry
-
-lemma TL_SNOC: "tl (SNOC x l) = (if List.null l then [] else SNOC x (tl l))"
- sorry
-
-lemma EL_REVERSE: "n < length l ==> EL n (rev l) = EL (PRE (length l - n)) l"
- sorry
-
-lemma EL_REVERSE_ELL: "n < length l ==> EL n (rev l) = ELL n l"
- sorry
-
-lemma ELL_LENGTH_APPEND: "~ List.null l1 ==> ELL (length l2) (l1 @ l2) = last l1"
- sorry
-
-lemma ELL_IS_EL: "n < length l ==> List.member l (ELL n l)"
- sorry
-
-lemma ELL_REVERSE: "n < length l ==> ELL n (rev l) = ELL (PRE (length l - n)) l"
- sorry
-
-lemma ELL_REVERSE_EL: "n < length l ==> ELL n (rev l) = EL n l"
- sorry
-
-lemma FIRSTN_BUTLASTN: "n <= length l ==> FIRSTN n l = BUTLASTN (length l - n) l"
- sorry
-
-lemma BUTLASTN_FIRSTN: "n <= length l ==> BUTLASTN n l = FIRSTN (length l - n) l"
- sorry
-
-lemma LASTN_BUTFIRSTN: "n <= length l ==> LASTN n l = BUTFIRSTN (length l - n) l"
- sorry
-
-lemma BUTFIRSTN_LASTN: "n <= length l ==> BUTFIRSTN n l = LASTN (length l - n) l"
- sorry
-
-lemma SEG_LASTN_BUTLASTN: "n + m <= length l ==> SEG n m l = LASTN n (BUTLASTN (length l - (n + m)) l)"
- sorry
-
-lemma BUTFIRSTN_REVERSE: "n <= length l ==> BUTFIRSTN n (rev l) = rev (BUTLASTN n l)"
- sorry
-
-lemma BUTLASTN_REVERSE: "n <= length l ==> BUTLASTN n (rev l) = rev (BUTFIRSTN n l)"
- sorry
-
-lemma LASTN_REVERSE: "n <= length l ==> LASTN n (rev l) = rev (FIRSTN n l)"
- sorry
-
-lemma FIRSTN_REVERSE: "n <= length l ==> FIRSTN n (rev l) = rev (LASTN n l)"
- sorry
-
-lemma SEG_REVERSE: "n + m <= length l ==> SEG n m (rev l) = rev (SEG n (length l - (n + m)) l)"
- sorry
-
-lemma LENGTH_GENLIST: "length (GENLIST f n) = n"
- sorry
-
-lemma LENGTH_REPLICATE: "length (REPLICATE n x) = n"
- sorry
-
-lemma IS_EL_REPLICATE: "0 < n ==> List.member (REPLICATE n x) x"
- sorry
-
-lemma ALL_EL_REPLICATE: "list_all (op = x) (REPLICATE n x)"
- sorry
-
-lemma AND_EL_FOLDL: "AND_EL l = foldl op & True l"
- sorry
-
-lemma AND_EL_FOLDR: "AND_EL l = foldr op & l True"
- sorry
-
-lemma OR_EL_FOLDL: "OR_EL l = foldl op | False l"
- sorry
-
-lemma OR_EL_FOLDR: "OR_EL l = foldr op | l False"
- sorry
-
-;end_setup
-
-setup_theory "~~/src/HOL/Import/HOL4/Generated" state_transformer
-
-definition
- UNIT :: "'b => 'a => 'b * 'a" where
- "(op ==::('b::type => 'a::type => 'b::type * 'a::type)
- => ('b::type => 'a::type => 'b::type * 'a::type) => prop)
- (UNIT::'b::type => 'a::type => 'b::type * 'a::type)
- (Pair::'b::type => 'a::type => 'b::type * 'a::type)"
-
-lemma UNIT_DEF: "UNIT x = Pair x"
- sorry
-
-definition
- BIND :: "('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a" where
- "BIND == %g f. (%(x, y). f x y) o g"
-
-lemma BIND_DEF: "BIND (g::'a => 'b * 'a) (f::'b => 'a => 'c * 'a) =
-(%(x::'b, y::'a). f x y) o g"
- sorry
-
-definition
- MMAP :: "('c => 'b) => ('a => 'c * 'a) => 'a => 'b * 'a" where
- "MMAP == %(f::'c => 'b) m::'a => 'c * 'a. BIND m (UNIT o f)"
-
-lemma MMAP_DEF: "MMAP f m = BIND m (UNIT o f)"
- sorry
-
-definition
- JOIN :: "('a => ('a => 'b * 'a) * 'a) => 'a => 'b * 'a" where
- "JOIN == %z. BIND z I"
-
-lemma JOIN_DEF: "JOIN z = BIND z I"
- sorry
-
-lemma BIND_LEFT_UNIT: "BIND (UNIT (x::'a)) (k::'a => 'b => 'c * 'b) = k x"
- sorry
-
-lemma UNIT_UNCURRY: "prod_case UNIT x = x"
- sorry
-
-lemma BIND_RIGHT_UNIT: "BIND k UNIT = k"
- sorry
-
-lemma BIND_ASSOC: "BIND (x::'a => 'b * 'a)
- (%a::'b. BIND ((xa::'b => 'a => 'c * 'a) a) (xb::'c => 'a => 'd * 'a)) =
-BIND (BIND x xa) xb"
- sorry
-
-lemma MMAP_ID: "MMAP I = I"
- sorry
-
-lemma MMAP_COMP: "MMAP ((f::'c => 'd) o (g::'b => 'c)) = MMAP f o MMAP g"
- sorry
-
-lemma MMAP_UNIT: "MMAP (f::'b => 'c) o UNIT = UNIT o f"
- sorry
-
-lemma MMAP_JOIN: "MMAP f o JOIN = JOIN o MMAP (MMAP f)"
- sorry
-
-lemma JOIN_UNIT: "JOIN o UNIT = I"
- sorry
-
-lemma JOIN_MMAP_UNIT: "JOIN o MMAP UNIT = I"
- sorry
-
-lemma JOIN_MAP_JOIN: "JOIN o MMAP JOIN = JOIN o JOIN"
- sorry
-
-lemma JOIN_MAP: "BIND (x::'a => 'b * 'a) (xa::'b => 'a => 'c * 'a) = JOIN (MMAP xa x)"
- sorry
-
-lemma FST_o_UNIT: "fst o UNIT (x::'a) = K x"
- sorry
-
-lemma SND_o_UNIT: "snd o UNIT (x::'a) = I"
- sorry
-
-lemma FST_o_MMAP: "fst o MMAP (x::'a => 'b) (xa::'c => 'a * 'c) = x o (fst o xa)"
- sorry
-
-;end_setup
-
-end
-