Theory ConsFuncHBDModel

theory ConsFuncHBDModel
imports ExtendedHBDAlgebra Constructive
subsection{*Constructive Functions are a Model of the HBD Algebra*}

(* Was: Model.thy *)

theory ConsFuncHBDModel imports ExtendedHBDAlgebra Constructive
begin

  datatype Types = int | bool | nat

  datatype Values = Inte (integer : "int option") | Bool (boolean: "bool option") | Nat (natural: "nat option")

  primrec tv :: "Values ⇒ Types" where
      "tv (Inte i) = int" |
      "tv (Bool b) = bool" |
      "tv (Nat n) = nat"
  
  primrec tp :: "Values list ⇒ Types list" where
      "tp [] = []" |
      "tp (a # v) = tv a # tp v"

  fun le_val :: "Values ⇒ Values ⇒ bool" where
    "(le_val (Inte v) (Inte u)) = (v ≤ u)" |
    "(le_val (Bool v) (Bool u)) = (v ≤ u)" |
    "(le_val (Nat v) (Nat u)) = (v ≤ u)"  |
    "le_val _ _ = False"

  instantiation Values :: order
    begin
      definition le_Values_def: "((v::Values) ≤ u) = le_val v u"
      definition less_Values_def: "((v::Values) < u) = (v ≤ u ∧ ¬ u ≤ v)"
      instance
      proof
        fix x::Values fix y::Values show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
          by (simp add: less_Values_def)

       show "x ≤ x"
          by (case_tac x, simp_all add: le_Values_def less_Values_def)
       

      fix z show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
          apply (case_tac x, simp_all)
          apply (case_tac y, case_tac z, simp_all add: less_option_def le_Values_def less_Values_def)
          apply (case_tac y, simp_all add:  less_option_def le_Values_def less_Values_def)
          apply (case_tac z, simp_all)
          apply (case_tac y, case_tac z, simp_all add:  less_option_def le_Values_def less_Values_def)
          by (case_tac z, simp_all)

      show "x ≤ y ⟹ y ≤ x ⟹ x = y"
          apply (case_tac x, simp_all)
          apply (case_tac y, simp_all add: less_option_def le_Values_def less_Values_def)
          apply (case_tac y, simp_all add:  less_option_def le_Values_def less_Values_def)
          by (case_tac y, simp_all add:  less_option_def le_Values_def less_Values_def)

     qed
    end

  fun le_list :: "'a::order list ⇒ 'a::order list ⇒ bool" where
    "le_list [] [] = True" |
    "le_list (a # x) (b # y) = (a ≤ b ∧ le_list x y)" |
    "le_list _ _ = False"
    
  instantiation list :: (order) order 
    begin
      definition le_list_def: "((v::'a list) ≤ u) = le_list u v"
      definition less_list_def: "((v::'a list) < u) = (v ≤ u ∧ ¬ u ≤ v)"
      instance
      proof
        fix x y show "((x::'a list) < y) = (x ≤ y ∧ ¬ y ≤ x)"
          by (simp add: less_list_def)
        show "x ≤ x"
          by (induction x, simp_all add: le_list_def)

        fix z show "⋀ y z . x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
          apply (induction x, simp_all add: le_list_def)
          apply (case_tac y, simp_all add: le_list_def)
          apply (case_tac y, simp_all)
          by (case_tac z, simp_all, auto)
       show "⋀ y . x ≤ y ⟹ y ≤ x ⟹ x = y"
          apply (induction x, simp_all add: le_list_def)
          apply (case_tac y, simp_all add: le_list_def)
          by (case_tac y, simp_all add: le_list_def, auto)
     qed
   end

  lemma [simp]: "mono integer"
    apply (simp add: mono_def le_Values_def, safe)
    apply (case_tac x, simp_all)
    apply (case_tac y, simp_all)
    apply (case_tac y, simp_all)
    apply (simp add: integer_def)
    apply (case_tac y, simp_all)
    by (simp add: integer_def)

  lemma [simp]: "mono boolean"
    apply (simp add: mono_def le_Values_def, safe)
    apply (case_tac x, simp_all)
    apply (case_tac y, simp_all)
    apply (simp add: boolean_def)
    apply (case_tac y, simp_all)
    apply (case_tac y, simp_all)
    by (simp add: boolean_def)

  lemma [simp]: "mono natural"
    apply (simp add: mono_def le_Values_def, safe)
    apply (case_tac x, simp_all)
    apply (case_tac y, simp_all)
    apply (simp add: natural_def)
    apply (case_tac y, simp_all)
    apply (simp add: natural_def)
    by (case_tac y, simp_all)
      
  definition "has_in_type x  = {f . (dom f = {v . tp v = x})}"
  definition "has_out_type x = {f . (image f (dom f) ⊆ Some ` {v . tp v = x})}"
  
  definition "has_in_out_type x y = has_in_type x ∩ has_out_type y"
  
  definition "ID_f x v = (if tp v = x then Some v else None)"
  
  lemma [simp]: "(tp x = []) = (x = [])"
    by (case_tac x, simp_all)
      
  lemma map_comp_type: "f ∈ has_in_out_type x y ⟹ g ∈ has_in_out_type y z ⟹ g ∘m f ∈ has_in_out_type x z"
    apply (simp add: has_in_out_type_def has_in_type_def has_out_type_def dom_def map_comp_def image_def, auto)
    apply (case_tac "f xa", simp_all)
    apply force
    apply (simp add: subset_eq)
    apply force
    apply (case_tac "f xa", simp_all)
    by force
    
  definition "TI_f f = (SOME x . (∃ y . f ∈ has_in_out_type x y))"

  definition "TO_f f = (SOME y . (∃ x . f ∈ has_in_out_type x y))"
  
  fun pref :: "Values list ⇒ Types list ⇒ Values list" where
    "pref v [] = []" |
    "pref (a # v) (t # x) = (if tv a = t then a # pref v x else undefined)" |
    "pref v x = undefined"

  fun suff :: "Values list ⇒ Types list ⇒ Values list" where
    "suff v [] = v" |
    "suff (a # v) (t # x) = (if tv a = t then suff v x else undefined)" |
    "suff v x = undefined"
    
  lemma tp_pref_suff: "⋀ x y . tp v = x @ y ⟹ tp (pref v x) = x ∧ tp (suff v x) = y"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)
    
    
  definition "par_f f g v = (if tp v = (TI_f f) @ (TI_f g) then Some (the (f (pref v (TI_f f))) @ (the (g (suff v (TI_f f))))) else None)"
      
  fun some_v:: "Types list ⇒ Values list" where
    "some_v [] = []" |
    "some_v (int # x) = (Inte undefined) # some_v x" |
    "some_v (bool # x) = (Bool undefined) # some_v x" |
    "some_v (nat # x) = (Nat undefined) # some_v x"
    
  lemma [simp]: "tp (some_v x) = x"
    apply (induction x, auto)
    by (case_tac a, auto)
      
  lemma same_in_type: "f ∈ has_in_type x ⟹ f ∈ has_in_type y ⟹ x = y"
    apply (simp add: has_in_type_def set_eq_iff dom_def)
    apply (drule_tac x = "some_v x" in spec, simp)
    by (drule_tac x = "some_v x" in spec, simp)

  lemma same_out_type: "f ∈ has_in_type z ⟹ f ∈ has_out_type x ⟹ f ∈ has_out_type y ⟹ x = y"
    apply (simp add: has_out_type_def has_in_type_def set_eq_iff dom_def subset_eq image_def)
    apply (drule_tac x = "some_v z" in spec, simp, safe)
    apply (drule_tac x = "f (some_v z) " in spec, simp, safe, simp_all)
    apply (drule_tac x = "(some_v z) " in spec, simp)
    apply (drule_tac x = "f (some_v z) " in spec, simp, safe, simp_all)
    by (drule_tac x = "(some_v z) " in spec, simp)

  lemma type_has_type:
    assumes A: "f ∈ has_in_out_type x y"
    shows "TI_f f = x" and "TO_f f = y"
    using A apply (simp add: has_in_out_type_def TI_f_def TO_f_def)
    using same_in_type apply blast
    using A apply (simp add: has_in_out_type_def TI_f_def TO_f_def)
    using same_out_type by blast
    
  lemma has_type_out_type: "f ∈ has_in_out_type x y ⟹ tp v = x ⟹ tp (the (f v)) = y"
    apply (simp add: has_in_out_type_def has_out_type_def has_in_type_def dom_def image_def set_eq_iff subset_eq, safe)
    apply (drule_tac x = v in spec, simp, safe)
    by (drule_tac x = "Some ya" in spec, auto)
    
  lemma tp_append: "tp (v @ u) = tp v @ tp u"
    by (induction v, simp_all)
    
  lemma par_f_type: "f ∈ has_in_out_type x y ⟹ g ∈ has_in_out_type x' y' ⟹ par_f f g ∈ has_in_out_type (x @ x') (y @ y')"
    apply (subst has_in_out_type_def)
    apply (simp add:  has_in_type_def has_out_type_def dom_def par_f_def  image_def, auto)
    apply (simp_all add: type_has_type)
    apply (frule tp_pref_suff, safe)
    by (simp add: tp_append has_type_out_type)
    
  definition "Dup_f x v = (if tp v = x then Some (v @ v) else None)"
  
  lemma Dup_has_in_out_type: "Dup_f x ∈ has_in_out_type x (x @ x)"
    apply (simp add: has_in_out_type_def has_out_type_def has_in_type_def dom_def Dup_f_def image_def subset_eq, safe)
    using tp_append by blast
    
  definition "Sink_f x v = (if tp v = x then Some [] else None)"

  lemma Sink_has_in_out_type: "Sink_f x ∈ has_in_out_type x []"
    by (simp add: has_in_out_type_def has_out_type_def has_in_type_def dom_def Sink_f_def image_def subset_eq, auto)

  definition "Switch_f x y v = (if tp v = x @ y then Some (suff v x @ pref v x) else None)"

  lemma Switch_has_in_out_type: "Switch_f x y ∈ has_in_out_type (x @ y) (y @ x)"
    apply (simp add: has_in_out_type_def has_out_type_def has_in_type_def dom_def Switch_f_def image_def subset_eq, safe)
    apply (rule_tac x = "suff xaa x @ pref xaa x" in exI)
    using tp_append tp_pref_suff by simp
  
  
  primrec fb_t :: "Types ⇒ (Values ⇒ Values) ⇒ Values" where
    "fb_t int f  = Inte (Lfp (λ a . integer (f (Inte a))))" |
    "fb_t bool f = Bool (Lfp (λ a . boolean (f (Bool a))))" |
    "fb_t nat f  = Nat  (Lfp (λ a . natural (f (Nat a))))"

  definition "fb_f f v =  (if tp v = tl (TI_f f) then Some (tl (the (f ((fb_t (hd (TI_f f)) (λ a . hd (the (f (a # v))))) # v)))) else None)"


  thm le_Values_def
  thm le_val.simps


  lemma [simp]: "mono Inte"
    by (simp add: mono_def le_Values_def)

  lemma [simp]: "mono Bool"
    by (simp add: mono_def le_Values_def)

  lemma [simp]: "mono Nat"
    by (simp add: mono_def le_Values_def)

  thm monoE
  thm monoI
  thm mono_aD
  lemma [simp]: "mono A ⟹ mono B ⟹ mono C ⟹ mono_a f⟹ mono_a (λa b. C (f (A a) (B b)))"
    apply (subst mono_a_def, safe)
    apply (rule monoD, simp_all)
    apply (rule_tac f = f in  mono_aD, simp_all)
    apply (rule monoD, simp_all)
    by (rule monoD, simp_all)


  lemma fb_t_commute: "mono_a f ⟹ mono_a g  
    ⟹ fb_t t  (λ b . f (fb_t t' (λ a . (g (fb_t t (f a))) a)) b) = fb_t t (λ b . f (fb_t t' (g b)) b)"
    apply (case_tac t', simp_all)
    apply (case_tac t, simp_all)
    apply (subst Lfp_commute, simp_all)
    apply (subst Lfp_commute, simp_all)
    apply (subst Lfp_commute, simp_all)
    apply (case_tac t, simp_all)
    apply (subst Lfp_commute, simp_all)
    apply (subst Lfp_commute, simp_all)
    apply (subst Lfp_commute, simp_all)
    apply (case_tac t, simp_all)
    apply (subst Lfp_commute, simp_all)
    apply (subst Lfp_commute, simp_all)
    by (subst Lfp_commute, simp_all)


  lemma fb_t_eq_type: "(⋀ a . tv a = t ⟹ f a = g a) ⟹ fb_t t f = fb_t t g"
    by (case_tac t, simp_all)
  

    
  lemma [simp]: "tv (fb_t t f) = t"
     by (case_tac t, simp_all)
      
  lemma has_type_type_in: "f v = Some u ⟹ f ∈ has_in_out_type x y ⟹ tp v = x"
    by (simp add: has_in_out_type_def has_in_type_def, auto)

  lemma has_type_type_in_a: "f v = None ⟹ f ∈ has_in_out_type x y ⟹ tp v ≠ x"
    apply (simp add: has_in_out_type_def has_in_type_def dom_def)
    apply (unfold set_eq_iff, safe)
    by (drule_tac x = v in spec, simp)
    
  lemma has_type_defined: "f ∈ has_in_out_type x y ⟹ tp v = x ⟹ ∃ u . f v = Some u"
    by (simp add: has_in_out_type_def has_in_type_def, auto)
    
  lemma tp_tail: "tp (tl x) = tl (tp x)"
    by (induction x, simp_all)
  
  lemma fb_type: "f ∈ has_in_out_type (t # x) (t # y) ⟹ fb_f f ∈ has_in_out_type x y"
    apply (subst has_in_out_type_def)
    apply (simp add: has_out_type_def has_in_type_def fb_f_def dom_def image_def subset_eq, safe)
    apply (simp_all add: type_has_type)
    apply (frule_tac v = "(fb_t t (λa::Values. hd (the (f (a # xa)))) # xa)" in has_type_out_type)
    by (simp_all add: tp_append tp_tail)
    
  lemma [simp]: "TI_f (Switch_f x y) = x @ y"
    using Switch_has_in_out_type type_has_type(1) by blast

  lemma ID_f_type[simp]: "ID_f ts ∈ has_in_out_type ts ts"
    by (simp add: ID_f_def has_in_out_type_def has_in_type_def has_out_type_def dom_def Image_def subset_eq)

    
  lemma [simp]: "TI_f (ID_f ts) = ts"
    using ID_f_type type_has_type(1) by blast
    
  lemma [simp]: "tp v = ts ⟹ ID_f ts v = Some v"
    by (simp add: ID_f_def)
    
  lemma fb_switch_aux: "f ∈  has_in_out_type (t' # t # ts) ( t' # t # ts') ⟹
      par_f (Switch_f [t'] [t]) (ID_f ts') ∘m (f ∘m par_f (Switch_f [t] [t']) (ID_f ts)) = 
        (λ v . (if tp v = t # t' # ts then case v of a # b # v' ⇒ (case f (b # a # v') of Some (c # d # u) ⇒ Some (d # c # u)) else None))"
    apply (simp add: fun_eq_iff par_f_def Switch_f_def map_comp_def, safe)
    apply (case_tac x, simp_all)
    apply (case_tac list, simp_all)
    apply (cut_tac f = f and v = "aa # a # lista" and x = "t' # t # ts" in has_type_defined, simp_all, safe, simp)
    apply (simp add: fun_eq_iff par_f_def Switch_f_def map_comp_def, safe)
    apply (case_tac u, simp_all)
    apply (case_tac list, simp_all)
    apply (cut_tac v= "aa # a # lista" in has_type_out_type, simp_all)
    apply simp
    apply (case_tac u, simp_all)
    apply (case_tac list, simp_all)
    apply (cut_tac v= "aa # a # lista" in has_type_out_type, simp_all)
    apply simp
    apply (case_tac x, simp_all)
    by (case_tac list, simp_all)

       
  lemma TI_f_fb_f[simp]: "f ∈  has_in_out_type (t # ts) ( t # ts') ⟹ TI_f (fb_f f) = ts"
    using fb_type type_has_type(1) by blast
    
  declare [[show_types=false]]

  lemma fb_t_type: "fb_t t (λa. if tv a = t then f a else g a) = fb_t t f"
    by (case_tac t, simp_all)

  lemma le_values_same_type:  "a ≤ b ⟹ tv a = tv b"
    apply (simp add: le_Values_def)
    apply (case_tac a, simp_all)
    apply (case_tac b, simp_all)
    apply (case_tac b, simp_all)
    by (case_tac b, simp_all)

  thm has_type_out_type

  definition "mono_f = {f . (∀ x y . le_list x y ⟶ le_list (the (f x)) (the (f y)))}"

  lemma [simp]: "le_list v v"
    by (induction v, auto)



  lemma le_pref: "⋀ v x . le_list u v ⟹ le_list (pref u x) (pref v x)"
    apply (induction u)
    apply (case_tac v, simp_all)
    apply (case_tac v, simp_all)
    apply (case_tac x, simp_all, safe)
    using le_values_same_type by auto

  lemma le_suff: "⋀ v x . le_list u v ⟹ le_list (suff u x) (suff v x)"
    apply (induction u)
    apply (case_tac v, simp_all)
    apply (case_tac v, simp_all)
    apply (case_tac x, simp_all, safe)
    using le_values_same_type by auto


  lemma le_list_append: "⋀ y . le_list x y ⟹ le_list x' y' ⟹ le_list (x @ x') (y @ y')"
    apply (induction x, simp_all)
    apply (case_tac y, simp_all)
    by (case_tac y, simp_all)

  thm monoD

  lemma mono_fD: "f ∈ mono_f ⟹ le_list x y ⟹ le_list (the (f x)) (the (f y))"
    by (simp add: mono_f_def)

  lemma le_values_list_same_type: "⋀ (y::Values list) . le_list x y ⟹ tp x = tp y"
    apply (induction x, simp_all)
    apply (case_tac y, simp_all add: le_list_def)
    apply (case_tac y, simp_all, safe)
    by (simp add: le_values_same_type)

  lemma map_comp_mono: "f ∈ mono_f ⟹ g ∈ mono_f ⟹ (⋀ x y . tp x = tp y ⟹ f x = None ⟹ f y = None) ⟹ (⋀ x y . tp x = tp y ⟹ g x = None ⟹ g y = None) ⟹ g ∘m f ∈ mono_f"
    apply (subst mono_f_def, safe)
    apply (simp add: map_comp_def)
    apply (case_tac "f x", simp_all)
    apply (case_tac "f y", simp_all)
    apply (metis le_values_list_same_type option.simps(3))
    apply (case_tac "f y", simp_all)
    apply (metis le_values_list_same_type option.simps(3))
    apply (case_tac "g a", simp_all)
    apply (case_tac "g aa", simp_all)
    apply (metis mono_fD option.sel)
    by (metis (no_types, lifting) mem_Collect_eq mono_f_def option.sel)


  lemma par_mono: "f ∈ mono_f ⟹ g ∈ mono_f ⟹ (⋀ x y . tp x  = tp y ⟹ f x = None ⟹ f y = None) ⟹ (⋀ x y . tp x  = tp y ⟹ g x = None ⟹ g y = None) ⟹ par_f f g ∈ mono_f"
    apply (subst mono_f_def, simp, safe)
    apply (simp add: par_f_def, safe)
    apply (case_tac "f (pref x (TI_f f))", simp_all)
    apply (case_tac "f (pref y (TI_f f))", simp_all)
    apply (case_tac "g (suff x (TI_f f))", simp_all)
    apply (case_tac "g (suff y (TI_f f))", simp_all)
    apply (rule le_list_append, simp_all)
    apply (drule_tac f = g and x = "suff x (TI_f f)" and y = "suff y (TI_f f)" in mono_fD)
    apply (rule le_suff, simp_all)
    apply (case_tac "f (pref y (TI_f f))", simp_all)
    apply (metis (no_types, hide_lams) le_list_append le_pref le_suff mono_fD option.sel)
    apply (metis (no_types, hide_lams) le_list_append le_pref le_suff mono_fD option.sel)

    apply (case_tac "f (pref y (TI_f f))", simp_all)
    apply (metis (no_types, hide_lams) le_list_append le_pref le_suff mono_fD option.sel)

    apply (case_tac "g (suff x (TI_f f))", simp_all)
    apply (case_tac "g (suff y (TI_f f))", simp_all)
    
    apply (rule le_list_append, simp_all)
    apply (drule_tac f = f and x = "pref x (TI_f f)" and y = "pref y (TI_f f)" in mono_fD)
    apply (rule le_pref, simp_all)

    apply (metis (no_types, hide_lams) le_list_append le_pref le_suff mono_fD option.sel)

    apply (case_tac "g (suff y (TI_f f))", simp_all)
    apply (metis (no_types, hide_lams) le_list_append le_pref le_suff mono_fD option.sel)

    apply (rule le_list_append)
    apply (drule_tac f = f and x = "pref x (TI_f f)" and y = "pref y (TI_f f)" in mono_fD)
    apply (rule le_pref, simp_all)
    apply (drule_tac f = g and x = "suff x (TI_f f)" and y = "suff y (TI_f f)" in mono_fD)
    apply (rule le_suff, simp_all)
    by (simp_all add: le_values_list_same_type)

  lemma mono_f_emono: "f ∈ mono_f ⟹ (⋀ x y . tp x  = tp y ⟹ f x = None ⟹ f y = None) ⟹ mono A ⟹ mono B ⟹ emono (λa. A (hd (the (f (B a # x)))))"
    apply (simp add: emono_def, safe)
    apply (rule_tac f = A in monoD, simp_all)
    apply (case_tac "(f (B xa # x))", simp_all)
    apply (case_tac "(f (B y # x))", simp_all)
    apply (metis le_values_same_type mono_def option.simps(3) tp.simps(2))
    apply (case_tac "(f (B y # x))", simp_all)
    apply (metis le_values_same_type mono_def option.simps(3) tp.simps(2))
    apply (drule_tac x = "B xa # x" and y = "B y # x" in mono_fD, simp add: le_Values_def)
    apply (cut_tac f = B in monoD, simp_all add: le_Values_def)
    apply (case_tac a, simp_all)
    apply (case_tac aa, simp_all)
    by (case_tac aa, simp_all)

  lemma mono_fb_t_aux: "f ∈ mono_f ⟹
    le_list x y ⟹ (⋀x y. tp x = tp y ⟹ f x = None ⟹ f y = None) ⟹ mono (A::'a::order ⇒ 'b::fin_cpo) ⟹ mono B
      ⟹ B (Lfp (λa. A (hd (the (f (B a # x)))))) ≤ B (Lfp (λa. A (hd (the (f (B a # y))))))"
    apply (rule_tac f = B in monoD, simp_all)
    apply (rule  Lfp_mono)
    apply (rule mono_f_emono)
    apply simp
    apply blast
    apply simp_all
    apply (rule mono_f_emono)
    apply simp
    apply blast
    apply simp_all
    apply (case_tac "(f (B a # x))", simp_all)
    apply (case_tac "(f (B a # y))", simp_all)
    apply (metis le_values_list_same_type option.simps(3) tp.simps(2))
    apply (case_tac "(f (B a # y))", simp_all)
    apply (metis le_values_list_same_type option.simps(3) tp.simps(2))

    apply (drule_tac x = "(B a # x)" and y = "(B a # y)" in mono_fD, simp_all)
    apply (case_tac aa, simp_all)
    apply (case_tac ab, simp_all)
    apply (case_tac ab, simp_all)
    by (rule_tac f = A in monoD, simp_all)

  thm mono_fb_t_aux [of f x y integer]

  lemma mono_fb_f: "f ∈ mono_f ⟹ le_list x y ⟹ (⋀ x y . tp x  = tp y ⟹ f x = None ⟹ f y = None) 
    ⟹  fb_t (hd (TI_f f)) (λa. hd (the (f (a # x)))) ≤ fb_t (hd (TI_f f)) (λa. hd (the (f (a # y))))"
    by (case_tac "hd (TI_f f)", simp_all add: mono_fb_t_aux)


  lemma fb_mono: "f ∈ mono_f ⟹ (⋀ x y . tp x  = tp y ⟹ f x = None ⟹ f y = None) ⟹ fb_f f ∈ mono_f"
    apply (subst mono_f_def, simp, safe)
    apply (simp add: fb_f_def, safe)
    apply (simp_all add: le_values_list_same_type)
    apply (case_tac "(f (fb_t (hd (TI_f f)) (λa. hd (the (f (a # x)))) # x))", simp_all)
    apply (case_tac "(f (fb_t (hd (TI_f f)) (λa. hd (the (f (a # y)))) # y))", simp_all)
    apply (subgoal_tac "tp (fb_t (hd (TI_f f)) (λa. hd (the (f (a # y)))) # y) = tp (fb_t (hd (TI_f f)) (λa. hd (the (f (a # x)))) # x)")
    apply (metis option.distinct(1))
    apply (simp_all add: le_values_list_same_type)
    apply (case_tac "(f (fb_t (hd (TI_f f)) (λa. hd (the (f (a # y)))) # y))", simp_all)
    apply (subgoal_tac "tp (fb_t (hd (TI_f f)) (λa. hd (the (f (a # y)))) # y) = tp (fb_t (hd (TI_f f)) (λa. hd (the (f (a # x)))) # x)")
    apply (metis option.distinct(1))
    apply (simp_all add: le_values_list_same_type)
    apply (frule_tac x = "fb_t (hd (TI_f f)) (λa::Values. hd (the (f (a # x)))) # x" and y = "fb_t (hd (TI_f f)) (λa::Values. hd (the (f (a # y)))) # y" in mono_fD, simp_all)
    apply (rule mono_fb_f)
    apply simp
    apply simp
    apply blast
    by (metis hd_Cons_tl le_list.elims(2) le_list.simps(2) list.distinct(1) list.sel(2))
    
  lemma mono_f_mono_a[simp]: "f ∈ mono_f ⟹ f ∈  has_in_out_type (t # t' # ts) ts' ⟹ tp v = ts ⟹ mono_a (λa b. hd (the (f (b # a # v))))"
    apply (simp add: mono_a_def, safe)
    apply (case_tac "f (b # a # v)", simp_all)
    apply (case_tac "f (b' # a' # v)", simp_all)
    apply (frule has_type_type_in, simp_all, safe)
    apply (frule has_type_type_in_a, simp_all, safe)
    apply (simp add: le_values_same_type)
    apply (simp add: le_values_same_type)
    apply (case_tac "f (b' # a' # v)", simp_all)
    apply (frule has_type_type_in, simp_all, safe)
    apply (frule has_type_type_in_a, simp_all, safe)
    apply (simp add: le_values_same_type)
    apply (simp add: le_values_same_type)
    apply (case_tac aa, simp_all)
    apply (case_tac ab, simp_all)
    apply (frule_tac v = "b # a # v" in has_type_out_type, simp_all)
    apply (frule has_type_type_in, simp_all, safe)
    apply (frule_tac v = "b' # a' # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "b' # a' # v" and f = f in  has_type_type_in, simp_all, safe)
    apply (case_tac ab, simp_all)
    apply (frule_tac v = "b # a # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "b # a # v" and f = f in  has_type_type_in, simp_all, safe)
    apply (frule_tac v = "b' # a' # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "b' # a' # v" and f = f in  has_type_type_in, simp_all, safe)
    apply (simp add: mono_f_def)
    apply (drule_tac x = "b # a # v" in spec)
    by (drule_tac x = "b' # a' # v" in spec, simp_all add: le_list_def)

  lemma mono_f_mono_a_b[simp]: "f ∈ mono_f ⟹ f ∈  has_in_out_type (t # t' # ts) ts' ⟹ tp v = ts ⟹ mono_a (λa b. hd (tl (the (f (a # b # v)))))"
    apply (simp add: mono_a_def, safe)
    apply (case_tac "f (a # b # v)", simp_all)
    apply (case_tac "f (a' # b' # v)", simp_all)
    apply (frule has_type_type_in, simp_all, safe)
    apply (frule has_type_type_in_a, simp_all, safe)
    apply (simp add: le_values_same_type)
    apply (simp add: le_values_same_type)
    apply (case_tac "f (a' # b' # v)", simp_all)
    apply (frule has_type_type_in, simp_all, safe)
    apply (frule has_type_type_in_a, simp_all, safe)
    apply (simp add: le_values_same_type)
    apply (simp add: le_values_same_type)
    apply (case_tac aa, simp_all)
    apply (case_tac ab, simp_all)
    apply (frule_tac v = "a # b # v" in has_type_out_type, simp_all)
    apply (frule has_type_type_in, simp_all, safe)
    apply (frule_tac v = "a' # b' # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "a' # b' # v" and f = f in  has_type_type_in, simp_all, safe)
    apply (case_tac ab, simp_all)
    apply (frule_tac v = "a # b # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "a # b # v" and f = f in  has_type_type_in, simp_all, safe)
    apply (frule_tac v = "a' # b' # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "a' # b' # v" and f = f in  has_type_type_in, simp_all, safe)

    apply (case_tac list, simp_all)
    apply (case_tac lista, simp_all)

    apply (frule_tac v = "a # b # v" in has_type_out_type, simp_all)
    apply (frule has_type_type_in, simp_all, safe)
    apply (frule_tac v = "a' # b' # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "a' # b' # v" and f = f in  has_type_type_in, simp_all, safe)

    apply (case_tac lista, simp_all)

    apply (frule_tac v = "a # b # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "a # b # v" and f = f in  has_type_type_in, simp_all, safe)
    apply (frule_tac v = "a' # b' # v" in has_type_out_type, simp_all)
    apply (frule_tac v = "a' # b' # v" and f = f in  has_type_type_in, simp_all, safe)


    apply (simp add: mono_f_def)
    apply (drule_tac x = "a # b # v" in spec)
    by (drule_tac x = "a' # b' # v" in spec, simp_all add: le_list_def)

  lemma [simp]: "Switch_f x y ∈ mono_f"
    apply (simp add: Switch_f_def mono_f_def, auto)
    apply (rule le_list_append)
    apply (simp add: le_suff)
    apply (simp add: le_pref)
    by (simp_all add: le_values_list_same_type)

  lemma [simp]: "ID_f x ∈ mono_f"
    apply (simp add: ID_f_def mono_f_def, auto)
    by (simp_all add: le_values_list_same_type)

  lemma has_type_None: "f ∈ has_in_out_type x y ⟹ tp u = tp v ⟹ f u = None ⟹ f v = None"
    by (metis has_type_type_in has_type_type_in_a option.exhaust)

    
  lemma fb_f_commute: "f ∈ mono_f ⟹ f ∈  has_in_out_type (t' # t # ts) ( t' # t # ts') ⟹
      fb_f (fb_f (par_f (Switch_f [t'] [t]) (ID_f ts') ∘m (f ∘m par_f (Switch_f [t] [t']) (ID_f ts)))) = (fb_f (fb_f f))"
    proof -
      assume [simp]: "f ∈ mono_f"
      assume [simp]: "f ∈  has_in_out_type (t' # t # ts) ( t' # t # ts')"
      have TI_f_f[simp]: "TI_f f = t' # t # ts"
        using ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› type_has_type(1) by blast
      
      define g where "g ≡ (λ v . (if tp v = t # t' # ts then case v of a # b # v' ⇒ (case f (b # a # v') of Some (c # d # u) ⇒ Some (d # c # u)) else None))"

      have A[simp]: "(par_f (Switch_f [t'] [t]) (ID_f ts') ∘m (f ∘m par_f (Switch_f [t] [t']) (ID_f ts))) = g"
        by (simp add: g_def fb_switch_aux)

      have [simp]: "g ∈  has_in_out_type (t # t' # ts) ( t # t' # ts')"
        apply (subst A [THEN sym])
        apply (rule_tac y = "t' # t # ts'" in map_comp_type)
        apply (rule_tac y = "t' # t # ts" in map_comp_type, simp_all)
        apply (cut_tac x = "[t,t']" and y = "[t',t]" and x' = ts and y' = ts and f = "Switch_f [t] [t']" and g = "ID_f ts" in par_f_type, simp_all)
        apply (metis (no_types, lifting) Cons_eq_append_conv Switch_has_in_out_type)
        apply (cut_tac x = "[t',t]" and y = "[t,t']" and x' = ts' and y' = ts' and f = "Switch_f [t'] [t]" and g = "ID_f ts'" in par_f_type, simp_all)
        by (metis (no_types, lifting) Cons_eq_append_conv Switch_has_in_out_type)

      have B: "⋀x y. tp x = tp y ⟹ (f ∘m par_f (Switch_f [t] [t']) (ID_f ts)) x = None ⟹ (f ∘m par_f (Switch_f [t] [t']) (ID_f ts)) y = None"
        apply (simp add: map_comp_def)
        apply (case_tac "par_f (Switch_f [t] [t']) (ID_f ts) x", simp_all)
        apply (case_tac "par_f (Switch_f [t] [t']) (ID_f ts) y", simp_all)
        apply (simp add: par_f_def)
        apply (case_tac "tp y = t # t' # ts", simp_all)
        apply (case_tac "par_f (Switch_f [t] [t']) (ID_f ts) y", simp_all)
          proof -
            fix x :: "Values list" and y :: "Values list" and a :: "Values list" and aa :: "Values list"
            assume a1: "f a = None"
            assume a2: "par_f (Switch_f [t] [t']) (ID_f ts) y = Some aa"
            assume a3: "par_f (Switch_f [t] [t']) (ID_f ts) x = Some a"
            assume a4: "tp x = tp y"
            have "f ∈ has_in_type (t' # t # ts) ∩ has_out_type (t' # t # ts')"
              using ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_in_out_type_def by blast
            then have f5: "dom f = {vs. tp vs = t' # t # ts}"
              by (simp add: has_in_type_def)
            then have f6: "tp a ≠ t' # t # ts"
              using a1 by blast
            have f7: "∀f fa vs. if tp vs = TI_f f @ TI_f fa then par_f f fa vs = Some (the (f (pref vs (TI_f f))) @ the (fa (suff vs (TI_f f)))) else par_f f fa vs = None"
              by (simp add: par_f_def)
            then have f8: "tp x = TI_f (Switch_f [t] [t']) @ TI_f (ID_f ts) ∨ Some a = Some aa"
              using a3 by fastforce
            have "∀f ts tsa vs. f ∉ has_in_out_type ts tsa ∨ tp vs ≠ ts ∨ tp (the (f vs)) = tsa"
              using has_type_out_type by satx
            then have f9: "tp (pref x (TI_f (Switch_f [t] [t']))) ≠ [t] @ [t'] ∨ tp (the (Switch_f [t] [t'] (pref x (TI_f (Switch_f [t] [t']))))) = [t'] @ [t]"
              using Switch_has_in_out_type by blast
            { assume "f aa ≠ None"
              { assume "Some a ≠ Some aa ∧ tp a ≠ tp aa"
                moreover
                { assume "Some a ≠ Some aa ∧ tp (the (Switch_f [t] [t'] (pref x (TI_f (Switch_f [t] [t']))))) ≠ tp (the (Switch_f [t] [t'] (pref y (TI_f (Switch_f [t] [t'])))))"
                  then have "tp aa = t' # t # ts ⟶ Some a ≠ Some aa ∧ tp (the (ID_f ts (suff x (TI_f (Switch_f [t] [t']))))) ≠ ts ∨ Some a ≠ Some aa ∧ tp (the (ID_f ts (suff y (TI_f (Switch_f [t] [t']))))) ≠ ts"
                    using f9 f8 f7 a4 a2 tp_append tp_pref_suff by force }
                ultimately have "tp aa ≠ t' # t # ts"
                  using f8 f7 a4 a3 a2 tp_append tp_pref_suff by force }
              then have "tp aa ≠ t' # t # ts"
                using f6 by force
              then have "f aa = None"
                using f5 by blast }
            then show "f aa = None"
              by blast
          qed

        
      have [simp]: "g ∈  mono_f"
        apply (subst A [THEN sym])
        apply (rule map_comp_mono)
        apply (rule map_comp_mono, simp_all)
        apply (rule par_mono, simp_all)
        apply (simp add: Switch_f_def, auto)
        apply (simp add: ID_f_def, auto)
        apply (simp add: par_f_def, auto)
        using ‹(f::Values list ⇒ Values list option) ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_None apply blast
        apply (rule par_mono, simp_all)
        apply (simp add: Switch_f_def, auto)
        apply (simp add: ID_f_def, auto)
        apply (rule B, simp_all)
        by (simp add: par_f_def, auto)
        
      have [simp]: "TI_f g = t # t' # ts"
        using ‹g ∈ has_in_out_type (t # t' # ts) (t # t' # ts')› type_has_type(1) by blast

      define fbt where "fbt ≡ (λ v . fb_t t' (λa . hd (the (f (a # v)))))"
      have fbt_simp: "⋀ v . fbt v = fb_t t' (λa . hd (the (f (a # v))))"
        by (simp add: fbt_def)

      have C: "⋀ v . tp v = t # ts ⟹ fb_f f v = Some (tl (the (f (fbt v # v))))"
        by (simp add: fb_f_def fun_eq_iff fbt_simp [THEN sym])

      have "⋀ v . tp v ≠ t # ts ⟹ fb_f f v = None"
        by (simp add: fb_f_def)

      have fb_f_f: "fb_f f = (λ v . (if tp v = t # ts then Some (tl (the (f (fbt v # v)))) else None))"
        apply (simp add: fun_eq_iff C)
        by (simp add: fb_f_def)
        
(****)
      define fbg where "fbg ≡ (λ v . fb_t t (λa . hd (the (g (a # v)))))"
      have fbg_simp: "⋀ v . fbg v = fb_t t (λa . hd (the (g (a # v))))"
        by (simp add: fbg_def)

      have D: "⋀ v . tp v = t' # ts ⟹ fb_f g v = Some (tl (the (g (fbg v # v))))"
        by (simp add: fb_f_def fun_eq_iff fbg_simp [THEN sym])

      have "⋀ v . tp v ≠ t' # ts ⟹ fb_f g v = None"
        by (simp add: fb_f_def fun_eq_iff)

      have fb_f_g: "fb_f g = (λ v . (if tp v = t' # ts then Some (tl (the (g (fbg v # v)))) else None))"
        apply (simp add: fun_eq_iff D)
        by (simp add: fb_f_def)

(****)
        
      define f' where "f' ≡ fb_f f"
      
      have [simp]: "TI_f f' = t # ts"
        using ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› f'_def fb_type type_has_type(1) by blast

      define fbt' where "fbt' ≡ (λ v . fb_t t (λa . hd (the (f' (a # v)))))"
      have fbt'_simp: "⋀ v . fbt' v = fb_t t (λa . hd (the (f' (a # v))))"
        by (simp add: fbt'_def)
      
      have A: "⋀ v . tp v = ts ⟹ fb_f f' v = Some (tl (the (f' (fbt' v # v))))"
        by (simp add: fb_f_def fun_eq_iff fbt'_simp [THEN sym])

      have [simp]: "⋀ v . tp v ≠ ts ⟹ fb_f f' v = None"
        by (simp add: fb_f_def fun_eq_iff fbt'_simp [THEN sym])
        
      define g' where "g' ≡ fb_f g"
      
      have [simp]: "TI_f g' = t' # ts"
        using ‹g ∈ has_in_out_type (t # t' # ts) (t # t' # ts')› fb_type g'_def type_has_type(1) by blast

      define fbg' where "fbg' ≡ (λ v . fb_t t' (λa . hd (the (g' (a # v)))))"
      have fbg'_simp: "⋀ v . fbg' v = fb_t t' (λa . hd (the (g' (a # v))))"
        by (simp add: fbg'_def)
      
      have B: "⋀ v . tp v = ts ⟹ fb_f g' v = Some (tl (the (g' (fbg' v # v))))"
        by (simp add: fb_f_def fun_eq_iff fbg'_simp [THEN sym])

      have [simp]: "⋀ v . tp v ≠ ts ⟹ fb_f g' v = None"
        by (simp add: fb_f_def fun_eq_iff)

      have [simp]: "⋀ v . tp v = ts ⟹ tv (fbt' v) = t"  
        by (simp add: fbt'_def)
        
      have [simp]: "⋀ v. tp v = ts ⟹ tv (fbg' v) = t'"
        by (simp add: fbg'_def)
        
      have E: "⋀ a b v . tp v = ts ⟹ tv a = t ⟹ tv b = t' ⟹ tl (tl (the (g (a # b # v)))) = tl (tl (the (f (b # a # v))))"
        apply (simp add: g_def, auto)
        apply (cut_tac f = f and v = "b # a # v" and y = "t' # t # ts'" in has_type_defined, simp_all)
        apply auto
        using ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› apply blast
        by (metis (mono_tags, lifting) ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_out_type list.case_eq_if list.sel(3) list.simps(3) option.sel tp.simps(1) tp.simps(2) tp_tail)

      have AA: "⋀ f b u v . f (if b then u else v) = (if b then f u else f v)"
        by (simp add: fun_eq_iff)

      have g_hd_tl: "⋀ a b v . tv a = t' ⟹ tv b = t ⟹ tp v = ts ⟹ hd (tl (the (g (b # a # v)))) = hd (the (f (a # b # v)))"
        apply (case_tac "f (a # b # v)", simp_all)
        apply (metis ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_defined option.simps(3) tp.simps(2))
        apply (case_tac aa, simp_all)
        apply (metis ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_out_type list.simps(3) option.sel tp.simps(1) tp.simps(2))
        apply (case_tac list, simp_all)
        apply (metis (mono_tags, lifting) ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_out_type list.distinct(1) list.sel(3) option.sel tp.simps(1) tp.simps(2))
        by (simp add: g_def)

      have g_hd: "⋀ a b v . tv a = t' ⟹ tv b = t ⟹ tp v = ts ⟹ hd ((the (g (b # a # v)))) = hd ( tl (the (f (a # b # v))))"
        apply (case_tac "f (a # b # v)", simp_all)
        apply (metis ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_defined option.simps(3) tp.simps(2))
        apply (case_tac aa, simp_all)
        apply (metis ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_out_type list.simps(3) option.sel tp.simps(1) tp.simps(2))
        apply (case_tac list, simp_all)
        apply (metis (mono_tags, lifting) ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› has_type_out_type list.distinct(1) list.sel(3) option.sel tp.simps(1) tp.simps(2))
        by (simp add: g_def)

      have [simp]: "⋀ v . tp v = ts ⟹ mono_a (λa b. hd (the (f (b # a # v))))"
        using ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› ‹f ∈ mono_f› mono_f_mono_a by blast

      have [simp]: "⋀ v . tp v = ts ⟹ mono_a (λa b. hd (tl (the (f (a # b # v)))))"
        using ‹f ∈ has_in_out_type (t' # t # ts) (t' # t # ts')› ‹f ∈ mono_f› mono_f_mono_a_b by blast
        

      have [simp]: "⋀ v . tp v = ts ⟹ mono_a (λa b. hd (the (g (b # a # v))))"
        using ‹g ∈ has_in_out_type (t # t' # ts) (t # t' # ts')› ‹g ∈ mono_f› mono_f_mono_a by blast

      have [simp]: "⋀ v . tp v = ts ⟹ mono_a (λa b. hd (tl (the (g (a # b # v)))))"
        using ‹g ∈ has_in_out_type (t # t' # ts) (t # t' # ts')› ‹g ∈ mono_f› mono_f_mono_a_b by blast
        
      have [simp]: "⋀v . tp v = ts ⟹ fbt (fbt' v # v) = fbg' v"
        apply (simp add: fbg'_def g'_def fbt_def fbt'_def f'_def)
        apply (simp add: fb_f_f fb_f_g)
        apply (subst fbt_def)
        apply (subst fbg_def)
        apply (simp add: AA fb_t_type)
        apply (subst fb_t_commute)
        apply (simp_all)
        apply (rule fb_t_eq_type)
        apply (simp add: g_hd_tl)
        apply (subgoal_tac "fb_t t (λb. hd (tl (the (f (a # b # v))))) = fb_t t (λaa. hd (the (g (aa # a # v))))", simp_all)
        apply (rule fb_t_eq_type)
        by (simp add: g_hd)
        
      have [simp]: "⋀ v . tp v = ts ⟹ fbg (fbg' v # v) = fbt' v"
        apply (simp add: fbg'_def g'_def fbt_def fbt'_def f'_def)
        apply (simp add: fb_f_f fb_f_g)
        apply (subst fbt_def)
        apply (subst fbg_def)
        apply (subst fbg_def)
        apply (simp add: AA fb_t_type)
        apply (subst fb_t_commute)
        apply simp_all
        apply (rule fb_t_eq_type)
        apply (simp add: g_hd)
        apply (subgoal_tac "(fb_t t' (λb. hd (tl (the (g (a # b # v)))))) = (fb_t t' (λaa. hd (the (f (aa # a # v)))))")
        apply simp_all
        apply (rule fb_t_eq_type)
        by (simp add: g_hd_tl)
      
      have F: "⋀ v . tp v = ts ⟹ fb_f (fb_f g) v = fb_f (fb_f f) v"
        apply (simp add: f'_def [THEN symmetric] A g'_def [THEN symmetric] B)
        apply (simp add: g'_def f'_def C D)
        by (subst E, simp_all)
        

      have "⋀ v . tp v ≠ ts ⟹ fb_f (fb_f g) v = fb_f (fb_f f) v"
        by (simp add: f'_def [THEN symmetric] g'_def [THEN symmetric])
        
      from F and this show ?thesis
        by (case_tac "tp v = ts", auto)
    qed
 
  definition "typed_func = (⋃ x . (⋃ y . has_in_out_type x y)) ∩ mono_f"

  typedef func = "typed_func"
    apply (simp add: typed_func_def)
    apply (rule_tac x = "ID_f []" in exI, simp)
    apply (rule_tac x = "[]" in exI)
    apply (rule_tac x = "[]" in exI)
    by simp
    
        
  definition "fb_func f = Abs_func (fb_f (Rep_func f))"

  definition "TI_func f = (TI_f (Rep_func f))"
  definition "TO_func f = (TO_f (Rep_func f))"
  definition "ID_func t = Abs_func (ID_f t)"
  
  definition "comp_func f g = Abs_func ((Rep_func g) ∘m (Rep_func f))"

  definition "parallel_func f g = Abs_func (par_f (Rep_func f) (Rep_func g))"

  definition "Dup_func x = Abs_func (Dup_f x)"

  definition "Sink_func x = Abs_func (Sink_f x)"
  definition "Switch_func x y = Abs_func (Switch_f x y)"
  
  lemma [simp]: "ID_f t ∈ typed_func"
    apply (simp add: typed_func_def)
    using ID_f_type by blast

    
  lemma map_comp_typed_func[simp]: "f ∈ typed_func ⟹ g ∈ typed_func ⟹ TI_f g = TO_f f ⟹ (g ∘m f) ∈ typed_func"
    apply (simp add: typed_func_def, safe)
    using map_comp_type type_has_type(1) type_has_type(2) apply fastforce
    by (simp add: has_type_None map_comp_mono)

  lemma par_typed_func[simp]: "f ∈ typed_func ⟹ g ∈ typed_func ⟹ par_f f g ∈ typed_func"
    apply (simp add: typed_func_def, safe)
    using par_f_type type_has_type(1) type_has_type(2) apply fastforce
    by (simp add: has_type_None par_mono)

  lemma fb_typed_func[simp]: "f ∈ typed_func ⟹ TI_f f = t # x ⟹ TO_f f = t # y ⟹ fb_f f ∈ typed_func"
    apply (simp add: typed_func_def, safe)
    using fb_type type_has_type(1) type_has_type(2) apply fastforce
    by (simp add: has_type_None fb_mono)

  lemma [simp]: "Switch_f x y ∈ typed_func"
    apply (simp add: typed_func_def)
    using Switch_has_in_out_type by auto
    
  lemma [simp]: "Dup_f x ∈ mono_f"
    apply (simp add: Dup_f_def mono_f_def, safe)
    apply (simp add: le_list_append)
    using le_values_list_same_type by auto

  lemma [simp]: "Dup_f x ∈ typed_func"
    apply (simp add: typed_func_def)
    using Dup_has_in_out_type by auto

  lemma [simp]: "Sink_f x ∈ mono_f"
    apply (simp add: Sink_f_def mono_f_def, safe)
    using le_values_list_same_type by auto

  lemma [simp]: "Sink_f x ∈ typed_func"
    apply (simp add: typed_func_def)
    using Sink_has_in_out_type by auto

  thm Rep_func
  thm Abs_func_inverse
  thm Rep_func_inverse
  
  lemma map_comp_assoc: "(f ∘m g) ∘m h = f ∘m (g ∘m h)"
    apply (simp add: map_comp_def fun_eq_iff, safe)
    by (case_tac "h x", simp_all)

  lemma map_comp_id: "f ∈ has_in_out_type x y ⟹ (f ∘m ID_f x) = f"
    apply (simp add: fun_eq_iff map_comp_def ID_f_def)
    by (metis has_type_type_in not_Some_eq)

  lemma id_map_comp: "f ∈ has_in_out_type x y ⟹ (ID_f y ∘m f) = f"
    apply (simp add: fun_eq_iff map_comp_def ID_f_def, safe)
    apply (case_tac "f xa", simp_all)
    by (metis (mono_tags, lifting) ID_f_def has_type_out_type has_type_type_in option.sel)


  lemma [simp]: "⋀ x x' . tp v = x @ x' @ x'' ⟹ pref (pref v (x @ x')) x = pref v x"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)

  lemma [simp]: "⋀ x x' . tp v = x @ x' @ x'' ⟹ suff (pref v (x @ x')) x = pref (suff v x) x'"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)

  lemma [simp]: "⋀ x x' . tp v = x @ x' @ x'' ⟹suff (suff v x) x' = suff v (x @ x')"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)

  lemma par_f_assoc: "f ∈ has_in_out_type x y ⟹ g ∈ has_in_out_type x' y' ⟹ h ∈ has_in_out_type x'' y'' ⟹
    par_f (par_f f g) h = par_f f (par_f g h)"
    proof -
      assume A: "f ∈ has_in_out_type x y"
      assume B: "g ∈ has_in_out_type x' y'"
      assume C: "h ∈ has_in_out_type x'' y''"
      have [simp]: "TI_f f = x"
        using A type_has_type(1) by auto
      have [simp]: "TI_f g = x'"
        using B type_has_type(1) by auto
      have [simp]: "TI_f h = x''"
        using C type_has_type(1) by auto

      have "par_f f g ∈  has_in_out_type (x @ x') (y @ y')"
        using  A B by (simp add: par_f_type)
      from this have [simp]: "TI_f (par_f f g) = x @ x'"
        using type_has_type(1) by auto


      have "par_f g h ∈  has_in_out_type (x' @ x'') (y' @ y'')"
        using  B C by (simp add: par_f_type)
      from this have [simp]: "TI_f (par_f g h) = x' @ x''"
        using type_has_type(1) by auto

      show ?thesis
        apply (simp add: fun_eq_iff par_f_def type_has_type par_f_type, safe)
        by (simp_all add: tp_pref_suff)
    qed

   lemma "f ∈ has_in_out_type x y ⟹ par_f (ID_f []) f = f"
    proof -
      assume A [simp]: "f ∈ has_in_out_type x y"
    show ?thesis
      apply (simp add: fun_eq_iff par_f_def ID_f_def, safe)      
      apply (metis A has_type_type_in_a option.collapse type_has_type(1))
      by (metis ID_f_def A map_comp_id map_comp_simps(1) type_has_type(1))
    qed

   lemma id_par_f: "f ∈ has_in_out_type x y ⟹ par_f (ID_f []) f = f"
    proof -
      assume A [simp]: "f ∈ has_in_out_type x y"
    show ?thesis
      apply (simp add: fun_eq_iff par_f_def ID_f_def, safe)      
      apply (metis A has_type_type_in_a option.collapse type_has_type(1))
      by (metis ID_f_def A map_comp_id map_comp_simps(1) type_has_type(1))
    qed

   lemma [simp]: "⋀ x . tp v = x ⟹ pref v x = v"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)

   lemma [simp]: "⋀ x . tp v = x ⟹ suff v x = []"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)

   lemma par_f_id: "f ∈ has_in_out_type x y ⟹ par_f f (ID_f []) = f"
    proof -
      assume A [simp]: "f ∈ has_in_out_type x y"
    show ?thesis
      apply (simp add: fun_eq_iff par_f_def ID_f_def, safe)      
      apply (metis A has_type_type_in_a option.collapse type_has_type(1))
      by (metis A ID_f_def map_comp_id map_comp_simps(1) type_has_type(1))
    qed
  lemma [simp]: "⋀ x . tp v = x @ y ⟹ pref v x @ suff v x = v"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)
    
  lemma [simp]: "⋀ x . tp v = x @ x' ⟹ tp (pref v x) = x"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)

  lemma [simp]: "⋀ x . tp v = x @ x' ⟹ tp (suff v x) = x'"
    apply (induction v, simp_all)
    by (case_tac x, simp_all)
    
  lemma [simp]: "⋀ x . tp u = x ⟹ pref (u @ v) x = u"
    apply (induction u, simp_all)
    by (case_tac x, simp_all)


  lemma [simp]: "⋀ x . tp u = x ⟹ suff (u @ v) x = v"
    apply (induction u, simp_all)
    by (case_tac x, simp_all)
    
  lemma par_comp_distrib: "f ∈ has_in_out_type x y ⟹ g ∈ has_in_out_type y z ⟹ 
    f' ∈ has_in_out_type x' y' ⟹ g' ∈ has_in_out_type y' z' ⟹ 
    par_f g g' ∘m par_f f f' = (par_f (g ∘m f) (g' ∘m f'))"
    proof -
      assume A: "f ∈ has_in_out_type x y"
      assume B: "f' ∈ has_in_out_type x' y'"
      assume C: "g ∈ has_in_out_type y z"
      assume D: "g' ∈ has_in_out_type y' z'"
      have [simp]: "TI_f f = x"
        using A type_has_type(1) by auto
      have [simp]: "TI_f g = y"
        using C type_has_type(1) by auto
      have [simp]: "TI_f f' = x'"
        using B type_has_type(1) by auto
      have [simp]: "TI_f g' = y'"
        using D type_has_type(1) by auto
          
      have [simp]: "TI_f (g ∘m f) = x"
        using A C map_comp_type type_has_type(1) by blast

      have [simp]: "TI_f (g' ∘m f') = x'"
        using B D map_comp_type type_has_type(1) by blast
        
      have Aa: "⋀ v . tp v = x @ x' ⟹ ∃ u . f (pref v x) = Some u ∧ tp u = y"
         apply (cut_tac A, cut_tac f = f and v = "pref v x" in has_type_defined)
         apply (simp_all)
         by (metis has_type_out_type has_type_type_in option.sel)
         
         
      have Ab: "⋀ v . tp v = x @ x' ⟹ ∃ u . f' (suff v x) = Some u ∧ tp u = y'"
         apply (cut_tac B, cut_tac f = f' and v = "suff v x" in has_type_defined)
         apply (simp_all)
         by (metis has_type_out_type has_type_type_in option.sel)
        
      show ?thesis
        apply (simp add: fun_eq_iff par_f_def, safe)
        apply (frule Aa, safe, simp)
        apply (frule Ab, safe, simp)
        apply (frule Aa, safe, simp)
        apply (frule Ab, safe, simp)
        by (simp add: tp_append)
     qed
     
  lemma TI_f_par: "f ∈ typed_func ⟹ g ∈ typed_func ⟹ TI_f (par_f f g) = TI_f f  @ TI_f g"
    apply (simp add: typed_func_def, safe)
    apply (frule_tac f = f and g = g in par_f_type, simp_all)
    using type_has_type(1) by auto

  lemma TO_f_par: "f ∈ typed_func ⟹ g ∈ typed_func ⟹ TO_f (par_f f g) = TO_f f  @ TO_f g"
    apply (simp add: typed_func_def, safe)
    apply (frule_tac f = f and g = g in par_f_type, simp_all)
    using type_has_type(2) by auto

  lemma TI_f_map_comp[simp]: "f ∈ typed_func ⟹ g ∈ typed_func ⟹ TO_f g = TI_f f ⟹ TI_f (f ∘m g) = TI_f g"
    apply (simp add: typed_func_def, safe)
    apply (frule_tac f = g and g = f and z = xa in map_comp_type)
    apply (simp add: type_has_type(1) type_has_type(2))
    by (simp add: type_has_type(1))

  lemma TO_f_map_comp[simp]: "f ∈ typed_func ⟹ g ∈ typed_func ⟹ TO_f g = TI_f f ⟹ TO_f (f ∘m g) = TO_f f"
    apply (simp add: typed_func_def, safe)
    apply (frule_tac f = g and g = f and z = xa in map_comp_type)
    apply (simp add: type_has_type(1) type_has_type(2))
    by (simp add: type_has_type(2))

  lemma [simp]: "TI_f (Sink_f ts) = ts"
    using Sink_has_in_out_type type_has_type(1) by blast

  lemma [simp]: "TO_f (Sink_f ts) = []"
    using Sink_has_in_out_type type_has_type(2) by blast

  lemma suff_append: "⋀ t . tp x = t ⟹ suff (x @ y) t = y"
    apply (induction x, simp_all)
    by (case_tac t, simp_all)

  lemma [simp]: "TI_f (Dup_f x) = x"
    using Dup_has_in_out_type type_has_type(1) by blast


  lemma [simp]: "TO_f (Dup_f x) = (x @ x)"
    using Dup_has_in_out_type type_has_type(2) by blast
        
  lemma [simp]: "pref (x @ y) (tp x) = x"
    by (induction x, simp_all)

  lemma [simp]: "TO_f (Switch_f x y) = (y @ x)"
    using Switch_has_in_out_type type_has_type(2) by blast

  lemma [simp]: "TO_f (ID_f x) = x"
    using ID_f_type type_has_type(2) by blast

  declare TO_f_par [simp]

  declare TI_f_par [simp]

  lemma [simp]: "⋀ ts .  tp x = ts @ ts' @ ts'' ⟹ pref (suff x ts) ts' @ suff x (ts @ ts') = suff x ts"
    apply (induction x, simp_all)
    by (case_tac ts, simp_all)


  lemma [simp]: "⋀ts . tp x = ts ⟹  suff (x @ y) (ts @ ts') = suff y ts'"
    apply (induction x, simp_all)
    by (case_tac ts, simp_all)

  lemma AAA: "S x ≠ None ⟹ tv a = t ⟹ tp x = TI_f S ⟹ the ((par_f (ID_f [t]) S) (a # x)) = a # the (S x) "
    by (simp add: par_f_def)

  lemma AAAb: "S x ≠ None ⟹ tv a = t ⟹ tp x = TI_f S ⟹ ((par_f (ID_f [t]) S) (a # x)) = Some (a # the (S x))"
    by (simp add: par_f_def)

  lemma pref_suff_append: "⋀ ts . tp x = ts @ ts' ⟹ pref x ts @ suff x ts = x"
    apply (induction x)
    by auto

  lemma [simp]: "Lfp (λ b. a) = a"
    apply (rule lfp_exists)
    by (simp add: is_lfp_def)


  lemma [simp]: "fb_t (tv a) (λ b . a) = a"
    apply (case_tac "tv a", simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac a, simp_all)
    by (case_tac a, simp_all)

  interpretation func: BaseOperation TI_func TO_func ID_func comp_func parallel_func Dup_func Sink_func Switch_func fb_func
    proof
      fix ts show "TI_func (ID_func ts) = ts"
        by (simp add: TI_func_def ID_func_def Abs_func_inverse)
      fix ts show "TO_func (ID_func ts) = ts"
        by (simp add: TO_func_def ID_func_def Abs_func_inverse)
      fix S S' show " TI_func S' = TO_func S ⟹ TI_func (comp_func S S') = TI_func S"
        by (simp add: TI_func_def comp_func_def TO_func_def Rep_func Abs_func_inverse)
        
      fix S S' show " TI_func S' = TO_func S ⟹ TO_func (comp_func S S') = TO_func S'"
        by (simp add: TI_func_def comp_func_def TO_func_def Rep_func Abs_func_inverse)
        
      fix S show "comp_func (ID_func (TI_func S)) S = S"
        apply (simp add: TI_func_def comp_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)
        apply (cut_tac x = S in Rep_func)
        apply (simp add: typed_func_def, safe)
        by (simp add: Rep_func_inverse map_comp_id type_has_type(1))

      fix S show "comp_func S (ID_func (TO_func S)) = S"
        apply (simp add: TI_func_def comp_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)
        apply (cut_tac x = S in Rep_func)
        apply (simp add: typed_func_def, safe)
        by (simp add: Rep_func_inverse id_map_comp type_has_type(2))

      fix T S R show "TI_func T = TO_func S ⟹ TI_func R = TO_func T ⟹ comp_func (comp_func S T) R = comp_func S (comp_func T R)"
        by (simp add: comp_func_def Rep_func Abs_func_inverse TI_func_def TO_func_def map_comp_assoc)

      fix S T show "TI_func (parallel_func S T) = TI_func S @ TI_func T"
        by (simp add: TI_func_def parallel_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)

      fix S T show "TO_func (parallel_func S T) = TO_func S @ TO_func T"
        by (simp add: TI_func_def parallel_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)

      fix A B C show "parallel_func (parallel_func A B) C = parallel_func A (parallel_func B C)"
        apply (simp add: TI_func_def parallel_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)
        apply (cut_tac x = A in Rep_func)
        apply (cut_tac x = B in Rep_func)
        apply (cut_tac x = C in Rep_func)
        apply (simp add: typed_func_def, safe)
        by (subst par_f_assoc, simp_all)

      fix S show "parallel_func (ID_func []) S = S"
        apply (simp add: TI_func_def parallel_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)
        apply (cut_tac x = S in Rep_func)
        apply (simp add: typed_func_def, safe)
        by (subst id_par_f, simp_all add: Rep_func_inverse)
        
      fix S show " parallel_func S (ID_func []) = S"
        apply (simp add: TI_func_def parallel_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)
        apply (cut_tac x = S in Rep_func)
        apply (simp add: typed_func_def, safe)
        by (subst par_f_id, simp_all add: Rep_func_inverse)

      fix ts ts' show  "parallel_func (ID_func ts) (ID_func ts') = ID_func (ts @ ts')"
        apply (simp add: TI_func_def parallel_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)
        apply (rule_tac f = Abs_func in arg_cong)
        by (simp add: par_f_def fun_eq_iff ID_f_def)

      fix S S' T T' show "TO_func S = TI_func S' ⟹
        TO_func T = TI_func T' ⟹ comp_func (parallel_func S T) (parallel_func S' T') = parallel_func (comp_func S S') (comp_func T T')"
        apply (simp add: TI_func_def parallel_func_def comp_func_def TO_func_def Rep_func Abs_func_inverse ID_func_def)
        apply (cut_tac x = S in Rep_func)
        apply (cut_tac x = S' in Rep_func)
        apply (cut_tac x = T in Rep_func)
        apply (cut_tac x = T' in Rep_func)
        apply (simp add: typed_func_def type_has_type, safe)
        apply (unfold type_has_type)
        by (subst par_comp_distrib , simp_all)
        
      fix ts show "TI_func (Dup_func ts) = ts"
        by (simp add: TI_func_def Dup_func_def Abs_func_inverse)

      fix ts show "TO_func (Dup_func ts) = ts @ ts"
        by (simp add: TO_func_def Dup_func_def Abs_func_inverse)

      fix ts show "TI_func (Sink_func ts) = ts" and "TO_func (Sink_func ts) = []"
        by (simp_all add: TO_func_def TI_func_def Sink_func_def Abs_func_inverse)
        
      fix ts ts' show "TI_func (Switch_func ts ts') = ts @ ts'" and "TO_func (Switch_func ts ts') = ts' @ ts"
        by (simp_all add: TO_func_def TI_func_def Switch_func_def Abs_func_inverse)
        
      fix ts show "comp_func (Dup_func ts) (parallel_func (Sink_func ts) (ID_func ts)) = ID_func ts"
        apply (simp add: comp_func_def Dup_func_def parallel_func_def ID_func_def Abs_func_inverse Rep_func Sink_func_def)
        apply (rule_tac f = Abs_func in arg_cong)
        apply (simp add: fun_eq_iff map_comp_def, safe)
        apply (case_tac "Dup_f ts x", simp_all)
        apply (simp add: Dup_f_def ID_f_def)
        apply auto [1]
        apply (simp add: par_f_def, safe)
        apply (simp add: Dup_f_def Sink_f_def)
        apply (case_tac " tp x = ts", simp_all)
        using suff_append apply blast
        using Dup_f_def ID_f_def tp_append by auto

      fix ts show "comp_func (Dup_func ts) (Switch_func ts ts) = Dup_func ts"
        apply (simp add: comp_func_def Dup_func_def  Abs_func_inverse Rep_func Switch_func_def)
        apply (rule_tac f = Abs_func in arg_cong)
        by (simp add: fun_eq_iff map_comp_def Dup_f_def Switch_f_def tp_append)

      fix ts show "comp_func (Dup_func ts) (parallel_func (ID_func ts) (Dup_func ts)) 
        = comp_func (Dup_func ts) (parallel_func (Dup_func ts) (ID_func ts))"
        apply (simp add: comp_func_def Dup_func_def parallel_func_def ID_func_def Abs_func_inverse Rep_func)
        apply (rule_tac f = Abs_func in arg_cong)
        by (simp add: fun_eq_iff map_comp_def Dup_f_def par_f_def)

      fix S t' t ts ts' have "TI_func S = t' # t # ts ⟹
        TO_func S = t' # t # ts' ⟹
        (fb_func ^^ (Suc (Suc 0)))
         (comp_func (comp_func (parallel_func (Switch_func [t] [t']) (ID_func ts)) S) (parallel_func (Switch_func [t'] [t]) (ID_func ts'))) =
        (fb_func ^^ (Suc (Suc 0))) S"
        
        apply (simp add: TO_func_def TI_func_def fb_func_def comp_func_def parallel_func_def Rep_func Abs_func_inverse Switch_func_def ID_func_def)
        apply (cut_tac x = S in Rep_func)
        apply (simp add: typed_func_def, safe)
        apply (subst fb_f_commute, simp_all)
        by (simp add: type_has_type(1) type_has_type(2))
        
     from this show "TI_func S = t' # t # ts ⟹
        TO_func S = t' # t # ts' ⟹
        (fb_func ^^ 2)
         (comp_func (comp_func (parallel_func (Switch_func [t] [t']) (ID_func ts)) S) (parallel_func (Switch_func [t'] [t]) (ID_func ts'))) =
        (fb_func ^^ 2) S"
        by (simp add: numeral_2_eq_2)

     fix ts'' show "Switch_func ts (ts' @ ts'') = comp_func (parallel_func (Switch_func ts ts') (ID_func ts'')) (parallel_func (ID_func ts') (Switch_func ts ts''))"
       apply (simp add: Switch_func_def comp_func_def parallel_func_def ID_func_def Abs_func_inverse)
       apply (rule_tac f = Abs_func in arg_cong)
       by (simp add: fun_eq_iff Switch_f_def par_f_def tp_append)

     show "parallel_func (Sink_func ts) (Sink_func ts') = Sink_func (ts @ ts')"
       apply (simp add: Sink_func_def parallel_func_def Abs_func_inverse)
       apply (rule_tac f = Abs_func in arg_cong)
       by (simp add: fun_eq_iff Sink_f_def par_f_def)

    show "Dup_func (ts @ ts') = comp_func (parallel_func (Dup_func ts) (Dup_func ts')) (parallel_func (parallel_func (ID_func ts) (Switch_func ts ts')) (ID_func ts'))"
       apply (simp add: Switch_func_def comp_func_def parallel_func_def ID_func_def Dup_func_def Abs_func_inverse)
       apply (rule_tac f = Abs_func in arg_cong)
       by (simp add: fun_eq_iff Switch_f_def par_f_def Dup_f_def tp_append)       
      
       thm has_type_defined
       
    have [simp]: "⋀ B . Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))"
      by (metis (no_types, lifting) Int_iff Rep_func mem_simps(8) type_has_type(1) type_has_type(2) typed_func_def)
       
    fix ti to ti' to' show "TI_func A = ti ⟹ TO_func A = to ⟹ TI_func B = ti' ⟹ TO_func B = to' 
      ⟹ comp_func (comp_func (Switch_func ti ti') (parallel_func B A)) (Switch_func to' to) = parallel_func A B"
       apply (simp add: Switch_func_def comp_func_def parallel_func_def ID_func_def Dup_func_def TI_func_def TO_func_def Rep_func Abs_func_inverse)
       apply (rule_tac f = Abs_func in arg_cong)
       apply (simp add: fun_eq_iff Switch_f_def par_f_def map_comp_def tp_append, auto)
       apply (cut_tac f = "Rep_func B" and x = ti' and y = to' and v = "suff x (TI_f (Rep_func A))" in has_type_defined, simp_all)
       apply (safe, simp_all)
       apply (cut_tac f = "Rep_func A" and x = ti and y = to and v = "pref x (TI_f (Rep_func A))" in has_type_defined, simp_all)
       apply (safe, simp_all)
       apply (cut_tac f = "Rep_func B" and x = ti' and y = to' and v = "suff x (TI_f (Rep_func A))" in has_type_out_type, simp_all)
       apply (cut_tac f = "Rep_func A" and x = ti and y = to and v = "pref x (TI_f (Rep_func A))" in has_type_out_type, simp_all)
       by (cut_tac f = "Rep_func B" and x = ti' and y = to' and v = "suff x (TI_f (Rep_func A))" in has_type_out_type, simp_all)
       
    show "TI_func S = t # ts ⟹ TO_func S = t # ts' ⟹ TI_func (fb_func S) = ts"
      apply (simp add: TI_func_def fb_func_def TO_func_def Abs_func_inverse Rep_func)
      by (metis ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› fb_type type_has_type(1))

    show "TI_func S = t # ts ⟹ TO_func S = t # ts' ⟹ TO_func (fb_func S) = ts'"
      apply (simp add: TI_func_def fb_func_def TO_func_def Abs_func_inverse Rep_func)
      by (metis ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› fb_type type_has_type(2))
      
    show "TI_func S = t # TO_func A ⟹
               TO_func S = t # TI_func B ⟹
               fb_func (comp_func (comp_func (parallel_func (ID_func [t]) A) S) (parallel_func (ID_func [t]) B)) = comp_func (comp_func A (fb_func S)) B"
      
      apply (simp add: TI_func_def fb_func_def TO_func_def Abs_func_inverse Rep_func parallel_func_def ID_func_def comp_func_def)
      apply (subst Abs_func_inverse)
      apply (rule map_comp_typed_func)
      apply (simp_all add: Rep_func)
      apply (metis ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› fb_type type_has_type(1))
      apply (rule_tac f = Abs_func in arg_cong)
      apply (simp add: fun_eq_iff, safe)
      apply (subst (3) map_comp_def)
      (*apply (subst (1) fb_f_def, simp, safe)*)
      apply (case_tac "(fb_f (Rep_func S) ∘m Rep_func A) x", simp_all)
      apply (simp add: fb_f_def)
      apply (subst TI_f_map_comp)
      apply (simp_all add: Rep_func)
      apply (metis ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› fb_type has_type_out_type has_type_type_in_a map_comp_None_iff option.sel)
      
      apply (simp add: fb_f_def)
      apply (subst TI_f_map_comp)
      apply (simp_all add: Rep_func, safe)
      apply (subst (asm) map_comp_def)
      apply (case_tac " Rep_func A x", simp_all)
      apply (subst (asm) fb_f_def, simp)
      apply (case_tac "tp aa = TO_f (Rep_func A)", simp_all)
      apply (case_tac "(Rep_func S (fb_t t (λa. hd (the (Rep_func S (a # aa)))) # aa))")
      apply (simp_all)
      apply (case_tac "tp (fb_t t (λa. hd (the (Rep_func S (a # aa)))) # aa) =  t # TO_f (Rep_func A)")
      apply (metis ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› has_type_type_in_a)
      apply simp
      prefer 2
      apply (meson ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› has_type_type_in map_comp_Some_iff)
      proof - 
        fix x a ab aa
        define b where "b ≡ fb_t t (λa. hd (the ((par_f (ID_f [t]) (Rep_func B) ∘m (Rep_func S ∘m par_f (ID_f [t]) (Rep_func A))) (a # x))))"

        assume "TI_f (Rep_func S) = t # TO_f (Rep_func A)"
        assume "TO_f (Rep_func S) = t # TI_f (Rep_func B)"
        assume D: "Rep_func S (fb_t t (λa. hd (the (Rep_func S (a # aa)))) # aa) = Some ab"
        assume E: "tl ab = a"
        assume "tp x = TI_f (Rep_func A)"
        assume [simp]:"Rep_func A x = Some aa"
        assume"tp aa = TO_f (Rep_func A)"

        have [simp]: "tv b = t"
          by (simp add: b_def)

        have C: "b = fb_t t (λa. hd (the (Rep_func S (a # aa))))"
        apply (simp add: b_def)
        apply (rule fb_t_eq_type)
        apply (simp add: map_comp_def)
        apply (subst AAAb, simp_all)
        apply (simp add: ‹tp x = TI_f (Rep_func A)›)
        apply (case_tac "Rep_func S (a # aa)", simp_all)
        apply (case_tac "aaa", simp_all)
        apply (metis ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› has_type_out_type list.distinct(1) option.sel tp.simps(1) tp.simps(2))
        apply (subst AAAb, simp_all)
        apply (metis ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› has_type_defined has_type_out_type list.sel(3) option.sel tp.simps(2))
        apply (metis ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› has_type_out_type list.inject option.sel tp.simps(2))
        by (metis ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› has_type_out_type list.inject option.sel tp.simps(2))

        obtain  u v where [simp]: "Rep_func S (b # aa) = Some (u # v)"
          apply (case_tac " Rep_func S (b # aa)")
          apply (simp_all)
          apply (simp add: ‹Rep_func S (fb_t t (λa. hd (the (Rep_func S (a # aa)))) # aa) = Some ab› ‹b = fb_t t (λa. hd (the (Rep_func S (a # aa))))›)
          apply (case_tac "a")
          apply simp_all  
          by (metis ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› ‹tv b = t› has_type_out_type list.distinct(1) option.sel tp.simps(1) tp.simps(2))

        from this have B: "v = a"
          apply (simp add: C D)
          by (cut_tac E, simp)

        have A: "((par_f (ID_f [t]) (Rep_func B) ∘m (Rep_func S ∘m par_f (ID_f [t]) (Rep_func A))) (b # x)) = Some (u # the (Rep_func B v))"
          apply (simp add: map_comp_def)
          apply (subst AAAb, simp_all)
          apply (simp add: ‹tp x = TI_f (Rep_func A)›)
          apply (subst AAAb, simp_all)
          apply (metis (mono_tags, lifting) ‹Rep_func S (b # aa) = Some (u # v)› ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› ‹tv b = t› has_type_defined has_type_out_type list.sel(3) option.sel tp.simps(2))
          apply (metis ‹Rep_func S (b # aa) = Some (u # v)› ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› ‹tv b = t› has_type_out_type list.inject option.sel tp.simps(2))
          by (metis ‹Rep_func S (b # aa) = Some (u # v)› ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹tp aa = TO_f (Rep_func A)› ‹tv b = t› has_type_out_type list.sel(3) option.sel tp.simps(2))

        have " Some (tl (the ((par_f (ID_f [t]) (Rep_func B) ∘m (Rep_func S ∘m par_f (ID_f [t]) (Rep_func A))) (b # x)))) =
           Rep_func B a"
           apply (simp add: A)
           apply (simp add: B)
           apply (case_tac " Rep_func B a", simp_all)
           by (metis ‹Rep_func S (fb_t t (λa. hd (the (Rep_func S (a # aa)))) # aa) = Some ab› ‹TI_f (Rep_func S) = t # TO_f (Rep_func A)› ‹TO_f (Rep_func S) = t # TI_f (Rep_func B)› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› ‹⋀thesis. (⋀u v. Rep_func S (b # aa) = Some (u # v) ⟹ thesis) ⟹ thesis› ‹b = fb_t t (λa. hd (the (Rep_func S (a # aa))))› ‹tl ab = a› ‹tp aa = TO_f (Rep_func A)› ‹tv b = t› has_type_out_type has_type_type_in_a list.sel(3) option.sel tp.simps(2))
        from this show " Some (tl (the ((par_f (ID_f [t]) (Rep_func B) ∘m (Rep_func S ∘m par_f (ID_f [t]) (Rep_func A)))
                           (fb_t t (λa. hd (the ((par_f (ID_f [t]) (Rep_func B) ∘m (Rep_func S ∘m par_f (ID_f [t]) (Rep_func A))) (a # x)))) # x)))) =
           Rep_func B a"
           by (simp add: b_def)
      qed

     show "TI_func S = t # ts ⟹ TO_func S = t # ts' ⟹ fb_func (parallel_func S T) = parallel_func (fb_func S) T"
      apply (simp add: TI_func_def fb_func_def TO_func_def Abs_func_inverse Rep_func parallel_func_def ID_func_def comp_func_def)
      apply (subgoal_tac " (fb_f (par_f (Rep_func S) (Rep_func T))) = (par_f (fb_f (Rep_func S)) (Rep_func T))")
      apply simp_all
      apply (simp add: fun_eq_iff, safe)
      apply (simp add: par_f_def, auto)
      apply (subst fb_f_def, auto)
      prefer 2
      apply (subst TI_f_par)
      apply (simp_all add: Rep_func)
      apply (metis TI_f_fb_f ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))›)
      prefer 2
      apply (metis Rep_func TI_f_fb_f TI_f_par ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› append.simps(2) fb_f_def list.sel(3))
      apply (simp add: fb_f_def)
      proof -
        fix x
        assume Ca: "TI_f (Rep_func S) = t # ts"
        assume "TO_f (Rep_func S) = t # ts'"
        assume "TI_f (fb_f (Rep_func S)) = ts"
        assume "tp x = ts @ TI_f (Rep_func T)"
        from this have A: "x = pref x ts @ suff x ts"
          by (simp add: pref_suff_append)
        have [simp]: "⋀a . tv a = t ⟹ (pref (a # pref x ts @ suff x ts) (TI_f (Rep_func S))) = a # pref x ts"
          using A ‹TI_f (Rep_func S) = t # ts› by auto
        have B: "⋀ a . tv a = t ⟹ 
          par_f (Rep_func S) (Rep_func T) (a # pref x ts @ suff x ts) = Some (the (Rep_func S (a # pref x ts)) @ the (Rep_func T (suff x ts)))"
          apply (simp add: par_f_def, safe)
          using A ‹TI_f (Rep_func S) = t # ts› apply auto[1]
          using ‹TI_f (Rep_func S) = t # ts› ‹tp x = ts @ TI_f (Rep_func T)› by auto

        have C: "(fb_t t (λa. hd (the (par_f (Rep_func S) (Rep_func T) (a # x))))) = (fb_t t (λa. hd (the (Rep_func S (a # pref x ts)))))"
          apply (rule fb_t_eq_type)
          apply (subst A)
          apply (simp add: B)
          apply (case_tac "the (Rep_func S (a # pref x ts))")
          apply simp_all
          proof -
            fix a :: Values
            assume a1: "tv a = t"
            assume a2: "the (Rep_func S (a # pref x ts)) = []"
            have f3: "tp (a # pref x ts) = t # ts"
              using a1 by (simp add: ‹tp x = ts @ TI_f (Rep_func T)›)
            have "tp (the (Rep_func S (a # pref x ts))) = []"
              using a2 by (metis tp.simps(1))
            then show "hd (the (Rep_func T (suff x ts))) = hd []"
              using f3 by (metis (no_types) ‹TI_f (Rep_func S) = t # ts› ‹TO_f (Rep_func S) = t # ts'› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› has_type_out_type list.distinct(1))
          qed

       have "(pref (fb_t t (λa. hd (the (Rep_func S (a # pref x ts)))) # x) (TI_f (Rep_func S))) 
            = (fb_t t (λa. hd (the (Rep_func S (a # pref x ts)))) # pref x ts)"
            by (simp add: Ca)
          
      show " tl (the (par_f (Rep_func S) (Rep_func T) (fb_t t (λa. hd (the (par_f (Rep_func S) (Rep_func T) (a # x)))) # x))) =
         tl (the (Rep_func S (fb_t t (λa. hd (the (Rep_func S (a # pref x ts)))) # pref x ts))) @ the (Rep_func T (suff x ts))"
         apply (simp add: C)
         apply (simp add: par_f_def, auto)
         prefer 2 
         apply (simp add: ‹TI_f (Rep_func S) = t # ts› ‹tp x = ts @ TI_f (Rep_func T)›)
         apply (simp add: Ca)
         apply (case_tac "the (Rep_func S (fb_t t (λa. hd (the (Rep_func S (a # pref x ts)))) # pref x ts))")
         apply (simp_all)
         apply (subgoal_tac "tp ((fb_t t (λa. hd (the (Rep_func S (a # pref x ts)))) # pref x ts)) = t # ts")
         apply (metis Ca ‹TO_f (Rep_func S) = t # ts'› ‹⋀B. Rep_func B ∈ has_in_out_type (TI_f (Rep_func B)) (TO_f (Rep_func B))› has_type_out_type list.distinct(1) tp.simps(1))
         by simp

     qed
     show "fb_func (Switch_func [t] [t]) = ID_func [t]"
      apply (simp add: TI_func_def fb_func_def TO_func_def Switch_func_def Abs_func_inverse Rep_func parallel_func_def ID_func_def comp_func_def)
      apply (subgoal_tac "(fb_f (Switch_f [t] [t])) = (ID_f [t])", simp_all)
      apply (simp add: fun_eq_iff Switch_f_def ID_f_def fb_f_def, auto)
      apply (case_tac x, simp_all, safe)
      proof -
        fix a
        assume "t = tv a"
      have "fb_t (tv a) (λaa. hd (the (if tv aa = tv a then Some (suff [aa, a] [tv a] @ pref [aa, a] [tv a]) else None)))
        = fb_t (tv a) (λ aa . a)"
        apply (rule fb_t_eq_type)
        by simp
      from this show "fb_t (tv a) (λaa. hd (the (if tv aa = tv a then Some (suff [aa, a] [tv a] @ pref [aa, a] [tv a]) else None))) = a"
        by simp
    qed
  qed
end