File ExtMain.ML


(* 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";