Theory FCF_Connection

(* We here combine the solver for FCF problems with the phase 1 and phase 2 algorithm,
   to obtain the fully working algorithm of Section 5 in the journal paper. *)

theory FCF_Connection
  imports 
    Pattern_Completeness
    FCF_List
    Finite_IDL_Solver
begin

text ‹Combining the three solvers to get the full algorithm of section 5: 
  arbitrary-to-fcf: @{const pat_complete_impl_fcf},
  fcf-to-idl: @{const pattern_completeness_context.fcf_solver_alg}, and
  idl-solver: @{const default_fidl_solver}›

definition decide_pat_complete_new :: "_ ⇒ _ ⇒ (('f × 's list) × 's)list ⇒ ('f,'v,'s)pats_problem_list ⇒ bool" where
  "decide_pat_complete_new rn rv Cs P = (let 
      m = max_arity_list Cs;
      Cl = constr_list Cs; 
      Cm = Mapping.of_alist Cs;
      (IS,CD) = compute_inf_card_sorts_bnd Cs;
      solve = pattern_completeness_context.fcf_solver_alg (Mapping.lookup Cm) m Cl CD default_fidl_solver
     in pat_complete_impl_fcf m Cl (λ s. s ∈ IS) (Mapping.lookup Cm) rn rv solve P)" 

theorem decide_pat_complete_new:
  assumes dist: "distinct (map fst Cs)" 
    and non_empty_sorts: "decide_nonempty_sorts (sorts_of_ssig_list Cs) Cs = None" 
    and P: "snd ` ⋃ (vars ` fst ` set (concat (concat P))) ⊆ set (sorts_of_ssig_list Cs)"
    and ren: "renaming_funs rn rv" 
  shows "decide_pat_complete_new rn rv Cs P ⟷ pats_complete (map_of Cs) (pat_list ` set P)"
proof -
  interpret pattern_completeness_list Cs
    apply unfold_locales
    using dist non_empty_sorts.
  have nemp:
    "∀ f τs τ τ'. f : τs → τ in map_of Cs ⟶ τ' ∈ set τs ⟶ ¬ empty_sort (map_of Cs) τ'"
    using C_sub_S by (auto intro!: nonempty_sort)
  obtain inf cd where "compute_inf_card_sorts_bnd Cs = (inf,cd)" by force
  with compute_inf_card_sorts_bnd(2,3)[OF refl nemp dist this]
  have cics: "compute_inf_card_sorts_bnd Cs = (compute_inf_sorts Cs, minBnd o card_of_sort (map_of Cs))"
    by auto
  have Cm: "Mapping.lookup (Mapping.of_alist Cs) = map_of Cs" using dist
    using lookup_of_alist by fastforce
  show ?thesis
    apply (unfold decide_pat_complete_new_def Let_def case_prod_beta)
    unfolding pat_complete_impl_fcf_def Cm
    by (rule pat_complete_impl[OF ren fcf_solver_alg'[OF default_fidl_solver] refl P])
qed
  
export_code decide_pat_complete_new checking 

definition decide_pat_complete_lhss_new :: 
  "_ ⇒ _ ⇒ _ ⇒ _ ⇒  ('f,'v)term list ⇒ showsl + bool" where
  "decide_pat_complete_lhss_new rn rv C D lhss = do {
    check_signatures C D;
    return (decide_pat_complete_new rn rv C (pats_of_lhss D lhss))
  }"  

theorem decide_pat_complete_lhss_new:
  fixes C D :: "(('f × 's list) × 's) list" and lhss :: "('f,'v)term list"
  assumes "decide_pat_complete_lhss_new rn rv C D lhss = return b" 
    and ren: "renaming_funs rn rv" 
  shows "b = pat_complete_lhss (map_of C) (map_of D) (set lhss)" 
proof -
  let ?C = "map_of C"
  let ?D = "map_of D"
  define S where "S = sorts_of_ssig_list C"
  define P where "P = pats_of_lhss D lhss"
  have sig: "isOK(check_signatures C D)" 
    and b: "b = decide_pat_complete_new rn rv C P"
    using assms
     apply (unfold decide_pat_complete_lhss_new_def)
     apply (unfold Let_def P_def[symmetric] S_def[symmetric])
    by auto
  note * = check_signatures[OF sig]
  note distC = *(1) note distD = *(2) note condD = *(3) note dec = *(4)  
  interpret pattern_completeness_list C
    rewrites "sorts_of_ssig_list C = S"
     apply unfold_locales
    using * by (auto simp: S_def)
  have "b = pats_complete ?C (pat_list ` set P)"
    apply (unfold b)
    apply (rule decide_pat_complete_new[OF dist dec[unfolded S_def] _ ren])
    apply (unfold P_def)
    apply (rule pats_of_lhss_vars[OF condD[unfolded P_def S_def]])
    done
  also have "… = (∀t∈ℬ(?C,?D). ∃l∈set lhss. l matches t)" unfolding P_def
    by (rule pats_of_lhss[OF sig])
  finally show ?thesis unfolding pat_complete_lhss_def .
qed

end