Theory NF_Impl

theory NF_Impl
  imports NF
    Type_Instances_Impl
begin

subsubsection ‹Implementation of normal form construction›
(* Implementation *)
fun supteq_list :: "('f, 'v) Term.term ⇒ ('f, 'v) Term.term list"
where
  "supteq_list (Var x) = [Var x]" |
  "supteq_list (Fun f ts) = Fun f ts # concat (map supteq_list ts)"

fun supt_list :: "('f, 'v) Term.term ⇒ ('f, 'v) Term.term list"
where
  "supt_list (Var x) = []" |
  "supt_list (Fun f ts) = concat (map supteq_list ts)"

lemma supteq_list [simp]:
  "set (supteq_list t) = {s. t ⊵ s}"
proof (rule set_eqI, simp)
  fix s
  show "s ∈ set(supteq_list t) = (t ⊵ s)"
  proof (induct t, simp add: supteq_var_imp_eq)
    case (Fun f ss)
    show ?case
    proof (cases "Fun f ss = s", (auto)[1])
      case False
      show ?thesis
      proof
        assume "Fun f ss ⊵ s"
        with False have sup: "Fun f ss ⊳ s" using supteq_supt_conv by auto
        obtain C where "C ≠ □" and "Fun f ss = C⟨s⟩" using sup by auto
        then obtain b D a where "Fun f ss = Fun f (b @ D⟨s⟩ # a)" by (cases C, auto)
        then have D: "D⟨s⟩ ∈ set ss" by auto
        with Fun[OF D] ctxt_imp_supteq[of D s] obtain t where "t ∈ set ss" and "s ∈ set (supteq_list t)" by auto
        then show "s ∈ set (supteq_list (Fun f ss))" by auto
      next
        assume "s ∈ set (supteq_list (Fun f ss))"
        with False obtain t where t: "t ∈ set ss" and "s ∈ set (supteq_list t)" by auto
        with Fun[OF t] have "t ⊵ s" by auto
        with t show "Fun f ss ⊵ s" by auto
      qed
    qed
  qed
qed

lemma supt_list_sound [simp]:
  "set (supt_list t) = {s. t ⊳ s}"
  by (cases t) auto

fun mergeP_impl where
  "mergeP_impl Bot t = True"
| "mergeP_impl t Bot = True"
| "mergeP_impl (BFun f ss) (BFun g ts) =
  (if f = g ∧ length ss = length ts then list_all (λ (x, y). mergeP_impl x y) (zip ss ts)  else False)"

lemma [simp]: "mergeP_impl s Bot = True" by (cases s) auto 

lemma [simp]: "mergeP_impl s t ⟷ (s, t) ∈ mergeP" (is "?LS = ?RS")
proof
  show "?LS ⟹ ?RS"
    by (induct rule: mergeP_impl.induct, auto split: if_splits intro!: step)
      (smt length_zip list_all_length mergeP.step min_less_iff_conj nth_mem nth_zip old.prod.case)
next
  show "?RS ⟹ ?LS" by (induct rule: mergeP.induct, auto simp add: list_all_length)
qed

fun bless_eq_impl where
  "bless_eq_impl Bot t = True"
| "bless_eq_impl (BFun f ss) (BFun g ts) =
  (if f = g ∧ length ss = length ts then list_all (λ (x, y). bless_eq_impl x y) (zip ss ts) else False)"
| "bless_eq_impl _ _ = False"


lemma [simp]: "bless_eq_impl s t ⟷ (s, t) ∈ bless_eq" (is "?RS = ?LS")
proof
  show "?LS ⟹ ?RS" by (induct rule: bless_eq.induct, auto simp add: list_all_length)
next
  show "?RS ⟹ ?LS"
    by (induct rule: bless_eq_impl.induct, auto split: if_splits intro!: bless_eq.step)
      (metis (full_types) length_zip list_all_length min_less_iff_conj nth_mem nth_zip old.prod.case)
qed

definition "psubt_bot_impl R ≡ remdups (map term_to_bot_term (concat (map supt_list R)))"
lemma psubt_bot_impl[simp]: "set (psubt_bot_impl R) = psubt_lhs_bot (set R)"
  by (induct R, auto simp: psubt_bot_impl_def)

definition "states_impl R = List.insert Bot (map the (removeAll None
    (closure_impl (lift_f_total mergeP_impl (↑)) (map Some (psubt_bot_impl R)))))"

lemma states_impl [simp]: "set (states_impl R) = states (set R)"
proof -
  have [simp]: "lift_f_total mergeP_impl (↑) = lift_f_total (λ x y. mergeP_impl x y) (↑)" by blast
  show ?thesis unfolding states_impl_def states_def
    using lift_total.cl.closure_impl
    by (simp add: lift_total.cl.pred_closure_lift_closure) 
qed

abbreviation check_intance_lhs where
  "check_intance_lhs qs f R ≡ list_all (λ u. ¬ bless_eq_impl u (BFun f qs)) R"

definition min_elem where
  "min_elem s ss = (let ts = filter (λ x. bless_eq_impl x s) ss in
      foldr (↑) ts Bot)"

lemma bound_impl [simp, code]:
  "bound_max s (set ss) = min_elem s ss"
proof -
  have [simp]: "{y. lift_total.lifted_less_eq y (Some s) ∧ y ∈ Some ` set ss} = Some ` {x ∈ set ss. x ≤⇩b s}"
    by auto
  then show ?thesis
    using lift_total.supremum_impl[of "filter (λ x. bless_eq_impl x s) ss"]
    using lift_total.supremum_smaller_exists_unique[of "set ss" s]
    by (auto simp: min_elem_def Let_def lift_total.lift_ord.smaller_subset_def)
qed


definition nf_rule_impl where
  "nf_rule_impl S R SR h = (let (f, n) = h in
     let states = List.n_lists n S in
     let nlhs_inst = filter (λ qs. check_intance_lhs qs f R) states in
     map (λ qs. TA_rule f qs (min_elem (BFun f qs) SR)) nlhs_inst)"

abbreviation nf_rules_impl where
  "nf_rules_impl R ℱ ≡ concat (map (nf_rule_impl (states_impl R) (map term_to_bot_term R) (psubt_bot_impl R)) ℱ)"

(* Section proves that the implementation constructs the same rule set *)

lemma nf_rules_in_impl:
  assumes "TA_rule f qs q |∈| nf_rules (fset_of_list R) (fset_of_list ℱ)"
  shows "TA_rule f qs q |∈| fset_of_list (nf_rules_impl R ℱ)"
proof -
  have funas: "(f, length qs) ∈ set ℱ" and st: "fset_of_list qs |⊆| fstates (fset_of_list R)"
   and nlhs: "¬(∃ s ∈ (set R). s⇧⊥ ≤⇩b BFun f qs)"
   and min: "q = bound_max (BFun f qs) (psubt_lhs_bot (set R))"
    using assms by (auto simp add: nf_rules_fmember simp flip: fset_of_list_elem)
  then have st_impl: "qs |∈| fset_of_list (List.n_lists (length qs) (states_impl R))"
    by (auto simp add: fset_of_list_elem subset_code(1) set_n_lists
        fset_of_list.rep_eq less_eq_fset.rep_eq fstates.rep_eq)
  from nlhs have nlhs_impl: "check_intance_lhs qs f (map term_to_bot_term R)"
    by (auto simp: list.pred_set)
  have min_impl: "q = min_elem (BFun f qs) (psubt_bot_impl R)"
    using bound_impl min
    by (auto simp flip: psubt_bot_impl)
  then show ?thesis using funas nlhs_impl funas st_impl unfolding nf_rule_impl_def
    by (auto simp: fset_of_list_elem)
qed


lemma nf_rules_impl_in_rules:
  assumes "TA_rule f qs q |∈| fset_of_list (nf_rules_impl R ℱ)"
  shows "TA_rule f qs q |∈| nf_rules (fset_of_list R) (fset_of_list ℱ)"
proof -
  have funas: "(f, length qs) ∈ set ℱ"
   and st_impl: "qs |∈| fset_of_list (List.n_lists (length qs) (states_impl R))"
   and nlhs_impl: "check_intance_lhs qs f (map term_to_bot_term R)"
   and min: "q = min_elem (BFun f qs) (psubt_bot_impl R)" using assms
    by (auto simp add: set_n_lists nf_rule_impl_def fset_of_list_elem)    
  from st_impl have st: "fset_of_list qs |⊆| fstates (fset_of_list R)"
    by (force simp: set_n_lists fset_of_list_elem fstates.rep_eq fset_of_list.rep_eq)
  from nlhs_impl have nlhs: "¬(∃ l ∈ (set R). l⇧⊥ ≤⇩b BFun f qs)"
    by auto (metis (no_types, lifting) Ball_set_list_all in_set_idx length_map nth_map nth_mem)
  have "q = bound_max (BFun f qs) (psubt_lhs_bot (set R))"
    using bound_impl min
    by (auto simp flip: psubt_bot_impl)
  then show ?thesis using funas st nlhs
    by (auto simp add: nf_rules_fmember fset_of_list_elem fset_of_list.rep_eq)
qed

lemma rule_set_eq:
  shows "nf_rules (fset_of_list R) (fset_of_list ℱ) = fset_of_list (nf_rules_impl R ℱ)" (is "?Ls = ?Rs")
proof -
  {fix r assume "r |∈| ?Ls" then have "r |∈| ?Rs"
      using nf_rules_in_impl[where ?R = R and ?ℱ = ℱ]
      by (cases r) auto}
  moreover
  {fix r assume "r |∈| ?Rs" then have "r |∈| ?Ls"
      using nf_rules_impl_in_rules[where ?R = R and ?ℱ = ℱ]
      by (cases r) auto}
  ultimately show ?thesis by blast
qed

(* Code equation for normal form TA *)

lemma fstates_code[code]:
  "fstates R = fset_of_list (states_impl (sorted_list_of_fset R))"
  by (auto simp: fstates.rep_eq fset_of_list.rep_eq)

lemma nf_ta_code [code]:
  "nf_ta R ℱ = TA (fset_of_list (nf_rules_impl (sorted_list_of_fset R) (sorted_list_of_fset ℱ))) {||}"
  unfolding nf_ta_def using rule_set_eq[of "sorted_list_of_fset R" "sorted_list_of_fset ℱ"]
  by (intro TA_equalityI) auto

(*
export_code nf_ta in Haskell
*)

end