diff --git a/thys/Launchbury/Abstract-Denotational-Props.thy b/thys/Launchbury/Abstract-Denotational-Props.thy
--- a/thys/Launchbury/Abstract-Denotational-Props.thy
+++ b/thys/Launchbury/Abstract-Denotational-Props.thy
@@ -1,171 +1,170 @@
 theory "Abstract-Denotational-Props"
   imports AbstractDenotational Substitution
 begin
 
 context semantic_domain
 begin
 
 subsubsection \<open>The semantics ignores fresh variables\<close>
 
 lemma ESem_considers_fv': "\<lbrakk> e \<rbrakk>\<^bsub>\<rho>\<^esub> = \<lbrakk> e \<rbrakk>\<^bsub>\<rho> f|` (fv e)\<^esub>"
 proof (induct e arbitrary: \<rho> rule:exp_induct)
   case Var
   show ?case by simp
 next
   have [simp]: "\<And> S x. S \<inter> insert x S = S" by auto
   case App
   show ?case
     by (simp, subst (1 2) App, simp)
 next
   case (Lam x e)
   show ?case by simp
 next
   case (IfThenElse scrut e\<^sub>1 e\<^sub>2)
   have [simp]: "(fv scrut \<inter> (fv scrut \<union> fv e\<^sub>1 \<union> fv e\<^sub>2)) = fv scrut" by auto
   have [simp]: "(fv e\<^sub>1 \<inter> (fv scrut \<union> fv e\<^sub>1 \<union> fv e\<^sub>2)) = fv e\<^sub>1" by auto
   have [simp]: "(fv e\<^sub>2 \<inter> (fv scrut \<union> fv e\<^sub>1 \<union> fv e\<^sub>2)) = fv e\<^sub>2" by auto
   show ?case
     apply simp
     apply (subst (1 2) IfThenElse(1))
     apply (subst (1 2) IfThenElse(2))
     apply (subst (1 2) IfThenElse(3))
     apply (simp)
     done
 next
   case (Let as e)
 
   have "\<lbrakk>e\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>\<rho>\<^esub> = \<lbrakk>e\<rbrakk>\<^bsub>(\<lbrace>as\<rbrace>\<rho>) f|` (fv as \<union> fv e)\<^esub>"
     apply (subst (1 2) Let(2))
     apply simp
-    apply (metis inf_sup_absorb sup_commute)
     done
   also
   have "fv as \<subseteq> fv as \<union> fv e" by (rule inf_sup_ord(3))
   hence "(\<lbrace>as\<rbrace>\<rho>) f|` (fv as \<union> fv e) = \<lbrace>as\<rbrace>(\<rho> f|` (fv as \<union> fv e))"
      by (rule HSem_ignores_fresh_restr'[OF _ Let(1)])
   also
   have "\<lbrace>as\<rbrace>(\<rho> f|` (fv as \<union> fv e)) = \<lbrace>as\<rbrace>\<rho> f|` (fv as \<union> fv e - domA as)"
     by (rule HSem_restr_cong) (auto simp add: lookup_env_restr_eq)
   finally
   show ?case by simp
 qed auto
 
 sublocale has_ignore_fresh_ESem ESem
   by standard (rule fv_supp_exp, rule ESem_considers_fv')
 
 subsubsection \<open>Nicer equations for ESem, without freshness requirements\<close>
 
 lemma ESem_Lam[simp]: "\<lbrakk> Lam [x]. e \<rbrakk>\<^bsub>\<rho>\<^esub> = tick \<cdot> (Fn \<cdot> (\<Lambda> v. \<lbrakk> e \<rbrakk>\<^bsub>\<rho>(x := v)\<^esub>))"
 proof-
   have *: "\<And> v. ((\<rho> f|` (fv e - {x}))(x := v)) f|` fv e = (\<rho>(x := v)) f|` fv e"
     by (rule ext) (auto simp add: lookup_env_restr_eq)
 
   have "\<lbrakk> Lam [x]. e \<rbrakk>\<^bsub>\<rho>\<^esub> = \<lbrakk> Lam [x]. e \<rbrakk>\<^bsub>env_delete x \<rho>\<^esub>"
     by (rule ESem_fresh_cong) simp
   also have "\<dots> = tick \<cdot> (Fn \<cdot> (\<Lambda> v. \<lbrakk> e \<rbrakk>\<^bsub>(\<rho> f|` (fv e - {x}))(x := v)\<^esub>))"
     by simp
   also have "\<dots> = tick \<cdot> (Fn \<cdot> (\<Lambda> v. \<lbrakk> e \<rbrakk>\<^bsub>((\<rho> f|` (fv e - {x}))(x := v)) f|` fv e\<^esub>))"
     by (subst  ESem_considers_fv, rule)
   also have "\<dots> = tick \<cdot> (Fn \<cdot> (\<Lambda> v. \<lbrakk> e \<rbrakk>\<^bsub>\<rho>(x := v) f|` fv e\<^esub>))"
     unfolding *..
   also have "\<dots> = tick \<cdot> (Fn \<cdot> (\<Lambda> v. \<lbrakk> e \<rbrakk>\<^bsub>\<rho>(x := v)\<^esub>))"
     unfolding  ESem_considers_fv[symmetric]..
   finally show ?thesis.
 qed
 declare ESem.simps(1)[simp del]
 
 lemma ESem_Let[simp]: "\<lbrakk>Let as body\<rbrakk>\<^bsub>\<rho>\<^esub> = tick \<cdot> (\<lbrakk>body\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>\<rho>\<^esub>)"
 proof-
   have "\<lbrakk> Let as body \<rbrakk>\<^bsub>\<rho>\<^esub> = tick \<cdot> (\<lbrakk>body\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>(\<rho> f|` fv (Let as body))\<^esub>)" 
     by simp
   also have "\<lbrace>as\<rbrace>(\<rho> f|` fv(Let as body)) = \<lbrace>as\<rbrace>(\<rho> f|` (fv as \<union> fv body))" 
     by (rule HSem_restr_cong) (auto simp add: lookup_env_restr_eq)
   also have "\<dots> = (\<lbrace>as\<rbrace>\<rho>) f|` (fv as \<union> fv body)"
     by (rule HSem_ignores_fresh_restr'[symmetric, OF _ ESem_considers_fv]) simp
   also have "\<lbrakk>body\<rbrakk>\<^bsub>\<dots>\<^esub> = \<lbrakk>body\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>\<rho>\<^esub>"
     by (rule ESem_fresh_cong) (auto simp add: lookup_env_restr_eq)
   finally show ?thesis.
 qed
 declare ESem.simps(4)[simp del]
 
 
 subsubsection \<open>Denotation of Substitution\<close>
 
 lemma ESem_subst_same: "\<rho> x = \<rho> y \<Longrightarrow>  \<lbrakk> e \<rbrakk>\<^bsub>\<rho>\<^esub> = \<lbrakk> e[x::= y] \<rbrakk>\<^bsub>\<rho>\<^esub>"
   and 
   "\<rho> x = \<rho> y  \<Longrightarrow>  (\<^bold>\<lbrakk> as \<^bold>\<rbrakk>\<^bsub>\<rho>\<^esub>) = \<^bold>\<lbrakk> as[x::h=y] \<^bold>\<rbrakk>\<^bsub>\<rho>\<^esub>"
 proof (nominal_induct e and as avoiding: x y arbitrary: \<rho> and \<rho> rule:exp_heap_strong_induct)
 case Var thus ?case by auto
 next
 case App
   from App(1)[OF App(2)] App(2)
   show ?case by auto
 next
 case (Let as exp x y \<rho>)
   from \<open>atom ` domA as \<sharp>* x\<close> \<open>atom ` domA as  \<sharp>* y\<close> 
   have "x \<notin> domA as" "y \<notin> domA as"
     by (metis fresh_star_at_base imageI)+
   hence [simp]:"domA (as[x::h=y]) = domA as" 
     by (metis bn_subst)
 
   from \<open>\<rho> x = \<rho> y\<close>
   have "(\<lbrace>as\<rbrace>\<rho>) x = (\<lbrace>as\<rbrace>\<rho>) y"
     using \<open>x \<notin> domA as\<close> \<open>y \<notin> domA as\<close>
     by (simp add: lookup_HSem_other)
   hence "\<lbrakk>exp\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>\<rho>\<^esub> = \<lbrakk>exp[x::=y]\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>\<rho>\<^esub>"
     by (rule Let)
   moreover
   from \<open>\<rho> x = \<rho> y\<close>
   have "\<lbrace>as\<rbrace>\<rho> = \<lbrace>as[x::h=y]\<rbrace>\<rho>" and "(\<lbrace>as\<rbrace>\<rho>) x = (\<lbrace>as[x::h=y]\<rbrace>\<rho>) y"
     apply (induction rule: parallel_HSem_ind)
     apply (intro adm_lemmas cont2cont cont2cont_fun)
     apply simp
     apply simp
     apply simp
     apply (erule arg_cong[OF Let(3)])
     using \<open>x \<notin> domA as\<close> \<open>y \<notin> domA as\<close>
     apply simp
     done
   ultimately
   show ?case using Let(1,2,3) by (simp add: fresh_star_Pair)
 next
 case (Lam var exp x y \<rho>)
   from \<open>\<rho> x = \<rho> y\<close>
   have "\<And>v. (\<rho>(var := v)) x = (\<rho>(var := v)) y"
     using Lam(1,2) by (simp add: fresh_at_base)
   hence "\<And> v. \<lbrakk>exp\<rbrakk>\<^bsub>\<rho>(var := v)\<^esub> = \<lbrakk>exp[x::=y]\<rbrakk>\<^bsub>\<rho>(var := v)\<^esub>"
     by (rule Lam)
   thus ?case using Lam(1,2) by simp
 next
 case IfThenElse
   from IfThenElse(1)[OF IfThenElse(4)] IfThenElse(2)[OF IfThenElse(4)] IfThenElse(3)[OF IfThenElse(4)]
   show ?case
     by simp
 next
 case Nil thus ?case by auto
 next
 case Cons
   from Cons(1,2)[OF Cons(3)] Cons(3)
   show ?case by auto
 qed auto
 
 lemma ESem_subst:
   shows "\<lbrakk> e \<rbrakk>\<^bsub>\<sigma>(x := \<sigma> y)\<^esub> = \<lbrakk> e[x::= y] \<rbrakk>\<^bsub>\<sigma>\<^esub>"
 proof(cases "x = y")
   case False
   hence [simp]: "x \<notin> fv e[x::=y]" by (auto simp add: fv_def supp_subst supp_at_base dest: subsetD[OF supp_subst]) 
 
   have "\<lbrakk> e \<rbrakk>\<^bsub>\<sigma>(x := \<sigma> y)\<^esub> = \<lbrakk> e[x::= y] \<rbrakk>\<^bsub>\<sigma>(x := \<sigma> y)\<^esub>"
     by (rule ESem_subst_same) simp
   also have "\<dots> = \<lbrakk> e[x::= y] \<rbrakk>\<^bsub>\<sigma>\<^esub>"
     by (rule ESem_fresh_cong) simp
   finally
   show ?thesis.
 next
   case True
   thus ?thesis by simp
 qed
 
 end
 
 end
diff --git a/thys/MiniML/W.thy b/thys/MiniML/W.thy
--- a/thys/MiniML/W.thy
+++ b/thys/MiniML/W.thy
@@ -1,585 +1,558 @@
 (* Title:     HOL/MiniML/W.thy
    Author:    Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow
    Copyright  1996 TU Muenchen
 *)
 
 section "Correctness and completeness of type inference algorithm W"
 
 theory W
 imports MiniML
 begin
 
 type_synonym result_W = "(subst * typ * nat) option"
 
 \<comment> \<open>type inference algorithm W\<close>
 primrec W :: "[expr, ctxt, nat] => result_W" where
   "W (Var i) A n =  
      (if i < length A then Some( id_subst,   
                                  bound_typ_inst (\<lambda>b. TVar(b+n)) (A!i),   
                                  n + (min_new_bound_tv (A!i)) )  
                       else None)"
   
 | "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
                      Some( S, (S n) -> t, m) )"
   
 | "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
                          (S2,t2,m2) := W e2 ($S1 A) m1;
                          U := mgu ($S2 t1) (t2 -> (TVar m2));
                          Some( $U \<circ> $S2 \<circ> S1, U m2, Suc m2) )"
   
 | "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
                          (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
                          Some( $S2 \<circ> S1, t2, m2) )"
 
 
 declare Suc_le_lessD [simp]
 
 inductive_cases has_type_casesE:
 "A |- Var n :: t"
 "A |- Abs e :: t"
 "A |- App e1 e2 ::t"
 "A |- LET e1 e2 ::t"
 
 
 \<comment> \<open>the resulting type variable is always greater or equal than the given one\<close>
 lemma W_var_ge [rule_format (no_asm)]: 
   "\<forall>A n S t m. W e A n  = Some (S,t,m) \<longrightarrow> n\<le>m"
 apply (induct_tac "e")
 (* case Var(n) *)
 apply (simp (no_asm) split: split_option_bind)
 (* case Abs e *)
 apply (simp (no_asm) split: split_option_bind)
 apply (fast dest: Suc_leD)
 (* case App e1 e2 *)
 apply (simp (no_asm) split: split_option_bind)
 apply (blast intro: le_SucI le_trans)
 (* case LET e1 e2 *)
 apply (simp (no_asm) split: split_option_bind)
 apply (blast intro: le_trans)
 done
 
 declare W_var_ge [simp]
 
 lemma W_var_geD: 
   "Some (S,t,m) = W e A n \<Longrightarrow> n\<le>m"
 apply (simp add: eq_sym_conv)
 done
 
 lemma new_tv_compatible_W: 
   "new_tv n A \<Longrightarrow> Some (S,t,m) = W e A n \<Longrightarrow> new_tv m A"
 apply (drule W_var_geD)
 apply (rule new_scheme_list_le)
 apply assumption
 apply assumption
 done
 
 lemma new_tv_bound_typ_inst_sch [rule_format (no_asm)]: 
   "new_tv n sch \<longrightarrow> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (\<lambda>b. TVar (b + n)) sch)"
 apply (induct_tac "sch")
   apply simp
  apply (simp add: add.commute)
 apply (intro strip)
 apply simp
 apply (erule conjE)
 apply (rule conjI)
  apply (rule new_tv_le)
   prefer 2 apply (assumption)
  apply (rule add_le_mono)
   apply (simp (no_asm))
  apply (simp (no_asm) add: max_def)
 apply (rule new_tv_le)
  prefer 2 apply (assumption)
 apply (rule add_le_mono)
  apply (simp (no_asm))
 apply (simp (no_asm) add: max_def)
 done
 
 declare new_tv_bound_typ_inst_sch [simp]
 
 \<comment> \<open>resulting type variable is new\<close>
 lemma new_tv_W [rule_format (no_asm)]: 
   "\<forall>n A S t m. new_tv n A \<longrightarrow> W e A n = Some (S,t,m) \<longrightarrow>     
                new_tv m S \<and> new_tv m t"
 proof (induct e)
   case Var then show ?case
     apply (simp (no_asm) split: split_option_bind)
     apply (intro strip)
     apply (drule new_tv_nth_nat_A)
     apply assumption
     apply (simp (no_asm_simp))
     done
 next
   case Abs then show ?case
     apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split: split_option_bind)
     apply (intro strip)
     apply (erule_tac x = "Suc n" in allE)
     apply (erule_tac x = " (FVar n) #A" in allE)
     apply (fastforce simp add: new_tv_subst new_tv_Suc_list)
     done
 next
   case App then show ?case
     apply (simp (no_asm) split: split_option_bind)
     apply (intro strip)
     apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
     apply (erule_tac x = "n" in allE)
     apply (erule_tac x = "A" in allE)
     apply (erule_tac x = "S1" in allE)
     apply (erule_tac x = "t1" in allE)
     apply (erule_tac x = "n1" in allE)
     apply (erule_tac x = "n1" in allE)
     apply (simp add: eq_sym_conv del: all_simps)
     apply (erule_tac x = "$S1 A" in allE)
     apply (erule_tac x = "S2" in allE)
     apply (erule_tac x = "t2" in allE)
     apply (erule_tac x = "n2" in allE)
     apply ( simp add: o_def rotate_Some)
     apply (rule conjI)
     apply (rule new_tv_subst_comp_2)
     apply (rule new_tv_subst_comp_2)
     apply (rule lessI [THEN less_imp_le, THEN new_tv_le])
     apply (rule_tac n = "n1" in new_tv_subst_le)
     apply (simp add: rotate_Some)
     apply (simp (no_asm_simp))
     apply (fast dest: W_var_geD intro: new_scheme_list_le new_tv_subst_scheme_list lessI [THEN less_imp_le [THEN new_tv_subst_le]])
     apply (erule sym [THEN mgu_new])
     apply (blast dest!: W_var_geD
       intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te 
       new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
 
     apply (erule impE)
     apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
     apply clarsimp
 
     apply (rule lessI [THEN new_tv_subst_var])
     apply (erule sym [THEN mgu_new])
     apply (blast dest!: W_var_geD
       intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te 
       new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
 
     apply (erule impE)
     apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
     apply clarsimp
     done
 next
   case LET then show ?case
     apply (simp (no_asm) split: split_option_bind)
     apply (intro strip)
     apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, assumption, erule impE, assumption) 
     apply (erule conjE)
     apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, erule_tac [2] notE impE,
       tactic "assume_tac @{context} 2")
     apply (simp only: new_tv_def)
     apply (simp (no_asm_simp))
     apply (drule W_var_ge)+
     apply (rule allI)
     apply (intro strip)
     apply (simp only: free_tv_subst)
     apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
     apply (best elim: less_le_trans)
     apply (erule conjE)
     apply (rule conjI)
     apply (simp only: o_def)
     apply (rule new_tv_subst_comp_2)
     apply (erule W_var_ge [THEN new_tv_subst_le])
     apply assumption
     apply assumption
     apply assumption
     done
 qed
 
 lemma free_tv_bound_typ_inst1 [rule_format (no_asm)]: 
   "(v \<notin> free_tv sch) \<longrightarrow> (v \<in> free_tv (bound_typ_inst (TVar \<circ> S) sch)) \<longrightarrow> (\<exists>x. v = S x)"
 apply (induct_tac "sch")
 apply simp
 apply simp
 apply (intro strip)
 apply (rule exI)
 apply (rule refl)
 apply simp
 done
 
 declare free_tv_bound_typ_inst1 [simp]
 
 lemma free_tv_W [rule_format (no_asm)]: 
   "\<forall>n A S t m v. W e A n = Some (S,t,m) \<longrightarrow>             
           (v\<in>free_tv S \<or> v\<in>free_tv t) \<longrightarrow> v<n \<longrightarrow> v\<in>free_tv A"
 proof (induct e)
   case (Var n) then show ?case
     apply (simp (no_asm) add: free_tv_subst split: split_option_bind)
     apply (intro strip)
     apply (case_tac "v : free_tv (A!n)")
     apply simp
     apply (drule free_tv_bound_typ_inst1)
     apply (simp (no_asm) add: o_def)
     apply (erule exE)
     apply simp
     done
   case Abs then show ?case
     apply (simp add: free_tv_subst split: split_option_bind del: all_simps)
     apply (intro strip)
     apply (rename_tac S t n1 v)
     apply (erule_tac x = "Suc n" in allE)
     apply (erule_tac x = "FVar n # A" in allE)
     apply (erule_tac x = "S" in allE)
     apply (erule_tac x = "t" in allE)
     apply (erule_tac x = "n1" in allE)
     apply (erule_tac x = "v" in allE)
     apply (bestsimp intro: cod_app_subst simp add: less_Suc_eq)
     done
   case App then show ?case
     apply (simp (no_asm) split: split_option_bind del: all_simps)
     apply (intro strip)
     apply (rename_tac S t n1 S1 t1 n2 S2 v)
     apply (erule_tac x = "n" in allE)
     apply (erule_tac x = "A" in allE)
     apply (erule_tac x = "S" in allE)
     apply (erule_tac x = "t" in allE)
     apply (erule_tac x = "n1" in allE)
     apply (erule_tac x = "n1" in allE)
     apply (erule_tac x = "v" in allE)
     (* second case *)
     apply (erule_tac x = "$ S A" in allE)
     apply (erule_tac x = "S1" in allE)
     apply (erule_tac x = "t1" in allE)
     apply (erule_tac x = "n2" in allE)
     apply (erule_tac x = "v" in allE)
     apply (intro conjI impI | elim conjE)+
     apply (simp add: rotate_Some o_def)
     apply (drule W_var_geD)
     apply (drule W_var_geD)
     apply ( (frule less_le_trans) , (assumption))
     apply clarsimp 
     apply (drule free_tv_comp_subst [THEN subsetD])
     apply (drule sym [THEN mgu_free])
     apply clarsimp 
     apply (fastforce dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_scheme_list [THEN subsetD] less_le_trans less_not_refl2 subsetD)
     apply simp
     apply (drule sym [THEN W_var_geD])
     apply (drule sym [THEN W_var_geD])
     apply ( (frule less_le_trans) , (assumption))
     apply clarsimp
     apply (drule mgu_free)
     apply (fastforce dest: mgu_free codD free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_scheme_list [THEN subsetD] less_le_trans subsetD)
     done
 next
   case LET then show ?case
     apply (simp (no_asm) split: split_option_bind del: all_simps)
     apply (intro strip)
     apply (rename_tac S1 t1 n2 S2 t2 n3 v)
     apply (erule_tac x = "n" in allE)
     apply (erule_tac x = "A" in allE)
     apply (erule_tac x = "S1" in allE)
     apply (erule_tac x = "t1" in allE)
     apply (rotate_tac -1)
     apply (erule_tac x = "n2" in allE)
     apply (rotate_tac -1)
     apply (erule_tac x = "v" in allE)
     apply (erule (1) notE impE)
     apply (erule allE,erule allE,erule allE,erule allE,erule allE,erule_tac  x = "v" in allE)
     apply (erule (1) notE impE)
     apply simp
     apply (rule conjI)
     apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] free_tv_o_subst [THEN subsetD] W_var_ge dest: less_le_trans)
     apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] W_var_ge dest: less_le_trans)
     done
 qed
 
 lemma weaken_A_Int_B_eq_empty: "(\<forall>x. x \<in> A \<longrightarrow> x \<notin> B) \<Longrightarrow> A \<inter> B = {}"
 apply fast
 done
 
 lemma weaken_not_elem_A_minus_B: "x \<notin> A \<or> x \<in> B \<Longrightarrow> x \<notin> A - B"
 apply fast
 done
 
 \<comment> \<open>correctness of W with respect to @{text has_type}\<close>
 lemma W_correct_lemma [rule_format (no_asm)]: "\<forall>A S t m n . new_tv n A \<longrightarrow> Some (S,t,m) = W e A n \<longrightarrow> $S A |- e :: t"
 apply (induct_tac "e")
 (* case Var n *)
 apply simp
 apply (intro strip)
 apply (rule has_type.VarI)
 apply (simp (no_asm))
 apply (simp (no_asm) add: is_bound_typ_instance)
 apply (rule exI)
 apply (rule refl)
 (* case Abs e *)
 apply (simp add: app_subst_list split: split_option_bind)
 apply (intro strip)
 apply (erule_tac x = " (mk_scheme (TVar n)) # A" in allE)
 apply simp
 apply (rule has_type.AbsI)
 apply (drule le_refl [THEN le_SucI, THEN new_scheme_list_le])
 apply (drule sym)
 apply (erule allE)+
 apply (erule impE)
 apply (erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
 apply (simp (no_asm_simp))
 apply assumption
 (* case App e1 e2 *)
 apply (simp (no_asm) split: split_option_bind)
 apply (intro strip)
 apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
 apply (rule_tac ?t2.0 = "$ S3 t2" in has_type.AppI)
 apply (rule_tac S1 = "S3" in app_subst_TVar [THEN subst])
 apply (rule app_subst_Fun [THEN subst])
 apply (rule_tac t = "$S3 (t2 -> (TVar n2))" and s = "$S3 ($S2 t1) " in subst)
 apply simp
 apply (simp only: subst_comp_scheme_list [symmetric] o_def) 
 apply ((rule has_type_cl_sub [THEN spec]) , (rule has_type_cl_sub [THEN spec]))
 apply (simp add: eq_sym_conv)
 apply (simp add: subst_comp_scheme_list [symmetric] o_def has_type_cl_sub eq_sym_conv)
 apply (rule has_type_cl_sub [THEN spec])
 apply (frule new_tv_W)
 apply assumption
 apply (drule conjunct1)
 apply (frule new_tv_subst_scheme_list)
 apply (rule new_scheme_list_le)
 apply (rule W_var_ge)
 apply assumption
 apply assumption
 apply (erule thin_rl)
 apply (erule allE)+
 apply (drule sym)
 apply (drule sym)
 apply (erule thin_rl)
 apply (erule thin_rl)
 apply (erule (1) notE impE)
 apply (erule (1) notE impE)
 apply assumption
 (* case Let e1 e2 *)
 apply (simp (no_asm) split: split_option_bind)
 apply (intro strip)
 (*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
 apply (rename_tac S1 t1 m1 S2)
 apply (rule_tac ?t1.0 = "$ S2 t1" in has_type.LETI)
  apply (simp (no_asm) add: o_def)
  apply (simp only: subst_comp_scheme_list [symmetric])
  apply (rule has_type_cl_sub [THEN spec])
  apply (drule_tac x = "A" in spec)
  apply (drule_tac x = "S1" in spec)
  apply (drule_tac x = "t1" in spec)
  apply (drule_tac x = "m1" in spec)
  apply (drule_tac x = "n" in spec)
  apply (erule (1) notE impE)
  apply (simp add: eq_sym_conv)
 apply (simp (no_asm) add: o_def)
 apply (simp only: subst_comp_scheme_list [symmetric])
 apply (rule gen_subst_commutes [symmetric, THEN subst])
  apply (rule_tac [2] app_subst_Cons [THEN subst])
  apply (erule_tac [2] thin_rl)
  apply (drule_tac [2] x = "gen ($S1 A) t1 # $ S1 A" in spec)
  apply (drule_tac [2] x = "S2" in spec)
  apply (drule_tac [2] x = "t" in spec)
  apply (drule_tac [2] x = "m" in spec)
  apply (drule_tac [2] x = "m1" in spec)
  apply (frule_tac [2] new_tv_W)
-  prefer 2 apply (assumption)
- apply (drule_tac [2] conjunct1)
- apply (frule_tac [2] new_tv_subst_scheme_list)
-  apply (rule_tac [2] new_scheme_list_le)
-   apply (rule_tac [2] W_var_ge)
-   prefer 2 apply (assumption)
-  prefer 2 apply (assumption)
- apply (erule_tac [2] impE)
-  apply (rule_tac [2] A = "$ S1 A" in new_tv_only_depends_on_free_tv_scheme_list)
-   prefer 2 apply simp
-   apply (fast)
-  prefer 2 apply (assumption)
- prefer 2 apply simp
+    prefer 2 apply (assumption)
+  prefer 2
+  apply (metis new_tv_Cons new_tv_compatible_W new_tv_compatible_gen new_tv_subst_scheme_list)
 apply (rule weaken_A_Int_B_eq_empty)
 apply (rule allI)
 apply (intro strip)
 apply (rule weaken_not_elem_A_minus_B)
-apply (case_tac "x < m1")
- apply (rule disjI2)
- apply (rule free_tv_gen_cons [THEN subst])
- apply (rule free_tv_W)
-   apply assumption
-  apply simp
- apply assumption
-apply (rule disjI1)
-apply (drule new_tv_W)
-apply assumption
-apply (drule conjunct2)
-apply (rule new_tv_not_free_tv)
-apply (rule new_tv_le)
- prefer 2 apply (assumption)
-apply (simp add: linorder_not_less)
-done
+  by (metis free_tv_W free_tv_gen_cons free_tv_le_new_tv new_tv_W)
 
 \<comment> \<open>Completeness of W w.r.t. @{text has_type}\<close>
 lemma W_complete_lemma [rule_format (no_asm)]: 
   "\<forall>S' A t' n. $S' A |- e :: t' \<longrightarrow> new_tv n A \<longrightarrow>
                (\<exists>S t. (\<exists>m. W e A n = Some (S,t,m)) \<and>
                        (\<exists>R. $S' A = $R ($S A) \<and> t' = $R t))"
-apply (induct e)
-   (* case Var n *)
-   apply (intro strip)
-   apply (simp (no_asm) cong add: conj_cong)
-   apply (erule has_type_casesE)
-   apply (simp add: is_bound_typ_instance)
-   apply (erule exE)
-   apply (hypsubst)
-   apply (rename_tac "S")
-   apply (rule_tac x = "\<lambda>x. (if x < n then S' x else S (x - n))" in exI)
-   apply (rule conjI)
-   apply (simp (no_asm_simp))
-   apply (simp (no_asm_simp) add: bound_typ_inst_composed_subst [symmetric] new_tv_nth_nat_A o_def nth_subst 
-                             del: bound_typ_inst_composed_subst)
-
-  (* case Abs e *)
-  apply (intro strip)
-  apply (erule has_type_casesE)
-  apply (erule_tac x = "\<lambda>x. if x=n then t1 else (S' x) " in allE)
-  apply (erule_tac x = " (FVar n) #A" in allE)
-  apply (erule_tac x = "t2" in allE)
-  apply (erule_tac x = "Suc n" in allE)
-  apply (bestsimp dest!: mk_scheme_injective cong: conj_cong split: split_option_bind)
+  apply (induct e)
+    (* case Var n *)
+     apply (intro strip)
+     apply (simp (no_asm) cong add: conj_cong)
+     apply (erule has_type_casesE)
+     apply (simp add: is_bound_typ_instance)
+     apply (erule exE)
+     apply (hypsubst)
+     apply (rename_tac "S")
+     apply (rule_tac x = "\<lambda>x. (if x < n then S' x else S (x - n))" in exI)
+     apply (rule conjI)
+      apply (simp (no_asm_simp))
+     apply (simp (no_asm_simp) add: bound_typ_inst_composed_subst [symmetric] new_tv_nth_nat_A o_def nth_subst 
+      del: bound_typ_inst_composed_subst)
 
- (* case App e1 e2 *)
- apply (intro strip)
- apply (erule has_type_casesE)
- apply (erule_tac x = "S'" in allE)
- apply (erule_tac x = "A" in allE)
- apply (erule_tac x = "t2 -> t'" in allE)
- apply (erule_tac x = "n" in allE)
- apply safe
- apply (erule_tac x = "R" in allE)
- apply (erule_tac x = "$ S A" in allE)
- apply (erule_tac x = "t2" in allE)
- apply (erule_tac x = "m" in allE)
- apply simp
- apply safe
-  apply (blast intro: sym [THEN W_var_geD] new_tv_W [THEN conjunct1] new_scheme_list_le new_tv_subst_scheme_list)
- 
- (** LEVEL 33 **)
-apply (subgoal_tac "$ (\<lambda>x. if x=ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t) = $ (\<lambda>x. if x=ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) (ta -> (TVar ma))")
-apply (rule_tac [2] t = "$ (\<lambda>x. if x = ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t) " and s = " ($ Ra ta) -> t'" in ssubst)
-prefer 2 apply (simp (no_asm_simp) add: subst_comp_te) prefer 2
-apply (rule_tac [2] eq_free_eq_subst_te)
-prefer 2 apply (intro strip) prefer 2
-apply (subgoal_tac [2] "na \<noteq>ma")
- prefer 3 apply (best dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
-apply (case_tac [2] "na:free_tv Sa")
-(* n1 \<notin> free_tv S1 *)
-apply (frule_tac [3] not_free_impl_id)
- prefer 3 apply (simp)
-(* na : free_tv Sa *)
-apply (drule_tac [2] A1 = "$ S A" in trans [OF _ subst_comp_scheme_list])
-apply (drule_tac [2] eq_subst_scheme_list_eq_free)
- prefer 2 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
-prefer 2 apply (simp (no_asm_simp)) prefer 2
-apply (case_tac [2] "na:dom Sa")
-(* na \<notin> dom Sa *)
- prefer 3 apply (simp add: dom_def)
-(* na : dom Sa *)
-apply (rule_tac [2] eq_free_eq_subst_te)
-prefer 2 apply (intro strip) prefer 2
-apply (subgoal_tac [2] "nb \<noteq> ma")
-apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
-apply (erule_tac [3] conjE)
-apply (drule_tac [3] new_tv_subst_scheme_list)
-   prefer 3 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
-  prefer 3 apply (fastforce dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
- prefer 2 apply (fastforce simp add: cod_def free_tv_subst)
-prefer 2 apply (simp (no_asm)) prefer 2
-apply (rule_tac [2] eq_free_eq_subst_te)
-prefer 2 apply (intro strip) prefer 2
-apply (subgoal_tac [2] "na \<noteq> ma")
-apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
-apply (erule_tac [3] conjE)
-apply (drule_tac [3] sym [THEN W_var_geD])
- prefer 3 apply (fast dest: new_scheme_list_le new_tv_subst_scheme_list new_tv_W new_tv_not_free_tv)
-apply (case_tac [2] "na: free_tv t - free_tv Sa")
-(* case na \<notin> free_tv t - free_tv Sa *)
- prefer 3 
- apply simp
- apply fast
-(* case na : free_tv t - free_tv Sa *)
-prefer 2 apply simp prefer 2
-apply (drule_tac [2] A1 = "$ S A" and r = "$ R ($ S A)" in trans [OF _ subst_comp_scheme_list])
-apply (drule_tac [2] eq_subst_scheme_list_eq_free)
- prefer 2 
- apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
-(** LEVEL 73 **)
- prefer 2 apply (simp add: free_tv_subst dom_def)
-apply (simp (no_asm_simp) split: split_option_bind)
-apply safe
-apply (drule mgu_Some)
- apply fastforce  
-(** LEVEL 78 *)
-apply (drule mgu_mg, assumption)
-apply (erule exE)
-apply (rule_tac x = "Rb" in exI)
-apply (rule conjI)
-apply (drule_tac [2] x = "ma" in fun_cong)
- prefer 2 apply (simp add: eq_sym_conv)
-apply (simp (no_asm) add: subst_comp_scheme_list)
-apply (simp (no_asm) add: subst_comp_scheme_list [symmetric])
-apply (rule_tac A1 = "($ Sa ($ S A))" in trans [OF _ subst_comp_scheme_list [symmetric]])
-apply (simp add: o_def eq_sym_conv)
-apply (drule_tac s = "Some _" in sym)
-apply (rule eq_free_eq_subst_scheme_list)
-apply safe
-apply (subgoal_tac "ma \<noteq> na")
-apply (frule_tac [2] new_tv_W) prefer 2 apply assumption
-apply (erule_tac [2] conjE)
-apply (drule_tac [2] new_tv_subst_scheme_list)
- prefer 2 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
-apply (frule_tac [2] n = "m" in new_tv_W) prefer 2 apply assumption
-apply (erule_tac [2] conjE)
-apply (drule_tac [2] free_tv_app_subst_scheme_list [THEN subsetD])
- apply (tactic \<open>
+(* case Abs e *)
+    apply (intro strip)
+    apply (erule has_type_casesE)
+    apply (erule_tac x = "\<lambda>x. if x=n then t1 else (S' x) " in allE)
+    apply (erule_tac x = " (FVar n) #A" in allE)
+    apply (erule_tac x = "t2" in allE)
+    apply (erule_tac x = "Suc n" in allE)
+    apply (bestsimp dest!: mk_scheme_injective cong: conj_cong split: split_option_bind)
+
+(* case App e1 e2 *)
+   apply (intro strip)
+   apply (erule has_type_casesE)
+   apply (erule_tac x = "S'" in allE)
+   apply (erule_tac x = "A" in allE)
+   apply (erule_tac x = "t2 -> t'" in allE)
+   apply (erule_tac x = "n" in allE)
+   apply safe
+   apply (erule_tac x = "R" in allE)
+   apply (erule_tac x = "$ S A" in allE)
+   apply (erule_tac x = "t2" in allE)
+   apply (erule_tac x = "m" in allE)
+   apply simp
+   apply safe
+    apply (blast intro: sym [THEN W_var_geD] new_tv_W [THEN conjunct1] new_scheme_list_le new_tv_subst_scheme_list)
+
+(** LEVEL 33 **)
+   apply (subgoal_tac "$ (\<lambda>x. if x=ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t) = $ (\<lambda>x. if x=ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) (ta -> (TVar ma))")
+    apply (rule_tac [2] t = "$ (\<lambda>x. if x = ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t) " and s = " ($ Ra ta) -> t'" in ssubst)
+     prefer 2 apply (simp (no_asm_simp) add: subst_comp_te) prefer 2
+     apply (rule_tac [2] eq_free_eq_subst_te)
+     prefer 2 apply (intro strip) prefer 2
+     apply (subgoal_tac [2] "na \<noteq>ma")
+      prefer 3 apply (best dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
+     apply (case_tac [2] "na:free_tv Sa")
+    (* n1 \<notin> free_tv S1 *)
+      apply (frule_tac [3] not_free_impl_id)
+      prefer 3 apply (simp)
+    (* na : free_tv Sa *)
+     apply (drule_tac [2] A1 = "$ S A" in trans [OF _ subst_comp_scheme_list])
+     apply (drule_tac [2] eq_subst_scheme_list_eq_free)
+      prefer 2 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
+     prefer 2 apply (simp (no_asm_simp)) prefer 2
+     apply (case_tac [2] "na:dom Sa")
+    (* na \<notin> dom Sa *)
+      prefer 3 apply (simp add: dom_def)
+    (* na : dom Sa *)
+     apply (rule_tac [2] eq_free_eq_subst_te)
+     prefer 2 apply (intro strip) prefer 2
+     apply (subgoal_tac [2] "nb \<noteq> ma")
+      apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
+      apply (erule_tac [3] conjE)
+      apply (drule_tac [3] new_tv_subst_scheme_list)
+       prefer 3 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
+      prefer 3 apply (fastforce dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
+     prefer 2 apply (fastforce simp add: cod_def free_tv_subst)
+    prefer 2 apply (simp (no_asm)) prefer 2
+    apply (rule_tac [2] eq_free_eq_subst_te)
+    prefer 2 apply (intro strip) prefer 2
+    apply (subgoal_tac [2] "na \<noteq> ma")
+     apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
+     apply (erule_tac [3] conjE)
+     apply (drule_tac [3] sym [THEN W_var_geD])
+     prefer 3 apply (fast dest: new_scheme_list_le new_tv_subst_scheme_list new_tv_W new_tv_not_free_tv)
+    apply (case_tac [2] "na: free_tv t - free_tv Sa")
+    (* case na \<notin> free_tv t - free_tv Sa *)
+     prefer 3 
+     apply simp
+     apply fast
+    (* case na : free_tv t - free_tv Sa *)
+    prefer 2 apply simp prefer 2
+    apply (drule_tac [2] A1 = "$ S A" and r = "$ R ($ S A)" in trans [OF _ subst_comp_scheme_list])
+    apply (drule_tac [2] eq_subst_scheme_list_eq_free)
+     prefer 2 
+     apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
+    (** LEVEL 73 **)
+    prefer 2 apply (simp add: free_tv_subst dom_def)
+   apply (simp (no_asm_simp) split: split_option_bind)
+   apply safe
+    apply (drule mgu_Some)
+    apply fastforce  
+    (** LEVEL 78 *)
+   apply (drule mgu_mg, assumption)
+   apply (erule exE)
+   apply (rule_tac x = "Rb" in exI)
+   apply (rule conjI)
+    apply (drule_tac [2] x = "ma" in fun_cong)
+    prefer 2 apply (simp add: eq_sym_conv)
+   apply (simp (no_asm) add: subst_comp_scheme_list)
+   apply (simp (no_asm) add: subst_comp_scheme_list [symmetric])
+   apply (rule_tac A1 = "($ Sa ($ S A))" in trans [OF _ subst_comp_scheme_list [symmetric]])
+   apply (simp add: o_def eq_sym_conv)
+   apply (drule_tac s = "Some _" in sym)
+   apply (rule eq_free_eq_subst_scheme_list)
+   apply safe
+   apply (subgoal_tac "ma \<noteq> na")
+    apply (frule_tac [2] new_tv_W) prefer 2 apply assumption
+    apply (erule_tac [2] conjE)
+    apply (drule_tac [2] new_tv_subst_scheme_list)
+     prefer 2 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
+    apply (frule_tac [2] n = "m" in new_tv_W) prefer 2 apply assumption
+    apply (erule_tac [2] conjE)
+    apply (drule_tac [2] free_tv_app_subst_scheme_list [THEN subsetD])
+    apply (tactic \<open>
     (fast_tac (put_claset (claset_of @{theory_context Fun}) @{context}
       addDs [sym RS @{thm W_var_geD}, @{thm new_scheme_list_le}, @{thm codD},
         @{thm new_tv_not_free_tv}]) 2)\<close>)
-apply (case_tac "na: free_tv t - free_tv Sa")
-(* case na \<notin> free_tv t - free_tv Sa *)
- prefer 2 apply simp apply blast
-(* case na : free_tv t - free_tv Sa *)
-apply simp
-apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
- apply (fastforce dest: codD trans [OF _ subst_comp_scheme_list]
-                       eq_subst_scheme_list_eq_free 
-             simp add: free_tv_subst dom_def)
-(* case Let e1 e2 *)
-apply (erule has_type_casesE)
-apply (erule_tac x = "S'" in allE)
-apply (erule_tac x = "A" in allE)
-apply (erule_tac x = "t1" in allE)
-apply (erule_tac x = "n" in allE)
-apply (erule (1) notE impE)
-apply (erule (1) notE impE)
-apply safe  
-apply (simp (no_asm_simp))
-apply (erule_tac x = "R" in allE)
-apply (erule_tac x = "gen ($ S A) t # $ S A" in allE)
-apply (erule_tac x = "t'" in allE)
-apply (erule_tac x = "m" in allE)
-apply simp
-apply (drule mp)
-apply (rule has_type_le_env)
-apply assumption
-apply (simp (no_asm))
-apply (rule gen_bound_typ_instance)
-apply (drule mp)
-apply (frule new_tv_compatible_W)
-apply (rule sym)
-apply assumption
-apply (fast dest: new_tv_compatible_gen new_tv_subst_scheme_list new_tv_W)
-apply safe
-apply simp
-apply (rule_tac x = "Ra" in exI)
-apply (simp (no_asm) add: o_def subst_comp_scheme_list [symmetric])
-done
+   apply (case_tac "na: free_tv t - free_tv Sa")
+    (* case na \<notin> free_tv t - free_tv Sa *)
+    prefer 2 apply simp apply blast
+    (* case na : free_tv t - free_tv Sa *)
+   apply simp
+   apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
+   apply (fastforce dest: codD trans [OF _ subst_comp_scheme_list]
+      eq_subst_scheme_list_eq_free 
+      simp add: free_tv_subst dom_def)
+    (* case Let e1 e2 *)
+  apply (erule has_type_casesE)
+  apply (erule_tac x = "S'" in allE)
+  apply (erule_tac x = "A" in allE)
+  apply (erule_tac x = "t1" in allE)
+  apply (erule_tac x = "n" in allE)
+  apply (erule (1) notE impE)
+  apply (erule (1) notE impE)
+  apply safe  
+  apply (simp (no_asm_simp))
+  apply (erule_tac x = "R" in allE)
+  apply (erule_tac x = "gen ($ S A) t # $ S A" in allE)
+  apply (erule_tac x = "t'" in allE)
+  apply (erule_tac x = "m" in allE)
+  apply simp
+  apply (drule mp)
+   apply (rule has_type_le_env)
+    apply assumption
+   apply (simp (no_asm))
+   apply (rule gen_bound_typ_instance)
+  apply (drule mp)
+   apply (frule new_tv_compatible_W)
+    apply (rule sym)
+    apply assumption
+   apply (fast dest: new_tv_compatible_gen new_tv_subst_scheme_list new_tv_W)
+  apply safe
+  apply simp
+  apply (rule_tac x = "Ra" in exI)
+  apply (simp (no_asm) add: o_def subst_comp_scheme_list [symmetric])
+  done
 
 
-lemma W_complete: 
+theorem W_complete: 
   "[] |- e :: t' \<Longrightarrow> (\<exists>S t. (\<exists>m. W e [] n = Some(S,t,m)) \<and>
                      (\<exists>R. t' = $ R t))"
-apply (cut_tac A = "[]" and S' = "id_subst" and e = "e" and t' = "t'" in W_complete_lemma)
-apply simp_all
-done
+  by (metis W_complete_lemma app_subst_Nil new_tv_Nil)
 
 end
diff --git a/thys/Statecharts/HAOps.thy b/thys/Statecharts/HAOps.thy
--- a/thys/Statecharts/HAOps.thy
+++ b/thys/Statecharts/HAOps.thy
@@ -1,1174 +1,1117 @@
 (*  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 (simp add: AddSA_HAStates AddSA_CompFun)
-apply (simp add: AddSA_HAStates AddSA_SAs)
-apply auto
-apply (simp add: Int_def)
-apply (cut_tac SA=SA2 in EX_State_SA)
-apply (erule exE)
-apply (frule HAStates_SA_mem)
-apply fast
-apply (simp only: HAStates_def)
-apply fast
-apply (simp add: AddSA_HAStates AddSA_CompFun)
-done
+  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 (rule ballI)
-apply (rule impI)
-apply (subst AddSA_CompFun [THEN sym])
-apply simp
-apply simp
-apply (subst AddSA_CompFun [THEN sym])
-apply (simp add: AddSA_HAStates)
-apply (simp add: AddSA_HAStates)
-apply (subst AddSA_CompFun [THEN sym])
-apply simp
-apply simp
-apply (subst AddSA_CompFun [THEN sym])
-apply (simp add: AddSA_HAStates)
-apply (simp add: AddSA_HAStates)
-apply (rule CompFun_Int_disjoint)
-apply simp
-apply (simp add: AddSA_HAStates)
-apply (simp add: AddSA_HAStates)
-apply (simp only: dom_CompFun [THEN sym])
-apply (cut_tac F="CompFun A [f+] (S, SA1)" and S=T and SA="SA2" in FAddSA_dom_dom_States)
-apply (cut_tac F="CompFun A" and S=S and SA="SA1" in FAddSA_dom_dom_States)
-apply fast
-apply fast
-apply simp
-apply fast
-apply simp
-apply (cut_tac F="CompFun A" and S=S and SA="SA1" in FAddSA_dom_dom_States)
-apply simp
-apply fast
-apply simp
-apply (subst FAddSA_dom_dom_States)
-apply (subst FAddSA_dom_dom_States)
-apply simp
-apply fast
-apply simp
-apply fast
-apply (subst FAddSA_dom_dom_States)
-apply simp
-apply fast
-apply simp
-apply (subst FAddSA_dom_dom_States)
-apply (subst FAddSA_dom_dom_States)
-apply simp
-apply fast
-apply simp
-apply fast
-apply (subst FAddSA_dom_dom_States)
-apply simp
-apply fast
-apply simp
-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
-apply (case_tac "{SA2} \<notin> ran (CompFun A [f+] (S,SA1))")
-apply fast
-apply (simp add:AddSA_CompFun_ran_not_mem) 
-done
+  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 (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
 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 (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 (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 (rule rtrancl_into_rtrancl)
 apply auto
 apply (rule rtrancl_into_rtrancl)
 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