Theory Sep_Generic_Wp

theory Sep_Generic_Wp
imports 
  "../lib/Sep_Algebra_Add" 
  "../lib/Frame_Infer"
  "../lib/Monad"
  "HOL-Library.Extended_Nat" (* TODO: This gives us Complex_Main. Too much for this theory! *)
  "../basic/kernel/LLVM_Shallow" (* TODO: Just used for acostC datatype. Move this datatype! *)
  "../cost/Enat_Cost"
begin


  (* TODO: Move, to Sep_Lift *)  
  text ‹Lifting Assertions over Product›
  definition FST :: "('a ⇒ bool) ⇒ 'a × 'b::zero ⇒ bool" 
    where "FST P ≡ λ(a,b). P a ∧ b=0"
  
  definition SND :: "('b ⇒ bool) ⇒ 'a::zero × 'b ⇒ bool" 
    where "SND P ≡ λ(a,b). a=0 ∧ P b"
    
  
  lemma FST_project_frame: "(FST P ∧* F) (a, b) ⟷ (P ** (λa. F (a,b))) a"
    unfolding sep_conj_def
    by (force simp add: sep_algebra_simps FST_def) 

  lemma SND_project_frame: "(SND P ∧* F) (a, b) ⟷ (P ** (λb. F (a,b))) b"
    unfolding sep_conj_def
    by (force simp add: sep_algebra_simps SND_def) 
    
        
  lemma FST_conj_conv: "(FST P ** FST Q) = FST (P**Q)"  
    unfolding sep_conj_def
    by (force simp add: sep_algebra_simps FST_def) 

  lemma SND_conj_conv: "(SND P ** SND Q) = SND (P**Q)"  
    unfolding sep_conj_def
    by (force simp add: sep_algebra_simps SND_def) 
    
        
  lemma FST_apply[sep_algebra_simps]: "FST P (a,b) ⟷ P a ∧ b=0"
    unfolding FST_def by auto
    
  lemma SND_apply[sep_algebra_simps]: "SND P (a,b) ⟷ P b ∧ a=0"
    unfolding SND_def by auto



declare [[coercion_enabled = false]]
hide_const (open) Transcendental.pi


section ‹General VCG Setup for Separation Logic›

(* TODO: Move to Library *)

locale generic_wp_defs =
  fixes wp :: "'c ⇒ ('r ⇒ 's ⇒ bool) ⇒ 's ⇒ bool"
begin
  definition "htripleF α F P c Q ≡ (∀s. (P**F) (α s) ⟶
      wp c (λr s'. (Q r ** F) (α s')) s)"

  definition "htriple α P c Q ≡ (∀F s. (P**F) (α s) ⟶
      wp c (λr s'. (Q r ** F) (α s')) s)"

  lemma htriple_as_F_eq: "htriple α P c Q = (∀F. htripleF α F P c Q)"    
    unfolding htriple_def htripleF_def by blast
      
end


locale generic_wp = generic_wp_defs wp
  for wp :: "'c ⇒ ('r ⇒ 's ⇒ bool) ⇒ 's ⇒ bool" +
  assumes wp_comm_inf: "inf (wp c Q) (wp c Q') = wp c (inf Q Q')"
begin

  lemma wp_comm_conj: "wp c (λr. Q r and Q' r) s ⟷ wp c Q s ∧ wp c Q' s"
    using wp_comm_inf[of c Q Q']
    unfolding inf_fun_def inf_bool_def by metis

  lemma wp_comm_conjI: "⟦ wp c Q s; wp c Q' s ⟧ ⟹ wp c (λr s. Q r s ∧ Q' r s) s"
    using wp_comm_inf[of c Q Q']
    unfolding inf_fun_def inf_bool_def by metis


  lemma wp_mono: "Q≤Q' ⟹ wp c Q ≤ wp c Q'"
    by (metis (mono_tags) antisym_conv le_inf_iff order_refl wp_comm_inf)

  lemma wp_monoI:
    assumes "wp c Q s"
    assumes "⋀r x. Q r x ⟹ Q' r x"
    shows "wp c Q' s"
    using assms wp_mono[of Q Q' c] by auto
      
  lemma htripleI:     
    assumes "⋀F s. (P**F) (α s) ⟹ wp c (λr s'. (Q r ** F) (α s')) s"
    shows "htriple α P c Q"
    using assms by (auto simp: htriple_def)

  lemma htripleFI:     
    assumes "⋀s. (P**F) (α s) ⟹ wp c (λr s'. (Q r ** F) (α s')) s"
    shows "htripleF α F P c Q"
    using assms by (auto simp: htripleF_def)
        
  lemma htripleD:  
    assumes "htriple α P c Q"
    assumes "(P**F) (α s)"
    shows "wp c (λr s'. (Q r ** F) (α s')) s"
    using assms by (auto simp: htriple_def)
    
  lemma htriple_triv[simp, intro!]: "htriple α sep_false c Q"
    by (auto simp: htriple_def)
      
  lemma frame_rule: "htriple α P c Q ⟹ htriple α (P ** F) c (λr. Q r ** F)"
    unfolding htriple_def
    by (fastforce)

  lemma cons_rule:
    assumes "htriple α P c Q"
    assumes "⋀s. P' s ⟹ P s"
    assumes "⋀r s. Q r s ⟹ Q' r s"
    shows "htriple α P' c Q'"
    unfolding htriple_def
  proof clarsimp
    fix F s
    assume "(P' ∧* F) (α s)"
    with assms(2) have "(P ∧* F) (α s)"
      using sep_conj_impl1 by blast
    with assms(1) have "wp c (λr s'. (Q r ∧* F) (α s')) s"
      unfolding htriple_def by auto
    thus "wp c (λr s'. (Q' r ∧* F) (α s')) s"
      apply (rule wp_monoI)
      using assms(3)
      using sep_conj_impl1 by blast
  qed

  lemma cons_post_rule:
    assumes "htriple α P c Q"
    assumes "⋀r s. Q r s ⟹ Q' r s"
    shows "htriple α P c Q'"
    using cons_rule assms by blast
  
  
  lemma htriple_alt:
    "htriple α P c Q 
      = (∀p s f. p##f ∧ α s = p + f ∧ P p ⟶ wp c (λr s'. ∃p'. p'##f ∧ α s'=p'+f ∧ Q r p') s)"
  proof (rule iffI, goal_cases)
    case 1
    show ?case
      using htripleD[OF 1, where F="EXACT x" for x]
        by (auto simp: sep_conj_def)
    
  next
    case 2
    show ?case proof (rule htripleI)
      fix F s 
      assume "(P ∧* F) (α s)"
      then obtain p f where "p##f" "P p" "F f" "α s = p+f"
        by (blast elim: sep_conjE)
      with 2 have "wp c (λr s'. ∃p'. p' ## f ∧ α s' = p' + f ∧ Q r p') s" by blast
      then show "wp c (λr s'. (Q r ∧* F) (α s')) s"
        apply (rule wp_monoI)
        using ‹F f› by (auto intro: sep_conjI)
    qed
  qed
  
  lemma htripleI': 
    assumes "⋀p s f. ⟦ p##f; α s = p + f; P p⟧ ⟹ wp c (λr s'. ∃p'. p'##f ∧ α s'=p'+f ∧ Q r p') s"
    shows "htriple α P c Q"
    using assms by (auto simp: htriple_alt)

  lemma htripleD': 
    assumes "htriple α P c Q"
    assumes "p##f" "α s = p + f" "P p"
    shows "wp c (λr s'. ∃p'. p'##f ∧ α s'=p'+f ∧ Q r p') s"
    using assms by (auto simp: htriple_alt)
        
    
    
  lemma htriple_extract_pre_pure: 
    "htriple α (↑Φ**P) c Q ⟷ Φ ⟶ htriple α P c Q"  
    by (cases Φ) (auto simp: sep_algebra_simps)
    
  (*
  lemma htriple_extract_pre_EXS: 
    assumes "⋀x s. Φ x ⟹ P s ⟹ f x ## s"
    shows "htriple α (EXS x. ↑Φ x ** EXACT (f x) ** P) c Q ⟷ (∃x. Φ x ∧ htriple α (EXACT (f x) ** P) c Q)"
    apply rule
  *)  
    
  thm htripleD
  
  thm option.simps
  
  lemma sv_htripleD:
    assumes "htriple α P c Q"
    assumes "(P**F) (α s)"
    assumes "⋀r s. (Q r ** F) (α s) ⟹ Q' r s"
    shows "wp c Q' s"
    using assms 
    by (force simp: htriple_def intro: wp_monoI)
  
  lemma sv_htripleFD:
    assumes "htripleF α F P c Q"
    assumes "(P**F) (α s)"
    assumes "⋀r s. (Q r ** F) (α s) ⟹ Q' r s"
    shows "wp c Q' s"
    using assms 
    by (force simp: htripleF_def intro: wp_monoI)
    
    
  lemma htriple_conj_pure:
    fixes α
    assumes "htriple α P c Q"
    assumes "htriple α P c (λr. ↑Φ r ** sep_true)"
    shows "htriple α P c (λr. ↑Φ r ** Q r)"
  proof (rule htripleI)  
    fix F s
    assume "(P**F) (α s)"
    from wp_comm_conjI[OF assms[THEN htripleD,OF this]]
    show "wp c (λr s'. ((↑Φ r ∧* Q r) ∧* F) (α s')) s"
      apply (rule wp_monoI)
      using and_pure_true unfolding entails_def by blast
      
  qed    

  
  text ‹With garbage collection›
  abbreviation "htriple_gc GC α P c Q ≡ htriple α P c (λr. Q r ** GC)"
  
  lemma htriple_to_gc: "⟦ □⊢GC; htriple α P c Q ⟧ ⟹ htriple_gc GC α P c Q"
    apply (erule cons_rule)
    apply simp
    by (metis abel_semigroup.commute entails_def sep.mult.abel_semigroup_axioms sep_conj_empty sep_globalise)
  
      
end



experiment begin
  text ‹Precondition defined by semantics relation:
    ▪ ‹T c s› command terminates in state ‹s›
    ▪ ‹R c s r s'› command yields result ‹r› and new state ‹s'›
  ›
  
  definition "my_wp T (R::_ ⇒ 's⇒_⇒'s⇒bool) c Q s ≡ T c s ∧ (∀r s'. R c s r s' ⟶ Q r s')"
  

  interpretation generic_wp "my_wp T R"  
    apply unfold_locales
    unfolding my_wp_def
    by auto
  

end




definition STATE :: "('s ⇒ 'a::sep_algebra) ⇒ ('a ⇒ bool) ⇒ 's ⇒ bool" 
  where "STATE α P s ≡ P (α s)"

lemma STATE_assn_cong[fri_extract_congs]: "P≡P' ⟹ STATE α P s ≡ STATE α P' s" by simp
  
lemma STATE_extract[vcg_normalize_simps]:
  "STATE α (↑Φ) h ⟷ Φ ∧ STATE α □ h"
  "STATE α (↑Φ ** P) h ⟷ Φ ∧ STATE α P h"
  "STATE α (EXS x. Q x) h ⟷ (∃x. STATE α (Q x) h)"
  "STATE α (λ_. False) h ⟷ False"
  "STATE α ((λ_. False) ** P) h ⟷ False"
  by (auto simp: STATE_def sep_algebra_simps pred_lift_extract_simps)
 

definition POSTCOND :: "('s ⇒ 'a::sep_algebra) ⇒ ('a ⇒ bool) ⇒ 's ⇒ bool" 
  where [vcg_tag_defs]: "POSTCOND α ≡ STATE α"
  
lemma POSTCONDI:
  "STATE α A h ⟹ POSTCOND α A h"
  by (auto simp add: POSTCOND_def)
lemma POSTCOND_cong[vcg_normalize_congs]: "POSTCOND α A = POSTCOND α A" ..

lemma POSTCOND_triv_simps[vcg_normalize_simps]:
  "POSTCOND α sep_true h"
  "¬POSTCOND α sep_false h"
  unfolding POSTCOND_def STATE_def by auto
  
lemma start_entailsE:
  assumes "STATE α P h"
  assumes "ENTAILS P P'"
  shows "STATE α P' h"
  using assms unfolding STATE_def ENTAILS_def entails_def
  by auto

declaration ‹
  K (Basic_VCG.add_xformer (@{thms POSTCONDI},@{binding postcond_xformer},
    fn ctxt => eresolve_tac ctxt @{thms start_entailsE}
  ))
›


named_theorems htriple_vcg_intros
named_theorems htriple_vcg_intro_congs
definition [vcg_tag_defs]: "DECOMP_HTRIPLE φ ≡ φ"
lemma DECOMP_HTRIPLEI: "φ ⟹ DECOMP_HTRIPLE φ" unfolding vcg_tag_defs by simp

 
context generic_wp begin
  thm frame_rule
  thm cons_rule  
    
  lemma htriple_vcg_frame_erule[vcg_frame_erules]:
    assumes S: "STATE α P' s"
    assumes F: "PRECOND (FRAME P' P F)"
    assumes HT: "htriple α P c Q"  
    assumes P: "⋀r s. STATE α (Q r ** F) s ⟹ PRECOND (EXTRACT (Q' r s))"
    shows "wp c Q' s"
  proof -
    from S F have "(P ∧* F) (α s)"
      unfolding vcg_tag_defs
      by (metis (no_types) FRAME_def entails_def STATE_def)
    with P show ?thesis
      unfolding vcg_tag_defs
      by (metis (no_types) STATE_def sv_htripleD[OF HT])
      
  qed

  lemma htripleF_vcg_frame_erule[vcg_frame_erules]:
    assumes S: "STATE α P' s"
    assumes F: "PRECOND (FRAME P' P F)"
    assumes HT: "htripleF α F P c Q"  
    assumes P: "⋀r s. STATE α (Q r ** F) s ⟹ PRECOND (EXTRACT (Q' r s))"
    shows "wp c Q' s"
  proof -
    from S F have "(P ∧* F) (α s)"
      unfolding vcg_tag_defs
      by (metis (no_types) FRAME_def entails_def STATE_def)
    with P show ?thesis
      unfolding vcg_tag_defs
      by (metis (no_types) STATE_def sv_htripleFD[OF HT])
      
  qed
  
  
  
  lemma htriple_vcgI': 
    assumes "⋀F s. STATE α (P**F) s ⟹ wp c (λr. POSTCOND α (Q r ** F)) s"
    shows "htriple α P c Q"
    apply (rule htripleI)
    using assms unfolding vcg_tag_defs STATE_def .
  
  lemma htriple_vcgI[htriple_vcg_intros]: 
    assumes "⋀F s. STATE α (P**F) s ⟹ EXTRACT (wp c (λr. POSTCOND α (Q r ** F)) s)"
    shows "htriple α P c Q"
    apply (rule htripleI)
    using assms unfolding vcg_tag_defs STATE_def .

  lemma htripleF_vcgI[htriple_vcg_intros]: 
    assumes "⋀s. STATE α (P**F) s ⟹ EXTRACT (wp c (λr. POSTCOND α (Q r ** F)) s)"
    shows "htripleF α F P c Q"
    apply (rule htripleFI)
    using assms unfolding vcg_tag_defs STATE_def .
    
      
  lemma htriple_decompI[vcg_decomp_rules]: 
    "DECOMP_HTRIPLE (htriple α P c Q) ⟹ htriple α P c Q"
    "DECOMP_HTRIPLE (htripleF α F P c Q) ⟹ htripleF α F P c Q"
    unfolding vcg_tag_defs by auto

  lemma htriple_assn_cong[htriple_vcg_intro_congs]: 
    "P≡P' ⟹ Q≡Q' ⟹  htriple α P c Q ≡ htriple α P' c Q'" by simp

  lemma htripleF_assn_cong[htriple_vcg_intro_congs]: 
    "P≡P' ⟹ Q≡Q' ⟹  htripleF α F P c Q ≡ htripleF α F P' c Q'" by simp
            
  lemma htriple_ent_pre:
    "P⊢P' ⟹ htriple α P' c Q ⟹ htriple α P c Q"
    unfolding entails_def
    apply (erule cons_rule) by blast+
    
  lemma htriple_ent_post:
    "⟦⋀r. Q r ⊢ Q' r⟧ ⟹ htriple α P c Q ⟹ htriple α P c Q'"
    unfolding entails_def
    apply (erule cons_rule) by blast+
   
  lemma htriple_pure_preI: "⟦pure_part P ⟹ htriple α P c Q⟧ ⟹ htriple α P c Q"  
    by (meson htriple_def pure_partI sep_conjE)
    
     
end


declaration ‹
  K (Basic_VCG.add_xformer (@{thms DECOMP_HTRIPLEI},@{binding decomp_htriple_xformer},
    fn ctxt => 
      (full_simp_tac (put_simpset HOL_basic_ss ctxt 
        addsimps (Named_Theorems.get ctxt @{named_theorems vcg_tag_defs})
        |> fold Simplifier.add_cong (Named_Theorems.get ctxt @{named_theorems htriple_vcg_intro_congs})
      ))
      THEN' resolve_tac ctxt (Named_Theorems.get ctxt @{named_theorems htriple_vcg_intros})
  ))
›



section ‹a General framework for abstract and concrete costs›

text ‹This locale fixes a type of concrete costs ‹'cc› which is used in ‹mres› and a type for
      abstract costs ‹'ca› which should be used in the separation logic with (resource) credits. 
      There is some invariant that has to hold between the credits currently available "on the heap"
      and the resources spent in the computation, ‹I› captures that.
      Also it needs to be possible to deduct the resources used by the computation from the credits,
      this is captured by ‹minus›.
      ›

locale cost_framework =
  fixes
    I :: "'cc::{monoid_add} ⇒ 'ca ⇒ bool"
  and minus :: "'ca ⇒ 'cc ⇒ 'ca" ― ‹takes abstract credits, and returns the effect of consuming
                                        the concrete resources›
assumes minus_0[simp]: "⋀y. minus y 0 = y"
  and I_0[simp,intro!]: "I 0 cr"
  and minus_minus_add: "⋀a b c. minus (minus a b) c = minus a (b + c)"
  ― ‹TODO: maybe some of these are redundant›
  and I1: "⋀a b c. I (a + b) c ⟹ I b (minus c a)"
  and I2: "⋀a b c. I (a + b) c ⟹ I a c"
  and I3:  "⋀a b c. I a (minus c b) ⟹ I b c ⟹ I (b + a) c"
begin


  definition  wp :: "('d, 'e, _, 'a, 'f) M ⇒ _ ⇒ _" where
    "wp m Q ≡ λ(s,cr). mwp (run m s) bot bot bot (λr c s. Q r (s,minus cr c) ∧ I c cr)"

(*
  term "α x ≤ y ⟷ x ≤ γ y"    
*)
    
  interpretation generic_wp wp
    apply unfold_locales
    unfolding wp_def fun_eq_iff inf_fun_def inf_bool_def mwp_def
    by (auto split: mres.split)


  lemma wp_return: "wp (return x) Q s ⟷ Q x s"
    by (auto simp: wp_def run_simps minus_0 I_0)

  lemma wp_fail: "¬ wp (fail x) Q s"
    by (auto simp: wp_def run_simps)

  lemma wp_fcheck: "wp (fcheck e Φ) Q s ⟷ Φ ∧ Q () s"
    by (auto simp: wp_def run_simps minus_0 I_0 split: if_splits)

  (* TODO: refactor that proof, should not need to unfold mwp_def at that stage *)
  lemma wp_bind: "wp (m⤜f) Q s = wp m (λx. wp (f x) Q) s"
    apply (auto simp: wp_def run_simps split: prod.splits)
    unfolding mwp_def apply (auto split: mres.splits simp add: minus_minus_add)
    subgoal
      by (metis I1)
    subgoal
      by (metis I2)
    subgoal
      by (metis I3)
    done
    
  lemma wp_consume: "wp (consume c) Q (s,cr) ⟷ I c cr ∧ Q () (s,minus cr c)"  
    unfolding wp_def mwp_def consume_def by (auto split: mres.split)
    
end



interpretation nat: cost_framework "λ(c::nat) (cr::nat). cr-c+c=cr" "(-)"
  apply standard
  by auto

interpretation int: cost_framework "λ(c::int) (cr::int). True" "(-)"
  apply standard
  by auto

locale cost_framework2 = cost_framework I minus for I :: "'cc::{monoid_add} ⇒ 'ca::{plus} ⇒ bool" and minus +
  assumes I_left_mono: "⋀x c d. I x c ⟹ I x (c+d)" ― ‹@{thm ordered_comm_monoid_add_class.add_increasing2}›
  assumes minus_add_assoc2: "⋀x c d. I x c ⟹ minus (c + d) x = minus c x + d" ― ‹@{thm ordered_cancel_comm_monoid_diff_class.diff_add_assoc2}›
begin


end

locale cost_framework3 = cost_framework2 I minus for I :: "'cc::{monoid_add} ⇒ 'ca::{plus} ⇒ bool" and minus +
  fixes lift :: "'cc ⇒ 'ca"
  assumes I_add1: "⋀c cr. I c (lift c + cr)" ― ‹@{thm le_add1}›
  assumes add_minus_cancel: "⋀c cr. minus (lift c + cr) c = cr" ― ‹@{thm Extended_Nat.add_diff_cancel_enat}›
begin


end




  
term acostC  
  


context cost_framework begin                     

abbreviation "I_fun ≡ (λcc ca. ∀x. I (the_acost cc x) (the_acost ca x))"
abbreviation "minus_fun ≡ (λca cc. acostC (λx. minus (the_acost ca x) (the_acost cc x)))"

  lemma fun_cost_framework: "cost_framework I_fun minus_fun"
    apply unfold_locales
    apply (simp_all add: zero_acost_def I_0 minus_0 minus_minus_add fun_eq_iff)
    subgoal for a b c by (cases a;cases b;cases c; auto)
    subgoal for a b c by (cases a;cases b;cases c; auto simp: I1)
    subgoal for a b c by (cases a;cases b;cases c; auto intro: I2)
    subgoal for a b c by (cases a;cases b;cases c; auto simp: I3)
    done
end

context cost_framework3
begin


lemma fun_cost_framework2: "cost_framework2 I_fun minus_fun"
  unfolding cost_framework2_def
  apply safe apply (fact fun_cost_framework)
  apply unfold_locales
  subgoal for x c d by(cases x; cases c; cases d) (auto intro: I_left_mono)
  subgoal for x c d by(cases x; cases c; cases d) (auto intro: minus_add_assoc2)
  done


abbreviation "lift_fun ≡ (λcc. acostC (λx. lift (the_acost cc x)))"

lemma fun_cost_framework3: "cost_framework3 I_fun minus_fun lift_fun"
  unfolding cost_framework3_def
  apply safe apply (fact fun_cost_framework2)
  apply unfold_locales
  subgoal for c cr by(cases c; cases cr) (auto intro: I_add1)
  subgoal for c cr by(cases c; cases cr) (auto intro: add_minus_cancel)
  done


end


section ‹Setup for mres-Monad›

  lemma "cr-c+c=(cr::nat) ⟷ cr≥c" by auto
  lemma "cr-c+c=(cr::int) ⟷ True" by auto


  lemma enat_diff_diff: "a - enat b - enat c = a - enat (b + c)"
    apply(cases a) by auto
  lemma enat_aux1: "c - enat (a + b) + enat (a + b) = c ⟹ c - enat a + enat a = c"
    apply(cases c) by auto
    
  definition le_cost_ecost :: "cost ⇒ ecost ⇒ bool" 
    where "le_cost_ecost cc ca ≡ ∀x. enat (the_acost cc x) ≤ (the_acost ca x)"

  definition minus_ecost_cost :: "ecost ⇒ cost ⇒ ecost"
    where "minus_ecost_cost ca cc ≡ acostC (λx. (the_acost ca x) - enat (the_acost cc x))"
      
  interpretation cost_framework le_cost_ecost minus_ecost_cost
    unfolding le_cost_ecost_def minus_ecost_cost_def
    apply (rule cost_framework.fun_cost_framework)
    apply standard
    apply (auto simp flip: zero_enat_def)
    subgoal by (metis enat_diff_diff)
    subgoal
      by (smt add.commute add_diff_cancel_enat add_right_mono enat.distinct(1) enat_aux1 eq_iff le_iff_add linear of_nat_add of_nat_eq_enat)
    subgoal
      by (meson enat_ord_simps(1) le_add1 order_subst2)
    subgoal
      by (metis add_diff_cancel_enat add_left_mono enat.simps(3) le_iff_add plus_enat_simps(1))
    done

    
  (*      
  term pi  
  interpretation cost_framework "λ(c::nat) (cr::enat). cr-c+c=cr" "(-)"
    apply standard
         apply (auto simp: zero_enat_def)
    subgoal
      by (metis enat_diff_diff)
    subgoal
      by (metis enat_diff_diff add_diff_assoc_enat add_diff_cancel_left' enat_ord_simps(1)
                idiff_enat_enat le_add_same_cancel1 zero_le)
    subgoal
      by (metis enat_aux1)
    subgoal
      by (metis enat_diff_diff add.assoc add.commute plus_enat_simps(1))
    done
  *)

  (*
  lemma enat_nat_I_conv: "cr - enat c + enat c = cr ⟷ cr ≥ c"
    by (cases cr; cases c; auto)
  *)

  (* Definition for presentation *)
  lemma natenat_alt: "wp m Q = (λ(s, cr). mwp (run m s) bot bot bot (λr c s. Q r (s, minus_ecost_cost cr c) ∧ le_cost_ecost c cr))" unfolding wp_def ..

  (* Definition for presentation in paper *)
  lemma wp_alt: "wp m Q (s,cr::ecost) = (∃r (c::cost) s'. run m s = SUCC r c s' ∧ Q r (s', minus_ecost_cost cr c) ∧ le_cost_ecost c cr )"
    unfolding wp_def mwp_def by (fastforce split: mres.splits)

  interpretation generic_wp wp 
    apply unfold_locales 
    unfolding wp_def fun_eq_iff inf_fun_def inf_bool_def mwp_def
    by (auto split: mres.split)

  declare wp_return[vcg_normalize_simps]

  declare wp_fail[vcg_normalize_simps]

  declare wp_fcheck[vcg_normalize_simps]

  declare wp_bind[vcg_normalize_simps]

  thm vcg_normalize_simps

  
  
  (* TODO: Move *)
  instantiation enat :: stronger_sep_algebra begin
    definition "(_::enat) ## _ ≡ True"
  
    instance
      apply standard
      apply (simp_all add: sep_disj_enat_def)
      done
      
  end
  
  
  instantiation acost :: (type,stronger_sep_algebra) stronger_sep_algebra begin
    definition "f1 ## f2 ⟷ (∀x. the_acost f1 x ## the_acost f2 x)"
    (*definition [simp]: "(f1 + f2) = acostC (λx. the_acost f1 x + the_acost f2 x)"
    definition [simp]: "0 x ≡ 0"
    *)
  
    instance
      apply standard
      unfolding sep_disj_acost_def plus_acost_alt zero_acost_def
      apply (auto simp: sep_algebra_simps split: acost.splits)
      done  
    
  end
  
  

definition time_credits_assn :: "ecost ⇒ (_ × ecost ⇒ bool)" ("$_" [900] 900) where "($c) ≡ SND (EXACT c)"

term "a ** $c"
term "c ** $a"

definition "GC ≡ SND sep_true"
  
lemma GC_absorb[simp]: "(GC ** GC) = GC" by (auto simp: GC_def sep_algebra_simps SND_conj_conv)

lemma entails_GC: "$c ⊢ GC" unfolding GC_def time_credits_assn_def
  by (auto simp: entails_def SND_def) (* TODO: Monotonicity of FST,SND as lemmas? *)

lemma "$0 = □" oops 
  
lemma empty_ent_GC: "□⊢GC" unfolding GC_def time_credits_assn_def
  by (auto simp: entails_def SND_def sep_algebra_simps) 


lemma dollar_aux_conv: "($c) (aa, ba) = (aa=0 ∧ ba=c)"
  unfolding time_credits_assn_def EXACT_def SND_def
  by auto


lemma "F ⊢ GC ** G ⟹ $c ** F ⊢ GC ** G"
  by (metis (no_types, lifting) GC_absorb conj_entails_mono entails_GC sep_conj_assoc)
  
lemma htriple_to_GC: "⟦ htriple α P c Q ⟧ ⟹ htriple_gc GC α P c Q"
  using htriple_to_gc[OF empty_ent_GC] .
  
lemma time_credits_add: "($A ** $B) = $(A+B)"   
  by (simp add: EXACT_split SND_conj_conv sep_disj_acost_def sep_disj_enat_def time_credits_assn_def)  

  

(* For presentation *)
lemma "($c) (s,c') ⟷ s=0 ∧ c'=c"
  unfolding time_credits_assn_def by (simp add: sep_algebra_simps SND_def) (* TODO: Lemmas for SND! *)
  
lemma "($c) a ⟷ a=(0,c)"  
  unfolding time_credits_assn_def by (cases a) (simp add: sep_algebra_simps SND_def)
    
definition "lift_α_cost α ≡ λ(s,c). (α s,c)"  


lemma cost_ecost_minus_add_assoc2: "le_cost_ecost x c ⟹ minus_ecost_cost (c + d) x = minus_ecost_cost c x + d"
  apply(cases x; cases c; cases d) apply(auto simp: minus_ecost_cost_def le_cost_ecost_def)
  by (simp add: add.commute add_diff_assoc_enat)

lemma cost_ecost_add_increasing2: "le_cost_ecost x c ⟹ le_cost_ecost x (c + d)"  
  apply(cases x; cases c; cases d) apply (auto simp:   le_cost_ecost_def) 
  by (simp add:  add_increasing2) 

lemma cost_ecost_add1: "le_cost_ecost c (lift_acost c + cr')" 
  apply(cases cr') by (auto simp: le_cost_ecost_def lift_acost_def )

lemma cost_ecost_add_minus_cancel: "minus_ecost_cost (lift_acost c + cr') c = cr'"  
  apply(cases cr') by (auto simp: minus_ecost_cost_def lift_acost_def )
    
lemma consume_rule_aux: "htriple (lift_α_cost α) ($(lift_acost c)) (consume c) (λ_. □)"  
  apply (rule htripleI)
  apply clarify
  apply (simp add: wp_consume time_credits_assn_def lift_α_cost_def)
proof (rule conjI)
  fix F s cr
  assume "(SND (EXACT (lift_acost c)) ∧* F) ((α s, cr))"
  from this have "(EXACT (lift_acost c) ∧* (λb. F (α s, b))) cr" by (simp add: SND_project_frame)
  then obtain cr' where [simp]: "lift_acost c ## cr'" "cr = lift_acost c + cr'" and F: "F (α s, cr')"
    by (rule sep_conjE) (simp add: sep_algebra_simps)
  have "0 ≼ cr'"
    by (simp add: sep_substate_def) 
  show "le_cost_ecost c cr" by (simp add: cost_ecost_add1)
  
  show "F (α s, minus_ecost_cost cr c)" using F by (simp add: cost_ecost_add_minus_cancel)
qed    
  
lemmas consume_rule = htriple_to_GC[OF consume_rule_aux]

    
section ‹experiment: Hoare-triple without Time›  
 
  
      
    
    
    
    
    
    
    
    
  
  text ‹Weakest precondition without time›
  definition "wpn m Q s ≡ mwp (run m s) bot bot bot (λr c s'. c=0 ∧ Q r s')"
  
  lemma wpn_def': "wpn m Q s = (∃r s'. run m s = SUCC r 0 s' ∧ Q r s')"
    unfolding wpn_def mwp_def
    by (auto split: mres.split)
  
  (* TODO: Move *)  
  lemma le_cost_zero_conv[simp]: "le_cost_ecost c 0 ⟷ c=0"
    unfolding le_cost_ecost_def by (cases c; auto simp: zero_acost_def zero_enat_def)
  
    
  lemma wpn_alt: "wpn m Q s = wp m (FST o Q) (s,0)"
    unfolding wp_def wpn_def mwp_def
    by (auto split: mres.split simp: zero_enat_def FST_def)

  lemma wpn_alt': "wpn m Q s = wp m (λr (s,c). Q r s ∧ c=0) (s,0)"
    unfolding wp_def wpn_def mwp_def
    by (auto split: mres.split simp: zero_enat_def FST_def)
    
      
  interpretation notime: generic_wp wpn  
    apply unfold_locales 
    unfolding wpn_def fun_eq_iff inf_fun_def inf_bool_def mwp_def
    by (auto split: mres.split)

        
  lemma wpn_return[vcg_normalize_simps]: "wpn (return x) Q s ⟷ Q x s"
    by (auto simp: wpn_def run_simps)

  lemma wpn_fail[vcg_normalize_simps]: "¬ wpn (fail x) Q s"
    by (auto simp: wpn_def run_simps)

  lemma wpn_fcheck[vcg_normalize_simps]: "wpn (fcheck e Φ) Q s ⟷ Φ ∧ Q () s"
    by (auto simp: wpn_def run_simps split: if_splits)

  (* TODO: refactor that proof, should not need to unfold mwp_def at that stage *)
  (* TODO: Intuitively, want equality here: BUT, equality only holds if costs cannot be negative! *)
  lemma wpn_bind[vcg_decomp_rules]: "wpn m (λx. wpn (f x) Q) s ⟹ wpn (m⤜f) Q s"
    apply (auto simp: wpn_def[abs_def] run_simps split: prod.splits)
    unfolding mwp_def 
    by (auto 
      split: mres.splits 
      simp add: minus_minus_add dest!: addcost_SUCC_D)
  
  (*      
  lemma wpn_bind: "wpn (m⤜f) Q s = wpn m (λx. wpn (f x) Q) s"
    apply (auto simp: wpn_def run_simps split: prod.splits)
    unfolding mwp_def 
    apply (auto 
      split: mres.splits 
      simp add: minus_minus_add dest!: addcost_SUCC_D)
    xxx. ctd here: need positive costs, 
      otherwise negatove+positive can cancel out.
      
  *)
  
  
  lemma notime_return_rule: "notime.htriple α P (return x) (λr. ↑(r=x)**P)" for α
    by vcg
  
      
  text ‹Transfer of Hoare-Triples›
    
  (* TODO: Move *)
  lemma wp_time_mono: "wp m Q (s,c) ⟹ wp m (λr (s',c'). ∃cc'. c'=cc'+d ∧ Q r (s',cc')) (s,c+d)"
    unfolding wp_def mwp_def
    apply (auto simp add: algebra_simps sep_algebra_simps SND_def sep_conj_def split: mres.split)
    subgoal by (intro exI conjI; assumption?) (rule cost_ecost_minus_add_assoc2)
    subgoal by (rule cost_ecost_add_increasing2)
    done
      
  lemma notime_to_htriple:
    fixes c :: "('a, 'b, cost, 'd, 'e) M"
    assumes H: "notime.htriple α P c Q"
    shows "htriple (lift_α_cost α) (FST P) c (FST o Q)"
    unfolding lift_α_cost_def
    apply (rule htripleI)
    apply clarify
  proof -
    fix F a and b :: ecost
    assume "(FST P ∧* F) (α a, b)"
    hence "(P ** (λa. F (a,b))) (α a)"
      by (simp add: sep_algebra_simps FST_project_frame)
    from notime.htripleD[OF H this] have "wpn c (λr s'. (Q r ∧* (λa. F (a, b))) (α s')) a" .
    then have "wp c (λx (a, ba). (Q x ∧* (λa. F (a, b))) (α a) ∧ ba = 0) (a, 0)"
      unfolding wpn_alt FST_def comp_def by simp
    from wp_time_mono[OF this, of b] have "wp c (λr (s', c'). c' = b ∧ (Q r ∧* (λa. F (a, b))) (α s')) (a, b)"
      by simp
    then show "wp c (λr s'. ((FST ∘ Q) r ∧* F) (case s' of (s, x) ⇒ (α s, x))) (a, b)"  
      apply (rule wp_monoI)
      apply (auto simp: FST_project_frame)
      done
  qed  

  lemma htriple_to_notime:
    assumes H: "htriple (lift_α_cost α) (FST P) c (FST o Q)"
    shows "notime.htriple α P c Q"
    apply (rule notime.htripleI)
    unfolding wpn_alt
  proof -  
    fix F s
    assume A: "(P ∧* F) (α s)"
    
    show "wp c (FST ∘ (λr s'. (Q r ∧* F) (α s'))) (s, 0)"
      apply (rule wp_monoI)
      apply (rule htripleD[OF H, where F="FST F"])
      unfolding lift_α_cost_def
      apply (auto simp: FST_conj_conv sep_algebra_simps A)
      done
  qed      
  
  lemma notime_htriple_eq: "notime.htriple α P c Q = htriple (lift_α_cost α) (FST P) c (FST o Q)"
    by (blast intro: notime_to_htriple htriple_to_notime)
  

  definition "wlp c Q s ≡ mwp (run c s) top top top (λr c s. Q r s)"
  lemma wlp_true[simp, intro!]:
    "wlp c (λ_ _. True) s"
    "wlp c top s"
    by (auto simp: wlp_def mwp_def split: mres.splits)
    
  lemma wlp_return[simp]: "wlp (return x) Q s = Q x s"
    by (auto simp: wlp_def run_simps)
        
  
section ‹experiment: cost type for Space›


datatype space_cost = Space_Cost (sca: nat) (scb: nat) (* highest point,  how far below that mark at the moment *)


(*

  mm_alloc n ⟹ λ(m,c). (max m (c+n),c+n)
  mm_free n ⟹ λ(m,c). assert(n≤c), (m,c-n)


*)


fun max_cost where "max_cost (Space_Cost h _) = h"
fun curr_cost where "curr_cost (Space_Cost h c) = int h - int c"

definition "new_h m1 c1 m2 c2 ≡ (max (int m1) (((int m1 - int c1)+int m2)))"
definition "new_c m1 c1 m2 c2 ≡ (new_h m1 c1 m2 c2 - ((int m1 - int c1)+(int m2 - int c2)))"

lemma new_h_nonneg: "new_h m1 c1 m2 c2 ≥ 0"
  by (auto simp: new_h_def)

lemma new_c_nonneg: "new_c m1 c1 m2 c2 ≥ 0"
  by (auto simp: new_c_def new_h_def)

instantiation space_cost :: plus
begin
  lemma fixes m1 c1 m2 c2 :: nat
    shows "(max (int m1) (((int m1 - int c1)+int m2))) - ((int m1 - int c1)+(int m2 - int c2)) ≥ 0"
    by auto

lemma "new_h m1 c1 m2 c2 - ((int m1 - int c1)+(int m2 - int c2)) ≥ 0"
  by (auto simp: new_h_def)

  fun plus_space_cost :: "space_cost ⇒ space_cost ⇒ space_cost" where
    "plus_space_cost (Space_Cost m1 c1) (Space_Cost m2 c2) =
             Space_Cost (nat (new_h m1 c1 m2 c2)) (nat (new_c m1 c1 m2 c2))"

  instance ..
end


instantiation space_cost :: monoid_add
begin
  definition zero_space_cost :: space_cost where "zero_space_cost = Space_Cost 0 0"

  instance
    apply standard
    subgoal for a b c
      apply(cases a; cases b; cases c)
      apply (simp add: new_h_nonneg new_c_nonneg) apply safe
      subgoal for m1 c1 m2 c2 m3 c3
        apply(subst (2) new_h_def)
        apply(simp add: new_c_nonneg  new_h_nonneg)
        apply(subst (4) new_h_def)
        apply(simp add: new_c_nonneg  new_h_nonneg)
        by (auto simp: new_h_def new_c_def max.assoc)
      subgoal for m1 c1 m2 c2 m3 c3
        apply(subst (3) new_c_def)
        apply(simp add: new_c_nonneg  new_h_nonneg)
        apply(subst (3) new_c_def)
        apply(subst (3) new_h_def)
        apply(simp add: new_c_nonneg  new_h_nonneg)
        apply(subst (2) new_c_def)
        apply(simp add: new_c_nonneg  new_h_nonneg)
        by (auto simp: new_h_def new_c_def max.assoc)
      done
    subgoal for a apply(cases a)
      subgoal for m c
        by (auto simp: new_h_def new_c_def zero_space_cost_def)
      done
    subgoal for a apply(cases a)
      subgoal for m c
        by (auto simp: new_h_def new_c_def zero_space_cost_def)
      done
    done
end


text ‹the Invariant denotes, that maximum space ‹m› is at most the number of space_credits ‹n››

fun space_I :: "space_cost ⇒ nat ⇒ bool"  where
  "space_I (Space_Cost m c) n ⟷ m≤n"

fun space_minus :: "nat ⇒ space_cost ⇒ nat"  where
  "space_minus  n (Space_Cost m c) = n - m + c"
― ‹if space_I holds, this is n - (m-c), i.e. credits minus newly occupied space›

interpretation space: cost_framework "space_I" "space_minus"
  apply standard
  subgoal for a by(simp add: zero_space_cost_def)
  subgoal for cr apply (simp add: zero_space_cost_def) done
  subgoal for a b c apply(cases b; cases c) by (simp add: new_c_def new_h_def)
  subgoal for a b c apply(cases a; cases b) by (simp add: new_c_def new_h_def)
  subgoal for a b c apply(cases a; cases b) by (simp add: new_c_def new_h_def)
  subgoal for a b c apply(cases a; cases b) by (simp add: new_c_def new_h_def)
  done


lemma space_minus_aux: "space_I b 0 ⟹ Space_Cost 0 (space_minus 0 b) = b"
  apply(cases b) by simp


text ‹The test ‹sm≤cr› makes sure that the maximum of space ‹sm› used does not exceed 
      the allowed space by the "space-credits" cr.
      When before executing ‹m› there are ‹cr› credits, after the execution there will be
      ‹cr - (sm-c)›, i.e. the credits before minus the number of consumed space,
      see @{const curr_cost}.›

lemma "space.wp m Q (s,cr) = (∃r sm c s'. run m s = SUCC r (Space_Cost sm c) s'
                                   ∧ Q r (s', cr - sm + c) ∧ sm≤cr )"
    unfolding space.wp_def  mwp_def
    apply (auto split: mres.splits)
    subgoal for a b c apply(cases b)
      by simp
    done


(* TODO: again clash with type class lifting with prod for sep_algebra!
instantiation prod :: (monoid_add,monoid_add) monoid_add
begin

end

lemma
  assumes "cost_framework I1 minus1"
    and "cost_framework I2 minus2"
  shows "cost_framework (λ(a,b) (c,d). I1 a c ∧ I2 b d) (λ(a,b) (c,d). (minus1 a c, minus2 b d))"
*)

end