theory Segfault
  imports "HOL-IMP.Big_Step" "HOL-Library.Extended_Nat"
begin

inductive
  big_step_t :: "com \<times> state \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"  ("_ \<Rightarrow>^/_ _" 55)
where
Skip: "(SKIP, s) \<Rightarrow>^1 s" |
Assign: "(x ::= a,s) \<Rightarrow>^1 s(x := aval a s)" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow>^n\<^sub>1 s\<^sub>2;  (c\<^sub>2,s\<^sub>2) \<Rightarrow>^n\<^sub>2 s\<^sub>3; n\<^sub>1+n\<^sub>2 = n\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow>^n\<^sub>3 s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s;  (c\<^sub>1,s) \<Rightarrow>^n\<^sub>1 t; n\<^sub>3 = Suc n\<^sub>1 \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow>^n\<^sub>3 t" |
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2,s) \<Rightarrow>^n\<^sub>2 t; n\<^sub>3 = Suc n\<^sub>2 \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow>^n\<^sub>3 t" |
WhileFalse: "\<lbrakk> \<not>bval b s \<rbrakk> \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow>^1 s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1;  (c,s\<^sub>1) \<Rightarrow>^n\<^sub>1 s\<^sub>2;  (WHILE b DO c, s\<^sub>2) \<Rightarrow>^n\<^sub>2 s\<^sub>3; n\<^sub>1+n\<^sub>2+1 = n\<^sub>3 \<rbrakk>
  \<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow>^n\<^sub>3 s\<^sub>3"

inductive_cases If_tE[elim!]: "(IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<Rightarrow>^x t"

type_synonym qassn = "state \<Rightarrow> enat"

fun emb :: "bool \<Rightarrow> enat" ("\<down>") where
   "emb False = \<infinity>"
 | "emb True = 0"

definition hoare_Qvalid :: "qassn \<Rightarrow> com \<Rightarrow> qassn \<Rightarrow> bool"
  ("\<Turnstile>\<^sub>Q {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile>\<^sub>Q {P} c {Q}  \<longleftrightarrow>  (\<forall>s.  P s < \<infinity> \<longrightarrow> (\<exists>t p. ((c,s) \<Rightarrow>^p t) \<and> P s \<ge> p + Q t))"

theorem If_sound:
    assumes "\<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (bval b a)} c\<^sub>1 {Q}"
      and " \<Turnstile>\<^sub>Q {\<lambda>a. P a + \<down> (\<not> bval b a)} c\<^sub>2 {Q}"
  shows "\<Turnstile>\<^sub>Q {\<lambda>a. eSuc (P a)} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}"
unfolding hoare_Qvalid_def proof(safe)
  fix s
  assume "eSuc (P s) < \<infinity>"
  then have Ps_fin: "P s < \<infinity>" by (metis eSuc_infinity eSuc_mono)
  show "\<exists>t p. ((IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow>^p t) \<and> enat p + Q t \<le> eSuc (P s)"
  proof(cases "bval b s")
    case True
    have "P s + \<down>(bval b s) < \<infinity> \<longrightarrow> (\<exists>t p. ((c\<^sub>1, s) \<Rightarrow>^p t) \<and> enat p + Q t \<le> P s + \<down>(bval b s))"
      using assms(1) unfolding hoare_Qvalid_def by simp
    then obtain t p where "(c\<^sub>1, s) \<Rightarrow>^p t" and "enat p + Q t \<le> eSuc (P s)" using True Ps_fin try sorry
    then show ?thesis sorry
  next
    case False
    then show ?thesis sorry
  qed
qed

end