Basis.ML
Back to theory Basis
infixr 0 y;
fun _ y t = by t;
val b=9999;
val HOL_cs1 = HOL_cs delrules [conjI, disjE, impCE];
val strip_tac1 = SELECT_GOAL (safe_tac HOL_cs1);
val image_rev = prove_goalw Set.thy [image_def]
"!!x. x : f``A ==> ? y. y : A & x = f y" (K [Auto_tac()]);
fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
val afst = asm_full_simp_tac;
val select_split = prove_goalw Prod.thy [split_def]
"(@(x,y). P x y) = (@xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
val split_beta = prove_goal Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
val split_beta2 = prove_goal Prod.thy "(%(x,y). P x y) (w,z) = P w z"
(fn _ => [Auto_tac ()]);
val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
rtac (split_beta RS subst) 1,
rtac (hd prems) 1]);
val splitE2' = prove_goal Prod.thy "[|((%(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
res_inst_tac [("P1","P")] (split_beta RS subst) 1,
rtac (hd prems) 1]);
goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
by (fast_tac (!claset addbefore split_all_tac) 1);
qed "split_paired_Ex";
Addsimps [split_paired_Ex];
val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (fn _ => [
rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
Addsimps [surj_pair];
fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
val BallE = prove_goal thy "[|Ball A P; x ~: A ==> Q; P x ==> Q |] ==> Q"
(fn prems => [rtac ballE 1, resolve_tac prems 1,
eresolve_tac prems 1, eresolve_tac prems 1]);
val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
Addsimps [first_def, secnd_def, third_def(*,split_beta*)];
Addsimps [surjective_pairing RS sym];
(* To HOL.ML *)
val Eps_eq = prove_goal HOL.thy "Eps (op = x) = x" (fn _ => [
rtac select_equality 1, Auto_tac ()]);
Addsimps [Eps_eq];
val ex1_Eps_eq = prove_goal HOL.thy "[|?!x. P x; P y|] ==> Eps P = y"
(fn prems => [
cut_facts_tac prems 1,
rtac select_equality 1,
atac 1,
etac ex1E 1,
etac all_dupE 1,
Fast_tac 1]);
(*
val TripleE = prove_goal thy "(!!x y z. t = (x, y, z) ==> Q) ==> Q" (fn prems => [
res_inst_tac [("x","fst t"), ("y","fst (snd t)"),
("z","snd (snd t)")] (hd prems) 1,
Simp_tac 1]);
fun triple_tac s = res_inst_tac [("t",s)] TripleE;
*)
val ball_insert = prove_goalw equalities.thy [Ball_def]
"Ball (insert x A) P = (P x & Ball A P)" (fn _ => [
fast_tac set_cs 1]);
val hol_ss = simpset_of "List" addsimps [ball_insert]
addsimps option.simps
addloop (split_tac [expand_option_case]);
val hol_cs = claset_of "Prod"
(*######List"*)
addSDs [ball_insert RS iffD1]
addSIs [ball_insert RS iffD2];
(*
val hol_css = (no_tac, safe_thin_ss hol_ss, hol_cs,
split_tac [expand_option_case]);
*)
val hol_css = HOL_css;
fun fast_tac2 css = fast_tac (op addss css);
val case_eqD7 = prove_goal thy
"(case y of None => None | Some x => Some (f x)) = Some z --> \
\ (? x. y = Some x & f x = z)"
(fn _ => [split_tac [expand_option_case] 1, Auto_tac()]) RS mp;
fun option_case_tac i = EVERY [
etac option_caseE i,
rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
rotate_tac ~2 i , asm_full_simp_tac HOL_basic_ss i];
(*
val not_NoneE = prove_goal thy "[|x ~= None; !!y. x = Some y ==> R|] ==> R"
(fn prems => [
cut_facts_tac prems 1,
dtac (Some_not_None RS iffD2) 1,
etac exE 1,
eresolve_tac prems 1]);
*)
val not_None_tac = EVERY' [dtac (Some_not_None RS iffD2),rotate_tac ~1,etac exE,
rotate_tac ~1,asm_full_simp_tac
(!simpset delsimps [split_paired_All,split_paired_Ex])];
fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
asm_full_simp_tac (!simpset delsimps [split_paired_All,split_paired_Ex])];
val optionE = prove_goal thy
"[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P" (fn prems => [
case_tac "opt = None" 1,
eresolve_tac prems 1,
not_None_tac 1,
eresolve_tac prems 1]);
fun option_case_tac2 s i = EVERY [
res_inst_tac [("opt",s)] optionE i,
rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i];
val option_map_SomeD = prove_goalw thy [option_map_def]
"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
option_case_tac2 "x" 1,
Auto_tac()]);
open Basis;
val the_atmost1 = prove_goalw thy [atmost1_def, s2o_def]
"[|atmost1 A; x:A|] ==> s2o A = Some x" (fn prems => [
cut_facts_tac prems 1,
subgoal_tac "?!x. x : A" 1,
stac ex1_Eps_eq 1,
atac 1,
atac 1,
Asm_simp_tac 1,
rtac ex1I 1,
atac 1,
fast_tac set_cs 1]);
val s2o_SomeD = prove_goalw thy [s2o_def] "s2o A = Some x --> x:A" (K [
rtac impI 1,
case_tac "?!x. x : A" 1,
ALLGOALS (rotate_tac ~1),
ALLGOALS Asm_full_simp_tac,
etac ex1E 1,
hyp_subst_tac 1,
etac selectI 1]) RS mp;
val uniqueD = prove_goalw thy [unique_def]
"[|unique l; (x,y):set l; (x',y'):set l; x = x'|] ==> y = y'" (fn prems => [
cut_facts_tac prems 1, Fast_tac 1]);
val unique_rev = prove_goalw thy [unique_def]
"[|unique l; (x,y):set l; (x',y'):set l; y ~= y'|] ==> x ~= x'"(fn prems =>[
cut_facts_tac prems 1,
Fast_tac 1]);
val unique_Nil = prove_goalw thy [unique_def] "unique []"
(fn _ => [Simp_tac 1]);
val unique_Cons = (prove_goalw thy [unique_def]
"unique l --> (!(x',y'):set l. x = x' --> y = y') --> unique ((x,y)#l)"
(fn _ =>[Auto_tac()]) RS mp RS mp);
Addsimps [unique_Nil,unique_Cons];
val unique_ConsD = prove_goalw thy [unique_def]"unique (x#xs) ==> unique xs"
(fn prems => [cut_facts_tac prems 1,
auto_tac(!claset delrules [ballE] addSEs [BallE],!simpset),
IF_UNSOLVED no_tac]);
val unique_Cons_eq = prove_goal thy
"unique ((x,y)#l) = (unique l & (!(x',y'):set l. x = x' --> y = y'))" (fn _ =>[
safe_tac HOL_cs,
etac unique_ConsD 1,
etac unique_Cons 2,
atac 2,
Auto_tac(),
etac uniqueD 1,
Auto_tac()]);
val unique_append = (prove_goal thy "unique l' ==> unique l --> \
\ (!(x,y):set l. !(x',y'):set l'. x = x' --> y = y') --> unique (l @ l')"
(fn prems => [
cut_facts_tac prems 1,
list.induct_tac "l" 1,
Asm_simp_tac 1,
pair_tac "a" 1,
strip_tac 1,
forward_tac [unique_ConsD] 1,
mp_tac 1,
Asm_full_simp_tac 1,
etac unique_Cons 1,
stac set_append 1,
safe_tac (!claset),
etac thin_rl 1,
etac uniqueD 1,
Auto_tac(),
etac BallE 1,
contr_tac 1,
Asm_full_simp_tac 1]) RS mp RS mp);
val unique_map' = (prove_goal thy
"!a b a' b' x y y'. f (a,b) = (x,y) --> f (a',b') = (x,y') --> a=a' ==> \
\ unique l --> unique (map f l)" (fn prems => [
cut_facts_tac prems 1,
list.induct_tac "l" 1,
Simp_tac 1,
safe_tac HOL_cs,
dtac unique_ConsD 1,
contr_tac 1,
pair_tac "a" 1,
Simp_tac 1,
res_inst_tac [("p","f (x, y)")] PairE 1,
Asm_simp_tac 1,
rtac unique_Cons 1,
atac 1,
Auto_tac(),
rotate_tac ~2 1,
dtac sym 1,
pair_tac "xa" 1,
subgoal_tac "x = xb" 1,
fast_tac HOL_cs 2,
dtac (unique_Cons_eq RS iffD1) 1,
step_tac set_cs2 1,
Auto_tac()]) RS mp);
val unique_map = prove_goal thy
"!!l. unique l ==> unique (map (%(k,x). (k, f x)) l)" (K [
rtac unique_map' 1, Auto_tac()]);
val unique_map_Pair = prove_goal thy
"!!l. unique l ==> unique (map (split (%k. Pair (k, C))) l)" (K [
rtac unique_map' 1, Auto_tac()]);
(*Addsimps [split_beta];*)
val prems= goal Basis.thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
b y rtac set_ext 1;
b y simp_tac (!simpset addsimps image_def::prems) 1;
qed "image_cong";
val split_Pair_eq = prove_goal List.thy
"!!X. ((x, y), z) : split (%x. Pair (x, Y)) `` A ==> y = Y" (K [
etac imageE 1,
split_all_tac 1,
Auto_tac()]);