(* general *) val prems = Goal "[| ALL x. Pa x & Pb x ; \ \ [| ALL x. Pa x ; ALL x. Pb x |] ==> P |] ==> P"; by (cut_facts_tac prems 1); by (auto_tac (claset() addIs prems, simpset())); qed "all_conjE"; Goal "f = g ==> f x = g x"; by (Auto_tac); qed "inst_fun_eq"; Goal "f = g ==> ALL x. f x = g x"; by (Auto_tac); qed "inst_fun_eq_all"; Goal "max (i::nat) j <= k ==> i <= k"; by (Auto_tac); qed "max_le1"; Goal "max (i::nat) j <= k ==> j <= k"; by (Auto_tac); qed "max_le2"; (* sets *) Goal "a : A ==> insert a A = A"; by (Auto_tac); qed "insert_elem"; Goal "Inter (insert A AA) = A Int (Inter AA)"; by (Auto_tac); qed "Inter_insert"; Goal "finite A ==> finite (Inter (insert A AA))"; by (Auto_tac); qed "Inter_insert_finite"; Goal "[| finite A ; A : AA |] ==> finite (Inter AA)"; by (dres_inst_tac [("AA", "AA")] Inter_insert_finite 1); by (auto_tac (claset(), simpset() addsimps [Inter_insert, insert_elem])); qed "Inter_finite_elem"; Goal "A = B ==> Inter A = Inter B"; by (Auto_tac); qed "eq_Inter_mono"; Goal "insert a (insert b A) = insert b (insert a A)"; by (Auto_tac); qed "insert_swap"; Goal "A <= B ==> insert a A <= insert a B"; by (Auto_tac); qed "subset_insert_mono"; Goal "A <= insert a B ==> insert a A <= insert a B"; by (Auto_tac); qed "subset_insert_mono1"; Goal "a:A ==> insert a A = A"; by (Auto_tac); qed "insert_elem"; Goal "A Un B <= C ==> A <= C & B <= C"; by (Auto_tac); qed "Un_subset_conj"; Goal "[| a : A ; b ~: A |] ==> a ~= b"; by (Auto_tac); qed "set_elem_dist"; Goal "(a, b) : R^* ==> a = b | a ~=b & (a, b) : R^+"; by (etac rtrancl_induct 1); by (auto_tac (claset() addIs [trancl_trans], simpset())); qed "rtranclD"; (* lists *) Goal "finite A ==> \ \ EX xs. set xs = A & length xs = card A & nodups xs"; by (etac finite_induct 1); by (Clarify_tac 2); by (res_inst_tac [("x", "x#xs")] exI 2); by (Auto_tac); qed "set_list_transform"; Goal "[| nodups xs ; xs ~= [] |] ==> nodups (tl xs)"; by (case_tac "xs" 1); by (Auto_tac); qed "nodups_tl"; Goal "nodups (xs@ys) --> nodups xs"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "nodups (xs@ys) ==> nodups xs"; by (fast_tac (claset() addIs [lemma RS mp]) 1); qed "nodups_app1"; Goal "nodups (xs@ys) --> nodups ys"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "nodups (xs@ys) ==> nodups ys"; by (fast_tac (claset() addIs [lemma RS mp]) 1); qed "nodups_app2"; Goal "nodups (xs @ ys) & x ~: set xs & x ~: set ys \ \ --> nodups (xs @ x # ys)"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "[| nodups (xs @ ys) ; x ~: set xs ; x ~: set ys |] \ \ ==> nodups (xs @ x # ys)"; by (fast_tac (claset() addIs [lemma RS mp]) 1); qed "nodups_insert"; Goal "nodups (xs @ x # ys) --> nodups (xs @ ys)"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "nodups (xs @ x # ys) ==> nodups (xs @ ys)"; by (fast_tac (claset() addDs [lemma RS mp]) 1); qed "nodups_rem"; Goal "[| nodups xs ; x ~: set xs |] ==> nodups (x # xs)"; by (dres_inst_tac [("xs", "[]")] (rotate_prems 2 nodups_insert) 1); by (Auto_tac); qed "nodups_cons"; Goal "nodups (xs @ ys) --> nodups (ys @ xs)"; by (induct_tac "xs" 1); by (auto_tac (claset() addIs [nodups_insert], simpset())); qed "lemma"; Goal "nodups (xs @ ys) ==> nodups (ys @ xs)"; by (fast_tac (claset() addIs [lemma RS mp]) 1); qed "nodups_swap_app"; Goal "nodups (xs @ x # ys) --> x ~: set xs"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "nodups (xs @ x # ys) ==> x ~: set xs"; by (fast_tac (claset() addDs [lemma RS mp]) 1); qed "nodups_set1"; Goal "nodups (xs @ x # ys) --> x ~: set ys"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "nodups (xs @ x # ys) ==> x ~: set ys"; by (fast_tac (claset() addDs [lemma RS mp]) 1); qed "nodups_set2"; Goal "nodups (x # xs @ y # ys) ==> nodups (x # y # xs @ ys)"; by (auto_tac (claset() addDs [nodups_set1, nodups_set2, nodups_rem], simpset())); qed "nodups_rearrange"; Goal "[| ys ~= [] ; nodups (x # xs @ ys) |] \ \ ==> nodups (x # (hd ys) # xs @ (tl ys))"; by (rtac nodups_rearrange 1); by (Auto_tac); qed "nodups_hd_tl2"; Goal "nodups (x#xs@ys) ==> nodups xs"; by (auto_tac (claset() addIs [nodups_app1], simpset())); qed "nodups_cons_app1"; Goal "nodups (x#xs@ys) ==> nodups ys"; by (auto_tac (claset() addIs [nodups_app2], simpset())); qed "nodups_cons_app2"; Goal "Suc n <= length xs --> xs ~= [] & n <= length (tl xs)"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "Suc n <= length xs ==> xs ~= [] & n <= length (tl xs)"; by (fast_tac (claset() addDs [lemma RS mp]) 1); qed "Suc_le_lengthD"; Goal "[| set ys Int insert a A = {} ; ys ~= [] |] \ \ ==> a ~= hd ys"; by (case_tac "ys" 1); by (Auto_tac); qed "Int_empty_ineq_hd"; Goal "[| set ys Int insert a A = {} ; ys ~= [] ; nodups ys |] \ \ ==> set (tl ys) Int insert (hd ys) A = {}"; by (case_tac "ys" 1); by (Auto_tac); qed "Int_empty_Int_tl_empty"; Goal "[| set ys Int insert a A = {} ; ys ~= [] ; nodups ys |] \ \ ==> set (tl ys) Int insert a (insert (hd ys) A) = {}"; by (case_tac "ys" 1); by (Auto_tac); qed "Int_empty_sort"; Goal "[| set ys Int insert a A = {} ; ys ~= [] ; nodups ys |] \ \ ==> hd ys ~: A"; by (case_tac "ys" 1); by (Auto_tac); qed "Int_empty_not_cont_hd"; Goal "[| set ys Int insert a A = {} ; ys ~= [] ; nodups ys |] \ \ ==> hd ys ~: insert a A"; by (case_tac "ys" 1); by (Auto_tac); qed "Int_empty_not_cont_hd_ins"; Goal "a ~: set (map fst xs) & x:set xs --> a ~= fst x"; by (induct_tac "xs" 1); by (Auto_tac); qed "lemma"; Goal "a ~: set (map fst xs) ==> ALL x:set xs. a ~= fst x"; by (rtac ballI 1); by (fast_tac (claset() addSIs [lemma RS mp]) 1); qed "not_in_not_fst"; Goal "[| set ys Int insert a A = {} ; ys ~= [] ; nodups ys ; b : A |] \ \ ==> hd ys ~= b"; by (case_tac "ys" 1); by (Auto_tac); qed "Int_empty_ineq_mem";