diff --git a/thys/CAVA_Automata/Digraph_Basic.thy b/thys/CAVA_Automata/Digraph_Basic.thy
--- a/thys/CAVA_Automata/Digraph_Basic.thy
+++ b/thys/CAVA_Automata/Digraph_Basic.thy
@@ -1,695 +1,692 @@
 section \<open>Relations interpreted as Directed Graphs\<close>
 theory Digraph_Basic
 imports   
   "Automatic_Refinement.Misc"
   "Automatic_Refinement.Refine_Util"
   "HOL-Library.Omega_Words_Fun"
 begin
 
 text \<open>
   This theory contains some basic graph theory on directed graphs which are 
   modeled as a relation between nodes. 
 
   The theory here is very fundamental, and 
   also used by non-directly graph-related applications like the theory of 
   tail-recursion in the Refinement Framework. Thus, we decided to put it 
   in the basic theories of the refinement framework.
 \<close>
 
 
 text \<open>Directed graphs are modeled as a relation on nodes\<close>
 type_synonym 'v digraph = "('v\<times>'v) set"
 
 locale digraph = fixes E :: "'v digraph"
 
 subsection \<open>Paths\<close>
 text \<open>Path are modeled as list of nodes, the last node of a path is not included
   into the list. This formalization allows for nice concatenation and splitting
   of paths.\<close>
 inductive path :: "'v digraph \<Rightarrow> 'v \<Rightarrow> 'v list \<Rightarrow> 'v \<Rightarrow> bool" for E where
   path0: "path E u [] u"
 | path_prepend: "\<lbrakk> (u,v)\<in>E; path E v l w \<rbrakk> \<Longrightarrow> path E u (u#l) w"
 
 lemma path1: "(u,v)\<in>E \<Longrightarrow> path E u [u] v"
   by (auto intro: path.intros)
 
 lemma path_empty_conv[simp]:
   "path E u [] v \<longleftrightarrow> u=v"
   by (auto intro: path0 elim: path.cases)
 
 inductive_cases path_uncons: "path E u (u'#l) w"
 inductive_simps path_cons_conv: "path E u (u'#l) w"
 
 lemma path_no_edges[simp]: "path {} u p v \<longleftrightarrow> (u=v \<and> p=[])"
   by (cases p) (auto simp: path_cons_conv)
 
 lemma path_conc: 
   assumes P1: "path E u la v" 
   assumes P2: "path E v lb w"
   shows "path E u (la@lb) w"
   using P1 P2 apply induct 
   by (auto intro: path.intros)
   
 lemma path_append:
   "\<lbrakk> path E u l v; (v,w)\<in>E \<rbrakk> \<Longrightarrow> path E u (l@[v]) w"
   using path_conc[OF _ path1] .
 
 lemma path_unconc:
   assumes "path E u (la@lb) w"
   obtains v where "path E u la v" and "path E v lb w"
   using assms 
   thm path.induct
   apply (induct u "la@lb" w arbitrary: la lb rule: path.induct)
   apply (auto intro: path.intros elim!: list_Cons_eq_append_cases)
   done
 
 lemma path_conc_conv: 
   "path E u (la@lb) w \<longleftrightarrow> (\<exists>v. path E u la v \<and> path E v lb w)"
   by (auto intro: path_conc elim: path_unconc)
 
 lemma (in -) path_append_conv: "path E u (p@[v]) w \<longleftrightarrow> (path E u p v \<and> (v,w)\<in>E)"
   by (simp add: path_cons_conv path_conc_conv)
 
 lemmas path_simps = path_empty_conv path_cons_conv path_conc_conv
 
 
 lemmas path_trans[trans] = path_prepend path_conc path_append
 lemma path_from_edges: "\<lbrakk>(u,v)\<in>E; (v,w)\<in>E\<rbrakk> \<Longrightarrow> path E u [u] v" 
   by (auto simp: path_simps)
 
 
 lemma path_edge_cases[case_names no_use split]: 
   assumes "path (insert (u,v) E) w p x"
   obtains 
     "path E w p x" 
   | p1 p2 where "path E w p1 u" "path (insert (u,v) E) v p2 x"
   using assms
   apply induction
   apply simp
   apply (clarsimp)
   apply (metis path_simps path_cons_conv)
   done
 
 lemma path_edge_rev_cases[case_names no_use split]: 
   assumes "path (insert (u,v) E) w p x"
   obtains 
     "path E w p x" 
   | p1 p2 where "path (insert (u,v) E) w p1 u" "path E v p2 x"
   using assms
   apply (induction p arbitrary: x rule: rev_induct)
   apply simp
   apply (clarsimp simp: path_cons_conv path_conc_conv)
   apply (metis path_simps path_append_conv)
   done
 
 
 lemma path_mono: 
   assumes S: "E\<subseteq>E'" 
   assumes P: "path E u p v" 
   shows "path E' u p v"
   using P
   apply induction
   apply simp
   using S
   apply (auto simp: path_cons_conv)
   done
 
 lemma path_is_rtrancl: 
   assumes "path E u l v"
   shows "(u,v)\<in>E\<^sup>*"
   using assms 
   by induct auto
 
 lemma rtrancl_is_path:
   assumes "(u,v)\<in>E\<^sup>*"
   obtains l where "path E u l v"
   using assms 
   by induct (auto intro: path0 path_append)
 
 lemma path_is_trancl: 
   assumes "path E u l v"
   and "l\<noteq>[]"
   shows "(u,v)\<in>E\<^sup>+"
   using assms 
   apply induct
   apply auto []
   apply (case_tac l)
   apply auto
   done
 
 lemma trancl_is_path:
   assumes "(u,v)\<in>E\<^sup>+"
   obtains l where "l\<noteq>[]" and "path E u l v"
   using assms 
   by induct (auto intro: path0 path_append)
 
 lemma path_nth_conv: "path E u p v \<longleftrightarrow> (let p'=p@[v] in
   u=p'!0 \<and>
   (\<forall>i<length p' - 1. (p'!i,p'!Suc i)\<in>E))"
   apply (induct p arbitrary: v rule: rev_induct)
   apply (auto simp: path_conc_conv path_cons_conv nth_append)
   done
 
 lemma path_mapI:
   assumes "path E u p v"
   shows "path (pairself f ` E) (f u) (map f p) (f v)"
   using assms
   apply induction
   apply (simp)
   apply (force simp: path_cons_conv)
   done
 
 lemma path_restrict: 
   assumes "path E u p v" 
   shows "path (E \<inter> set p \<times> insert v (set (tl p))) u p v"
   using assms
 proof induction
   print_cases
   case (path_prepend u v p w)
   from path_prepend.IH have "path (E \<inter> set (u#p) \<times> insert w (set p)) v p w"
     apply (rule path_mono[rotated])
     by (cases p) auto
   thus ?case using \<open>(u,v)\<in>E\<close>
     by (cases p) (auto simp add: path_cons_conv)
 qed auto
 
 lemma path_restrict_closed:
   assumes CLOSED: "E``D \<subseteq> D"
   assumes I: "v\<in>D" and P: "path E v p v'"
   shows "path (E\<inter>D\<times>D) v p v'"
   using P CLOSED I
   by induction (auto simp: path_cons_conv)
 
 
 lemma path_set_induct:
   assumes "path E u p v" and "u\<in>I" and "E``I \<subseteq> I"
   shows "set p \<subseteq> I"
   using assms
   by (induction rule: path.induct) auto
 
 lemma path_nodes_reachable: "path E u p v \<Longrightarrow> insert v (set p) \<subseteq> E\<^sup>*``{u}"
   apply (auto simp: in_set_conv_decomp path_cons_conv path_conc_conv)
   apply (auto dest!: path_is_rtrancl)
   done
 
 lemma path_nodes_edges: "path E u p v \<Longrightarrow> set p \<subseteq> fst`E"
   by (induction rule: path.induct) auto
 
 lemma path_tl_nodes_edges: 
   assumes "path E u p v"
   shows "set (tl p) \<subseteq> fst`E \<inter> snd`E"
 proof -
   from path_nodes_edges[OF assms] have "set (tl p) \<subseteq> fst`E"
     by (cases p) auto
 
   moreover have "set (tl p) \<subseteq> snd`E"
     using assms
     apply (cases)
     apply simp
     apply simp
     apply (erule path_set_induct[where I = "snd`E"])
     apply auto
     done
   ultimately show ?thesis
     by auto
 qed
 
 lemma path_loop_shift: 
   assumes P: "path E u p u"
   assumes S: "v\<in>set p"
   obtains p' where "set p' = set p" "path E v p' v"
 proof -
   from S obtain p1 p2 where [simp]: "p = p1@v#p2" by (auto simp: in_set_conv_decomp)
   from P obtain v' where A: "path E u p1 v" "(v, v') \<in> E" "path E v' p2 u" 
     by (auto simp: path_simps)
   hence "path E v (v#p2@p1) v" by (auto simp: path_simps)
   thus ?thesis using that[of "v#p2@p1"] by auto
 qed
 
 lemma path_hd:
   assumes "p \<noteq> []" "path E v p w"
   shows "hd p = v"
   using assms
   by (auto simp: path_cons_conv neq_Nil_conv)
 
 
 lemma path_last_is_edge:
   assumes "path E x p y"
   and "p \<noteq> []"
   shows "(last p, y) \<in> E"
   using assms
   by (auto simp: neq_Nil_rev_conv path_simps)
 
 lemma path_member_reach_end:
   assumes P: "path E x p y"
   and v: "v \<in> set p"
   shows "(v,y) \<in> E\<^sup>+"
   using assms 
   by (auto intro!: path_is_trancl simp: in_set_conv_decomp path_simps)
 
 lemma path_tl_induct[consumes 2, case_names single step]:
   assumes P: "path E x p y"
   and NE: "x \<noteq> y"
   and S: "\<And>u. (x,u) \<in> E \<Longrightarrow> P x u"
   and ST: "\<And>u v. \<lbrakk>(x,u) \<in> E\<^sup>+; (u,v) \<in> E; P x u\<rbrakk> \<Longrightarrow> P x v"
   shows "P x y \<and> (\<forall> v \<in> set (tl p). P x v)"
 proof -
   from P NE have "p \<noteq> []" by auto
   thus ?thesis using P
   proof (induction p arbitrary: y rule: rev_nonempty_induct)
     case (single u) hence "(x,y) \<in> E" by (simp add: path_cons_conv)
     with S show ?case by simp
   next
     case (snoc u us) hence "path E x us u" by (simp add: path_append_conv)
     with snoc path_is_trancl have 
       "P x u" "(x,u) \<in> E\<^sup>+" "\<forall>v \<in> set (tl us). P x v" 
       by simp_all
     moreover with snoc have "\<forall>v \<in> set (tl (us@[u])). P x v" by simp
     moreover from snoc have "(u,y) \<in> E" by (simp add: path_append_conv)
     ultimately show ?case by (auto intro: ST)
   qed
 qed
 
 
 lemma path_restrict_tl: 
   "\<lbrakk> u\<notin>R; path (E \<inter> UNIV \<times> -R) u p v \<rbrakk> \<Longrightarrow> path (rel_restrict E R) u p v"
   apply (induction p arbitrary: u)
   apply (auto simp: path_simps rel_restrict_def)
   done
 
 lemma path1_restr_conv: "path (E\<inter>UNIV \<times> -R) u (x#xs) v 
   \<longleftrightarrow> (\<exists>w. w\<notin>R \<and> x=u \<and> (u,w)\<in>E \<and> path (rel_restrict E R) w xs v)"
 proof -
   have 1: "rel_restrict E R \<subseteq> E \<inter> UNIV \<times> - R" by (auto simp: rel_restrict_def)
 
   show ?thesis
     by (auto simp: path_simps intro: path_restrict_tl path_mono[OF 1])
 qed
 
 
 
 lemma dropWhileNot_path:
   assumes "p \<noteq> []"
   and "path E w p x"
   and "v \<in> set p"
   and "dropWhile ((\<noteq>) v) p = c"
   shows "path E v c x"
   using assms
 proof (induction arbitrary: w c rule: list_nonempty_induct)
   case (single p) thus ?case by (auto simp add: path_simps)
 next
   case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
   show ?case
   proof (cases "p=v")
     case True with cons show ?thesis by simp
   next
     case False with cons have "c = dropWhile ((\<noteq>) v) ps" by simp
     moreover from cons.prems obtain y where "path E y ps x" 
       using path_uncons by metis
     moreover from cons.prems False have "v \<in> set ps" by simp
     ultimately show ?thesis using cons.IH by metis
   qed
 qed
 
 lemma takeWhileNot_path:
   assumes "p \<noteq> []"
   and "path E w p x"
   and "v \<in> set p"
   and "takeWhile ((\<noteq>) v) p = c"
   shows "path E w c v"
   using assms
 proof (induction arbitrary: w c rule: list_nonempty_induct)
   case (single p) thus ?case by (auto simp add: path_simps)
 next
   case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
   show ?case
   proof (cases "p=v")
     case True with cons show ?thesis by simp
   next
     case False with cons obtain c' where 
       "c' = takeWhile ((\<noteq>) v) ps" and 
       [simp]: "c = p#c'"
       by simp_all
     moreover from cons.prems obtain y where 
       "path E y ps x" and "(w,y) \<in> E" 
       using path_uncons by metis+
     moreover from cons.prems False have "v \<in> set ps" by simp
     ultimately have "path E y c' v" using cons.IH by metis
     with \<open>(w,y) \<in> E\<close> show ?thesis by (auto simp add: path_cons_conv)
   qed
 qed
 
 
 subsection \<open>Infinite Paths\<close>
 definition ipath :: "'q digraph \<Rightarrow> 'q word \<Rightarrow> bool"
   \<comment> \<open>Predicate for an infinite path in a digraph\<close>
   where "ipath E r \<equiv> \<forall>i. (r i, r (Suc i))\<in>E"
 
 
 lemma ipath_conc_conv: 
   "ipath E (u \<frown> v) \<longleftrightarrow> (\<exists>a. path E a u (v 0) \<and> ipath E v)"
   apply (auto simp: conc_def ipath_def path_nth_conv nth_append)
   apply (metis add_Suc_right diff_add_inverse not_add_less1)
   by (metis Suc_diff_Suc diff_Suc_Suc not_less_eq)
 
 lemma ipath_iter_conv:
   assumes "p\<noteq>[]"
   shows "ipath E (p\<^sup>\<omega>) \<longleftrightarrow> (path E (hd p) p (hd p))"
 proof (cases p)
   case Nil thus ?thesis using assms by simp
 next
   case (Cons u p') hence PLEN: "length p > 0" by simp
   show ?thesis proof 
     assume "ipath E (iter (p))"
     hence "\<forall>i. (iter (p) i, iter (p) (Suc i)) \<in> E"
       unfolding ipath_def by simp
     hence "(\<forall>i<length p. (p!i,(p@[hd p])!Suc i)\<in>E)" 
       apply (simp add: assms)
       apply safe
       apply (drule_tac x=i in spec)
       apply simp
       apply (case_tac "Suc i = length p")
       apply (simp add: Cons)
       apply (simp add: nth_append)
       done
     thus "path E (hd p) p (hd p)"
       by (auto simp: path_nth_conv Cons nth_append nth_Cons')
   next
     assume "path E (hd p) p (hd p)"
     thus "ipath E (iter p)"
       apply (auto simp: path_nth_conv ipath_def assms Let_def)
       apply (drule_tac x="i mod length p" in spec)
       apply (auto simp: nth_append assms split: if_split_asm)
       apply (metis less_not_refl mod_Suc)
       by (metis PLEN diff_self_eq_0 mod_Suc nth_Cons_0 mod_less_divisor)
   qed
 qed
 
 lemma ipath_to_rtrancl:
   assumes R: "ipath E r"
   assumes I: "i1\<le>i2"
   shows "(r i1,r i2)\<in>E\<^sup>*"
   using I
 proof (induction i2)
   case (Suc i2)
   show ?case proof (cases "i1=Suc i2")
     assume "i1\<noteq>Suc i2"
     with Suc have "(r i1,r i2)\<in>E\<^sup>*" by auto
     also from R have "(r i2,r (Suc i2))\<in>E" unfolding ipath_def by auto
     finally show ?thesis .
   qed simp
 qed simp
     
 lemma ipath_to_trancl:
   assumes R: "ipath E r"
   assumes I: "i1<i2"
   shows "(r i1,r i2)\<in>E\<^sup>+"
 proof -
   from R have "(r i1,r (Suc i1))\<in>E"
     by (auto simp: ipath_def)
   also have "(r (Suc i1),r i2)\<in>E\<^sup>*"
     using ipath_to_rtrancl[OF R,of "Suc i1" i2] I by auto
   finally (rtrancl_into_trancl2) show ?thesis .
 qed
 
 lemma run_limit_two_connectedI:
   assumes A: "ipath E r" 
   assumes B: "a \<in> limit r" "b\<in>limit r"
   shows "(a,b)\<in>E\<^sup>+"
 proof -
   from B have "{a,b} \<subseteq> limit r" by simp
   with A show ?thesis
     by (metis ipath_to_trancl two_in_limit_iff)
 qed
 
 
 lemma ipath_subpath:
   assumes P: "ipath E r"
   assumes LE: "l\<le>u"
   shows "path E (r l) (map r [l..<u]) (r u)"
   using LE
 proof (induction "u-l" arbitrary: u l)
   case (Suc n)
   note IH=Suc.hyps(1)
   from \<open>Suc n = u-l\<close> \<open>l\<le>u\<close> obtain u' where [simp]: "u=Suc u'" 
     and A: "n=u'-l" "l \<le> u'" 
     by (cases u) auto
     
   note IH[OF A]
   also from P have "(r u',r u)\<in>E"
     by (auto simp: ipath_def)
   finally show ?case using \<open>l \<le> u'\<close> by (simp add: upt_Suc_append)
 qed auto  
 
 lemma ipath_restrict_eq: "ipath (E \<inter> (E\<^sup>*``{r 0} \<times> E\<^sup>*``{r 0})) r \<longleftrightarrow> ipath E r"
   unfolding ipath_def
   by (auto simp: relpow_fun_conv rtrancl_power)
 lemma ipath_restrict: "ipath E r \<Longrightarrow> ipath (E \<inter> (E\<^sup>*``{r 0} \<times> E\<^sup>*``{r 0})) r"
   by (simp add: ipath_restrict_eq)
 
 
 lemma ipathI[intro?]: "\<lbrakk>\<And>i. (r i, r (Suc i)) \<in> E\<rbrakk> \<Longrightarrow> ipath E r"
   unfolding ipath_def by auto
 
 lemma ipathD: "ipath E r \<Longrightarrow> (r i, r (Suc i)) \<in> E"
   unfolding ipath_def by auto
 
 lemma ipath_in_Domain: "ipath E r \<Longrightarrow> r i \<in> Domain E"
   unfolding ipath_def by auto
 
 lemma ipath_in_Range: "\<lbrakk>ipath E r; i\<noteq>0\<rbrakk> \<Longrightarrow> r i \<in> Range E"
   unfolding ipath_def by (cases i) auto
 
 lemma ipath_suffix: "ipath E r \<Longrightarrow> ipath E (suffix i r)"
   unfolding suffix_def ipath_def by auto
 
 subsection \<open>Strongly Connected Components\<close>
 
 text \<open>A strongly connected component is a maximal mutually connected set 
   of nodes\<close>
 definition is_scc :: "'q digraph \<Rightarrow> 'q set \<Rightarrow> bool"
   where "is_scc E U \<longleftrightarrow> U\<times>U\<subseteq>E\<^sup>* \<and> (\<forall>V. V\<supset>U \<longrightarrow> \<not> (V\<times>V\<subseteq>E\<^sup>*))"
 
 lemma scc_non_empty[simp]: "\<not>is_scc E {}" unfolding is_scc_def by auto
 
 lemma scc_non_empty'[simp]: "is_scc E U \<Longrightarrow> U\<noteq>{}" unfolding is_scc_def by auto
 
 lemma is_scc_closed: 
   assumes SCC: "is_scc E U"
   assumes MEM: "x\<in>U"
   assumes P: "(x,y)\<in>E\<^sup>*" "(y,x)\<in>E\<^sup>*"
   shows "y\<in>U"
 proof -
   from SCC MEM P have "insert y U \<times> insert y U \<subseteq> E\<^sup>*"
     unfolding is_scc_def
     apply clarsimp
     apply rule
     apply clarsimp_all
     apply (erule disjE1)
     apply clarsimp
     apply (metis in_mono mem_Sigma_iff rtrancl_trans)
     apply auto []
-    apply (erule disjE1)
-    apply clarsimp
     apply (metis in_mono mem_Sigma_iff rtrancl_trans)
-    apply auto []
     done
   with SCC show ?thesis unfolding is_scc_def by blast
 qed
 
 lemma is_scc_connected:
   assumes SCC: "is_scc E U"
   assumes MEM: "x\<in>U" "y\<in>U"
   shows "(x,y)\<in>E\<^sup>*"
   using assms unfolding is_scc_def by auto
 
 text \<open>In the following, we play around with alternative characterizations, and
   prove them all equivalent .\<close>
 
 text \<open>A common characterization is to define an equivalence relation 
   ,,mutually connected'' on nodes, and characterize the SCCs as its 
   equivalence classes:\<close>
 
 definition mconn :: "('a\<times>'a) set \<Rightarrow> ('a \<times> 'a) set"
   \<comment> \<open>Mutually connected relation on nodes\<close>
   where "mconn E = E\<^sup>* \<inter> (E\<inverse>)\<^sup>*"
 
 lemma mconn_pointwise:
    "mconn E = {(u,v). (u,v)\<in>E\<^sup>* \<and> (v,u)\<in>E\<^sup>*}"
   by (auto simp add: mconn_def rtrancl_converse)
 
 text \<open>\<open>mconn\<close> is an equivalence relation:\<close>
 lemma mconn_refl[simp]: "Id\<subseteq>mconn E"
   by (auto simp add: mconn_def)
 
 lemma mconn_sym: "mconn E = (mconn E)\<inverse>"
   by (auto simp add: mconn_pointwise)
 
 lemma mconn_trans: "mconn E O mconn E = mconn E"
   by (auto simp add: mconn_def)
 
 lemma mconn_refl': "refl (mconn E)"
   by (auto intro: refl_onI simp: mconn_pointwise)
 
 lemma mconn_sym': "sym (mconn E)"
   by (auto intro: symI simp: mconn_pointwise)
 
 lemma mconn_trans': "trans (mconn E)"
   by (metis mconn_def trans_Int trans_rtrancl)
 
 lemma mconn_equiv: "equiv UNIV (mconn E)"
   using mconn_refl' mconn_sym' mconn_trans'
   by (rule equivI)
 
 
 lemma is_scc_mconn_eqclasses: "is_scc E U \<longleftrightarrow> U \<in> UNIV // mconn E"
   \<comment> \<open>The strongly connected components are the equivalence classes of the 
     mutually-connected relation on nodes\<close>
 proof
   assume A: "is_scc E U"
   then obtain x where "x\<in>U" unfolding is_scc_def by auto
   hence "U = mconn E `` {x}" using A
     unfolding mconn_pointwise is_scc_def
     apply clarsimp
     apply rule
     apply auto []
     apply clarsimp
     by (metis A is_scc_closed)
   thus "U \<in> UNIV // mconn E"
     by (auto simp: quotient_def)
 next
   assume "U \<in> UNIV // mconn E"
   thus "is_scc E U"
     by (auto simp: is_scc_def mconn_pointwise quotient_def)
 qed
 
 (* For presentation in the paper *)
 lemma "is_scc E U \<longleftrightarrow> U \<in> UNIV // (E\<^sup>* \<inter> (E\<inverse>)\<^sup>*)"
   unfolding is_scc_mconn_eqclasses mconn_def by simp
 
 text \<open>We can also restrict the notion of "reachability" to nodes
   inside the SCC
 \<close>
 
 lemma find_outside_node:
   assumes "(u,v)\<in>E\<^sup>*"
   assumes "(u,v)\<notin>(E\<inter>U\<times>U)\<^sup>*"
   assumes "u\<in>U" "v\<in>U"
   shows "\<exists>u'. u'\<notin>U \<and> (u,u')\<in>E\<^sup>* \<and> (u',v)\<in>E\<^sup>*"
   using assms
   apply (induction)
   apply auto []
   apply clarsimp
   by (metis IntI mem_Sigma_iff rtrancl.simps)
 
 lemma is_scc_restrict1:
   assumes SCC: "is_scc E U"
   shows "U\<times>U\<subseteq>(E\<inter>U\<times>U)\<^sup>*"
   using assms
   unfolding is_scc_def
   apply clarsimp
   apply (rule ccontr)
   apply (drule (2) find_outside_node[rotated])
   apply auto []
   by (metis is_scc_closed[OF SCC] mem_Sigma_iff rtrancl_trans subsetD)
 
 lemma is_scc_restrict2:
   assumes SCC: "is_scc E U"
   assumes "V\<supset>U"
   shows "\<not> (V\<times>V\<subseteq>(E\<inter>V\<times>V)\<^sup>*)"
   using assms
   unfolding is_scc_def
   apply clarsimp
   using rtrancl_mono[of "E \<inter> V \<times> V" "E"]
   apply clarsimp
   apply blast
   done
 
 lemma is_scc_restrict3: 
   assumes SCC: "is_scc E U"
   shows "((E\<^sup>*``((E\<^sup>*``U) - U)) \<inter> U = {})"
   apply auto
   by (metis assms is_scc_closed is_scc_connected rtrancl_trans)
   
 lemma is_scc_alt_restrict_path:
   "is_scc E U \<longleftrightarrow> U\<noteq>{} \<and>
     (U\<times>U \<subseteq> (E\<inter>U\<times>U)\<^sup>*) \<and> ((E\<^sup>*``((E\<^sup>*``U) - U)) \<inter> U = {})"
   apply rule
   apply (intro conjI)
   apply simp
   apply (blast dest: is_scc_restrict1)
   apply (blast dest: is_scc_restrict3)
   
   unfolding is_scc_def
   apply rule
   apply clarsimp
   apply (metis (full_types) Int_lower1 in_mono mem_Sigma_iff rtrancl_mono_mp)
   apply blast
   done
 
 lemma is_scc_pointwise:
   "is_scc E U \<longleftrightarrow> 
     U\<noteq>{}
   \<and> (\<forall>u\<in>U. \<forall>v\<in>U. (u,v)\<in>(E\<inter>U\<times>U)\<^sup>*) 
   \<and> (\<forall>u\<in>U. \<forall>v. (v\<notin>U \<and> (u,v)\<in>E\<^sup>*) \<longrightarrow> (\<forall>u'\<in>U. (v,u')\<notin>E\<^sup>*))"
   \<comment> \<open>Alternative, pointwise characterization\<close>
   unfolding is_scc_alt_restrict_path
   by blast  
 
 lemma is_scc_unique:
   assumes SCC: "is_scc E scc" "is_scc E scc'"
   and v: "v \<in> scc" "v \<in> scc'"
   shows "scc = scc'"
 proof -
   from SCC have "scc = scc' \<or> scc \<inter> scc' = {}"
     using quotient_disj[OF mconn_equiv]
     by (simp add: is_scc_mconn_eqclasses)
   with v show ?thesis by auto
 qed
 
 lemma is_scc_ex1:
   "\<exists>!scc. is_scc E scc \<and> v \<in> scc"
 proof (rule ex1I, rule conjI)
   let ?scc = "mconn E `` {v}"
   have "?scc \<in> UNIV // mconn E" by (auto intro: quotientI)
   thus "is_scc E ?scc" by (simp add: is_scc_mconn_eqclasses)
   moreover show "v \<in> ?scc" by (blast intro: refl_onD[OF mconn_refl'])
   ultimately show "\<And>scc. is_scc E scc \<and> v \<in> scc \<Longrightarrow> scc = ?scc"
     by (metis is_scc_unique)
 qed
 
 lemma is_scc_ex:
   "\<exists>scc. is_scc E scc \<and> v \<in> scc"
   by (metis is_scc_ex1)
 
 lemma is_scc_connected':
   "\<lbrakk>is_scc E scc; x \<in> scc; y \<in> scc\<rbrakk> \<Longrightarrow> (x,y)\<in>(Restr E scc)\<^sup>*"
   unfolding is_scc_pointwise
   by blast
 
 definition scc_of :: "('v\<times>'v) set \<Rightarrow> 'v \<Rightarrow> 'v set"
   where
   "scc_of E v = (THE scc. is_scc E scc \<and> v \<in> scc)"
 
 lemma scc_of_is_scc[simp]:
   "is_scc E (scc_of E v)"
   using is_scc_ex1[of E v]
   by (auto dest!: theI' simp: scc_of_def)
 
 lemma node_in_scc_of_node[simp]:
   "v \<in> scc_of E v"
   using is_scc_ex1[of E v]
   by (auto dest!: theI' simp: scc_of_def)
 
 lemma scc_of_unique:
   assumes "w \<in> scc_of E v"
   shows "scc_of E v = scc_of E w"
 proof -
   have "is_scc E (scc_of E v)" by simp
   moreover note assms
   moreover have "is_scc E (scc_of E w)" by simp
   moreover have "w \<in> scc_of E w" by simp
   ultimately show ?thesis using is_scc_unique by metis
 qed
 
 end
diff --git a/thys/Statecharts/HAOps.thy b/thys/Statecharts/HAOps.thy
--- a/thys/Statecharts/HAOps.thy
+++ b/thys/Statecharts/HAOps.thy
@@ -1,1117 +1,1111 @@
 (*  Title:      statecharts/HA/HAOps.thy
     Author:     Steffen Helke, Software Engineering Group
     Copyright   2010 Technische Universitaet Berlin
 *)
 
 section \<open>Constructing Hierarchical Automata\<close>
 theory HAOps
 imports HA
 begin
 
 subsection "Constructing a Composition Function for a PseudoHA"
 
 definition
   EmptyMap :: "'s set => ('s \<rightharpoonup> (('s,'e,'d)seqauto) set)" where
   "EmptyMap S = (\<lambda> a . if a \<in> S then Some {} else None)"
 
 lemma EmptyMap_dom [simp]:
   "dom (EmptyMap S) = S"
 by (unfold dom_def EmptyMap_def,auto)
 
 lemma EmptyMap_ran [simp]:
    "S \<noteq> {} \<Longrightarrow> ran (EmptyMap S) = {{}}"
 by (unfold ran_def EmptyMap_def, auto)
 
 lemma EmptyMap_the [simp]:
    "x \<in> S \<Longrightarrow> the ((EmptyMap S) x) = {}"
 by (unfold ran_def EmptyMap_def, auto)
 
 lemma EmptyMap_ran_override:
   "\<lbrakk> S \<noteq> {}; (S \<inter> (dom G)) = {} \<rbrakk> \<Longrightarrow>  
   ran (G ++ EmptyMap S) = insert {} (ran G)"
 apply (subst ran_override)
 apply (simp add: Int_commute)
 apply simp
 done
 
 lemma EmptyMap_Union_ran_override:
  "\<lbrakk> S \<noteq> {};  
     S \<inter> dom G = {} \<rbrakk> \<Longrightarrow>  
   (Union (ran (G ++ (EmptyMap S)))) = (Union (ran G))"
 apply (subst EmptyMap_ran_override)
 apply auto
 done
 
 lemma EmptyMap_Union_ran_override2:
  "\<lbrakk> S \<noteq> {}; S \<inter> dom G1 = {}; 
     dom G1 \<inter> dom G2 = {} \<rbrakk> \<Longrightarrow> 
    \<Union> (ran (G1 ++ EmptyMap S ++ G2)) = (\<Union> (ran G1 \<union> ran G2))"
 apply (unfold Union_eq UNION_eq EmptyMap_def Int_def ran_def)
 apply (simp add: map_add_Some_iff)
 apply (unfold dom_def)
 apply simp
 apply (rule equalityI)
 apply (rule subsetI)
 apply simp
 apply fast
 apply (rule subsetI)
 apply (rename_tac t)
 apply simp
 apply (erule bexE)
 apply (rename_tac U)
 apply simp
 apply (erule disjE)
 apply (erule exE)
 apply (rename_tac v)
 apply (rule_tac x=U in exI)
 apply simp
 apply (rule_tac x=v in exI)
 apply auto
 done
 
 lemma EmptyMap_Root [simp]:
  "Root {SA} (EmptyMap (States SA)) = SA"
 by (unfold Root_def, auto)
 
 lemma EmptyMap_RootEx [simp]:
   "RootEx {SA} (EmptyMap (States SA))"
 by (unfold RootEx_def, auto)
 
 lemma EmptyMap_OneAncestor [simp]:
  "OneAncestor {SA} (EmptyMap (States SA))"
 by (unfold OneAncestor_def, auto)
 
 lemma EmptyMap_NoCycles [simp]:
   "NoCycles {SA} (EmptyMap (States SA))"
 by (unfold NoCycles_def EmptyMap_def , auto)
 
 lemma EmptyMap_IsCompFun [simp]:
  "IsCompFun {SA} (EmptyMap (States SA))"
 by (unfold IsCompFun_def, auto)
 
 lemma EmptyMap_hierauto [simp]:
  "(D,{SA}, SAEvents SA, EmptyMap (States SA)) \<in> hierauto"
 by (unfold hierauto_def HierAuto_def, auto)
 
 subsection "Extending a Composition Function by a SA"
 
 definition
   FAddSA :: "[('s \<rightharpoonup> (('s,'e,'d)seqauto) set), 's * ('s,'e,'d)seqauto]
              => ('s \<rightharpoonup> (('s,'e,'d)seqauto) set)"
            ("(_ [f+]/ _)" [10,11]10) where
   "FAddSA G SSA = (let  (S,SA) = SSA
                    in
                      (if ((S \<in> dom G) \<and> (S \<notin> States SA)) then
                         (G ++ (Map.empty(S \<mapsto> (insert SA (the (G S)))))
                          ++ EmptyMap (States SA))
                       else G))"
 
 lemma FAddSA_dom [simp]:
  "(S \<notin> (dom (A::('a => ('a,'c,'d)seqauto set option)))) \<Longrightarrow>
    ((A [f+] (S,(SA::('a,'c,'d)seqauto))) = A)"
 by (unfold FAddSA_def Let_def, auto)
 
 lemma FAddSA_States [simp]:
  "(S \<in> (States (SA::('a,'c,'d)seqauto))) \<Longrightarrow>
    (((A::('a => ('a,'c,'d)seqauto set option)) [f+] (S,SA)) = A)"
 by (unfold FAddSA_def Let_def, auto)
 
 lemma FAddSA_dom_insert [simp]:
  "\<lbrakk> S \<in> (dom A); S \<notin>  States SA \<rbrakk> \<Longrightarrow> 
    (((A [f+] (S,SA)) S) = Some (insert SA (the (A S))))"
 by (unfold FAddSA_def Let_def restrict_def, auto)
 
 lemma FAddSA_States_neq [simp]:
  "\<lbrakk> S' \<notin> States (SA::('a,'c,'d)seqauto); S \<noteq>  S' \<rbrakk> \<Longrightarrow> 
   ((((A::('a => ('a,'c,'d)seqauto set option)) [f+] (S,SA)) S') = (A S'))"
 apply (case_tac "S \<in> dom A")
 apply (case_tac "S \<in> States SA")
 apply auto
 apply (case_tac "S' \<in> dom A")
 apply (unfold FAddSA_def Let_def)
 apply auto
 apply (simp add: dom_None)
 done
 
 lemma FAddSA_dom_emptyset [simp]:
  "\<lbrakk> S \<in> (dom A); S \<notin> States SA; S' \<in> States (SA::('a,'c,'d)seqauto) \<rbrakk> \<Longrightarrow>  
     ((((A::('a => ('a,'c,'d)seqauto set option))) [f+] (S,SA)) S') = (Some {})"
 apply (unfold FAddSA_def Let_def)
 apply auto
 apply (unfold EmptyMap_def)
 apply auto
 done
 
 lemma FAddSA_dom_dom_States [simp]:
   "\<lbrakk> S \<in> (dom F); S \<notin> States SA \<rbrakk> \<Longrightarrow> 
     (dom ((F::('a \<rightharpoonup> (('a,'b,'d)seqauto) set)) [f+] (S, SA))) = 
     ((dom F) \<union> (States (SA::('a,'b,'d)seqauto)))"
 by (unfold FAddSA_def Let_def, auto)
 
 lemma FAddSA_dom_dom [simp]:
   "S \<notin> (dom F) \<Longrightarrow>   
    (dom ((F::('a \<rightharpoonup> (('a,'b,'d)seqauto) set)) [f+] 
        (S,(SA::('a,'b,'d)seqauto)))) = (dom F)"
 by (unfold FAddSA_def Let_def, auto)
 
 lemma FAddSA_States_dom [simp]:
   "S \<in> (States SA) \<Longrightarrow>  
    (dom ((F::('a \<rightharpoonup> (('a,'b,'d)seqauto) set)) [f+] 
         (S,(SA::('a,'b,'d)seqauto)))) = (dom F)"
 by (unfold FAddSA_def Let_def, auto)
 
 lemma FAddSA_dom_insert_dom_disjunct [simp]:
    "\<lbrakk> S \<in> dom G; States SA \<inter> dom G = {} \<rbrakk> \<Longrightarrow> ((G [f+] (S,SA)) S) = Some (insert SA (the (G S)))"
 apply (rule  FAddSA_dom_insert)
 apply auto
 done
 
 lemma FAddSA_Union_ran:
  "\<lbrakk> S \<in> dom G; (States SA) \<inter> (dom G) = {} \<rbrakk> \<Longrightarrow> 
    (\<Union> (ran (G [f+] (S,SA)))) = (insert SA (\<Union> (ran G)))"
 apply (unfold FAddSA_def Let_def)
 apply simp
 apply (rule conjI)
 prefer 2
 apply (rule impI)
 apply (unfold Int_def)
 apply simp
 apply (fold Int_def)
 apply (rule impI)
 apply (subst EmptyMap_Union_ran_override)
 apply auto
 done
 
 lemma FAddSA_Union_ran2:
  "\<lbrakk> S \<in> dom G1; (States SA) \<inter> (dom G1) = {}; (dom G1 \<inter> dom G2) = {} \<rbrakk> \<Longrightarrow>
    (\<Union> (ran ((G1 [f+] (S,SA)) ++ G2))) = (insert SA (\<Union> ((ran G1) \<union> (ran G2))))"
 apply (unfold FAddSA_def Let_def)
 apply (simp (no_asm_simp))
 apply (rule conjI)
 apply (rule impI)
 apply (subst EmptyMap_Union_ran_override2)
 apply simp
 apply simp
 apply simp
 apply fast
 apply (subst Union_Un_distrib)
 apply (subst Union_ran_override2)
 apply auto
 done
 
 lemma FAddSA_ran:
   "\<lbrakk> \<forall> T \<in> dom G . T \<noteq> S \<longrightarrow> (the (G T) \<inter> the (G S)) = {};  
      S \<in> dom G; (States SA) \<inter>  (dom G) = {} \<rbrakk> \<Longrightarrow>  
     ran (G [f+] (S,SA)) = insert {} (insert (insert SA (the (G S))) (ran G - {the (G S)}))"
 apply (unfold FAddSA_def Let_def)
 apply simp
 apply (rule conjI)
 apply (rule impI)+
 prefer 2
 apply fast
 apply (simp add: EmptyMap_ran_override)
 apply (unfold ran_def)
 apply auto
 apply (rename_tac Y X a xa xb)
 apply (erule_tac x=a in allE)
 apply simp
 apply (erule_tac x=a in allE)
 apply simp
 done
 
 lemma FAddSA_RootEx_def: 
   "\<lbrakk> S \<in> dom G; (States SA) \<inter> (dom G) = {} \<rbrakk> \<Longrightarrow> 
     RootEx F (G [f+] (S,SA)) = (\<exists>! A . A \<in> F \<and> A \<notin> insert SA (\<Union> (ran G)))"
 apply (unfold RootEx_def)
 apply (simp only: FAddSA_Union_ran Int_commute)
 done
 
 lemma FAddSA_RootEx:
   "\<lbrakk> \<Union> (ran G) = F - {Root F G}; 
      dom G = \<Union>(States ` F); 
      (dom G \<inter> States SA) = {}; S \<in> dom G; 
      RootEx F G \<rbrakk> \<Longrightarrow> RootEx (insert SA F) (G [f+] (S,SA))"
 apply (simp add: FAddSA_RootEx_def Int_commute cong: rev_conj_cong)
 apply (auto cong: conj_cong) 
 done
 
 lemma FAddSA_Root_def:
   "\<lbrakk> S \<in> dom G; (States SA) \<inter> (dom G) = {} \<rbrakk>  \<Longrightarrow> 
    (Root F (G [f+] (S,SA)) = (@ A . A \<in> F \<and> A \<notin> insert SA (\<Union> (ran G))))" 
 apply (unfold Root_def)
 apply (simp only: FAddSA_Union_ran Int_commute)
 done
 
 lemma FAddSA_RootEx_Root: 
   "\<lbrakk> Union (ran G) = F - {Root F G};  
      \<Union>(States ` F) = dom G; 
      (dom G \<inter> States SA) = {}; S \<in> dom G;
      RootEx F G \<rbrakk> \<Longrightarrow> (Root (insert SA F) (G [f+] (S,SA))) = (Root F G)"
 apply (simp add: FAddSA_Root_def Int_commute cong: rev_conj_cong)
 apply (simp cong:conj_cong)
 done
 
 lemma FAddSA_OneAncestor:
   "\<lbrakk> \<Union> (ran G) = F - {Root F G}; 
      (dom G \<inter> States SA) = {}; S \<in> dom G; 
      \<Union>(States ` F) = dom G; RootEx F G;
      OneAncestor F G \<rbrakk> \<Longrightarrow> OneAncestor (insert SA F) (G [f+] (S,SA))"
 apply (subst OneAncestor_def)
 apply simp
 apply (rule ballI)
 apply (rename_tac SAA)
 apply (case_tac "SA = SAA")
 apply (rule_tac a=S in ex1I)
 apply (rule conjI)
 apply simp
 apply fast
 apply (subst FAddSA_dom_insert)
 apply simp
 apply (simp add:Int_def)
 apply simp
 apply (rename_tac T)
 apply (erule conjE bexE exE disjE)+
 apply (rename_tac SAAA)
 apply simp
 apply (erule conjE)
 apply (subst not_not [THEN sym])
 apply (rule notI)
 apply (case_tac "T \<in> States SAA")
 apply blast
 apply (drule_tac A=G and S=S and SA=SAA in FAddSA_States_neq)
 apply fast
 apply simp
 apply (case_tac "SAA \<notin> Union (ran G)")
 apply (frule ran_dom_the)
 prefer 2
 apply fast
 apply blast
 apply simp
 apply (erule conjE)
 apply (simp add: States_Int_not_mem)
 apply (unfold OneAncestor_def)
 apply (drule_tac G=G and S=S and SA=SA in FAddSA_RootEx_Root)
 apply simp
 apply simp
 apply simp
 apply simp
 apply (erule_tac x=SAA in ballE)
 prefer 2
 apply simp
 apply simp
 apply (erule conjE bexE ex1E exE disjE)+
 apply (rename_tac T SAAA)
 apply (rule_tac a=T in ex1I)
 apply (rule conjI)
 apply fast
 apply (case_tac "T = S")
 apply simp
 apply (case_tac "S \<notin> States SA")
 apply simp
 apply simp
 apply (subst FAddSA_States_neq)
 apply blast
 apply (rule not_sym)
 apply simp
 apply simp
 apply (rename_tac U)
 apply simp
 apply (erule conjE bexE)+
 apply (rename_tac SAAAA)
 apply simp
 apply (erule conjE disjE)+
 apply (frule FAddSA_dom_emptyset)
 prefer 2
 apply fast
 back
 back
 apply simp
 apply blast
 apply simp
 apply (erule_tac x=U in allE)
 apply (erule impE)
 prefer 2
 apply simp
 apply (rule conjI)
 apply fast
 apply (case_tac "S \<noteq> U")
 apply (subgoal_tac "U \<notin> States SA")
 apply (drule_tac A=G in FAddSA_States_neq)
 apply fast
 apply simp
 apply blast
 apply (drule_tac A=G and SA=SA in FAddSA_dom_insert)
 apply simp
 apply blast
 apply auto
 done
 
 lemma FAddSA_NoCycles:
   "\<lbrakk> (States SA \<inter> dom G) = {}; S \<in> dom G;
      dom G = \<Union>(States ` F); NoCycles F G \<rbrakk> \<Longrightarrow> 
      NoCycles  (insert SA F) (G [f+] (S,SA))"
 apply (unfold NoCycles_def)
 apply (rule ballI impI)+
 apply (rename_tac SAA)
 apply (case_tac "\<exists> s \<in> SAA. s \<in> States SA")
 apply simp
 apply (erule bexE)+
 apply (rename_tac SAAA T)
 apply (rule_tac x=T in bexI)
 apply simp
 apply (subst FAddSA_dom_emptyset)
 apply simp
 apply fast
 apply blast
 apply simp
 apply simp
 apply simp
 apply simp
 apply (erule_tac x=SAA in ballE)
 prefer 2
 apply simp
 apply auto[1]
 apply (unfold UNION_eq Pow_def)
 apply simp
 apply (case_tac "SAA = {}")
 apply fast
 apply simp
 apply (erule bexE)+
 apply (rename_tac SAAA T)
 apply (rule_tac x=T in bexI)
 prefer 2
 apply simp
 apply (case_tac "T=S")
 apply simp
 apply (subst FAddSA_dom_insert)
 apply auto
 done
 
 lemma FAddSA_IsCompFun:
  "\<lbrakk> (States SA \<inter> (\<Union>(States ` F))) = {};
      S \<in> (\<Union>(States ` F)); 
      IsCompFun F G \<rbrakk> \<Longrightarrow>  IsCompFun (insert SA F) (G [f+] (S,SA))"
 apply (unfold IsCompFun_def)
 apply (erule conjE)+
 apply (simp add: Int_commute FAddSA_RootEx_Root FAddSA_RootEx FAddSA_OneAncestor FAddSA_NoCycles)
 apply (rule conjI)
 apply (subst FAddSA_dom_dom_States)
 apply simp
 apply blast
 apply (simp add: Un_commute)
 apply (simp add: FAddSA_Union_ran)
 apply (case_tac "SA = Root F G")
 prefer 2
 apply blast
 apply (subgoal_tac "States (Root F G) \<subseteq>  \<Union>(States ` F)")
 apply simp
 apply (frule subset_lemma)
 apply auto
 done
 
 lemma FAddSA_HierAuto:
   "\<lbrakk> (States SA \<inter> (\<Union>(States ` F))) = {};
       S \<in> (\<Union>(States ` F)); 
       HierAuto D F E G \<rbrakk> \<Longrightarrow> HierAuto D (insert SA F) (E \<union> SAEvents SA) (G [f+] (S,SA))"
 apply (unfold HierAuto_def)
 apply auto
 apply (simp add: MutuallyDistinct_Insert)
 apply (rule FAddSA_IsCompFun)
 apply auto
 done
 
 lemma FAddSA_HierAuto_insert [simp]:
   "\<lbrakk> (States SA \<inter> HAStates HA) = {};
       S \<in> HAStates HA \<rbrakk> \<Longrightarrow> 
     HierAuto (HAInitValue HA)                  
              (insert SA (SAs HA))              
              (HAEvents HA \<union> SAEvents SA)      
              (CompFun HA [f+] (S,SA))"
 apply (unfold HAStates_def)
 apply (rule FAddSA_HierAuto)
 apply auto
 done
 
 subsection "Constructing a PseudoHA" 
 
 definition
   PseudoHA :: "[('s,'e,'d)seqauto,'d data] => ('s,'e,'d)hierauto" where
   "PseudoHA SA D = Abs_hierauto(D,{SA}, SAEvents SA ,EmptyMap (States SA))"
 
 lemma PseudoHA_SAs [simp]:
   "SAs (PseudoHA SA D) = {SA}"
 by (unfold PseudoHA_def SAs_def, simp add: Abs_hierauto_inverse)
 
 lemma PseudoHA_Events [simp]:
   "HAEvents (PseudoHA SA D) = SAEvents SA"
 by (unfold PseudoHA_def HAEvents_def, simp add: Abs_hierauto_inverse)
  
 lemma PseudoHA_CompFun [simp]:
   "CompFun (PseudoHA SA D) = EmptyMap (States SA)"
 by (unfold PseudoHA_def CompFun_def, simp add: Abs_hierauto_inverse)
 
 lemma PseudoHA_HAStates [simp]:
   "HAStates (PseudoHA SA D) = (States SA)"
 by (unfold HAStates_def, auto)
 
 lemma PseudoHA_HAInitValue [simp]:
   "(HAInitValue (PseudoHA SA D)) = D"
 by (unfold PseudoHA_def Let_def HAInitValue_def, simp add: Abs_hierauto_inverse)
  
 lemma PseudoHA_CompFun_the [simp]: 
  "S \<in> States A \<Longrightarrow> (the (CompFun (PseudoHA A D) S)) = {}"
 by simp
 
 lemma PseudoHA_CompFun_ran [simp]:
  "(ran (CompFun (PseudoHA SA D))) = {{}}"
 by auto
 
 lemma PseudoHA_HARoot [simp]:
  "(HARoot (PseudoHA SA D)) = SA"
 by (unfold HARoot_def, auto)
 
 lemma PseudoHA_HAInitState [simp]:
   "HAInitState (PseudoHA A D) = InitState A"
 apply (unfold HAInitState_def)
 apply simp
 done
 
 lemma PseudoHA_HAInitStates [simp]:
   "HAInitStates (PseudoHA A D) = {InitState A}" 
 apply (unfold HAInitStates_def)
 apply simp
 done
 
 lemma PseudoHA_Chi [simp]:
   "S \<in> States A \<Longrightarrow> Chi (PseudoHA A D) S = {}"
 apply (unfold Chi_def restrict_def)
 apply auto
 done
 
 lemma PseudoHA_ChiRel [simp]:
   "ChiRel (PseudoHA A D) = {}"
 apply (unfold ChiRel_def)
 apply simp
 done
 
 lemma PseudoHA_InitConf [simp]:
  "InitConf (PseudoHA A D) = {InitState A}"
 apply (unfold InitConf_def)
 apply simp
 done
 
 subsection \<open>Extending a HA by a SA (\<open>AddSA\<close>)\<close>
 
 definition
   AddSA :: "[('s,'e,'d)hierauto, 's * ('s,'e,'d)seqauto]
              => ('s,'e,'d)hierauto"
            ("(_ [++]/ _)" [10,11]10) where
   "AddSA HA SSA = (let (S,SA) = SSA;
                         DNew = HAInitValue HA;
                         FNew = insert SA (SAs HA);
                         ENew  = HAEvents HA \<union> SAEvents SA;
                         GNew  = CompFun HA [f+] (S,SA)
                    in
                        Abs_hierauto(DNew,FNew,ENew,GNew))"
 
 definition
   AddHA :: "[('s,'e,'d)hierauto, 's * ('s,'e,'d)hierauto]
              => ('s,'e,'d)hierauto"
            ("(_ [**]/ _)" [10,11]10) where
   "AddHA HA1 SHA =
             (let (S,HA2)     = SHA;
                  (D1,F1,E1,G1) = Rep_hierauto (HA1 [++] (S,HARoot HA2));
                  (D2,F2,E2,G2) = Rep_hierauto HA2;
                  FNew       = F1 \<union> F2;
                  ENew       = E1 \<union> E2;
                  GNew       = G1 ++ G2
              in
                  Abs_hierauto(D1,FNew,ENew,GNew))"
 
 lemma AddSA_SAs:
   "\<lbrakk> (States SA \<inter>  HAStates HA) = {}; 
       S \<in> HAStates HA \<rbrakk> \<Longrightarrow> (SAs (HA [++] (S,SA))) = insert SA (SAs HA)"
 apply (unfold Let_def AddSA_def)
 apply (subst SAs_def)
 apply (simp add: hierauto_def Abs_hierauto_inverse)
 done
 
 lemma AddSA_Events:
   "\<lbrakk> (States SA \<inter> HAStates HA) = {}; 
       S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
      HAEvents (HA [++] (S,SA)) = (HAEvents HA) \<union> (SAEvents SA)"
 apply (unfold Let_def AddSA_def)
 apply (subst HAEvents_def)
 apply (simp add: hierauto_def Abs_hierauto_inverse)
 done
 
 lemma AddSA_CompFun:
    "\<lbrakk> (States SA \<inter>  HAStates HA) = {}; 
       S \<in> HAStates HA \<rbrakk> \<Longrightarrow>  
      CompFun (HA [++] (S,SA)) = (CompFun HA [f+] (S,SA))"
 apply (unfold Let_def AddSA_def)
 apply (subst CompFun_def)
 apply (simp add: hierauto_def Abs_hierauto_inverse)
 done
 
 lemma AddSA_HAStates:
    "\<lbrakk> (States SA \<inter> HAStates HA) = {}; 
        S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
       HAStates (HA [++] (S,SA)) = (HAStates HA) \<union> (States SA)"
 apply (unfold HAStates_def)
 apply (subst AddSA_SAs)
 apply (unfold HAStates_def)
 apply auto
 done
 
 lemma AddSA_HAInitValue:
    "\<lbrakk> (States SA \<inter> HAStates HA) = {};
        S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
       (HAInitValue (HA [++] (S,SA))) = (HAInitValue HA)"
 apply (unfold Let_def AddSA_def)
 apply (subst HAInitValue_def)
 apply (simp add: hierauto_def Abs_hierauto_inverse)
 done
 
 lemma AddSA_HARoot:
    "\<lbrakk> (States SA \<inter> HAStates HA) = {};
       S \<in> HAStates HA \<rbrakk> \<Longrightarrow> 
       (HARoot (HA [++] (S,SA))) = (HARoot HA)"
 apply (unfold HARoot_def)
 apply (simp add: AddSA_CompFun AddSA_SAs)
 apply (subst FAddSA_RootEx_Root)
 apply auto
 apply (simp only: HAStates_SA_mem)
 apply (unfold HAStates_def)
 apply fast
 done
 
 lemma AddSA_CompFun_the: 
  "\<lbrakk> (States SA \<inter> HAStates A) = {}; 
     S \<in> HAStates A \<rbrakk> \<Longrightarrow> 
   (the ((CompFun (A [++] (S,SA))) S)) = insert SA (the ((CompFun A) S))"
 by (simp add: AddSA_CompFun)
 
 lemma AddSA_CompFun_the2:
  "\<lbrakk> S' \<in> States (SA::('a,'c,'d)seqauto); 
     (States SA \<inter> HAStates A) = {};
     S \<in> HAStates A \<rbrakk> \<Longrightarrow>
     the ((CompFun (A [++] (S,SA))) S') = {}"
 apply (simp add: AddSA_CompFun)
 apply (subst FAddSA_dom_emptyset)
 apply auto
 done
 
 lemma AddSA_CompFun_the3:
  "\<lbrakk> S' \<notin> States (SA::('a,'c,'d)seqauto); 
     S \<noteq> S'; 
     (States SA \<inter> HAStates A) = {}; 
     S \<in> HAStates A \<rbrakk> \<Longrightarrow> 
    (the ((CompFun (A [++] (S,SA))) S')) = (the ((CompFun A) S'))"
 by (simp add: AddSA_CompFun)
 
 lemma AddSA_CompFun_ran:
  "\<lbrakk> (States SA \<inter> HAStates A) = {};
      S \<in> HAStates A \<rbrakk> \<Longrightarrow> 
    ran (CompFun (A [++] (S,SA))) = 
        insert {} (insert (insert SA (the ((CompFun A) S))) (ran (CompFun A) - {the ((CompFun A) S)}))"
 apply (simp add: AddSA_CompFun)
 apply (subst FAddSA_ran)
 apply auto
 apply (fast dest: CompFun_Int_disjoint) 
 done
 
 lemma AddSA_CompFun_ran2:
  "\<lbrakk> (States SA1 \<inter> HAStates A) = {};
     (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
      S \<in> HAStates A;
      T \<in> States SA1 \<rbrakk> \<Longrightarrow>
    ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2))) = 
        insert {} (insert {SA2} (ran (CompFun (A  [++] (S,SA1)))))"
 apply (simp add: AddSA_HAStates AddSA_CompFun)
 apply (subst FAddSA_ran)
 apply (rule ballI)
 apply (rule impI)
 apply (subst AddSA_CompFun [THEN sym])
 apply simp
 apply simp
 apply (subst AddSA_CompFun [THEN sym])
 apply simp
 apply simp
 apply (rule CompFun_Int_disjoint)
 apply simp
 apply (simp add: AddSA_HAStates)
 apply (simp add: AddSA_HAStates)
 apply (case_tac "S \<in> States SA1")
 apply simp
 apply (simp only: dom_CompFun [THEN sym])
 apply (frule FAddSA_dom_dom_States)
 apply fast
 apply simp
 apply (case_tac "S \<in> States SA1")
 apply simp
 apply fast
 apply (subst FAddSA_dom_dom_States)
 apply simp
 apply simp
 apply simp
 apply (case_tac "S \<in>  States SA1")
 apply simp
 apply fast
 apply (subst FAddSA_dom_dom_States)
 apply simp
 apply simp
 apply simp
 apply (case_tac "S \<in>  States SA1")
 apply simp
 apply fast
 apply simp
 apply fast
 done
 
 lemma AddSA_CompFun_ran_not_mem:
  "\<lbrakk> States SA2 \<inter> (HAStates A \<union> States SA1) = {};
     States SA1 \<inter> HAStates A = {};
     S \<in> HAStates A \<rbrakk> \<Longrightarrow> 
    {SA2} \<notin> ran (CompFun A [f+] (S, SA1))"
   apply (cut_tac HA="A [++] (S,SA1)" and Sas="{SA2}" in ran_CompFun_is_not_SA)
   apply (metis AddSA_HAStates SA_States_disjunct2 SAs_States_HAStates insert_subset)
    apply (simp add: AddSA_HAStates AddSA_CompFun)
   done
 
 lemma AddSA_CompFun_ran3:
  "\<lbrakk> (States SA1 \<inter> HAStates A) = {};
     (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
     (States SA3 \<inter> (HAStates A \<union> States SA1 \<union> States SA2)) = {};
      S \<in> HAStates A; 
      T \<in> States SA1 \<rbrakk> \<Longrightarrow> 
     ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2) [++] (T,SA3))) = 
        insert {} (insert {SA3,SA2} (ran (CompFun (A  [++] (S,SA1)))))"
   apply (simp add: AddSA_HAStates AddSA_CompFun)
   apply (subst FAddSA_ran)
   apply (metis AddSA_CompFun AddSA_HAStates CompFun_Int_disjoint UnCI dom_CompFun)
   apply (metis AddSA_CompFun AddSA_HAStates UnCI dom_CompFun)
   apply (metis AddSA_CompFun AddSA_HAStates UnCI dom_CompFun)
 
   apply (subst AddSA_CompFun [THEN sym])
     back
     apply simp
    apply simp
 
   apply (subst AddSA_CompFun [THEN sym])
     back
     apply (simp add: AddSA_HAStates)
    apply (simp add: AddSA_HAStates)
   apply (subst AddSA_CompFun_ran2)
       apply fast
      apply fast
     apply fast
    apply fast
   apply (simp add: AddSA_CompFun)
   apply (subst  FAddSA_dom_insert)
     apply (subst FAddSA_dom_dom_States)
       apply simp
      apply fast
     apply simp
    apply fast
   apply (subst FAddSA_dom_emptyset)
      apply simp
     apply fast
    apply simp
   apply simp
   apply (subst  FAddSA_dom_insert)
     apply (subst FAddSA_dom_dom_States)
       apply simp
      apply fast
     apply simp
    apply fast
   apply (subst FAddSA_dom_emptyset)
      apply simp
     apply fast
    apply simp
   apply simp
   by (simp add: AddSA_CompFun_ran_not_mem insert_Diff_if insert_commute)
 
 lemma AddSA_CompFun_PseudoHA_ran:
   "\<lbrakk> S \<in> States RootSA;
      States RootSA \<inter> States SA = {} \<rbrakk> \<Longrightarrow> 
      (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA)))) = (insert {} {{SA}})"
 apply (subst AddSA_CompFun_ran)
 apply auto
 done
 
 lemma AddSA_CompFun_PseudoHA_ran2:
   "\<lbrakk> States SA1 \<inter> States RootSA = {};
      States SA2 \<inter> (States RootSA \<union> States SA1) = {}; 
      S \<in> States RootSA \<rbrakk> \<Longrightarrow>  
      (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA1) [++] (S,SA2)))) = (insert {} {{SA2,SA1}})"
 apply (subst AddSA_CompFun_ran) 
 prefer 3
 apply (subst AddSA_CompFun_the)
 apply simp
 apply simp
 apply (subst AddSA_CompFun_PseudoHA_ran)
 apply fast
 apply fast
 apply (subst AddSA_CompFun_the)
 apply simp
 apply simp
 apply simp
 apply fast
 apply (simp add: AddSA_HAStates)
 apply (simp add: AddSA_HAStates)
 done
 
 lemma AddSA_HAInitStates [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
     S \<in> HAStates A \<rbrakk> \<Longrightarrow>
    HAInitStates (A [++] (S,SA)) = insert (InitState SA) (HAInitStates A)"
 apply (unfold HAInitStates_def)
 apply (simp add: AddSA_SAs)
 done
 
 lemma AddSA_HAInitState [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
     S \<in> HAStates A \<rbrakk> \<Longrightarrow>
   HAInitState (A [++] (S,SA)) = (HAInitState A)"
 apply (unfold HAInitState_def)
 apply (simp add: AddSA_HARoot)
 done
 
 lemma AddSA_Chi [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>  
   Chi (A [++] (S,SA)) S = (States SA) \<union> (Chi A S)"
 apply (unfold Chi_def restrict_def)
 apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the)
 apply auto
 done
 
 lemma AddSA_Chi2 [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
     S \<in> HAStates A;  
     T \<in> States SA \<rbrakk> \<Longrightarrow>
     Chi (A [++] (S,SA)) T = {}"
 apply (unfold Chi_def restrict_def)
 apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the2)
 done
 
 lemma AddSA_Chi3 [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
     S \<in> HAStates A; 
     T \<notin> States SA; T \<noteq> S \<rbrakk> \<Longrightarrow>
     Chi (A [++] (S,SA)) T = Chi A T"
 apply (unfold Chi_def restrict_def)
 apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the3)
 apply auto
 done
 
 lemma AddSA_ChiRel [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
     S \<in> HAStates A \<rbrakk> \<Longrightarrow> 
    ChiRel (A [++] (S,SA)) = { (T,T') . T = S \<and> T' \<in> States SA } \<union> (ChiRel A)" 
 apply (unfold ChiRel_def)
 apply (simp add: AddSA_HAStates)
 apply safe
 apply (rename_tac T U)
 apply (case_tac "T \<in> States SA")
 apply simp
 apply simp
 apply (rename_tac T U)
 apply (case_tac "T \<noteq> S")
 apply (case_tac "T \<in>  States SA")
 apply simp
 apply simp
 apply simp
 apply (rename_tac T U)
 apply (case_tac "T \<in>  States SA")
 apply simp
 apply simp
 apply (cut_tac A=A and T=T in Chi_HAStates)
 apply fast
 apply (case_tac "T \<in> States SA")
 apply simp
 apply simp
 apply (cut_tac A=A and T=T in Chi_HAStates)
 apply fast
 apply fast
 apply (rename_tac T U)
 apply (case_tac "T \<noteq> S")
 apply (case_tac "T \<in> States SA")
 apply simp
 apply simp
 apply simp
 apply (rename_tac T U)
 apply (case_tac "T \<in>  States SA")
 apply auto
 apply (metis AddSA_Chi AddSA_Chi3 Int_iff Un_iff empty_iff)
 done
 
 lemma help_InitConf:
   "\<lbrakk>States SA \<inter> HAStates A = {} \<rbrakk> \<Longrightarrow> {p. fst p \<noteq> InitState SA \<and> snd p \<noteq> InitState SA \<and> 
        p \<in>  insert (InitState SA) (HAInitStates A) \<times> insert (InitState SA) (HAInitStates A) \<and>  
        (p \<in>  {S} \<times> States SA \<or>  p \<in>  ChiRel A)} = 
    (HAInitStates A \<times> HAInitStates A \<inter>  ChiRel A)"    
 apply auto
 apply (cut_tac A=SA in InitState_States)
 apply (cut_tac A=A in HAInitStates_HAStates, fast)
 apply (cut_tac A=SA in InitState_States)
 apply (cut_tac A=A in HAInitStates_HAStates, fast)
 done
  
 lemma AddSA_InitConf [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
     S \<in> InitConf A \<rbrakk> \<Longrightarrow> 
     InitConf (A [++] (S,SA)) = insert (InitState SA) (InitConf A)"
 apply (frule InitConf_HAStates2)
 apply (unfold InitConf_def)
 apply (simp del: insert_Times_insert)
-apply auto
-apply (rename_tac T)
-apply (case_tac "T=S")
-apply auto
-prefer 3
-apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
-apply auto
-apply (rotate_tac 3)
-apply (frule trancl_collect)
-prefer 2
-apply fast
-apply auto
-apply (cut_tac A=SA in InitState_States)
-apply (frule ChiRel_HAStates)
-apply fast
-apply (frule ChiRel_HAStates)
-apply (cut_tac A=SA in InitState_States)
-apply fast
-apply (frule ChiRel_HAStates)
-apply (cut_tac A=SA in InitState_States)
-apply fast
-apply (subst help_InitConf [THEN sym])
-apply fast
-apply auto
+  apply auto
+  apply (rename_tac T)
+   apply (case_tac "T=S")
+  apply auto
+  prefer 3
+   apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
+ apply auto
+ apply (rotate_tac 3)
+ apply (frule trancl_collect)
+   prefer 2
+   apply fast
+  apply auto
+   apply (cut_tac A=SA in InitState_States)
+   apply (frule ChiRel_HAStates)
+   apply fast
+  apply (frule ChiRel_HAStates)
+  apply (cut_tac A=SA in InitState_States)
+  apply fast
+ apply (subst help_InitConf [THEN sym])
+  apply fast
+ apply auto
 apply (rule_tac b=S in rtrancl_into_rtrancl)
-apply auto
-prefer 2
-apply (erule rtranclE)
-apply auto
-prefer 2
-apply (erule rtranclE)
-apply auto
-apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
+ apply auto
+  prefer 2
+  apply (erule rtranclE)
+   apply auto
+ prefer 2
+ apply (erule rtranclE)
+  apply auto
+ apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
 apply auto
 done
 
 lemma AddSA_InitConf2 [simp]:
  "\<lbrakk> States SA \<inter> HAStates A = {};
     S \<notin> InitConf A;
   S \<in> HAStates A \<rbrakk> \<Longrightarrow>
   InitConf (A [++] (S,SA)) = InitConf A"
 apply (unfold InitConf_def)
 apply simp
 apply auto
-apply (rename_tac T)
-prefer 2
-apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
-apply auto
+ apply (rename_tac T)
+ prefer 2
+ apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
+  apply auto
 apply (case_tac "T=InitState SA")
-apply auto
-prefer 2
-apply (rotate_tac 3)
-apply (frule trancl_collect)
-prefer 2
-apply fast
-apply auto
-apply (cut_tac A=SA in InitState_States)
-apply (frule ChiRel_HAStates)
-apply fast
-apply (cut_tac A=SA in InitState_States)
-apply (frule ChiRel_HAStates)
-apply fast
-apply (cut_tac A=SA in InitState_States)
-apply (cut_tac A=A in HAInitStates_HAStates)
-apply fast
-apply (subst help_InitConf [THEN sym])
-apply fast
-apply auto
+ apply auto
+ prefer 2
+ apply (rotate_tac 3)
+ apply (frule trancl_collect)
+   prefer 2
+   apply fast
+  apply auto
+   apply (cut_tac A=SA in InitState_States)
+   apply (frule ChiRel_HAStates)
+   apply fast
+  apply (cut_tac A=SA in InitState_States)
+  apply (frule ChiRel_HAStates)
+ apply fast
+ apply (cut_tac A=SA in InitState_States)
+ apply (cut_tac A=A in HAInitStates_HAStates)
+ apply (subst help_InitConf [THEN sym])
+  apply fast
+ apply auto
 apply (rule_tac b="InitState SA" in rtrancl_induct)
-apply auto
-apply (frule ChiRel_HAStates2)
-apply (cut_tac A=SA in InitState_States)
-apply fast
-prefer 2
-apply (frule ChiRel_HAStates)
-apply (cut_tac A=SA in InitState_States)
-apply fast
+  apply auto
+  apply (frule ChiRel_HAStates2)
+  apply (cut_tac A=SA in InitState_States)
+  apply fast
+ prefer 2
+ apply (frule ChiRel_HAStates)
+ apply (cut_tac A=SA in InitState_States)
+ apply fast
 apply (rule rtrancl_into_rtrancl)
-apply auto
-apply (rule rtrancl_into_rtrancl)
-apply auto
+ apply auto
 done
 
 subsection "Theorems for Calculating Wellformedness of HA"
 
 lemma PseudoHA_HAStates_IFF:
  "(States SA) = X  \<Longrightarrow> (HAStates (PseudoHA SA D)) = X"
 apply simp
 done
 
 lemma AddSA_SAs_IFF:
  "\<lbrakk> States SA \<inter> HAStates HA = {};
     S \<in> HAStates HA;
     (SAs HA) = X \<rbrakk> \<Longrightarrow> (SAs (HA [++] (S, SA))) = (insert SA X)"
 apply (subst AddSA_SAs)
 apply auto
 done
 
 lemma AddSA_Events_IFF:
  "\<lbrakk> States SA \<inter> HAStates HA = {}; 
     S \<in> HAStates HA; 
     (HAEvents HA) = HAE;
     (SAEvents SA) = SAE;  
     (HAE \<union> SAE) = X \<rbrakk> \<Longrightarrow> (HAEvents (HA [++] (S, SA))) = X"
 apply (subst AddSA_Events)
 apply auto
 done
 
 lemma AddSA_CompFun_IFF:
  "\<lbrakk> States SA \<inter>  HAStates HA = {};
     S \<in> HAStates HA;
     (CompFun HA) = HAG;
     (HAG [f+] (S, SA)) = X \<rbrakk> \<Longrightarrow> (CompFun (HA [++] (S, SA))) = X"
 apply (subst AddSA_CompFun)
 apply auto
 done
 
 lemma AddSA_HAStates_IFF: 
  "\<lbrakk> States SA \<inter> HAStates HA = {};
     S \<in> HAStates HA;
     (HAStates HA) = HAS;
     (States SA) = SAS;
     (HAS \<union> SAS) = X \<rbrakk> \<Longrightarrow> (HAStates (HA [++] (S, SA))) = X"
 apply (subst AddSA_HAStates)
 apply auto
 done
 
 lemma AddSA_HAInitValue_IFF:
  "\<lbrakk> States SA \<inter> HAStates HA = {};
     S \<in> HAStates HA;
     (HAInitValue HA) = X \<rbrakk> \<Longrightarrow> (HAInitValue (HA [++] (S, SA))) = X"
 apply (subst AddSA_HAInitValue)
 apply auto
 done
 
 lemma AddSA_HARoot_IFF:
  "\<lbrakk> States SA \<inter> HAStates HA = {};
     S \<in> HAStates HA;
     (HARoot HA) = X \<rbrakk> \<Longrightarrow> (HARoot (HA [++] (S, SA))) = X"
 apply (subst AddSA_HARoot)
 apply auto
 done
 
 lemma AddSA_InitConf_IFF:
  "\<lbrakk> InitConf A = Y;
     States SA \<inter> HAStates A = {};
     S \<in> HAStates A; 
     (if S \<in> Y then insert (InitState SA) Y else Y) = X \<rbrakk> \<Longrightarrow> 
     InitConf (A [++] (S,SA)) = X" 
 apply (case_tac "S \<in> Y")
 apply auto
 done
 
 lemma AddSA_CompFun_ran_IFF:
   "\<lbrakk> (States SA \<inter> HAStates A) = {}; 
      S \<in> HAStates A;
      (insert {} (insert (insert SA (the ((CompFun A) S))) (ran (CompFun A) - {the ((CompFun A) S)}))) = X \<rbrakk> \<Longrightarrow>
      ran (CompFun (A [++] (S,SA))) = X"
 apply (subst  AddSA_CompFun_ran)
 apply auto
 done
 
 lemma AddSA_CompFun_ran2_IFF:
  "\<lbrakk> (States SA1 \<inter> HAStates A) = {}; 
     (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
     S \<in> HAStates A;
     T \<in> States SA1;
     insert {} (insert {SA2} (ran (CompFun (A  [++] (S,SA1))))) = X \<rbrakk> \<Longrightarrow>
     ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2))) = X"
 apply (subst AddSA_CompFun_ran2)
 apply auto
 done
    
 lemma AddSA_CompFun_ran3_IFF:
  "\<lbrakk> (States SA1 \<inter> HAStates A) = {};
     (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
     (States SA3 \<inter> (HAStates A \<union> States SA1 \<union> States SA2)) = {};
      S \<in> HAStates A;
      T \<in> States SA1;
      insert {} (insert {SA3,SA2} (ran (CompFun (A  [++] (S,SA1))))) = X \<rbrakk> \<Longrightarrow>
      ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2) [++] (T,SA3))) = X" 
 apply (subst AddSA_CompFun_ran3)
 apply auto
 done
 
 lemma AddSA_CompFun_PseudoHA_ran_IFF:
   "\<lbrakk> S \<in> States RootSA; 
      States RootSA \<inter> States SA = {};
    (insert {} {{SA}}) = X \<rbrakk> \<Longrightarrow> 
    (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA)))) = X"
 apply (subst AddSA_CompFun_PseudoHA_ran)
 apply auto
 done
 
 lemma AddSA_CompFun_PseudoHA_ran2_IFF:
   "\<lbrakk> States SA1 \<inter> States RootSA = {};
      States SA2 \<inter> (States RootSA \<union> States SA1) = {};
      S \<in> States RootSA;
      (insert {} {{SA2,SA1}}) = X \<rbrakk> \<Longrightarrow> 
      (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA1) [++] (S,SA2)))) = X" 
 apply (subst AddSA_CompFun_PseudoHA_ran2)
 apply auto
 done
 
 
 ML \<open>
 
 val AddSA_SAs_IFF = @{thm AddSA_SAs_IFF};
 val AddSA_Events_IFF = @{thm AddSA_Events_IFF};
 val AddSA_CompFun_IFF = @{thm AddSA_CompFun_IFF};
 val AddSA_HAStates_IFF = @{thm AddSA_HAStates_IFF};
 val PseudoHA_HAStates_IFF = @{thm PseudoHA_HAStates_IFF};
 val AddSA_HAInitValue_IFF = @{thm AddSA_HAInitValue_IFF};
 val AddSA_CompFun_ran_IFF = @{thm AddSA_CompFun_ran_IFF};
 val AddSA_HARoot_IFF = @{thm AddSA_HARoot_IFF};
 val insert_inter = @{thm insert_inter};
 val insert_notmem = @{thm insert_notmem};
 val PseudoHA_CompFun = @{thm PseudoHA_CompFun};
 val PseudoHA_Events = @{thm PseudoHA_Events};
 val PseudoHA_SAs = @{thm PseudoHA_SAs};
 val PseudoHA_HARoot = @{thm PseudoHA_HARoot};
 val PseudoHA_HAInitValue = @{thm PseudoHA_HAInitValue};
 val PseudoHA_CompFun_ran = @{thm PseudoHA_CompFun_ran};
 val Un_empty_right = @{thm Un_empty_right};
 val insert_union = @{thm insert_union};
 
 
 fun wellformed_tac ctxt L i =
   FIRST[resolve_tac ctxt [AddSA_SAs_IFF] i,
         resolve_tac ctxt [AddSA_Events_IFF] i,
         resolve_tac ctxt [AddSA_CompFun_IFF] i,
         resolve_tac ctxt [AddSA_HAStates_IFF] i,
         resolve_tac ctxt [PseudoHA_HAStates_IFF] i,
         resolve_tac ctxt [AddSA_HAInitValue_IFF] i,
         resolve_tac ctxt [AddSA_HARoot_IFF] i,
         resolve_tac ctxt [AddSA_CompFun_ran_IFF] i,
         resolve_tac ctxt [insert_inter] i,
         resolve_tac ctxt [insert_notmem] i,
         CHANGED (simp_tac (put_simpset HOL_basic_ss ctxt addsimps
            [PseudoHA_HARoot, PseudoHA_CompFun, PseudoHA_CompFun_ran,PseudoHA_Events,PseudoHA_SAs,insert_union,
             PseudoHA_HAInitValue,Un_empty_right]@ L) i),
         fast_tac ctxt i,
         CHANGED (simp_tac ctxt i)];
 \<close>
 
 method_setup wellformed  = \<open>Attrib.thms >> (fn thms => fn ctxt => (METHOD (fn facts => 
                                        (HEADGOAL (wellformed_tac ctxt (facts @ thms))))))\<close>
 
 end