(* prove axioms for sequent to be in type class plus_ac0, order, pm_ge0 *) val seq_defs = [seq_zero_def, seq_plus_def, seq_minus_def, seq_le_def, seq_less_def] ; val sdss as [sds_plus_def, sds_minus_def, sds_le_def, sds_less_def] = map (simplify (simpset ()) o read_instantiate [("seq", "?X |- ?Y"), ("fmls", "?ant |- ?suc")]) (tl seq_defs) ; Addsimps sdss ; val pm_ths = [diff_0_le, minus_minus, le_add_diff] ; val ttcs = [ (case_tac_frees 1), TRY Safe_tac, (ALLGOALS (asm_full_simp_tac (esimps ( symmetric Zero_multiset_def :: seq_zero_def :: pm_ths))))] ; val seq_commute = prove_goal seqdef.thy "x + y = y + (x :: sequent)" (fn _ => ttcs) ; val seq_assoc = prove_goal seqdef.thy "(x + y) + z = (x :: sequent) + (y + z)" (fn _ => ttcs) ; val seq_zero = prove_goal seqdef.thy "0 + x = (x :: sequent)" (fn _ => ttcs) ; val seq_refl = prove_goal seqdef.thy "x <= (x :: sequent)" (fn _ => ttcs) ; val seq_trans = meta_std (prove_goal seqdef.thy "x <= y --> y <= z --> (x :: sequent) <= z" (fn _ => ttcs @ [Safe_tac, REPEAT (eatac order_trans 1 1)])) ; val seq_antisym = meta_std (prove_goal seqdef.thy "x <= y --> y <= x --> (x :: sequent) = y" (fn _ => ttcs @ [Safe_tac, REPEAT (eatac order_antisym 1 1)])) ; val seq_less_le = seq_less_def RS def_imp_eq ; val seq_all_ge0 = prove_goal seqdef.thy "0 <= (A :: sequent)" (fn _ => ttcs) ; val seq_diff_0_le = prove_goal seqdef.thy "(A - B = 0) = ((A :: sequent) <= B)" (fn _ => ttcs) ; val seq_plus_minus = prove_goal seqdef.thy "A + B - (A :: sequent) = B" (fn _ => ttcs) ; val seq_minus_minus = prove_goal seqdef.thy "A - B - C = (A :: sequent) - (B + C)" (fn _ => ttcs) ; val seq_le_add_diff = meta_std (prove_goal seqdef.thy "B <= A --> B + ((A :: sequent) - B) = A" (fn _ => ttcs)) ; (* consequence of atomicity *) val () = qed_goal_spec_mp "atom_le_union" seqdef.thy "seq_size A <= 1 --> A <= B + C --> A <= B | A <= C" (fn _ => [ (strip_tac 1), (subgoal_tac "seq_size A = 0 | seq_size A = Suc 0" 1), (arith_tac 2), (case_tac_frees 1), (Asm_full_simp_tac 1), (safe_tac (claset () delrules [disjCI])), (simp_tac (esimps [symmetric Zero_multiset_def]) 1), (case_tac "size multiset1" 1), (case_tac "size multiset2" 2), (ALLGOALS Asm_full_simp_tac), (ALLGOALS (force_tac (cesimps [single_le, ms_size_eq_1, symmetric Zero_multiset_def])))]) ; val () = qed_goal_spec_mp "less_seq_size_less" seqdef.thy "M < N --> seq_size M < seq_size N" (fn _ => [ (case_tac_frees 1), (asm_simp_tac (esimps seq_defs) 1), Safe_tac, (ALLGOALS (datac order_lessI 1)), (ALLGOALS (dtac less_size_less THEN' dtac le_size_le)), (ALLGOALS arith_tac)]) ; val () = qed_goal "seq_size_ms" seqdef.thy "seq_size A = size (ms_of_seq A)" (fn _ => ttcs) ; val () = qed_goalw "seq_size_eq0" seqdef.thy [seq_zero_def] "(seq_size A = 0) = (A = 0)" (fn _ => ttcs) ; val () = qed_goal "seq_size_plus" seqdef.thy "seq_size (M + N) = seq_size M + seq_size N" (fn _ => ttcs) ; val () = qed_goalw "ms_of_seq_eq0" seqdef.thy [seq_zero_def] "(ms_of_seq A = 0) = (A = 0)" (fn _ => ttcs) ; val () = qed_goal "ms_of_seq_plus" seqdef.thy "ms_of_seq (M + N) = ms_of_seq M + ms_of_seq N" (fn _ => ttcs) ; val () = ListPair.app bind_thm (["seq_size_0", "ms_of_seq_0"], [refl] RL ([seq_size_eq0, ms_of_seq_eq0] RL [iffD2])); Addsimps [seq_size_0, seq_size_eq0, seq_size_plus, ms_of_seq_0, ms_of_seq_eq0, ms_of_seq_plus] ;