Theory Pattern_Completeness_Set

section ‹Pattern Completeness›

text ‹Pattern-completeness is the question whether in a given program all terms
  of the form f(c1,..,cn) are matched by some lhs of the program,
  where here each ci is a constructor ground term and f is a defined symbol.
  This will be represented as a pattern problem of the shape 
  (f(x1,...xn), {lhs1, ..., lhsn}) where the xi will represent arbitrary constructor terms.›

section ‹A Set-Based Inference System to Decide Pattern Completeness›

text ‹This theory contains an algorithm to decide whether pattern problems are complete.
  It represents the inference rules of the paper on the set-based level.

  On this level we prove partial correctness and preservation of well-formed inputs,
  but not termination.›

theory Pattern_Completeness_Set
  imports
    First_Order_Terms.Term_More
    Complete_Non_Orders.Complete_Relations
    Sorted_Terms.Sorted_Contexts
    Compute_Nonempty_Infinite_Sorts
begin

lemmas type_conversion = hastype_in_Term_empty_imp_subst

lemma ball_insert_un_cong: "f y = Ball zs f ⟹ Ball (insert y A) f = Ball (zs ∪ A) f"
  by auto

lemma bex_insert_cong: "f y = f z ⟹ Bex (insert y A) f = Bex (insert z A) f"
  by auto

lemma not_bdd_above_natD: 
  assumes "¬ bdd_above (A :: nat set)"
  shows "∃ x ∈ A. x > n" 
  using assms by (meson bdd_above.unfold linorder_le_cases order.strict_iff)

lemma list_eq_nth_eq: "xs = ys ⟷ length xs = length ys ∧ (∀ i < length ys. xs ! i = ys ! i)"
  using nth_equalityI by metis

lemma subt_size: "p ∈ poss t ⟹ size (t |_ p) ≤ size t"
proof (induct p arbitrary: t)
  case (Cons i p t)
  thus ?case 
  proof (cases t)
    case (Fun f ss)
    from Cons Fun have i: "i < length ss" and sub: "t |_ (i # p) = (ss ! i) |_ p" 
      and "p ∈ poss (ss ! i)" by auto
    with Cons(1)[OF this(3)]
    have "size (t |_ (i # p)) ≤ size (ss ! i)" by auto
    also have "… ≤ size t" using i unfolding Fun by (simp add: termination_simp)
    finally show ?thesis .
  qed auto
qed auto

lemma removeAll_remdups: "removeAll x (remdups ys) = remdups (removeAll x ys)"
  by (simp add: remdups_filter removeAll_filter_not_eq)

lemma removeAll_eq_Nil_iff: "removeAll x ys = [] ⟷ (∀y ∈ set ys. y = x)"
  by (induction ys, auto)

lemma concat_removeAll_Nil: "concat (removeAll [] xss) = concat xss"
  by (induction xss, auto)

lemma removeAll_eq_imp_concat_eq:
  assumes "removeAll [] xss = removeAll [] xss'"
  shows "concat xss = concat xss'"
  apply (subst (1 2) concat_removeAll_Nil[symmetric])
  by (simp add: assms)

lemma map_remdups_commute:
  assumes "inj_on f (set xs)"
  shows "map f (remdups xs) = remdups (map f xs)"
  using assms by (induction xs, auto)

lemma Uniq_False: "∃⇩≤⇩1 a. False" by (auto intro!: Uniq_I)

abbreviation "UNIQ A ≡ ∃⇩≤⇩1 a. a ∈ A"

lemma Uniq_eq_the_elem:
  assumes "UNIQ A" and "a ∈ A" shows "a = the_elem A"
  using the1_equality'[OF assms]
  by (metis assms empty_iff is_singletonI' is_singleton_some_elem
      some_elem_nonempty the1_equality' the_elem_eq)

lemma bij_betw_imp_Uniq_iff:
  assumes "bij_betw f A B" shows "UNIQ A ⟷ UNIQ B"
  using assms[THEN bij_betw_imp_surj_on]
  apply (auto simp: Uniq_def)
  by (metis assms bij_betw_def imageI inv_into_f_eq)

lemma image_Uniq: "UNIQ A ⟹ UNIQ (f ` A)"
  by (smt (verit) Uniq_I image_iff the1_equality')

lemma successively_eq_iff_Uniq: "successively (=) xs ⟷ UNIQ (set xs)" (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r"
    apply (induction xs rule: induct_list012)
    by (auto intro: Uniq_I)
  show "?r ⟹ ?l"
  proof (induction xs)
    case Nil
    then show ?case by simp
  next
    case xxs: (Cons x xs)
    show ?case
    proof (cases xs)
      case Nil
      then show ?thesis by simp
    next
      case xs: (Cons y ys)
      have "successively (=) xs"
        apply (rule xxs(1)) using xxs(2) by (simp add: Uniq_def)
      with xxs(2)
      show ?thesis by (auto simp: xs Uniq_def)
    qed
  qed
qed

subsection ‹Defining Pattern Completeness›

text ‹
  We first consider matching problems, which are set of matching atoms.
  Each matching atom is a pair of terms: matchee and pattern.
  Matchee and pattern may have different type of variables: 
  Matchees use natural numbers (annotated with sorts) as variables, 
  so that it is easy to generate new variables,
  whereas patterns allow arbitrary variables of type ‹'v› without any further information.
  Then pattern problems are sets of matching problems, and we also have sets of pattern problems.

  The suffix ‹_set› is used to indicate that here these problems are modeled via sets.›

abbreviation tvars :: "nat × 's ⇀ 's" ("𝒱") where "𝒱 ≡ sort_annotated"

type_synonym ('f,'v,'s)match_atom = "('f,nat × 's)term × ('f,'v)term"
type_synonym ('f,'v,'s)match_problem_set = "('f,'v,'s) match_atom set" 
type_synonym ('f,'v,'s)pat_problem_set = "('f,'v,'s)match_problem_set set" 
type_synonym ('f,'v,'s)pats_problem_set = "('f,'v,'s)pat_problem_set set" 

abbreviation (input) bottom :: "('f,'v,'s)pats_problem_set" where "bottom ≡ {{}}"

definition tvars_match :: "('f,'v,'s)match_problem_set ⇒ (nat × 's) set" where
  "tvars_match mp = (⋃(t,l) ∈ mp. vars t)"

definition tvars_pat :: "('f,'v,'s)pat_problem_set ⇒ (nat × 's) set" where
  "tvars_pat pp = (⋃mp ∈ pp. tvars_match mp)"

definition tvars_pats :: "('f,'v,'s)pats_problem_set ⇒ (nat × 's) set" where
  "tvars_pats P = (⋃pp ∈ P. tvars_pat pp)"

definition subst_left :: "('f,nat × 's)subst ⇒ (('f,nat × 's)term × ('f,'v)term) ⇒ (('f,nat × 's)term × ('f,'v)term)" where
  "subst_left τ = (λ(t,r). (t ⋅ τ, r))"

text ‹A definition of pattern completeness for pattern problems.›

definition match_complete_wrt :: "('f,nat × 's,'w)gsubst ⇒ ('f,'v,'s)match_problem_set ⇒ bool" where
  "match_complete_wrt σ mp = (∃ μ. ∀ (t,l) ∈ mp. t ⋅ σ = l ⋅ μ)" 

lemma match_complete_wrt_cong:
  assumes s: "⋀x. x ∈ tvars_match mp ⟹ σ x = σ' x"
    and mp: "mp = mp'"
  shows "match_complete_wrt σ mp = match_complete_wrt σ' mp'"
  apply (unfold match_complete_wrt_def Ball_Pair_conv mp[symmetric])
  apply (intro ex_cong1 all_cong1 imp_cong[OF refl])
proof-
  fix μ t l assume "(t,l) ∈ mp"
  with s have "∀x ∈ vars t. σ x = σ' x" by (auto simp: tvars_match_def)
  from subst_same_vars[OF this] show "t⋅σ = l⋅μ ⟷ t⋅σ' = l⋅μ" by simp
qed

lemma match_complete_wrt_imp_o:
  assumes "match_complete_wrt σ mp" shows "match_complete_wrt (σ ∘⇩s τ) mp"
proof (unfold match_complete_wrt_def)
  from assms[unfolded match_complete_wrt_def] obtain μ where eq: "∀(t,l) ∈ mp. t⋅σ = l⋅μ"
    by auto
  { fix t l
    assume tl: "(t,l) ∈ mp"
    with eq have "t⋅(σ ∘⇩s τ) = l⋅(μ ∘⇩s τ)" by auto
  }
  then show "∃μ'. ∀(t,l) ∈ mp. t⋅(σ ∘⇩s τ) = l⋅μ'" by blast
qed

lemma match_complete_wrt_o_imp:
  assumes s: "σ :⇩s 𝒱 |` tvars_match mp → 𝒯(C,∅)" and m: "match_complete_wrt (σ ∘⇩s τ) mp"
  shows "match_complete_wrt σ mp"
proof (unfold match_complete_wrt_def)
  from m[unfolded match_complete_wrt_def] obtain μ where eq: "∀(t,l) ∈ mp. t⋅σ⋅τ = l⋅μ"
    by auto
  have "∀x ∈ tvars_match mp. σ x : snd x in 𝒯(C,∅)"
    by (auto intro!: sorted_mapD[OF s] simp: hastype_restrict)
  then have g: "x ∈ tvars_match mp ⟹ ground (σ x)" for x
    by (auto simp: hatype_imp_ground)
  { fix t l
    assume tl: "(t,l) ∈ mp"
    then have "ground (t⋅σ)" by (force intro!: g simp: tvars_match_def)
    then have "t⋅σ⋅τ⋅undefined = t⋅σ" by (metis eval_subst ground_subst_apply)
    with tl eq have "t⋅σ = l⋅(μ ∘⇩s undefined)" by auto
  }
  then show "∃μ'. ∀(t,l) ∈ mp. t⋅σ = l⋅μ'" by blast
qed

text ‹Pattern completeness is match completeness w.r.t. any constructor-ground substitution.
  Note that variables to instantiate are represented as pairs of (number, sort).›

definition pat_complete :: "('f,'s) ssig ⇒ ('f,'v,'s)pat_problem_set ⇒ bool" where
  "pat_complete C pp ⟷ (∀σ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C). ∃ mp ∈ pp. match_complete_wrt σ mp)"

lemma pat_completeD:
  assumes pp: "pat_complete C pp"
    and s: "σ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C,∅)"
  shows "∃ mp ∈ pp. match_complete_wrt σ mp"
proof -
  from s have "σ ∘⇩s undefined :⇩s 𝒱 |` tvars_pat pp → 𝒯(C)"
    by (simp add: subst_compose_sorted_map)
  from pp[unfolded pat_complete_def, rule_format, OF this]
  obtain mp where mp: "mp ∈ pp"
    and m: "match_complete_wrt (σ ∘⇩s undefined :: _ ⇒ (_,unit) term) mp" 
    by auto
  have "σ :⇩s 𝒱 |` tvars_match mp → 𝒯(C,∅)"
    apply (rule sorted_map_cmono[OF s])
    using mp
    by (auto simp: tvars_pat_def intro!: restrict_map_mono_right)
  from match_complete_wrt_o_imp[OF this m] mp
  show ?thesis by auto
qed

lemma pat_completeI:
  assumes r: "∀σ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C,∅::'v⇀'s). ∃ mp ∈ pp. match_complete_wrt σ mp"
  shows "pat_complete C pp"
proof (unfold pat_complete_def, safe)
  fix σ assume s: "σ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C)"
  then have "σ ∘⇩s undefined :⇩s 𝒱 |` tvars_pat pp → 𝒯(C,∅)"
    by (simp add: subst_compose_sorted_map)
  from r[rule_format, OF this]
  obtain mp where mp: "mp ∈ pp" and m: "match_complete_wrt (σ ∘⇩s undefined::_⇒(_,'v) term) mp" 
    by auto
  have "σ :⇩s 𝒱 |` tvars_match mp → 𝒯(C)"
    apply (rule sorted_map_cmono[OF s restrict_map_mono_right])
    using mp by (auto simp: tvars_pat_def)
  from match_complete_wrt_o_imp[OF this m] mp
  show "Bex pp (match_complete_wrt σ)" by auto
qed

lemma tvars_pat_empty[simp]: "tvars_pat {} = {}"
  by (simp add: tvars_pat_def)

lemma pat_complete_empty[simp]: "pat_complete C {} = False" 
  unfolding pat_complete_def by simp

abbreviation pats_complete :: "('f,'s) ssig ⇒ ('f,'v,'s)pats_problem_set ⇒ bool" where
  "pats_complete C P ≡ ∀pp ∈ P. pat_complete C pp"
(*  "pats_complete C P ≡ ∀σ :⇩s 𝒱 |` tvars_pats P → 𝒯(C). ∀pp ∈ P. ∃ mp ∈ pp. match_complete_wrt σ mp"
*)

subsection ‹Definition of Algorithm -- Inference Rules›

text ‹A function to compute for a variable $x$ all substitution that instantiate
  $x$ by $c(x_n, ..., x_{n+a})$ where $c$ is a constructor of arity $a$ and $n$ is a parameter that
  determines from where to start the numbering of variables.›

definition τc :: "nat ⇒ nat × 's ⇒ 'f × 's list ⇒ ('f,nat × 's)subst" where 
  "τc n x = (λ(f,ss). subst x (Fun f (map Var (zip [n ..< n + length ss] ss))))"

text ‹Compute the list of conflicting variables (Some list), or detect a clash (None)›
fun conflicts :: "('f,'v×'s)term ⇒ ('f,'v×'s)term ⇒ ('v×'s) list option" where 
  "conflicts (Var x) (Var y) = (if x = y then Some [] else
   if snd x = snd y then Some [x,y] else None)"
| "conflicts (Var x) (Fun _ _) = (Some [x])"
| "conflicts (Fun _ _) (Var x) = (Some [x])" 
| "conflicts (Fun f ss) (Fun g ts) = (if (f,length ss) = (g,length ts)
     then map_option concat (those (map2 conflicts ss ts))
    else None)" 

abbreviation "Conflict_Var s t x ≡ conflicts s t ≠ None ∧ x ∈ set (the (conflicts s t))" 
abbreviation "Conflict_Clash s t ≡ conflicts s t = None" 

lemma conflicts_sym: "rel_option (λ xs ys. set xs = set ys) (conflicts s t) (conflicts t s)" (is "rel_option _ (?c s t) _")
proof (induct s t rule: conflicts.induct)
  case (4 f ss g ts)
  define c where "c = ?c" 
  show ?case
  proof (cases "(f,length ss) = (g,length ts)")
    case True
    hence len: "length ss = length ts" 
      "((f, length ss) = (g, length ts)) = True"
      "((g, length ts) = (f, length ss)) = True" by auto
    show ?thesis using len(1) 4[OF True _ refl]
      unfolding conflicts.simps len(2,3) if_True
      unfolding option.rel_map c_def[symmetric] set_concat
    proof (induct ss ts rule: list_induct2, goal_cases)
      case (2 s ss t ts)
      hence IH: "rel_option (λx y. ⋃ (set ` set x) = ⋃ (set ` set y)) (those (map2 c ss ts)) (those (map2 c ts ss))" by auto
      from 2 have st: "rel_option (λxs ys. set xs = set ys) (c s t) (c t s)" by auto
      from IH st show ?case by (cases "c s t"; cases "c t s"; auto simp: option.rel_map)
        (simp add: option.rel_sel)
    qed simp
  qed auto
qed auto


lemma conflicts:
  shows "Conflict_Clash s t ⟹
    ∃ p. p ∈ poss s ∧ p ∈ poss t ∧
    (is_Fun (s |_p) ∧ is_Fun (t |_p) ∧ root (s |_p) ≠ root (t |_ p) ∨
    (∃x y. s |_p = Var x ∧ t |_p = Var y ∧ snd x ≠ snd y))"
    (is "?B1 ⟹ ?B2")
    and "Conflict_Var s t x ⟹
    ∃ p . p ∈ poss s ∧ p ∈ poss t ∧ s |_p ≠ t |_p ∧
    (s |_p = Var x ∨ t |_p = Var x)"
    (is "?C1 x ⟹ ?C2 x")
    and "s ≠ t ⟹ ∃ x. Conflict_Clash s t ∨ Conflict_Var s t x" 
    and "Conflict_Var s t x ⟹ x ∈ vars s ∪ vars t" 
    and "conflicts s t = Some [] ⟷ s = t" (is ?A)
proof -
  let ?B = "?B1 ⟶ ?B2" 
  let ?C = "λ x. ?C1 x ⟶ ?C2 x" 
  {
    fix x
    have "(conflicts s t = Some [] ⟶ s = t) ∧ ?B ∧ ?C x"
    proof (induction s arbitrary: t)
      case (Var y t)
      thus ?case by (cases t, cases y, auto)
    next
      case (Fun f ss t)
      show ?case 
      proof (cases t)
        case t: (Fun g ts)
        show ?thesis
        proof (cases "(f,length ss) = (g,length ts)")
          case False
          hence res: "conflicts (Fun f ss) t = None" unfolding t by auto
          show ?thesis unfolding res unfolding t using False
            by (auto intro!: exI[of _ Nil])
        next
          case f: True
          let ?s = "Fun f ss" 
          show ?thesis 
          proof (cases "those (map2 conflicts ss ts)")
            case None
            hence res: "conflicts ?s t = None" unfolding t by auto
            from None[unfolded those_eq_None] obtain i where i: "i < length ss" "i < length ts" and 
              confl: "conflicts (ss ! i) (ts ! i) = None"
              using f unfolding set_conv_nth set_zip by auto
            from i have "ss ! i ∈ set ss" by auto
            from Fun.IH[OF this, of "ts ! i"] confl obtain p 
              where p: "p ∈ poss (ss ! i) ∧ p ∈ poss (ts ! i) ∧
(is_Fun (ss ! i |_ p) ∧ is_Fun (ts ! i |_ p) ∧ root (ss ! i |_ p) ≠ root (ts ! i |_ p) ∨
(∃x y. ss!i |_ p = Var x ∧ ts!i |_ p = Var y ∧ snd x ≠ snd y))" 
              by force
            from p have p: "∃ p. p ∈ poss ?s ∧ p ∈ poss t ∧
(is_Fun (?s |_ p) ∧ is_Fun (t |_ p) ∧ root (?s |_ p) ≠ root (t |_ p) ∨
(∃x y. ?s |_ p = Var x ∧ t |_ p = Var y ∧ snd x ≠ snd y))" 
              by (intro exI[of _ "i # p"], unfold t, insert i f, auto)
            from p res show ?thesis by auto
          next
            case (Some xss)
            hence res: "conflicts ?s t = Some (concat xss)" unfolding t using f by auto
            from Some have map2: "map2 conflicts ss ts = map Some xss" by auto
            from arg_cong[OF this, of length] have len: "length xss = length ss" using f by auto
            have rec: "i < length ss ⟹ conflicts (ss ! i) (ts ! i) = Some (xss ! i)" for i 
              using arg_cong[OF map2, of "λ xs. xs ! i"] len f by auto
            {
              assume "x ∈ set (the (conflicts ?s t))" 
              hence "x ∈ set (concat xss)" unfolding res by auto
              then obtain xs where xs: "xs ∈ set xss" and x: "x ∈ set xs" by auto
              from xs len obtain i where i: "i < length ss" and xs: "xs = xss ! i" by (auto simp: set_conv_nth)
              from i have "ss ! i ∈ set ss" by auto
              from Fun.IH[OF this, of "ts ! i", unfolded rec[OF i, folded xs]] x
              obtain p where "p ∈ poss (ss ! i) ∧ p ∈ poss (ts ! i) ∧ ss ! i |_ p ≠ ts ! i |_ p ∧ (ss ! i |_ p = Var x ∨ ts ! i |_ p = Var x)" 
                by auto
              hence "∃ p. p ∈ poss ?s ∧ p ∈ poss t ∧ ?s |_ p ≠ t |_ p ∧ (?s |_ p = Var x ∨ t |_ p = Var x)" 
                by (intro exI[of _ "i # p"], insert i f, auto simp: t)
            }
            moreover
            {
              assume "conflicts ?s t = Some []" 
              with res have empty: "concat xss = []" by auto
              {
                fix i
                assume i: "i < length ss" 
                from rec[OF i] have "conflicts (ss ! i) (ts ! i) = Some (xss ! i)" .
                moreover from empty i len have "xss ! i = []" by auto
                ultimately have res: "conflicts (ss ! i) (ts ! i) = Some []" by simp
                from i have "ss ! i ∈ set ss" by auto
                from Fun.IH[OF this, of "ts ! i", unfolded res] have "ss ! i = ts ! i" by auto
              }
              with f have "?s = t" unfolding t by (auto intro: nth_equalityI)
            }
            ultimately show ?thesis unfolding res by auto
          qed
        qed
      qed auto
    qed
  } note main = this
  from main show B: "?B1 ⟹ ?B2" and C: "?C1 x ⟹ ?C2 x" by blast+
  show ?A
  proof
    assume "s = t" 
    with B have "conflicts s t ≠ None" by force
    then obtain xs where res: "conflicts s t = Some xs" by auto     
    show "conflicts s t = Some []" 
    proof (cases xs)
      case Nil 
      thus ?thesis using res by auto
    next
      case (Cons x xs)
      with main[of x] res ‹s = t› show ?thesis by auto
    qed
  qed (insert main, blast)
  {
    assume diff: "s ≠ t" 
    show "∃ x. Conflict_Clash s t ∨ Conflict_Var s t x" 
    proof (cases "conflicts s t")
      case (Some xs)
      with ‹?A› diff obtain x where "x ∈ set xs" by (cases xs, auto)
      thus ?thesis unfolding Some
        apply auto
        by (metis surj_pair)
    qed auto
  }
  assume "Conflict_Var s t x" 
  with C obtain p where "p ∈ poss s" "p ∈ poss t" "(s |_ p = Var x ∨ t |_ p = Var x)" 
    by blast
  thus "x ∈ vars s ∪ vars t" 
    by (metis UnCI subt_at_imp_supteq' subteq_Var_imp_in_vars_term)
qed

declare conflicts.simps[simp del] 

lemma conflicts_refl[simp]: "conflicts t t = Some []" 
  using conflicts(5)[of t t] by auto

locale pattern_completeness_context =
  fixes S :: "'s set" ― ‹set of sort-names›
    and C :: "('f,'s)ssig" ― ‹sorted signature›
    and m :: nat ― ‹upper bound on arities of constructors›
    and Cl :: "'s ⇒ ('f × 's list)list" ― ‹a function to compute all constructors of given sort as list› 
    and inf_sort :: "'s ⇒ bool" ― ‹a function to indicate whether a sort is infinite›
    and cd_sort :: "'s ⇒ nat" ― ‹a function to compute finite cardinality of a sort›
    and improved :: bool ― ‹if improved = False, then FSCD-version of algorithm is used;
                             if improved = True, the better journal version (under development) is used.›
begin

definition tvars_disj_pp :: "nat set ⇒ ('f,'v,'s)pat_problem_set ⇒ bool" where
  "tvars_disj_pp V p = (∀ mp ∈ p. ∀ (ti,pi) ∈ mp. fst ` vars ti ∩ V = {})" 

definition lvars_disj_mp :: "'v list ⇒ ('f,'v,'s)match_problem_set ⇒ bool" where
  "lvars_disj_mp ys mp = (⋃ (vars ` snd ` mp) ∩ set ys = {} ∧ distinct ys)" 

definition inf_var_conflict :: "('f,'v,'s)match_problem_set ⇒ bool" where
  "inf_var_conflict mp = (∃ s t x y. 
    (s,Var x) ∈ mp ∧ (t,Var x) ∈ mp ∧ Conflict_Var s t y ∧ inf_sort (snd y))" 

definition subst_match_problem_set :: "('f,nat × 's)subst ⇒ ('f,'v,'s)match_problem_set ⇒ ('f,'v,'s)match_problem_set" where
  "subst_match_problem_set τ mp = subst_left τ ` mp" 

definition subst_pat_problem_set :: "('f,nat × 's)subst ⇒ ('f,'v,'s)pat_problem_set ⇒ ('f,'v,'s)pat_problem_set" where
  "subst_pat_problem_set τ pp = subst_match_problem_set τ ` pp"

definition τs :: "nat ⇒ nat × 's ⇒ ('f,nat × 's)subst set" where 
  "τs n x = {τc n x (f,ss) | f ss. f : ss → snd x in C}" 

text ‹The transformation rules of the paper.

The formal definition contains two deviations from the rules in the paper: first, the instantiate-rule
can always be applied; and second there is an identity rule, which will simplify later refinement 
proofs. Both of the deviations cause non-termination.

The formal inference rules further separate those rules that deliver a bottom- or top-element from
the ones that deliver a transformed problem.›
inductive mp_step :: "('f,'v,'s)match_problem_set ⇒ ('f,'v,'s)match_problem_set ⇒ bool"
(infix ‹→⇩s› 50) where
  mp_decompose: "length ts = length ls ⟹ insert (Fun f ts, Fun f ls) mp →⇩s set (zip ts ls) ∪ mp"
| mp_match: "x ∉ ⋃ (vars ` snd ` mp) ⟹ insert (t, Var x) mp →⇩s mp" 
| mp_identity: "mp →⇩s mp"
| mp_decompose': "mp ∪ mp' →⇩s (⋃ (t, l) ∈ mp. set (zip (args t) (map Var ys))) ∪ mp'" 
if "⋀ t l. (t,l) ∈ mp ⟹ l = Var y ∧ root t = Some (f,n)" 
   "⋀ t l. (t,l) ∈ mp' ⟹ y ∉ vars l"
   "lvars_disj_mp ys (mp ∪ mp')" "length ys = n" (* ys = n fresh vars *) 
   improved (* decompose' is not available in FSCD version *)

inductive mp_fail :: "('f,'v,'s)match_problem_set ⇒ bool" where
  mp_clash: "(f,length ts) ≠ (g,length ls) ⟹ mp_fail (insert (Fun f ts, Fun g ls) mp)" 
| mp_clash': "Conflict_Clash s t ⟹ mp_fail ({(s,Var x),(t, Var x)} ∪ mp)"
| mp_clash_sort: "𝒯(C,𝒱) s ≠ 𝒯(C,𝒱) t ⟹ mp_fail ({(s,Var x),(t, Var x)} ∪ mp)"

inductive pp_step :: "('f,'v,'s)pat_problem_set ⇒ ('f,'v,'s)pat_problem_set ⇒ bool"
(infix ‹⇒⇩s› 50) where
  pp_simp_mp: "mp →⇩s mp' ⟹ insert mp pp ⇒⇩s insert mp' pp" 
| pp_remove_mp: "mp_fail mp ⟹ insert mp pp ⇒⇩s pp"
| pp_inf_var_conflict: "pp ∪ pp' ⇒⇩s pp'" 
  if "Ball pp inf_var_conflict" 
    "finite pp" 
    "Ball (tvars_pat pp') (λ x. ¬ inf_sort (snd x))" 
    "¬ improved ⟹ pp' = {}" (* no pp' allowed in FSCD algorithm *)

text ‹Note that in @{thm[source] pp_inf_var_conflict} the conflicts have to be simultaneously occurring. 
  If just some matching problem has such a conflict, then this cannot be deleted immediately!

  Example-program: f(x,x) = ..., f(s(x),y) = ..., f(x,s(y)) = ... cover all cases of natural numbers,
    i.e., f(x1,x2), but if one would immediately delete the matching problem of the first lhs
    because of the resulting @{const inf_var_conflict} in {(x1,x),(x2,x)} then it is no longer complete.›


inductive pp_success :: "('f,'v,'s)pat_problem_set ⇒ bool" where
  "pp_success (insert {} pp)" 

inductive P_step_set :: "('f,'v,'s)pats_problem_set ⇒ ('f,'v,'s)pats_problem_set ⇒ bool"
(infix ‹⇛⇩s› 50) where
  P_fail: "insert {} P ⇛⇩s bottom"
| P_simp: "pp ⇒⇩s pp' ⟹ insert pp P ⇛⇩s insert pp' P"
| P_remove_pp: "pp_success pp ⟹ insert pp P ⇛⇩s P"
| P_instantiate: "tvars_disj_pp {n ..< n+m} pp ⟹ x ∈ tvars_pat pp ⟹
    insert pp P ⇛⇩s {subst_pat_problem_set τ pp |. τ ∈ τs n x} ∪ P"


subsection ‹Soundness of the inference rules›

text ‹Well-formed matching and pattern problems: all occurring variables 
  (in left-hand sides of matching problems) have a known sort.›
definition wf_match :: "('f,'v,'s)match_problem_set ⇒ bool" where
  "wf_match mp = (snd ` tvars_match mp ⊆ S)" 

lemma wf_match_iff: "wf_match mp ⟷ (∀(x,ι) ∈ tvars_match mp. ι ∈ S)"
  by (auto simp: wf_match_def)

lemma tvars_match_subst: "tvars_match (subst_match_problem_set σ mp) = (⋃(t,l) ∈ mp. vars (t⋅σ))"
  by (auto simp: tvars_match_def subst_match_problem_set_def subst_left_def)

lemma wf_match_subst:
  assumes s: "σ :⇩s 𝒱 |` tvars_match mp → 𝒯(C',{x : ι in 𝒱. ι ∈ S})"
  shows "wf_match (subst_match_problem_set σ mp)"
  apply (unfold wf_match_iff tvars_match_subst)
proof (safe)
  fix t l x ι assume tl: "(t,l) ∈ mp" and xt: "(x,ι) ∈ vars (t⋅σ)"
  from xt obtain y κ where y: "(y,κ) ∈ vars t" and xy: "(x,ι) ∈ vars (σ (y,κ))" by (auto simp: vars_term_subst)
  from tl y have "(y,κ) : κ in 𝒱 |` tvars_match mp" by (auto simp: hastype_restrict tvars_match_def)
  from sorted_mapD[OF s this]
  have "σ (y,κ) : κ in 𝒯(C',{x : ι in 𝒱. ι ∈ S})".
  from hastype_in_Term_imp_vars[OF this xy]
  have "(x,ι) : ι in {x : ι in 𝒱. ι ∈ S}" by (auto elim!: in_dom_hastypeE)
  then show "ι ∈ S" by auto
qed

definition wf_pat :: "('f,'v,'s)pat_problem_set ⇒ bool" where
  "wf_pat pp = (∀mp ∈ pp. wf_match mp)"

lemma wf_pat_subst:
  assumes s: "σ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C',{x : ι in 𝒱. ι ∈ S})"
  shows "wf_pat (subst_pat_problem_set σ pp)"
  apply (unfold wf_pat_def subst_pat_problem_set_def)
proof safe
  fix mp assume mp: "mp ∈ pp"
  show "wf_match (subst_match_problem_set σ mp)"
    apply (rule wf_match_subst)
    apply (rule sorted_map_cmono[OF s])
    apply (rule restrict_map_mono_right) using mp by (auto simp: tvars_pat_def)
qed

definition wf_pats :: "('f,'v,'s)pats_problem_set ⇒ bool" where
  "wf_pats P = (∀pp ∈ P. wf_pat pp)"

lemma wf_pat_iff: "wf_pat pp ⟷ (∀(x,ι) ∈ tvars_pat pp. ι ∈ S)"
  by (auto simp: wf_pat_def tvars_pat_def wf_match_iff)

text ‹The reduction of match problems preserves completeness.›

lemma mp_step_pcorrect: "mp →⇩s mp' ⟹ match_complete_wrt σ mp = match_complete_wrt σ mp'" 
proof (induct mp mp' rule: mp_step.induct)
  case *: (mp_decompose f ts ls mp)
  show ?case unfolding match_complete_wrt_def
    apply (rule ex_cong1)
    apply (rule ball_insert_un_cong)
    apply (unfold split) using * by (auto simp add: set_zip list_eq_nth_eq)
next
  case *: (mp_match x mp t)
  show ?case unfolding match_complete_wrt_def
  proof 
    assume "∃μ. ∀(ti, li)∈mp. ti ⋅ σ = li ⋅ μ" 
    then obtain μ where eq: "⋀ ti li. (ti, li)∈mp ⟹  ti ⋅ σ = li ⋅ μ" by auto
    let ?μ = "μ(x := t ⋅ σ)" 
    have "(ti, li) ∈ mp ⟹ ti ⋅ σ = li ⋅ ?μ" for ti li using * eq[of ti li]
      by (auto intro!: term_subst_eq)
    thus "∃μ. ∀(ti, li)∈insert (t, Var x) mp. ti ⋅ σ = li ⋅ μ" by (intro exI[of _ ?μ], auto)
  qed auto
next
  case *: (mp_decompose' mp y f n mp' ys)
  note * = *[unfolded lvars_disj_mp_def]
  let ?mpi = "(⋃(t, l)∈mp. set (zip (args t) (map Var ys)))" 
  let ?y = "Var y" 
  show ?case
  proof
    assume "match_complete_wrt σ (?mpi ∪ mp')" 
    from this[unfolded match_complete_wrt_def] obtain μ
      where match: "⋀ t l. (t,l) ∈ ?mpi ⟹ t ⋅ σ = l ⋅ μ" 
        and match': "⋀ t l. (t,l) ∈ mp' ⟹ t ⋅ σ = l ⋅ μ" by force
    let ?μ = "μ( y := Fun f (map μ ys))" 
    show "match_complete_wrt σ (mp ∪ mp')" unfolding match_complete_wrt_def
    proof (intro exI[of _ ?μ] ballI, elim UnE; clarify)
      fix t l
      {
        assume "(t,l) ∈ mp'" 
        from match'[OF this] *(2)[OF this]
        show "t ⋅ σ = l ⋅ ?μ" by (auto intro: term_subst_eq)
      }
      assume tl: "(t,l) ∈ mp"
      from *(1)[OF this] obtain ts where l: "l = Var y" and t: "t = Fun f ts"  
        and lts: "length ts = n" by (cases t, auto)
      {
        fix ti yi
        assume "(ti,yi) ∈ set (zip ts ys)" 
        hence "(ti, Var yi) ∈ set (zip (args t) (map Var ys))" 
          using t lts ‹length ys = n› by (force simp: set_conv_nth)
        hence "(ti, Var yi) ∈ ?mpi" using tl by blast
        from match[OF this] have "μ yi = ti ⋅ σ" by simp
      } note yi = this
      show "t ⋅ σ = l ⋅ ?μ" unfolding l t using yi lts ‹length ys = n› 
        by (force intro!: nth_equalityI simp: set_zip)
    qed
  next
    assume "match_complete_wrt σ (mp ∪ mp')" 
    from this[unfolded match_complete_wrt_def]
    obtain μ where match: "⋀ t l. (t,l) ∈ mp ⟹ t ⋅ σ = l ⋅ μ"
      and match': "⋀ t l. (t,l) ∈ mp' ⟹ t ⋅ σ = l ⋅ μ" by force
    define μ' where "μ' = (λ x. case map_of (zip ys (args (μ y))) x of 
      None ⇒ μ x | Some Ti ⇒ Ti)"
    show "match_complete_wrt σ (?mpi ∪ mp')" 
      unfolding match_complete_wrt_def
    proof (intro exI[of _ μ'] ballI, elim UnE; clarify)
      fix t l
      assume tl: "(t,l) ∈ mp'" 
      from *(3) tl have vars: "vars l ∩ set ys = {}" by force
      hence "map_of (zip ys (args (μ y))) x = None" if "x ∈ vars l" for x
        using that by (meson disjoint_iff map_of_SomeD option.exhaust set_zip_leftD)
      with match'[OF tl] 
      show "t ⋅ σ = l ⋅ μ'" by (auto intro!: term_subst_eq simp: μ'_def)
    next
      fix t l ti and vyi :: "('f,_)term" 
      assume tl: "(t,l) ∈ mp"   
        and i: "(ti,vyi) ∈ set (zip (args t) (map Var ys))" 
      from *(1)[OF tl] obtain ts where l: "l = Var y" and t: "t = Fun f ts"  
        and lts: "length ts = n" by (cases t, auto)
      from i lts obtain i where i: "i < n" and ti: "ti = ts ! i" and yi: "vyi = Var (ys ! i)" 
        unfolding set_zip using ‹length ys = n› t by auto
      from match[OF tl] have mu_y: "μ y = Fun f ts ⋅ σ" unfolding l t by auto
      have yi: "vyi ⋅ μ' = args (μ y) ! i" unfolding μ'_def yi
        using i lts ‹length ys = n› *(3) mu_y 
        by (force split: option.splits simp: set_zip distinct_conv_nth)
      also have "… = ti ⋅ σ" unfolding mu_y ti using i lts by auto
      finally show "ti ⋅ σ = vyi ⋅ μ'" ..
    qed
  qed
qed auto

lemma mp_fail_pcorrect1:
  assumes "mp_fail mp" "σ :⇩s sort_annotated |` tvars_match mp → 𝒯(C,X)"
  shows "¬ match_complete_wrt σ mp"
  using assms
proof (induct mp rule: mp_fail.induct)
  case *: (mp_clash f ts g ls mp)
  {
    assume "length ts ≠ length ls" 
    hence "(map (λt. t ⋅ μ) ls = map (λt. t ⋅ σ) ts) = False" for σ :: "('f,nat × 's,'a)gsubst" and μ
      by (metis length_map)
  } note len = this
  from * show ?case unfolding match_complete_wrt_def
    apply (auto simp: len split: prod.splits)
    using map_eq_imp_length_eq by force
next
  case *: (mp_clash' s t x mp)
  from conflicts(1)[OF *(1)]
  obtain po where po: "po ∈ poss s" "po ∈ poss t"
    and disj: "is_Fun (s |_ po) ∧ is_Fun (t |_ po) ∧ root (s |_ po) ≠ root (t |_ po) ∨
    (∃x y. s |_ po = Var x ∧ t |_ po = Var y ∧ snd x ≠ snd y)" 
    by auto
  show ?case 
  proof 
    assume "match_complete_wrt σ ({(s, Var x), (t, Var x)} ∪ mp)"
    from this[unfolded match_complete_wrt_def]
    have eq: "s ⋅ σ |_po = t ⋅ σ |_po" by auto
    from disj
    show False
    proof (elim disjE conjE exE)
      assume *: "is_Fun (s |_ po)" "is_Fun (t |_ po)" "root (s |_ po) ≠ root (t |_ po)"
      from eq have "root (s ⋅ σ |_po) = root (t ⋅ σ |_po)" by auto
      also have "root (s ⋅ σ |_po) = root (s |_po ⋅ σ)" using po by auto
      also have "… = root (s |_po)" using * by (cases "s |_ po", auto)
      also have "root (t ⋅ σ |_po) = root (t |_po ⋅ σ)" using po by (cases "t |_ po", auto)
      also have "… = root (t |_po)" using * by (cases "t |_ po", auto)
      finally show False using * by auto
    next
      fix y z assume y: "s |_ po = Var y" and z: "t |_ po = Var z" and ty: "snd y ≠ snd z"
      from y z eq po have yz: "σ y = σ z" by auto
      have "y ∈ vars_term s" "z ∈ vars_term t"
        using po[THEN vars_term_subt_at] y z by auto
      then
      have "σ y : snd y in 𝒯(C,X)" "σ z : snd z in 𝒯(C,X)"
        by (auto intro!: *(2)[THEN sorted_mapD] simp: hastype_restrict tvars_match_def)
      with ty yz show False by (auto simp: has_same_type)
    qed
  qed
next
  case *: (mp_clash_sort s t x mp)
  show ?case
  proof
    assume "match_complete_wrt σ ({(s, Var x), (t, Var x)} ∪ mp)"
    from this[unfolded match_complete_wrt_def]
    have eq: "s ⋅ σ = t ⋅ σ" by auto
    define V where "V = tvars_match ({(s, Var x), (t, Var x)} ∪ mp)" 
    from *(2) have σ: "σ :⇩s 𝒱 |` V → 𝒯(C,X)" unfolding V_def .
    have vars: "vars s ∪ vars t ⊆ V" unfolding V_def tvars_match_def by auto
    show False
    proof (cases "None ∈ {𝒯(C,𝒱) s, 𝒯(C,𝒱) t}")
      case False
      from False obtain σs σt where st: "s : σs in 𝒯(C,𝒱)" "t : σt in 𝒯(C,𝒱)" 
        by (cases "𝒯(C,𝒱) s"; cases "𝒯(C,𝒱) t"; auto simp: hastype_def)
      from st(1) vars σ have "(s ⋅ σ) : σs in  𝒯(C,X)" 
        by (meson le_supE restrict_map_mono_right sorted_algebra.eval_has_same_type_vars sorted_map_cmono
            term.sorted_algebra_axioms)
      moreover from st(2) vars σ have "(t ⋅ σ) : σt in  𝒯(C,X)" 
        by (meson le_supE restrict_map_mono_right sorted_algebra.eval_has_same_type_vars sorted_map_cmono
            term.sorted_algebra_axioms)
      ultimately have "σs = σt" unfolding eq hastype_def by auto
      with st *(1) show False by (auto simp: hastype_def)
    next
      case True
      have "∃ s σs. vars s ⊆ V ∧ s ⋅ σ : σs in 𝒯(C,X) ∧ 𝒯(C,𝒱) s = None" 
      proof (cases "𝒯(C,𝒱) s")
        case None
        with *(1) obtain σt where "t : σt in 𝒯(C,𝒱)" by (cases "𝒯(C,𝒱) t"; force simp: hastype_def)
        from this vars σ have "(t ⋅ σ) : σt in  𝒯(C,X)" 
          by (meson le_supE restrict_map_mono_right sorted_algebra.eval_has_same_type_vars sorted_map_cmono
            term.sorted_algebra_axioms)
        from this[folded eq] None vars show ?thesis by auto
      next
        case (Some σs)
        with True have None: "𝒯(C,𝒱) t = None" and Some: "s : σs in 𝒯(C,𝒱)" by (auto simp: hastype_def)
        from Some vars σ have "(s ⋅ σ) : σs in  𝒯(C,X)" 
          by (meson le_supE restrict_map_mono_right sorted_algebra.eval_has_same_type_vars sorted_map_cmono
            term.sorted_algebra_axioms)
        from this[unfolded eq] None vars show ?thesis by auto
      qed
      then obtain s σs where "vars s ⊆ V" "s ⋅ σ: σs in 𝒯(C,X)" "𝒯(C,𝒱) s = None" by auto
      thus False
      proof (induct s arbitrary: σs)
        case (Fun f ss τ)
        hence mem: "Fun f (map (λs. s ⋅ σ) ss) : τ in 𝒯(C,X)" by auto
        from this[unfolded Fun_hastype]  
        obtain τs where f: "f : τs → τ in C" and args: "map (λs. s ⋅ σ) ss :⇩l τs in 𝒯(C,X)" by auto
        {
          fix s 
          assume "s ∈ set ss" 
          hence "s ⋅ σ ∈ set (map (λs. s ⋅ σ) ss)" by auto
          hence "∃ τ. s ⋅ σ : τ in 𝒯(C,X)"
            by (metis Fun_in_dom_imp_arg_in_dom mem hastype_imp_dom in_dom_hastypeE)
        } note arg = this
        show ?case
        proof (cases "∃ s ∈ set ss. 𝒯(C,𝒱) s = None") 
          case True
          then obtain s where s: "s ∈ set ss" and None: "𝒯(C,𝒱) s = None" by auto
          from arg[OF s] obtain τ where Some: "s ⋅ σ : τ in 𝒯(C,X) " by auto
          from Fun(1)[OF s _ Some None] s Fun(2) show False by auto
        next
          case False
          have "Fun f ss : τ in 𝒯(C,𝒱)" 
          proof (intro Fun_hastypeI[OF f], unfold list_all2_conv_all_nth, intro conjI allI impI)
            show "length ss = length τs" using args[unfolded list_all2_conv_all_nth] by auto
            fix i
            assume i: "i < length ss" 
            hence ssi: "ss ! i ∈ set ss" by auto
            with False obtain τi where type: "ss ! i : τi in 𝒯(C,𝒱)" by (auto simp: hastype_def)
            from ssi Fun(2) have vars: "vars (ss ! i) ⊆ V" by auto
            from vars type σ have "ss ! i ⋅ σ : τi in 𝒯(C,X)"
              by (meson restrict_map_mono_right sorted_map_cmono term.eval_has_same_type_vars)
            moreover from args i have "ss ! i ⋅ σ : τs ! i in 𝒯(C,X)"
              unfolding list_all2_conv_all_nth by auto
            ultimately have "τi = τs ! i" by (auto simp: hastype_def)
            with type show "ss ! i : τs ! i in 𝒯(C,𝒱)" by auto
          qed
          with Fun(4) show False unfolding hastype_def using not_None_eq by blast
        qed 
      qed auto
    qed
  qed
qed

lemma mp_fail_pcorrect:
  assumes f: "mp_fail mp" and s: "σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)" and wf: "wf_match mp"
  shows "¬ match_complete_wrt σ mp"
  apply (rule mp_fail_pcorrect1[OF f])
  apply (rule sorted_map_cmono[OF s])
  using wf by (auto intro!: subssetI simp: hastype_restrict wf_match_iff)

end

text ‹For proving partial correctness we need further properties of the fixed parameters:
   We assume that ‹m› is sufficiently large and that there exists some constructor ground terms.
   Moreover ‹inf_sort› really computes whether a sort has terms of arbitrary size.
   Further all symbols in ‹C› must have sorts of ‹S›.
   Finally, ‹Cl› should precisely compute the constructors of a sort.›

locale pattern_completeness_context_with_assms = pattern_completeness_context S C m Cl inf_sort cd_sort
  for S and C :: "('f,'s)ssig" 
    and m Cl inf_sort cd_sort +
  assumes not_empty_sort: "⋀ s. s ∈ S ⟹ ¬ empty_sort C s"
    and C_sub_S: "⋀ f ss s. f : ss → s in C ⟹ insert s (set ss) ⊆ S"
    and m: "⋀ f ss s. f : ss → s in C ⟹ length ss ≤ m"
    and finite_C: "finite (dom C)"
    and inf_sort: "⋀s. s ∈ S ⟹ inf_sort s ⟷ ¬ finite_sort C s"
    and Cl: "⋀ s. set (Cl s) = {(f,ss). f : ss → s in C}"
    and Cl_len: "⋀ σ. Ball (length ` snd ` set (Cl σ)) (λ a. a ≤ m)"
    and cd: "⋀s. s ∈ S ⟹ cd_sort s = card_of_sort C s"
begin

lemma sorts_non_empty: "s ∈ S ⟹ ∃ t. t : s in 𝒯(C,∅)"
  apply (drule not_empty_sort)
  by (auto elim: not_empty_sortE)

lemma inf_sort_not_bdd: "s ∈ S ⟹ ¬ bdd_above (size ` {t . t : s in 𝒯(C,∅)}) ⟷ inf_sort s"
  apply (subst finite_sig_bdd_above_iff_finite[OF finite_C])
  by (auto simp: inf_sort finite_sort)

lemma C_nth_S: "f : ss → s in C ⟹ i < length ss ⟹ ss!i ∈ S"
  using C_sub_S by force

lemmas subst_defs_set = 
  subst_pat_problem_set_def
  subst_match_problem_set_def

text ‹Preservation of well-formedness›

lemma mp_step_wf: "mp →⇩s mp' ⟹ wf_match mp ⟹ wf_match mp'" 
  unfolding wf_match_def tvars_match_def
proof (induct mp mp' rule: mp_step.induct)
  case (mp_decompose f ts ls mp)
  then show ?case by (auto dest!: set_zip_leftD)
next 
  case *: (mp_decompose' mp y f n mp' ys)
  from *(1) *(6)  
  show ?case 
    apply (auto dest!: set_zip_leftD) 
    subgoal for _ _ t by (cases t; force)
    subgoal for _ _ t by (cases t; force)
    done
qed auto

lemma pp_step_wf: "pp ⇒⇩s pp' ⟹ wf_pat pp ⟹ wf_pat pp'" 
  unfolding wf_pat_def
proof (induct pp pp' rule: pp_step.induct)
  case (pp_simp_mp mp mp' pp)
  then show ?case using mp_step_wf[of mp mp'] by auto
qed auto

theorem P_step_set_wf: "P ⇛⇩s P' ⟹ wf_pats P ⟹ wf_pats P'" 
  unfolding wf_pats_def
proof (induct P P' rule: P_step_set.induct)
  case (P_simp pp pp' P)
  then show ?case using pp_step_wf[of pp pp'] by auto
next
  case *: (P_instantiate n p x P)
  let ?s = "snd x" 
  from * have sS: "?s ∈ S" and p: "wf_pat p" unfolding wf_pat_def wf_match_def tvars_pat_def by auto
  {
    fix τ
    assume tau: "τ ∈ τs n x" 
    from tau[unfolded τs_def τc_def, simplified]
    obtain f sorts where f: "f : sorts → snd x in C" and τ: "τ = subst x (Fun f (map Var (zip [n..<n + length sorts] sorts)))" by auto
    let ?i = "length sorts" 
    let ?xs = "zip [n..<n + length sorts] sorts" 
    from C_sub_S[OF f] have sS: "?s ∈ S" and xs: "snd ` set ?xs ⊆ S" 
      unfolding set_conv_nth set_zip by auto
    {
      fix mp y
      assume mp: "mp ∈ p"  and "y ∈ tvars_match (subst_left τ ` mp)"
      then obtain s t where y: "y ∈ vars (s ⋅ τ)" and st: "(s,t) ∈ mp" 
        unfolding tvars_match_def subst_left_def by auto
      from y have "y ∈ vars s ∪ set ?xs" unfolding vars_term_subst τ
        by (auto simp: subst_def split: if_splits)
      hence "snd y ∈ snd ` vars s ∪ snd ` set ?xs" by auto
      also have "… ⊆ snd ` vars s ∪ S" using xs by auto
      also have "… ⊆ S" using p mp st
        unfolding wf_pat_def wf_match_def tvars_match_def by force
      finally have "snd y ∈ S" .
    }
    hence "wf_pat (subst_pat_problem_set τ p)" 
      unfolding wf_pat_def wf_match_def subst_defs_set by auto
  }
  with * show ?case by auto
qed (auto simp: wf_pat_def)


text ‹Soundness requires some preparations›

definition σg :: "nat×'s ⇒ ('f,'v) term" where
  "σg x = (SOME t. t : snd x in 𝒯(C,∅))"

lemma σg: "σg :⇩s {x : ι in sort_annotated. ι ∈ S} → 𝒯(C,∅)"
  using sorts_non_empty[THEN someI_ex]
  by (auto intro!: sorted_mapI simp: σg_def)

lemma wf_pat_complete_iff:
  assumes "wf_pat pp"
  shows "pat_complete C pp ⟷ (∀σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C). ∃ mp ∈ pp. match_complete_wrt σ mp)"
  (is "?l ⟷ ?r")
proof
  assume l: ?l
  show ?r
  proof (intro allI impI)
    fix σ :: "nat × 's ⇒ _"
    assume s: "σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)"
    have "σ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C)"
      apply (rule sorted_map_cmono[OF s])
      using assms by (auto intro!: subssetI simp: hastype_restrict wf_pat_iff)
    from pat_completeD[OF l this] show "∃mp∈pp. match_complete_wrt σ mp".
  qed
next
  assume r: ?r
  show ?l
  proof (unfold pat_complete_def, safe)
    fix σ assume s: "σ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C)"
    define σ' where "σ' x ≡ if x ∈ tvars_pat pp then σ x else σg x" for x
    have "σ' :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)"
      by (auto intro!: sorted_mapI sorted_mapD[OF s] sorted_mapD[OF σg] simp: σ'_def hastype_restrict)
    from r[rule_format, OF this]
    obtain mp where mp: "mp ∈ pp" and m: "match_complete_wrt σ' mp" by auto
    have [simp]: "x ∈ tvars_match mp ⟹ σ x = σ' x" for x using mp by (auto simp: σ'_def tvars_pat_def)
    from m have "match_complete_wrt σ mp" by (simp cong: match_complete_wrt_cong)
    with mp show "Bex pp (match_complete_wrt σ)" by auto
  qed
qed

lemma wf_pats_complete_iff:
  assumes wf: "wf_pats P"
  shows "pats_complete C P ⟷
  (∀σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C). ∀pp ∈ P. ∃mp ∈ pp. match_complete_wrt σ mp)"
    (is "?l ⟷ ?r")
proof safe
  fix σ pp assume s: "σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)" and pp: "pp ∈ P"
  have s2: "σ :⇩s 𝒱 |` tvars_pats P → 𝒯(C)"
    apply (rule sorted_map_cmono[OF s])
    using wf
    by (auto intro!: subssetI simp: hastype_restrict wf_pats_def wf_pat_iff tvars_pats_def
        split: prod.splits)
  assume ?l
  with pp have comp: "pat_complete C pp" by auto
  from wf pp have "wf_pat pp" by (auto simp: wf_pats_def)
  from comp[unfolded wf_pat_complete_iff[OF this], rule_format, OF s]
  show "∃mp ∈ pp. match_complete_wrt σ mp".
next
  fix pp assume pp: "pp ∈ P"
  assume r[rule_format]: ?r
  from wf pp have "wf_pat pp" by (auto simp: wf_pats_def)
  note * = wf_pat_complete_iff[OF this]
  show "pat_complete C pp"
    apply (unfold *) using r[OF _ pp] by auto
qed

lemma inf_var_conflictD: assumes "inf_var_conflict mp" 
  shows "∃ p s t x y. 
    (s,Var x) ∈ mp ∧ (t,Var x) ∈ mp ∧ s |_p = Var y ∧ s |_ p ≠ t |_p ∧
   p ∈ poss s ∧ p ∈ poss t ∧ inf_sort (snd y)" 
proof -
  from assms[unfolded inf_var_conflict_def]
  obtain s t x y where "(s, Var x) ∈ mp ∧ (t, Var x) ∈ mp" and conf: "Conflict_Var s t y" and y: "inf_sort (snd y)" by blast
  with conflicts(2)[OF conf] show ?thesis by metis
qed

lemmas cg_term_vars = hastype_in_Term_empty_imp_vars

text ‹Main partial correctness theorems on well-formed problems: the transformation rules do
  not change the semantics of a problem›

lemma pp_step_pcorrect:
  "pp ⇒⇩s pp' ⟹ wf_pat pp ⟹ pat_complete C pp = pat_complete C pp'" 
proof (induct pp pp' rule: pp_step.induct)
  case *: (pp_simp_mp mp mp' pp)
  with mp_step_wf[OF *(1)]
  have "wf_pat (insert mp' pp)" by (auto simp: wf_pat_def)
  with *(2) mp_step_pcorrect[OF *(1)]
  show ?case by (auto simp: wf_pat_complete_iff)
next
  case *: (pp_remove_mp mp pp)
  from mp_fail_pcorrect[OF *(1)] *(2)
  show ?case by (auto simp: wf_pat_complete_iff wf_pat_def)
next
  case *: (pp_inf_var_conflict pp pp')
  note wf = ‹wf_pat (pp ∪ pp')› and fin = ‹finite pp›
  hence "wf_pat pp" and wfpp': "wf_pat pp'" by (auto simp: wf_pat_def)
  with wf have easy: "pat_complete C pp' ⟹ pat_complete C (pp ∪ pp')"
    by (auto simp: wf_pat_complete_iff)
  {
    assume pp: "pat_complete C (pp ∪ pp')" 
    have "pat_complete C pp'" unfolding wf_pat_complete_iff[OF wfpp']
    proof (intro allI impI)
      fix δ
      assume δ: "δ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)" 
      define conv :: "('f,unit) term ⇒ ('f, nat × 's) term" where "conv t = t ⋅ undefined" for t
      define conv' :: "('f, nat × 's) term ⇒ ('f, unit) term" where "conv' t = t ⋅ undefined" for t
      define confl' :: "('f, nat × 's) term ⇒ ('f, nat × 's)term ⇒ nat × 's ⇒ bool" where "confl' = (λ sp tp y. 
           sp = Var y ∧ inf_sort (snd y) ∧ sp ≠ tp)" 
      define P1 where "P1 = (λ mp s t x y p. mp ∈ pp ⟶ (s, Var x) ∈ mp ∧ (t, Var x) ∈ mp ∧ p ∈ poss s ∧ p ∈ poss t ∧ confl' (s |_ p) (t |_ p) y)" 
      {
        fix mp
        assume "mp ∈ pp" 
        hence "inf_var_conflict mp" using * by auto
        from inf_var_conflictD[OF this] 
        have "∃ s t x y p. P1 mp s t x y p" unfolding P1_def confl'_def by force
      }
      hence "∀ mp. ∃ s t x y p. P1 mp s t x y p" unfolding P1_def by blast
      from choice[OF this] obtain s where "∀ mp. ∃ t x y p. P1 mp (s mp) t x y p" by blast
      from choice[OF this] obtain t where "∀ mp. ∃ x y p. P1 mp (s mp) (t mp) x y p" by blast
      from choice[OF this] obtain x where "∀ mp. ∃ y p. P1 mp (s mp) (t mp) (x mp) y p" by blast
      from choice[OF this] obtain y where "∀ mp. ∃ p. P1 mp (s mp) (t mp) (x mp) (y mp) p" by blast
      from choice[OF this] obtain p where "∀ mp. P1 mp (s mp) (t mp) (x mp) (y mp) (p mp)" by blast
      note P1 = this[unfolded P1_def, rule_format]
      from *(2) have "finite (y ` pp)" by blast
      from ex_bij_betw_finite_nat[OF this] obtain index and n :: nat where 
        bij: "bij_betw index (y ` pp) {..<n}" 
        by (auto simp add: atLeast0LessThan)
      define var_ind :: "nat ⇒ nat × 's ⇒ bool" where
        "var_ind i x = (x ∈ y ` pp ∧ index x ∈ {..<n} - {..<i})" for i x
      have [simp]: "var_ind n x = False" for x
        unfolding var_ind_def by auto  
      define cg_subst_ind :: "nat ⇒ ('f,nat × 's)subst ⇒ bool" where
        "cg_subst_ind i σ = (∀ x. (var_ind i x ⟶ σ x = Var x)
            ∧ (¬ var_ind i x ⟶ (vars_term (σ x) = {} ∧ (snd x ∈ S ⟶ σ x : snd x in 𝒯(C,∅))))
            ∧ (snd x ∈ S ⟶ ¬ inf_sort (snd x) ⟶ σ x = conv (δ x)))" for i σ
      define confl :: "nat ⇒ ('f, nat × 's) term ⇒ ('f, nat × 's)term ⇒ bool" where "confl = (λ i sp tp. 
           (case (sp,tp) of (Var x, Var y) ⇒ x ≠ y ∧ var_ind i x ∧ var_ind i y
           | (Var x, Fun _ _) ⇒ var_ind i x
           | (Fun _ _, Var x) ⇒ var_ind i x
           | (Fun f ss, Fun g ts) ⇒ (f,length ss) ≠ (g,length ts)))"
      have confl_n: "confl n s t ⟹ ∃ f g ss ts. s = Fun f ss ∧ t = Fun g ts ∧ (f,length ss) ≠ (g,length ts)" for s t
        by (cases s; cases t; auto simp: confl_def)
      {
        fix i x
        assume "var_ind i x" 
        from this[unfolded var_ind_def] obtain i 
          where z: "x ∈ y ` pp" "index x = i" by blast 
        from z obtain mp where "mp ∈ pp" and "index (y mp) = i" and "x = y mp" by auto
        with P1[OF this(1), unfolded confl'_def] have inf: "inf_sort (snd x)" by auto
      } note var_ind_inf = this
      {
        fix i
        assume "i ≤ n"
        hence "∃ σ. cg_subst_ind i σ ∧ (∀ mp ∈ pp. ∃ p. p ∈ poss (s mp ⋅ σ) ∧ p ∈ poss (t mp ⋅ σ) ∧ confl i (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p))" 
        proof (induction i)
          case 0
          define σ where "σ x = (if var_ind 0 x then Var x else if snd x ∈ S then conv (δ x) else Fun undefined [])" for x
          have σ: "cg_subst_ind 0 σ" unfolding cg_subst_ind_def
          proof (intro allI impI conjI)
            fix x
            show "var_ind 0 x ⟹ σ x = Var x" unfolding σ_def by auto
            show "¬ var_ind 0 x ⟹ vars (σ x) = {}" 
              unfolding σ_def conv_def using δ[THEN sorted_mapD, of x] 
              by (auto simp: vars_term_subst  hastype_in_Term_empty_imp_vars)
            show "¬ var_ind 0 x ⟹ snd x ∈ S ⟹ σ x : snd x in 𝒯(C,∅)" 
              using δ[THEN sorted_mapD, of x]
              unfolding σ_def conv_def by (auto simp: σ_def intro: type_conversion)
            show "snd x ∈ S ⟹ ¬ inf_sort (snd x) ⟹ σ x = conv (δ x)" 
              unfolding σ_def by (auto dest: var_ind_inf)
          qed            
          show ?case
          proof (rule exI, rule conjI[OF σ], intro ballI exI conjI)
            fix mp
            assume mp: "mp ∈ pp" 
            note P1 = P1[OF this]
            from mp have mem: "y mp ∈ y ` pp" by auto
            with bij have y: "index (y mp) ∈ {..<n}" by (metis bij_betw_apply)
            hence y0: "var_ind 0 (y mp)" using mem unfolding var_ind_def by auto
            show "p mp ∈ poss (s mp ⋅ σ)" using P1 by auto
            show "p mp ∈ poss (t mp ⋅ σ)" using P1 by auto
            let ?t = "t mp |_ p mp" 
            define c where "c = confl 0 (s mp ⋅ σ |_ p mp) (t mp ⋅ σ |_ p mp)" 
            have "c = confl 0 (s mp |_ p mp ⋅ σ) (?t ⋅ σ)" 
              using P1 unfolding c_def by auto
            also have s: "s mp |_ p mp = Var (y mp)" using P1 unfolding confl'_def by auto
            also have "… ⋅ σ = Var (y mp)" using y0 unfolding σ_def by auto
            also have "confl 0 (Var (y mp)) (?t ⋅ σ)" 
            proof (cases "?t ⋅ σ")
              case Fun
              thus ?thesis using y0 unfolding confl_def by auto
            next
              case (Var z)
              then obtain u where t: "?t = Var u" and ssig: "σ u = Var z" 
                by (cases ?t, auto)
              from P1[unfolded s] have "confl' (Var (y mp)) ?t (y mp)" by auto
              from this[unfolded confl'_def t] have uy: "y mp ≠ u" by auto
              show ?thesis
              proof (cases "var_ind 0 u")
                case True
                with y0 uy show ?thesis unfolding t σ_def confl_def by auto
              next
                case False
                with ssig[unfolded σ_def] have uS: "snd u ∈ S" and contra: "conv (δ u) = Var z" 
                  by (auto split: if_splits)
                from δ[THEN sorted_mapD, of u] uS contra
                have False by (cases "δ u", auto simp: conv_def)
                thus ?thesis ..
              qed
            qed
            finally show "confl 0 (s mp ⋅ σ |_ p mp) (t mp ⋅ σ |_ p mp)" unfolding c_def .
          qed
        next
          case (Suc i)
          then obtain σ where σ: "cg_subst_ind i σ" and confl: "(∀mp∈pp. ∃p. p ∈ poss (s mp ⋅ σ) ∧ p ∈ poss (t mp ⋅ σ) ∧ confl i (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p))" 
            by auto
          from Suc have "i ∈ {..< n}" and i: "i < n" by auto
          with bij obtain z where z: "z ∈ y ` pp" "index z = i" unfolding bij_betw_def by (metis imageE)
          {
            from z obtain mp where "mp ∈ pp" and "index (y mp) = i" and "z = y mp" by auto
            with P1[OF this(1), unfolded confl'_def] have inf: "inf_sort (snd z)" 
              and *: "p mp ∈ poss (s mp)" "s mp |_ p mp = Var z" "(s mp, Var (x mp)) ∈ mp"
              by auto
            from *(1,2) have "z ∈ vars (s mp)" using vars_term_subt_at by fastforce
            with *(3) have "z ∈ tvars_match mp" unfolding tvars_match_def by force
            with ‹mp ∈ pp› wf have "snd z ∈ S" unfolding wf_pat_def wf_match_def by auto
            from not_bdd_above_natD[OF inf_sort_not_bdd[OF this, THEN iffD2, OF inf]]
              sorts_non_empty[OF this]
            have "⋀ n. ∃ t. t : snd z in 𝒯(C,∅::nat×'s⇀_) ∧ n < size t" by auto
            note this inf
          } note z_inf = this
            (* define d as 1 + maximal size of all s- and t-terms in pp σ *)
          define all_st where "all_st = (λ mp. s mp ⋅ σ) ` pp ∪ (λ mp. t mp ⋅ σ) ` pp" 
          have fin_all_st: "finite all_st" unfolding all_st_def using *(2) by simp
          define d :: nat where "d = Suc (Max (size ` all_st))" 
          from z_inf(1)[of d]
          obtain u :: "('f,nat×'s) term"
            where u: "u : snd z in 𝒯(C,∅)" and du: "d ≤ size u" by auto
          have vars_u: "vars u = {}" by (rule cg_term_vars[OF u])
          define σ' where "σ' x = (if x = z then u else σ x)" for x
          have σ'_def': "σ' x = (if x ∈ y ` pp ∧ index x = i then u else σ x)" for x
            unfolding σ'_def by (rule if_cong, insert bij z, auto simp: bij_betw_def inj_on_def) 
          have var_ind_conv: "var_ind i x = (x = z ∨ var_ind (Suc i) x)" for x
          proof
            assume "x = z ∨ var_ind (Suc i) x" 
            thus "var_ind i x" using z i unfolding var_ind_def by auto
          next
            assume "var_ind i x" 
            hence x: "x ∈ y ` pp" "index x ∈ {..<n} - {..<i}" unfolding var_ind_def by auto
            with i have "index x = i ∨ index x ∈ {..<n} - {..<Suc i}" by auto
            thus "x = z ∨ var_ind (Suc i) x"
            proof
              assume "index x = i" 
              with x(1) z bij have "x = z" by (auto simp: bij_betw_def inj_on_def)
              thus ?thesis by auto
            qed (insert x, auto simp: var_ind_def)
          qed
          have [simp]: "var_ind i z" unfolding var_ind_conv by auto
          have [simp]: "var_ind (Suc i) z = False" unfolding var_ind_def using z by auto
          have σz[simp]: "σ z = Var z" using σ[unfolded cg_subst_ind_def, rule_format, of z] by auto
          have σ'_upd: "σ' = σ(z := u)" unfolding σ'_def by (intro ext, auto)
          have σ'_comp: "σ' = σ ∘⇩s Var(z := u)" unfolding subst_compose_def σ'_upd
          proof (intro ext)
            fix x
            show "(σ(z := u)) x = σ x ⋅ Var(z := u)" 
            proof (cases "x = z")
              case False
              hence "σ x ⋅ (Var(z := u)) = σ x ⋅ Var" 
              proof (intro term_subst_eq)
                fix y
                assume y: "y ∈ vars (σ x)" 
                show "(Var(z := u)) y = Var y" 
                proof (cases "var_ind i x")
                  case True
                  with σ[unfolded cg_subst_ind_def, rule_format, of x]
                  have "σ x = Var x" by auto
                  with False y show ?thesis by auto
                next
                  case False
                  with σ[unfolded cg_subst_ind_def, rule_format, of x]
                  have "vars (σ x) = {}" by auto
                  with y show ?thesis by auto
                qed
              qed
              thus ?thesis by auto
            qed simp
          qed
          have σ': "cg_subst_ind (Suc i) σ'" unfolding cg_subst_ind_def
          proof (intro allI conjI impI)
            fix x
            assume "var_ind (Suc i) x" 
            hence "var_ind i x" and diff: "index x ≠ i" unfolding var_ind_def by auto
            hence "σ x = Var x" using σ[unfolded cg_subst_ind_def] by blast
            thus "σ' x = Var x" unfolding σ'_def' using diff by auto
          next
            fix x
            assume "¬ var_ind (Suc i) x" and "snd x ∈ S" 
            thus "σ' x : snd x in 𝒯(C,∅)" 
              using σ[unfolded cg_subst_ind_def, rule_format, of x] u
              unfolding σ'_def var_ind_conv by auto
          next
            fix x
            assume "¬ var_ind (Suc i) x"  
            hence "x = z ∨ ¬ var_ind i x" unfolding var_ind_conv by auto
            thus "vars (σ' x) = {}" unfolding σ'_upd using σ[unfolded cg_subst_ind_def, rule_format, of x] vars_u by auto
          next
            fix x :: "nat × 's" 
            assume *: "snd x ∈ S" "¬ inf_sort (snd x)" 
            with z_inf(2) have "x ≠ z" by auto
            hence "σ' x = σ x" unfolding σ'_def by auto
            thus "σ' x = conv (δ x)" using σ[unfolded cg_subst_ind_def, rule_format, of x] * by auto
          qed
          show ?case
          proof (intro exI[of _ σ'] conjI σ' ballI)
            fix mp
            assume mp: "mp ∈ pp" 
            define s' where "s' = s mp ⋅ σ" 
            define t' where "t' = t mp ⋅ σ" 
            from confl[rule_format, OF mp]
            obtain p where p: "p ∈ poss s'" "p ∈ poss t'" and confl: "confl i (s' |_ p) (t' |_ p)" by (auto simp: s'_def t'_def)
            {
              fix s' t' :: "('f, nat × 's) term" and p f ss x
              assume *: "(s' |_ p, t' |_p) = (Fun f ss, Var x)" "var_ind i x" and p: "p ∈ poss s'" "p ∈ poss t'" 
                and range_all_st: "s' ∈ all_st" 
              hence s': "s' ⋅ Var(z := u) |_ p = Fun f ss ⋅ Var(z := u)" (is "_ = ?s")
                and t': "t' ⋅ Var(z := u) |_ p = (if x = z then u else Var x)" using p by auto
              from range_all_st[unfolded all_st_def] 
              have rangeσ: "∃ S. s' = S ⋅ σ" by auto
              define s where "s = ?s"
              have "∃p. p ∈ poss (s' ⋅ Var(z := u)) ∧ p ∈ poss (t' ⋅ Var(z := u)) ∧ confl (Suc i) (s' ⋅ Var(z := u) |_ p) (t' ⋅ Var(z := u) |_ p)" 
              proof (cases "x = z")
                case False
                thus ?thesis using * p unfolding s' t' by (intro exI[of _ p], auto simp: confl_def var_ind_conv)
              next
                case True
                hence t': "t' ⋅ Var(z := u) |_ p = u" unfolding t' by auto
                have "∃ p'. p' ∈ poss u ∧ p' ∈ poss s ∧ confl (Suc i) (s |_ p') (u |_ p')" 
                proof (cases "∃ x. x ∈ vars s ∧ var_ind (Suc i) x")
                  case True
                  then obtain x where xs: "x ∈ vars s" and x: "var_ind (Suc i) x" by auto
                  from xs obtain p' where p': "p' ∈ poss s" and sp: "s |_ p' = Var x" by (metis vars_term_poss_subt_at)
                  from p' sp vars_u show ?thesis 
                  proof (induct u arbitrary: p' s) 
                    case (Fun f us p' s)
                    show ?case
                    proof (cases s)
                      case (Var y)
                      with Fun have s: "s = Var x" by auto
                      with x show ?thesis by (intro exI[of _ Nil], auto simp: confl_def)
                    next
                      case s: (Fun g ss)
                      with Fun obtain j p where p: "p' = j # p" "j < length ss" "p ∈ poss (ss ! j)" "(ss ! j) |_ p = Var x" by auto
                      show ?thesis
                      proof (cases "(f,length us) = (g,length ss)")
                        case False
                        thus ?thesis by (intro exI[of _ Nil], auto simp: s confl_def)
                      next
                        case True
                        with p have j: "j < length us" by auto
                        hence usj: "us ! j ∈ set us" by auto
                        with Fun have "vars (us ! j) = {}" by auto
                        from Fun(1)[OF usj p(3,4) this] obtain p' where 
                          "p' ∈ poss (us ! j) ∧ p' ∈ poss (ss ! j) ∧ confl (Suc i) (ss ! j |_ p') (us ! j |_ p')" by auto
                        thus ?thesis using j p by (intro exI[of _ "j # p'"], auto simp: s)
                      qed
                    qed
                  qed auto
                next
                  case False
                  from * have fss: "Fun f ss = s' |_ p" by auto 
                  from rangeσ obtain S where sS: "s' = S ⋅ σ" by auto
                  from p have "vars (s' |_ p) ⊆ vars s'" by (metis vars_term_subt_at)
                  also have "… = (⋃y∈vars S. vars (σ y))" unfolding sS by (simp add: vars_term_subst)
                  also have "… ⊆ (⋃y∈vars S. Collect (var_ind i))" 
                  proof -
                    {
                      fix x y
                      assume "x ∈ vars (σ y)" 
                      hence "var_ind i x" 
                        using σ[unfolded cg_subst_ind_def, rule_format, of y] by auto
                    }
                    thus ?thesis by auto
                  qed
                  finally have sub: "vars (s' |_ p) ⊆ Collect (var_ind i)" by blast
                  have "vars s = vars (s' |_ p ⋅ Var(z := u))" unfolding s_def s' fss by auto 
                  also have "… = ⋃ (vars ` Var(z := u) ` vars (s' |_ p))" by (simp add: vars_term_subst) 
                  also have "… ⊆ ⋃ (vars ` Var(z := u) ` Collect (var_ind i))" using sub by auto
                  also have "… ⊆ Collect (var_ind (Suc i))" 
                    by (auto simp: vars_u var_ind_conv)
                  finally have vars_s: "vars s = {}" using False by auto
                      (* so u and s are ground terms; we will show that they differ and hence a 
                   clash must exist *)
                  {
                    assume "s = u" 
                    from this[unfolded s_def fss]
                    have eq: "s' |_ p ⋅ Var(z := u) = u" by auto
                    have False
                    proof (cases "z ∈ vars (s' |_ p)")
                      case True
                      have diff: "s' |_ p ≠ Var z" using * by auto 
                      from True obtain C where id: "s' |_ p = C ⟨ Var z ⟩" 
                        by (metis ctxt_supt_id vars_term_poss_subt_at)
                      with diff have diff: "C ≠ Hole" by (cases C, auto)
                      from eq[unfolded id, simplified] diff
                      obtain C where "C⟨u⟩ = u" and "C ≠ Hole" by (cases C; force)
                      from arg_cong[OF this(1), of size] this(2) show False 
                        by (simp add: less_not_refl2 size_ne_ctxt)
                    next
                      case False
                      have size: "size s' ∈ size ` all_st" using range_all_st by auto
                      from False have "s' |_ p ⋅ Var(z := u) = s' |_ p ⋅ Var" 
                        by (intro term_subst_eq, auto)
                      with eq have eq: "s' |_ p = u" by auto
                      hence "size u = size (s' |_ p)" by auto
                      also have "… ≤ size s'" using p(1) 
                        by (rule subt_size)
                      also have "… ≤ Max (size ` all_st)" 
                        using size fin_all_st by simp
                      also have "… < d" unfolding d_def by simp
                      also have "… ≤ size u" using du .
                      finally show False by simp
                    qed
                  }
                  hence "s ≠ u" by auto
                  with vars_s vars_u
                  show ?thesis 
                  proof (induct s arbitrary: u)
                    case s: (Fun f ss u)
                    then obtain g us where u: "u = Fun g us" by (cases u, auto)
                    show ?case
                    proof (cases "(f,length ss) = (g,length us)")
                      case False
                      thus ?thesis unfolding u by (intro exI[of _ Nil], auto simp: confl_def)
                    next
                      case True
                      with s(4)[unfolded u] have "∃ j < length us. ss ! j ≠ us ! j" 
                        by (auto simp: list_eq_nth_eq)
                      then obtain j where j: "j < length us" and diff: "ss ! j ≠ us ! j" by auto
                      from j True have mem: "ss ! j ∈ set ss" "us ! j ∈ set us" by auto
                      with s(2-) u have "vars (ss ! j) = {}" "vars (us ! j) = {}" by auto
                      from s(1)[OF mem(1) this diff] obtain p' where
                        "p' ∈ poss (us ! j) ∧ p' ∈ poss (ss ! j) ∧ confl (Suc i) (ss ! j |_ p') (us ! j |_ p')" 
                        by blast
                      thus ?thesis unfolding u using True j by (intro exI[of _ "j # p'"], auto)
                    qed
                  qed auto
                qed
                then obtain p' where p': "p' ∈ poss u" "p' ∈ poss s" and confl: "confl (Suc i) (s |_ p') (u |_ p')" by auto
                have s'': "s' ⋅ Var(z := u) |_ (p @ p') = s |_ p'" unfolding s_def s'[symmetric] using p p' by auto
                have t'': "t' ⋅ Var(z := u) |_ (p @ p') = u |_ p'" using t' p p' by auto
                show ?thesis 
                proof (intro exI[of _ "p @ p'"], unfold s'' t'', intro conjI confl)
                  have "p ∈ poss (s' ⋅ Var(z := u))" using p by auto
                  moreover have "p' ∈ poss ((s' ⋅ Var(z := u)) |_ p)" using s' p' p unfolding s_def by auto
                  ultimately show "p @ p' ∈ poss (s' ⋅ Var(z := u))" by simp
                  have "p ∈ poss (t' ⋅ Var(z := u))" using p by auto
                  moreover have "p' ∈ poss ((t' ⋅ Var(z := u)) |_ p)" using t' p' p by auto
                  ultimately show "p @ p' ∈ poss (t' ⋅ Var(z := u))" by simp
                qed
              qed
            } note main = this
            consider (FF) f g ss ts where "(s' |_ p, t' |_ p) = (Fun f ss, Fun g ts)" "(f,length ss) ≠ (g,length ts)" 
              | (FV) f ss x where "(s' |_ p, t' |_ p) = (Fun f ss, Var x)" "var_ind i x"
              | (VF) f ss x where "(s' |_ p, t' |_ p) = (Var x, Fun f ss)" "var_ind i x" 
              | (VV) x x' where "(s' |_ p, t' |_ p) = (Var x, Var x')" "x ≠ x'" "var_ind i x" "var_ind i x'" 
              using confl by (auto simp: confl_def split: term.splits)
            hence "∃p. p ∈ poss (s' ⋅ Var(z := u)) ∧ p ∈ poss (t' ⋅ Var(z := u)) ∧ confl (Suc i) (s' ⋅ Var(z := u) |_ p) (t' ⋅ Var(z := u) |_ p)" 
            proof cases
              case (FF f g ss ts)
              thus ?thesis using p by (intro exI[of _ p], auto simp: confl_def)
            next
              case (FV f ss x)
              have "s' ∈ all_st" unfolding s'_def using mp all_st_def by auto
              from main[OF FV p this] show ?thesis by auto
            next
              case (VF f ss x)
              have t': "t' ∈ all_st" unfolding t'_def using mp all_st_def by auto
              from VF have "(t' |_ p, s' |_ p) = (Fun f ss, Var x)" "var_ind i x" by auto
              from main[OF this p(2,1) t'] 
              obtain p where "p ∈ poss (t' ⋅ Var(z := u))" "p ∈ poss (s' ⋅ Var(z := u))" "confl (Suc i) (t' ⋅ Var(z := u) |_ p) (s' ⋅ Var(z := u) |_ p)"
                by auto
              thus ?thesis by (intro exI[of _ p], auto simp: confl_def split: term.splits)
            next
              case (VV x x')
              thus ?thesis using p vars_u by (intro exI[of _ p], cases u, auto simp: confl_def var_ind_conv)
            qed
            thus "∃p. p ∈ poss (s mp ⋅ σ') ∧ p ∈ poss (t mp ⋅ σ') ∧ confl (Suc i) (s mp ⋅ σ' |_ p) (t mp ⋅ σ' |_ p)" 
              unfolding σ'_comp subst_subst_compose s'_def t'_def by auto
          qed
        qed
      }
      from this[of n]
      obtain σ where σ: "cg_subst_ind n σ" and confl: "⋀ mp. mp ∈ pp ⟹ ∃p. p ∈ poss (s mp ⋅ σ) ∧ p ∈ poss (t mp ⋅ σ) ∧ confl n (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p)" 
        by blast
      define σ' :: "('f,nat × 's,unit)gsubst" where "σ' x = conv' (Var x)" for x
      let ?σ = "σ ∘⇩s σ'" 
      {
        fix x :: "nat × 's" 
        assume *: "snd x ∈ S" "¬ inf_sort (snd x)" 
        from δ[THEN sorted_mapD, of x] * have "δ x : snd x in 𝒯(C,∅)" by auto
        hence vars: "vars (δ x) = {}" by (simp add: hastype_in_Term_empty_imp_vars)
        from * σ[unfolded cg_subst_ind_def] have "σ x = conv (δ x)" by blast
        hence "?σ x = δ x ⋅ (undefined ∘⇩s σ')" by (simp add: subst_compose_def conv_def subst_subst)
        also have "… = δ x" by (rule ground_term_subst[OF vars]) 
        finally have "?σ x = δ x" .
      } note σδ = this
      have "?σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)"
      proof (intro sorted_mapI, unfold subst_compose_def hastype_in_restrict_sset conj_imp_eq_imp_imp)
        fix x :: "nat × 's" and ι
        assume "x : ι in 𝒱" and "ι ∈ S"
        then have "snd x = ι" "ι ∈ S" by auto
        with σ[unfolded cg_subst_ind_def, rule_format, of x]
        have "σ x : ι in 𝒯(C,∅)" by auto
        thus "σ x ⋅ σ' : ι in 𝒯(C,∅)" by (rule type_conversion)
      qed
      from pp[unfolded wf_pat_complete_iff[OF wf] match_complete_wrt_def, rule_format, OF this]
      obtain mp μ where mp: "mp ∈ pp ∪ pp'" and match: "⋀ ti li. (ti, li)∈ mp ⟹ ti ⋅ ?σ = li ⋅ μ" by force
      {
        assume mp: "mp ∈ pp" 
        from P1[OF this(1)] 
        have "(s mp, Var (x mp)) ∈ mp" "(t mp, Var (x mp)) ∈ mp" by auto
        from match[OF this(1)] match[OF this(2)] have ident: "s mp ⋅ ?σ = t mp ⋅ ?σ" by auto
        from confl[OF mp] obtain p 
          where p: "p ∈ poss (s mp ⋅ σ)" "p ∈ poss (t mp ⋅ σ)" and confl: "confl n (s mp ⋅ σ |_ p) (t mp ⋅ σ |_ p)" 
          by auto
        let ?s = "s mp ⋅ σ" let ?t = "t mp ⋅ σ" 
        from confl_n[OF confl] obtain f g ss ts where 
          confl: "?s |_p = Fun f ss" "?t |_p = Fun g ts" and diff: "(f,length ss) ≠ (g,length ts)" by auto
        define s' where "s' = s mp ⋅ σ" 
        define t' where "t' = t mp ⋅ σ" 
        from confl p ident 
        have False 
          unfolding subst_subst_compose s'_def[symmetric] t'_def[symmetric]
        proof (induction p arbitrary: s' t')
          case Nil
          then show ?case using diff by (auto simp: list_eq_nth_eq)
        next
          case (Cons i p s t)
          from Cons obtain h1 us1 where s: "s = Fun h1 us1" by (cases s, auto)
          from Cons obtain h2 us2 where t: "t = Fun h2 us2" by (cases t, auto)
          from Cons(2,4)[unfolded s] have si: "(us1 ! i) |_ p = Fun f ss" "p ∈ poss (us1 ! i)" and i1: "i < length us1" by auto
          from Cons(3,5)[unfolded t] have ti: "(us2 ! i) |_ p = Fun g ts" "p ∈ poss (us2 ! i)" and i2: "i < length us2" by auto
          from Cons(6)[unfolded s t] i1 i2 have " us1 ! i ⋅ σ' = us2 ! i ⋅ σ'" by (auto simp: list_eq_nth_eq)
          from Cons.IH[OF si(1) ti(1) si(2) ti(2) this]
          show False .
        qed
      }
      with mp have mp: "mp ∈ pp'" by auto
      show "Bex pp' (match_complete_wrt δ)" 
        unfolding match_complete_wrt_def
      proof (intro bexI[OF _ mp] exI[of _ μ] ballI, clarify)
        fix ti li
        assume tl: "(ti, li) ∈ mp" 
        have "ti ⋅ δ = ti ⋅ ?σ" 
        proof (intro term_subst_eq, rule sym, rule σδ)
          fix x
          assume x: "x ∈ vars ti"
          from *(3) x tl mp show "¬ inf_sort (snd x)" by (auto simp: tvars_pat_def tvars_match_def) 
          from *(5) x tl mp show "snd x ∈ S" 
            unfolding wf_pat_def wf_match_def tvars_match_def by auto
        qed
        also have "… = li ⋅ μ" using match[OF tl] .
        finally show "ti ⋅ δ = li ⋅ μ" .
      qed
    qed
  }
  with easy show ?case by auto
qed

lemma pp_success_pcorrect: "pp_success pp ⟹ pat_complete C pp" 
  by (induct pp rule: pp_success.induct, auto simp: pat_complete_def match_complete_wrt_def)

theorem P_step_set_pcorrect:
  "P ⇛⇩s P' ⟹ wf_pats P ⟹ pats_complete C P ⟷ pats_complete C P'"
proof (induct P P' rule: P_step_set.induct)
  case (P_fail P)
  with σg show ?case by (auto simp: wf_pats_complete_iff)
next
  case *: (P_simp pp pp' P)
  with pp_step_wf have "wf_pat pp" "wf_pats P" "wf_pats (insert pp P)" "wf_pats (insert pp' P)"
    by (auto simp: wf_pats_def)
  with pp_step_pcorrect[OF *(1)] show ?case
    by (auto simp: wf_pat_complete_iff wf_pats_complete_iff wf_pats_def)
next
  case *: (P_remove_pp pp P)
  with pp_step_wf have "wf_pat pp" "wf_pats P" "wf_pats (insert pp P)" by (auto simp: wf_pats_def)
  then show ?case using pp_success_pcorrect[OF *(1)]
    by (auto simp: wf_pats_complete_iff wf_pat_complete_iff)
next
  case *: (P_instantiate n pp x P)
  note wfppP = ‹wf_pats (insert pp P)›
  then have wfpp: "wf_pat pp" and wfP: "wf_pats P" by (auto simp: wf_pats_def)
  (* This is the step where well-formedness is essential *)
  from wfpp *(2) have x: "snd x ∈ S"
    unfolding tvars_pat_def tvars_match_def wf_pat_def wf_match_def by force
  note def = wf_pat_complete_iff[unfolded match_complete_wrt_def]
  define P' where "P' = {subst_pat_problem_set τ pp |. τ ∈ τs n x}"
  show ?case
    apply (fold P'_def)
  proof (rule ball_insert_un_cong, standard)
    assume complete: "Ball P' (pat_complete C)"
    show "pat_complete C pp" unfolding def[OF wfpp]
    proof (intro allI impI)
      fix σ
      assume cg: "σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)"
      from sorted_mapD[OF this] x
      have "σ x : snd x in 𝒯(C)" by auto
      then obtain f ts σs where f: "f : σs → snd x in C"
        and args: "ts :⇩l σs in 𝒯(C)"
        and σx: "σ x = Fun f ts"
        by (induct, auto)
      from f have f: "f : σs → snd x in C"
        by (meson fun_hastype_def)
      let ?l = "length ts" 
      from args have len: "length σs = ?l" by (simp add: list_all2_lengthD)
      have l: "?l ≤ m" using m[OF f] len by auto
      have σsS: "∀ι ∈ set σs. ι ∈ S" using C_sub_S f by auto
      define σ' where "σ' = (λ ys. let y = fst ys in if n ≤ y ∧ y < n + ?l ∧ σs ! (y - n) = snd ys then ts ! (y - n) else σ ys)" 
      have cg: "σ' :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)"
      proof (intro sorted_mapI, unfold hastype_in_restrict_sset conj_imp_eq_imp_imp)
        fix ys :: "nat × 's" and ι
        assume "ys : ι in 𝒱" and "ι ∈ S"
        then have [simp]: "ι = snd ys" and ysS: "snd ys ∈ S" by auto
        show "σ' ys : ι in 𝒯(C)" 
        proof (cases "σ' ys = σ ys")
          case True
          thus ?thesis using cg ysS by (auto simp: sorted_mapD)
        next
          case False
          obtain y s where ys: "ys = (y,s)" by force
          with False have y: "y - n < ?l" "n ≤ y" "y < n + ?l" and arg: "σs ! (y - n) = s"
            and σ': "σ' ys = ts ! (y - n)" 
            unfolding σ'_def Let_def by (auto split: if_splits)
          show ?thesis
            using σ' len list_all2_nthD[OF args y(1)]
            by (auto simp: ys arg[symmetric])
        qed
      qed
      define τ where "τ = subst x (Fun f (map Var (zip [n..<n + ?l] σs)))"
      have "τ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C,{x : ι in 𝒱. ι ∈ S})"
        using Fun_hastypeI[OF f, of "{x : ι in 𝒱. ι ∈ S}" "map Var (zip [n..<n + ?l] σs)"] σsS wfpp
        by (auto intro!: sorted_mapI
            simp: τ_def subst_def len[symmetric] list_all2_conv_all_nth hastype_restrict wf_pat_iff)
      from wf_pat_subst[OF this]
      have wf2: "wf_pat (subst_pat_problem_set τ pp)".
      from f have "τ ∈ τs n x" unfolding τs_def τ_def τc_def using len[symmetric] by auto
      hence "pat_complete C (subst_pat_problem_set τ pp)" using complete by (auto simp: P'_def)
      from this[unfolded def[OF wf2], rule_format, OF cg]
      obtain tl μ where tl: "tl ∈ subst_pat_problem_set τ pp" 
        and match: "⋀ ti li. (ti, li) ∈ tl ⟹ ti ⋅ σ' = li ⋅ μ" by force          
      from tl[unfolded subst_defs_set subst_left_def set_map]
      obtain tl' where tl': "tl' ∈ pp" and tl: "tl = {(t' ⋅ τ, l) |. (t',l) ∈ tl'}" by auto 
      show "∃tl∈ pp. ∃μ. ∀(ti, li)∈ tl. ti ⋅ σ = li ⋅ μ" 
      proof (intro bexI[OF _  tl'] exI[of _ μ], clarify)
        fix ti li
        assume tli: "(ti, li) ∈ tl'" 
        hence tlit: "(ti ⋅ τ, li) ∈ tl" unfolding tl by force
        from match[OF this] have match: "ti ⋅ τ ⋅ σ' = li ⋅ μ" by auto
        from *(1)[unfolded tvars_disj_pp_def, rule_format, OF tl' tli]
        have vti: "fst ` vars_term ti ∩ {n..<n + m} = {}" by auto
        have "ti ⋅ σ = ti ⋅ (τ ∘⇩s σ')" 
        proof (rule term_subst_eq, unfold subst_compose_def)
          fix y
          assume "y ∈ vars_term ti" 
          with vti have y: "fst y ∉ {n..<n + m}" by auto
          show "σ y = τ y ⋅ σ'" 
          proof (cases "y = x")
            case False
            hence "τ y ⋅ σ' = σ' y" unfolding τ_def subst_def by auto
            also have "… = σ y" 
              unfolding σ'_def using y l by auto
            finally show ?thesis by simp
          next
            case True
            show ?thesis unfolding True τ_def subst_simps σx eval_term.simps map_map o_def term.simps
              by (intro conjI refl nth_equalityI, auto simp: len σ'_def)
          qed
        qed  
        also have "… = li ⋅ μ" using match by simp
        finally show "ti ⋅ σ = li ⋅ μ" by blast
      qed
    qed
  next
    assume complete: "pat_complete C pp"
    show "∀pp ∈ P'. pat_complete C pp"
      apply (unfold P'_def) 
    proof safe
      fix τ
      assume "τ ∈ τs n x"
      from this[unfolded τs_def τc_def, simplified]
      obtain f ιs where f: "f : ιs → snd x in C" and τ: "τ = subst x (Fun f (map Var (zip [n..<n + length ιs] ιs)))" by auto
      let ?i = "length ιs" 
      let ?xs = "zip [n..<n + length ιs] ιs"
      have i: "?i ≤ m" by (rule m[OF f])
      have "∀ι ∈ set ιs. ι ∈ S" using C_sub_S f by blast 
      with Fun_hastypeI[OF f, of "{x : ι in 𝒱. ι ∈ S}" "map Var ?xs"] wfpp
      have "τ :⇩s 𝒱 |` tvars_pat pp → 𝒯(C,{x : ι in 𝒱. ι ∈ S})"
        by (auto intro!: sorted_mapI
            simp: τ subst_def hastype_restrict list_all2_conv_all_nth wf_pat_iff)
      note def2 = def[OF wf_pat_subst[OF this]]
      show "pat_complete C (subst_pat_problem_set τ pp)" unfolding def2
      proof (intro allI impI)
        fix σ assume cg: "σ :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)"
        define σ' where "σ' = σ(x := Fun f (map σ ?xs))" 
        from C_sub_S[OF f] have sortsS: "set ιs ⊆ S" by auto
        from f have f: "f : ιs → snd x in C" by (simp add: fun_hastype_def)
        with sorted_mapD[OF cg] set_mp[OF sortsS]
        have "Fun f (map σ ?xs) : snd x in 𝒯(C)" 
          by (auto intro!: Fun_hastypeI simp: list_all2_conv_all_nth)
        with sorted_mapD[OF cg]
        have cg: "σ' :⇩s {x : ι in 𝒱. ι ∈ S} → 𝒯(C)" by (auto intro!: sorted_mapI simp: σ'_def)
        from complete[unfolded def[OF wfpp], rule_format, OF this] 
        obtain tl μ where tl: "tl ∈ pp" and tli: "⋀ ti li. (ti, li)∈ tl ⟹ ti ⋅ σ' = li ⋅ μ" by force
        from tl have tlm: "{(t ⋅ τ, l) |. (t,l) ∈ tl} ∈ subst_pat_problem_set τ pp"
          unfolding subst_defs_set subst_left_def by auto
        {
          fix ti li
          assume mem: "(ti, li) ∈ tl"
          from *[unfolded tvars_disj_pp_def] tl mem have vti: "fst ` vars_term ti ∩ {n..<n + m} = {}" by force
          from tli[OF mem] have "li ⋅ μ = ti ⋅ σ'" by auto
          also have "… = ti ⋅ (τ ∘⇩s σ)"
          proof (intro term_subst_eq, unfold subst_compose_def)
            fix y
            assume "y ∈ vars_term ti" 
            with vti have y: "fst y ∉ {n..<n + m}" by auto
            show "σ' y = τ y ⋅ σ" 
            proof (cases "y = x")
              case False
              hence "τ y ⋅ σ = σ y" unfolding τ subst_def by auto
              also have "… = σ' y" 
                unfolding σ'_def using False by auto
              finally show ?thesis by simp
            next
              case True
              show ?thesis unfolding True τ
                by (simp add: o_def σ'_def)
            qed
          qed
          finally have "ti ⋅ τ ⋅ σ = li ⋅ μ" by auto
        }
        thus "∃tl ∈ subst_pat_problem_set τ pp. ∃μ. ∀(ti, li)∈tl. ti ⋅ σ = li ⋅ μ" 
          by (intro bexI[OF _ tlm], auto)
      qed
    qed
  qed
qed 
end

text ‹Represent a variable-form as a set of maps.›

definition "match_of_var_form f = {(Var y, Var x) | x y. y ∈ f x}"

definition "pat_of_var_form ff = match_of_var_form ` ff"

definition "var_form_of_match mp x = {y. (Var y, Var x) ∈ mp}"

definition "var_form_of_pat pp = var_form_of_match ` pp"

definition "tvars_var_form_pat ff = (⋃f ∈ ff. ⋃(range f))"

definition var_form_match where
  "var_form_match mp ⟷ mp ⊆ range (map_prod Var Var)"

definition "var_form_pat pp ≡ ∀mp ∈ pp. var_form_match mp"

lemma match_of_var_form_of_match:
  assumes "var_form_match mp"
  shows "match_of_var_form (var_form_of_match mp) = mp"
  using assms
  by (auto simp: var_form_match_def match_of_var_form_def var_form_of_match_def)

lemma tvars_match_var_form:
  assumes "var_form_match mp"
  shows "tvars_match mp = {v. ∃x. (Var v, Var x) ∈ mp}"
  using assms by (force simp: var_form_match_def tvars_match_def)

lemma pat_of_var_form_pat:
  assumes "var_form_pat pp"
  shows "pat_of_var_form (var_form_of_pat pp) = pp"
  using assms match_of_var_form_of_match
  by (auto simp: var_form_pat_def var_form_of_pat_def pat_of_var_form_def)

lemma tvars_pat_var_form: "tvars_pat (pat_of_var_form ff) = tvars_var_form_pat ff"
  by (fastforce simp: tvars_var_form_pat_def tvars_pat_def tvars_match_def pat_of_var_form_def match_of_var_form_def
      split: prod.splits)

lemma tvars_var_form_pat:
  assumes "var_form_pat pp"
  shows "tvars_var_form_pat (var_form_of_pat pp) = tvars_pat pp"
  apply (subst(2) pat_of_var_form_pat[OF assms,symmetric])
  by (simp add: tvars_pat_var_form)

lemma pat_complete_var_form:
  "pat_complete C (pat_of_var_form ff) ⟷
  (∀σ :⇩s 𝒱 |` tvars_var_form_pat ff → 𝒯(C). ∃f ∈ ff. ∃μ. ∀x. ∀y ∈ f x. σ y = μ x)"
proof-
  define V where "V = 𝒱 |` tvars_var_form_pat ff"
  have boo: "𝒱 |` tvars_pat {{(Var (a, b), Var xa) | xa a b. (a, b) ∈ x xa} |. x ∈ ff} = V"
    apply (unfold V_def)
    apply (subst tvars_pat_var_form[of ff, symmetric])
    by (auto simp: V_def pat_of_var_form_def match_of_var_form_def)
  show ?thesis
    apply (fold V_def)
    apply (auto simp: pat_complete_def match_complete_wrt_def pat_of_var_form_def
      match_of_var_form_def imp_conjL imp_ex boo)
    apply (metis old.prod.exhaust)
    by metis
qed

lemma pat_complete_var_form_set:
  "pat_complete C (pat_of_var_form ff) ⟷
  (∀σ :⇩s 𝒱 |` tvars_var_form_pat ff → 𝒯(C). ∃f ∈ ff. ∃μ. ∀x. σ ` f x ⊆ {μ x})"
  by (auto simp: pat_complete_var_form image_subset_iff)

lemma pat_complete_var_form_Uniq:
  "pat_complete C (pat_of_var_form ff) ⟷
  (∀σ :⇩s 𝒱 |` tvars_var_form_pat ff → 𝒯(C). ∃f ∈ ff. ∀x. UNIQ (σ ` f x))"
proof-
  { fix σ f assume σ: "σ :⇩s 𝒱 |` tvars_var_form_pat ff → 𝒯(C)" and f: "f ∈ ff"
    have "(∃μ. ∀x. σ ` f x ⊆ {μ x}) ⟷ (∀x. ∃⇩≤⇩1 y. y ∈ σ ` f x)"
    proof (safe)
      fix μ x
      assume "∀x. σ ` f x ⊆ {μ x}"
      from this[rule_format, of x]
      have "y ∈ f x ⟹ σ y = μ x" for y by auto
      then show "∃⇩≤⇩1 y. y ∈ σ ` f x" by (auto intro!: Uniq_I)
    next
      define μ where "μ x = the_elem (σ ` f x)" for x
      fix x assume "∀x. ∃⇩≤⇩1 y. y ∈ σ ` f x"
      from Uniq_eq_the_elem[OF this[rule_format], folded μ_def]
      show "∃μ. ∀x. σ ` f x ⊆ {μ x}" by auto
    qed
  }
  then show ?thesis by (simp add: pat_complete_var_form_set)
qed

lemma ex_var_form_pat: "(∃f∈var_form_of_pat pp. P f) ⟷ (∃mp ∈ pp. P (var_form_of_match mp))"
  by (auto simp: var_form_of_pat_def)

lemma pat_complete_var_form_nat:
  assumes fin: "∀(x,ι) ∈ tvars_var_form_pat ff. finite_sort C ι"
    and uniq: "∀f ∈ ff. ∀x::'v. UNIQ (snd ` f x)"
  shows "pat_complete C (pat_of_var_form ff) ⟷
  (∀α. (∀v ∈ tvars_var_form_pat ff. α v < card_of_sort C (snd v)) ⟶
  (∃f ∈ ff. ∀x. UNIQ (α ` f x)))"
  (is "?l ⟷ (∀α. ?s α ⟶ ?r α)")
proof safe
  note fin = fin[unfolded Ball_Pair_conv, rule_format]
  { fix α
    assume l: ?l and a: "?s α"
    define σ :: "_ ⇒ (_,unit) term" where
      "σ ≡ λ(x,ι). term_of_index C ι (α (x,ι))"
    have "σ (x,ι) : ι in 𝒯(C)" if x: "(x,ι) ∈ tvars_var_form_pat ff" for x ι
      using term_of_index_bij[OF fin, OF x]
        a[unfolded Ball_Pair_conv, rule_format, OF x]
      by (auto simp: bij_betw_def σ_def)
    then have "σ :⇩s 𝒱 |` tvars_var_form_pat ff → 𝒯(C)"
      by (auto intro!: sorted_mapI simp: hastype_restrict)
    from l[unfolded pat_complete_var_form_Uniq, rule_format, OF this]
    obtain f where f: "f ∈ ff" and u: "⋀x. UNIQ (σ ` f x)" by auto
    have id: "y ∈ f x ⟹ index_of_term C (σ y) = α y" for y x
      using assms a f
      by (force simp: σ_def index_of_term_of_index tvars_var_form_pat_def Ball_def split: prod.splits)
    then have "α ` f x = index_of_term C ` σ ` f x" for x
      by (auto simp: image_def)
    then have "UNIQ (α ` f x)" for x by (simp add: image_Uniq[OF u])
    with f show "?r α" by auto
  next
    assume r: "∀α. ?s α ⟶ ?r α"
    show ?l
      unfolding pat_complete_var_form_Uniq
    proof safe
      fix σ
      assume σ: "σ :⇩s 𝒱 |` tvars_var_form_pat ff → 𝒯(C)"
      from sorted_mapD[OF this]
      have ty: "(x,ι) ∈ tvars_var_form_pat ff ⟹ σ (x,ι) : ι in 𝒯(C)"
        for x ι by (auto simp: hastype_restrict)
      define α where "α ≡ index_of_term C ∘ σ"
      have "α (x,ι) < card_of_sort C ι" if x: "(x,ι) ∈ tvars_var_form_pat ff"
        for x ι using index_of_term_bij[OF fin[OF x]] ty[OF x]
        by (auto simp: α_def bij_betw_def)
      then have "∃f∈ff. ∀x. UNIQ (α ` f x)" by (auto intro!: r[rule_format])
      then obtain f where f: "f ∈ ff" and u: "⋀x. UNIQ (α ` f x)" by auto
      have "UNIQ (σ ` f x)" for x
      proof-
        from uniq[rule_format, OF f]
        have ex: "∃ι. snd ` f x ⊆ {ι}"
          by (auto simp: subset_singleton_iff_Uniq)
        then obtain ι where sub: "snd ` f x ⊆ {ι}" by auto
        { fix y κ assume yk: "(y,κ) ∈ f x"
          with sub have [simp]: "κ = ι" by auto 
          from yk f have y: "(y,ι) ∈ tvars_var_form_pat ff"
            by (auto simp: tvars_var_form_pat_def)
          from y fin[OF y]
          have "term_of_index C ι (α (y,κ)) = σ (y,κ)"
            by (auto simp: α_def hastype_restrict
                intro!: term_of_index_of_term sorted_mapD[OF σ])
        }
        then have "y ∈ f x ⟹ term_of_index C ι (α y) = σ y" for y
          by (cases y, auto)
        then have "σ ` f x = term_of_index C ι ` α ` f x"
          by (auto simp: image_def)
        then show "UNIQ (σ ` f x)" by (simp add: image_Uniq[OF u])
      qed
      with f show "∃f ∈ ff. ∀x. UNIQ (σ ` f x)" by auto
    qed
  }
qed

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)

context pattern_completeness_context begin

definition weak_finite_var_form_match :: "('f,'v,'s)match_problem_set ⇒ bool" where
  "weak_finite_var_form_match mp = ((∀ (t,l) ∈ mp. ∃ y. l = Var y)
     ∧ (∀ f ts y. (Fun f ts, Var y) ∈ mp ⟶  
          (∃ x. (Var x, Var y) ∈ mp ∧ inf_sort (snd x))
        ∧ (∀ t. (t, Var y) ∈ mp ⟶ root t ∈ {None, Some (f,length ts)})))"

definition weak_finite_var_form_pat :: "('f,'v,'s)pat_problem_set ⇒ bool" where
  "weak_finite_var_form_pat p = (∀ mp ∈ p. weak_finite_var_form_match mp)"

end

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

end