Theory ListProp

(**-----------------------------------------------------------------------------
 * © [I Dragomir, V Preoteasa, S Tripakis]
 *
 * Contributors:
 *  Viorel Preoteasa
 *  Iulia Dragomir
 *
 * This software is governed by the MIT licence and abiding by the rules of
 * distribution of free software. You can use, modify and/or redistribute the
 * software under the terms of the MIT licence included in this distribution.
 *)

section‹\label{sec_ListProp}List Operations. Permutations and Substitutions›

theory ListProp imports Main "~~/src/HOL/Library/Permutation"
begin
  
lemma perm_mset: "perm x y = (mset x = mset y)"
  by (simp add: mset_eq_perm)

lemma perm_tp: "perm (x@y) (y@x)"
  by (simp add: perm_mset union_commute)

  lemma perm_union_left: "perm x z ⟹ perm (x @ y) (z @ y)"
    by (simp add: perm_mset)

  lemma perm_union_right: "perm x z ⟹ perm (y @ x) (y @ z)"
    by (simp add: perm_mset)

  lemma perm_trans: "perm x y ⟹ perm y z ⟹ perm x z"
    by (simp add: perm_mset)

  lemma perm_sym: "perm x y ⟹ perm y x"
    by (simp add: perm_mset)

  lemma perm_length: "perm u v ⟹ length u = length v"
    by (metis perm_mset size_mset)

   lemma perm_set_eq: "perm x y ⟹ set x = set y"
     by (metis perm_mset set_mset_mset)
       
     lemma perm_empty[simp]: "(perm [] v) = (v = [])" and "(perm v []) = (v = [])"
       by (simp_all add: perm_mset)
         
      lemma perm_refl[simp]: "perm x x"
        by (simp add: perm_mset)


  lemma dist_perm: "⋀ y . distinct x ⟹ perm x y ⟹ distinct y"
    by (metis card_distinct distinct_card mset_eq_setD perm_mset perm_length )


      lemma split_perm: "perm (a # x) x' = (∃ y y' . x' = y @ a # y' ∧ perm x (y @ y'))"
        apply safe
        apply (subgoal_tac "∃ y y' .  x' = y @ a # y'")
        apply safe
        apply (rule_tac x = y in exI)
        apply (rule_tac x = y' in exI, simp_all)
          apply (simp add: perm_mset)
        apply (drule perm_set_eq)
        apply (simp add: set_eq_iff)
        using split_list apply fastforce
          by (simp add: perm_mset)

  fun subst:: "'a list ⇒ 'a list ⇒ 'a ⇒ 'a" where
    "subst [] [] c = c" |
    "subst (a#x) (b#y) c = (if a = c then b else subst x y c)" |
    "subst x y c = undefined"

  lemma subst_notin [simp]: "⋀ y . length x = length y ⟹ a ∉ set x ⟹ subst x y a = a"
    apply (induction x, simp_all)
    by (metis Suc_length_conv subst.simps(2))

  lemma subst_cons_a:"⋀ y . distinct x ⟹ a ∉ set x ⟹ b ∉ set x ⟹ length x = length y ⟹  subst (a # x) (b # y) c =  (subst x y (subst [a] [b] c))"
    by simp

  lemma subst_eq: "subst x x y = y"
    apply (induct x) 
    by (auto) 

  fun Subst :: "'a list ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
    "Subst x y [] = []" |
    "Subst x y (a # z) = subst x y a # (Subst x y z)"

  lemma Subst_empty[simp]: "Subst [] [] y = y"
    apply (induct y) 
    by (auto) 

  (*todo: make simp*)
  lemma Subst_eq: "Subst x x y = y"
    apply (induction y)
    by (simp_all add: subst_eq)


  lemma Subst_append: "Subst a b (x@y) = Subst a b x @ Subst a b y"
    by (induction x, simp_all)

  lemma Subst_notin[simp]: "a ∉ set z ⟹ Subst (a # x) (b # y) z = Subst x y z"
    by (induction z, simp_all)

  lemma Subst_all[simp]: "⋀ v . distinct u ⟹length u = length v ⟹ Subst u v u = v"
    apply (induction u, simp_all)
    by (case_tac v, simp_all)
    
  lemma Subst_inex[simp]: "⋀ b. set a ∩ set x = {} ⟹ length a = length b ⟹ Subst a b x = x"
    apply (induction a, simp_all)
    by (metis Subst_notin Suc_length_conv)
  
  lemma set_Subst: "set (Subst [a] [b] x) = (if a ∈ set x then (set x - {a}) ∪ {b} else set x)"
    apply (induction x)
    by auto

  lemma distinct_Subst: "distinct (b#x) ⟹ distinct (Subst [a] [b] x)"
    apply (induction x)
    apply simp_all
    by (auto simp add: set_Subst)
        
  lemma inter_Subst: "distinct(b#y) ⟹ set x ∩ set y = {} ⟹ b ∉ set x ⟹ set x ∩ set (Subst [a] [b] y) = {}"
    apply (induction y)
    by simp_all

  lemma incl_Subst: "distinct(b#x) ⟹ set y ⊆ set x ⟹ set (Subst [a] [b] y) ⊆ set (Subst [a] [b] x)"
    apply safe
    apply (simp add: set_Subst less_eq_set_def le_fun_def, auto)
    apply (case_tac "a ∈ set y", simp_all)
    apply (metis DiffE Diff_insert_absorb UnE singletonI)
    by meson

  lemma subst_in_set: "⋀y. length x = length y ⟹ a ∈ set x ⟹ subst x y a ∈ set y"
    apply (induction x, auto)
    apply (case_tac y, simp_all)
    by (case_tac y, simp_all)


  lemma Subst_set_incl: "length x = length y ⟹ set z ⊆ set x ⟹ set (Subst x y z) ⊆ set y"
    apply (induction z, auto)
    by (simp add: subst_in_set)

  lemma subst_not_in: "⋀ y . a ∉ set x' ⟹ length x = length y ⟹ length x' = length y' ⟹ subst (x @ x') (y @ y') a = subst x y a"
    apply (induction x, simp_all)
    by (case_tac y, simp_all)
    
  lemma subst_not_in_b: "⋀ y . a ∉ set x ⟹ length x = length y ⟹ length x' = length y' ⟹ subst (x @ x') (y @ y') a = subst x' y' a"
    apply (induction x, simp_all)
    by (case_tac y, simp_all, auto)

  lemma Subst_not_in: "set x' ∩ set z = {} ⟹ length x = length y ⟹ length x' = length y' ⟹ Subst (x @ x') (y @ y') z = Subst x y z"
    apply (induction z, simp_all)
    by (simp add: subst_not_in)

  lemma Subst_not_in_a: "set x ∩ set z = {} ⟹ length x = length y ⟹ length x' = length y' ⟹ Subst (x @ x') (y @ y') z = Subst x' y' z"
    apply (induction z, simp_all)
    by (simp add: subst_not_in_b)

  lemma subst_cancel_right [simp]: "⋀ y z . set x ∩ set y = {} ⟹ length y = length z ⟹ subst (x @ y) (x @ z) a = subst y z a"
    by (induction x, simp_all, safe, simp)
    
  lemma Subst_cancel_right: "set x ∩ set y = {} ⟹ length y = length z ⟹ Subst (x @ y) (x @ z) w = Subst y z w"
    by (induction w, simp_all)

  lemma subst_cancel_left [simp]: "⋀ y z . set x ∩ set z = {} ⟹ length x = length y ⟹ subst (x @ z) (y @ z) a = subst x y a"
    apply (induction x, simp_all, safe, simp)
    apply (simp add: subst_eq)
    by (case_tac y, simp_all)

  lemma Subst_cancel_left: "set x ∩ set z = {} ⟹ length x = length y ⟹ Subst (x @ z) (y @ z) w = Subst x y w"
    by (induction w, simp_all)


  lemma Subst_cancel_right_a: "a ∉  set y ⟹ length y = length z ⟹ Subst (a # y) (a # z) w = Subst y z w"
    apply (cut_tac x = "[a]" in Subst_cancel_right)
    by (simp_all)

  lemma subst_subst_id [simp]: "⋀ y . a ∈ set y ⟹ distinct x ⟹ length x = length y ⟹ subst x y (subst y x a) = a"
    apply (induction x, simp_all)
    apply (case_tac y, simp_all, auto)
    by (simp add: subst_in_set)

  lemma Subst_Subst_id[simp]: "set z ⊆ set y ⟹ distinct x ⟹ length x = length y ⟹ Subst x y (Subst y x z) = z"
    by (induction z, simp_all)

  lemma Subst_cons_aux_a: "set x ∩ set y = {} ⟹ distinct y ⟹ length y = length z ⟹ Subst (x @ y) (x @ z) y = z"
    apply (induction x)
    by simp_all

  lemma Subst_set_empty [simp]: "set z ∩ set x = {} ⟹ length x = length y ⟹ Subst x y z = z"
    by (induction z, simp_all)

  lemma length_Subst[simp]: "length (Subst x y z) = length z"
    by (induction z, simp_all)


  lemma subst_Subst: "⋀ y y' . length y = length y' ⟹ a ∈ set w ⟹ subst w (Subst y y' w) a = subst y y' a"
    by (induction w, simp_all, auto)

  lemma Subst_Subst: "length y = length y' ⟹ set z ⊆ set w ⟹ Subst w (Subst y y' w) z = Subst y y' z"
    by (induction z, simp_all add: subst_Subst)
    
  (*to sort*)
  
  primrec listinter :: "'a list ⇒ 'a list ⇒ 'a list" (infixl "⊗" 60) where
    "[] ⊗ y = []" |
    "(a # x) ⊗ y = (if a ∈ set y then a # (x ⊗ y) else x ⊗ y)"

  lemma inter_filter: "x ⊗ y = filter (λ a . a ∈ set y) x"
    by (induction x, simp_all)

  lemma inter_append: "set y ∩ set z = {} ⟹ perm (x ⊗ (y @ z)) ((x ⊗ y) @ (x ⊗ z))"
    apply (induction x, simp_all add: perm_mset)
    apply safe
    by blast

  lemma append_inter: "(x @ y) ⊗ z = (x ⊗ z) @ (y ⊗ z)"
    by (induction x, simp_all)

  lemma notin_inter [simp]: "a ∉ set x ⟹ a ∉ set (x ⊗ y)"
    by (induction x, simp_all)

  lemma distinct_inter: "distinct x ⟹ distinct (x ⊗ y)"
    by (induction x, simp_all)

  lemma set_inter: "set (x ⊗ y) = set x ∩ set y"
    by (induction x, simp_all)


  primrec diff :: "'a list ⇒ 'a list ⇒ 'a list" (infixl "⊖" 52) where
    "[] ⊖ y = []" |
    "(a # x) ⊖ y = (if a ∈ set y then x ⊖ y else a # (x ⊖ y))"

  lemma diff_filter: "x ⊖ y = filter (λ a . a ∉ set y) x"
    by (induction x, simp_all)

  lemma diff_distinct: "set x ∩ set y = {} ⟹ (y ⊖ x) = y"
    by (induction y, simp_all)

  lemma set_diff: "set (x ⊖ y) = set x - set y"
    by (induction x, simp_all, auto)

  lemma distinct_diff: "distinct x ⟹ distinct (x ⊖ y)"
    by (induction x, simp_all add: set_diff)


  definition addvars :: "'a list ⇒ 'a list ⇒ 'a list" (infixl "⊕" 55) where
    "addvars x y = x @ (y ⊖ x)"

  lemma addvars_distinct: "set x ∩ set y = {} ⟹ x ⊕ y = x @ y"
    by (simp add: addvars_def diff_distinct)

  lemma set_addvars: "set (x ⊕ y) = set x ∪ set y"
    by (simp add: addvars_def set_diff)

  lemma distinct_addvars: "distinct x ⟹ distinct y ⟹ distinct (x ⊕ y)"
    apply (simp add: addvars_def, induction x, simp_all)
    apply (simp add: distinct_diff)
    by (simp add: Diff_Int_distrib distinct_diff set_diff)

  lemma mset_inter_diff: "mset oa = mset (oa ⊗ ia) + mset (oa ⊖ (oa ⊗ ia))"
    apply (simp add: inter_filter diff_filter)
    by (metis (mono_tags, lifting) filter_cong mset_filter multiset_partition)

  lemma diff_inter_left: "(x ⊖ (x ⊗ y)) = (x ⊖ y)"
    apply (simp add: diff_filter inter_filter)
    by (metis (no_types, lifting) filter_cong)

  lemma diff_inter_right: "(x ⊖ (y ⊗ x)) = (x ⊖ y)"
    apply (simp add: diff_filter inter_filter)
    by (metis (no_types, lifting) filter_cong)

  lemma addvars_minus: "(x ⊕ y) ⊖ z = (x ⊖ z) ⊕ (y ⊖ z)"
    apply (simp add: diff_filter addvars_def)
    by (metis)
   
  lemma addvars_assoc: "x ⊕ y ⊕ z = x ⊕ (y ⊕ z)"
    apply (simp add: addvars_def diff_filter)
    by metis

  lemma diff_sym: "(x ⊖ y ⊖ z) = (x ⊖ z ⊖ y)"
    apply (simp add: diff_filter)
    by metis
   
  lemma diff_union: "(x ⊖ y @ z) = (x ⊖ y ⊖ z)"
    by (simp add: diff_filter)

  lemma diff_notin: "set x ∩ set z = {} ⟹ (x ⊖ (y ⊖ z)) = (x ⊖ y)"
    apply (simp add: diff_filter disjoint_iff_not_equal)
    by (metis (no_types, lifting) filter_cong)

  lemma union_diff: "x @ y ⊖ z = ((x ⊖ z) @ (y ⊖ z))"
    by (simp add: diff_filter)

  lemma diff_inter_empty: "set x ∩ set y = {} ⟹ x ⊖ y ⊗ z = x"
    apply (simp add: diff_filter inter_filter)
    by (metis (no_types, lifting) disjoint_iff_not_equal filter_True)

  lemma inter_diff_empty: "set x ∩ set z = {} ⟹ x ⊗ (y ⊖ z) = (x ⊗ y)"
    apply (simp add: diff_filter inter_filter)
    by (metis (no_types, lifting) disjoint_iff_not_equal filter_cong)

  lemma inter_diff_distrib: "(x ⊖ y) ⊗ z = ((x ⊗ z) ⊖ (y ⊗ z))"
    apply (simp add: diff_filter inter_filter)
    by (metis)

  lemma diff_emptyset: "x ⊖ [] = x"
    by (simp add: diff_filter)

  lemma diff_eq: "x ⊖ x = []"
    by (simp add: diff_filter)

  lemma diff_subset: "set x ⊆ set y ⟹ x ⊖ y = []"
    by (metis Diff_eq_empty_iff set_diff set_empty)

  lemma empty_inter: "set x ∩ set y = {} ⟹ x ⊗ y = []"
    by (metis set_empty set_inter)

  lemma empty_inter_diff: "set x ∩ set y = {} ⟹ x ⊗ (y ⊖ z) = []"
    apply (simp add: inter_filter diff_filter)
    by (metis (no_types, lifting) disjoint_iff_not_equal filter_False)

  lemma inter_addvars_empty: "set x ∩ set z = {} ⟹ x ⊗ y @ z = x ⊗ y"
    apply (simp add: inter_filter)
    by (metis (no_types, lifting) disjoint_iff_not_equal filter_cong)

  lemma diff_disjoint: "set x ∩ set y = {} ⟹ x ⊖ y = x"
    by (metis diff_distinct inter_filter inter_set_filter set_inter)
    
      lemma addvars_empty[simp]: "x ⊕ [] = x"
        by (simp add: addvars_def)

      lemma empty_addvars[simp]: "[] ⊕ x = x"
        apply (induction x, simp_all)
        by (simp add: addvars_def)


  lemma distrib_diff_addvars: "x ⊖ (y @ z) = ((x ⊖ y) ⊗ (x ⊖ z))"
    apply (simp add: diff_filter inter_filter)
    by (metis diff_filter diff_inter_left filter_True filter_filter inter_diff_distrib inter_filter inter_set_filter set_inter)

  lemma inter_subset: "x ⊗ (x ⊖ y) = (x ⊖ y)"
    by (metis diff_emptyset diff_union distrib_diff_addvars)

  lemma diff_cancel: "x ⊖ y ⊖ (z ⊖ y) = (x ⊖ y ⊖ z)"
    by (simp add: diff_notin inf_commute set_diff)

  lemma diff_cancel_set: "set x ∩ set u = {} ⟹ x ⊖ y ⊖ (z ⊖ u) = (x ⊖ y ⊖ z)"
    by (metis diff_notin diff_sym)

  lemma inter_subset_l1: "⋀ y. distinct x ⟹ length y = 1 ⟹ set y ⊆ set x ⟹ x ⊗ y = y"
    apply (induction x, simp_all)
    apply safe
    apply (metis (no_types, lifting) Diff_insert_absorb Int_insert_left_if0 Suc_length_conv empty_inter empty_iff inf.orderE inf_commute length_0_conv list.set(1) list.simps(15) singletonD subset_insert_iff)
    by auto

  lemma perm_diff_left_inter: "perm (x ⊖ y) (((x ⊖ y) ⊗ z) @ ((x ⊖ y) ⊖ z))"
    proof (simp add: diff_filter inter_filter perm_mset)
      have "∀p as pa. {#a ∈# mset as. pa (a::'a) ∧ p a#} = filter_mset p (filter_mset pa (mset as))"
        by (metis filter_filter mset_filter)
      then show "{#a ∈# mset x. a ∉ set y#} = {#a ∈# mset x. a ∉ set y ∧ a ∈ set z#} + {#a ∈# mset x. a ∉ set y ∧ a ∉ set z#}"
        by auto
    qed
    
  lemma perm_diff_right_inter: "perm (x ⊖ y) (((x ⊖ y) ⊖ z) @ ((x ⊖ y) ⊗ z))"  
    by (metis perm_mset perm_diff_left_inter perm_tp)      


  lemma perm_switch_aux_a: "perm x ((x ⊖ y) @ (x ⊗ y))"
    by (metis diff_emptyset perm_diff_right_inter)

  lemma perm_switch_aux_b: "perm (x @ (y ⊖ x)) ((x ⊖ y) @ (x ⊗ y) @ (y ⊖ x))"
    by (metis perm_switch_aux_a append_assoc mset_append perm_mset)

  lemma perm_switch_aux_c: "distinct x ⟹ distinct y ⟹ perm ((y ⊗ x) @ (y ⊖ x)) y"
    by (metis perm_switch_aux_a perm_mset perm_tp)

  lemma perm_switch_aux_d: "distinct x ⟹ distinct y ⟹ perm (x ⊗ y) (y ⊗ x)"
    by (metis distinct_inter inf.commute perm_mset set_eq_iff_mset_eq_distinct set_inter)
     
  lemma perm_switch_aux_e: "distinct x ⟹ distinct y ⟹ perm ((x ⊗ y) @ (y ⊖ x)) ((y ⊗ x) @ (y ⊖ x))"
    by (simp add: perm_union_left perm_switch_aux_d)

  lemma perm_switch_aux_f: "distinct x ⟹ distinct y ⟹ perm ((x ⊗ y) @ (y ⊖ x)) y"
    apply (cut_tac x="((x ⊗ y) @ (y ⊖ x))"  and y ="((y ⊗ x) @ (y ⊖ x))" and z="y" in perm_trans)
      apply (simp add: perm_switch_aux_e)
      apply (simp add: perm_switch_aux_d)
    apply (simp add: perm_switch_aux_c)
    by simp
      
  lemma perm_switch_aux_h: "distinct x ⟹ distinct y ⟹ perm ((x ⊖ y) @ (x ⊗ y) @ (y ⊖ x)) ((x ⊖ y) @ y)"
    by (simp add: perm_union_right perm_switch_aux_f)

  lemma perm_switch: "distinct x ⟹ distinct y ⟹ perm (x @ (y ⊖ x)) ((x ⊖ y) @ y)"
    apply (cut_tac x="(x @ (y ⊖ x))"  and y ="((x ⊖ y) @ (x ⊗ y) @ (y ⊖ x))" and z="((x ⊖ y) @ y)" in perm_trans)
      apply (simp add: perm_switch_aux_b)
      using perm_switch_aux_h apply blast
    by simp

  lemma perm_aux_a: "distinct x ⟹ distinct y ⟹ x ⊗ y = x ⟹ perm (x @ (y ⊖ x)) y"
    apply (cut_tac x=x and y=y in perm_switch_aux_f)
    by (simp_all)
      lemma ZZZ_a: "x ⊕ (y ⊖ x) = (x ⊕ y)"
        apply (simp add: addvars_def)
        by (induction y, simp_all)

      lemma ZZZ_b: "set (y ⊗ z) ∩ set x = {} ⟹ (x ⊖ (y ⊖ z) ⊖ (z ⊖ y)) = (x ⊖ y ⊖ z)"
        by (induction x, simp_all add: set_diff set_inter)

      lemma subst_subst: "⋀ y z . a ∈ set z ⟹ distinct x ⟹ length x = length y ⟹ length z = length x 
        ⟹ subst x y (subst z x a) = subst z y a"
        apply (induction x, simp_all)
        apply (case_tac y, simp_all)
        apply (case_tac z, simp_all, auto)
        by (simp add: subst_in_set)

        
      lemma Subst_Subst_a: "set u ⊆ set z ⟹ distinct x ⟹ length x = length y ⟹ length z = length x 
      ⟹ Subst x y (Subst z x u) = (Subst z y u)"
        apply (induction u, simp_all)
        apply (case_tac y, simp_all)
        by (rule subst_subst,simp_all)
      lemma subst_in: "⋀ x' . length x = length x' ⟹ a ∈ set x ⟹ subst (x @ y) (x' @ y') a = subst x x' a"
        apply (induction x, simp_all)
        by (case_tac x', auto)

      lemma subst_switch: "⋀ x' . set x ∩ set y = {} ⟹ length x = length x' ⟹ length y = length y' 
        ⟹ subst (x @ y) (x' @ y') a = subst (y @ x) (y' @ x') a"
        apply (induction x, simp_all)
        apply (case_tac x', simp_all, safe)
        apply (simp add: subst_not_in_b)
        apply (case_tac "a ∈ set y", simp_all)
        apply (simp add: subst_in)
        by (simp add: subst_not_in_b)

      lemma Subst_switch: "set x ∩ set y = {} ⟹ length x = length x' ⟹ length y = length y' 
        ⟹ Subst (x @ y) (x'@ y') z = Subst (y @ x) (y'@ x') z"
        apply (induction z, simp_all)
        by (subst subst_switch, simp_all)

      lemma subst_comp: "⋀ x' . set x ∩ set y = {} ⟹ set x' ∩ set y = {} ⟹ length x = length x' 
        ⟹ length y = length y' ⟹ subst (x @ y) (x' @ y') a = subst y y' (subst x x' a)"
        apply (induction x, simp_all)
        by (case_tac x', simp_all)

      lemma Subst_comp: "set x ∩ set y = {} ⟹ set x' ∩ set y = {} ⟹ length x = length x' 
      ⟹ length y = length y' ⟹ Subst (x @ y) (x' @ y') z = Subst y y' (Subst x x' z)"
        by (induction z, simp_all add: subst_comp)

      lemma set_subst: "⋀ u' . length u = length u' ⟹ subst u u' a ∈ set u' ∪ ({a} - set u)"
        apply (induction u, simp_all)
        by (case_tac u', simp_all, auto)


      lemma set_Subst_a: "length u = length u' ⟹ set (Subst u u' z) ⊆ set u' ∪ (set z - set u)"
        apply (induction z, simp_all)
        by (cut_tac u = u and u' = u' and a  = a in set_subst, simp_all, auto)


      lemma set_SubstI: "length u = length u' ⟹ set u' ∪ (set z - set u) ⊆ X ⟹ set (Subst u u' z) ⊆ X"
        apply (rule_tac y = "set u' ∪ (set z - set u)" in order_trans)
        by (rule set_Subst_a, simp_all)

  lemma not_in_set_diff: "a ∉ set x ⟹ x ⊖ ys @ a # zs = x ⊖ ys @ zs"
    by (induction x, auto)
      
  lemma [simp]: "(X ∩ (Y ∪ Z) = {}) = (X ∩ Y = {} ∧ X ∩ Z = {})"
    by auto
      
      (*very specialized*)  
      lemma Comp_assoc_new_subst_aux: "set u ∩ set y ∩ set z = {} ⟹ distinct z ⟹ length u = length u' 
        ⟹ Subst (z ⊖ v) (Subst u u' (z ⊖ v)) z = Subst (u ⊖ y ⊖ v) (Subst u u' (u ⊖ y ⊖ v)) z"
        apply (induction z, simp_all, auto)
        apply (subst subst_notin)
        apply (simp_all add: set_diff)
        apply (case_tac "a ∈ set u", simp_all)
        apply (cut_tac z = "[a]" in Subst_Subst [of u u' _ "(u ⊖ y ⊖ v)"], simp_all)
        by (simp_all add: set_diff)

      lemma [simp]: "(x ⊖ y ⊖ (y ⊖ z)) = (x ⊖ y)"
        by (induction x, simp_all, auto simp add: set_diff)

      lemma [simp]: "(x ⊖ y ⊖ (y ⊖ z ⊖ z')) = (x ⊖ y)"
        by (induction x, simp_all, auto simp add: set_diff)

      lemma diff_addvars: "x ⊖ (y ⊕ z) = (x ⊖ y ⊖ z)"
        by (induction x, auto simp add: set_diff set_addvars)

      lemma diff_redundant_a: "x ⊖ y ⊖ z ⊖ (y ⊖ u) = (x ⊖ y ⊖ z)"
        by (induction x, simp_all add: set_diff)

      lemma diff_redundant_b: "x ⊖ y ⊖ z ⊖ (z ⊖ u) = (x ⊖ y ⊖ z)"
        by (induction x, simp_all add: set_diff)

      lemma diff_redundant_c: "x ⊖ y ⊖ z ⊖ (y ⊖ u ⊖ v) = (x ⊖ y ⊖ z)"
        by (induction x, simp_all add: set_diff)

      lemma diff_redundant_d: "x ⊖ y ⊖ z ⊖ (z ⊖ u ⊖ v) = (x ⊖ y ⊖ z)"
        by (induction x, simp_all add: set_diff)

   lemma set_list_empty: "set x = {} ⟹ x = []"
      by (induction x, simp_all)

    lemma [simp]: "(x ⊖ x ⊗ y) ⊗ (y ⊖ x ⊗ y) = []"
      apply (rule set_list_empty)
      by (simp add: set_inter set_diff, auto)

    lemma [simp]: "set x ∩ set (y ⊖ x) = {}"
      by (simp add: set_diff)

lemma [simp]:" distinct x ⟹ distinct y ⟹ set x ⊆ set y ⟹ perm (x @ (y ⊖ x)) y"
  by (metis append_Nil diff_subset perm_switch)

    lemma [simp]: "perm x y ⟹ set x ⊆ set y"
      by (simp add: perm_set_eq)
    lemma [simp]: "perm x y ⟹ set y ⊆ set x"
      by (simp add: perm_set_eq)

    lemma [simp]: "set (x ⊖ y) ⊆ set x"
      by (auto simp add: set_diff)
        
      lemma perm_diff[simp]: "⋀ x' . perm x x' ⟹ perm y y' ⟹ perm (x ⊖ y) (x' ⊖ y')"
        apply (induction x, simp_all)
        apply (frule_tac x = y and y = y' in perm_set_eq, simp)
        apply (simp add: split_perm union_diff)
        apply auto
        apply (simp_all add: union_diff)
        apply (metis union_diff)
        by (metis union_diff)

    lemma [simp]: "perm x x' ⟹ perm y y' ⟹ perm (x @ y) (x' @ y')"
      by (simp add: perm_mset)

    lemma [simp]: "perm x x' ⟹ perm y y' ⟹ perm (x ⊕ y) (x' ⊕ y')"
      by (simp add: addvars_def)

    thm distinct_diff
      
declare distinct_diff [simp]
  (*
    declare perm_set_eq [simp]
*)
    lemma [simp]: "⋀ x' . perm x x' ⟹ perm y y' ⟹ perm (x ⊗ y) (x' ⊗ y')"
      apply (induction x, simp_all, safe)
      apply (simp add: split_perm, safe, simp_all)
      apply (rule_tac x = "ya ⊗ y'" in exI)
      apply (rule_tac x = "y'a ⊗ y'" in exI)
      apply (simp add: append_inter)
      apply (subgoal_tac "perm (x ⊗ y) ((ya @ y'a) ⊗ y')")
      apply (subst (asm) append_inter, simp_all add: perm_set_eq)

      apply (simp add: split_perm, safe, simp_all)
      apply (subgoal_tac "perm (x ⊗ y) ((ya @ y'a) ⊗ y')")
      apply (subst (asm) append_inter, simp add: append_inter)
      by simp

    declare distinct_inter [simp]

    lemma perm_ops: "perm x x' ⟹ perm y y' ⟹ f = (⊗) ∨ f = (⊖) ∨ f = (⊕) ⟹ perm (f x y) (f x' y')"
      apply safe
      by (simp_all)
      

    lemma [simp]: "perm x' x ⟹ perm y' y ⟹ f = (⊗) ∨ f = (⊖) ∨ f = (⊕) ⟹ perm (f x y) (f x' y')"
      by (rule_tac x = x and y = y and x' = x' and y' = y' in perm_ops, unfold perm_mset, simp_all)
      
    lemma [simp]: "perm x x' ⟹ perm y' y ⟹ f = (⊗) ∨ f = (⊖) ∨ f = (⊕) ⟹ perm (f x y) (f x' y')"
      by (rule_tac x = x and y = y and x' = x' and y' = y' in perm_ops, unfold perm_mset, simp_all)

    lemma [simp]: "perm x' x ⟹ perm y y' ⟹ f = (⊗) ∨ f = (⊖) ∨ f = (⊕) ⟹ perm (f x y) (f x' y')"
      by (rule_tac x = x and y = y and x' = x' and y' = y' in perm_ops, unfold perm_mset, simp_all)

      lemma diff_cons: "(x ⊖ (a # y)) = (x ⊖ [a] ⊖ y)"
        by (induction x, simp_all)

    lemma [simp]: "x ⊕ y ⊕ x = x ⊕ y"
        apply (simp add: addvars_def)
        by (simp add: diff_eq diff_union)

      lemma  subst_subst_inv: "⋀ y . distinct y ⟹ length x = length y ⟹ a ∈ set x ⟹ subst y x (subst x y a) = a"
        by (induction x, auto)
              

      lemma Subst_Subst_inv: "distinct y ⟹ length x = length y ⟹ set z ⊆ set x ⟹ Subst y x (Subst x y z) = z"
        apply (induction z)
        by (simp_all add: subst_subst_inv)

      (*move*)
      lemma perm_append: "perm x x' ⟹ perm y y' ⟹ perm (x @ y) (x' @ y')"
        by (simp add: perm_mset)



      lemma "x' = y @ a # y' ⟹ perm x (y @ y') ⟹ perm (a # x) x'"
        by (simp add: perm_mset)



      lemma perm_diff_eq: "perm y y' ⟹ (x ⊖ y) = (x ⊖ y')"
        apply (drule perm_set_eq)
        by (induction x, auto)

      lemma [simp]: "A ∩ B = {} ⟹ x ∈ A ⟹ x ∈ B ⟹ False"
        by auto
      lemma [simp]: "A ∩ B = {} ⟹ x ∈ A ⟹ x ∉ B"
        by auto

      lemma [simp]: "B ∩ A = {} ⟹ x ∈ A ⟹ x ∉ B"
        by auto
      lemma [simp]: "B ∩ A = {} ⟹ x ∈ A ⟹ x ∈ B ⟹ False"
        by auto

lemma distinct_perm_set_eq: "distinct x ⟹ distinct y ⟹ perm x y = (set x = set y)"
  by (simp add: perm_mset set_eq_iff_mset_eq_distinct)

      lemma set_perm: "distinct x ⟹ distinct y ⟹ set x = set y ⟹ perm x y"
        by (simp add: distinct_perm_set_eq)

      lemma distinct_perm_switch: "distinct x ⟹ distinct y ⟹ perm (x ⊕ y) (y ⊕ x)"
        apply (simp add: addvars_def)
        by (rule set_perm, simp_all add: set_diff, auto)
lemma listinter_diff: "(x ⊗ y) ⊖ z = (x ⊖ z) ⊗ (y ⊖ z)"
  apply (induction x, simp_all)
  by (simp add: set_diff)
    
lemma set_listinter: "set y = set z ⟹ x ⊗ y = x ⊗ z"
  by (induction x, simp_all)
    
lemma AAA_c: "a ∉ set x ⟹ x ⊖ [a] = x"
  by (induction x, simp_all, auto)

lemma distinct_perm_cons: "distinct x ⟹ perm (a # y) x ⟹ perm y (x ⊖ [a])"
  apply (rule set_perm)
    apply (meson dist_perm distinct.simps(2) perm_sym)
   apply simp
  proof -
    assume a1: "distinct x"
  assume a2: "perm (a # y) x"
  then have "set (a # y) = set x"
    by (meson perm_set_eq)
  then show "set y = set (x ⊖ [a])"
    using a2 a1 by (metis (no_types) AAA_c diff.simps(2) dist_perm distinct.simps(2) list.set_intros(1) perm_sym set_diff)
qed
   
lemma listinter_empty[simp]: " y ⊗ [] = []"
  by (induction y, simp_all)
    

lemma subsetset_inter: "set x ⊆ set y ⟹ (x ⊗ y) = x"
  by (induction x, auto)

  
lemma addvars_addsame: "x ⊕ y ⊕ (x ⊖ z) = x ⊕ y"
  by (metis ListProp.diff_eq ZZZ_a addvars_empty diff_addvars)

lemma ZZZ: "x ⊖ x ⊕ y = []"
  by (simp add: ListProp.diff_eq diff_addvars)

lemma perm_dist_mem: "distinct x ⟹ a ∈ set x ⟹ perm (a # (x ⊖ [a])) x"
  by (metis Diff_iff distinct.simps(2) distinct_diff empty_set insert_Diff list.set(2) list.set_intros(1) set_diff set_perm) 


lemma addvars_diff: "b # (x ⊕ (z ⊖ [b])) = (b # x) ⊕ z"
proof -
  have "z ⊖ [b] ⊖ b # x = z ⊖ [b] ⊖ [] ⊖ [b] ⊖ x ⊖ []"
    by (metis diff_cons diff_emptyset)
    then have f1: "x @ (z ⊖ [b] ⊖ b # x) = x ⊕ (z ⊖ [b] ⊖ b # x)"
      by (metis (no_types) ZZZ_a addvars_def diff_cons)
    have "z ⊖ [b] ⊖ b # x = z ⊖ [b] ⊖ x ⊖ [b]"
      by (metis (no_types) diff_cons diff_sym)
    then show ?thesis
      using f1 by (metis (no_types) addvars_def append.simps(2) diff_cons)
  qed

    
lemma perm_cons: "a ∈ set y ⟹ distinct y ⟹ perm x (y ⊖ [a]) ⟹ perm (a # x) y"
  apply (rule set_perm, simp_all add: set_diff perm_set_eq, safe)
  using dist_perm distinct_diff perm_sym by blast
 
end