src/HOL/MicroJava/J/JBasis.ML
author nipkow
Thu Oct 12 18:38:23 2000 +0200 (2000-10-12)
changeset 10212 33fe2d701ddd
parent 10138 412a3ced6efd
child 10613 78b1d6c3ee9c
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOL/MicroJava/J/JBasis.ML
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 TU Muenchen
     5 *)
     6 
     7 val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
     8 
     9 Goalw [image_def]
    10 	"x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and>  x = f y";
    11 by(Auto_tac);
    12 qed "image_rev";
    13 
    14 fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
    15 
    16 val select_split = prove_goalw Product_Type.thy [split_def] 
    17 	"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
    18 	 
    19 
    20 val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
    21 	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
    22 val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
    23 	(fn _ => [Auto_tac]);
    24 val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
    25 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
    26 	rtac (split_beta RS subst) 1,
    27 	rtac (hd prems) 1]);
    28 val splitE2' = prove_goal Product_Type.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
    29 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
    30 	res_inst_tac [("P1","P")] (split_beta RS subst) 1,
    31 	rtac (hd prems) 1]);
    32 	
    33 
    34 fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
    35 
    36 val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q"
    37 	(fn prems => [rtac ballE 1, resolve_tac prems 1, 
    38 			eresolve_tac prems 1, eresolve_tac prems 1]);
    39 
    40 val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
    41 
    42 Addsimps [Let_def];
    43 
    44 (* To HOL.ML *)
    45 
    46 val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y" 
    47 	(fn prems => [
    48 	cut_facts_tac prems 1,
    49 	rtac some_equality 1,
    50 	 atac 1,
    51 	etac ex1E 1,
    52 	etac all_dupE 1,
    53 	fast_tac HOL_cs 1]);
    54 
    55 
    56 val ball_insert = prove_goalw equalities.thy [Ball_def]
    57 	"Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
    58 	fast_tac set_cs 1]);
    59 
    60 fun option_case_tac i = EVERY [
    61 	etac option_caseE i,
    62 	 rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
    63 	 rotate_tac ~2  i   , asm_full_simp_tac HOL_basic_ss i];
    64 
    65 val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
    66 		rotate_tac ~1,asm_full_simp_tac 
    67 	(simpset() delsimps [split_paired_All,split_paired_Ex])];
    68 
    69 Goal "{y. x = Some y} \\<subseteq> {the x}";
    70 by Auto_tac;
    71 qed "some_subset_the";
    72 
    73 fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
    74   asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
    75 
    76 val optionE = prove_goal thy 
    77        "[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" 
    78    (fn prems => [
    79 	case_tac "opt = None" 1,
    80 	 eresolve_tac prems 1,
    81 	not_None_tac 1,
    82 	eresolve_tac prems 1]);
    83 
    84 fun option_case_tac2 s i = EVERY [
    85 	 case_tac s i,
    86 	 rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
    87 	 rotate_tac ~1  i   , asm_full_simp_tac HOL_basic_ss i];
    88 
    89 val option_map_SomeD = prove_goalw thy [option_map_def]
    90 	"!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [
    91 	option_case_tac2 "x" 1,
    92 	 Auto_tac]);
    93 
    94 
    95 section "unique";
    96 
    97 Goal "(x, y) : set l --> x : fst `` set l";
    98 by (induct_tac "l" 1);
    99 by  Auto_tac;
   100 qed_spec_mp "fst_in_set_lemma";
   101 
   102 Goalw [unique_def] "unique []";
   103 by (Simp_tac 1);
   104 qed "unique_Nil";
   105 
   106 Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
   107 by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
   108 qed "unique_Cons";
   109 
   110 Addsimps [unique_Nil,unique_Cons];
   111 
   112 Goal "unique l' ==> unique l --> \
   113 \ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
   114 by (induct_tac "l" 1);
   115 by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
   116 qed_spec_mp "unique_append";
   117 
   118 Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
   119 by (induct_tac "l" 1);
   120 by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
   121 qed_spec_mp "unique_map_inj";
   122 
   123 Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
   124 by(etac unique_map_inj 1);
   125 by(rtac injI 1);
   126 by Auto_tac;
   127 qed "unique_map_Pair";
   128 
   129 Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N";
   130 by(rtac set_ext 1);
   131 by(simp_tac (simpset() addsimps image_def::premises()) 1);
   132 qed "image_cong";
   133 
   134 val split_Pair_eq = prove_goal Product_Type.thy 
   135 "!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
   136 	etac imageE 1,
   137 	split_all_tac 1,
   138 	auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]);
   139 
   140 
   141 (* More about Maps *)
   142 
   143 val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \
   144 \ t k = Some x |  t k = None \\<and>  s k = Some x" (fn prems => [
   145 	cut_facts_tac prems 1,
   146 	case_tac "\\<exists>x. t k = Some x" 1,
   147 	 etac exE 1,
   148 	 rotate_tac ~1 1,
   149 	 Asm_full_simp_tac 1,
   150 	asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
   151 	 rotate_tac ~1 1,
   152 	 Asm_full_simp_tac 1]);
   153 
   154 Addsimps [fun_upd_same, fun_upd_other];
   155 
   156 Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
   157 by(induct_tac "xys" 1);
   158  by(Simp_tac 1);
   159 by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
   160 qed_spec_mp "unique_map_of_Some_conv";
   161 
   162 val in_set_get = unique_map_of_Some_conv RS iffD2;
   163 val get_in_set = unique_map_of_Some_conv RS iffD1;
   164 
   165 Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
   166 by(induct_tac "l" 1);
   167 by(ALLGOALS Simp_tac);
   168 by Safe_tac;
   169 by Auto_tac;
   170 bind_thm("Ball_set_table",result() RS mp);
   171 
   172 val table_mono = prove_goal thy 
   173 "unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\
   174 \ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [
   175 	induct_tac "l" 1,
   176 	 Auto_tac,
   177  	 fast_tac (HOL_cs addSIs [in_set_get]) 1])
   178  RS mp RS mp RS spec RS spec RS mp;
   179 
   180 val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \
   181 \ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
   182 	induct_tac "t" 1,	
   183 	 ALLGOALS Simp_tac,
   184 	case_tac1 "k = fst a" 1,
   185 	 Auto_tac]) RS mp;
   186 val table_map_Some = prove_goal thy 
   187 "map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
   188 \map_of t (k, k') = Some x" (K [
   189 	induct_tac "t" 1,	
   190 	Auto_tac]) RS mp;
   191 
   192 
   193 val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \
   194 \ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [
   195 	induct_tac "t" 1,	
   196 	Auto_tac]) RS mp;
   197 val table_mapf_SomeD = prove_goal thy 
   198 "map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and>  z = f y)"(K [
   199 	induct_tac "t" 1,	
   200 	Auto_tac]) RS mp;
   201 
   202 val table_mapf_Some2 = prove_goal thy 
   203 "!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [
   204 	forward_tac [table_mapf_SomeD] 1,
   205 	Auto_tac,
   206 	rtac table_mapf_Some 1,
   207 	 atac 2,
   208 	Fast_tac 1]);
   209 
   210 val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
   211 
   212 Goal
   213 "map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
   214 by (induct_tac "xs" 1);
   215 auto();
   216 qed "map_of_map";
   217 
   218