1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/MicroJava/J/JBasis.ML Thu Nov 11 12:23:45 1999 +0100
1.3 @@ -0,0 +1,230 @@
1.4 +(* Title: HOL/MicroJava/J/JBasis.ML
1.5 + ID: $Id$
1.6 + Author: David von Oheimb
1.7 + Copyright 1999 TU Muenchen
1.8 +*)
1.9 +
1.10 +val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
1.11 +
1.12 +Goalw [image_def]
1.13 + "x \\<in> f``A \\<Longrightarrow> \\<exists>y. y \\<in> A \\<and> x = f y";
1.14 +by(Auto_tac);
1.15 +qed "image_rev";
1.16 +
1.17 +fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
1.18 +
1.19 +val select_split = prove_goalw Prod.thy [split_def]
1.20 + "(\\<epsilon>(x,y). P x y) = (\\<epsilon>xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
1.21 +
1.22 +
1.23 +val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
1.24 + (fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
1.25 +val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
1.26 + (fn _ => [Auto_tac]);
1.27 +val splitE2 = prove_goal Prod.thy "\\<lbrakk>Q (split P z); \\<And>x y. \\<lbrakk>z = (x, y); Q (P x y)\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
1.28 + REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
1.29 + rtac (split_beta RS subst) 1,
1.30 + rtac (hd prems) 1]);
1.31 +val splitE2' = prove_goal Prod.thy "\\<lbrakk>((\\<lambda>(x,y). P x y) z) w; \\<And>x y. \\<lbrakk>z = (x, y); (P x y) w\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
1.32 + REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
1.33 + res_inst_tac [("P1","P")] (split_beta RS subst) 1,
1.34 + rtac (hd prems) 1]);
1.35 +
1.36 +
1.37 +fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
1.38 +
1.39 +val BallE = prove_goal thy "\\<lbrakk>Ball A P; x \\<notin> A \\<Longrightarrow> Q; P x \\<Longrightarrow> Q \\<rbrakk> \\<Longrightarrow> Q"
1.40 + (fn prems => [rtac ballE 1, resolve_tac prems 1,
1.41 + eresolve_tac prems 1, eresolve_tac prems 1]);
1.42 +
1.43 +val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
1.44 +
1.45 +Addsimps [Let_def];
1.46 +Addsimps [surjective_pairing RS sym];
1.47 +
1.48 +(* To HOL.ML *)
1.49 +
1.50 +val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y"
1.51 + (fn prems => [
1.52 + cut_facts_tac prems 1,
1.53 + rtac select_equality 1,
1.54 + atac 1,
1.55 + etac ex1E 1,
1.56 + etac all_dupE 1,
1.57 + fast_tac HOL_cs 1]);
1.58 +
1.59 +
1.60 +val ball_insert = prove_goalw equalities.thy [Ball_def]
1.61 + "Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
1.62 + fast_tac set_cs 1]);
1.63 +
1.64 +fun option_case_tac i = EVERY [
1.65 + etac option_caseE i,
1.66 + rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
1.67 + rotate_tac ~2 i , asm_full_simp_tac HOL_basic_ss i];
1.68 +
1.69 +val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
1.70 + rotate_tac ~1,asm_full_simp_tac
1.71 + (simpset() delsimps [split_paired_All,split_paired_Ex])];
1.72 +
1.73 +fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
1.74 + asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
1.75 +
1.76 +val optionE = prove_goal thy
1.77 + "\\<lbrakk> opt = None \\<Longrightarrow> P; \\<And>x. opt = Some x \\<Longrightarrow> P \\<rbrakk> \\<Longrightarrow> P"
1.78 + (fn prems => [
1.79 + case_tac "opt = None" 1,
1.80 + eresolve_tac prems 1,
1.81 + not_None_tac 1,
1.82 + eresolve_tac prems 1]);
1.83 +
1.84 +fun option_case_tac2 s i = EVERY [
1.85 + exhaust_tac s i,
1.86 + rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
1.87 + rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i];
1.88 +
1.89 +val option_map_SomeD = prove_goalw thy [option_map_def]
1.90 + "\\<And>x. option_map f x = Some y \\<Longrightarrow> \\<exists>z. x = Some z \\<and> f z = y" (K [
1.91 + option_case_tac2 "x" 1,
1.92 + Auto_tac]);
1.93 +
1.94 +
1.95 +section "unique";
1.96 +
1.97 +Goal "(x, y) : set l --> x : fst `` set l";
1.98 +by (induct_tac "l" 1);
1.99 +by Auto_tac;
1.100 +qed_spec_mp "fst_in_set_lemma";
1.101 +
1.102 +Goalw [unique_def] "unique []";
1.103 +by (Simp_tac 1);
1.104 +qed "unique_Nil";
1.105 +
1.106 +Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
1.107 +by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
1.108 +qed "unique_Cons";
1.109 +
1.110 +Addsimps [unique_Nil,unique_Cons];
1.111 +
1.112 +Goal "unique l' ==> unique l --> \
1.113 +\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
1.114 +by (induct_tac "l" 1);
1.115 +by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
1.116 +qed_spec_mp "unique_append";
1.117 +
1.118 +Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
1.119 +by (induct_tac "l" 1);
1.120 +by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
1.121 +qed_spec_mp "unique_map_inj";
1.122 +
1.123 +Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
1.124 +by(etac unique_map_inj 1);
1.125 +by(rtac injI 1);
1.126 +by Auto_tac;
1.127 +qed "unique_map_Pair";
1.128 +
1.129 +Goal "\\<lbrakk>M = N; \\<And>x. x\\<in>N \\<Longrightarrow> f x = g x\\<rbrakk> \\<Longrightarrow> f``M = g``N";
1.130 +by(rtac set_ext 1);
1.131 +by(simp_tac (simpset() addsimps image_def::premises()) 1);
1.132 +qed "image_cong";
1.133 +
1.134 +val split_Pair_eq = prove_goal Prod.thy
1.135 +"\\<And>X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A \\<Longrightarrow> y = Y" (K [
1.136 + etac imageE 1,
1.137 + split_all_tac 1,
1.138 + auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
1.139 +
1.140 +
1.141 +section "list_all2";
1.142 +
1.143 +val list_all2_lengthD = prove_goalw thy [list_all2_def]
1.144 + "\\<And>X. list_all2 P as bs \\<Longrightarrow> length as = length bs" (K [Auto_tac]);
1.145 +
1.146 +val list_all2_Nil = prove_goalw thy [list_all2_def]
1.147 + "list_all2 P [] []" (K [Auto_tac]);
1.148 +Addsimps[list_all2_Nil];
1.149 +AddSIs[list_all2_Nil];
1.150 +
1.151 +val list_all2_Cons = prove_goalw thy [list_all2_def]
1.152 + "\\<And>X. list_all2 P (a#as) (b#bs) = (P a b \\<and> list_all2 P as bs)" (K [Auto_tac]);
1.153 +AddIffs[list_all2_Cons];
1.154 +
1.155 +
1.156 +(* More about Maps *)
1.157 +
1.158 +val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
1.159 +\ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [
1.160 + cut_facts_tac prems 1,
1.161 + case_tac "\\<exists>x. t k = Some x" 1,
1.162 + etac exE 1,
1.163 + rotate_tac ~1 1,
1.164 + Asm_full_simp_tac 1,
1.165 + asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
1.166 + rotate_tac ~1 1,
1.167 + Asm_full_simp_tac 1]);
1.168 +
1.169 +Addsimps [fun_upd_same, fun_upd_other];
1.170 +
1.171 +Goal "unique xys \\<longrightarrow> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
1.172 +by(induct_tac "xys" 1);
1.173 + by(Simp_tac 1);
1.174 +by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
1.175 +qed_spec_mp "unique_map_of_Some_conv";
1.176 +
1.177 +val in_set_get = unique_map_of_Some_conv RS iffD2;
1.178 +val get_in_set = unique_map_of_Some_conv RS iffD1;
1.179 +
1.180 +Goal "(\\<forall>(x,y)\\<in>set l. P x y) \\<longrightarrow> (\\<forall>x. \\<forall>y. map_of l x = Some y \\<longrightarrow> P x y)";
1.181 +by(induct_tac "l" 1);
1.182 +by(ALLGOALS Simp_tac);
1.183 +by Safe_tac;
1.184 +by Auto_tac;
1.185 +bind_thm("Ball_set_table",result() RS mp);
1.186 +
1.187 +val table_mono = prove_goal thy
1.188 +"unique l' \\<longrightarrow> (\\<forall>xy. (xy)\\<in>set l \\<longrightarrow> (xy)\\<in>set l') \\<longrightarrow>\
1.189 +\ (\\<forall>k y. map_of l k = Some y \\<longrightarrow> map_of l' k = Some y)" (fn _ => [
1.190 + induct_tac "l" 1,
1.191 + Auto_tac,
1.192 + fast_tac (HOL_cs addSIs [in_set_get]) 1])
1.193 + RS mp RS mp RS spec RS spec RS mp;
1.194 +
1.195 +val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) \\<longrightarrow> \
1.196 +\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
1.197 + induct_tac "t" 1,
1.198 + ALLGOALS Simp_tac,
1.199 + case_tac1 "k = fst a" 1,
1.200 + Auto_tac]) RS mp;
1.201 +val table_map_Some = prove_goal thy
1.202 +"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \\<longrightarrow> \
1.203 +\map_of t (k, k') = Some x" (K [
1.204 + induct_tac "t" 1,
1.205 + Auto_tac]) RS mp;
1.206 +
1.207 +
1.208 +val table_mapf_Some = prove_goal thy "\\<And>f. \\<forall>x y. f x = f y \\<longrightarrow> x = y \\<Longrightarrow> \
1.209 +\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) \\<longrightarrow> map_of t k = Some x" (K [
1.210 + induct_tac "t" 1,
1.211 + Auto_tac]) RS mp;
1.212 +val table_mapf_SomeD = prove_goal thy
1.213 +"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z \\<longrightarrow> (\\<exists>y. (k,y)\\<in>set t \\<and> z = f y)"(K [
1.214 + induct_tac "t" 1,
1.215 + Auto_tac]) RS mp;
1.216 +
1.217 +val table_mapf_Some2 = prove_goal thy
1.218 +"\\<And>k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) \\<Longrightarrow> C = D \\<and> map_of t k = Some x" (K [
1.219 + forward_tac [table_mapf_SomeD] 1,
1.220 + Auto_tac,
1.221 + rtac table_mapf_Some 1,
1.222 + atac 2,
1.223 + Fast_tac 1]);
1.224 +
1.225 +val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
1.226 +
1.227 +Goal
1.228 +"map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
1.229 +by (induct_tac "xs" 1);
1.230 +auto();
1.231 +qed "map_of_map";
1.232 +
1.233 +