Theory Pattern_Completeness

section ‹Pattern-Completeness and Related Properties›

text ‹We use the core decision procedure for pattern completeness 
  and connect it to other properties like pattern completeness of programs (where the lhss are given), 
  or (strong) quasi-reducibility.›

theory Pattern_Completeness
  imports 
    Pattern_Completeness_List
    Show.Shows_Literal
    Certification_Monads.Check_Monad
begin


text ‹A pattern completeness decision procedure for a set of lhss›

definition basic_terms :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('v ⇀ 's) ⇒ ('f,'v)term set" ("ℬ'(_,_,_')") where
  "ℬ(C,D,V) = { Fun f ts | f ss s ts . f : ss → s in D ∧ ts :⇩l ss in 𝒯(C,V)}" 

definition matches :: "('f,'v)term ⇒ ('f,'v)term ⇒ bool" (infix "matches" 50) where
  "l matches t = (∃ σ. t = l ⋅ σ)"

definition pat_complete_lhss :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('f,'v)term set ⇒ bool" where
  "pat_complete_lhss C D L = (∀ t ∈ ℬ(C,D,∅). ∃l ∈ L. l matches t)" 


definition decide_pat_complete_lhss :: 
  "(('f × 's list) × 's)list ⇒ (('f × 's list) × 's)list ⇒ ('f,'v)term list ⇒ showsl + bool" where
  "decide_pat_complete_lhss C D lhss = do {
    check (distinct (map fst C)) (showsl_lit (STR ''constructor information contains duplicate''));
    check (distinct (map fst D)) (showsl_lit (STR ''defined symbol information contains duplicate''));
    let S = sorts_of_ssig_list C;
    check_allm (λ ((f,ss),_). check_allm (λ s. check (s ∈ set S) 
      (showsl_lit (STR ''a defined symbol has argument sort that is not known in constructors''))) ss) D;
    (case (decide_nonempty_sorts S C) of None ⇒ return () | Some s ⇒ error (showsl_lit (STR ''some sort is empty'')));
    let pats = [Fun f (map Var (zip [0..<length ss] ss)). ((f,ss),s) ← D];
    let P = [[[(pat,lhs)]. lhs ← lhss]. pat ← pats];
    return (decide_pat_complete C P)
  }" 

theorem decide_pat_complete_lhss: 
  assumes "decide_pat_complete_lhss C D (lhss :: ('f,'v)term list) = return b" 
  shows "b = pat_complete_lhss (map_of C) (map_of D) (set lhss)" 
proof -
  let ?EMPTY = "pattern_completeness_context.EMPTY" 
  let ?cg_subst = "pattern_completeness_context.cg_subst" 
  let ?C = "map_of C"
  let ?D = "map_of D" 
  define S where "S = sorts_of_ssig_list C" 
  define pats where "pats = map (λ ((f,ss),s). Fun f (map Var (zip [0..<length ss] ss))) D" 
  define P where "P = map (λ pat. map (λ lhs. [(pat,lhs)]) lhss) pats" 
  let ?match_lhs = "λt. ∃l ∈ set lhss. l matches t" 
  note ass = assms(1)[unfolded decide_pat_complete_lhss_def, folded S_def, 
      unfolded Let_def, folded pats_def, folded P_def, simplified]
  from ass have dec: "decide_nonempty_sorts S C = None" (is "?e = _") by (cases ?e, auto) 
  note ass = ass[unfolded dec, simplified]
  from ass have b: "b = decide_pat_complete C P" and dist: "distinct (map fst C)" "distinct (map fst D)" by auto
  have "b = decide_pat_complete C P" by fact
  also have "… = pats_complete (set S) ?C (pat_list ` set P)" 
  proof (rule decide_pat_complete[OF refl dist(1) dec[unfolded S_def]], unfold S_def[symmetric])
    {
      fix i si f ss s
      assume mem: "((f, ss), s) ∈ set D" and isi: "(i, si) ∈ set (zip [0..<length ss] ss)" 
      from isi have si: "si ∈ set ss" by (metis in_set_zipE)
      from mem si ass
      have "si ∈ set S" by auto
    }
    thus "snd ` ⋃ (vars ` fst ` set (concat (concat P))) ⊆ set S" unfolding P_def pats_def by force
  qed simp
  also have "pat_list ` set P = { { {(pat,lhs)} | lhs. lhs ∈ set lhss} | pat. pat ∈ set pats}" 
    unfolding pat_list_def P_def by (auto simp: image_comp)
  also have "pats_complete (set S) ?C … ⟷
     Ball { pat ⋅ σ | pat σ. pat ∈ set pats ∧ ?cg_subst (set S) ?C σ} ?match_lhs" (is "_ = Ball ?L _")
    unfolding pattern_completeness_context.pat_complete_def 
      pattern_completeness_context.match_complete_wrt_def matches_def 
    by auto (smt (verit, best) case_prod_conv mem_Collect_eq singletonI, blast)
  also have "?L = ℬ(?C,?D,∅)" (is "_ = ?R")
  proof 
    {
      fix pat and σ :: "('f,_,'v)gsubst" 
      assume pat: "pat ∈ set pats" and subst: "?cg_subst (set S) ?C σ"
      from pat[unfolded pats_def] obtain f ss s where pat: "pat = Fun f (map Var (zip [0..<length ss] ss))" 
        and inDs: "((f,ss),s) ∈ set D" by auto
      from dist(2) inDs have f: "f : ss → s in ?D" unfolding hastype_in_ssig_def by simp
      {
        fix i
        assume i: "i < length ss" 
        hence "ss ! i ∈ set ss" by auto
        with inDs ass have "ss ! i ∈ set S" by auto
        with subst have "σ (i, ss ! i) : ss ! i in 𝒯(?C,∅)" unfolding pattern_completeness_context.cg_subst_def 
            pattern_completeness_context.EMPTY_def by auto
      } note ssigma = this
      define ts where "ts = (map (λ i. σ (i, ss ! i)) [0..<length ss])" 
      have ts: "ts :⇩l ss in 𝒯(?C,∅)" unfolding list_all2_conv_all_nth ts_def using ssigma by auto
      have pat: "pat ⋅ σ = Fun f ts" 
        unfolding pat ts_def by (auto intro: nth_equalityI)
      from pat f ts have "pat ⋅ σ ∈ ?R" unfolding basic_terms_def by auto
    }
    thus "?L ⊆ ?R" by blast
    {
      fix f ss s and ts :: "('f,'v)term list" 
      assume f: "f : ss → s in ?D" and ts: "ts :⇩l ss in 𝒯(?C,∅)" 
      from ts have len: "length ts = length ss" by (metis list_all2_lengthD)
      define pat where "pat = Fun f (map Var (zip [0..<length ss] ss))"
      from f have "((f,ss),s) ∈ set D" unfolding hastype_in_ssig_def by (metis map_of_SomeD)
      hence pat: "pat ∈ set pats" unfolding pat_def pats_def by force
      define σ where "σ x = (case x of (i,s) ⇒ if i < length ss ∧ s = ss ! i then ts ! i else 
        (SOME t. t : s in 𝒯(?C,?EMPTY)))" for x
      have id: "Fun f ts = pat ⋅ σ" unfolding pat_def using len
        by (auto intro!: nth_equalityI simp: σ_def)
      have ssigma: "?cg_subst (set S) ?C σ" 
        unfolding pattern_completeness_context.cg_subst_def
      proof (intro allI impI)
        fix x :: "nat × _" 
        assume "snd x ∈ set S" 
        then obtain i s where x: "x = (i,s)" and s: "s ∈ set S" by (cases x, auto)
        show "σ x : snd x in 𝒯(?C,?EMPTY)" 
        proof (cases "i < length ss ∧ s = ss ! i")
          case True
          hence id: "σ x = ts ! i" unfolding x σ_def by auto
          from ts True show ?thesis unfolding id unfolding x snd_conv pattern_completeness_context.EMPTY_def 
            by (simp add: list_all2_conv_all_nth)
        next
          case False
          hence id: "σ x = (SOME t. t : s in 𝒯(?C,?EMPTY))" unfolding x σ_def by auto
          from decide_nonempty_sorts(1)[OF dist(1) refl dec] s
          have "∃ t. t : s in 𝒯(?C,?EMPTY)" unfolding pattern_completeness_context.EMPTY_def by auto
          from someI_ex[OF this] have "σ x : s in 𝒯(?C,?EMPTY)" unfolding id .
          thus ?thesis unfolding x by auto
        qed
      qed
      from pat id ssigma
      have "Fun f ts ∈ ?L" by auto
    }
    thus "?R ⊆ ?L" unfolding basic_terms_def by auto
  qed
  finally show ?thesis unfolding pat_complete_lhss_def by blast
qed

text ‹Definition of strong quasi-reducibility and a corresponding decision procedure›

definition strong_quasi_reducible :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('f,'v)term set ⇒ bool" where
  "strong_quasi_reducible C D L =
  (∀ t ∈ ℬ(C,D,∅). ∃ ti ∈ set (t # args t). ∃l ∈ L. l matches ti)" 


definition term_and_args :: "'f ⇒ ('f,'v)term list ⇒ ('f,'v)term list" where
  "term_and_args f ts = Fun f ts # ts"  

definition decide_strong_quasi_reducible :: 
  "(('f × 's list) × 's)list ⇒ (('f × 's list) × 's)list ⇒ ('f,'v)term list ⇒ showsl + bool" where
  "decide_strong_quasi_reducible C D lhss = do {
    check (distinct (map fst C)) (showsl_lit (STR ''constructor information contains duplicate''));
    check (distinct (map fst D)) (showsl_lit (STR ''defined symbol information contains duplicate''));
    let S = sorts_of_ssig_list C;
    check_allm (λ ((f,ss),_). check_allm (λ s. check (s ∈ set S) 
      (showsl_lit (STR ''defined symbol f has argument sort s that is not known in constructors''))) ss) D;
    (case (decide_nonempty_sorts S C) of None ⇒ return () | Some s ⇒ error (showsl_lit (STR ''sort s is empty'')));
    let pats = map (λ ((f,ss),s). term_and_args f (map Var (zip [0..<length ss] ss))) D;
    let P = map (List.maps (λ pat. map (λ lhs. [(pat,lhs)]) lhss)) pats;
    return (decide_pat_complete C P)
  }" 

lemma decide_strong_quasi_reducible: 
  assumes "decide_strong_quasi_reducible C D (lhss :: ('f,'v)term list) = return b" 
  shows "b = strong_quasi_reducible (map_of C) (map_of D) (set lhss)" 
proof -
  let ?EMPTY = "pattern_completeness_context.EMPTY" 
  let ?cg_subst = "pattern_completeness_context.cg_subst" 
  let ?C = "map_of C"
  let ?D = "map_of D" 
  define S where "S = sorts_of_ssig_list C" 
  define pats where "pats = map (λ ((f,ss),s). term_and_args f (map Var (zip [0..<length ss] ss))) D" 
  define P where "P = map (List.maps (λ pat. map (λ lhs. [(pat,lhs)]) lhss)) pats" 
  let ?match_lhs = "λt. ∃l ∈ set lhss. l matches t" 
  note ass = assms(1)[unfolded decide_strong_quasi_reducible_def, folded S_def, folded pats_def, 
      unfolded Let_def, folded P_def]
  from ass have dec: "decide_nonempty_sorts S C = None" (is "?e = _") by (cases ?e, auto) 
  note ass = ass[unfolded dec, simplified]
  from ass have b: "b = decide_pat_complete C P" and dist: "distinct (map fst C)" "distinct (map fst D)" by auto
  have "b = decide_pat_complete C P" by fact
  also have "… = pats_complete (set S) ?C (pat_list ` set P)" 
  proof (rule decide_pat_complete[OF refl dist(1) dec[unfolded S_def]], unfold S_def[symmetric])
    {
      fix f ss s i si
      assume mem: "((f, ss), s) ∈ set D" and isi: "(i, si) ∈ set (zip [0..<length ss] ss)"
      from isi have si: "si ∈ set ss" by (metis in_set_zipE)
      from mem si ass
      have "si ∈ set S" by auto
    }
    thus "snd ` ⋃ (vars ` fst ` set (concat (concat P))) ⊆ set S" unfolding P_def pats_def term_and_args_def List.maps_def
      by fastforce
  qed simp
  also have "pat_list ` set P = { { {(pat,lhs)} | lhs pat. pat ∈ set patL ∧ lhs ∈ set lhss} | patL. patL ∈ set pats}" 
    unfolding pat_list_def P_def List.maps_def by (auto simp: image_comp) force+
  also have "pats_complete (set S) ?C … ⟷
     (∀ patsL σ. patsL ∈ set pats ⟶ ?cg_subst (set S) ?C σ ⟶ (∃ pat ∈ set patsL. ?match_lhs (pat ⋅ σ)))" (is "_ ⟷ ?L")
    unfolding pattern_completeness_context.pat_complete_def 
      pattern_completeness_context.match_complete_wrt_def matches_def 
    by auto 
      (smt (verit, best) case_prod_conv mem_Collect_eq singletonI, 
        metis (mono_tags, lifting) case_prod_conv singleton_iff)
  also have "?L 
    ⟷ (∀ f ss s (ts :: ('f,'v)term list). f : ss → s in ?D ⟶ ts :⇩l ss in 𝒯(?C,∅) ⟶ 
           (∃ ti ∈ set (term_and_args f ts). ?match_lhs ti))" (is "_ = ?R")
  proof (standard; intro allI impI)  
    fix patL and σ :: "('f,_,'v)gsubst" 
    assume patL: "patL ∈ set pats" and subst: "?cg_subst (set S) ?C σ" and R: ?R
    from patL[unfolded pats_def] obtain f ss s where patL: "patL = term_and_args f (map Var (zip [0..<length ss] ss))" 
      and inDs: "((f,ss),s) ∈ set D" by auto
    from dist(2) inDs have f: "f : ss → s in ?D" unfolding hastype_in_ssig_def by simp
    {
      fix i
      assume i: "i < length ss" 
      hence "ss ! i ∈ set ss" by auto
      with inDs ass have "ss ! i ∈ set S" by auto
      with subst have "σ (i, ss ! i) : ss ! i in 𝒯(?C,∅)" 
        unfolding pattern_completeness_context.cg_subst_def pattern_completeness_context.EMPTY_def by auto
    } note ssigma = this
    define ts where "ts = (map (λ i. σ (i, ss ! i)) [0..<length ss])" 
    have ts: "ts :⇩l ss in 𝒯(?C,∅)" unfolding list_all2_conv_all_nth ts_def using ssigma by auto
    from R[rule_format, OF f ts] obtain ti where ti: "ti ∈ set (term_and_args f ts)" and match: "?match_lhs ti" by auto
    have "map (λ pat. pat ⋅ σ) patL = term_and_args f ts" unfolding patL term_and_args_def ts_def
      by (auto intro: nth_equalityI)
    from ti[folded this] match
    show "∃pat∈set patL. ?match_lhs (pat ⋅ σ)" by auto
  next
    fix f ss s and ts :: "('f,'v)term list" 
    assume f: "f : ss → s in ?D" and ts: "ts :⇩l ss in 𝒯(?C,∅)" and L: ?L
    from ts have len: "length ts = length ss" by (metis list_all2_lengthD)
    define patL where "patL = term_and_args f (map Var (zip [0..<length ss] ss))" 
    from f have "((f,ss),s) ∈ set D" unfolding hastype_in_ssig_def by (metis map_of_SomeD)
    hence patL: "patL ∈ set pats" unfolding patL_def pats_def by force
    define σ where "σ x = (case x of (i,s) ⇒ if i < length ss ∧ s = ss ! i then ts ! i else 
      (SOME t. t : s in 𝒯(?C,?EMPTY)))" for x
    have ssigma: "?cg_subst (set S) ?C σ" 
      unfolding pattern_completeness_context.cg_subst_def
    proof (intro allI impI)
      fix x :: "nat × _" 
      assume "snd x ∈ set S" 
      then obtain i s where x: "x = (i,s)" and s: "s ∈ set S" by (cases x, auto)
      show "σ x : snd x in 𝒯(?C,?EMPTY)" 
      proof (cases "i < length ss ∧ s = ss ! i")
        case True
        hence id: "σ x = ts ! i" unfolding x σ_def by auto
        from ts True show ?thesis unfolding id unfolding x snd_conv pattern_completeness_context.EMPTY_def 
          by (simp add: list_all2_conv_all_nth)
      next
        case False
        hence id: "σ x = (SOME t. t : s in 𝒯(?C,?EMPTY))" unfolding x σ_def by auto
        from decide_nonempty_sorts(1)[OF dist(1) refl dec] s
        have "∃ t. t : s in 𝒯(?C,?EMPTY)" unfolding pattern_completeness_context.EMPTY_def by auto
        from someI_ex[OF this] have "σ x : s in 𝒯(?C,?EMPTY)" unfolding id .
        thus ?thesis unfolding x by auto
      qed
    qed
    from L[rule_format, OF patL ssigma]
    obtain pat where pat: "pat ∈ set patL" and match: "?match_lhs (pat ⋅ σ)" by auto
    have id: "map (λ pat. pat ⋅ σ) patL = term_and_args f ts" unfolding patL_def term_and_args_def using len
      by (auto intro!: nth_equalityI simp: σ_def)      
    show "∃ti ∈ set (term_and_args f ts). ?match_lhs ti" unfolding id[symmetric] using pat match by auto
  qed
  also have "… = (∀t. t ∈ ℬ(?C,?D,∅) ⟶ (∃ ti ∈ set (t # args t). ?match_lhs ti))" 
    unfolding basic_terms_def term_and_args_def by force
  finally show ?thesis unfolding strong_quasi_reducible_def by blast
qed

subsection ‹Connecting Pattern-Completeness, Strong Quasi-Reducibility and Quasi-Reducibility›

definition quasi_reducible :: "('f,'s)ssig ⇒ ('f,'s)ssig ⇒ ('f,'v)term set ⇒ bool" where
  "quasi_reducible C D L = (∀ t ∈ ℬ(C,D,∅). ∃ tp ⊴ t. ∃l ∈ L. l matches tp)" 

lemma pat_complete_imp_strong_quasi_reducible:
  "pat_complete_lhss C D L ⟹ strong_quasi_reducible C D L" 
  unfolding pat_complete_lhss_def strong_quasi_reducible_def by force

lemma arg_imp_subt: "s ∈ set (args t) ⟹ t ⊵ s" 
  by (cases t, auto)

lemma strong_quasi_reducible_imp_quasi_reducible:
  "strong_quasi_reducible C D L ⟹ quasi_reducible C D L" 
  unfolding strong_quasi_reducible_def quasi_reducible_def 
  by (force dest: arg_imp_subt)

text ‹If no root symbol of a left-hand sides is a constructor, then pattern completeness and 
  quasi-reducibility coincide.›
lemma quasi_reducible_iff_pat_complete: fixes L :: "('f,'v)term set" 
  assumes "⋀ l f ls τs τ. l ∈ L ⟹ l = Fun f ls ⟹ ¬ f : τs → τ in C" 
  shows "pat_complete_lhss C D L ⟷ quasi_reducible C D L" 
proof (standard, rule strong_quasi_reducible_imp_quasi_reducible[OF pat_complete_imp_strong_quasi_reducible])
  assume q: "quasi_reducible C D L" 
  show "pat_complete_lhss C D L" 
    unfolding pat_complete_lhss_def
  proof 
    fix t :: "('f,'v)term" 
    assume t: "t ∈ ℬ(C,D,∅)" 
    from q[unfolded quasi_reducible_def, rule_format, OF this]
    obtain tp where tp: "t ⊵ tp" and match: "∃l ∈ L. l matches tp" by auto
    show "∃l ∈ L. l matches t" 
    proof (cases "t = tp")
      case True
      thus ?thesis using match by auto
    next
      case False
      from t[unfolded basic_terms_def] obtain f ts ss where t: "t = Fun f ts" and ts: "ts :⇩l ss in 𝒯(C,∅)" by auto
      from t False tp obtain ti where ti: "ti ∈ set ts" and subt: "ti ⊵ tp"
        by (meson Fun_supteq)
      from subt obtain CC where ctxt: "ti = CC ⟨ tp ⟩" by auto
      from ti ts obtain s where "ti : s in 𝒯(C,∅)" unfolding list_all2_conv_all_nth set_conv_nth by auto
      from hastype_context_decompose[OF this[unfolded ctxt]] obtain s where tp: "tp : s in 𝒯(C,∅)" by blast
      from match[unfolded matches_def] obtain l σ where l: "l ∈ L" and match: "tp = l ⋅ σ" by auto
      show ?thesis
      proof (cases l)
        case (Var x)
        with l show ?thesis unfolding matches_def by (auto intro!: bexI[of _ l])
      next
        case (Fun f ls)
        from tp[unfolded match this, simplified] obtain ss where "f : ss → s in C" 
          by (meson Fun_hastype hastype_def hastype_in_ssig_def)
        with assms[OF l Fun, of ss s] show ?thesis by auto
      qed
    qed
  qed
qed

end