# HG changeset patch
# User wenzelm
# Date 1329863136 -3600
# Node ID a935175fe6b61cd9105413d0ed0fd38f5bd37d85
# Parent  926957a621dd101ed82fd1720cd00507642093f0
tuned proofs;

diff -r 926957a621dd -r a935175fe6b6 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Tue Feb 21 23:24:49 2012 +0100
+++ b/src/HOL/Bali/Table.thy	Tue Feb 21 23:25:36 2012 +0100
@@ -45,11 +45,12 @@
   (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b"
 
 (* ### To map *)
-lemma map_add_find_left[simp]:
-"n k = None \<Longrightarrow> (m ++ n) k = m k"
-by (simp add: map_add_def)
+lemma map_add_find_left[simp]: "n k = None \<Longrightarrow> (m ++ n) k = m k"
+  by (simp add: map_add_def)
+
 
 section {* Conditional Override *}
+
 definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where
 
 --{* when merging tables old and new, only override an entry of table old when  
@@ -65,27 +66,27 @@
                                          else Some old_val))))"
 
 lemma cond_override_empty1[simp]: "cond_override c empty t = t"
-by (simp add: cond_override_def fun_eq_iff)
+  by (simp add: cond_override_def fun_eq_iff)
 
 lemma cond_override_empty2[simp]: "cond_override c t empty = t"
-by (simp add: cond_override_def fun_eq_iff)
+  by (simp add: cond_override_def fun_eq_iff)
 
 lemma cond_override_None[simp]:
- "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
-by (simp add: cond_override_def)
+  "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
+  by (simp add: cond_override_def)
 
 lemma cond_override_override:
- "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
-  \<Longrightarrow> (cond_override C old new) k = Some nv"
-by (auto simp add: cond_override_def)
+  "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
+    \<Longrightarrow> (cond_override C old new) k = Some nv"
+  by (auto simp add: cond_override_def)
 
 lemma cond_override_noOverride:
- "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
-  \<Longrightarrow> (cond_override C old new) k = Some ov"
-by (auto simp add: cond_override_def)
+  "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
+    \<Longrightarrow> (cond_override C old new) k = Some ov"
+  by (auto simp add: cond_override_def)
 
 lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
-by (auto simp add: cond_override_def dom_def)
+  by (auto simp add: cond_override_def dom_def)
 
 lemma finite_dom_cond_override:
  "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
@@ -93,13 +94,14 @@
 apply (rule dom_cond_override)
 by (rule finite_UnI)
 
+
 section {* Filter on Tables *}
 
-definition
-  filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
-  "filter_tab c t = (\<lambda>k. (case t k of 
-                           None   \<Rightarrow> None
-                         | Some x \<Rightarrow> if c k x then Some x else None))"
+definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
+  where
+    "filter_tab c t = (\<lambda>k. (case t k of 
+                             None   \<Rightarrow> None
+                           | Some x \<Rightarrow> if c k x then Some x else None))"
 
 lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
 by (simp add: filter_tab_def empty_def)
@@ -165,8 +167,7 @@
 "\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
   \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
  \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
-apply (force simp add: filter_tab_def)
-done
+by (force simp add: filter_tab_def)
 
 lemma cond_override_filter: 
   "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
@@ -178,7 +179,7 @@
 by (auto simp add: fun_eq_iff cond_override_def filter_tab_def )
 
 
-section {* Misc. *}
+section {* Misc *}
 
 lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y"
 apply (erule rev_mp)
@@ -210,62 +211,46 @@
 
 lemma table_of_mapconst_SomeI:
   "\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow>
-   table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"
-apply (induct t)
-apply auto
-done
+    table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"
+  by (induct t) auto
 
 lemma table_of_mapconst_NoneI:
   "\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow>
-   table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"
-apply (induct t)
-apply auto
-done
+    table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"
+  by (induct t) auto
 
 lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI]
 
-lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
+lemma table_of_map_SomeI: "table_of t k = Some x \<Longrightarrow>
    table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
-apply (induct_tac "t")
-apply auto
-done
+  by (induct t) auto
 
-lemma table_of_remap_SomeD [rule_format (no_asm)]: 
-  "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow>
-  table_of t (k, k') = Some x"
-apply (induct_tac "t")
-apply  auto
-done
+lemma table_of_remap_SomeD:
+  "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<Longrightarrow>
+    table_of t (k, k') = Some x"
+  by (induct t) auto
 
-lemma table_of_mapf_Some [rule_format (no_asm)]: "\<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"
-apply (induct_tac "t")
-apply  auto
-done
+lemma table_of_mapf_Some:
+  "\<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"
+  by (induct t) auto
 
-lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]: 
-"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"
-apply (induct_tac "t")
-apply  auto
-done
+lemma table_of_mapf_SomeD [dest!]:
+  "table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<Longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"
+  by (induct t) auto
 
-lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]: 
-"table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<longrightarrow> (table_of t k = None)"
-apply (induct_tac "t")
-apply auto
-done
+lemma table_of_mapf_NoneD [dest!]:
+  "table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<Longrightarrow> (table_of t k = None)"
+  by (induct t) auto
 
-lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]: 
-  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x"
-apply (induct_tac "t")
-apply  auto
-done
-lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]: 
-  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x 
-   \<longrightarrow> C = snd ek \<and> table_of t (fst ek) = Some x"
-apply (induct_tac "t")
-apply  auto
-done
+lemma table_of_mapkey_SomeD [dest!]:
+  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<Longrightarrow> C = D \<and> table_of t k = Some x"
+  by (induct t) auto
+
+lemma table_of_mapkey_SomeD2 [dest!]:
+  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x \<Longrightarrow>
+    C = snd ek \<and> table_of t (fst ek) = Some x"
+  by (induct t) auto
 
 lemma table_append_Some_iff: "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))"
@@ -275,16 +260,14 @@
 
 lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
   "table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"
-apply (induct xs)
-apply (auto del: map_of_SomeD intro!: map_of_SomeD)
-done
+  by (induct xs) (auto del: map_of_SomeD intro!: map_of_SomeD)
 
 
 definition Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
   where "Un_tables ts = (\<lambda>k. \<Union>t\<in>ts. t k)"
 
-definition
-  overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"  (infixl "\<oplus>\<oplus>" 100)
+definition overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"
+    (infixl "\<oplus>\<oplus>" 100)
   where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)"
 
 definition
@@ -305,59 +288,52 @@
                           ("_ hiding _ under _ entails _"  20)
   where "(t hiding  s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)"
 
+
 section "Untables"
 
-lemma Un_tablesI [intro]:  "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k"
-apply (simp add: Un_tables_def)
-apply auto
-done
+lemma Un_tablesI [intro]:  "t \<in> ts \<Longrightarrow> x \<in> t k \<Longrightarrow> x \<in> Un_tables ts k"
+  by (auto simp add: Un_tables_def)
 
-lemma Un_tablesD [dest!]: "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"
-apply (simp add: Un_tables_def)
-apply auto
-done
+lemma Un_tablesD [dest!]: "x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"
+  by (auto simp add: Un_tables_def)
 
 lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"
-apply (unfold Un_tables_def)
-apply (simp (no_asm))
-done
+  by (simp add: Un_tables_def)
 
 
 section "overrides"
 
 lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
-apply (unfold overrides_t_def)
-apply (simp (no_asm))
-done
+  by (simp add: overrides_t_def)
+
 lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"
-apply (unfold overrides_t_def)
-apply (simp (no_asm))
-done
+  by (simp add: overrides_t_def)
 
 lemma overrides_t_Some_iff: 
- "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
-by (simp add: overrides_t_def)
+  "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
+  by (simp add: overrides_t_def)
 
 lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]
 
 lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k"  
-by (simp add: overrides_t_def)
+  by (simp add: overrides_t_def)
 
 lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k"  
-by (simp add: overrides_t_def)
+  by (simp add: overrides_t_def)
+
 
 section "hiding entails"
 
 lemma hiding_entailsD: 
-  "\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"
-by (simp add: hiding_entails_def)
+  "t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y"
+  by (simp add: hiding_entails_def)
 
-lemma empty_hiding_entails: "empty hiding s entails R"
-by (simp add: hiding_entails_def)
+lemma empty_hiding_entails [simp]: "empty hiding s entails R"
+  by (simp add: hiding_entails_def)
 
-lemma hiding_empty_entails: "t hiding empty entails R"
-by (simp add: hiding_entails_def)
-declare empty_hiding_entails [simp] hiding_empty_entails [simp]
+lemma hiding_empty_entails [simp]: "t hiding empty entails R"
+  by (simp add: hiding_entails_def)
+
 
 section "cond hiding entails"
 
@@ -374,16 +350,14 @@
 lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
 by (simp add: hidings_entails_def)
 
-lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R"
+lemma hidings_empty_entails [intro!]: "t hidings (\<lambda>k. {}) entails R"
 apply (unfold hidings_entails_def)
 apply (simp (no_asm))
 done
 
-lemma empty_hidings_entails: 
+lemma empty_hidings_entails [intro!]:
   "(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)
 by (simp (no_asm))
-declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]
-
 
 
 (*###TO Map?*)
@@ -429,7 +403,7 @@
 done
 declare fun_upd_apply [simp]
 
-lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
+lemma atleast_free_SucD: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
 apply auto
 apply (case_tac "aa = a")
 apply auto
@@ -438,4 +412,5 @@
 done
 
 declare atleast_free_Suc [simp del]
+
 end