Theory FCF_Set

(* solving pattern problems in finite constructor form:
  - all l-terms are variables (so these can be deleted)
  - all t-terms are constructor terms of finite sorts
 *)

(* this theory has set-based transformation rules *)

theory FCF_Set
  imports 
    Pattern_Completeness_Multiset
    FCF_Problem
begin


text ‹A problem is in finite variable form, if only variables occur in the problem and
   these variable all have a finite sort. Moreover, comparison of variables is only done
   if they have the same sort.
›

definition finite_var_form_match :: "('f,'s) ssig ⇒ ('f,'v,'s)match_problem_set ⇒ bool" where
  "finite_var_form_match C mp ⟷ var_form_match mp ∧
  (∀l x y. (Var x, l) ∈ mp ⟶ (Var y, l) ∈ mp ⟶ snd x = snd y) ∧
  (∀l x. (Var x, l) ∈ mp ⟶ finite_sort C (snd x))"

lemma finite_var_form_matchD:
  assumes "finite_var_form_match C mp" and "(t,l) ∈ mp"
  shows "∃x ι y. t = Var (x,ι) ∧ l = Var y ∧ finite_sort C ι ∧
    (∀z. (Var z, Var y) ∈ mp ⟶ snd z = ι)"
  using assms by (auto simp: finite_var_form_match_def var_form_match_def)

definition finite_var_form_pat :: "('f,'s) ssig ⇒ ('f,'v,'s)pat_problem_set ⇒ bool" where
  "finite_var_form_pat C p = (∀ mp ∈ p. finite_var_form_match C mp)"

lemma finite_var_form_patD:
  assumes "finite_var_form_pat C pp" "mp ∈ pp" "(t,l) ∈ mp"
  shows "∃x ι y. t = Var (x,ι) ∧ l = Var y ∧ finite_sort C ι ∧
    (∀z. (Var z, Var y) ∈ mp ⟶ snd z = ι)"
  using assms[unfolded finite_var_form_pat_def] finite_var_form_matchD by metis

lemma finite_var_form_imp_of_var_form_pat:
  "finite_var_form_pat C pp ⟹ var_form_pat pp"
  by (auto simp: finite_var_form_pat_def var_form_pat_def finite_var_form_match_def)

lemma finite_var_form_pat_UNIQ_sort:
  assumes fvf: "finite_var_form_pat C pp"
    and f: "f ∈ var_form_of_pat pp"
  shows "UNIQ (snd ` f x)"
proof (intro Uniq_I, clarsimp)
  from f obtain mp where mp: "mp ∈ pp" and f: "f = var_form_of_match mp"
    by (auto simp: var_form_of_pat_def)
  fix y ι z κ assume "(y,ι) ∈ f x" "(z,κ) ∈ f x"
  with f have y: "(Var (y,ι), Var x) ∈ mp" and z: "(Var (z,κ), Var x) ∈ mp"
    by (auto simp: var_form_of_match_def)
  from finite_var_form_patD[OF fvf mp y] z
  show "ι = κ" by auto
qed

lemma finite_var_form_pat_pat_complete:
  assumes fvf: "finite_var_form_pat C pp"
  shows "pat_complete C pp ⟷
    (∀α. (∀v ∈ tvars_pat pp. α v < card_of_sort C (snd v)) ⟶
    (∃mp ∈ pp. ∀x. UNIQ {α y |y. (Var y, Var x) ∈ mp}))"
proof-
  note vf = finite_var_form_imp_of_var_form_pat[OF fvf]
  note pat_complete_var_form_nat[of "var_form_of_pat pp" C]
  note this[unfolded tvars_var_form_pat[OF vf]]
  note * = this[unfolded pat_of_var_form_pat[OF vf]]
  show ?thesis
    apply (subst *)
    subgoal
    proof
      fix y ι
      assume y: "(y,ι) ∈ tvars_pat pp"
      from y obtain mp t l where mp: "mp ∈ pp" and tl:"(t,l) ∈ mp" and yt: "(y, ι) ∈ vars t"
        by (auto simp: tvars_pat_def tvars_match_def)
      from finite_var_form_patD[OF fvf mp tl] yt
      show "finite_sort C ι" by auto
    qed
    subgoal using finite_var_form_pat_UNIQ_sort[OF fvf] by force
    subgoal 
      apply (rule all_cong)
      apply (unfold ex_var_form_pat)
      apply (rule bex_cong[OF refl])
      apply (rule all_cong1)
      apply (rule arg_cong[of _ _ UNIQ])
      by (auto simp: var_form_of_match_def)
    done
qed


context pattern_completeness_context
begin


(* all subterms of some sort of cardinality 1 will be replaced by the same variable (which is here fixed to 0) *)
fun flatten_triv_sort_main :: "('f,nat × 's)term ⇒ ('f,nat × 's)term × 's" where
  "flatten_triv_sort_main (Var x) = (if cd_sort (snd x) = 1 then (Var (0, snd x), snd x) else (Var x, snd x))" 
| "flatten_triv_sort_main (Fun f ts) = (let tss = map flatten_triv_sort_main ts in
     case C (f,map snd tss) of Some s ⇒ if cd_sort s = 1 then (Var (0,s), s) else (Fun f (map fst tss), s))" 

definition flatten_triv_sort :: "('f,nat × 's)term ⇒ ('f,nat × 's)term" where
  "flatten_triv_sort = fst o flatten_triv_sort_main" 

definition flatten_triv_sort_pat :: "('f,'s)simple_pat_problem ⇒ ('f,'s)simple_pat_problem" where
  "flatten_triv_sort_pat = image (image (image flatten_triv_sort))" 

end

context pattern_completeness_context_with_assms
begin

lemma flatten_triv_sort_spp: assumes "finite_constructor_form_pat p" 
  shows "finite_constructor_form_pat (flatten_triv_sort_pat p)" 
    "simple_pat_complete C SS (flatten_triv_sort_pat p) ⟷ simple_pat_complete C SS p" 
proof -
  show "simple_pat_complete C SS (flatten_triv_sort_pat p) ⟷ simple_pat_complete C SS p"
    unfolding simple_pat_complete_def flatten_triv_sort_pat_def bex_simps simple_match_complete_wrt_def ball_simps
      UNIQ_subst_def
  proof (intro all_cong bex_cong refl ball_cong arg_cong[of _ _ UNIQ])
    fix σ mp eqc
    assume σ: "σ :⇩s 𝒱 |` SS → 𝒯(C)" 
      and mp: "mp ∈ p" 
      and eqc: "eqc ∈ mp" 
    {
      fix t
      assume "t ∈ eqc" 
      with assms[unfolded finite_constructor_form_defs, rule_format, OF mp eqc]
      obtain ι where "t : ι in 𝒯(C,𝒱 |` SS)" by auto
      hence "map_prod (λ t. t ⋅ σ) id (flatten_triv_sort_main t) = (t ⋅ σ, ι)" 
      proof (induct)
        case (Var x ι)
        then obtain v where xv: "x = (v,ι)" and ι: "ι ∈ S" 
          by (auto simp: sorted_map_def restrict_map_def hastype_def split: if_splits)
        show ?case
        proof (cases "cd_sort ι = 1")
          case False
          thus ?thesis using xv by auto
        next
          case True
          from cd[OF ι] True
          have "card_of_sort C ι = 1" using minBnd1 by auto
          from this[unfolded card_of_sort_def] obtain s where s: "{s. s : ι in 𝒯(C)} = {s}" 
            by (metis card_1_singletonE)
          {
            fix y
            have "σ (y, ι) : ι in 𝒯(C)" using σ ι
              by (simp add: hastype_restrict sorted_map_def)
            with s have "σ (y, ι) = s" by auto
          }
          thus ?thesis using True xv by simp
        qed
      next
        case (Fun f ts ιs ι) 
        from Fun(1) have C: "C (f, ιs) = Some ι" by (rule fun_hastypeD)
        from Fun(3) have map_snd: "map snd (map flatten_triv_sort_main ts) = ιs"
          apply (intro nth_equalityI) 
          subgoal by (auto simp: list_all2_conv_all_nth)
          subgoal for i using arg_cong[OF list_all2_nthD[OF Fun(3), of i], of snd] by auto
          done  
        show ?case
        proof (cases "cd_sort ι = 1")
          case False
          hence "map_prod (λt. t ⋅ σ) id (flatten_triv_sort_main (Fun f ts)) = 
               (Fun f (map (λ t. t ⋅ σ) (map fst (map flatten_triv_sort_main ts))), ι)" 
            using map_snd C by simp
          also have "(map (λ t. t ⋅ σ) (map fst (map flatten_triv_sort_main ts)))
               = (map (λ t. t ⋅ σ) ts)" unfolding map_map o_def
            apply (intro nth_equalityI, force)
            subgoal for i using arg_cong[OF list_all2_nthD[OF Fun(3), of i], of fst] by auto
            done
          finally show ?thesis by simp
        next
          case True
          hence id: "map_prod (λt. t ⋅ σ) id (flatten_triv_sort_main (Fun f ts)) = (σ (0,ι), ι)" 
            using C map_snd by simp
          from C_sub_S[OF Fun(1)] have ι: "ι ∈ S" by auto
          from True[unfolded cd[OF ι] card_of_sort_def minBnd1]
          obtain s where s: "{s. s : ι in 𝒯(C)} = {s}" 
            by (metis card_1_singletonE)
          have var: "Var (0, ι) : ι in 𝒯(C, 𝒱 |` SS)" using ι by (simp add: hastype_def)            
          have f: "Fun f ts : ι in 𝒯(C, 𝒱 |` SS)" using Fun(1-2) by (metis Fun_hastypeI)
          {
            fix t
            assume "t : ι in 𝒯(C, 𝒱 |` SS)" 
            hence "t ⋅ σ : ι in 𝒯(C)" using σ by (metis subst_hastype)
            with s have "t ⋅ σ = s" by blast
          } note subst = this 
          from subst[OF var] subst[OF f]
          show ?thesis unfolding id by auto
        qed
      qed          
      from arg_cong[OF this, of fst]
      have "flatten_triv_sort t ⋅ σ = t ⋅ σ" unfolding flatten_triv_sort_def by simp
    }
    thus "flatten_triv_sort ` eqc ⋅⇩s⇩e⇩t σ = eqc ⋅⇩s⇩e⇩t σ"
      by (metis (no_types, lifting) image_cong image_image)
  qed
  show "finite_constructor_form_pat (flatten_triv_sort_pat p)" 
    unfolding flatten_triv_sort_pat_def ball_simps finite_constructor_form_defs
  proof (intro ballI conjI)
    fix mp eqc
    assume "mp ∈ p" "eqc ∈ mp" 
    from assms[unfolded finite_constructor_form_defs, rule_format, OF this] obtain ι
      where fin: "finite_sort C ι" and t: "⋀ t. t ∈ eqc ⟹ t : ι in 𝒯(C,𝒱 |` SS)" 
         and ne: "eqc ≠ {}" by auto
    show "flatten_triv_sort ` eqc ≠ {}" using ne by auto
    show "∃ι. finite_sort C ι ∧ (∀ t ∈ eqc. flatten_triv_sort t : ι in 𝒯(C,𝒱 |` SS))" 
    proof (intro exI[of _ ι] conjI fin ballI)
      fix t
      assume "t ∈ eqc" 
      from t[OF this] have "t : ι in 𝒯(C,𝒱 |` SS)" by auto
      hence "fst (flatten_triv_sort_main t) : ι in 𝒯(C,𝒱 |` SS) ∧ snd (flatten_triv_sort_main t) = ι" 
      proof (induct)
        case (Var x ι)
        thus ?case by (auto simp: hastype_def restrict_map_def split: if_splits)
      next
        case (Fun f ts ιs ι)
        from Fun(1) have C: "C (f, ιs) = Some ι" by (rule fun_hastypeD)
        from C_sub_S[OF Fun(1)] have ι: "ι ∈ S" by auto
        from Fun(3) have map_snd: "map snd (map flatten_triv_sort_main ts) = ιs"
          apply (intro nth_equalityI) 
          subgoal by (auto simp: list_all2_conv_all_nth)
          subgoal for i using list_all2_nthD[OF Fun(3), of i] by auto
          done  
        show ?case
        proof (cases "cd_sort ι = 1")
          case False
          hence id: "flatten_triv_sort_main (Fun f ts) = 
             (Fun f (map fst (map flatten_triv_sort_main ts)), ι)" 
            using map_snd C by simp
          show ?thesis unfolding id fst_conv snd_conv
            apply (intro conjI refl Fun_hastypeI[OF Fun(1)] list_all2_all_nthI)
            subgoal using Fun(3) by (auto simp: list_all2_conv_all_nth)
            subgoal for i using list_all2_nthD[OF Fun(3), of i] by auto
            done
        next
          case True
          hence id: "flatten_triv_sort_main (Fun f ts) = (Var (0,ι), ι)" 
            using C map_snd by auto
          thus ?thesis using ι by (simp add: hastype_def restrict_map_def)
        qed
      qed
      thus "flatten_triv_sort t : ι in 𝒯(C,𝒱 |` SS)" unfolding flatten_triv_sort_def by auto
    qed
  qed
qed

lemma eliminate_uniq_spp: assumes "finite_constructor_form_pat p" 
  and "p = insert mp p'" 
  and "mp = insert eqc mp'" 
  and "pn = insert mp' p'" 
  and "UNIQ eqc" 
shows "simple_pat_complete C SS p ⟷ simple_pat_complete C SS pn" 
  "finite_constructor_form_pat pn"
proof 
  show "simple_pat_complete C SS p ⟹ simple_pat_complete C SS pn" unfolding assms
    by (auto simp: simple_pat_complete_def simple_match_complete_wrt_def)
  show "finite_constructor_form_pat pn"
    using assms unfolding finite_constructor_form_defs by auto
  from ‹UNIQ eqc› have "UNIQ_subst σ eqc" for σ :: "_ ⇒ ('f, unit)term" 
    unfolding UNIQ_subst_def by (rule image_Uniq)
  thus "simple_pat_complete C SS pn ⟹ simple_pat_complete C SS p" unfolding assms
    by (auto simp: simple_pat_complete_def simple_match_complete_wrt_def)
qed

(* note that a decomposition step might create equivalence classes with
   different sorts, so these need to be filtered. Example: consider 
     f : [Int,Int] → Bool and f : [Nat,Nat] → Bool, then
     decomposing f(xI,yI) = f(xN,yN) would lead to xI = xN and yI = yN *)
lemma decompose_spp: assumes "finite_constructor_form_pat p" 
  and p: "p = insert mp p'" 
  and mp: "mp = insert eqc mp'" 
  and root: "⋀ t. t ∈ eqc ⟹ root t = Some (f,n)" 
  and eqcn: "eqcn = (λ i. (λ t. args t ! i) ` eqc) ` {0..<n}" 
  and pn: "pn = (if Ball eqcn (λ eq. UNIQ (𝒯(C,𝒱) ` eq)) then insert (eqcn ∪ mp') p' else p')" 
shows "simple_pat_complete C SS p ⟷ simple_pat_complete C SS pn" 
  "finite_constructor_form_pat pn"
proof -
  {
    fix t
    assume "t ∈ eqc" 
    from root[OF this]
    have "t = Fun f (map (λ i. args t ! i) [0..<n])" 
      by (cases t; auto intro: nth_equalityI)
  } note to_args = this
  from assms(1)[unfolded finite_constructor_form_pat_def p]
  have "finite_constructor_form_mp mp" by auto
  from this[unfolded mp finite_constructor_form_mp_def]
  obtain ι where typed: "⋀ t. t ∈ eqc ⟹ t : ι in 𝒯(C,𝒱 |` SS)" by auto
  have "simple_pat_complete C SS p ⟷ simple_pat_complete C SS (insert (eqcn ∪ mp') p')" 
    unfolding simple_pat_complete_def p pn bex_simps mp simple_match_complete_wrt_def ball_simps ball_Un
  proof (intro all_cong disj_cong refl conj_cong) 
    fix σ :: "_ ⇒ (_,unit)term" 
    show "UNIQ_subst σ eqc = Ball eqcn (UNIQ_subst σ)" 
    proof 
      assume uniq: "UNIQ_subst σ eqc" 
      show "Ball eqcn (UNIQ_subst σ)" unfolding eqcn
      proof clarsimp
        fix i
        assume i: "i < n" 
        show "UNIQ_subst σ {args t ! i |. t ∈ eqc}" (is "UNIQ_subst _ ?args")
        proof (intro UNIQ_subst_pairI)
          fix si ti
          assume *: "si ∈ ?args" "ti ∈ ?args" 
          from * obtain s where s: "s ∈ eqc" and si: "si = args s ! i" by auto
          from * obtain t where t: "t ∈ eqc" and ti: "ti = args t ! i" by auto
          from arg_cong[OF UNIQ_subst_pairD[OF uniq s t], of "λ t. args t ! i"] i
          show "si ⋅ σ = ti ⋅ σ" unfolding si ti using root[OF s] root[OF t] by (cases s; cases t; auto)
        qed
      qed
    next
      assume "Ball eqcn (UNIQ_subst σ)" 
      from this[unfolded eqcn, simplified]
      have uniq: "i < n ⟹ UNIQ_subst σ {args t ! i |. t ∈ eqc}" for i by auto
      show "UNIQ_subst σ eqc" 
      proof (intro UNIQ_subst_pairI)
        fix s t
        assume s: "s ∈ eqc" and t: "t ∈ eqc" 
        show "s ⋅ σ = t ⋅ σ" 
          apply (subst to_args[OF s], subst to_args[OF t])
          apply clarsimp
          subgoal for i using UNIQ_subst_pairD[OF uniq[of i]] s t by auto
          done
      qed
    qed
  qed
  also have "… = simple_pat_complete C SS pn" 
  proof (cases "∀eq∈eqcn. UNIQ (𝒯(C,𝒱) ` eq)")
    case True
    thus ?thesis unfolding pn by auto
  next
    case False
    hence pn: "pn = p'" unfolding pn by auto
    from False obtain eq where eq_mem: "eq ∈ eqcn" and nuniq: "¬ UNIQ (𝒯(C,𝒱) ` eq)" by auto
    from nuniq[unfolded Uniq_def] obtain si ti where 
      st: "si ∈ eq" "ti ∈ eq" and diff: "𝒯(C,𝒱) si ≠ 𝒯(C,𝒱) ti" by auto
    from eq_mem[unfolded eqcn] obtain i where i: "i < n" and eq: "eq = {args t ! i |. t ∈ eqc}" by auto
    {
      fix ti
      assume "ti ∈ eq" 
      from this[unfolded eq] obtain t where ti: "ti = args t ! i" and t: "t ∈ eqc" by auto
      from typed[OF t] have "t : ι in 𝒯(C,𝒱 |` SS)" by auto
      with to_args[OF t] have "Fun f (map ((!) (args t)) [0..<n]) : ι in 𝒯(C,𝒱 |` SS)" by auto
      from this[unfolded Fun_hastype list_all2_conv_all_nth] i 
      have "∃ ι. ti : ι in 𝒯(C,𝒱 |` SS)" unfolding ti by force
    }
    from this[OF st(1)] this[OF st(2)] obtain ιs ιt where 
      typed: "si : ιs in 𝒯(C,𝒱 |` SS)" "ti : ιt in 𝒯(C,𝒱 |` SS)" by auto
    hence "si : ιs in 𝒯(C,𝒱)" "ti : ιt in 𝒯(C,𝒱)" 
      by (meson hastype_in_Term_mono_right restrict_submap)+
    with diff have diff: "ιs ≠ ιt" unfolding hastype_def by auto
    show ?thesis unfolding simple_pat_complete_def pn
    proof (intro all_cong)
      fix σ
      assume sig: "σ :⇩s 𝒱 |` SS → 𝒯(C)" 
      have "¬ simple_match_complete_wrt σ (eqcn ∪ mp')" 
      proof
        assume "simple_match_complete_wrt σ (eqcn ∪ mp')" 
        hence "simple_match_complete_wrt σ eqcn" unfolding simple_match_complete_wrt_def by auto
        from this[unfolded simple_match_complete_wrt_def] eq_mem
        have "UNIQ_subst σ eq" by auto
        with st have equiv: "si ⋅ σ = ti ⋅ σ" by (metis UNIQ_subst_pairD)
        from typed sig 
        have typed: "si ⋅ σ : ιs in 𝒯(C)" "ti ⋅ σ : ιt in 𝒯(C)" by (metis subst_hastype)+
        hence "si ⋅ σ ≠ ti ⋅ σ" using diff unfolding hastype_def by auto
        with equiv show False by simp
      qed
      thus "Bex (insert (eqcn ∪ mp') p') (simple_match_complete_wrt σ) = Bex p' (simple_match_complete_wrt σ)" 
        by simp
    qed
  qed
  finally show "simple_pat_complete C SS p = simple_pat_complete C SS pn" .
  show "finite_constructor_form_pat pn" using assms(1)
    unfolding pn p mp finite_constructor_form_pat_def ball_simps
  proof (simp, intro impI)
    assume fin: "finite_constructor_form_mp (insert eqc mp') ∧ Ball p' finite_constructor_form_mp" 
      and uniq: "∀eq∈eqcn. UNIQ (𝒯(C,𝒱) ` eq)" 
    show "finite_constructor_form_mp (eqcn ∪ mp')" unfolding finite_constructor_form_mp_def
    proof
      fix eqc'
      assume "eqc' ∈ eqcn ∪ mp'" 
      thus "eqc' ≠ {} ∧ (∃ι. finite_sort C ι ∧ (∀ t ∈ eqc'. t : ι in 𝒯(C,𝒱 |` SS)))" 
      proof
        assume "eqc' ∈ mp'" 
        thus ?thesis using fin unfolding finite_constructor_form_mp_def by auto
      next
        assume eqc'_mem: "eqc' ∈ eqcn" 
        from this[unfolded eqcn] obtain i where i: "i < n" and 
           eqc': "eqc' = {args t ! i |. t ∈ eqc}" by auto
        from fin[unfolded finite_constructor_form_mp_def] obtain ι
          where fin: "finite_sort C ι" and ne: "eqc ≠ {}" and typed: "t ∈ eqc ⟹ t : ι in 𝒯(C,𝒱 |` SS)" for t
          by auto
        from ne obtain t where t: "t ∈ eqc" by auto
        from typed[OF t] have "t : ι in 𝒯(C,𝒱 |` SS)" by auto
        with to_args[OF t] 
        have "Fun f (map ((!) (args t)) [0..<n]) : ι in 𝒯(C,𝒱 |` SS)" by auto
        from finite_arg_sorts[OF fin this, of "args t ! i"] i
        obtain ιi where ti: "args t ! i : ιi in 𝒯(C, 𝒱 |` SS)" and fin: "finite_sort C ιi" by auto  
        have ti_mem: "args t ! i ∈ eqc'" unfolding eqc' using i t by auto
        have wti: "args t ! i : ιi in 𝒯(C, 𝒱)" using ti 
          by (meson hastype_in_Term_mono_right restrict_submap)
        from ti_mem ti wti obtain ti where 
          ti: "ti : ιi in 𝒯(C, 𝒱 |` SS)" "ti : ιi in 𝒯(C, 𝒱)" "ti ∈ eqc'" by auto
        show ?thesis
        proof (intro exI[of _ ιi] conjI ballI fin)
          show "eqc' ≠ {}" using ne unfolding eqc' by auto
          fix si
          assume si: "si ∈ eqc'"
          with uniq[rule_format, OF eqc'_mem] ti 
          have type_si: "si : ιi in 𝒯(C,𝒱)" 
            unfolding Uniq_def hastype_def by auto
          from si[unfolded eqc'] obtain s where si: "si = args s ! i" and s: "s ∈ eqc" by auto
          from typed[OF s] to_args[OF s]
          have "Fun f (map ((!) (args s)) [0..<n]) : ι in 𝒯(C,𝒱 |` SS)" by auto
          from this[unfolded Fun_hastype list_all2_conv_all_nth] i si
          have "∃ ιi. si : ιi in 𝒯(C, 𝒱 |` SS)" by auto
          then obtain ι2 where si: "si : ι2 in 𝒯(C, 𝒱 |` SS)" by auto
          hence "si : ι2 in 𝒯(C, 𝒱)"
            by (meson hastype_in_Term_mono_right restrict_submap)
          with type_si have "ιi = ι2" by (auto simp: hastype_def)    
          thus "si : ιi in 𝒯(C,𝒱 |` SS)" using si by auto
        qed
      qed
    qed
  qed
qed        

lemma eliminate_clash_spp: assumes "finite_constructor_form_pat p" 
  and "p = insert mp pn" 
  and "mp = insert eqc mp'" 
  and "eqc = {s,t} ∪ eqc'" 
  and "Conflict_Clash s t" 
shows "simple_pat_complete C SS p ⟷ simple_pat_complete C SS pn" 
  "finite_constructor_form_pat pn"
proof 
  from mp_fail_pcorrect1[OF match_fail_mp_fail[OF match_fail.match_clash'[OF assms(5)]], 
      of _ undefined "{#}" "λ _. None", unfolded match_complete_wrt_def tvars_match_def, simplified]
  have clash: "σ :⇩s 𝒱 |` (vars s ∪ vars t) → 𝒯(C) ⟹ s ⋅ σ ≠ t ⋅ σ" for σ by metis
  from assms(1)[unfolded finite_constructor_form_pat_def finite_constructor_form_mp_def] assms
  obtain ι where typed: "u ∈ {s,t} ⟹  u : ι in 𝒯(C,𝒱 |` SS)" for u by auto
  have "vars u ⊆ dom (𝒱 |` SS)" if "u ∈ {s,t}" for u using typed[OF that] 
    by (rule hastype_in_Term_imp_vars_subset)
  hence st: "vars s ∪ vars t ⊆ SS" by auto
  {
    fix σ
    assume sig: "σ :⇩s 𝒱 |` SS → 𝒯(C)" 
    have "s ⋅ σ ≠ t ⋅ σ" 
    proof (rule clash)
      show "σ :⇩s 𝒱 |` (vars s ∪ vars t) → 𝒯(C)" 
        using sig st by (meson restrict_map_mono_right sorted_map_cmono)
    qed
    hence "¬ UNIQ_subst σ eqc" unfolding assms UNIQ_subst_def Uniq_def by auto 
  }
  thus "simple_pat_complete C SS p ⟹ simple_pat_complete C SS pn" unfolding assms(2-3)
    by (auto simp: simple_pat_complete_def simple_match_complete_wrt_def)
  show "finite_constructor_form_pat pn"
    using assms unfolding finite_constructor_form_defs by auto
  show "simple_pat_complete C SS pn ⟹ simple_pat_complete C SS p" unfolding assms
    by (auto simp: simple_pat_complete_def simple_match_complete_wrt_def)
qed


lemma detect_sat_spp: 
  assumes "p = insert {} p'" 
  shows "simple_pat_complete C SS p" 
  unfolding assms by (auto simp: simple_pat_complete_def simple_match_complete_wrt_def)

lemma detect_unsat_spp:
  shows "¬ simple_pat_complete C SS {}" 
  using σg' by (auto simp: simple_pat_complete_def simple_match_complete_wrt_def)

lemma separate_var_fun_spp: assumes "finite_constructor_form_pat p"
  and p: "p = insert mp p'" 
  and mp: "mp = insert eqc mp'" 
  and eqc: "eqc = {x,t} ∪ eqcV ∪ eqcF" 
  and Pn: "Pn = {insert {{x,t}} p', insert ({insert x eqcV}) p', insert ({insert t eqcF} ∪ mp') p'}" 
shows "simple_pat_complete C SS p ⟷ (∀ pn ∈ Pn. simple_pat_complete C SS pn)" 
  "Ball Pn finite_constructor_form_pat" 
proof -
  let ?spc = "simple_pat_complete C SS" 
  note spc = simple_pat_complete_def simple_match_complete_wrt_def
  have main: "UNIQ_subst σ eqc ⟷ UNIQ_subst σ {x,t} ∧ UNIQ_subst σ (insert x eqcV) ∧ UNIQ_subst σ (insert t eqcF)"   
    (is "?l = ?r") for σ :: "_ ⇒ (_,unit)term"
  proof 
    assume ?l
    show ?r 
      by (intro conjI; rule UNIQ_subst_mono[OF _ ‹?l›], auto simp: eqc)
  next
    assume ?r
    hence *: "UNIQ_subst σ {x, t}" "UNIQ_subst σ (insert x eqcV)" "UNIQ_subst σ (insert t eqcF)" by auto
    show ?l 
    proof (intro UNIQ_subst_pairI)
      fix a b
      assume "a ∈ eqc" "b ∈ eqc" 
      with
        UNIQ_subst_pairD[OF *(1), of x t]
        UNIQ_subst_pairD[OF *(2), of x]
        UNIQ_subst_pairD[OF *(2), of a b]
        UNIQ_subst_pairD[OF *(3), of t]
        UNIQ_subst_pairD[OF *(3), of a b]
      show "a ⋅ σ = b ⋅ σ" unfolding eqc by fastforce
    qed
  qed
  have "?spc p ⟷ (?spc (insert {eqc} p') ∧ ?spc (insert mp' p'))" 
    unfolding p mp spc by auto
  also have "… ⟷
     ?spc (insert {{x,t}} p') ∧ (?spc (insert mp' p') ∧ ?spc (insert {insert x eqcV} p') ∧ ?spc (insert {insert t eqcF} p'))" 
    (is "_ ⟷ _ ∧ ?sub")
    unfolding spc by (auto simp: main)
  also have "?sub ⟷ ?spc (insert ({insert x eqcV}) p') ∧ ?spc (insert ({insert t eqcF} ∪ mp') p')" 
    by (auto simp: spc) 
  finally show "?spc p ⟷ (∀ pn ∈ Pn. ?spc pn)" unfolding Pn by auto
  show "Ball Pn finite_constructor_form_pat" using assms(1) unfolding assms
    by (auto simp: finite_constructor_form_pat_def finite_constructor_form_mp_def)
qed

lemma separate_var_fun_spp_single: assumes "finite_constructor_form_pat p"
  and p: "p = insert mp p'" 
  and mp: "mp = insert eqc mp'" 
  and eqc: "eqc = {x,t} ∪ eqc'" 
  and Pn: "Pn = {insert {{x,t}} p', insert ({insert x eqc'} ∪ mp') p'}" 
shows "simple_pat_complete C SS p ⟷ (∀ pn ∈ Pn. simple_pat_complete C SS pn)" 
  "Ball Pn finite_constructor_form_pat" 
proof -
  let ?spc = "simple_pat_complete C SS" 
  have swap: "{t, x} = {x,t}" by auto
  from eqc have eqc: "eqc = {t,x} ∪ {} ∪ eqc'" by auto
  note step = separate_var_fun_spp[OF assms(1) p mp eqc refl]
  from step(2) show "Ball Pn finite_constructor_form_pat" unfolding Pn swap by auto
  show  "simple_pat_complete C SS p ⟷ (∀ pn ∈ Pn. simple_pat_complete C SS pn)" 
    unfolding step(1) unfolding swap Pn
    by (simp, auto simp: simple_pat_complete_def simple_match_complete_wrt_def)
qed
     


lemma instantiate_spp: assumes "finite_constructor_form_pat p"
  and disj: "fst ` tvars_spat p ∩ {n..<n + m} = {}" 
  and x: "x ∈ tvars_spat p" 
  and Pn: "Pn = (λ τ. (`) ((`) (λ t. t ⋅ τ)) ` p) ` τs n x" 
shows "simple_pat_complete C SS p ⟷ (∀ pn ∈ Pn. simple_pat_complete C SS pn)" 
  "Ball Pn finite_constructor_form_pat" 
proof 
  assume comp: "simple_pat_complete C SS p" 
  show "(∀ pn ∈ Pn. simple_pat_complete C SS pn)" 
    unfolding simple_pat_complete_def
  proof (intro ballI allI impI)
    fix pn σ
    assume "pn ∈ Pn" and sig: "σ :⇩s 𝒱 |` SS → 𝒯(C)" 
    from this[unfolded Pn] obtain τ where tau: "τ ∈ τs n x" 
      and pn: "pn = (`) ((`) (λt. t ⋅ τ)) ` p" by auto
    from tau[unfolded τs_def] obtain f ιs where
      tau: "τ = τc n x (f,ιs)" and f: "f : ιs → snd x in C" by auto
    define t where "t = Fun f (map (λ i. σ (n + i, ιs ! i)) [0 ..< length ιs])" 
    from C_sub_S[OF f] have x: "snd x ∈ S" and ιs: "set ιs ⊆ S" by auto
    have t: "t : snd x in 𝒯(C)" 
      unfolding t_def
    proof (intro Fun_hastypeI[OF f] list_all2_all_nthI, force, clarsimp)
      fix i
      assume "i < length ιs" 
      hence "ιs ! i ∈ S" using ιs by auto
      with sig show "σ (n + i, ιs ! i) : ιs ! i in 𝒯(C)"
        by (simp add: restrict_map_eq_restrict_sset sorted_map_def)
    qed        
    define σ' where "σ' = σ(x := t)" 
    from sig t have sig': "σ' :⇩s 𝒱 |` SS → 𝒯(C)" unfolding σ'_def sorted_map_def
      by (metis comp_apply fun_upd_apply hastypeD hastypeI hastype_restrict)
    from comp[unfolded simple_pat_complete_def, rule_format, OF this]
    obtain mp where mp: "mp ∈ p" and comp: "simple_match_complete_wrt σ' mp" by auto
    let ?mp = "(`) (λt. t ⋅ τ) ` mp" 
    from mp have mem: "?mp ∈ pn" unfolding pn by auto
    {
      fix i
      assume i: "i < length ιs" and 
        x: "x = (n + i, ιs ! i)" 
      from m[OF f] i have "i < m" by auto
      with disj x assms(3) have False by fastforce
    } note x_disj = this

    have xtau: "x ∉ vars (s ⋅ τ)" for s 
    proof
      assume "x ∈ vars (s ⋅ τ)" 
      from this[unfolded tau τc_def split vars_term_subst subst_def]
      obtain i where i: "i < length ιs" and 
        x: "x = (n + i, ιs ! i)" by (auto simp: set_conv_nth split: if_splits)
      with x_disj show False by auto
    qed

    show "Bex pn (simple_match_complete_wrt σ)" 
    proof (intro bexI[OF _ mem])
      have "simple_match_complete_wrt σ ?mp = simple_match_complete_wrt σ' ?mp" 
      proof (rule tvars_spat_cong[of pn])
        show "?mp ∈ pn" unfolding pn  using mp by auto
        fix y
        assume "y ∈ tvars_spat pn" 
        thus "σ y = σ' y" 
          unfolding σ'_def pn by (auto simp: xtau)
      qed
      also have …
        unfolding simple_match_complete_wrt_def
      proof (intro ballI UNIQ_subst_pairI, clarsimp)
        fix eqc s s'
        assume eqc: "eqc ∈ mp" and st: "s ∈ eqc" "s' ∈ eqc" 
        from comp[unfolded simple_match_complete_wrt_def UNIQ_subst_alt_def, rule_format, OF this]
        have eq: "s ⋅ σ' = s' ⋅ σ'" .
        {
          fix y
          have "(τ ∘⇩s σ') y = σ' y" 
          proof (cases "y = x")
            case False
            thus ?thesis unfolding subst_compose_def tau τc_def split by (simp add: subst_def)
          next
            case True
            show ?thesis unfolding True using x_disj 
              by (auto simp add: tau τc_def subst_compose_def σ'_def t_def intro!: nth_equalityI)
          qed
        }
        thus "s ⋅ τ ⋅ σ' = s' ⋅ τ ⋅ σ'" using eq
          by (metis subst_same_vars subst_subst_compose)
      qed
      finally show "simple_match_complete_wrt σ ?mp" by auto
    qed
  qed
next
  {
    from x obtain eqc mp t where *: "eqc ∈ mp" "mp ∈ p" "t ∈ eqc" and x: "x ∈ vars t" by auto
    from * assms(1)[unfolded finite_constructor_form_pat_def] 
    have "finite_constructor_form_mp mp" by auto
    from this[unfolded finite_constructor_form_mp_def] * obtain ι 
      where "t : ι in 𝒯(C, 𝒱 |` SS)" by auto
    from hastype_in_Term_imp_vars[OF this x]
    have "snd x ∈ S" unfolding restrict_map_def by (auto split: if_splits)
  } note xS = this

  assume comp: "∀pn∈Pn. simple_pat_complete C SS pn" 
  show "simple_pat_complete C SS p" unfolding simple_pat_complete_def
  proof (intro impI allI)
    fix σ
    assume sig: "σ :⇩s 𝒱 |` SS → 𝒯(C)" 
    have "x : snd x in 𝒱 |` SS" using xS by (cases x, auto simp: hastype_def restrict_map_def)
    with sig have sigx: "σ x : snd x in 𝒯(C)" by (rule sorted_mapD)
    then obtain f ts where sigxF: "σ x = Fun f ts" 
      by (cases "σ x", auto)
    from sigx[unfolded this Fun_hastype] obtain ιs 
      where f: "f : ιs → snd x in C" and ts: "ts :⇩l ιs in 𝒯(C)" by auto
    define τ where "τ = τc n x (f,ιs)" 
    define cond where "cond y = (fst y ∈ {n..<n+length ιs} ∧ snd y = ιs ! (fst y - n))" for y 
    define σ' where "σ' y = (if cond y then ts ! (fst y - n) else σ y)" for y
    {
      fix y
      assume "cond y" 
      hence "∃ i. y = (n + i, ιs ! i) ∧ σ' y = ts ! i ∧ i < length ιs" 
        unfolding cond_def σ'_def by (cases y, auto intro!: exI[of _ "fst y - n"])
    } note cond = this
    have sig': "σ' :⇩s 𝒱 |` SS → 𝒯(C)" 
    proof
      fix y ι
      assume y: "y : ι in 𝒱 |` SS" 
      show "σ' y : ι in 𝒯(C)" 
      proof (cases "cond y")
        case False
        hence "σ' y = σ y" unfolding σ'_def by auto
        with y sig show ?thesis by (metis sorted_mapE)
      next
        case True
        from cond[OF this]
        obtain i where *: "i < length ιs" "σ' y = ts ! i" "y = (n + i, ιs ! i)" by auto
        from *(3) y have "ι = ιs ! i" 
          by (auto simp: hastype_def restrict_map_def split: if_splits)
        with y * show ?thesis using list_all2_nthD2[OF ts, of i] by auto
      qed
    qed
    let ?p = "(`) ((`) (λ t. t ⋅ τ)) ` p" 
    from f have "τ ∈ τs n x" unfolding τs_def τ_def by auto
    hence "?p ∈ Pn" by (auto simp: assms)
    from comp[rule_format, OF this, unfolded simple_pat_complete_def, rule_format, OF sig']
    obtain mp where mp: "mp ∈ p" and comp: "simple_match_complete_wrt σ' ((`) (λt. t ⋅ τ) ` mp)" by auto
    show "Bex p (simple_match_complete_wrt σ)" 
    proof (intro bexI[OF _ mp])
      have "simple_match_complete_wrt σ mp = simple_match_complete_wrt σ' mp" 
      proof (rule tvars_spat_cong[OF _ mp])
        fix y
        assume yp: "y ∈ tvars_spat p" 
        show "σ y = σ' y" 
        proof (cases "cond y")
          case False
          thus ?thesis unfolding σ'_def by auto
        next
          case True
          from cond[OF this] obtain i where y: "y = (n + i, ιs ! i)" and i: "i < length ιs" by auto
          from disj yp have "fst y ∉ {n ..< n + m}" by fastforce
          with y have "i ≥ m" by auto
          with m[OF f] i have False by auto
          thus ?thesis ..
        qed
      qed
      also have … unfolding simple_match_complete_wrt_def UNIQ_subst_alt_def
      proof clarify
        fix eqc s t
        assume "eqc ∈ mp" "s ∈ eqc" "t ∈ eqc" 
        from comp[unfolded simple_match_complete_wrt_def UNIQ_subst_alt_def, rule_format, OF imageI imageI imageI, OF this]
        have eq: "s ⋅ τ ⋅ σ' = t ⋅ τ ⋅ σ'" .
        {
          fix y
          have "(τ ∘⇩s σ') y = σ' y" 
          proof (cases "y = x")
            case False
            thus ?thesis unfolding subst_compose_def τ_def τc_def split by (simp add: subst_def)
          next
            case True
            have cx: "¬ cond x" 
            proof
              assume "cond x" 
              from cond[OF this] m[OF f] have "fst x ∈ {n ..< n + m}" by auto
              with disj x show False by blast
            qed
            hence sig'x: "σ' x = σ x" unfolding σ'_def by auto
            show ?thesis unfolding True sig'x sigxF using cx ts[unfolded list_all2_conv_all_nth]
              by (auto simp add: τc_def subst_compose_def σ'_def τ_def cond_def intro!: nth_equalityI)
          qed
        }
        with eq show "s ⋅ σ' = t ⋅ σ'" by (metis eval_same_vars_cong eval_subst)
      qed
      finally show "simple_match_complete_wrt σ mp" .
    qed
  qed
next
  show "Ball Pn finite_constructor_form_pat" 
    unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def
  proof (intro ballI, goal_cases)
    case (1 pn mpn eqcn)
    from this[unfolded Pn] obtain τ mp eqc where
      mem: "mp ∈ p" "eqc ∈ mp" and eqcn: "eqcn = (λ t. t ⋅ τ) ` eqc" 
      and tau: "τ ∈ τs n x" 
      by auto
    from tau[unfolded τs_def] obtain f σs where f: "f : σs → snd x in C" and tau: "τ = τc n x (f,σs)" by auto
    from assms(1)[unfolded finite_constructor_form_pat_def finite_constructor_form_mp_def, rule_format, OF mem]
    obtain ι where ne: "eqc ≠ {}" and fin: "finite_sort C ι" and typed: " t ∈ eqc ⟹ t : ι in 𝒯(C,𝒱 |` SS)" for t by auto 
    show "eqcn ≠ {} ∧ (∃ι. finite_sort C ι ∧ (∀t∈eqcn. t : ι in 𝒯(C,𝒱 |` SS)))" 
    proof (intro conjI exI[of _ ι] fin ballI)
      show "eqcn ≠ {}" using ne unfolding eqcn by auto
      fix tt
      assume "tt ∈ eqcn" 
      then obtain t where t: "t ∈ eqc" and tt: "tt = t ⋅ τ" unfolding eqcn by auto
      from typed[OF t] have t: "t : ι in 𝒯(C,𝒱 |` SS)" by auto
      show "tt : ι in 𝒯(C, 𝒱 |` SS)" unfolding tt
      proof (rule subst_hastype[OF _ t], standard)
        fix y σ
        assume y: "y : σ in 𝒱 |` SS" 
        show "τ y : σ in 𝒯(C,𝒱 |` SS)" 
        proof (cases "y = x")
          case False
          with y show ?thesis unfolding tau τc_def split subst_def by simp
        next
          case True
          with y have σ: "σ = snd x" by (auto simp: hastype_def restrict_map_def split: if_splits)
          {
            fix i
            assume "i < length σs"
            hence "σs ! i ∈ S" using C_sub_S[OF f] by auto
            hence "(n + i, σs ! i) : σs ! i in 𝒱 |` SS" by (auto simp: hastype_def restrict_map_def)
          }
          thus ?thesis unfolding σ True tau τc_def split subst_def
            by (auto intro!: Fun_hastypeI[OF f] list_all2_all_nthI)
        qed
      qed
    qed
  qed
qed

lemma typed_restrict_imp_typed: "t : s in 𝒯(D, W |` F) ⟹ t : s in 𝒯(D, W)"
  by (meson Term_mono_right restrict_submap subssetD)

lemma eliminate_large_sort: assumes
  cond: "⋀ i. i ≤ (n :: nat) ⟹ snd (x i) = ι ∧ eq i ∈ mp i ∧ Var (x i) ≠ t i ∧ {Var (x i), t i} ⊆ eq i" and
  vars: "(t ` {0..n} ∪ (Var o x) ` {0..n}) ∩ Var ` tvars_spat p = {}" and
  large: "card (t ` {0..n}) < cd_sort ι" and
  fin: "finite_constructor_form_pat (p ∪ mp ` {0..n})" 
shows "simple_pat_complete C SS (p ∪ mp ` {0..n}) = simple_pat_complete C SS p" 
proof 
  assume comp: "simple_pat_complete C SS p"
  thus "simple_pat_complete C SS (p ∪ mp ` {0..n})" 
    unfolding simple_pat_complete_def by blast
next
  let ?p' = "p ∪ mp ` {0..n}"
  assume comp: "simple_pat_complete C SS ?p'"
  show "simple_pat_complete C SS p" 
    unfolding simple_pat_complete_def
  proof (intro allI impI, goal_cases)
    case σ: (1 σ)
    let ?T = "t ` {0..n}" 
    let ?TX = "?T ∪ (Var o x) ` {0..n}" 
    define DomT where "DomT = {x. Var x ∈ ?T}"
    define Dom where "Dom = DomT ∪ x ` {0..n}" 
    define Avoid where "Avoid = {t ⋅ σ |t. t ∈ ?T ∧ is_Fun t}"
    define Ran where "Ran = {t. t : ι in 𝒯(C)} - Avoid"
    {
      fix i
      assume i: "i ≤ n" 
      note cond = cond[OF this]
      from cond have eq: "eq i ∈ mp i" by auto
      from i fin have "finite_constructor_form_mp (mp i)" 
        unfolding finite_constructor_form_pat_def by auto
      from this[unfolded finite_constructor_form_mp_def, rule_format, OF eq]
      obtain ι' where fin: "finite_sort C ι'" and sort: "⋀ s. s∈eq i ⟹ s : ι' in 𝒯(C,𝒱 |` SS)" 
        by auto
      from cond have terms: "Var (x i) ∈ eq i" "t i ∈ eq i" "x i : ι in 𝒱" by auto
      from sort[OF this(1)] this(3) have id: "ι' = ι"
        by (metis Var_hastype typed_S_eq)
      note fin = fin[unfolded id]
      note sort = sort[unfolded id]
      from sort[OF terms(1)] have iota: "ι ∈ S" by (rule typed_imp_S)
      note sort[OF terms(1)] sort[OF terms(2)] fin iota
    } note terms = this
  
    have finι: "finite_sort C ι" using terms[of 0] by auto
    have "ι ∈ S" using terms[of 0] by auto
    note terms = terms(1,2)
    {
      fix s
      assume "s ∈ ?TX" 
      with terms have "s : ι in 𝒯(C,𝒱 |` SS)" by auto
    } note TX = this
    hence T: "s ∈ ?T ⟹ s : ι in 𝒯(C,𝒱 |` SS)" for s by auto
        
    {
      define Terms where "Terms = ?T" 
      define GTerms where "GTerms = {s. s : ι in 𝒯(C)}" 
      from finι have finG: "finite GTerms" unfolding GTerms_def finite_sort_def by auto
      from large[unfolded cd[OF ‹ι ∈ S›] card_of_sort_def] minBnd_gt
      have fin: "finite Terms" 
        and card: "card Terms < card GTerms" 
        by (auto simp: Terms_def GTerms_def)
      define Other where "Other = {t. t ∈ ?T ∧ is_Fun t}" 
      let ?Var = "Var :: nat × 's ⇒ ('f, nat × 's)term"
      have splitTerms: "?Var ` DomT ∪ Other ⊆ Terms" "?Var ` DomT ∩ Other = {}"  
        unfolding DomT_def Terms_def Other_def by auto
      from splitTerms finite_subset[OF _ fin] 
      have fin': "finite (?Var ` DomT)" "finite Other" 
        by auto
      from card_mono[OF fin splitTerms(1)] card card_Un_disjoint[OF fin'] splitTerms
      have "card (?Var ` DomT) + card Other < card GTerms" 
        by auto
      hence "card DomT < card GTerms - card Other" using card_image[of ?Var]
        by simp
      also have "… ≤ card GTerms - card (Other  ⋅⇩s⇩e⇩t σ)" using fin'(2)
        by (meson card_image_le diff_le_mono2)
      also have "… = card (GTerms - (Other  ⋅⇩s⇩e⇩t σ))" 
      proof (rule card_Diff_subset[symmetric, OF finite_imageI[OF fin'(2)]])
        {
          fix ts
          assume "ts ∈ Other ⋅⇩s⇩e⇩t σ"
          then obtain t where "t ∈ ?T" and ts: "ts = t ⋅ σ" 
            unfolding Other_def by auto
          with terms have "t : ι in 𝒯(C, 𝒱 |` SS)" by auto
          with σ have "ts ∈ GTerms" unfolding ts GTerms_def by (simp add: subst_hastype)
        }
        thus "Other ⋅⇩s⇩e⇩t σ ⊆ GTerms" by auto
      qed
      also have "Other  ⋅⇩s⇩e⇩t σ = Avoid" unfolding Other_def Avoid_def by auto
      also have id: "GTerms - Avoid = Ran" unfolding Ran_def GTerms_def by simp
      finally have main: "card DomT < card Ran" .      
      from finG have finR: "finite Ran" unfolding id[symmetric] by blast
      have finD: "finite DomT" using finite_imageD[OF fin'(1)] by auto
      from main obtain fresh where fresh: "fresh ∈ Ran" by (cases "Ran = {}", auto)
      define RanT where "RanT = Ran - {fresh}" 
      have "card RanT = card Ran - 1" using fresh finR unfolding RanT_def by auto
      with main have main: "card DomT ≤ card RanT" by auto
      from finR have finRT: "finite RanT" unfolding RanT_def by auto
      from card_le_inj[OF finD finRT main]
      obtain h where h: "h ∈ DomT → RanT" and hinj: "inj_on h DomT" by auto
      define g where "g y = (if y ∈ DomT then h y else fresh)" for y
      have gRan: "g ∈ Dom → Ran" unfolding g_def using fresh h RanT_def by auto
      have gInj: "inj_on g DomT" unfolding g_def using hinj by (auto simp: inj_on_def)
      {
        fix y
        assume "y ∈ Dom - DomT" 
        hence "g y = fresh" unfolding g_def by auto
        hence "g y ∉ RanT" unfolding RanT_def by auto
        hence "g y ∉ g ` DomT" using h unfolding g_def by auto
      }
      with gRan gInj have "∃ g. g ∈ Dom → Ran ∧ inj_on g DomT ∧ (∀ y ∈ Dom - DomT. g y ∉ g ` DomT)" 
        by blast
    }
    then obtain δ where δRan: "δ ∈ Dom → Ran" 
      and inj: "inj_on δ DomT"
      and inj': "y ∈ Dom - DomT ⟹ δ y ∉ δ ` DomT" for y
      by blast


    {
      fix y
      assume "y ∈ Dom" 
      hence "Var y ∈ ?TX" unfolding DomT_def Dom_def by auto
      from TX[OF this] have "snd y = ι"
        by (simp add: hastype_restrict)
    } note Dom = this

    define σ' where "σ' x = (if x ∈ Dom then δ x else σ x)" for x


    {
      fix s
      assume s: "s ∈ ?T" and cond: "is_Fun s ∨ the_Var s ∉ Dom" 
      have "s ⋅ σ' = s ⋅ σ" 
      proof (intro term_subst_eq)
        fix y
        assume y: "y ∈ vars s"
        show "σ' y = σ y" using cond
        proof (cases s)
          case (Fun f ts)
          with y have "s ⊳ Var y" by fastforce
          then obtain c where c: "c ≠ Hole" and sc: "s = c ⟨ Var y ⟩" by blast
          from T[OF s] have s: "s : ι in 𝒯(C,𝒱 |` SS)" .
          with σ have sσ: "s ⋅ σ : ι in 𝒯(C)" by (rule subst_hastype)
          have "y ∉ Dom" 
          proof
            assume "y ∈ Dom" 
            hence "Var y ∈ ?TX" unfolding Dom_def DomT_def by auto
            from TX[OF this]
            have "Var y : ι in 𝒯(C,𝒱 |` SS) " .
            hence σy: "σ y : ι in 𝒯(C)" using σ
              by (simp add: sorted_mapD)
            obtain t1 d t2 where id: "t1 = s ⋅ σ" "d = c ⋅⇩c σ" "t2 = σ y" by auto
            from sc have eq: "t1 = d ⟨ t2 ⟩" 
              by (simp add: id)
            from σy sσ have t1: "t1 : ι in 𝒯(C)" "t2 : ι in 𝒯(C)" by (auto simp: id)
            from c have dh: "d ≠ Hole" by (cases c, auto simp: id)
            from dh have size: "size (d ⟨ t ⟩) > size t" for t by (rule size_ne_ctxt)
            define stack where "stack i = ((λ t. d ⟨t⟩) ^^ i) t2" for i
            from t1[unfolded eq]
            have d: "d : ι → ι in 𝒞(C,λx. None)" by (rule apply_ctxt_hastype_imp_hastype_context)
            {
              fix i
              have "stack i : ι in 𝒯(C) ∧ size (stack i) ≥ i" 
              proof (induct i)
                case 0
                thus ?case by (simp add: stack_def t1)
              next
                case (Suc i)
                have "stack (Suc i) = d ⟨stack i⟩" unfolding stack_def by simp
                with Suc d size[of "stack i"] show ?case by (auto intro: hastype_context_apply)
              qed
            } note stack = this
            have inf: "infinite (range stack)" 
            proof
              assume "finite (range stack)" 
              hence "finite (size ` range stack)" by auto
              then obtain n where "⋀ i. size (stack i) ≤ n"
                by (meson UNIV_I finite_nat_set_iff_bounded_le image_eqI)
              from this[of "Suc n"] stack[of "Suc n"] show False by auto
            qed
            from stack have "range stack ⊆ {t . t : ι in 𝒯(C)}" by auto
            with inf have "infinite {t. t : ι in 𝒯(C)}" by (metis infinite_super)
            with finι
            show False unfolding finite_sort_def by blast
          qed
          thus "σ' y = σ y" unfolding σ'_def by auto
        next
          case (Var y)
          with cond y show ?thesis unfolding σ'_def by auto
        qed
      qed
    } note σ'σ = this

    {
      fix x
      assume "x ∈ Dom" 
      with δRan have "δ x ∈ Ran" by auto
      from this[unfolded Ran_def]
      have "δ x ∈ {t. t : ι in 𝒯(C)} - Avoid" .
    } note δ = this

    from Dom δ σ have σ': "σ' :⇩s 𝒱 |` SS → 𝒯(C)" 
      unfolding σ'_def sorted_map_def restrict_map_def by (auto split: if_splits)
    from comp[unfolded simple_pat_complete_def, rule_format, OF this]
    obtain mp' where mp: "mp' ∈ ?p'" and comp: "simple_match_complete_wrt σ' mp'" 
      by auto

    from mp show ?case
    proof
      assume mp': "mp' ∈ p" 
      have "simple_match_complete_wrt σ' mp' = simple_match_complete_wrt σ mp'" 
        unfolding simple_match_complete_wrt_def
      proof (intro ball_cong refl)
        fix eqc
        assume eqc: "eqc ∈ mp'" 
        {
          fix s
          assume s: "s ∈ eqc" 
          define V where "V = tvars_spat p" 
          have "s ⋅ σ = s ⋅ σ'" 
          proof (rule term_subst_eq)
            fix y
            assume "y ∈ vars s" 
            with eqc s mp' have "y ∈ tvars_spat p" by auto
            with vars have "Var y ∉ ?TX" unfolding V_def[symmetric] by fastforce
            hence "y ∉ Dom" unfolding Dom_def DomT_def by auto
            thus "σ y = σ' y" unfolding σ'_def by auto
          qed
        }
        thus "UNIQ_subst σ' eqc = UNIQ_subst σ eqc" unfolding UNIQ_subst_alt_def by auto
      qed
      with comp show ?thesis using mp' by auto
    next
      assume "mp' ∈ mp ` {0..n}" 
      then obtain i where "mp' = mp i" and i: "i ∈ {0..n}" by auto
      with comp[unfolded simple_match_complete_wrt_def] cond[of i]
      have "UNIQ_subst σ' (eq i)" by auto
      from this[unfolded UNIQ_subst_alt_def] cond[of i] i
      have eq: "σ' (x i) = t i ⋅ σ'" by auto
      from cond[of i] i have diff: "Var (x i) ≠ t i" by auto
      from i have xi: "x i ∈ Dom" unfolding Dom_def by auto
      have False
      proof (cases "t i")
        case (Var y)
        with eq diff have eq: "σ' (x i) = σ' y" and diff: "x i ≠ y" by auto
        from Var i have x: "x i ∈ Dom" and y: "y ∈ DomT" "y ∈ Dom" unfolding Dom_def DomT_def by auto
        with eq have eq: "δ (x i) = δ y" unfolding σ'_def by auto
        show False
        proof (cases "x i ∈ DomT")
          case True
          with inj eq diff y show False by (auto simp: inj_on_def)
        next
          case False
          hence "x i ∈ Dom - DomT" using x by auto
          from inj'[OF this] eq y show False by auto
        qed
      next
        case Fun
        have "σ' (x i) = δ (x i)" using xi by (auto simp: σ'_def)
        with δ[OF xi] have xi: "σ' (x i) ∉ Avoid" by auto
        from σ'σ[of "t i"] Fun i have "t i ⋅ σ' = t i ⋅ σ" by auto
        hence "t i ⋅ σ' ∈ Avoid" unfolding Avoid_def using i Fun by fastforce
        with eq xi show False by simp
      qed
      thus ?thesis ..
    qed
  qed
qed

end

end