Theory Bag

Up to index of Isabelle/HOL/Marvin2002

Bag = Marvin_lemmas +

types
  'a bag = "('a * nat) set"
  
  consts
  bag_elems :: "'a bag => 'a set"
   add_elem_bag :: "['a, nat, 'a bag] => 'a bag"
  bag_union :: "['a bag, 'a bag] => 'a bag"
  
  defs
  bag_elems_def "bag_elems B == (UN x:B. {fst x})"

  add_elem_bag "add_elem_bag e n B == UN y: B . ({x. fst y = e & x = (e, n + (snd y))} Un {x. fst y ~= e & x = y}) "
  
(*  bag_union_def "bag_union B1 B2 == (UN y: B1. (add_elem_bag (fst y) (snd y) B2))" *)
  rules
 bag_union_def "bag_union A B = ((if A = insert (x,n) C
                                then (add_elem_bag x n (bag_union C B))
                                else B))"
end

  

theorem bagtest1:

  bag_elems {(a, 2), (b, 1)} = {b, a}

theorem bagtest2:

  add_elem_bag ''a'' w {(''a'', 2), (''b'', 1), (''c'', n), (''a'', m)} =
  {(''a'', w + m), (''c'', n), (''b'', Suc 0), (''a'', Suc (Suc w))}

theorem baguniontest1:

  bag_union {(''a'', m)} {(''a'', n)} = bag_union {(''a'', m)} {(''a'', n)}

theorem baguniontest2:

  bag_union {(''a'', m), (''b'', n), (''c'', w)}
   {(''a'', n), (''b'', 2), (''d'', 1)} =
  bag_union {(''a'', m), (''b'', n), (''c'', w)}
   {(''a'', n), (''b'', 2), (''d'', Suc 0)}

theorem insertList12_applic_1:

  e # s = r ==> set r = {e} Un set s