# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1395414479 0
# Node ID 38cef5407d823ab72a197aaff51b4c966a2a8dfb
# Parent  6c722e960f2ed86aa066cd0e226b51a25942bf59
updated various files to Isabelle-2013-2

diff -r 6c722e960f2e -r 38cef5407d82 ROOT
--- a/ROOT	Fri Mar 21 13:49:20 2014 +0000
+++ b/ROOT	Fri Mar 21 15:07:59 2014 +0000
@@ -9,3 +9,7 @@
 session "Hoare_abc" in "thys" = "Hoare_tm" +
   theories
      Hoare_abc
+
+session "TM" in "thys" = Hoare_abc +
+  theories 
+    TM_Assemble
\ No newline at end of file
diff -r 6c722e960f2e -r 38cef5407d82 thys/AList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/AList.thy	Fri Mar 21 15:07:59 2014 +0000
@@ -0,0 +1,698 @@
+(*  Title:      HOL/Library/AList.thy
+    Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
+*)
+
+header {* Implementation of Association Lists *}
+
+theory AList
+imports Main
+begin
+
+text {*
+  The operations preserve distinctness of keys and 
+  function @{term "clearjunk"} distributes over them. Since 
+  @{term clearjunk} enforces distinctness of keys it can be used
+  to establish the invariant, e.g. for inductive proofs.
+*}
+
+subsection {* @{text update} and @{text updates} *}
+
+primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
+    "update k v [] = [(k, v)]"
+  | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
+
+lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
+  by (induct al) (auto simp add: fun_eq_iff)
+
+corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
+  by (simp add: update_conv')
+
+lemma dom_update: "fst ` set (update k v al) = {k} \<union> fst ` set al"
+  by (induct al) auto
+
+lemma update_keys:
+  "map fst (update k v al) =
+    (if k \<in> set (map fst al) then map fst al else map fst al @ [k])"
+  by (induct al) simp_all
+
+lemma distinct_update:
+  assumes "distinct (map fst al)" 
+  shows "distinct (map fst (update k v al))"
+  using assms by (simp add: update_keys)
+
+lemma update_filter: 
+  "a\<noteq>k \<Longrightarrow> update k v [q\<leftarrow>ps . fst q \<noteq> a] = [q\<leftarrow>update k v ps . fst q \<noteq> a]"
+  by (induct ps) auto
+
+lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
+  by (induct al) auto
+
+lemma update_nonempty [simp]: "update k v al \<noteq> []"
+  by (induct al) auto
+
+lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
+proof (induct al arbitrary: al') 
+  case Nil thus ?case 
+    by (cases al') (auto split: split_if_asm)
+next
+  case Cons thus ?case
+    by (cases al') (auto split: split_if_asm)
+qed
+
+lemma update_last [simp]: "update k v (update k v' al) = update k v al"
+  by (induct al) auto
+
+text {* Note that the lists are not necessarily the same:
+        @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and 
+        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
+lemma update_swap: "k\<noteq>k' 
+  \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
+  by (simp add: update_conv' fun_eq_iff)
+
+lemma update_Some_unfold: 
+  "map_of (update k v al) x = Some y \<longleftrightarrow>
+    x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
+  by (simp add: update_conv' map_upd_Some_unfold)
+
+lemma image_update [simp]:
+  "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
+  by (simp add: update_conv')
+
+definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
+  "updates ks vs = fold (prod_case update) (zip ks vs)"
+
+lemma updates_simps [simp]:
+  "updates [] vs ps = ps"
+  "updates ks [] ps = ps"
+  "updates (k#ks) (v#vs) ps = updates ks vs (update k v ps)"
+  by (simp_all add: updates_def)
+
+lemma updates_key_simp [simp]:
+  "updates (k # ks) vs ps =
+    (case vs of [] \<Rightarrow> ps | v # vs \<Rightarrow> updates ks vs (update k v ps))"
+  by (cases vs) simp_all
+
+lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
+proof -
+  have "map_of \<circ> fold (prod_case update) (zip ks vs) =
+    fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
+    by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
+  then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def)
+qed
+
+lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
+  by (simp add: updates_conv')
+
+lemma distinct_updates:
+  assumes "distinct (map fst al)"
+  shows "distinct (map fst (updates ks vs al))"
+proof -
+  have "distinct (fold
+       (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
+       (zip ks vs) (map fst al))"
+    by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
+  moreover have "map fst \<circ> fold (prod_case update) (zip ks vs) =
+    fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
+    by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
+  ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
+qed
+
+lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
+  updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
+  by (induct ks arbitrary: vs al) (auto split: list.splits)
+
+lemma updates_list_update_drop[simp]:
+ "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
+   \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
+  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
+
+lemma update_updates_conv_if: "
+ map_of (updates xs ys (update x y al)) =
+ map_of (if x \<in>  set(take (length ys) xs) then updates xs ys al
+                                  else (update x y (updates xs ys al)))"
+  by (simp add: updates_conv' update_conv' map_upd_upds_conv_if)
+
+lemma updates_twist [simp]:
+ "k \<notin> set ks \<Longrightarrow> 
+  map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
+  by (simp add: updates_conv' update_conv')
+
+lemma updates_apply_notin[simp]:
+ "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
+  by (simp add: updates_conv)
+
+lemma updates_append_drop[simp]:
+  "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
+  by (induct xs arbitrary: ys al) (auto split: list.splits)
+
+lemma updates_append2_drop[simp]:
+  "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
+  by (induct xs arbitrary: ys al) (auto split: list.splits)
+
+
+subsection {* @{text delete} *}
+
+definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
+  delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
+
+lemma delete_simps [simp]:
+  "delete k [] = []"
+  "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
+  by (auto simp add: delete_eq)
+
+lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
+  by (induct al) (auto simp add: fun_eq_iff)
+
+corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
+  by (simp add: delete_conv')
+
+lemma delete_keys:
+  "map fst (delete k al) = removeAll k (map fst al)"
+  by (simp add: delete_eq removeAll_filter_not_eq filter_map split_def comp_def)
+
+lemma distinct_delete:
+  assumes "distinct (map fst al)" 
+  shows "distinct (map fst (delete k al))"
+  using assms by (simp add: delete_keys distinct_removeAll)
+
+lemma delete_id [simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
+  by (auto simp add: image_iff delete_eq filter_id_conv)
+
+lemma delete_idem: "delete k (delete k al) = delete k al"
+  by (simp add: delete_eq)
+
+lemma map_of_delete [simp]:
+    "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
+  by (simp add: delete_conv')
+
+lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
+  by (auto simp add: delete_eq)
+
+lemma dom_delete_subset: "fst ` set (delete k al) \<subseteq> fst ` set al"
+  by (auto simp add: delete_eq)
+
+lemma delete_update_same:
+  "delete k (update k v al) = delete k al"
+  by (induct al) simp_all
+
+lemma delete_update:
+  "k \<noteq> l \<Longrightarrow> delete l (update k v al) = update k v (delete l al)"
+  by (induct al) simp_all
+
+lemma delete_twist: "delete x (delete y al) = delete y (delete x al)"
+  by (simp add: delete_eq conj_commute)
+
+lemma length_delete_le: "length (delete k al) \<le> length al"
+  by (simp add: delete_eq)
+
+
+subsection {* @{text restrict} *}
+
+definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
+  restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
+
+lemma restr_simps [simp]:
+  "restrict A [] = []"
+  "restrict A (p#ps) = (if fst p \<in> A then p # restrict A ps else restrict A ps)"
+  by (auto simp add: restrict_eq)
+
+lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
+proof
+  fix k
+  show "map_of (restrict A al) k = ((map_of al)|` A) k"
+    by (induct al) (simp, cases "k \<in> A", auto)
+qed
+
+corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
+  by (simp add: restr_conv')
+
+lemma distinct_restr:
+  "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
+  by (induct al) (auto simp add: restrict_eq)
+
+lemma restr_empty [simp]: 
+  "restrict {} al = []" 
+  "restrict A [] = []"
+  by (induct al) (auto simp add: restrict_eq)
+
+lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
+  by (simp add: restr_conv')
+
+lemma restr_out [simp]: "x \<notin> A \<Longrightarrow> map_of (restrict A al) x = None"
+  by (simp add: restr_conv')
+
+lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
+  by (induct al) (auto simp add: restrict_eq)
+
+lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
+  by (induct al) (auto simp add: restrict_eq)
+
+lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
+  by (induct al) (auto simp add: restrict_eq)
+
+lemma restr_update[simp]:
+ "map_of (restrict D (update x y al)) = 
+  map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
+  by (simp add: restr_conv' update_conv')
+
+lemma restr_delete [simp]:
+  "(delete x (restrict D al)) = 
+    (if x \<in> D then restrict (D - {x}) al else restrict D al)"
+apply (simp add: delete_eq restrict_eq)
+apply (auto simp add: split_def)
+proof -
+  have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y" by auto
+  then show "[p \<leftarrow> al. fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al. fst p \<in> D \<and> fst p \<noteq> x]"
+    by simp
+  assume "x \<notin> D"
+  then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" by auto
+  then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
+    by simp
+qed
+
+lemma update_restr:
+ "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
+  by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
+
+lemma update_restr_conv [simp]:
+ "x \<in> D \<Longrightarrow> 
+ map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
+  by (simp add: update_conv' restr_conv')
+
+lemma restr_updates [simp]: "
+ \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
+ \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
+     map_of (updates xs ys (restrict (D - set xs) al))"
+  by (simp add: updates_conv' restr_conv')
+
+lemma restr_delete_twist: "(restrict A (delete a ps)) = delete a (restrict A ps)"
+  by (induct ps) auto
+
+
+subsection {* @{text clearjunk} *}
+
+function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
+    "clearjunk [] = []"  
+  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
+  by pat_completeness auto
+termination by (relation "measure length")
+  (simp_all add: less_Suc_eq_le length_delete_le)
+
+lemma map_of_clearjunk:
+  "map_of (clearjunk al) = map_of al"
+  by (induct al rule: clearjunk.induct)
+    (simp_all add: fun_eq_iff)
+
+lemma clearjunk_keys_set:
+  "set (map fst (clearjunk al)) = set (map fst al)"
+  by (induct al rule: clearjunk.induct)
+    (simp_all add: delete_keys)
+
+lemma dom_clearjunk:
+  "fst ` set (clearjunk al) = fst ` set al"
+  using clearjunk_keys_set by simp
+
+lemma distinct_clearjunk [simp]:
+  "distinct (map fst (clearjunk al))"
+  by (induct al rule: clearjunk.induct)
+    (simp_all del: set_map add: clearjunk_keys_set delete_keys)
+
+lemma ran_clearjunk:
+  "ran (map_of (clearjunk al)) = ran (map_of al)"
+  by (simp add: map_of_clearjunk)
+
+lemma ran_map_of:
+  "ran (map_of al) = snd ` set (clearjunk al)"
+proof -
+  have "ran (map_of al) = ran (map_of (clearjunk al))"
+    by (simp add: ran_clearjunk)
+  also have "\<dots> = snd ` set (clearjunk al)"
+    by (simp add: ran_distinct)
+  finally show ?thesis .
+qed
+
+lemma clearjunk_update:
+  "clearjunk (update k v al) = update k v (clearjunk al)"
+  by (induct al rule: clearjunk.induct)
+    (simp_all add: delete_update)
+
+lemma clearjunk_updates:
+  "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
+proof -
+  have "clearjunk \<circ> fold (prod_case update) (zip ks vs) =
+    fold (prod_case update) (zip ks vs) \<circ> clearjunk"
+    by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
+  then show ?thesis by (simp add: updates_def fun_eq_iff)
+qed
+
+lemma clearjunk_delete:
+  "clearjunk (delete x al) = delete x (clearjunk al)"
+  by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
+
+lemma clearjunk_restrict:
+ "clearjunk (restrict A al) = restrict A (clearjunk al)"
+  by (induct al rule: clearjunk.induct) (auto simp add: restr_delete_twist)
+
+lemma distinct_clearjunk_id [simp]:
+  "distinct (map fst al) \<Longrightarrow> clearjunk al = al"
+  by (induct al rule: clearjunk.induct) auto
+
+lemma clearjunk_idem:
+  "clearjunk (clearjunk al) = clearjunk al"
+  by simp
+
+lemma length_clearjunk:
+  "length (clearjunk al) \<le> length al"
+proof (induct al rule: clearjunk.induct [case_names Nil Cons])
+  case Nil then show ?case by simp
+next
+  case (Cons kv al)
+  moreover have "length (delete (fst kv) al) \<le> length al" by (fact length_delete_le)
+  ultimately have "length (clearjunk (delete (fst kv) al)) \<le> length al" by (rule order_trans)
+  then show ?case by simp
+qed
+
+lemma delete_map:
+  assumes "\<And>kv. fst (f kv) = fst kv"
+  shows "delete k (map f ps) = map f (delete k ps)"
+  by (simp add: delete_eq filter_map comp_def split_def assms)
+
+lemma clearjunk_map:
+  assumes "\<And>kv. fst (f kv) = fst kv"
+  shows "clearjunk (map f ps) = map f (clearjunk ps)"
+  by (induct ps rule: clearjunk.induct [case_names Nil Cons])
+    (simp_all add: clearjunk_delete delete_map assms)
+
+
+subsection {* @{text map_ran} *}
+
+definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
+  "map_ran f = map (\<lambda>(k, v). (k, f k v))"
+
+lemma map_ran_simps [simp]:
+  "map_ran f [] = []"
+  "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps"
+  by (simp_all add: map_ran_def)
+
+lemma dom_map_ran:
+  "fst ` set (map_ran f al) = fst ` set al"
+  by (simp add: map_ran_def image_image split_def)
+  
+lemma map_ran_conv:
+  "map_of (map_ran f al) k = Option.map (f k) (map_of al k)"
+  by (induct al) auto
+
+lemma distinct_map_ran:
+  "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
+  by (simp add: map_ran_def split_def comp_def)
+
+lemma map_ran_filter:
+  "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
+  by (simp add: map_ran_def filter_map split_def comp_def)
+
+lemma clearjunk_map_ran:
+  "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
+  by (simp add: map_ran_def split_def clearjunk_map)
+
+
+subsection {* @{text merge} *}
+
+definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
+  "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
+
+lemma merge_simps [simp]:
+  "merge qs [] = qs"
+  "merge qs (p#ps) = update (fst p) (snd p) (merge qs ps)"
+  by (simp_all add: merge_def split_def)
+
+lemma merge_updates:
+  "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
+  by (simp add: merge_def updates_def foldr_conv_fold zip_rev zip_map_fst_snd)
+
+lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
+  by (induct ys arbitrary: xs) (auto simp add: dom_update)
+
+lemma distinct_merge:
+  assumes "distinct (map fst xs)"
+  shows "distinct (map fst (merge xs ys))"
+using assms by (simp add: merge_updates distinct_updates)
+
+lemma clearjunk_merge:
+  "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
+  by (simp add: merge_updates clearjunk_updates)
+
+lemma merge_conv':
+  "map_of (merge xs ys) = map_of xs ++ map_of ys"
+proof -
+  have "map_of \<circ> fold (prod_case update) (rev ys) =
+    fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
+    by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
+  then show ?thesis
+    by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff)
+qed
+
+corollary merge_conv:
+  "map_of (merge xs ys) k = (map_of xs ++ map_of ys) k"
+  by (simp add: merge_conv')
+
+lemma merge_empty: "map_of (merge [] ys) = map_of ys"
+  by (simp add: merge_conv')
+
+lemma merge_assoc[simp]: "map_of (merge m1 (merge m2 m3)) = 
+                           map_of (merge (merge m1 m2) m3)"
+  by (simp add: merge_conv')
+
+lemma merge_Some_iff: 
+ "(map_of (merge m n) k = Some x) = 
+  (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
+  by (simp add: merge_conv' map_add_Some_iff)
+
+lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
+
+lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
+  by (simp add: merge_conv')
+
+lemma merge_None [iff]: 
+  "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
+  by (simp add: merge_conv')
+
+lemma merge_upd[simp]: 
+  "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
+  by (simp add: update_conv' merge_conv')
+
+lemma merge_updatess[simp]: 
+  "map_of (merge m (updates xs ys n)) = map_of (updates xs ys (merge m n))"
+  by (simp add: updates_conv' merge_conv')
+
+lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
+  by (simp add: merge_conv')
+
+
+subsection {* @{text compose} *}
+
+function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list" where
+    "compose [] ys = []"
+  | "compose (x#xs) ys = (case map_of ys (snd x)
+       of None \<Rightarrow> compose (delete (fst x) xs) ys
+        | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
+  by pat_completeness auto
+termination by (relation "measure (length \<circ> fst)")
+  (simp_all add: less_Suc_eq_le length_delete_le)
+
+lemma compose_first_None [simp]: 
+  assumes "map_of xs k = None" 
+  shows "map_of (compose xs ys) k = None"
+using assms by (induct xs ys rule: compose.induct)
+  (auto split: option.splits split_if_asm)
+
+lemma compose_conv: 
+  shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
+proof (induct xs ys rule: compose.induct)
+  case 1 then show ?case by simp
+next
+  case (2 x xs ys) show ?case
+  proof (cases "map_of ys (snd x)")
+    case None with 2
+    have hyp: "map_of (compose (delete (fst x) xs) ys) k =
+               (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k"
+      by simp
+    show ?thesis
+    proof (cases "fst x = k")
+      case True
+      from True delete_notin_dom [of k xs]
+      have "map_of (delete (fst x) xs) k = None"
+        by (simp add: map_of_eq_None_iff)
+      with hyp show ?thesis
+        using True None
+        by simp
+    next
+      case False
+      from False have "map_of (delete (fst x) xs) k = map_of xs k"
+        by simp
+      with hyp show ?thesis
+        using False None
+        by (simp add: map_comp_def)
+    qed
+  next
+    case (Some v)
+    with 2
+    have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
+      by simp
+    with Some show ?thesis
+      by (auto simp add: map_comp_def)
+  qed
+qed
+   
+lemma compose_conv': 
+  shows "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
+  by (rule ext) (rule compose_conv)
+
+lemma compose_first_Some [simp]:
+  assumes "map_of xs k = Some v" 
+  shows "map_of (compose xs ys) k = map_of ys v"
+using assms by (simp add: compose_conv)
+
+lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
+proof (induct xs ys rule: compose.induct)
+  case 1 thus ?case by simp
+next
+  case (2 x xs ys)
+  show ?case
+  proof (cases "map_of ys (snd x)")
+    case None
+    with "2.hyps"
+    have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
+      by simp
+    also
+    have "\<dots> \<subseteq> fst ` set xs"
+      by (rule dom_delete_subset)
+    finally show ?thesis
+      using None
+      by auto
+  next
+    case (Some v)
+    with "2.hyps"
+    have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
+      by simp
+    with Some show ?thesis
+      by auto
+  qed
+qed
+
+lemma distinct_compose:
+ assumes "distinct (map fst xs)"
+ shows "distinct (map fst (compose xs ys))"
+using assms
+proof (induct xs ys rule: compose.induct)
+  case 1 thus ?case by simp
+next
+  case (2 x xs ys)
+  show ?case
+  proof (cases "map_of ys (snd x)")
+    case None
+    with 2 show ?thesis by simp
+  next
+    case (Some v)
+    with 2 dom_compose [of xs ys] show ?thesis 
+      by (auto)
+  qed
+qed
+
+lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)"
+proof (induct xs ys rule: compose.induct)
+  case 1 thus ?case by simp
+next
+  case (2 x xs ys)
+  show ?case
+  proof (cases "map_of ys (snd x)")
+    case None
+    with 2 have 
+      hyp: "compose (delete k (delete (fst x) xs)) ys =
+            delete k (compose (delete (fst x) xs) ys)"
+      by simp
+    show ?thesis
+    proof (cases "fst x = k")
+      case True
+      with None hyp
+      show ?thesis
+        by (simp add: delete_idem)
+    next
+      case False
+      from None False hyp
+      show ?thesis
+        by (simp add: delete_twist)
+    qed
+  next
+    case (Some v)
+    with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp
+    with Some show ?thesis
+      by simp
+  qed
+qed
+
+lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys"
+  by (induct xs ys rule: compose.induct) 
+     (auto simp add: map_of_clearjunk split: option.splits)
+   
+lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys"
+  by (induct xs rule: clearjunk.induct)
+     (auto split: option.splits simp add: clearjunk_delete delete_idem
+               compose_delete_twist)
+   
+lemma compose_empty [simp]:
+ "compose xs [] = []"
+  by (induct xs) (auto simp add: compose_delete_twist)
+
+lemma compose_Some_iff:
+  "(map_of (compose xs ys) k = Some v) = 
+     (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = Some v)" 
+  by (simp add: compose_conv map_comp_Some_iff)
+
+lemma map_comp_None_iff:
+  "(map_of (compose xs ys) k = None) = 
+    (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " 
+  by (simp add: compose_conv map_comp_None_iff)
+
+subsection {* @{text map_entry} *}
+
+fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+  "map_entry k f [] = []"
+| "map_entry k f (p # ps) = (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
+
+lemma map_of_map_entry:
+  "map_of (map_entry k f xs) = (map_of xs)(k := case map_of xs k of None => None | Some v' => Some (f v'))"
+by (induct xs) auto
+
+lemma dom_map_entry:
+  "fst ` set (map_entry k f xs) = fst ` set xs"
+by (induct xs) auto
+
+lemma distinct_map_entry:
+  assumes "distinct (map fst xs)"
+  shows "distinct (map fst (map_entry k f xs))"
+using assms by (induct xs) (auto simp add: dom_map_entry)
+
+subsection {* @{text map_default} *}
+
+fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+  "map_default k v f [] = [(k, v)]"
+| "map_default k v f (p # ps) = (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)"
+
+lemma map_of_map_default:
+  "map_of (map_default k v f xs) = (map_of xs)(k := case map_of xs k of None => Some v | Some v' => Some (f v'))"
+by (induct xs) auto
+
+lemma dom_map_default:
+  "fst ` set (map_default k v f xs) = insert k (fst ` set xs)" 
+by (induct xs) auto
+
+lemma distinct_map_default:
+  assumes "distinct (map fst xs)"
+  shows "distinct (map fst (map_default k v f xs))"
+using assms by (induct xs) (auto simp add: dom_map_default)
+
+hide_const (open) update updates delete restrict clearjunk merge compose map_entry
+
+end
diff -r 6c722e960f2e -r 38cef5407d82 thys/LetElim.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/LetElim.thy	Fri Mar 21 15:07:59 2014 +0000
@@ -0,0 +1,804 @@
+theory LetElim
+imports Main Data_slot
+begin
+
+ML {*
+  val _ = print_depth 100
+*}
+
+ML {*
+  val trace_elim = Attrib.setup_config_bool @{binding trace_elim} (K false)
+*}
+
+ML {* (* aux functions *)
+  val tracing  = (fn ctxt => fn str =>
+                   if (Config.get ctxt trace_elim) then tracing str else ())
+
+  val empty_env = (Vartab.empty, Vartab.empty)
+
+  fun match_env ctxt pat trm env = 
+            Pattern.match (ctxt |> Proof_Context.theory_of) (pat, trm) env
+
+  fun match ctxt pat trm = match_env ctxt pat trm empty_env;
+
+  val inst = Envir.subst_term;
+
+  fun term_of_thm thm = thm |>  prop_of |> HOLogic.dest_Trueprop
+
+  fun last [a]  = a |
+      last (a::b) = last b
+
+  fun but_last [a] = [] |
+      but_last (a::b) = a::(but_last b)
+
+  fun foldr f [] = (fn x => x) |
+      foldr f (x :: xs) = (f x) o  (foldr f xs)
+
+  fun concat [] = [] |
+      concat (x :: xs) = x @ concat xs
+
+  fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of
+  fun string_of_cterm ctxt ct = ct |> term_of |> string_of_term ctxt
+  fun pterm ctxt t =
+          t |> string_of_term ctxt |> tracing ctxt
+  fun pcterm ctxt ct = ct |> string_of_cterm ctxt |> tracing ctxt
+  fun pthm ctxt thm = thm |> prop_of |> pterm ctxt
+  fun string_for_term ctxt t =
+       Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                   (print_mode_value ())) (Syntax.string_of_term ctxt) t
+         |> String.translate (fn c => if Char.isPrint c then str c else "")
+         |> Sledgehammer_Util.simplify_spaces  
+  fun string_for_cterm ctxt ct = ct |> term_of |> string_for_term ctxt
+  fun attemp tac = fn i => fn st => (tac i st) handle exn => Seq.empty
+  fun try_tac tac = fn i => fn st => (tac i st) handle exn => (Seq.single st)       
+  fun ctxt_show ctxt = ctxt |>  Config.put Proof_Context.verbose true |> 
+                                Config.put Proof_Context.debug true |>
+                                Config.put Display.show_hyps true |>
+                                Config.put Display.show_tags true 
+  fun swf f = (fn x => fn y => f y x)
+*} (* aux end *) 
+
+ML {*
+  fun close_form_over vars trm = 
+     fold Logic.all (map Free vars) trm
+  fun try_star f g = (try_star f (g |> f)) handle _ => g
+
+  fun bind_judgment ctxt name =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
+    val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x;
+  in ((v, t), ctxt') end;
+
+  fun let_trm_of ctxt mjp = let
+     fun is_let_trm (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = true 
+       | is_let_trm _ = false
+  in
+             ZipperSearch.all_td_lr (mjp |> Zipper.mktop) 
+          |> Seq.filter (fn z => is_let_trm (Zipper.trm z))
+          |> Seq.hd |> Zipper.trm 
+  end
+
+  fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
+  | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
+  | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
+  | decr _ _ = raise Same.SAME
+  and decrh lev t = (decr lev t handle Same.SAME => t);
+
+ (* A new version of [result], copied from [obtain.ML] *)
+fun eliminate_term ctxt xs tm =
+  let
+    val vs = map (dest_Free o Thm.term_of) xs;
+    val bads = Term.fold_aterms (fn t as Free v =>
+      if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
+    val _ = null bads orelse
+      error ("Result contains obtained parameters: " ^
+        space_implode " " (map (Syntax.string_of_term ctxt) bads));
+  in tm end;
+
+fun eliminate fix_ctxt rule xs As thm =
+  let
+    val thy = Proof_Context.theory_of fix_ctxt;
+
+    val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
+    val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
+      error "Conclusion in obtained context must be object-logic judgment";
+
+    val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
+    val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
+  in
+    ((Drule.implies_elim_list thm' (map Thm.assume prems)
+        |> Drule.implies_intr_list (map Drule.norm_hhf_cterm As)
+        |> Drule.forall_intr_list xs)
+      COMP rule)
+    |> Drule.implies_intr_list prems
+    |> singleton (Variable.export ctxt' fix_ctxt)
+  end;
+
+fun obtain_export ctxt rule xs _ As =
+  (eliminate ctxt rule xs As, eliminate_term ctxt xs);
+
+fun check_result ctxt thesis th =
+  (case Thm.prems_of th of
+    [prem] =>
+      if Thm.concl_of th aconv thesis andalso
+        Logic.strip_assums_concl prem aconv thesis then th
+      else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
+  | [] => error "Goal solved -- nothing guessed"
+  | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
+
+fun result tac facts ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val cert = Thm.cterm_of thy;
+    
+   val ([thesisN], _) = Variable.variant_fixes [Auto_Bind.thesisN] ctxt
+    
+    val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt thesisN;
+    val rule =
+      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
+        NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
+      | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th)));
+
+    val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
+    val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
+    val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
+    val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
+    val (prems, ctxt'') =
+      Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
+        (Drule.strip_imp_prems stmt) fix_ctxt;
+  in ((params, prems), ctxt'') end;
+*}
+
+ML {*
+local
+   fun let_lhs ctxt vars let_rest =
+    case let_rest of
+      Const (@{const_name prod_case}, _) $ let_rest =>
+           let 
+               val (exp1, rest1) = let_lhs ctxt vars let_rest 
+               val vars = Term.add_frees exp1 vars
+               val (exp2, rest2) = let_lhs ctxt vars rest1
+           in ((Const (@{const_name Pair}, dummyT) $ exp1 $ exp2), rest2) end
+    | Abs (var, var_typ, rest) => let
+           val (vars', _) = Variable.variant_fixes ((map fst vars)@[var]) ctxt
+           val (_, var') = vars' |> split_last
+           val [(var, var_typ)] = Variable.variant_frees ctxt (map Free vars) [(var, var_typ)] in
+             (Free (var', var_typ), rest) end
+
+   fun sg_lhs_f ctxt (vars, eqns, let_trm) = let
+        val (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = let_trm
+        val let_rest = case let_rest of
+                           Abs ("", _, let_rest$Bound 0) => decrh 0 let_rest
+                       | _ => let_rest
+        val (lhs, let_trm) = let_rest |> let_lhs ctxt vars
+        val lhs = lhs|> Syntax.check_term ctxt
+        val let_expr = let_expr |> Syntax.check_term ctxt
+        val eqn = HOLogic.mk_eq (lhs, let_expr) |> Syntax.check_term ctxt
+        val eqns = (eqn::eqns)
+        val vars = Term.add_frees lhs vars
+        val let_trm = Term.subst_bounds ((map Free vars), let_trm)
+     in (vars, eqns, let_trm) end
+  fun dest_let ctxt let_trm = let
+     val (vars,  eqns, lrest) = try_star (sg_lhs_f ctxt) ([], [],  let_trm)
+  in (vars, eqns, lrest) end
+
+in 
+
+ fun let_elim_rule ctxt mjp = let
+  val ctxt = ctxt |> Variable.set_body false
+  val thy = Proof_Context.theory_of ctxt
+  val cterm = cterm_of thy
+  val tracing = tracing ctxt
+  val pthm = pthm ctxt
+  val pterm = pterm ctxt
+  val pcterm = pcterm ctxt
+
+  val let_trm = let_trm_of ctxt mjp
+  val ([pname], _) = Variable.variant_fixes ["P"] ctxt
+  val P = Free (pname, dummyT)
+  val mjp = (Const (@{const_name Trueprop}, dummyT)$(P$let_trm))
+               |> Syntax.check_term ctxt 
+  val (Const (@{const_name Trueprop}, _)$((P as Free(_, _))$let_trm)) = mjp
+  val (vars, eqns, lrest) = dest_let ctxt let_trm
+
+  val ([thesisN], _) = Variable.variant_fixes ["let_thesis"] ctxt
+  val thesis_p = Free (thesisN, @{typ bool}) |> HOLogic.mk_Trueprop
+  val next_p = (P $ lrest) |> (HOLogic.mk_Trueprop)
+  val that_prems = (P $ lrest) :: (rev eqns) |> map (HOLogic.mk_Trueprop) 
+  val that_prop = Logic.list_implies (that_prems, thesis_p)
+  val that_prop = close_form_over vars that_prop
+  fun exists_on_lhs eq = let
+     val (lhs, rhs) = eq |> HOLogic.dest_eq 
+     fun exists_on vars trm = let
+          fun sg_exists_on (n, ty) trm = HOLogic.mk_exists (n, ty, trm)
+          in fold sg_exists_on vars trm end
+  in exists_on (Term.add_frees lhs []) eq end
+  fun prove_eqn ctxt0 eqn = let
+    val (lhs, let_expr) = eqn |> HOLogic.dest_eq 
+    val eq_e_prop = exists_on_lhs eqn |> HOLogic.mk_Trueprop
+    fun case_rule_of ctxt let_expr = let
+       val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
+       val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of 
+                          |> Induct.vars_of |> hd |> cterm
+       val mt = Thm.match (case_var, let_expr |> cterm)
+       val case_rule = Thm.instantiate mt case_rule 
+    in case_rule end
+    val case_rule = SOME (case_rule_of ctxt0 let_expr) handle _ => NONE
+    val my_case_tac = case case_rule of 
+                        SOME case_rule => (rtac case_rule 1)
+                      | _ => all_tac
+    val eq_e = Goal.prove ctxt0 [] [] eq_e_prop
+                (K (my_case_tac THEN (auto_tac ctxt0)))
+  in eq_e end
+  val peqns = eqns |> map (prove_eqn ctxt)
+  fun add_result thm (facts, ctxt) = let
+      val ((_, [fact]), ctxt1) = (result (K (REPEAT (etac @{thm exE} 1))) [thm] ctxt)
+  in (fact::facts, ctxt1) end
+  val add_results = fold add_result
+  val (facts, ctxt1) = add_results (rev peqns) ([], ctxt)
+  (* val facts = rev facts *)
+  val ([mjp_p, that_p], ctxt2) = ctxt1 |> Assumption.add_assumes (map cterm [mjp, that_prop])
+  val sym_facts = map (swf (curry (op RS)) @{thm sym}) facts
+  fun rsn eq that_p = eq RSN (2, that_p)
+  val rule1 = fold rsn (rev facts) that_p
+  val tac = (Method.insert_tac ([mjp_p]@sym_facts) 1) THEN (auto_tac ctxt2)
+  val next_pp = Goal.prove ctxt [] [] next_p (K tac)
+  val result = next_pp RS rule1
+  val ctxt3 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) 
+                [mjp, thesis_p] ctxt2
+  val [let_elim_rule] = Proof_Context.export ctxt3 ctxt [result]
+ in let_elim_rule end
+
+ fun let_intro_rule ctxt mjp = let
+  val ctxt = ctxt |> Variable.set_body false
+  val thy = Proof_Context.theory_of ctxt
+  val cterm = cterm_of thy
+  val tracing = tracing ctxt
+  val pthm = pthm ctxt
+  val pterm = pterm ctxt
+  val pcterm = pcterm ctxt
+
+  val ([thesisN], _) = Variable.variant_fixes ["let_thesis"] ctxt
+  val thesis_p = Free (thesisN, @{typ bool}) |> HOLogic.mk_Trueprop
+  val let_trm = let_trm_of ctxt mjp
+  val ([pname], _) = Variable.variant_fixes ["P"] ctxt
+  val P = Free (pname, dummyT)
+  val mjp = (Const (@{const_name Trueprop}, dummyT)$(P$let_trm))
+               |> Syntax.check_term ctxt 
+  val (Const (@{const_name Trueprop}, _)$((P as Free(_, _))$let_trm)) = mjp
+  val (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = let_trm
+  val (vars, eqns, lrest) = dest_let ctxt let_trm
+
+  val next_p = (P $ lrest) |> (HOLogic.mk_Trueprop) 
+  val that_prems =  (rev eqns) |> map (HOLogic.mk_Trueprop) 
+  val that_prop = Logic.list_implies (that_prems, next_p) 
+  val that_prop = close_form_over vars that_prop |> Syntax.check_term ctxt 
+  fun exists_on_lhs eq = let
+     val (lhs, rhs) = eq |> HOLogic.dest_eq 
+     fun exists_on vars trm = let
+          fun sg_exists_on (n, ty) trm = HOLogic.mk_exists (n, ty, trm)
+          in fold sg_exists_on vars trm end
+  in exists_on (Term.add_frees lhs []) eq end
+  fun prove_eqn ctxt0 eqn = let
+    val (lhs, let_expr) = eqn |> HOLogic.dest_eq 
+    val eq_e_prop = exists_on_lhs eqn |> HOLogic.mk_Trueprop
+    fun case_rule_of ctxt let_expr = let
+       val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
+       val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of 
+                          |> Induct.vars_of |> hd |> cterm
+       val mt = Thm.match (case_var, let_expr |> cterm)
+       val case_rule = Thm.instantiate mt case_rule 
+    in case_rule end
+    val case_rule = SOME (case_rule_of ctxt0 let_expr) handle _ => NONE
+    val my_case_tac = case case_rule of 
+                        SOME case_rule => (rtac case_rule 1)
+                      | _ => all_tac
+    val eq_e = Goal.prove ctxt0 [] [] eq_e_prop
+                (K (my_case_tac THEN (auto_tac ctxt0)))
+  in eq_e end
+  val peqns = eqns |> map (prove_eqn ctxt)
+  fun add_result thm (facts, ctxt) = let
+      val ((_, [fact]), ctxt1) = (result (K (REPEAT (etac @{thm exE} 1))) [thm] ctxt)
+  in (fact::facts, ctxt1) end
+  val add_results = fold add_result
+  val (facts, ctxt1) = add_results (rev peqns) ([], ctxt)
+  val sym_facts = map (swf (curry (op RS)) @{thm sym}) facts
+  val ([that_p], ctxt2) = ctxt1 |> Assumption.add_assumes (map cterm [that_prop])
+  fun rsn eq that_p = eq RSN (1, that_p)
+  val rule1 = fold rsn (rev facts) that_p
+  val tac = (Method.insert_tac (rule1::sym_facts) 1) THEN (auto_tac ctxt2)
+  val result = Goal.prove ctxt [] [] mjp (K tac)
+  val ctxt3 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) 
+                [mjp, thesis_p] ctxt2
+  val [let_intro_rule] = Proof_Context.export ctxt3 ctxt [result]
+ in let_intro_rule end
+
+end
+*}
+
+ML {*
+ fun let_elim_tac ctxt i st = let
+  val thy = Proof_Context.theory_of ctxt
+  val cterm = cterm_of thy
+  val goal = nth (Thm.prems_of st) (i - 1)  |> cterm
+  val mjp = goal |> Drule.strip_imp_prems |> swf nth 0 |> term_of
+  val rule = let_elim_rule ctxt mjp
+  val tac = (etac rule i st)
+ in tac end
+*}
+
+ML {*
+local
+val case_names_tagN = "case_names";
+
+val implode_args = space_implode ";";
+val explode_args = space_explode ";";
+
+fun add_case_names NONE = I
+  | add_case_names (SOME names) =
+      Thm.untag_rule case_names_tagN
+      #> Thm.tag_rule (case_names_tagN, implode_args names);
+in
+ fun let_elim_cases_tac ctxt facts = let
+  val tracing = tracing ctxt
+  val pthm = pthm ctxt
+  val pterm = pterm ctxt
+  val pcterm = pcterm ctxt
+  val mjp = facts |> swf nth 0 |> prop_of
+  val _ = tracing "let_elim_cases_tac: elim rule derived is:"
+  val rule = (let_elim_rule ctxt mjp) |> Rule_Cases.put_consumes (SOME 1)
+             |> add_case_names (SOME ["LetE"])
+  val _ = rule |> pthm
+ in
+   Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts
+ end
+end
+*}
+
+ML {*
+  val ctxt = @{context}
+  val thy = Proof_Context.theory_of ctxt
+  val cterm = cterm_of thy
+  val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3
+                      in f w x1 y1 u)"}	
+*}
+
+ML {*
+    val mjp1 = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = e2 in (w +x1 *y1 +u))"}
+    val mjp2 = @{prop "P (let ((x, y), (z, u)) = e; (u, v) = e1 in 
+                             (case u of (Some t) \<Rightarrow> f t x y z |
+                                        None \<Rightarrow> g x y z))"}
+    val mjp3 = @{prop "P (let x = e1; ((x1, y1), u) = e2 in f x w x1 y1 u)"}
+    val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3
+                      in f w x1 y1 u)"}	
+    val mjps =  [mjp1, mjp2, mjp3,  mjp] 
+  val t = mjps |> map (let_elim_rule ctxt)
+  val t2 = mjps |> map (let_intro_rule ctxt)
+*}
+
+ML {*
+val let_elim_setup =
+  Method.setup @{binding let_elim}
+    (Scan.lift (Args.mode Induct.no_simpN) >>
+      (fn no_simp => fn ctxt =>
+        METHOD_CASES (fn facts =>  (HEADGOAL
+          (let_elim_cases_tac ctxt facts)))))
+    "elimination of prems containing lets ";
+*}
+
+setup {* let_elim_setup *}
+
+ML {*
+  val ctxt = @{context}
+  val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1
+                      in f w x1 y1 u)"}
+*}
+
+ML {*
+fun focus_params t ctxt =
+  let
+    val (xs, Ts) =
+      split_list (Term.variant_frees t (Term.strip_all_vars t));  (*as they are printed :-*)
+    (* val (xs', ctxt') = variant_fixes xs ctxt; *)
+    (* val ps = xs' ~~ Ts; *)
+    val ps = xs ~~ Ts
+    val (_, ctxt'') = ctxt |> Variable.add_fixes xs
+  in ((xs, ps), ctxt'') end
+
+fun focus_concl ctxt t =
+  let
+    val ((xs, ps), ctxt') = focus_params t ctxt
+    val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
+  in (t' |> Logic.strip_imp_concl, ctxt') end
+*}
+
+ML {*
+local
+val case_names_tagN = "case_names";
+
+val implode_args = space_implode ";";
+val explode_args = space_explode ";";
+
+fun add_case_names NONE = I
+  | add_case_names (SOME names) =
+      Thm.untag_rule case_names_tagN
+      #> Thm.tag_rule (case_names_tagN, implode_args names);
+
+in
+ fun let_intro_cases_tac ctxt facts i st = let
+  val (mjp, _) = nth (Thm.prems_of st) (i - 1) |> focus_concl ctxt 
+  val rule = (let_intro_rule ctxt mjp) |> add_case_names (SOME ["LetI"])
+ in
+   Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st
+ end
+end
+*}
+
+ML {*
+val let_intro_setup =
+  Method.setup @{binding let_intro}
+    (Scan.lift (Args.mode Induct.no_simpN) >>
+      (fn no_simp => fn ctxt =>
+        METHOD_CASES (fn facts => (HEADGOAL
+          (let_intro_cases_tac ctxt facts)))))
+    "introduction rule for goals containing lets ";
+*}
+
+setup {* let_intro_setup *}
+
+lemma assumes "Q xxx" "W uuuu"
+  shows "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1
+                      in f w x1 y1 u) = www"
+  using assms 
+proof(let_intro)
+  case (LetI x y w ww x1 y1 u x2 y2)
+  thus ?case
+    oops
+
+lemma
+  assumes "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1
+                      in f w x1 y1 u)"
+    and   "Q xxx" "W uuuu"
+  shows "thesis" using assms
+  proof(let_elim) 
+    case (LetE x y w ww x1 y1 u x2 y2)
+    thus ?case 
+      oops
+
+
+ML {*
+  val mjp = @{prop "P ( case (u@v) of
+                          Nil \<Rightarrow> f u v
+                       | x#xs \<Rightarrow> g u v x xs
+                    )"}
+  val mjp1 = @{term "( case (h u v) of
+                          None \<Rightarrow> g u v x
+                       | Some x \<Rightarrow> (case v of 
+                                      Nil \<Rightarrow> f u v |
+                                    x#xs \<Rightarrow> h x xs
+                                  )
+                    )"}
+*}
+
+
+ML {*
+  fun case_trm_of ctxt mjp = 
+             ZipperSearch.all_td_lr (mjp |> Zipper.mktop) 
+          |> Seq.filter (fn z => ((Case_Translation.strip_case ctxt true (Zipper.trm z)) <> NONE))
+          |> Seq.hd |> Zipper.trm 
+*}
+
+ML {*
+fun case_elim_rule ctxt mjp = let
+  val ctxt = ctxt |> Variable.set_body false
+  val thy = Proof_Context.theory_of ctxt;
+  val cterm = cterm_of thy
+  val ([thesisN], _) = Variable.variant_fixes ["my_thesis"] ctxt
+  val ((_, thesis_p), _) = bind_judgment ctxt thesisN
+  val case_trm = case_trm_of ctxt mjp
+  val (case_expr, case_eqns) = case_trm |> Case_Translation.strip_case ctxt true |> the
+  val ([pname], _) = Variable.variant_fixes ["P"] ctxt
+  val P = Free (pname, [(case_trm |> type_of)] ---> @{typ bool}) 
+  val mjp_p = (P $ case_trm) |> HOLogic.mk_Trueprop
+  val ctxt0 = Proof_Context.init_global thy 
+  val thats = case_eqns |> map (fn (lhs, rhs) => let
+               val vars = Term.add_frees lhs []
+          in 
+             Logic.list_implies ([(P$rhs)|>HOLogic.mk_Trueprop,
+                                 HOLogic.mk_eq (case_expr, lhs) |> HOLogic.mk_Trueprop], thesis_p) |>
+                close_form_over vars 
+          end) |>
+    map (Term.map_types (Term.map_type_tvar (fn _ => dummyT))) |> 
+    map (Syntax.check_term ctxt0)
+  val (mjp_p::that_ps, ctxt1) = ctxt |> Assumption.add_assumes (map cterm (mjp_p::thats))
+  fun case_rule_of ctxt let_expr = let
+       val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
+       val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of 
+                          |> Induct.vars_of |> hd |> cterm
+       val mt = Thm.match (case_var, let_expr |> cterm)
+       val case_rule = Thm.instantiate mt case_rule 
+    in case_rule end
+  val case_rule = case_rule_of ctxt case_expr
+  val my_case_tac = (rtac case_rule)
+  val my_tac = ((Method.insert_tac (mjp_p::that_ps)) THEN' my_case_tac THEN' (K (auto_tac ctxt1))) 1
+  val result = Goal.prove ctxt1 [] [] thesis_p (K my_tac)
+  val ctxt2 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) 
+                [P, thesis_p, mjp] ctxt1
+  val [case_elim_rule] =  Proof_Context.export ctxt2 ctxt [result]
+  val ocase_rule = Induct.find_casesT ctxt (case_expr |> type_of) |> hd
+  fun get_case_names rule = 
+     AList.lookup (op =) (Thm.get_tags rule) "case_names" |> the
+  fun put_case_names names rule =
+           Thm.tag_rule ("case_names", names) rule
+  val case_elim_rule = put_case_names (get_case_names ocase_rule) case_elim_rule
+in case_elim_rule end
+*}
+
+ML {*
+ fun case_elim_cases_tac ctxt facts = let
+  val mjp = facts |> swf nth 0 |> prop_of
+  val rule = (case_elim_rule ctxt mjp) |> Rule_Cases.put_consumes (SOME 1)
+ in
+   Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts
+ end
+*}
+
+
+ML {*
+val case_elim_setup =
+  Method.setup @{binding case_elim}
+    (Scan.lift (Args.mode Induct.no_simpN) >>
+      (fn no_simp => fn ctxt =>
+        METHOD_CASES (fn facts =>  (HEADGOAL
+          (case_elim_cases_tac ctxt facts)))))
+    "elimination of prems containing case ";
+*}
+
+setup {* case_elim_setup *}
+
+lemma assumes 
+    "P (case h u v of None \<Rightarrow> g u v x | Some x \<Rightarrow> case v of [] \<Rightarrow> f u v | x # xs \<Rightarrow> h x xs)"
+    "GG u v" "PP w x"
+  shows "thesis" using assms
+proof(case_elim) (* ccc *)
+  case None
+  thus ?case oops
+(*
+next
+  case (Some x)
+  thus ?case
+  proof(case_elim)
+    case Nil
+    thus ?case sorry
+  next
+    case (Cons y ys)
+    thus ?case sorry
+  qed
+qed
+*)
+
+ML {*
+fun case_intro_rule ctxt mjp = let
+  val ctxt = ctxt |> Variable.set_body false
+  val tracing = tracing ctxt
+  val pthm = pthm ctxt
+  val pterm = pterm ctxt
+  val pcterm = pcterm ctxt
+  val thy = Proof_Context.theory_of ctxt
+  val cterm = cterm_of thy
+  val ([thesisN], _) = Variable.variant_fixes ["my_thesis"] ctxt
+  val ((_, thesis_p), _) = bind_judgment ctxt thesisN
+  val case_trm = case_trm_of ctxt mjp
+  val (case_expr, case_eqns) = case_trm |> Case_Translation.strip_case ctxt true |> the
+  val ([pname], _) = Variable.variant_fixes ["P"] ctxt
+  val P = Free (pname, [(case_trm |> type_of)] ---> @{typ bool}) 
+  val mjp_p = (P $ case_trm) |> HOLogic.mk_Trueprop 
+  val ctxt0 = Proof_Context.init_global thy 
+  val thats = case_eqns |> map (fn (lhs, rhs) => let
+               val vars = Term.add_frees lhs []
+          in 
+             Logic.list_implies ([HOLogic.mk_eq (case_expr, lhs) |> HOLogic.mk_Trueprop], 
+                                     (P$rhs)|>HOLogic.mk_Trueprop) |>
+                close_form_over vars 
+          end) |> 
+    map (Term.map_types (Term.map_type_tvar (fn _ => dummyT))) |> 
+    map (Syntax.check_term ctxt0)
+  val (that_ps, ctxt1) = ctxt |> Assumption.add_assumes (map cterm (thats))
+  fun case_rule_of ctxt let_expr = let
+       val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
+       val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of 
+                          |> Induct.vars_of |> hd |> cterm
+       val mt = Thm.match (case_var, let_expr |> cterm)
+       val case_rule = Thm.instantiate mt case_rule 
+    in case_rule end
+ 
+  val case_rule = case_rule_of ctxt case_expr
+  val my_case_tac = (rtac case_rule)
+  val my_tac = ((Method.insert_tac (that_ps)) THEN' my_case_tac THEN' (K (auto_tac ctxt1))) 1
+  val result = Goal.prove ctxt1 [] [] mjp_p (K my_tac)
+  val ctxt2 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt)) 
+                [P, thesis_p, mjp] ctxt1
+  val [case_intro_rule] =  Proof_Context.export ctxt2 ctxt [result]
+  val ocase_rule = Induct.find_casesT ctxt (case_expr |> type_of) |> hd
+  fun get_case_names rule = 
+     AList.lookup (op =) (Thm.get_tags rule) "case_names" |> the
+  fun put_case_names names rule =
+           Thm.tag_rule ("case_names", names) rule
+  val case_intro_rule = put_case_names (get_case_names ocase_rule) case_intro_rule
+in case_intro_rule end
+*}
+
+ML {*
+  val t = [mjp, mjp1] |> map (case_intro_rule ctxt)
+*}
+
+ML {*
+ fun case_intro_cases_tac ctxt facts i st = let
+  val (mjp, _) = nth (Thm.prems_of st) (i - 1) |> focus_concl ctxt 
+  val rule = (case_intro_rule ctxt mjp) 
+ in
+   Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st
+ end
+*}
+
+ML {*
+val case_intro_setup =
+  Method.setup @{binding case_intro}
+    (Scan.lift (Args.mode Induct.no_simpN) >>
+      (fn no_simp => fn ctxt =>
+        METHOD_CASES (fn facts => (HEADGOAL
+          (case_intro_cases_tac ctxt facts)))))
+    "introduction rule for goals containing case";
+*}
+
+setup {* case_intro_setup *}
+
+
+lemma assumes "QQ (let u = e1; (j, k) = e1; (b, a) = qq j k in TT j k b a)"
+ shows "P (hhh y ys)" using assms
+proof(let_elim)
+  oops
+
+lemma assumes 
+    "QQ (let (j, k) = e1; (m, n) = qq j k in TT j k m n)"
+     "PP w x"
+  shows "P (case h u v of None \<Rightarrow> g u v x | Some x1 \<Rightarrow> case v of [] \<Rightarrow> f u v | xx # xs \<Rightarrow> hhh xx xs)"
+  using assms
+proof(case_intro)
+  case None
+  from None(2)
+  show ?case
+  proof(let_elim)
+    case (LetE j k a b)
+    with None
+    show ?case oops
+(*
+      sorry
+  qed
+next
+  case (Some x1)
+  thus ?case
+  proof(case_intro)
+    case Nil
+    from Nil(3)
+    show ?case
+    proof(let_elim)
+      case (LetE j k a b)
+      with Nil show ?case sorry
+    qed
+  next
+    case (Cons y ys) 
+    from Cons(3) 
+    show ?case
+    proof (let_elim)
+      case (LetE j k u v)
+      with Cons
+      show ?case sorry 
+    qed
+  qed
+qed
+*)
+
+lemma assumes 
+    "QQ (let (j, k) = e1; (m, n) = qq j k in TT j k m n)"
+     "PP w uux"
+  shows "P (case h u v of None \<Rightarrow> g u v x | Some x1 \<Rightarrow> case v of [] \<Rightarrow> f u v | xx # xs \<Rightarrow> hhh xx xs)"
+  using assms
+proof(let_elim)
+  case (LetE j k m n)
+  thus ?case
+  proof(case_intro)
+    case None
+    thus ?case oops (*
+  next
+    case (Some x)
+    thus ?case
+    proof(case_intro)
+      case Nil
+      thus ?case sorry
+    next
+      case (Cons y ys)
+      thus ?case sorry
+    qed
+  qed
+qed
+*)
+
+lemma ifE [consumes 1, case_names If_true If_false]: 
+  assumes "P (if b then e1 else e2)"
+          "\<lbrakk>b; P e1\<rbrakk> \<Longrightarrow> thesis"
+          "\<lbrakk>\<not> b; P e2\<rbrakk> \<Longrightarrow> thesis"
+  shows "thesis" using assms
+  by (auto split:if_splits)
+
+lemma ifI  [case_names If_true If_false]: 
+  assumes "b \<Longrightarrow> P e1" "\<not> b \<Longrightarrow> P e2"
+  shows "P (if b then e1 else e2)" using assms
+  by auto
+
+ML {*
+ fun if_elim_cases_tac ctxt facts = let
+  val rule = @{thm ifE}
+ in
+   Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts
+ end
+*}
+
+ML {*
+val if_elim_setup =
+  Method.setup @{binding if_elim}
+    (Scan.lift (Args.mode Induct.no_simpN) >>
+      (fn no_simp => fn ctxt =>
+        METHOD_CASES (fn facts =>  (HEADGOAL
+          (if_elim_cases_tac ctxt facts)))))
+    "elimination of prems containing if ";
+*}
+
+setup {* if_elim_setup *}
+
+ML {*
+ fun if_intro_cases_tac ctxt facts i st = let
+  val rule = @{thm ifI}
+ in
+   Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st
+ end
+*}
+
+ML {*
+val if_intro_setup =
+  Method.setup @{binding if_intro}
+    (Scan.lift (Args.mode Induct.no_simpN) >>
+      (fn no_simp => fn ctxt =>
+        METHOD_CASES (fn facts => (HEADGOAL
+          (if_intro_cases_tac ctxt facts)))))
+    "introduction rule for goals containing if";
+*}
+
+setup {* if_intro_setup *}
+
+lemma assumes "(if (B x y) then f x y else g y x) = (t, p)"
+     "P1 xxx" "P2 yyy"
+  shows "that" using assms
+proof(if_elim)
+  case If_true
+  thus ?case oops
+(*
+next
+  case If_false
+  thus ?case oops
+*)
+
+lemma assumes "P1 xx" "P2 yy"
+  shows "P (if b then e1 else e2)" using assms
+proof(if_intro)
+  case If_true
+  thus ?case oops
+(*
+next
+  case If_false
+  thus ?case sorry
+qed
+*)
+
+end
\ No newline at end of file
diff -r 6c722e960f2e -r 38cef5407d82 thys/StateMonad.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/StateMonad.thy	Fri Mar 21 15:07:59 2014 +0000
@@ -0,0 +1,481 @@
+theory StateMonad
+imports 
+       "~~/src/HOL/Library/Monad_Syntax" 
+begin
+
+datatype ('result, 'state) SM = SM "'state => ('result \<times> 'state) option"
+
+fun execute :: "('result, 'state) SM \<Rightarrow> 'state \<Rightarrow> ('result \<times> 'state) option" where
+  "execute (SM f) = f"
+
+lemma SM_cases [case_names succeed fail]:
+  fixes f and s
+  assumes succeed: "\<And>x s'. execute f h = Some (x, s') \<Longrightarrow> P"
+  assumes fail: "execute f h = None \<Longrightarrow> P"
+  shows P
+  using assms by (cases "execute f h") auto
+
+lemma SM_execute [simp]:
+  "SM (execute f) = f" by (cases f) simp_all
+
+lemma SM_eqI:
+  "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
+    by (cases f, cases g) (auto simp: fun_eq_iff)
+
+ML {* structure Execute_Simps = Named_Thms
+(
+  val name = @{binding execute_simps}
+  val description = "simplification rules for execute"
+) *}
+
+setup Execute_Simps.setup
+
+lemma execute_Let [execute_simps]:
+  "execute (let x = t in f x) = (let x = t in execute (f x))"
+  by (simp add: Let_def)
+
+
+subsubsection {* Specialised lifters *}
+
+definition sm :: "('state \<Rightarrow> 'a \<times> 'state) \<Rightarrow> ('a, 'state) SM" where
+  "sm f = SM (Some \<circ> f)"
+
+definition tap :: "('state \<Rightarrow> 'a) \<Rightarrow> ('a, 'state) SM" where
+  "tap f = SM (\<lambda>s. Some (f s, s))"
+
+definition "sm_get = tap id"
+
+definition "sm_map f = sm (\<lambda> s.((), f s))"
+
+definition "sm_set s' = sm_map (\<lambda> s. s)"
+
+lemma execute_tap [execute_simps]:
+  "execute (tap f) h = Some (f h, h)"
+  by (simp add: tap_def)
+
+
+lemma execute_heap [execute_simps]:
+  "execute (sm f) = Some \<circ> f"
+  by (simp add: sm_def)
+
+definition guard :: "('state \<Rightarrow> bool) \<Rightarrow> ('state \<Rightarrow> 'a \<times> 'state) 
+                        \<Rightarrow> ('a, 'state) SM" where
+ "guard P f = SM (\<lambda>h. if P h then Some (f h) else None)"
+
+lemma execute_guard [execute_simps]:
+  "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
+  "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
+  by (simp_all add: guard_def)
+
+
+subsubsection {* Predicate classifying successful computations *}
+
+definition success :: "('a, 'state) SM \<Rightarrow> 'state \<Rightarrow> bool" where
+  "success f h = (execute f h \<noteq> None)"
+
+lemma successI:
+  "execute f h \<noteq> None \<Longrightarrow> success f h"
+  by (simp add: success_def)
+
+lemma successE:
+  assumes "success f h"
+  obtains r h' where "r = fst (the (execute c h))"
+    and "h' = snd (the (execute c h))"
+    and "execute f h \<noteq> None"
+  using assms by (simp add: success_def)
+
+ML {* structure Success_Intros = Named_Thms
+(
+  val name = @{binding success_intros}
+  val description = "introduction rules for success"
+) *}
+
+setup Success_Intros.setup
+
+lemma success_tapI [success_intros]:
+  "success (tap f) h"
+  by (rule successI) (simp add: execute_simps)
+
+lemma success_heapI [success_intros]:
+  "success (sm f) h"
+  by (rule successI) (simp add: execute_simps)
+
+lemma success_guardI [success_intros]:
+  "P h \<Longrightarrow> success (guard P f) h"
+  by (rule successI) (simp add: execute_guard)
+
+lemma success_LetI [success_intros]:
+  "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
+  by (simp add: Let_def)
+
+lemma success_ifI:
+  "(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>
+    success (if c then t else e) h"
+  by (simp add: success_def)
+
+subsubsection {* Predicate for a simple relational calculus *}
+
+text {*
+  The @{text effect} predicate states that when a computation @{text c}
+  runs with the state @{text h} will result in return value @{text r}
+  and a state @{text "h'"}, i.e.~no exception occurs.
+*}  
+
+definition effect :: "('a, 'state) SM \<Rightarrow> 'state \<Rightarrow> 'state \<Rightarrow> 'a \<Rightarrow> bool" where
+  effect_def: "effect c h h' r = (execute c h = Some (r, h'))"
+
+lemma effectI:
+  "execute c h = Some (r, h') \<Longrightarrow> effect c h h' r"
+  by (simp add: effect_def)
+
+lemma effectE:
+  assumes "effect c h h' r"
+  obtains "r = fst (the (execute c h))"
+    and "h' = snd (the (execute c h))"
+    and "success c h"
+proof (rule that)
+  from assms have *: "execute c h = Some (r, h')" by (simp add: effect_def)
+  then show "success c h" by (simp add: success_def)
+  from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
+    by simp_all
+  then show "r = fst (the (execute c h))"
+    and "h' = snd (the (execute c h))" by simp_all
+qed
+
+lemma effect_success:
+  "effect c h h' r \<Longrightarrow> success c h"
+  by (simp add: effect_def success_def)
+
+lemma success_effectE:
+  assumes "success c h"
+  obtains r h' where "effect c h h' r"
+  using assms by (auto simp add: effect_def success_def)
+
+lemma effect_deterministic:
+  assumes "effect f h h' a"
+    and "effect f h h'' b"
+  shows "a = b" and "h' = h''"
+  using assms unfolding effect_def by auto
+
+ML {* structure Effect_Intros = Named_Thms
+(
+  val name = @{binding effect_intros}
+  val description = "introduction rules for effect"
+) *}
+
+ML {* structure Effect_Elims = Named_Thms
+(
+  val name = @{binding effect_elims}
+  val description = "elimination rules for effect"
+) *}
+
+setup "Effect_Intros.setup #> Effect_Elims.setup"
+
+lemma effect_LetI [effect_intros]:
+  assumes "x = t" "effect (f x) h h' r"
+  shows "effect (let x = t in f x) h h' r"
+  using assms by simp
+
+lemma effect_LetE [effect_elims]:
+  assumes "effect (let x = t in f x) h h' r"
+  obtains "effect (f t) h h' r"
+  using assms by simp
+
+lemma effect_ifI:
+  assumes "c \<Longrightarrow> effect t h h' r"
+    and "\<not> c \<Longrightarrow> effect e h h' r"
+  shows "effect (if c then t else e) h h' r"
+  by (cases c) (simp_all add: assms)
+
+lemma effect_ifE:
+  assumes "effect (if c then t else e) h h' r"
+  obtains "c" "effect t h h' r"
+    | "\<not> c" "effect e h h' r"
+  using assms by (cases c) simp_all
+
+lemma effect_tapI [effect_intros]:
+  assumes "h' = h" "r = f h"
+  shows "effect (tap f) h h' r"
+  by (rule effectI) (simp add: assms execute_simps)
+
+lemma effect_tapE [effect_elims]:
+  assumes "effect (tap f) h h' r"
+  obtains "h' = h" and "r = f h"
+  using assms by (rule effectE) (auto simp add: execute_simps)
+
+lemma effect_heapI [effect_intros]:
+  assumes "h' = snd (f h)" "r = fst (f h)"
+  shows "effect (sm f) h h' r"
+  by (rule effectI) (simp add: assms execute_simps)
+
+lemma effect_heapE [effect_elims]:
+  assumes "effect (sm f) h h' r"
+  obtains "h' = snd (f h)" and "r = fst (f h)"
+  using assms by (rule effectE) (simp add: execute_simps)
+
+lemma effect_guardI [effect_intros]:
+  assumes "P h" "h' = snd (f h)" "r = fst (f h)"
+  shows "effect (guard P f) h h' r"
+  by (rule effectI) (simp add: assms execute_simps)
+
+lemma effect_guardE [effect_elims]:
+  assumes "effect (guard P f) h h' r"
+  obtains "h' = snd (f h)" "r = fst (f h)" "P h"
+  using assms by (rule effectE)
+    (auto simp add: execute_simps elim!: successE, 
+        cases "P h", auto simp add: execute_simps)
+
+
+subsubsection {* Monad combinators *}
+
+definition return :: "'a \<Rightarrow> ('a, 'state) SM" where
+       "return x = sm (Pair x)"
+
+lemma execute_return [execute_simps]:
+  "execute (return x) = Some \<circ> Pair x"
+  by (simp add: return_def execute_simps)
+
+lemma success_returnI [success_intros]:
+  "success (return x) h"
+  by (rule successI) (simp add: execute_simps)
+
+lemma effect_returnI [effect_intros]:
+  "h = h' \<Longrightarrow> effect (return x) h h' x"
+  by (rule effectI) (simp add: execute_simps)
+
+lemma effect_returnE [effect_elims]:
+  assumes "effect (return x) h h' r"
+  obtains "r = x" "h' = h"
+  using assms by (rule effectE) (simp add: execute_simps)
+
+definition raise :: "string \<Rightarrow> ('a, 'state) SM" where 
+      -- {* the string is just decoration *}
+               "raise s = SM (\<lambda>_. None)"
+
+lemma execute_raise [execute_simps]:
+  "execute (raise s) = (\<lambda>_. None)"
+  by (simp add: raise_def)
+
+lemma effect_raiseE [effect_elims]:
+  assumes "effect (raise x) h h' r"
+  obtains "False"
+  using assms by (rule effectE) (simp add: success_def execute_simps)
+
+definition bind :: "('a, 'state) SM \<Rightarrow> ('a \<Rightarrow> ('b, 'state) SM) \<Rightarrow> ('b, 'state) SM" where
+  "bind f g = SM (\<lambda>h. case execute f h of
+                  Some (x, h') \<Rightarrow> execute (g x) h'
+                | None \<Rightarrow> None)"
+
+adhoc_overloading
+  Monad_Syntax.bind StateMonad.bind
+
+
+lemma execute_bind [execute_simps]:
+  "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
+  "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
+  by (simp_all add: bind_def)
+
+lemma execute_bind_case:
+  "execute (f \<guillemotright>= g) h = (case (execute f h) of
+    Some (x, h') \<Rightarrow> execute (g x) h' | None \<Rightarrow> None)"
+  by (simp add: bind_def)
+
+lemma execute_bind_success:
+  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
+  by (cases f h rule: SM_cases) (auto elim!: successE simp add: bind_def)
+
+lemma success_bind_executeI:
+  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
+  by (auto intro!: successI elim!: successE simp add: bind_def)
+
+lemma success_bind_effectI [success_intros]:
+  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
+  by (auto simp add: effect_def success_def bind_def)
+
+lemma effect_bindI [effect_intros]:
+  assumes "effect f h h' r" "effect (g r) h' h'' r'"
+  shows "effect (f \<guillemotright>= g) h h'' r'"
+  using assms
+  apply (auto intro!: effectI elim!: effectE successE)
+  apply (subst execute_bind, simp_all)
+  done
+
+lemma effect_bindE [effect_elims]:
+  assumes "effect (f \<guillemotright>= g) h h'' r'"
+  obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"
+  using assms by (auto simp add: effect_def bind_def split: option.split_asm)
+
+lemma execute_bind_eq_SomeI:
+  assumes "execute f h = Some (x, h')"
+    and "execute (g x) h' = Some (y, h'')"
+  shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
+  using assms by (simp add: bind_def)
+
+lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
+  by (rule SM_eqI) (simp add: execute_bind execute_simps)
+
+lemma bind_return [simp]: "f \<guillemotright>= return = f"
+  by (rule SM_eqI) (simp add: bind_def execute_simps split: option.splits)
+
+lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = (f :: ('a, 'state) SM) \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
+  by (rule SM_eqI) (simp add: bind_def execute_simps split: option.splits)
+
+lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
+  by (rule SM_eqI) (simp add: execute_simps)
+
+
+subsection {* Generic combinators *}
+
+subsubsection {* Assertions *}
+
+definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> ('a, 'state) SM" where
+  "assert P x = (if P x then return x else raise ''assert'')"
+
+lemma execute_assert [execute_simps]:
+  "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
+  "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
+  by (simp_all add: assert_def execute_simps)
+
+lemma success_assertI [success_intros]:
+  "P x \<Longrightarrow> success (assert P x) h"
+  by (rule successI) (simp add: execute_assert)
+
+lemma effect_assertI [effect_intros]:
+  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> effect (assert P x) h h' r"
+  by (rule effectI) (simp add: execute_assert)
+ 
+lemma effect_assertE [effect_elims]:
+  assumes "effect (assert P x) h h' r"
+  obtains "P x" "r = x" "h' = h"
+  using assms by (rule effectE) (cases "P x", simp_all add: execute_assert success_def)
+
+lemma assert_cong [fundef_cong]:
+  assumes "P = P'"
+  assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
+  shows "(assert P x >>= f) = (assert P' x >>= f')"
+  by (rule SM_eqI) (insert assms, simp add: assert_def)
+
+
+subsubsection {* Plain lifting *}
+
+definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b, 'state) SM" where
+  "lift f = return o f"
+
+lemma lift_collapse [simp]:
+  "lift f x = return (f x)"
+  by (simp add: lift_def)
+
+lemma bind_lift:
+  "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
+  by (simp add: lift_def comp_def)
+
+
+subsubsection {* Iteration -- warning: this is rarely useful! *}
+
+primrec fold_map :: "('a \<Rightarrow> ('b, 'state) SM) \<Rightarrow> 'a list \<Rightarrow> ('b list, 'state) SM" where
+  "fold_map f [] = return []"
+| "fold_map f (x # xs) = do {
+     y \<leftarrow> f x;
+     ys \<leftarrow> fold_map f xs;
+     return (y # ys)
+   }"
+
+lemma fold_map_append:
+  "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
+  by (induct xs) simp_all
+
+lemma execute_fold_map_unchanged_heap [execute_simps]:
+  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
+  shows "execute (fold_map f xs) h =
+    Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
+using assms proof (induct xs)
+  case Nil show ?case by (simp add: execute_simps)
+next
+  case (Cons x xs)
+  from Cons.prems obtain y
+    where y: "execute (f x) h = Some (y, h)" by auto
+  moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
+    Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
+  ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
+qed
+
+
+subsection {* Partial function definition setup *}
+
+definition SM_ord :: "('a, 'state) SM \<Rightarrow> ('a, 'state) SM \<Rightarrow> bool" where
+  "SM_ord = img_ord execute (fun_ord option_ord)"
+
+definition SM_lub :: "('a , 'state) SM set \<Rightarrow> ('a, 'state) SM" where
+  "SM_lub = img_lub execute SM (fun_lub (flat_lub None))"
+
+interpretation sm!: partial_function_definitions SM_ord SM_lub
+proof -
+  have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"
+    by (rule partial_function_lift) (rule flat_interpretation)
+  then have "partial_function_definitions (img_ord execute (fun_ord option_ord))
+      (img_lub execute SM (fun_lub (flat_lub None)))"
+    by (rule partial_function_image) (auto intro: SM_eqI)
+  then show "partial_function_definitions SM_ord SM_lub"
+    by (simp only: SM_ord_def SM_lub_def)
+qed
+
+declaration {* Partial_Function.init "sm" @{term sm.fixp_fun}
+  @{term sm.mono_body} @{thm sm.fixp_rule_uc} @{thm sm.fixp_induct_uc}  NONE *}
+
+
+abbreviation "mono_SM \<equiv> monotone (fun_ord SM_ord) SM_ord"
+
+lemma SM_ordI:
+  assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"
+  shows  "SM_ord x y"
+  using assms unfolding SM_ord_def img_ord_def fun_ord_def flat_ord_def
+  by blast
+
+lemma SM_ordE:
+  assumes "SM_ord x y"
+  obtains "execute x h = None" | "execute x h = execute y h"
+  using assms unfolding SM_ord_def img_ord_def fun_ord_def flat_ord_def
+  by atomize_elim blast
+
+lemma bind_mono [partial_function_mono]:
+  assumes mf: "mono_SM B" and mg: "\<And>y. mono_SM (\<lambda>f. C y f)"
+  shows "mono_SM (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
+proof (rule monotoneI)
+  fix f g :: "'a \<Rightarrow> ('b, 'c) SM" assume fg: "fun_ord SM_ord f g"
+  from mf
+  have 1: "SM_ord (B f) (B g)" by (rule monotoneD) (rule fg)
+  from mg
+  have 2: "\<And>y'. SM_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
+
+  have "SM_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
+    (is "SM_ord ?L ?R")
+  proof (rule SM_ordI)
+    fix h
+    from 1 show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+      by (rule SM_ordE[where h = h]) (auto simp: execute_bind_case)
+  qed
+  also
+  have "SM_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
+    (is "SM_ord ?L ?R")
+  proof (rule SM_ordI)
+    fix h
+    show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+    proof (cases "execute (B g) h")
+      case None
+      then have "execute ?L h = None" by (auto simp: execute_bind_case)
+      thus ?thesis ..
+    next
+      case Some
+      then obtain r h' where "execute (B g) h = Some (r, h')"
+        by (metis surjective_pairing)
+      then have "execute ?L h = execute (C r f) h'"
+        "execute ?R h = execute (C r g) h'"
+        by (auto simp: execute_bind_case)
+      with 2[of r] show ?thesis by (auto elim: SM_ordE)
+    qed
+  qed
+  finally (sm.leq_trans)
+  show "SM_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
+qed
+
+end
\ No newline at end of file
diff -r 6c722e960f2e -r 38cef5407d82 thys/TM_Assemble.thy
--- a/thys/TM_Assemble.thy	Fri Mar 21 13:49:20 2014 +0000
+++ b/thys/TM_Assemble.thy	Fri Mar 21 15:07:59 2014 +0000
@@ -868,7 +868,7 @@
       assume h[rule_format]:
         "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = i"
       from h1 h3 have p1: "l < length (sts' - sts)"
-        by (metis length_list_update min_max.inf.idem minus_list_len)
+        by (metis length_list_update min.idem minus_list_len)
       from p1 h2 h3 have p2: "(sts' - sts)!l = Bound"
         by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus)
       from h[OF p1 p2] have "(<(i = x ! l)>) 0" 
@@ -1674,7 +1674,7 @@
 proof(induct rule:nth_equalityI)
   case 1
   show ?case
-    by (metis min_max.inf.commute plus_list_len)
+    by (metis min.commute plus_list_len)
 next
   case 2
   { fix i