File Table.ML

open Table;

bind_thm ("Ball_set_table", prove_goal thy
"(\<forall>(x,y)\<in>set l. P x y) \<longrightarrow> (\<forall>x. \<forall>y\<in>map_of l x: P x y)" 
	(K [induct_tac "l" 1, ALLGOALS Simp_tac, Fast_tac 1]) RS mp);

bind_thm ("Ball_set_tableD", Ball_set_table RS spec RS bspec);


section "overrides";

qed_goalw "overrides_Some_iff" thy [overrides_def] 
	"\<And>X. (x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)" (K [Auto_tac]);

val overrides_SomeD = standard (overrides_Some_iff RS iffD1);
AddSDs[overrides_SomeD];


section "hiding_entails";

qed_goalw "hiding_entailsD" thy [hiding_entails_def]
 "\<And>X. \<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"
	(K [Fast_tac 1]);

qed_goalw "empty_hiding_entails" thy [hiding_entails_def]
 "empty hiding s entails R" (K [Simp_tac 1]);

qed_goalw "hiding_empty_entails" thy [hiding_entails_def]
 "t hiding empty entails R" (K [Simp_tac 1]);
Addsimps [empty_hiding_entails, hiding_empty_entails];

qed_goalw "hidings_entailsD" thy [hidings_entails_def]
 "\<And>X. \<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
	(K [Fast_tac 1]);


section "map_of / table_of";

val weak_in_set_get = weak_map_of_SomeI;
val in_set_get = map_of_SomeI;
val get_in_set = map_of_SomeD;
AddEs [get_in_set];

qed_goal "set_get_eq" thy 
 "\<And>X. unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)" (K [
	Safe_tac,
	 fast_tac (claset() addSDs [in_set_get]) 1,
	Auto_tac]);

(* unused 
qed_goal "table_of_mono" thy 
"\<And>X. \<lbrakk>unique l'; \<forall>x y. (x,y)\<in>set l \<longrightarrow> (x,y)\<in>set l'; table_of l k = Some y\<rbrakk> \<Longrightarrow> \
\ table_of l' k = Some y" (K [
	etac in_set_get 1,
	dtac get_in_set 1,
	Fast_tac 1]);
*)

Goal "inj (\<lambda>k. (k, C))";
b y rtac injI 1;
b y Auto_tac;
qed "inj_Pair_const2";
bind_thm ("table_of_map2_SomeI", inj_Pair_const2 RS map_of_mapk_SomeI);

Goal "table_of t k = Some x \<longrightarrow> \
\  table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)";
b y induct_tac "t" 1;
b y  Auto_tac;
qed_spec_mp "table_of_map_SomeI";

Goal "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow> \
\table_of t (k, k') = Some x";
b y induct_tac "t" 1;
b y  Auto_tac;
qed_spec_mp "table_of_remap_SomeD";

Goal "\<And>f. \<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> \
\ table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x";
b y induct_tac "t" 1;
b y  Auto_tac;
qed_spec_mp "table_of_mapf_Some";

Goal
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)";
b y induct_tac "t" 1;
b y  Auto_tac;
qed_spec_mp "table_of_mapf_SomeD";
AddSDs [table_of_mapf_SomeD];

Goal  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x";
b y induct_tac "t" 1;
b y  Auto_tac;
qed_spec_mp "table_of_mapkey_SomeD";
AddSDs [table_of_mapkey_SomeD];

Goal "table_of (xs@ys) k = Some z = (table_of xs k = Some z \<or> \
\ (table_of xs k = None \<and> table_of ys k = Some z))";
b y stac (map_of_override RS sym) 1;
b y rtac override_Some_iff 1;
qed "table_append_Some_iff";


Goal "table_of (filter P xs) k = Some z --> unique xs --> table_of xs k = Some z";
b y Simp_tac 1;
by (induct_tac "xs" 1);
by  (auto_tac (claset() addIs [get_in_set],simpset()));
qed_spec_mp "table_of_filter_unique_SomeD";


section "Un_tables";

qed_goalw "Un_tablesI" thy [Un_tables_def] 
  "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k" (K [Auto_tac]);

AddIs [Un_tablesI];

qed_goalw "Un_tablesD" thy [Un_tables_def] 
  "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k" (K [Auto_tac]);

AddSDs [Un_tablesD];