Structure bagTheory
signature bagTheory =
sig
type thm = Thm.thm
(* Definitions *)
val BAG_CARD : thm
val BAG_CARD_RELn : thm
val BAG_CHOICE_DEF : thm
val BAG_DELETE : thm
val BAG_DIFF : thm
val BAG_DISJOINT : thm
val BAG_FILTER_DEF : thm
val BAG_IMAGE_DEF : thm
val BAG_IN : thm
val BAG_INN : thm
val BAG_INSERT : thm
val BAG_INTER : thm
val BAG_MERGE : thm
val BAG_OF_SET : thm
val BAG_REST_DEF : thm
val BAG_UNION : thm
val BAG_VAL_DEF : thm
val BAG_delta : thm
val EL_BAG : thm
val EMPTY_BAG : thm
val FINITE_BAG : thm
val ITBAG_curried_def : thm
val ITBAG_tupled_primitive_def : thm
val PSUB_BAG : thm
val SET_OF_BAG : thm
val SING_BAG : thm
val SUB_BAG : thm
(* Theorems *)
val ASSOC_BAG_UNION : thm
val BAG_CARD_BAG_INN : thm
val BAG_CARD_EMPTY : thm
val BAG_CARD_THM : thm
val BAG_DELETE_11 : thm
val BAG_DELETE_BAG_IN : thm
val BAG_DELETE_BAG_IN_down : thm
val BAG_DELETE_BAG_IN_up : thm
val BAG_DELETE_EMPTY : thm
val BAG_DELETE_INSERT : thm
val BAG_DELETE_PSUB_BAG : thm
val BAG_DELETE_SING : thm
val BAG_DELETE_TWICE : thm
val BAG_DELETE_commutes : thm
val BAG_DELETE_concrete : thm
val BAG_DIFF_2L : thm
val BAG_DIFF_2R : thm
val BAG_DIFF_EMPTY : thm
val BAG_DIFF_EMPTY_simple : thm
val BAG_DIFF_EQNS : thm
val BAG_DIFF_INSERT : thm
val BAG_DIFF_INSERT_same : thm
val BAG_DIFF_UNION_eliminate : thm
val BAG_DISJOINT_DIFF : thm
val BAG_DISJOINT_EMPTY : thm
val BAG_EXTENSION : thm
val BAG_FILTER_BAG_INSERT : thm
val BAG_FILTER_EMPTY : thm
val BAG_IMAGE_EMPTY : thm
val BAG_IMAGE_FINITE : thm
val BAG_IMAGE_FINITE_INSERT : thm
val BAG_INN_0 : thm
val BAG_INN_BAG_DELETE : thm
val BAG_INN_BAG_FILTER : thm
val BAG_INN_BAG_INSERT : thm
val BAG_INN_BAG_UNION : thm
val BAG_INN_EMPTY_BAG : thm
val BAG_INN_LESS : thm
val BAG_INSERT_CHOICE_REST : thm
val BAG_INSERT_DIFF : thm
val BAG_INSERT_EQ_UNION : thm
val BAG_INSERT_NOT_EMPTY : thm
val BAG_INSERT_ONE_ONE : thm
val BAG_INSERT_UNION : thm
val BAG_INSERT_commutes : thm
val BAG_INTER_EQNS : thm
val BAG_IN_BAG_DELETE : thm
val BAG_IN_BAG_FILTER : thm
val BAG_IN_BAG_INSERT : thm
val BAG_IN_BAG_UNION : thm
val BAG_IN_FINITE_BAG_IMAGE : thm
val BAG_MERGE_EQNS : thm
val BAG_OF_EMPTY : thm
val BAG_UNION_DIFF : thm
val BAG_UNION_EMPTY : thm
val BAG_UNION_INSERT : thm
val BAG_UNION_LEFT_CANCEL : thm
val BAG_cases : thm
val BAG_delta_eliminate : thm
val BCARD_0 : thm
val BCARD_SUC : thm
val COMMUTING_ITBAG_INSERT : thm
val COMMUTING_ITBAG_RECURSES : thm
val COMM_BAG_UNION : thm
val C_BAG_INSERT_ONE_ONE : thm
val EL_BAG_11 : thm
val EL_BAG_INSERT_squeeze : thm
val EMPTY_BAG_alt : thm
val FINITE_BAG_DIFF : thm
val FINITE_BAG_DIFF_dual : thm
val FINITE_BAG_FILTER : thm
val FINITE_BAG_INDUCT : thm
val FINITE_BAG_INSERT : thm
val FINITE_BAG_THM : thm
val FINITE_BAG_UNION : thm
val FINITE_EMPTY_BAG : thm
val FINITE_SET_OF_BAG : thm
val FINITE_SUB_BAG : thm
val IN_SET_OF_BAG : thm
val ITBAG_EMPTY : thm
val ITBAG_IND : thm
val ITBAG_INSERT : thm
val ITBAG_THM : thm
val MEMBER_NOT_EMPTY : thm
val NOT_IN_BAG_DIFF : thm
val NOT_IN_EMPTY_BAG : thm
val NOT_IN_SUB_BAG_INSERT : thm
val PSUB_BAG_ANTISYM : thm
val PSUB_BAG_CARD : thm
val PSUB_BAG_IRREFL : thm
val PSUB_BAG_NOT_EQ : thm
val PSUB_BAG_REST : thm
val PSUB_BAG_SUB_BAG : thm
val PSUB_BAG_TRANS : thm
val SET_BAG_I : thm
val SET_OF_BAG_DIFF_SUBSET_down : thm
val SET_OF_BAG_DIFF_SUBSET_up : thm
val SET_OF_BAG_EQ_EMPTY : thm
val SET_OF_BAG_EQ_INSERT : thm
val SET_OF_BAG_INSERT : thm
val SET_OF_BAG_UNION : thm
val SET_OF_EL_BAG : thm
val SET_OF_EMPTY : thm
val SING_BAG_THM : thm
val SING_EL_BAG : thm
val STRONG_FINITE_BAG_INDUCT : thm
val SUB_BAG_ANTISYM : thm
val SUB_BAG_BAG_DIFF : thm
val SUB_BAG_BAG_IN : thm
val SUB_BAG_CARD : thm
val SUB_BAG_DIFF : thm
val SUB_BAG_DIFF_EQ : thm
val SUB_BAG_EL_BAG : thm
val SUB_BAG_EMPTY : thm
val SUB_BAG_EQNS : thm
val SUB_BAG_EXISTS : thm
val SUB_BAG_INSERT : thm
val SUB_BAG_LEQ : thm
val SUB_BAG_PSUB_BAG : thm
val SUB_BAG_REFL : thm
val SUB_BAG_REST : thm
val SUB_BAG_SET : thm
val SUB_BAG_TRANS : thm
val SUB_BAG_UNION : thm
val SUB_BAG_UNION_DIFF : thm
val SUB_BAG_UNION_MONO : thm
val SUB_BAG_UNION_down : thm
val SUB_BAG_UNION_eliminate : thm
val SUB_BAG_delta : thm
val move_BAG_UNION_over_eq : thm
val bag_grammars : type_grammar.grammar * term_grammar.grammar
val bag_rwts : simpLib.ssfrag
(*
[pred_set] Parent theory of "bag"
[BAG_CARD] Definition
|- !b. FINITE_BAG b ==> BAG_CARD_RELn b (BAG_CARD b)
[BAG_CARD_RELn] Definition
|- !b n.
BAG_CARD_RELn b n =
!P.
P {| |} 0 /\ (!b n. P b n ==> !e. P (BAG_INSERT e b) (SUC n)) ==> P b n
[BAG_CHOICE_DEF] Definition
|- !b. ~(b = {| |}) ==> BAG_IN (BAG_CHOICE b) b
[BAG_DELETE] Definition
|- !b0 e b. BAG_DELETE b0 e b = (b0 = BAG_INSERT e b)
[BAG_DIFF] Definition
|- !b1 b2. BAG_DIFF b1 b2 = (\x. b1 x - b2 x)
[BAG_DISJOINT] Definition
|- !b1 b2. BAG_DISJOINT b1 b2 = DISJOINT (SET_OF_BAG b1) (SET_OF_BAG b2)
[BAG_FILTER_DEF] Definition
|- !P b. BAG_FILTER P b = (\e. (if P e then b e else 0))
[BAG_IMAGE_DEF] Definition
|- !f b.
BAG_IMAGE f b =
(\e.
(let sb = BAG_FILTER (\e0. f e0 = e) b in
(if FINITE_BAG sb then BAG_CARD sb else 0)))
[BAG_IN] Definition
|- !e b. BAG_IN e b = BAG_INN e 1 b
[BAG_INN] Definition
|- !e n b. BAG_INN e n b = b e >= n
[BAG_INSERT] Definition
|- !e b. BAG_INSERT e b = (\x. (if x = e then b e + 1 else b x))
[BAG_INTER] Definition
|- !b1 b2. BAG_INTER b1 b2 = (\x. (if b1 x < b2 x then b1 x else b2 x))
[BAG_MERGE] Definition
|- !b1 b2. BAG_MERGE b1 b2 = (\x. (if b1 x < b2 x then b2 x else b1 x))
[BAG_OF_SET] Definition
|- !P. BAG_OF_SET P = (\x. (if x IN P then 1 else 0))
[BAG_REST_DEF] Definition
|- !b. BAG_REST b = BAG_DIFF b (EL_BAG (BAG_CHOICE b))
[BAG_UNION] Definition
|- !b c. BAG_UNION b c = (\x. b x + c x)
[BAG_VAL_DEF] Definition
|- !b x. BAG_VAL b x = b x
[BAG_delta] Definition
|- !B1 B2 B3.
BAG_delta (B1,B2) B3 =
BAG_DIFF (BAG_UNION B3 (BAG_DIFF B2 B1)) (BAG_DIFF B1 B2)
[EL_BAG] Definition
|- !e. EL_BAG e = {|e|}
[EMPTY_BAG] Definition
|- {| |} = K 0
[FINITE_BAG] Definition
|- !b.
FINITE_BAG b = !P. P {| |} /\ (!b. P b ==> !e. P (BAG_INSERT e b)) ==> P b
[ITBAG_curried_def] Definition
|- !f x x1. ITBAG f x x1 = ITBAG_tupled f (x,x1)
[ITBAG_tupled_primitive_def] Definition
|- !f.
ITBAG_tupled f =
WFREC
(@R.
WF R /\
!acc b.
FINITE_BAG b /\ ~(b = {| |}) ==>
R (BAG_REST b,f (BAG_CHOICE b) acc) (b,acc))
(\ITBAG_tupled a.
case a of
(b,acc) ->
I
(if FINITE_BAG b then
(if b = {| |} then
acc
else
ITBAG_tupled (BAG_REST b,f (BAG_CHOICE b) acc))
else
ARB))
[PSUB_BAG] Definition
|- !b1 b2. PSUB_BAG b1 b2 = SUB_BAG b1 b2 /\ ~(b1 = b2)
[SET_OF_BAG] Definition
|- !b. SET_OF_BAG b = (\x. BAG_IN x b)
[SING_BAG] Definition
|- !b. SING_BAG b = ?x. b = {|x|}
[SUB_BAG] Definition
|- !b1 b2. SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2
[ASSOC_BAG_UNION] Theorem
|- !b1 b2 b3. BAG_UNION b1 (BAG_UNION b2 b3) = BAG_UNION (BAG_UNION b1 b2) b3
[BAG_CARD_BAG_INN] Theorem
|- !b. FINITE_BAG b ==> !n e. BAG_INN e n b ==> n <= BAG_CARD b
[BAG_CARD_EMPTY] Theorem
|- BAG_CARD {| |} = 0
[BAG_CARD_THM] Theorem
|- (BAG_CARD {| |} = 0) /\
!b. FINITE_BAG b ==> !e. BAG_CARD (BAG_INSERT e b) = BAG_CARD b + 1
[BAG_DELETE_11] Theorem
|- !b0 e1 e2 b1 b2.
BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 ==> ((e1 = e2) = (b1 = b2))
[BAG_DELETE_BAG_IN] Theorem
|- !b0 b e. BAG_DELETE b0 e b ==> BAG_IN e b0
[BAG_DELETE_BAG_IN_down] Theorem
|- !b0 b e1 e2.
BAG_DELETE b0 e1 b /\ ~(e1 = e2) /\ BAG_IN e2 b0 ==> BAG_IN e2 b
[BAG_DELETE_BAG_IN_up] Theorem
|- !b0 b e. BAG_DELETE b0 e b ==> !e'. BAG_IN e' b ==> BAG_IN e' b0
[BAG_DELETE_EMPTY] Theorem
|- !e b. ~BAG_DELETE {| |} e b
[BAG_DELETE_INSERT] Theorem
|- !x y b1 b2.
BAG_DELETE (BAG_INSERT x b1) y b2 ==>
(x = y) /\ (b1 = b2) \/ (?b3. BAG_DELETE b1 y b3) /\ ~(x = y)
[BAG_DELETE_PSUB_BAG] Theorem
|- !b0 e b. BAG_DELETE b0 e b ==> PSUB_BAG b b0
[BAG_DELETE_SING] Theorem
|- !b e. BAG_DELETE b e {| |} ==> SING_BAG b
[BAG_DELETE_TWICE] Theorem
|- !b0 e1 e2 b1 b2.
BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 /\ ~(b1 = b2) ==>
?b. BAG_DELETE b1 e2 b /\ BAG_DELETE b2 e1 b
[BAG_DELETE_commutes] Theorem
|- !b0 b1 b2 e1 e2.
BAG_DELETE b0 e1 b1 /\ BAG_DELETE b1 e2 b2 ==>
?b'. BAG_DELETE b0 e2 b' /\ BAG_DELETE b' e1 b2
[BAG_DELETE_concrete] Theorem
|- !b0 b e.
BAG_DELETE b0 e b =
b0 e > 0 /\ (b = (\x. (if x = e then b0 e - 1 else b0 x)))
[BAG_DIFF_2L] Theorem
|- !X Y Z. BAG_DIFF (BAG_DIFF X Y) Z = BAG_DIFF X (BAG_UNION Y Z)
[BAG_DIFF_2R] Theorem
|- !A B C.
SUB_BAG C B ==> (BAG_DIFF A (BAG_DIFF B C) = BAG_DIFF (BAG_UNION A C) B)
[BAG_DIFF_EMPTY] Theorem
|- (!b. BAG_DIFF b b = {| |}) /\ (!b. BAG_DIFF b {| |} = b) /\
(!b. BAG_DIFF {| |} b = {| |}) /\
!b1 b2. SUB_BAG b1 b2 ==> (BAG_DIFF b1 b2 = {| |})
[BAG_DIFF_EMPTY_simple] Theorem
|- (!b. BAG_DIFF b b = {| |}) /\ (!b. BAG_DIFF b {| |} = b) /\
!b. BAG_DIFF {| |} b = {| |}
[BAG_DIFF_EQNS] Theorem
|- (!b. BAG_DIFF b {| |} = b) /\ (!b. BAG_DIFF {| |} b = {| |}) /\
(!x b y.
BAG_DIFF (BAG_INSERT x b) {|y|} =
(if x = y then b else BAG_INSERT x (BAG_DIFF b {|y|}))) /\
!b1 y b2. BAG_DIFF b1 (BAG_INSERT y b2) = BAG_DIFF (BAG_DIFF b1 {|y|}) b2
[BAG_DIFF_INSERT] Theorem
|- !x b1 b2.
~BAG_IN x b1 ==>
(BAG_DIFF (BAG_INSERT x b2) b1 = BAG_INSERT x (BAG_DIFF b2 b1))
[BAG_DIFF_INSERT_same] Theorem
|- !x b1 b2. BAG_DIFF (BAG_INSERT x b1) (BAG_INSERT x b2) = BAG_DIFF b1 b2
[BAG_DIFF_UNION_eliminate] Theorem
|- !b1 b2 b3.
(BAG_DIFF (BAG_UNION b1 b2) (BAG_UNION b1 b3) = BAG_DIFF b2 b3) /\
(BAG_DIFF (BAG_UNION b1 b2) (BAG_UNION b3 b1) = BAG_DIFF b2 b3) /\
(BAG_DIFF (BAG_UNION b2 b1) (BAG_UNION b1 b3) = BAG_DIFF b2 b3) /\
(BAG_DIFF (BAG_UNION b2 b1) (BAG_UNION b3 b1) = BAG_DIFF b2 b3)
[BAG_DISJOINT_DIFF] Theorem
|- !B1 B2. BAG_DISJOINT (BAG_DIFF B1 B2) (BAG_DIFF B2 B1)
[BAG_DISJOINT_EMPTY] Theorem
|- !b. BAG_DISJOINT b {| |} /\ BAG_DISJOINT {| |} b
[BAG_EXTENSION] Theorem
|- !b1 b2. (b1 = b2) = !n e. BAG_INN e n b1 = BAG_INN e n b2
[BAG_FILTER_BAG_INSERT] Theorem
|- BAG_FILTER P (BAG_INSERT e b) =
(if P e then BAG_INSERT e (BAG_FILTER P b) else BAG_FILTER P b)
[BAG_FILTER_EMPTY] Theorem
|- BAG_FILTER P {| |} = {| |}
[BAG_IMAGE_EMPTY] Theorem
|- BAG_IMAGE f {| |} = {| |}
[BAG_IMAGE_FINITE] Theorem
|- !b. FINITE_BAG b ==> FINITE_BAG (BAG_IMAGE f b)
[BAG_IMAGE_FINITE_INSERT] Theorem
|- !b.
FINITE_BAG b ==>
(BAG_IMAGE f (BAG_INSERT e b) = BAG_INSERT (f e) (BAG_IMAGE f b))
[BAG_INN_0] Theorem
|- !b e. BAG_INN e 0 b
[BAG_INN_BAG_DELETE] Theorem
|- !b n e. BAG_INN e n b /\ n > 0 ==> ?b'. BAG_DELETE b e b'
[BAG_INN_BAG_FILTER] Theorem
|- BAG_INN e n (BAG_FILTER P b) = (n = 0) \/ P e /\ BAG_INN e n b
[BAG_INN_BAG_INSERT] Theorem
|- !b e1 e2.
BAG_INN e1 n (BAG_INSERT e2 b) =
BAG_INN e1 (n - 1) b /\ (e1 = e2) \/ BAG_INN e1 n b
[BAG_INN_BAG_UNION] Theorem
|- !n e b1 b2.
BAG_INN e n (BAG_UNION b1 b2) =
?m1 m2. (n = m1 + m2) /\ BAG_INN e m1 b1 /\ BAG_INN e m2 b2
[BAG_INN_EMPTY_BAG] Theorem
|- !e n. BAG_INN e n {| |} = (n = 0)
[BAG_INN_LESS] Theorem
|- !b e n m. BAG_INN e n b /\ m < n ==> BAG_INN e m b
[BAG_INSERT_CHOICE_REST] Theorem
|- !b. ~(b = {| |}) ==> (b = BAG_INSERT (BAG_CHOICE b) (BAG_REST b))
[BAG_INSERT_DIFF] Theorem
|- !x b. ~(BAG_INSERT x b = b)
[BAG_INSERT_EQ_UNION] Theorem
|- !e b1 b2 b.
(BAG_INSERT e b = BAG_UNION b1 b2) ==> BAG_IN e b1 \/ BAG_IN e b2
[BAG_INSERT_NOT_EMPTY] Theorem
|- !x b. ~(BAG_INSERT x b = {| |})
[BAG_INSERT_ONE_ONE] Theorem
|- !b1 b2 x. (BAG_INSERT x b1 = BAG_INSERT x b2) = (b1 = b2)
[BAG_INSERT_UNION] Theorem
|- !b e. BAG_INSERT e b = BAG_UNION (EL_BAG e) b
[BAG_INSERT_commutes] Theorem
|- !b e1 e2. BAG_INSERT e1 (BAG_INSERT e2 b) = BAG_INSERT e2 (BAG_INSERT e1 b)
[BAG_INTER_EQNS] Theorem
|- (!b. BAG_INTER {| |} b = {| |}) /\ (!b. BAG_INTER b {| |} = {| |}) /\
!x b1 b2.
BAG_INTER (BAG_INSERT x b1) b2 =
(if BAG_IN x b2 then
BAG_INSERT x (BAG_INTER b1 (BAG_DIFF b2 {|x|}))
else
BAG_INTER b1 b2)
[BAG_IN_BAG_DELETE] Theorem
|- !b e. BAG_IN e b ==> ?b'. BAG_DELETE b e b'
[BAG_IN_BAG_FILTER] Theorem
|- BAG_IN e (BAG_FILTER P b) = P e /\ BAG_IN e b
[BAG_IN_BAG_INSERT] Theorem
|- !b e1 e2. BAG_IN e1 (BAG_INSERT e2 b) = (e1 = e2) \/ BAG_IN e1 b
[BAG_IN_BAG_UNION] Theorem
|- !b1 b2 e. BAG_IN e (BAG_UNION b1 b2) = BAG_IN e b1 \/ BAG_IN e b2
[BAG_IN_FINITE_BAG_IMAGE] Theorem
|- FINITE_BAG b ==> (BAG_IN x (BAG_IMAGE f b) = ?y. (f y = x) /\ BAG_IN y b)
[BAG_MERGE_EQNS] Theorem
|- (!b. BAG_MERGE {| |} b = b) /\ (!b. BAG_MERGE b {| |} = b) /\
!x b1 b2.
BAG_MERGE (BAG_INSERT x b1) b2 =
BAG_INSERT x (BAG_MERGE b1 (BAG_DIFF b2 {|x|}))
[BAG_OF_EMPTY] Theorem
|- SET_OF_BAG {| |} = {}
[BAG_UNION_DIFF] Theorem
|- !X Y Z.
SUB_BAG Z Y ==>
(BAG_UNION X (BAG_DIFF Y Z) = BAG_DIFF (BAG_UNION X Y) Z) /\
(BAG_UNION (BAG_DIFF Y Z) X = BAG_DIFF (BAG_UNION X Y) Z)
[BAG_UNION_EMPTY] Theorem
|- (!b. BAG_UNION b {| |} = b) /\ (!b. BAG_UNION {| |} b = b) /\
!b1 b2. (BAG_UNION b1 b2 = {| |}) = (b1 = {| |}) /\ (b2 = {| |})
[BAG_UNION_INSERT] Theorem
|- !e b1 b2.
(BAG_UNION (BAG_INSERT e b1) b2 = BAG_INSERT e (BAG_UNION b1 b2)) /\
(BAG_UNION b1 (BAG_INSERT e b2) = BAG_INSERT e (BAG_UNION b1 b2))
[BAG_UNION_LEFT_CANCEL] Theorem
|- !b b1 b2. (BAG_UNION b b1 = BAG_UNION b b2) = (b1 = b2)
[BAG_cases] Theorem
|- !b. (b = {| |}) \/ ?b0 e. b = BAG_INSERT e b0
[BAG_delta_eliminate] Theorem
|- (!A BU BD X.
SUB_BAG X A ==>
(BAG_delta (A,BAG_DIFF (BAG_UNION A BU) BD) X =
BAG_DIFF (BAG_UNION X BU) BD)) /\
!A BU BD X.
SUB_BAG X A ==>
(BAG_delta (A,BAG_DIFF (BAG_UNION BU A) BD) X =
BAG_DIFF (BAG_UNION BU X) BD)
[BCARD_0] Theorem
|- !b. FINITE_BAG b ==> ((BAG_CARD b = 0) = (b = {| |}))
[BCARD_SUC] Theorem
|- !b.
FINITE_BAG b ==>
!n.
(BAG_CARD b = SUC n) = ?b0 e. (b = BAG_INSERT e b0) /\ (BAG_CARD b0 = n)
[COMMUTING_ITBAG_INSERT] Theorem
|- !f b.
(!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==>
!x a. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a)
[COMMUTING_ITBAG_RECURSES] Theorem
|- !f e b a.
(!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==>
(ITBAG f (BAG_INSERT e b) a = f e (ITBAG f b a))
[COMM_BAG_UNION] Theorem
|- !b1 b2. BAG_UNION b1 b2 = BAG_UNION b2 b1
[C_BAG_INSERT_ONE_ONE] Theorem
|- !x y b. (BAG_INSERT x b = BAG_INSERT y b) = (x = y)
[EL_BAG_11] Theorem
|- !x y. (EL_BAG x = EL_BAG y) ==> (x = y)
[EL_BAG_INSERT_squeeze] Theorem
|- !x b y. (EL_BAG x = BAG_INSERT y b) ==> (x = y) /\ (b = {| |})
[EMPTY_BAG_alt] Theorem
|- {| |} = (\x. 0)
[FINITE_BAG_DIFF] Theorem
|- !b1. FINITE_BAG b1 ==> !b2. FINITE_BAG (BAG_DIFF b1 b2)
[FINITE_BAG_DIFF_dual] Theorem
|- !b1. FINITE_BAG b1 ==> !b2. FINITE_BAG (BAG_DIFF b2 b1) ==> FINITE_BAG b2
[FINITE_BAG_FILTER] Theorem
|- !b. FINITE_BAG b ==> FINITE_BAG (BAG_FILTER P b)
[FINITE_BAG_INDUCT] Theorem
|- !P.
P {| |} /\ (!b. P b ==> !e. P (BAG_INSERT e b)) ==>
!b. FINITE_BAG b ==> P b
[FINITE_BAG_INSERT] Theorem
|- !b. FINITE_BAG b ==> !e. FINITE_BAG (BAG_INSERT e b)
[FINITE_BAG_THM] Theorem
|- FINITE_BAG {| |} /\ !e b. FINITE_BAG (BAG_INSERT e b) = FINITE_BAG b
[FINITE_BAG_UNION] Theorem
|- !b1 b2. FINITE_BAG (BAG_UNION b1 b2) = FINITE_BAG b1 /\ FINITE_BAG b2
[FINITE_EMPTY_BAG] Theorem
|- FINITE_BAG {| |}
[FINITE_SET_OF_BAG] Theorem
|- !b. FINITE (SET_OF_BAG b) = FINITE_BAG b
[FINITE_SUB_BAG] Theorem
|- !b1. FINITE_BAG b1 ==> !b2. SUB_BAG b2 b1 ==> FINITE_BAG b2
[IN_SET_OF_BAG] Theorem
|- !x b. x IN SET_OF_BAG b = BAG_IN x b
[ITBAG_EMPTY] Theorem
|- !f acc. ITBAG f {| |} acc = acc
[ITBAG_IND] Theorem
|- !P.
(!b acc.
(FINITE_BAG b /\ ~(b = {| |}) ==>
P (BAG_REST b) (f (BAG_CHOICE b) acc)) ==>
P b acc) ==>
!v v1. P v v1
[ITBAG_INSERT] Theorem
|- !f acc.
FINITE_BAG b ==>
(ITBAG f (BAG_INSERT x b) acc =
ITBAG f (BAG_REST (BAG_INSERT x b))
(f (BAG_CHOICE (BAG_INSERT x b)) acc))
[ITBAG_THM] Theorem
|- !b f acc.
FINITE_BAG b ==>
(ITBAG f b acc =
(if b = {| |} then acc else ITBAG f (BAG_REST b) (f (BAG_CHOICE b) acc)))
[MEMBER_NOT_EMPTY] Theorem
|- !b. (?x. BAG_IN x b) = ~(b = {| |})
[NOT_IN_BAG_DIFF] Theorem
|- !x b1 b2. ~BAG_IN x b1 ==> (BAG_DIFF b1 (BAG_INSERT x b2) = BAG_DIFF b1 b2)
[NOT_IN_EMPTY_BAG] Theorem
|- !x. ~BAG_IN x {| |}
[NOT_IN_SUB_BAG_INSERT] Theorem
|- !b1 b2 e. ~BAG_IN e b1 ==> (SUB_BAG b1 (BAG_INSERT e b2) = SUB_BAG b1 b2)
[PSUB_BAG_ANTISYM] Theorem
|- !b1 b2. ~(PSUB_BAG b1 b2 /\ PSUB_BAG b2 b1)
[PSUB_BAG_CARD] Theorem
|- !b1 b2. FINITE_BAG b2 /\ PSUB_BAG b1 b2 ==> BAG_CARD b1 < BAG_CARD b2
[PSUB_BAG_IRREFL] Theorem
|- !b. ~PSUB_BAG b b
[PSUB_BAG_NOT_EQ] Theorem
|- !b1 b2. PSUB_BAG b1 b2 ==> ~(b1 = b2)
[PSUB_BAG_REST] Theorem
|- !b. ~(b = {| |}) ==> PSUB_BAG (BAG_REST b) b
[PSUB_BAG_SUB_BAG] Theorem
|- !b1 b2. PSUB_BAG b1 b2 ==> SUB_BAG b1 b2
[PSUB_BAG_TRANS] Theorem
|- !b1 b2 b3. PSUB_BAG b1 b2 /\ PSUB_BAG b2 b3 ==> PSUB_BAG b1 b3
[SET_BAG_I] Theorem
|- !s. SET_OF_BAG (BAG_OF_SET s) = s
[SET_OF_BAG_DIFF_SUBSET_down] Theorem
|- !b1 b2. SET_OF_BAG b1 DIFF SET_OF_BAG b2 SUBSET SET_OF_BAG (BAG_DIFF b1 b2)
[SET_OF_BAG_DIFF_SUBSET_up] Theorem
|- !b1 b2. SET_OF_BAG (BAG_DIFF b1 b2) SUBSET SET_OF_BAG b1
[SET_OF_BAG_EQ_EMPTY] Theorem
|- !b.
(({} = SET_OF_BAG b) = (b = {| |})) /\ ((SET_OF_BAG b = {}) = (b = {| |}))
[SET_OF_BAG_EQ_INSERT] Theorem
|- !b e s.
(e INSERT s = SET_OF_BAG b) =
?b0 eb.
(b = BAG_UNION eb b0) /\ (s = SET_OF_BAG b0) /\
(!e'. BAG_IN e' eb ==> (e' = e)) /\ (~(e IN s) ==> BAG_IN e eb)
[SET_OF_BAG_INSERT] Theorem
|- !e b. SET_OF_BAG (BAG_INSERT e b) = e INSERT SET_OF_BAG b
[SET_OF_BAG_UNION] Theorem
|- !b1 b2. SET_OF_BAG (BAG_UNION b1 b2) = SET_OF_BAG b1 UNION SET_OF_BAG b2
[SET_OF_EL_BAG] Theorem
|- !e. SET_OF_BAG (EL_BAG e) = {e}
[SET_OF_EMPTY] Theorem
|- BAG_OF_SET {} = {| |}
[SING_BAG_THM] Theorem
|- !e. SING_BAG {|e|}
[SING_EL_BAG] Theorem
|- !e. SING_BAG (EL_BAG e)
[STRONG_FINITE_BAG_INDUCT] Theorem
|- !P.
P {| |} /\ (!b. FINITE_BAG b /\ P b ==> !e. P (BAG_INSERT e b)) ==>
!b. FINITE_BAG b ==> P b
[SUB_BAG_ANTISYM] Theorem
|- !b1 b2. SUB_BAG b1 b2 /\ SUB_BAG b2 b1 ==> (b1 = b2)
[SUB_BAG_BAG_DIFF] Theorem
|- !X Y Y' Z W.
SUB_BAG (BAG_DIFF X Y) (BAG_DIFF Z W) ==>
SUB_BAG (BAG_DIFF X (BAG_UNION Y Y')) (BAG_DIFF Z (BAG_UNION W Y'))
[SUB_BAG_BAG_IN] Theorem
|- !x b1 b2. SUB_BAG (BAG_INSERT x b1) b2 ==> BAG_IN x b2
[SUB_BAG_CARD] Theorem
|- !b1 b2. FINITE_BAG b2 /\ SUB_BAG b1 b2 ==> BAG_CARD b1 <= BAG_CARD b2
[SUB_BAG_DIFF] Theorem
|- (!b1 b2. SUB_BAG b1 b2 ==> !b3. SUB_BAG (BAG_DIFF b1 b3) b2) /\
!b1 b2 b3 b4.
SUB_BAG b2 b1 ==>
SUB_BAG b4 b3 ==>
(SUB_BAG (BAG_DIFF b1 b2) (BAG_DIFF b3 b4) =
SUB_BAG (BAG_UNION b1 b4) (BAG_UNION b2 b3))
[SUB_BAG_DIFF_EQ] Theorem
|- !b1 b2. SUB_BAG b1 b2 ==> (b2 = BAG_UNION b1 (BAG_DIFF b2 b1))
[SUB_BAG_EL_BAG] Theorem
|- !e b. SUB_BAG (EL_BAG e) b = BAG_IN e b
[SUB_BAG_EMPTY] Theorem
|- (!b. SUB_BAG {| |} b) /\ !b. SUB_BAG b {| |} = (b = {| |})
[SUB_BAG_EQNS] Theorem
|- (!b. SUB_BAG {| |} b = T) /\
!x b1 b2.
SUB_BAG (BAG_INSERT x b1) b2 =
BAG_IN x b2 /\ SUB_BAG b1 (BAG_DIFF b2 {|x|})
[SUB_BAG_EXISTS] Theorem
|- !b1 b2. SUB_BAG b1 b2 = ?b. b2 = BAG_UNION b1 b
[SUB_BAG_INSERT] Theorem
|- !e b1 b2. SUB_BAG (BAG_INSERT e b1) (BAG_INSERT e b2) = SUB_BAG b1 b2
[SUB_BAG_LEQ] Theorem
|- !b1 b2. SUB_BAG b1 b2 = !x. b1 x <= b2 x
[SUB_BAG_PSUB_BAG] Theorem
|- !b1 b2. SUB_BAG b1 b2 = PSUB_BAG b1 b2 \/ (b1 = b2)
[SUB_BAG_REFL] Theorem
|- !b. SUB_BAG b b
[SUB_BAG_REST] Theorem
|- !b. SUB_BAG (BAG_REST b) b
[SUB_BAG_SET] Theorem
|- !b1 b2. SUB_BAG b1 b2 ==> SET_OF_BAG b1 SUBSET SET_OF_BAG b2
[SUB_BAG_TRANS] Theorem
|- !b1 b2 b3. SUB_BAG b1 b2 /\ SUB_BAG b2 b3 ==> SUB_BAG b1 b3
[SUB_BAG_UNION] Theorem
|- (!b1 b2. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b2 b)) /\
(!b1 b2. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b b2)) /\
(!b1 b2 b3.
SUB_BAG b1 (BAG_UNION b2 b3) ==>
!b. SUB_BAG b1 (BAG_UNION (BAG_UNION b2 b) b3)) /\
(!b1 b2 b3.
SUB_BAG b1 (BAG_UNION b2 b3) ==>
!b. SUB_BAG b1 (BAG_UNION (BAG_UNION b b2) b3)) /\
(!b1 b2 b3.
SUB_BAG b1 (BAG_UNION b3 b2) ==>
!b. SUB_BAG b1 (BAG_UNION b3 (BAG_UNION b2 b))) /\
(!b1 b2 b3.
SUB_BAG b1 (BAG_UNION b3 b2) ==>
!b. SUB_BAG b1 (BAG_UNION b3 (BAG_UNION b b2))) /\
(!b1 b2 b3 b4.
SUB_BAG b1 b3 ==>
SUB_BAG b2 b4 ==>
SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)) /\
(!b1 b2 b3 b4.
SUB_BAG b1 b4 ==>
SUB_BAG b2 b3 ==>
SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b1 (BAG_UNION b3 b5) ==>
SUB_BAG b2 b4 ==>
SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b1 (BAG_UNION b4 b5) ==>
SUB_BAG b2 b3 ==>
SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b2 (BAG_UNION b3 b5) ==>
SUB_BAG b1 b4 ==>
SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b2 (BAG_UNION b4 b5) ==>
SUB_BAG b1 b3 ==>
SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b1 (BAG_UNION b5 b3) ==>
SUB_BAG b2 b4 ==>
SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b1 (BAG_UNION b5 b4) ==>
SUB_BAG b2 b3 ==>
SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b2 (BAG_UNION b5 b3) ==>
SUB_BAG b1 b4 ==>
SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
(!b1 b2 b3 b4 b5.
SUB_BAG b2 (BAG_UNION b5 b4) ==>
SUB_BAG b1 b3 ==>
SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b5 (BAG_UNION b3 b4))) /\
(!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b1 b2) b4 ==>
SUB_BAG b3 b5 ==>
SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b1 b2) b5 ==>
SUB_BAG b3 b4 ==>
SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b3 b2) b4 ==>
SUB_BAG b1 b5 ==>
SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b3 b2) b5 ==>
SUB_BAG b1 b4 ==>
SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b2 b1) b4 ==>
SUB_BAG b3 b5 ==>
SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b2 b1) b5 ==>
SUB_BAG b3 b4 ==>
SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)) /\
(!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b2 b3) b4 ==>
SUB_BAG b1 b5 ==>
SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)) /\
!b1 b2 b3 b4 b5.
SUB_BAG (BAG_UNION b2 b3) b5 ==>
SUB_BAG b1 b4 ==>
SUB_BAG (BAG_UNION b2 (BAG_UNION b1 b3)) (BAG_UNION b5 b4)
[SUB_BAG_UNION_DIFF] Theorem
|- !b1 b2 b3.
SUB_BAG b1 b3 ==>
(SUB_BAG b2 (BAG_DIFF b3 b1) = SUB_BAG (BAG_UNION b1 b2) b3)
[SUB_BAG_UNION_MONO] Theorem
|- !x y. SUB_BAG x (BAG_UNION x y)
[SUB_BAG_UNION_down] Theorem
|- !b1 b2 b3. SUB_BAG (BAG_UNION b1 b2) b3 ==> SUB_BAG b1 b3 /\ SUB_BAG b2 b3
[SUB_BAG_UNION_eliminate] Theorem
|- !b1 b2 b3.
(SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b1 b3) = SUB_BAG b2 b3) /\
(SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b1) = SUB_BAG b2 b3) /\
(SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b1 b3) = SUB_BAG b2 b3) /\
(SUB_BAG (BAG_UNION b2 b1) (BAG_UNION b3 b1) = SUB_BAG b2 b3)
[SUB_BAG_delta] Theorem
|- (!A B0 B. SUB_BAG B0 A ==> SUB_BAG B (BAG_delta (B0,B) A)) /\
!A B0 B. SUB_BAG A B0 ==> SUB_BAG (BAG_delta (B0,B) A) B
[move_BAG_UNION_over_eq] Theorem
|- !X Y Z. (BAG_UNION X Y = Z) ==> (X = BAG_DIFF Z Y)
*)
end
HOL 4, Kananaskis-3