File Basis.ML

(*###TO Set.ML*)
Goal "[| A - {x} <= B; x : A |] ==> A <= insert x B"; 
by(Blast_tac 1);
qed "diff_single_insert";

(*###TO Set.ML*)
Goal "B <= f `` A = (? A'. A' <= A \<and> B = f `` A')";
by Safe_tac;
by  (Fast_tac 2);
by (res_inst_tac [("x","{a. a : A & f a : B}")] exI 1);
by (Fast_tac 1);
qed "subset_image_iff";

Goal "test_b_y";
b y all_tac;

(*###TO Pure?*)
val instantiate_tac = PRIMITIVE o read_instantiate;
fun inst1_tac s t = instantiate_tac [(s,t)];
fun defern_tac n = EVERY'(replicate n defer_tac) 1;

(*###TO HOL/simpdata?*)
Goal "(%s. f s) = f";
br refl 1;
qed "eta_contract_eq";
bind_thm("eta_contract_rl", symmetric (eta_contract_eq RS eq_reflection));
(*
context CPure.thy;
Goal "(%s. f s) == f";
br reflexive_thm 1;
Addsimps [eta_contract_eq];
Addsimps [eta_contract_rl];
*)
val eta_contract_proc = Simplifier.mk_simproc "eta_contract"
    [Thm.read_cterm (sign_of HOL.thy) ("%s. f s", HOLogic.termT)] 
     (K (K (K (Some eta_contract_rl))));
(*Addsimprocs [eta_contract_proc];*)

bind_thm("if_def2", read_instantiate [("P","\<lambda>x. x")] split_if);

(* A particular thm about wf;
   looks like it is an odd instance of something more general
*)
context WF.thy;
Goal "wf{((A,x),(B,y)) . A=B & wf (R (f A)) & (x,y) : R (f A)}";
by(simp_tac (simpset_of WF.thy delcongs [imp_cong] addsimps [wf_def]) 1);
by(fold_goals_tac [wf_def]);
by(strip_tac 1);
by(rename_tac "A x" 1);
by(case_tac "wf (R (f A))" 1);
by (eres_inst_tac [("a","x")] wf_induct 1);
by (Fast_tac 1);
by(Blast_tac 1);
qed "wf_rel_lemma";


open Basis; context thy;

Goal "(!x. (? b. x = f b & Q b) \<longrightarrow> P x) = (!b. Q b --> P (f b))";
b y Auto_tac;
qed "All_Ex_refl_eq2";
Addsimps[All_Ex_refl_eq2];

qed_goal "ex_ex_miniscope1" thy 
  "(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)" (K [Auto_tac]);
Addsimps [ex_ex_miniscope1];

qed_goal "ex_miniscope2" thy 
  "(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))" (K [Auto_tac]);
Addsimps [ex_miniscope2];

Goal "(\<exists>z x y. P x y z) = (\<exists>x y z. P x y z)";
b y Auto_tac;
qed "ex_reorder31";

Goal "{p. P (split f p)} = {(a,b). P (f a b)}";
b y Auto_tac;
qed "Collect_split_eq";

Goal "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)";
by (case_tac "x:A" 1);
by  (Fast_tac 2);
by (rtac disjI2 1);
by (res_inst_tac [("x","A-{x}")] exI 1);
by (Fast_tac 1);
qed "subset_insertD";

(* ###TO HOL/???.ML?? *)
fun make_simproc name pat pred thm = Simplifier.mk_simproc name
   [Thm.read_cterm (Thm.sign_of_thm thm) (pat, HOLogic.termT)] 
   (K (K (fn s => if pred s then None else Some (standard (mk_meta_eq thm)))));

val thin_All_tac = thin_tac "All ?P";
val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
fun noAll_simpset () = simpset() setmksimps 
	mksimps (filter (fn (x,_) => x<>"All") mksimps_pairs);
fun Clarsimp_noAllAsm_tac n = clarsimp_tac (claset(), noAll_simpset()) n;


simpset_ref() := simpset() addsplits [option.split]
	addsplits [split_if_asm, option.split_asm]
        addloop ("split_all_tac", split_all_tac);

Delcongs[if_weak_cong, thm "option.weak_case_cong"];
AddIffs [length_Suc_conv];
Delsimprocs [record_simproc];

Goal "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),\
\ snd (snd (snd (snd p))))";
b y Auto_tac;
qed "surjective_pairing5";

Goal "[| fst s' = x';  !!x s. [| s' = (x,s);  x = x' |] ==> Q |] ==> Q";
by (REPEAT (resolve_tac (premises()@[surjective_pairing]) 1));
qed "fst_splitE";
AddSEs[fst_splitE];

Goal "(!x. (? b. x = f b) --> P x) = (!b. P (f b))";
by Auto_tac;
qed "All_Ex_refl_eq1";
Addsimps[All_Ex_refl_eq1];

(*unused*)
Goal "range f = {f True, f False}";
b y Auto_tac;
b y case_tac "xa" 1;
b y Auto_tac;
qed "range_bool_domain";

Goal "[| finite (Collect P); !y. P y --> finite (range (f y)) |] ==> \
\ finite {f y x |x y. P y}";
b y subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (%y. range (f y))" 1;
b y  Fast_tac 2;
b y etac ssubst 1;
b y etac finite_UN_I 1;
b y Fast_tac 1;
qed "finite_SetCompr2";


section "sum";

qed_goalw "the_Inl_Inl" thy [the_Inl_def] "the_Inl (Inl e) = e" (K [Auto_tac]);
qed_goalw "the_Inr_Inr" thy [the_Inr_def] "the_Inr (Inr e) = e" (K [Auto_tac]);
Addsimps[the_Inl_Inl,the_Inr_Inr];

qed_goalw "the_In1_In1" thy [the_In1_def] "the_In1 (In1 e) = e" (K [Auto_tac]);
qed_goalw "the_In2_In2" thy [the_In2_def] "the_In2 (In2 e) = e" (K [Auto_tac]);
qed_goalw "the_In3_In3" thy [the_In3_def] "the_In3 (In3 e) = e" (K [Auto_tac]);
Addsimps[the_In1_In1,the_In2_In2,the_In3_In3];

fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq])
 (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"];

section "unique";

Goal "(x, y) : set l --> x : fst `` set l";
by (induct_tac "l" 1);
by  Auto_tac;
qed_spec_mp "fst_in_set_lemma";

Goalw [unique_def, o_def] 
"unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))";
by (induct_tac "l" 1);
by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
qed_spec_mp "uniqueD";

Goalw [unique_def] "unique []";
by (Simp_tac 1);
qed "unique_Nil";

Goalw [unique_def] "unique ((x,y)#l) = (unique l \<and> (!y. (x,y) ~: set l))";
by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
qed "unique_Cons";

bind_thm ("unique_ConsI", conjI RS (unique_Cons RS iffD2));

Addsimps [unique_Nil,unique_Cons];

Goal "!!p. unique [p]";
b y Auto_tac;
qed "unique_single";
Addsimps[unique_single];

Goal "unique (x#xs) ==> unique xs";
by (pair_tac "x" 1);
be (unique_Cons RS iffD1 RS conjunct1) 1;
qed "unique_ConsD";

Goal "unique l' ==> unique l --> \
\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
by (induct_tac "l" 1);
by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
qed_spec_mp "unique_append";

Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
by (induct_tac "l" 1);
by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset() addsimps [inj_eq]));
qed_spec_mp "unique_map_inj";

Goal "unique l --> (k, x) : set l --> map_of l k = Some x";
b y induct_tac "l" 1;
b y  Auto_tac;
qed_spec_mp "map_of_SomeI";


section "lsplit";

Goalw [lsplit_def] "lsplit c (x#xs) = c x xs";
by (Simp_tac 1);
qed "lsplit";
AddIffs [lsplit];

Goal "lsplit P (x#xs) y z = P x xs y z";
by (Simp_tac 1);
qed "lsplit2";
AddSIs [lsplit2 RS iffD2]; AddSDs [lsplit2 RS iffD1];

(*unused*)
qed_goalw "lsplit_beta" thy [lsplit_def] 
	"lsplit c l = c (hd l) (tl l)" (K [Simp_tac 1]);