File Bag.ML

Addsimps [bag_elems_def];

Goal "bag_elems {(a,2),(b,1)} = ?x";
by (Simp_tac 1);
qed "bagtest1";

Addsimps [add_elem_bag];

Goal "add_elem_bag ''a'' w {(''a'',2),(''b'',1),(''c'', n), (''a'', m)} = ?x";
by (Simp_tac 1);
qed "bagtest2";

Addsimps [bag_union_def];

Goal "bag_union {(''a'',m)} {(''a'',n)} = ?x";
by (Simp_tac 1);
qed "baguniontest1";

Goal "bag_union {(''a'',m),(''b'',n),(''c'',w)} {(''a'',n),(''b'',2),(''d'',1)} = ?x";
by (Simp_tac 1);
qed "baguniontest2";

Goal "e # s = r ==> set r = {e} Un set s";
by (Auto_tac);
qed "insertList12_applic_1";