Theory Gen_Iterator

section ‹\isaheader{Iterators}›
theory Gen_Iterator
imports Refine_Monadic.Refine_Monadic Proper_Iterator
begin
  text ‹
    Iterators are realized by to-list functions followed by folding.
    A post-optimization step then replaces these constructions by
    real iterators.›

  lemma param_it_to_list[param]: "(it_to_list,it_to_list) 
    (Rs  (Ra  bool_rel)  
    (Rb  Rblist_rel  Rblist_rel)  Rclist_rel  Rd)  Rs  Rd"
    unfolding it_to_list_def[abs_def]
    by parametricity


  definition key_rel :: "('k  'k  bool)  ('k×'v)  ('k×'v)  bool"
    where "key_rel R a b  R (fst a) (fst b)"

  lemma key_rel_UNIV[simp]: "key_rel (λ_ _. True) = (λ_ _. True)"
    unfolding key_rel_def[abs_def] by auto

  subsection ‹Setup for Autoref›
  text ‹Default pattern rules for it_to_sorted_list›
  definition "set_to_sorted_list R S  it_to_sorted_list R S"
  lemma set_to_sorted_list_itype[autoref_itype]: 
    "set_to_sorted_list R ::i Iii_set i Iii_listii_nres" 
    by simp

context begin interpretation autoref_syn .
  lemma set_to_sorted_list_pat[autoref_op_pat]: 
    "it_to_sorted_list R S  OP (set_to_sorted_list R) S"
    unfolding set_to_sorted_list_def[abs_def] by auto
end

  definition "map_to_sorted_list R M 
     it_to_sorted_list (key_rel R) (map_to_set M)"
  lemma map_to_sorted_list_itype[autoref_itype]:
    "map_to_sorted_list R ::i Rk,Rvii_map i Rk,Rvii_prodii_listii_nres"
    by simp

context begin interpretation autoref_syn .
  lemma map_to_sorted_list_pat[autoref_op_pat]:
    "it_to_sorted_list (key_rel R) (map_to_set M) 
       OP (map_to_sorted_list R) M"
    "it_to_sorted_list (λ_ _. True) (map_to_set M) 
       OP (map_to_sorted_list (λ_ _. True)) M"
    unfolding map_to_sorted_list_def[abs_def] by auto
end

  subsection ‹Set iterators›
  (*definition "is_set_to_sorted_list_deprecated ordR Rk Rs tsl ≡ ∀s s'.
    (s,s')∈⟨Rk⟩Rs ⟶ 
      (RETURN (tsl s),it_to_sorted_list ordR s')∈⟨⟨Rk⟩list_rel⟩nres_rel"
    *)

  definition "is_set_to_sorted_list ordR Rk Rs tsl  s s'.
    (s,s')RkRs 
       ( l'. (tsl s,l')Rklist_rel 
             RETURN l'  it_to_sorted_list ordR s')"

  definition "is_set_to_list  is_set_to_sorted_list (λ_ _. True)"


  lemma is_set_to_sorted_listE:
    assumes "is_set_to_sorted_list ordR Rk Rs tsl"
    assumes "(s,s')RkRs"
    obtains l' where "(tsl s,l')Rklist_rel" 
    and "RETURN l'  it_to_sorted_list ordR s'"
    using assms unfolding is_set_to_sorted_list_def by blast

  (* TODO: Move *)
  lemma it_to_sorted_list_weaken: 
    "RR'  it_to_sorted_list R s  it_to_sorted_list R' s"
    unfolding it_to_sorted_list_def
    by (auto intro!: sorted_wrt_mono_rel[where P=R])

  lemma set_to_list_by_set_to_sorted_list[autoref_ga_rules]:
    assumes "GEN_ALGO_tag (is_set_to_sorted_list ordR Rk Rs tsl)"
    shows "is_set_to_list Rk Rs tsl"
    using assms
    unfolding is_set_to_list_def is_set_to_sorted_list_def autoref_tag_defs
    apply (safe)
    apply (drule spec, drule spec, drule (1) mp)
    apply (elim exE conjE)
    apply (rule exI, rule conjI, assumption)
    apply (rule order_trans, assumption)
    apply (rule it_to_sorted_list_weaken)
    by blast


  definition "det_fold_set R c f σ result  
    l. distinct l  sorted_wrt R l  foldli l c f σ = result (set l)"

  lemma det_fold_setI[intro?]:
    assumes "l. distinct l; sorted_wrt R l 
       foldli l c f σ = result (set l)"
    shows "det_fold_set R c f σ result"
    using assms unfolding det_fold_set_def by auto

  text ‹Template lemma for generic algorithm using set iterator›
  lemma det_fold_sorted_set:
    assumes 1: "det_fold_set ordR c' f' σ' result"
    assumes 2: "is_set_to_sorted_list ordR Rk Rs tsl"
    assumes SREF[param]: "(s,s')RkRs"
    assumes [param]:  "(c,c')Id"
    assumes [param]: "(f,f')Rk    "
    assumes [param]: "(σ,σ')"
    shows "(foldli (tsl s) c f σ, result s')  "
  proof -
    obtain tsl' where
      [param]: "(tsl s,tsl')  Rklist_rel" 
      and IT: "RETURN tsl'  it_to_sorted_list ordR s'"
      using 2 SREF
      by (rule is_set_to_sorted_listE)
    
    have "(foldli (tsl s) c f σ, foldli tsl' c' f' σ')  "
      by parametricity
    also have "foldli tsl' c' f' σ' = result s'"
      using 1 IT 
      unfolding det_fold_set_def it_to_sorted_list_def
      by simp
    finally show ?thesis .
  qed

  lemma det_fold_set:
    assumes "det_fold_set (λ_ _. True) c' f' σ' result"
    assumes "is_set_to_list Rk Rs tsl"
    assumes "(s,s')RkRs"
    assumes "(c,c')Id"
    assumes "(f,f')Rk    "
    assumes "(σ,σ')"
    shows "(foldli (tsl s) c f σ, result s')  "
    using assms
    unfolding  is_set_to_list_def
    by (rule det_fold_sorted_set)

  subsection ‹Map iterators›

  text ‹Build relation on keys›
  
  (*definition "is_map_to_sorted_list_deprecated ordR Rk Rv Rm tsl ≡ ∀m m'.
    (m,m')∈⟨Rk,Rv⟩Rm ⟶ 
      (RETURN (tsl m),it_to_sorted_list (key_rel ordR) (map_to_set m'))
      ∈⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩nres_rel"*)

  definition "is_map_to_sorted_list ordR Rk Rv Rm tsl  m m'.
    (m,m')Rk,RvRm  (
      l'. (tsl m,l')Rk,Rvprod_rellist_rel
         RETURN l'  it_to_sorted_list (key_rel ordR) (map_to_set m'))"

  definition "is_map_to_list Rk Rv Rm tsl 
     is_map_to_sorted_list (λ_ _. True) Rk Rv Rm tsl"

  lemma is_map_to_sorted_listE:
    assumes "is_map_to_sorted_list ordR Rk Rv Rm tsl"
    assumes "(m,m')Rk,RvRm"
    obtains l' where "(tsl m,l')Rk,Rvprod_rellist_rel" 
    and "RETURN l'  it_to_sorted_list (key_rel ordR) (map_to_set m')"
    using assms unfolding is_map_to_sorted_list_def by blast

  lemma map_to_list_by_map_to_sorted_list[autoref_ga_rules]:
    assumes "GEN_ALGO_tag (is_map_to_sorted_list ordR Rk Rv Rm tsl)"
    shows "is_map_to_list Rk Rv Rm tsl"
    using assms
    unfolding is_map_to_list_def is_map_to_sorted_list_def autoref_tag_defs
    apply (safe)
    apply (drule spec, drule spec, drule (1) mp)
    apply (elim exE conjE)
    apply (rule exI, rule conjI, assumption)
    apply (rule order_trans, assumption)
    apply (rule it_to_sorted_list_weaken)
    unfolding key_rel_def[abs_def]
    by blast

  definition "det_fold_map R c f σ result  
    l. distinct (map fst l)  sorted_wrt (key_rel R) l 
       foldli l c f σ = result (map_of l)"

  lemma det_fold_mapI[intro?]:
    assumes "l. distinct (map fst l); sorted_wrt (key_rel R) l 
       foldli l c f σ = result (map_of l)"
    shows "det_fold_map R c f σ result"
    using assms unfolding det_fold_map_def by auto

  lemma det_fold_map_aux:
    assumes 1: "distinct (map fst l); sorted_wrt (key_rel R) l 
       foldli l c f σ = result (map_of l)"
    assumes 2: "RETURN l  it_to_sorted_list (key_rel R) (map_to_set m)"
    shows "foldli l c f σ = result m"
  proof -
    from 2 have "distinct l" and "set l = map_to_set m" 
      and SORTED: "sorted_wrt (key_rel R) l"
      unfolding it_to_sorted_list_def by simp_all
    hence "(k,v)set l. (k',v')set l. k=k'  v=v'"
      apply simp
      unfolding map_to_set_def
      apply auto
      done
    with distinct l have DF: "distinct (map fst l)"
      apply (induct l)
      apply simp
      apply force
      done
    with set l = map_to_set m have [simp]: "m = map_of l"
      by (metis map_of_map_to_set)
      
    from 1[OF DF SORTED] show ?thesis by simp
  qed
    
  text ‹Template lemma for generic algorithm using map iterator›
  lemma det_fold_sorted_map:
    assumes 1: "det_fold_map ordR c' f' σ' result"
    assumes 2: "is_map_to_sorted_list ordR Rk Rv Rm tsl"
    assumes MREF[param]: "(m,m')Rk,RvRm"
    assumes [param]:  "(c,c')Id"
    assumes [param]: "(f,f')Rk,Rvprod_rel    "
    assumes [param]: "(σ,σ')"
    shows "(foldli (tsl m) c f σ, result m')  "
  proof -
    obtain tsl' where
      [param]: "(tsl m,tsl')  Rk,Rvprod_rellist_rel" 
      and IT: "RETURN tsl'  it_to_sorted_list (key_rel ordR) (map_to_set m')"
      using 2 MREF by (rule is_map_to_sorted_listE)
    
    have "(foldli (tsl m) c f σ, foldli tsl' c' f' σ')  "
      by parametricity
    also have "foldli tsl' c' f' σ' = result m'"
      using det_fold_map_aux[of tsl' ordR c' f' σ' result] 1 IT
      unfolding det_fold_map_def
      by clarsimp
    finally show ?thesis .
  qed

  lemma det_fold_map:
    assumes "det_fold_map (λ_ _. True) c' f' σ' result"
    assumes "is_map_to_list Rk Rv Rm tsl"
    assumes "(m,m')Rk,RvRm"
    assumes "(c,c')Id"
    assumes "(f,f')Rk,Rvprod_rel    "
    assumes "(σ,σ')"
    shows "(foldli (tsl m) c f σ, result m')  "
    using assms
    unfolding is_map_to_list_def
    by (rule det_fold_sorted_map)

lemma set_to_sorted_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 11)"
  assumes TSL: "SIDE_GEN_ALGO (is_set_to_sorted_list R Rk Rs tsl)"
  shows "(λs. RETURN (tsl s), set_to_sorted_list R) 
     RkRs  Rklist_relnres_rel"
proof (intro fun_relI nres_relI)
  fix s s'
  assume "(s,s')RkRs"
  with TSL obtain l' where 
    R1: "(tsl s, l')  Rklist_rel" 
      and R2: "RETURN l'  set_to_sorted_list R s'"
    unfolding is_set_to_sorted_list_def set_to_sorted_list_def autoref_tag_defs
    by blast
  
  have "RETURN (tsl s)  (Rklist_rel) (RETURN l')"
    by (rule RETURN_refine) fact
  also note R2
  finally show "RETURN (tsl s)   (Rklist_rel) (set_to_sorted_list R s')" .
qed

lemma set_to_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 10)"
  assumes TSL: "SIDE_GEN_ALGO (is_set_to_list Rk Rs tsl)"
  shows "(λs. RETURN (tsl s), set_to_sorted_list (λ_ _. True)) 
     RkRs  Rklist_relnres_rel"
  using assms(2-) unfolding is_set_to_list_def
  by (rule set_to_sorted_list_by_tsl[OF PRIO_TAGI])

lemma map_to_sorted_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 11)"
  assumes TSL: "SIDE_GEN_ALGO (is_map_to_sorted_list R Rk Rv Rs tsl)"
  shows "(λs. RETURN (tsl s), map_to_sorted_list R) 
     Rk,RvRs  Rk,Rvprod_rellist_relnres_rel"
proof (intro fun_relI nres_relI)
  fix s s'
  assume "(s,s')Rk,RvRs"
  with TSL obtain l' where 
    R1: "(tsl s, l')  Rk,Rvprod_rellist_rel" 
      and R2: "RETURN l'  map_to_sorted_list R s'"
    unfolding is_map_to_sorted_list_def map_to_sorted_list_def autoref_tag_defs
    by blast
  
  have "RETURN (tsl s)  (Rk,Rvprod_rellist_rel) (RETURN l')"
    apply (rule RETURN_refine)
    by fact
  also note R2
  finally show 
    "RETURN (tsl s)   (Rk,Rvprod_rellist_rel) (map_to_sorted_list R s')" .
qed

lemma map_to_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 10)"
  assumes TSL: "SIDE_GEN_ALGO (is_map_to_list Rk Rv Rs tsl)"
  shows "(λs. RETURN (tsl s), map_to_sorted_list (λ_ _. True)) 
     Rk,RvRs  Rk,Rvprod_rellist_relnres_rel"
  using assms(2-) unfolding is_map_to_list_def
  by (rule map_to_sorted_list_by_tsl[OF PRIO_TAGI])


(*lemma dres_it_FOREACH_it_simp[iterator_simps]: 
  "dres_it_FOREACH (λs. dRETURN (i s)) s c f σ 
    = foldli (i s) (case_dres False False c) (λx s. s ⤜ f x) (dRETURN σ)"
  unfolding dres_it_FOREACH_def
  by simp
*)

text ‹
  TODO/FIXME: 
    * Integrate mono-prover properly into solver-infrastructure,
        i.e. tag a mono-goal.
    * Tag iterators, such that, for the mono-prover, we can just convert
        a proper iterator back to its foldli-equivalent!
›
lemma proper_it_mono_dres_pair:
  assumes PR: "proper_it' it it'"
  assumes A: "k v x. f k v x  f' k v x"
  shows "
    it' s (case_dres False False c) (λ(k,v) s. s  f k v) σ
     it' s (case_dres False False c) (λ(k,v) s. s  f' k v) σ" (is "?a  ?b")
proof -
  from proper_itE[OF PR[THEN proper_it'D]] obtain l where 
    A_FMT: 
      "?a = foldli l (case_dres False False c) (λ(k,v) s. s  f k v) σ" 
        (is "_ = ?a'")
    and B_FMT: 
      "?b = foldli l (case_dres False False c) (λ(k,v) s. s  f' k v) σ" 
        (is "_ = ?b'")
    by metis
  
  from A have A': "kv x. case_prod f kv x  case_prod f' kv x"
    by auto

  note A_FMT
  also have 
    "?a' = foldli l (case_dres False False c) (λkv s. s  case_prod f kv) σ"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note foldli_mono_dres[OF A']
  also have 
    "foldli l (case_dres False False c) (λkv s. s  case_prod f' kv) σ = ?b'"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note B_FMT[symmetric]
  finally show ?thesis .
qed

lemma proper_it_mono_dres_pair_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "k v x. flat_ge (f k v x) (f' k v x)"
  shows "
    flat_ge (it' s (case_dres False False c) (λ(k,v) s. s  f k v) σ)
      (it' s (case_dres False False c) (λ(k,v) s. s  f' k v) σ)" 
      (is "flat_ge ?a ?b")
proof -
  from proper_itE[OF PR[THEN proper_it'D]] obtain l where 
    A_FMT: 
      "?a = foldli l (case_dres False False c) (λ(k,v) s. s  f k v) σ" 
        (is "_ = ?a'")
    and B_FMT: 
      "?b = foldli l (case_dres False False c) (λ(k,v) s. s  f' k v) σ" 
        (is "_ = ?b'")
    by metis
  
  from A have A': "kv x. flat_ge (case_prod f kv x) (case_prod f' kv x)"
    by auto

  note A_FMT
  also have 
    "?a' = foldli l (case_dres False False c) (λkv s. s  case_prod f kv) σ"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note foldli_mono_dres_flat[OF A']
  also have 
    "foldli l (case_dres False False c) (λkv s. s  case_prod f' kv) σ = ?b'"
    apply (fo_rule fun_cong)
    apply (fo_rule arg_cong)
    by auto
  also note B_FMT[symmetric]
  finally show ?thesis .
qed

    
lemma proper_it_mono_dres:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. f kv x  f' kv x"
  shows "
    it' s (case_dres False False c) (λkv s. s  f kv) σ
     it' s (case_dres False False c) (λkv s. s  f' kv) σ"
  apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
  apply (erule_tac t="it' s" in ssubst)
  apply (rule foldli_mono_dres[OF A])
  done

lemma proper_it_mono_dres_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. flat_ge (f kv x) (f' kv x)"
  shows "
    flat_ge (it' s (case_dres False False c) (λkv s. s  f kv) σ)
      (it' s (case_dres False False c) (λkv s. s  f' kv) σ)"
  apply (rule proper_itE[OF PR[THEN proper_it'D[where s=s]]])
  apply (erule_tac t="it' s" in ssubst)
  apply (rule foldli_mono_dres_flat[OF A])
  done

lemma pi'_dom[icf_proper_iteratorI]: "proper_it' it it' 
   proper_it' (map_iterator_dom o it) (map_iterator_dom o it')"
  apply (rule proper_it'I)
  apply (simp add: comp_def)
  apply (rule icf_proper_iteratorI)
  apply (erule proper_it'D)
  done

lemma proper_it_mono_dres_dom:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. f kv x  f' kv x"
  shows "
    (map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f kv) σ
     
    (map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f' kv) σ"
  
  apply (rule proper_it_mono_dres)
  apply (rule icf_proper_iteratorI)
  by fact+

lemma proper_it_mono_dres_dom_flat:
  assumes PR: "proper_it' it it'"
  assumes A: "kv x. flat_ge (f kv x) (f' kv x)"
  shows "flat_ge 
    ((map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f kv) σ)
    ((map_iterator_dom o it') s (case_dres False False c) (λkv s. s  f' kv) σ)"
  apply (rule proper_it_mono_dres_flat)
  apply (rule icf_proper_iteratorI)
  by fact+


(* TODO/FIXME: Hack! Mono-prover should be able to find proper-iterators itself
*)
lemmas proper_it_monos = 
  proper_it_mono_dres_pair proper_it_mono_dres_pair_flat
  proper_it_mono_dres proper_it_mono_dres_flat
  proper_it_mono_dres_dom proper_it_mono_dres_dom_flat

(* TODO: Conceptually, this leads to some kind of bundles: 
  Each bundle has a list of processors, that are invoked for every registered
  theorem. *)


attribute_setup "proper_it" = Scan.succeed (Thm.declaration_attribute (fn thm => fn context => 
    let
      val mono_thms = map_filter (try (curry (RS) thm)) @{thms proper_it_monos}
      (*val mono_thms = map (fn mt => thm RS mt) @{thms proper_it_monos}*)
      val context = context 
        |> Icf_Proper_Iterator.add_thm thm
        |> fold Refine_Mono_Prover.add_mono_thm mono_thms
    in
      context
    end
  ))
  "Proper iterator declaration"

end