Theory RefineG_Transfer

header {* \isaheader{Transfer between Domains} *}
theory RefineG_Transfer
imports "../Refine_Misc"
begin
  text {* Currently, this theory is specialized to 
    transfers that include no data refinement.
    *}

ML {*
structure RefineG_Transfer = struct
  structure transfer = Named_Thms
    ( val name = @{binding refine_transfer}
      val description = "Refinement Framework: " ^ 
        "Transfer rules" );

  fun transfer_tac thms ctxt i st = let 
    val thms = thms @ transfer.get ctxt;
    val ss = HOL_basic_ss addsimps @{thms nested_prod_case_simp}
  in
    REPEAT_DETERM1 (
      COND (has_fewer_prems (nprems_of st)) no_tac (
        FIRST [
          Method.assm_tac ctxt i,
          resolve_tac thms i,
          Refine_Misc.triggered_mono_tac ctxt i,
          CHANGED_PROP (simp_tac ss i)]
      )) st
  end
  
end
*}

setup {* RefineG_Transfer.transfer.setup *}
method_setup refine_transfer = 
  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD'
    (RefineG_Transfer.transfer_tac thms ctxt)) 
  *} "Invoke transfer rules"


locale transfer = fixes α :: "'c => 'a::complete_lattice"
begin

text {*
  In the following, we define some transfer lemmas for general
  HOL - constructs.
*}

lemma transfer_if[refine_transfer]:
  assumes "b ==> α s1 ≤ S1"
  assumes "¬b ==> α s2 ≤ S2"
  shows "α (if b then s1 else s2) ≤ (if b then S1 else S2)"
  using assms by auto

lemma transfer_prod[refine_transfer]:
  assumes "!!a b. α (f a b) ≤ F a b"
  shows "α (prod_case f x) ≤ (prod_case F x)"
  using assms by (auto split: prod.split)

lemma transfer_Let[refine_transfer]:
  assumes "!!x. α (f x) ≤ F x"
  shows "α (Let x f) ≤ Let x F"
  using assms by auto

lemma transfer_option[refine_transfer]:
  assumes "α fa ≤ Fa"
  assumes "!!x. α (fb x) ≤ Fb x"
  shows "α (option_case fa fb x) ≤ option_case Fa Fb x"
  using assms by (auto split: option.split)

end

text {* Transfer into complete lattice structure *}
locale ordered_transfer = transfer + 
  constrains α :: "'c::complete_lattice => 'a::complete_lattice"

text {* Transfer into complete lattice structure with distributive
  transfer function. *}
locale dist_transfer = ordered_transfer + 
  constrains α :: "'c::complete_lattice => 'a::complete_lattice"
  assumes α_dist: "!!A. is_chain A ==> α (Sup A) = Sup (α`A)"
begin
  lemma α_mono[simp, intro!]: "mono α"
    apply rule
    apply (subgoal_tac "is_chain {x,y}")
    apply (drule α_dist)
    apply (auto simp: le_iff_sup) []
    apply (rule chainI)
    apply auto
    done

  lemma α_strict[simp]: "α bot = bot"
    using α_dist[of "{}"] by simp
end


text {* Transfer into ccpo *}
locale ccpo_transfer = transfer α for
  α :: "'c::ccpo => 'a::complete_lattice" 

text {* Transfer into ccpo with distributive
  transfer function. *}
locale dist_ccpo_transfer = ccpo_transfer α
  for α :: "'c::ccpo => 'a::complete_lattice" + 
  assumes α_dist: "!!A. is_chain A ==> α (Sup A) = Sup (α`A)"
begin

  lemma α_mono[simp, intro!]: "mono α"
  proof
    fix x y :: 'c
    assume LE: "x≤y"
    hence C[simp, intro!]: "is_chain {x,y}" by (auto intro: chainI)
    from LE have "α x ≤ sup (α x) (α y)" by simp
    also have "… = Sup (α`{x,y})" by simp
    also have "… = α (Sup {x,y})"
      by (rule α_dist[symmetric]) simp
    also have "Sup {x,y} = y"
      apply (rule antisym)
      apply (rule ccpo_Sup_least[OF C]) using LE apply auto []
      apply (rule ccpo_Sup_upper[OF C]) by auto
    finally show "α x ≤ α y" .
  qed

  lemma α_strict[simp]: "α (Sup {}) = bot"
    using α_dist[of "{}"] by simp
end

end