Theory Sepref_Translate

section ‹Translation›
theory Sepref_Translate
imports 
  Sepref_Monadify 
  Sepref_Constraints 
  Sepref_Conc_Post
  Sepref_Frame 
  Sepref_Rules 
  Sepref_Combinator_Setup
  "../lib/More_Eisbach_Tools"
  "Lib/User_Smashing"
begin


text ‹
  This theory defines the translation phase.
  
  The main functionality of the translation phase is to
  apply refinement rules. Thereby, the linearity information is
  exploited to create copies of parameters that are still required, but
  would be destroyed by a synthesized operation.
  These \emph{frame-based} rules are in the named theorem collection
  @{text sepref_fr_rules}, and the collection @{text sepref_copy_rules}
  contains rules to handle copying of parameters.

  Apart from the frame-based rules described above, there is also a set of
  rules for combinators, in the collection @{text sepref_comb_rules}, 
  where no automatic copying of parameters is applied.

  Moreover, this theory contains 
  \begin{itemize}
    \item A setup for the  basic monad combinators and recursion.
    \item A tool to import parametricity theorems.
    \item Some setup to identify pure refinement relations, i.e., those not
      involving the heap.
    \item A preprocessor that identifies parameters in refinement goals,
      and flags them with a special tag, that allows their correct handling.
  \end{itemize}
›


text ‹Tag to keep track of abstract bindings. 
  Required to recover information for side-condition solving.›
definition "bind_ref_tag x m ≡ RETURN x ≤ m"


text ‹Tag to keep track of preconditions in assertions›
definition "vassn_tag Γ ≡ ∃h. Γ h"

lemma vassn_tagI: "Γ h ⟹ vassn_tag Γ" 
  unfolding vassn_tag_def ..

lemma vassn_dest[dest!]:
  "vassn_tag (Γ1 ** Γ2) ⟹ vassn_tag Γ1 ∧ vassn_tag Γ2"
  "vassn_tag (hn_ctxt R a b) ⟹ rdomp R a"
  "vassn_tag (↑Φ) ⟹ Φ"
  unfolding vassn_tag_def hn_ctxt_def rdomp_def[abs_def]
  by (auto simp: sep_conj_def pred_lift_extract_simps)

lemma entails_preI:
  assumes "vassn_tag A ⟹ A ⊢ B"
  shows "A ⊢ B"
  using assms
  by (auto simp: entails_def vassn_tag_def)

lemma invalid_assn_const: 
  "invalid_assn (λ_ _. P) x y = ↑(vassn_tag P)"
  by (simp_all add: invalid_assn_def vassn_tag_def pure_part_def)

lemma vassn_tag_simps[simp]: 
  "vassn_tag □"
  "vassn_tag sep_true"
  by (auto simp: vassn_tag_def)

lemma hn_refine_vassn_tagI: 
  "⟦ vassn_tag Γ ⟹ hn_refine Γ c Γ' R CP a ⟧ ⟹ hn_refine Γ c Γ' R CP a"  
  apply (rule hn_refine_preI)
  by (auto simp: vassn_tag_def)
  
  
definition "GEN_ALGO f Φ ≡ Φ f"
― ‹Tag to synthesize @{term f} with property @{term Φ}.›

lemma is_GEN_ALGO: "GEN_ALGO f Φ ⟹ GEN_ALGO f Φ" .

named_theorems_rev sepref_gen_algo_rules ‹Sepref: Generic algorithm rules›


text ‹Tag for side-condition solver to discharge by assumption›
definition RPREM :: "bool ⇒ bool" where [simp]: "RPREM P = P"
lemma RPREMI: "P ⟹ RPREM P" by simp

lemma trans_frame_rule:
  assumes "RECOVER_PURE Γ Γ'"
  assumes "vassn_tag (Γ'**F) ⟹ hn_refine Γ' c Γ'' R CP a"
  shows "hn_refine (Γ**F) c (Γ''**F) R CP a"
  apply (rule hn_refine_vassn_tagI)
  apply (rule hn_refine_frame[OF _ entails_refl])
  applyF (rule hn_refine_cons_pre)
    focus using assms(1) unfolding RECOVER_PURE_def apply assumption solved
    
    apply1 (rule assms)
    applyS (metis RECOVER_PURE_def assms(1) entails_eq_iff entails_preI frame_thms(2))
  solved
  done

lemma recover_pure_cons: ― ‹Used for debugging›
  assumes "RECOVER_PURE Γ Γ'"
  assumes "hn_refine Γ' c Γ'' R CP a"
  shows "hn_refine (Γ) c (Γ'') R CP a"
  using trans_frame_rule[where F=□, OF assms] by simp


― ‹Tag to align structure of refinement assertions for consequence rule›
definition CPR_TAG :: "assn ⇒ assn ⇒ bool" where [simp]: "CPR_TAG y x ≡ True"
lemma CPR_TAG_starI:
  assumes "CPR_TAG P1 Q1"
  assumes "CPR_TAG P2 Q2"
  shows "CPR_TAG (P1**P2) (Q1**Q2)"
  by simp
lemma CPR_tag_ctxtI: "CPR_TAG (hn_ctxt R x xi) (hn_ctxt R' x xi)" by simp
lemma CPR_tag_fallbackI: "CPR_TAG P Q" by simp

lemmas CPR_TAG_rules = CPR_TAG_starI CPR_tag_ctxtI CPR_tag_fallbackI

lemma cons_pre_rule: ― ‹Consequence rule to be applied if no direct operation rule matches›
  assumes "CPR_TAG P P'"
  assumes "P ⊢ P'"
  assumes "hn_refine P' c Q R CP m"
  shows "hn_refine P c Q R CP m"
  using assms(2-) by (rule hn_refine_cons_pre)


― ‹Bounds-Solver›

named_theorems_rev sepref_bounds_dest ‹Bounds solver drules›
named_theorems_rev sepref_bounds_simps ‹Bounds solver simp rules›

ML ‹

structure Sepref_Translate = struct

  val cfg_debug = 
    Attrib.setup_config_bool @{binding sepref_debug_translate} (K false)
  
  val dbg_msg_tac = Sepref_Debugging.dbg_msg_tac cfg_debug  

  fun check_side_conds thm = let
    open Sepref_Basic
    (* Check that term is no binary operator on assertions *)
    fun is_atomic (Const (_,@{typ "assn⇒assn⇒assn"})$_$_) = false
      | is_atomic _ = true

    val is_atomic_star_list = ("Expected atoms separated by star",forall is_atomic o strip_star)

    val is_trueprop = ("Expected Trueprop conclusion",can HOLogic.dest_Trueprop)

    fun assert t' (msg,p) t = if p t then () else raise TERM(msg,[t',t])

    fun chk_prem t = let
      val assert = assert t
      
      fun chk @{mpat "MERGE ?l _ ?r _ ?m"} = (
            assert is_atomic_star_list l;
            assert is_atomic_star_list r;
            assert is_atomic_star_list m
          )
        | chk @{mpat "?l ⊢ ?r"} = (
            assert is_atomic_star_list l;
            assert is_atomic_star_list r
          )
        | chk _ = ()  

      val t = Logic.strip_assums_concl t 
    in
      assert is_trueprop t;
      chk (HOLogic.dest_Trueprop t)
    end    

  in
    map chk_prem (Thm.prems_of thm)
  end

  structure sepref_comb_rules = Named_Sorted_Thms (
    val name = @{binding "sepref_comb_rules"}
    val description = "Sepref: Combinator rules"
    val sort = K I
    fun transform _ thm = let
      val _ = check_side_conds thm  
    in
      [thm]
    end
  )

  structure sepref_fr_rules = Named_Sorted_Thms (
    val name = @{binding "sepref_fr_rules"}
    val description = "Sepref: Frame-based rules"
    val sort = K I
    fun transform context thm = let
      val ctxt = Context.proof_of context
      val thm = Sepref_Rules.ensure_hnr ctxt thm
        |> Conv.fconv_rule (Sepref_Frame.align_rl_conv ctxt)

      val _ = check_side_conds thm  
      val _ = case try (Sepref_Rules.analyze_hnr ctxt) thm of 
          NONE =>
            (Pretty.block [
              Pretty.str "hnr-analysis failed", 
              Pretty.str ":", 
              Pretty.brk 1, 
              Thm.pretty_thm ctxt thm])
            |> Pretty.string_of |> error  
        | SOME ana => let
            val _ = Sepref_Combinator_Setup.is_valid_abs_op ctxt (fst (#ahead ana))
              orelse Pretty.block [
                Pretty.str "Invalid abstract head:",
                Pretty.brk 1,
                Pretty.enclose "(" ")" [Syntax.pretty_term ctxt (fst (#ahead ana))],
                Pretty.brk 1,
                Pretty.str "in thm",
                Pretty.brk 1,
                Thm.pretty_thm ctxt thm                
              ]
            |> Pretty.string_of |> error  
          in () end
    in
      [thm]
    end
  )

  (***** Side Condition Solving *)
  local
    open Sepref_Basic
  in
  
    fun side_unfold_tac ctxt = let
      (*val ctxt = put_simpset HOL_basic_ss ctxt
        addsimps sepref_prep_side_simps.get ctxt*)
    in
      CONVERSION (Id_Op.unprotect_conv ctxt)
      THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms bind_ref_tag_def})
      THEN' TRY o (hyp_subst_tac ctxt)
      (*THEN' asm_full_simp_tac ctxt*)
    end
  
    (* TODO: Not accessible as single ML function? *)
    fun linarith_tac ctxt = 
      Method.insert_tac ctxt (rev (Named_Theorems.get ctxt named_theorems‹arith›))
      THEN' Lin_Arith.tac ctxt
    
    fun bounds_tac ctxt = let
      val ctxt = ctxt 
        addSDs Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_bounds_dest}
        addsimps Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_bounds_simps}
    in
      TRADE (fn ctxt => 
        SELECT_GOAL (auto_tac ctxt)
        THEN_ALL_NEW TRY o linarith_tac ctxt
      ) ctxt
    end
    
    fun side_fallback_tac ctxt = 
      side_unfold_tac ctxt 
      THEN' (
        TRADE (SELECT_GOAL o auto_tac) ctxt
        THEN_ALL_NEW (TRY o SOLVED' (bounds_tac ctxt))
      )
  
    val side_frame_tac = Sepref_Frame.frame_tac side_fallback_tac
    val side_merge_tac = Sepref_Frame.merge_tac side_fallback_tac
    val side_free_tac = Sepref_Frame.free_tac side_fallback_tac
    
    
    fun side_constraint_tac ctxt = Sepref_Constraints.constraint_tac ctxt
    
    val pf_mono_tac = Subgoal.FOCUS_PREMS (fn {context=ctxt,...} => CHANGED (ALLGOALS (Partial_Function.mono_tac ctxt)))
    
    fun side_mono_tac ctxt = side_unfold_tac ctxt THEN' TRADE pf_mono_tac ctxt
  
    fun side_gen_algo_tac ctxt = 
      side_unfold_tac ctxt
      THEN' resolve_tac ctxt (Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_gen_algo_rules})
  
    fun side_pref_def_tac ctxt = 
      side_unfold_tac ctxt THEN' 
      TRADE (fn ctxt => 
        resolve_tac ctxt @{thms PREFER_tagI DEFER_tagI} 
        THEN' (Sepref_Debugging.warning_tac' "Obsolete PREFER/DEFER side condition" ctxt THEN' Tagged_Solver.solve_tac ctxt)
      ) ctxt


    fun side_rprem_tac ctxt = 
      resolve_tac ctxt @{thms RPREMI} THEN' Refine_Util.rprems_tac ctxt
      THEN' (K (smash_new_rule ctxt))

    (*
      Solve side condition, or invoke hnr_tac on hn_refine goal.

      In debug mode, side-condition solvers are allowed to not completely solve 
      the side condition, but must change the goal.
    *)  
    fun side_cond_dispatch_tac dbg hnr_tac ctxt = let
      fun MK tac = if dbg then CHANGED o tac ctxt else SOLVED' (tac ctxt)

      val t_merge = MK side_merge_tac
      val t_frame = MK side_frame_tac
      val t_free = MK side_free_tac
      val t_indep = MK Indep_Vars.indep_tac
      val t_constraint = MK side_constraint_tac
      val t_mono = MK side_mono_tac
      val t_pref_def = MK side_pref_def_tac
      val t_rprem = MK side_rprem_tac
      val t_gen_algo = side_gen_algo_tac ctxt
      val t_cp_cond = MK (apply_method_noargs @{method cp_solve_cond})
      val t_cp_simplify = MK (apply_method_noargs @{method cp_simplify})
      
      val t_fallback = MK side_fallback_tac
    in
      WITH_concl 
        (fn @{mpat "Trueprop ?t"} => (case t of
              @{mpat "MERGE _ _ _ _ _"} => t_merge
            | @{mpat "MK_FREE _ _"} => t_free
            | @{mpat "_ ⊢ _"} => t_frame
            | @{mpat "INDEP _"} => t_indep     (* TODO: Get rid of this!? *)
            | @{mpat "CONSTRAINT _ _"} => t_constraint
            | @{mpat "monotone _ _ _"} => t_mono
            | @{mpat "∀_. monotone _ _ _"} => t_mono
            | @{mpat "PREFER_tag _"} => t_pref_def
            | @{mpat "DEFER_tag _"} => t_pref_def
            | @{mpat "RPREM _"} => t_rprem
            | @{mpat "GEN_ALGO _ _"} => t_gen_algo
            | @{mpat "CP_cond _"} => t_cp_cond           
            | @{mpat "CP_simplify _ _"} => t_cp_simplify
            | @{mpat "hn_refine _ _ _ _ _ _"} => hnr_tac 
            | _ => t_fallback
          )
        | _ => K no_tac  
      )
    end

  end  

  (***** Main Translation Tactic *)
  local
    open Sepref_Basic STactical

    (* ATTENTION: Beware of evaluation order, as some initialization operations on
      context are expensive, and should not be repeated during proof search! *)
  in


    (* Translate combinator, yields new translation goals and side conditions
      which must be processed in order. *)
    fun trans_comb_tac ctxt = let
      val comb_rl_net = sepref_comb_rules.get ctxt
        |> Tactic.build_net

    in
      DETERM o (
        resolve_from_net_tac ctxt comb_rl_net 
        (*ORELSE' (
          Sepref_Frame.norm_goal_pre_tac ctxt 
          THEN' resolve_from_net_tac ctxt comb_rl_net
        )*)
      )
    end

    (* Translate operator. Only succeeds if it finds an operator rule such that
      all resulting side conditions can be solved. Takes the first such rule.

      In debug mode, it returns a sequence of the unsolved side conditions of
      each applicable rule.
    *)
    fun gen_trans_op_tac dbg ctxt = let
      val fr_rl_net = sepref_fr_rules.get ctxt |> Tactic.build_net
      val fr_rl_tac = 
        resolve_from_net_tac ctxt fr_rl_net (* Try direct match *)
        ORELSE' (
          Sepref_Frame.norm_goal_pre_tac ctxt (* Normalize precondition *) 
          THEN' (
            resolve_from_net_tac ctxt fr_rl_net
            ORELSE' (
              resolve_tac ctxt @{thms cons_pre_rule} (* Finally, generate a frame condition *)
              THEN_ALL_NEW_LIST [
                SOLVED' (REPEAT_ALL_NEW_FWD (DETERM o resolve_tac ctxt @{thms CPR_TAG_rules})),
                K all_tac,  (* Frame remains unchanged as first goal, even if fr_rl creates side-conditions *)
                resolve_from_net_tac ctxt fr_rl_net
              ]
            )
          )  
        )
      
      val side_tac = REPEAT_ALL_NEW_FWD (side_cond_dispatch_tac false (K no_tac) ctxt)

      val fr_tac = 
        if dbg then (* Present all possibilities with (partially resolved) side conditions *)
          fr_rl_tac THEN_ALL_NEW_FWD (TRY o side_tac)
        else (* Choose first rule that solves all side conditions *)
          DETERM o SOLVED' (fr_rl_tac THEN_ALL_NEW_FWD (SOLVED' side_tac))

    in
      PHASES' [
        ("Align goal",Sepref_Frame.align_goal_tac, 0),
        ("Frame rule",fn ctxt => resolve_tac ctxt @{thms trans_frame_rule}, 1),
        (* RECOVER_PURE goal *)
        ("Recover pure",Sepref_Frame.recover_pure_tac, ~1),
        (* hn-refine goal with stripped precondition *)
        ("Apply rule",K fr_tac,~1)
      ] (flag_phases_ctrl ctxt dbg) ctxt
    end

    (* Translate combinator, operator, or side condition. *)
    fun gen_trans_step_tac dbg ctxt = side_cond_dispatch_tac dbg
      ( Sepref_Frame.norm_goal_pre_tac ctxt 
        THEN' (trans_comb_tac ctxt ORELSE' gen_trans_op_tac dbg ctxt))
      ctxt

    val trans_step_tac = gen_trans_step_tac false  
    val trans_step_keep_tac = gen_trans_step_tac true

    fun gen_trans_tac dbg ctxt = 
      PHASES' [
        ("Translation steps",REPEAT_DETERM' o trans_step_tac,~1),
        ("Constraint solving",fn ctxt => fn _ => Sepref_Constraints.process_constraint_slot ctxt, 0)
      ] (flag_phases_ctrl ctxt dbg) ctxt

    val trans_tac = gen_trans_tac false  
    val trans_keep_tac = gen_trans_tac true


  end


  val setup = I
    #> sepref_fr_rules.setup
    #> sepref_comb_rules.setup


end

›

setup Sepref_Translate.setup

method_setup sepref_bounds = ‹SIMPLE_METHOD_NOPARAM' (Sepref_Translate.bounds_tac)›


subsubsection ‹Basic Setup›
              
lemma hn_pass[sepref_fr_rules]:
  shows "hn_refine (hn_ctxt P x x') (Mreturn x') (hn_invalid P x x') P (λr. r=x') (PASS$x)"
  apply rule
  apply (subst invalidate_clone') unfolding hn_ctxt_def
  apply vcg
  done

(*lemma hn_pass_pure[sepref_fr_rules]:
  shows "hn_refine (hn_val P x x') (return x') (hn_val P x x') (pure P) (PASS$x)"
  by rule (sep_auto simp: hn_ctxt_def pure_def)
*)

thm hnr_bind

lemma hn_bind[sepref_comb_rules]:
  assumes D1: "hn_refine Γ m' Γ1 Rh CP1 m"
  assumes D2: 
    "⋀x x'. bind_ref_tag x m ⟹ CP_assm (CP1 x') ⟹
      hn_refine (hn_ctxt Rh x x' ** Γ1) (f' x') (Γ2 x x') R (CP2 x') (f x)"
  assumes IMP: "⋀x x'. Γ2 x x' ⊢ hn_ctxt Rx x x' ** Γ'"
  assumes "MK_FREE Rx fr"
  shows "hn_refine Γ (doM {x←m'; r←f' x; fr x; Mreturn r}) Γ' R (CP_SEQ CP1 CP2) (Refine_Basic.bind$m$(λ2x. f x))"
  using assms
  unfolding APP_def PROTECT2_def bind_ref_tag_def CP_defs
  by (rule hnr_bind)


lemma hn_RECT'[sepref_comb_rules]:
  assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
  assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
  assumes S: "⋀cf af ax px. ⟦
    ⋀ax px. hn_refine (hn_ctxt Rx ax px ** F) (cf px) (hn_ctxt Rx' ax px ** F) Ry (λ_. True)
      (RCALL$af$ax)⟧ 
    ⟹ hn_refine (hn_ctxt Rx ax px ** F) (cB cf px) (F' ax px) Ry (CP px)
          (aB af ax)"
  assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px ** F"
  assumes M: "M_mono_body cB"
  (*assumes PREC[unfolded CONSTRAINT_def]: "CONSTRAINT precise Ry"*)
  shows "hn_refine 
    (P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
        (RECT$(λ2D x. aB D x)$ax)"
  unfolding APP_def PROTECT2_def 
  apply (rule hn_refine_cons_pre[OF FR])
  apply (rule hnr_RECT)

  apply (rule hn_refine_cons_post[OF _ FR'])
  apply (rule hn_refine_cons_cp_only)
  apply (rule S[unfolded RCALL_def APP_def])
  apply (rule hn_refine_cons_cp_only)
  apply assumption
  apply simp
  apply assumption
  apply fact
  done

lemma hn_RCALL[sepref_comb_rules]:
  assumes "RPREM (hn_refine P' c Q' R CP (RCALL $ a $ b))"
    and "P ⊢ P' ** F"
  shows "hn_refine P c (Q'**F) R CP (RCALL $ a $ b)"
  using assms hn_refine_frame[where m="RCALL$a$b"] 
  by simp

  
definition RECT_cp_annot :: "('ai ⇒ 'bi ⇒ bool) ⇒ (('a ⇒ 'b nres) ⇒ 'a ⇒ 'b nres) ⇒ 'a ⇒ 'b nres" 
  where "RECT_cp_annot CP ≡ RECT"    

lemma RECT_cp_annot: "RECT = RECT_cp_annot CP" unfolding RECT_cp_annot_def ..

lemma RECT_cp_annot_pat[def_pat_rules]:
  "RECT_cp_annot$CP ≡ UNPROTECT (RECT_cp_annot CP)"
  by simp

lemma RECT_cp_annot_arity[sepref_monadify_arity]:
  "PR_CONST (RECT_cp_annot CP) ≡ λ2B x. SP (PR_CONST (RECT_cp_annot CP))$(λ2D x. B$(λ2x. RCALL$D$x)$x)$x" 
  by (simp_all)


lemma RECT_cp_annot_comb[sepref_monadify_comb]:
  "⋀B x. PR_CONST (RECT_cp_annot CP)$B$x ≡ Refine_Basic.bind$(EVAL$x)$(λ2x. SP (PR_CONST (RECT_cp_annot CP)$B$x))"
  by (simp_all)

lemma RECT_cp_annot_id[id_rules]: 
  "PR_CONST (RECT_cp_annot CP) ::i TYPE((('c ⇒ 'd nres) ⇒ 'c ⇒ 'd nres) ⇒ 'c ⇒ 'd nres)"
  by simp
  
  
lemma hn_RECT_cp_annot(*[sepref_comb_rules]*):
  assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
  assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
  assumes S: "⋀cf af ax px. ⟦
    ⋀ax px. hn_refine (hn_ctxt Rx ax px ** F) (cf px) (hn_ctxt Rx' ax px ** F) Ry (CP px)
      (RCALL$af$ax)⟧ 
    ⟹ hn_refine (hn_ctxt Rx ax px ** F) (cB cf px) (F' ax px) Ry (CP' px)
          (aB af ax)"
  assumes CP: "⋀px r. CP_assm (CP' px r) ⟹ CP_cond (CP px r)"        
  assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px ** F"
  assumes M: "M_mono_body cB"
  (*assumes PREC[unfolded CONSTRAINT_def]: "CONSTRAINT precise Ry"*)
  shows "hn_refine 
    (P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
        (PR_CONST (RECT_cp_annot CP)$(λ2D x. aB D x)$ax)"
  unfolding APP_def PROTECT2_def RECT_cp_annot_def PR_CONST_def
  apply (rule hn_refine_cons_pre[OF FR])
  
  thm hnr_RECT
  
  apply (rule hnr_RECT)

  apply (rule hn_refine_cons_post[OF _ FR'])
  apply (rule hn_refine_cons_cp_only)
  apply (rule S[unfolded RCALL_def APP_def])
  apply (rule hn_refine_cons_cp_only)
  applyS assumption
  applyS simp
  subgoal using CP by (simp add: CP_defs)
  applyS fact
  done

lemma hn_RECT_cp_annot_noframe:
  assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
  assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
  assumes S: "⋀cf af ax px. ⟦
    ⋀ax px. hn_refine (hn_ctxt Rx ax px) (cf px) (hn_ctxt Rx' ax px) Ry (CP px)
      (RCALL$af$ax)⟧ 
    ⟹ hn_refine (hn_ctxt Rx ax px) (cB cf px) (F' ax px) Ry (CP' px)
          (aB af ax)"
  assumes CP: "⋀px r. CP_assm (CP' px r) ⟹ CP_cond (CP px r)"        
  assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px"
  assumes M: "M_mono_body cB"
  (*assumes PREC[unfolded CONSTRAINT_def]: "CONSTRAINT precise Ry"*)
  shows "hn_refine 
    (P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
        (PR_CONST (RECT_cp_annot CP)$(λ2D x. aB D x)$ax)"
        
  apply (rule hn_refine_cons_post)
  apply (rule hn_refine_frame[where F=F])    
  apply (rule hn_RECT_cp_annot[where F=□, OF assms(1,2,3)])  
  applyS (rule entails_refl)
  focus apply simp apply (rule S) apply simp solved
  applyS fact
  focus apply simp apply fact solved
  applyS fact
  focus using FR apply (simp add: algebra_simps) solved
  applyS (simp add: algebra_simps)
  done
  
  
lemma hn_RECT'_cp[sepref_comb_rules]:
  assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
  assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
  assumes S: "⋀cf af ax px. ⟦
    ⋀ax px. hn_refine (hn_ctxt Rx ax px ** F) (cf px) (hn_ctxt Rx' ax px ** F) Ry (CP px)
      (RCALL$af$ax)⟧ 
    ⟹ hn_refine (hn_ctxt Rx ax px ** F) (cB cf px) (F' ax px) Ry (CP' px)
          (aB af ax)"
  assumes CP: "⋀px r. CP_assm (CP' px r) ⟹ CP_cond (CP px r)"        
  assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px ** F"
  assumes M: "M_mono_body cB"
  (*assumes PREC[unfolded CONSTRAINT_def]: "CONSTRAINT precise Ry"*)
  shows "hn_refine 
    (P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
        (PR_CONST (RECT_cp_annot CP)$(λ2D x. aB D x)$ax)"
  unfolding APP_def PROTECT2_def RECT_cp_annot_def PR_CONST_def
  apply (rule hn_refine_cons_pre[OF FR])
  apply (rule hnr_RECT)

  apply (rule hn_refine_cons_post[OF _ FR'])
  apply (rule hn_refine_cons_cp_only)
  apply (rule S[unfolded RCALL_def APP_def])
  apply (rule hn_refine_cons_cp_only)
  apply assumption
  apply simp
  subgoal using CP by (simp add: CP_defs)
  apply fact
  done
  
  
  
  
lemma hn_refine_synthI:
  assumes "hn_refine Γ c Γ' R' CP m"
  assumes "c = c'"
  assumes "R' = R''"
  assumes "Γ' ⊢ Γ''"
  shows "hn_refine Γ c' Γ'' R'' CP m"
  using assms by (blast intro: hn_refine_cons_post)
  
lemma hn_refine_extract_pre_val: 
  "hn_refine (hn_val S xa xc ** Γ) c Γ' R CP m ⟷ ((xc,xa)∈S ⟶ hn_refine Γ c Γ' R CP m)"
  unfolding hn_refine_def hn_ctxt_def pure_def
  apply (cases "(xc,xa)∈S")
  by (auto simp: sep_algebra_simps)
  
lemma hnr_freeI:
  assumes "MK_FREE R fr"
  assumes "hn_refine Γ c Γ' R' CP m"
  shows "hn_refine (hn_ctxt R x y ** Γ) (doM { fr y; c}) Γ' R' CP m"  
proof (rule hn_refine_nofailI)  
  assume "nofail m"
  note [vcg_rules] = MK_FREED[OF assms(1)] hn_refineD[OF assms(2) ‹nofail m›]
  show ?thesis unfolding hn_ctxt_def
    by rule vcg
qed  
  
lemma drop_hn_val: "hn_val R x y ⊢ □" by (auto simp: hn_ctxt_def pure_def entails_def pred_lift_extract_simps)
lemma drop_hn_invalid: "hn_invalid R x y ⊢ □" by (auto simp: hn_ctxt_def invalid_assn_def entails_def pred_lift_extract_simps)

  
  
definition [simp]: "op_ASSERT_bind I m ≡ Refine_Basic.bind (ASSERT I) (λ_. m)"
lemma pat_ASSERT_bind[def_pat_rules]:
  "Refine_Basic.bind$(ASSERT$I)$(λ2_. m) ≡ UNPROTECT (op_ASSERT_bind I)$m"
  by simp

term "PR_CONST (op_ASSERT_bind I)"
lemma id_op_ASSERT_bind[id_rules]: 
  "PR_CONST (op_ASSERT_bind I) ::i TYPE('a nres ⇒ 'a nres)"
  by simp

lemma arity_ASSERT_bind[sepref_monadify_arity]:
  "PR_CONST (op_ASSERT_bind I) ≡ λ2m. SP (PR_CONST (op_ASSERT_bind I))$m"
  apply (rule eq_reflection)
  by auto

lemma hn_ASSERT_bind[sepref_comb_rules]: 
  assumes "I ⟹ hn_refine Γ c Γ' R CP m"
  shows "hn_refine Γ c Γ' R CP (PR_CONST (op_ASSERT_bind I)$m)"
  using assms
  apply (cases I)
  apply auto
  done

definition [simp]: "op_ASSUME_bind I m ≡ Refine_Basic.bind (ASSUME I) (λ_. m)"
lemma pat_ASSUME_bind[def_pat_rules]:
  "Refine_Basic.bind$(ASSUME$I)$(λ2_. m) ≡ UNPROTECT (op_ASSUME_bind I)$m"
  by simp

lemma id_op_ASSUME_bind[id_rules]: 
  "PR_CONST (op_ASSUME_bind I) ::i TYPE('a nres ⇒ 'a nres)"
  by simp

lemma arity_ASSUME_bind[sepref_monadify_arity]:
  "PR_CONST (op_ASSUME_bind I) ≡ λ2m. SP (PR_CONST (op_ASSUME_bind I))$m"
  apply (rule eq_reflection)
  by auto

lemma hn_ASSUME_bind[sepref_comb_rules]: 
  assumes "vassn_tag Γ ⟹ I"
  assumes "I ⟹ hn_refine Γ c Γ' R CP m"
  shows "hn_refine Γ c Γ' R CP (PR_CONST (op_ASSUME_bind I)$m)"
  apply (rule hn_refine_preI)
  using assms
  apply (cases I)
  apply (auto simp: vassn_tag_def)
  done
    
text ‹Manual deallocation. Frees data before its variable goes out of scope›  
definition "mop_free x ≡ RETURN ()"
sepref_register mop_free

lemma mop_free_hnr[sepref_fr_rules]:
  assumes "MK_FREE R f"  
  shows "(f,mop_free)∈Rd→ad(λ_. unit_assn)"
  unfolding mop_free_def
  apply (rule hfrefI)
  apply (rule hn_refineI)
  apply (rule htriple_pure_preI)
  apply (clarsimp 
    simp: hn_ctxt_def pure_def sep_algebra_simps invalid_assn_def)
  supply [vcg_rules] = MK_FREED[OF assms]
  by vcg
    
subsection "Import of Parametricity Theorems"
lemma pure_hn_refineI:
  assumes "Q ⟶ (c,a)∈R"
  (* TODO: Weak CP copied from Sep-Imp-HOL. *)
  shows "hn_refine (↑Q) (Mreturn c) (↑Q) (pure R) (λ_. True) (RETURN a)"
  unfolding hn_refine_def pure_def using assms by vcg

lemma pure_hn_refineI_no_asm:
  assumes "(c,a)∈R"
  (* TODO: Weak CP copied from Sep-Imp-HOL. *)
  shows "hn_refine □ (Mreturn c) □ (pure R) (λ_. True) (RETURN a)"
  unfolding hn_refine_def pure_def using assms by vcg

lemma import_param_0:
  "(P⟹Q) ≡ Trueprop (PROTECT P ⟶ Q)"
  apply (rule, simp+)+
  done

lemma import_param_1: 
  "(P⟹Q) ≡ Trueprop (P⟶Q)"
  "(P⟶Q⟶R) ⟷ (P∧Q ⟶ R)"
  "PROTECT (P ∧ Q) ≡ PROTECT P ∧ PROTECT Q"
  "(P ∧ Q) ∧ R ≡ P ∧ Q ∧ R"
  "(a,c)∈Rel ∧ PROTECT P ⟷ PROTECT P ∧ (a,c)∈Rel"
  apply (rule, simp+)+
  done

lemma import_param_2:
  "Trueprop (PROTECT P ∧ Q ⟶ R) ≡ (P ⟹ Q⟶R)"
  apply (rule, simp+)+
  done

lemma import_param_3:
  "↑(P ∧ Q) = (↑P**↑Q)"
  "↑((c,a)∈R) = hn_val R a c"
  by (simp_all add: hn_ctxt_def pure_def sep_algebra_simps)

named_theorems_rev sepref_import_rewrite ‹Rewrite rules on importing parametricity theorems›

lemma to_import_frefD: 
  assumes "(f,g)∈fref P R S"
  shows "⟦PROTECT (P y); (x,y)∈R⟧ ⟹ (f x, g y)∈S y"
  using assms
  unfolding fref_def
  by auto

lemma add_PR_CONST: "(c,a)∈R ⟹ (c,PR_CONST a)∈R" by simp

ML ‹
structure Sepref_Import_Param = struct

  (* TODO: Almost clone of Sepref_Rules.to_foparam*)
  fun to_import_fo ctxt thm = let
    val unf_thms = @{thms 
      split_tupled_all prod_rel_simp uncurry_apply cnv_conj_to_meta Product_Type.split}
  in
    case Thm.concl_of thm of
      @{mpat "Trueprop ((_,_) ∈ fref _ _ _)"} =>
        (@{thm to_import_frefD} OF [thm])
        |> Thm.forall_intr_vars
        |> Local_Defs.unfold0 ctxt unf_thms
        |> Variable.gen_all ctxt
    | @{mpat "Trueprop ((_,_) ∈ _)"} =>
        Parametricity.fo_rule thm
    | _ => raise THM("Expected parametricity or fref theorem",~1,[thm])
  end

  fun add_PR_CONST thm = case Thm.concl_of thm of
    @{mpat "Trueprop ((_,_) ∈ fref _ _ _)"} => thm (* TODO: Hack. Need clean interfaces for fref and param rules. Also add PR_CONST to fref rules! *)
  | @{mpat "Trueprop ((_,PR_CONST _) ∈ _)"} => thm
  | @{mpat "Trueprop ((_,?a) ∈ _)"} => if is_Const a orelse is_Free a orelse is_Var a then
      thm
    else
      thm RS @{thm add_PR_CONST}
  | _ => thm  


  fun import ctxt thm = let
    open Sepref_Basic
    val thm = thm
      |> Conv.fconv_rule Thm.eta_conversion
      |> add_PR_CONST
      |> Local_Defs.unfold0 ctxt @{thms import_param_0}
      |> Local_Defs.unfold0 ctxt @{thms imp_to_meta}
      |> to_import_fo ctxt
      |> Local_Defs.unfold0 ctxt @{thms import_param_1}
      |> Local_Defs.unfold0 ctxt @{thms import_param_2}

    val thm = case Thm.concl_of thm of
      @{mpat "Trueprop (_⟶_)"} => thm RS @{thm pure_hn_refineI}
    | _ => thm RS @{thm pure_hn_refineI_no_asm}

    val thm = Local_Defs.unfold0 ctxt @{thms import_param_3} thm
      |> Conv.fconv_rule (hn_refine_concl_conv_a (K (Id_Op.protect_conv ctxt)) ctxt)

    val thm = Local_Defs.unfold0 ctxt (Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_import_rewrite}) thm
    val thm = Sepref_Rules.add_pure_constraints_rule ctxt thm
  in
    thm
  end

  val import_attr = Scan.succeed (Thm.mixed_attribute (fn (context,thm) =>
    let
      val thm = import (Context.proof_of context) thm
      val context = Sepref_Translate.sepref_fr_rules.add_thm thm context
    in (context,thm) end
  ))

  val import_attr_rl = Scan.succeed (Thm.rule_attribute [] (fn context =>
    import (Context.proof_of context) #> Sepref_Rules.ensure_hfref (Context.proof_of context)
  ))

  val setup = I
    #> Attrib.setup @{binding sepref_import_param} import_attr
        "Sepref: Import parametricity rule"
    #> Attrib.setup @{binding sepref_param} import_attr_rl
        "Sepref: Transform parametricity rule to sepref rule"
    #> Attrib.setup @{binding sepref_dbg_import_rl_only} 
        (Scan.succeed (Thm.rule_attribute [] (import o Context.proof_of)))
        "Sepref: Parametricity to hnr-rule, no conversion to hfref"    

end
›

setup Sepref_Import_Param.setup


subsection "Purity"
definition "import_rel1 R ≡ λA c ci. ↑(is_pure A ∧ (ci,c)∈⟨the_pure A⟩R)"
definition "import_rel2 R ≡ λA B c ci. ↑(is_pure A ∧ is_pure B ∧ (ci,c)∈⟨the_pure A, the_pure B⟩R)"
  
lemma import_rel1_pure_conv: "import_rel1 R (pure A) = pure (⟨A⟩R)"
  unfolding import_rel1_def
  apply simp
  apply (simp add: pure_def)
  done

lemma import_rel2_pure_conv: "import_rel2 R (pure A) (pure B) = pure (⟨A,B⟩R)"
  unfolding import_rel2_def
  apply simp
  apply (simp add: pure_def)
  done

(*  
lemma precise_pure[constraint_rules]: "single_valued R ⟹ precise (pure R)"
  unfolding precise_def pure_def
  by (auto dest: single_valuedD)

lemma precise_pure_iff_sv: "precise (pure R) ⟷ single_valued R"          
  apply (auto simp: precise_pure)
  using preciseD[where R="pure R" and F=emp and F'=emp]
  by (sep_auto simp: mod_and_dist intro: single_valuedI)

lemma pure_precise_iff_sv: "⟦is_pure R⟧ 
  ⟹ precise R ⟷ single_valued (the_pure R)"
  by (auto simp: is_pure_conv precise_pure_iff_sv)
*)


lemmas [safe_constraint_rules] = single_valued_Id br_sv


end