Quelle  Semantics.thy

section ‹Semantics of IMP›
theory Semantics
imports Syntax "HOL-Eisbach.Eisbach_Tools" 
begin

subsection ‹State›
text ‹The state maps variable names to values›
type_synonym state = "vname ==> val"

text ‹We introduce some syntax for the null state, and a state where only certain
 variables are set.›
definition null_state (‹<>\›) where
  "null_state ≡ λx. λi. 0"
syntax 
  "_State" :: "updbinds => 'a" (‹🪙›)
translations
  "_State ms" == "_Update <> ms"
  "_State (_updbinds b bs)" <= "_Update (_State b) bs"

subsubsection ‹State Combination›
text ‹The state combination operator constructs a state by
 taking the local variables from one state, and the globals from another state.›

definition combine_states :: "state ==> state ==> state" (‹<_|_>› [0,0] 1000)
  where "<s|t> n = (if is_local n then s n else t n)"

text ‹We prove some basic facts.

  that we use Isabelle's context command to locally declare the
 definition of @{const combine_states} as simp lemma, such that it is
 unfolded automatically.›
  
context notes [simp] = combine_states_def begin

lemma combine_collapse: "<s|s> = s" by auto

lemma combine_nest:  
  "<s|<s'|t>> = <s|t>"
  "<<s|t'>|t> = <s|t>"
  by auto  
  
lemma combine_query: 
  "is_local x ==> <s|t> x = s x"  
  "is_global x ==> <s|t> x = t x"  
  by auto

lemma combine_upd: 
  "is_local x ==> <s|t>(x:=v) = <s(x:=v)|t>"  
  "is_global x ==> <s|t>(x:=v) = <s|t(x:=v)>"  
  by auto  
  
lemma combine_cases[cases type]:
  obtains l g where "s = <l|g>"
  by (fastforce)
  
end  
  
  
  
    
  
  
subsection ‹Arithmetic Expressions›
text ‹The evaluation of arithmetic expressions is straightforward. ›
fun aval :: "aexp ==> state ==> pval" where
  "aval (N n) s = n" 
| "aval (Vidx x i) s = s x (aval i s)" 
| "aval (Unop f a₁) s = f (aval a₁ s)"
| "aval (Binop f a₁ a₂) s = f (aval a₁ s) (aval a₂ s)"

subsection ‹Boolean Expressions›
text ‹The evaluation of Boolean expressions is straightforward. ›

fun bval :: "bexp ==> state ==> bool" where
  "bval (Bc v) s = v" 
| "bval (Not b) s = (¬ bval b s)" 
| "bval (BBinop f b₁ b₂) s = f (bval b₁ s) (bval b₂ s)" 
| "bval (Cmpop f a₁ a₂) s = f (aval a₁ s) (aval a₂ s)"

subsection ‹Big-Step Semantics›
text ‹The big-step semantics is a relation from commands and start states to end states,
 such that there is a terminating execution.

 If there is no such execution, no end state will be related to the command and start state.
 This either means that the program does not terminate, or gets stuck because it tries to call
 an undefined procedure.

 The inference rules of the big-step semantics are pretty straightforward.
 ›

inductive big_step :: "program ==> com × state ==> state ==> bool" 
  (‹_: _ ==> _› [1000,55,55] 55)
where
  ― ‹No-Op›
  Skip: "π:(SKIP,s) ==> s" 
  
  ― ‹Assignments›
| AssignIdx: "π:(x[i] ::= a,s) ==> s(x := (s x)(aval i s := aval a s))" 
| ArrayCpy: "π:(x[] ::= y,s) ==> s(x := s y)" 
| ArrayClear: "π:(CLEAR x[],s) ==> s(x := (λ_. 0))" 
| Assign_Locals: "π:(Assign_Locals l,s) ==> <l|s>"

  ― ‹Block commands›
| Seq: "[ π:(c₁,s₁) ==> s₂; π:(c₂,s₂) ==> s₃ ] ==> π:(c₁;;c₂, s₁) ==> s₃" 
| IfTrue: "[ bval b s; π:(c₁,s) ==> t ] ==> π:(IF b THEN c₁ ELSE c₂, s) ==> t" 
| IfFalse: "[ ¬bval b s; π:(c₂,s) ==> t ] ==> π:(IF b THEN c₁ ELSE c₂, s) ==> t" 
| Scope: "[ π:(c,<<>|s>) ==> s' ] ==> π:(SCOPE c, s) ==> <s|s'>"
| WhileFalse: "¬bval b s ==> π:(WHILE b DO c,s) ==> s" 
| WhileTrue: "[ bval b s₁; π:(c,s₁) ==> s₂; π:(WHILE b DO c, s₂) ==> s₃ ]
    ==> π:(WHILE b DO c, s₁) ==> s₃"

  ― ‹Procedure commands›        
| PCall: "[ π p = Some c; π:(c,s) ==> t ] ==> π:(PCall p,s) ==> t"    
| PScope: "[ π':(c,s) ==> t ] ==> π:(PScope π' c, s) ==> t"


subsubsection ‹Proof Automation›    
text ‹
 We do some setup to make proofs over the big-step semantics more automatic.
 ›

declare big_step.intros [intro]
lemmas big_step_induct[induct set] = big_step.induct[split_format(complete)]

inductive_simps Skip_simp: "π:(SKIP,s) ==> t"
inductive_simps AssignIdx_simp: "π:(x[i] ::= a,s) ==> t"
inductive_simps ArrayCpy_simp: "π:(x[] ::= y,s) ==> t"
inductive_simps ArrayInit_simp: "π:(CLEAR x[],s) ==> t"
inductive_simps AssignLocals_simp: "π:(Assign_Locals l,s) ==> t"

inductive_simps Seq_simp: "π:(c1;;c2,s1) ==> s3"
inductive_simps If_simp: "π:(IF b THEN c1 ELSE c2,s) ==> t"
inductive_simps Scope_simp: "π:(SCOPE c,s) ==> t"
inductive_simps PCall_simp: "π:(PCall p,s) ==> t"
inductive_simps PScope_simp: "π:(PScope π' p,s) ==> t"

lemmas big_step_simps = 
  Skip_simp AssignIdx_simp ArrayCpy_simp ArrayInit_simp
  Seq_simp If_simp Scope_simp PCall_simp PScope_simp

  
inductive_cases SkipE[elim!]: "π:(SKIP,s) ==> t"
inductive_cases AssignIdxE[elim!]: "π:(x[i] ::= a,s) ==> t"
inductive_cases ArrayCpyE[elim!]: "π:(x[] ::= y,s) ==> t"
inductive_cases ArrayInitE[elim!]: "π:(CLEAR x[],s) ==> t"
inductive_cases AssignLocalsE[elim!]: "π:(Assign_Locals l,s) ==> t"

inductive_cases SeqE[elim!]: "π:(c1;;c2,s1) ==> s3"
inductive_cases IfE[elim!]: "π:(IF b THEN c1 ELSE c2,s) ==> t"
inductive_cases ScopeE[elim!]: "π:(SCOPE c,s) ==> t"
inductive_cases PCallE[elim!]: "π:(PCall p,s) ==> t"
inductive_cases PScopeE[elim!]: "π:(PScope π' p,s) ==> t"
  
inductive_cases WhileE[elim]: "π:(WHILE b DO c,s) ==> t"
                             

subsubsection ‹Automatic Derivation›
  (* TODO: More comments, test *)
  (* Testing the programs by constructing big-step derivations automatically *)    
    
  (* This rule is used to enforce simplification of the newly generated state, before passing it on *)
  lemma Assign': "s' = s(x := (s x)(aval i s := aval a s)) ==> π:(x[i] ::= a, s) ==> s'" by auto
  lemma ArrayCpy': "s' = s(x := (s y)) ==> π:(x[] ::= y, s) ==> s'" by auto
  lemma ArrayClear': "s' = s(x := (λ_. 0)) ==> π:(CLEAR x[], s) ==> s'" by auto

  lemma Scope': "s₁ = <<>|s> ==> π:(c,s₁) ==> t ==> t' = <s|t> ==> π:(Scope c,s) ==> t'" by auto

  named_theorems deriv_unfolds ‹Unfold rules before derivations›
  
  method bs_simp = simp add: combine_nest combine_upd combine_query fun_upd_same fun_upd_other del: fun_upd_apply
  
  method big_step' = 
    rule Skip Seq PScope
  | (rule Assign' ArrayCpy' ArrayClear', (bs_simp;fail)) 
  | (rule IfTrue IfFalse WhileTrue WhileFalse PCall Scope'), (bs_simp;fail)
  | unfold deriv_unfolds
  | (bs_simp; fail)
  
      
  method big_step = 
    rule Skip 
  | rule Seq, (big_step;fail), (big_step;fail)
  | rule PScope, (big_step;fail)  
  | (rule Assign' ArrayCpy' ArrayClear', (bs_simp;fail)) 
  | (rule IfTrue IfFalse), (bs_simp;fail), (big_step;fail)
  | rule WhileTrue, (bs_simp;fail), (big_step;fail), (big_step;fail)
  | rule WhileFalse, (bs_simp;fail)
  | rule PCall, (bs_simp;fail), (big_step;fail)
  | (rule Scope', (bs_simp;fail), (big_step;fail), (bs_simp;fail))
  | unfold deriv_unfolds, big_step
  
  schematic_goal "Map.empty: (
    ''a'' ::= N 1;;
    WHILE Cmpop (λx y. y < x) (V ''n'') (N 0) DO (
      ''a'' ::= Binop (+) (V ''a'') (V ''a'');;
      ''n'' ::= Binop (-) (V ''n'') (N 1)
    ),<''n'':=(λ_. 5)>) ==> ?s"  
    by big_step



subsection ‹Command Equivalence›

text ‹Two commands are equivalent if they have the same semantics.›
definition
  equiv_c :: "com ==> com ==> bool" (infix ‹∼› 50) where
  "c ∼ c' ≡ (∀π s t. π:(c,s) ==> t = π:(c',s) ==> t)"

lemma equivI[intro?]: "[
  ∧s t π. π:(c,s) ==> t ==> π:(c',s) ==> t;
  ∧s t π. π:(c',s) ==> t ==> π:(c,s) ==> t]
  ==> c ∼ c'"  
  by (auto simp: equiv_c_def)
  
lemma equivD[dest]: "c ∼ c' ==> π:(c,s) ==> t ⟷ π:(c',s) ==> t"  
  by (auto simp: equiv_c_def)

text ‹Command equivalence is an equivalence relation, i.e.\ it is
 , symmetric, and transitive.›

lemma equiv_refl[simp, intro!]:  "c ∼ c"
  by (blast intro: equivI)
lemma equiv_sym[sym]:   "(c ∼ c') ==> (c' ∼ c)"
  by (blast intro: equivI)
lemma equiv_trans[trans]: "c ∼ c' ==> c' ∼ c'' ==> c ∼ c''"
  by (blast intro: equivI)

subsubsection ‹Basic Equivalences›
lemma while_unfold:
  "(WHILE b DO c) ∼ (IF b THEN c;; WHILE b DO c ELSE SKIP)"
  by rule auto

lemma triv_if:
  "(IF b THEN c ELSE c) ∼ c"
  by (auto intro!: equivI)

lemma commute_if:
  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2)
   ∼
   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
  by (auto intro!: equivI)

lemma sim_while_cong_aux:
  "[π:(WHILE b DO c,s) ==> t; bval b = bval b'; c ∼ c' ] ==> π:(WHILE b' DO c',s) ==> t"
  by(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct) auto

lemma sim_while_cong: "bval b = bval b' ==> c ∼ c' ==> WHILE b DO c ∼ WHILE b' DO c'"
  using equiv_c_def sim_while_cong_aux by auto

subsection ‹Execution is Deterministic›

text ‹This proof is automatic.›

theorem big_step_determ: "[ π:(c,s) ==> t; π:(c,s) ==> u ] ==> u = t"
proof (induction arbitrary: u rule: big_step.induct)
  case (WhileTrue b s₁ c s₂ s₃)
    then show ?case by blast
qed fastforce+

subsection ‹Small-Step Semantics›

text ‹
 The small step semantics is defined by a step function on
 a pair of command and state. Intuitively, the command is
 the remaining part of the program that still has to be executed.
 The step function is defined to stutter if the command is @{const SKIP}.
 
 Moreover, the step function is explicitly partial, returning @{const None}
 on error, i.e., on an undefined procedure call.

 Most steps are straightforward.
 For a sequential composition, steps are performed on the first command,
 until it has been reduced to @{const SKIP}, then the sequential composition is
 reduced to the second command.

 A while command is reduced by unfolding the loop once.
 
 A scope command is reduced to the inner command, followed by
 an @{const Assign_Locals} command to restore the original local variables.

 A procedure scope command is reduced by performing a step in the inner command,
 with the new procedure environment, until the inner command has been reduced to @{const SKIP}.
 Then, the whole command is reduced to @{const SKIP}.
 ›

fun small_step :: "program ==> com × state ⇀ com × state" where
  "small_step π (x[i]::=a,s) = Some (SKIP, s(x := (s x)(aval i s := aval a s)))"
| "small_step π (x[]::=y,s) = Some (SKIP, s(x := s y))"  
| "small_step π (CLEAR x[],s) = Some (SKIP, s(x := (λ_. 0)))"
| "small_step π (Assign_Locals l,s) = Some (SKIP,<l|s>)"
| "small_step π (SKIP;;c,s) = Some (c,s)"
| "small_step π (c₁;;c₂,s) = (case small_step π (c₁,s) of Some (c₁',s') ==> Some (c₁';;c₂,s') | _ ==> None)"
| "small_step π (IF b THEN c₁ ELSE c₂,s) = Some (if bval b s then (c₁,s) else (c₂,s))"
| "small_step π (SCOPE c, s) = Some (c;;Assign_Locals s, <<>|s>)"
| "small_step π (WHILE b DO c,s) = Some (IF b THEN c;;WHILE b DO c ELSE SKIP, s)"
| "small_step π (PCall p, s) = (case π p of Some c ==> Some (c, s) | _ ==> None)"
| "small_step π (PScope π' SKIP, s) = Some (SKIP,s)"
| "small_step π (PScope π' c, s) = (case small_step π' (c,s) of Some (c',s') ==> Some (PScope π' c', s') | _ ==> None)"
| "small_step π (SKIP,s) = Some (SKIP,s)"

text ‹
 We define the reflexive transitive closure of the step function.
 ›
inductive small_steps :: "program ==> com × state ==> (com × state) option ==> bool" where
  [simp]: "small_steps π cs (Some cs)"
| "[ small_step π cs = None ] ==> small_steps π cs None"
| "[ small_step π cs = Some cs1; small_steps π cs1 cs2 ] ==> small_steps π cs cs2"

lemma small_steps_append: "small_steps π cs₁ (Some cs₂) ==> small_steps π cs₂ cs₃ ==> small_steps π cs₁ cs₃"
  apply (induction π cs₁ "Some cs₂" arbitrary: cs₂ rule: small_steps.induct)
  apply (auto intro: small_steps.intros)
  done

subsubsection ‹Equivalence to Big-Step Semantics›
text ‹We show that the small-step semantics yields a final
 configuration if and only if the big-step semantics terminates with the respective state.
 
 Moreover, we show that the big-step semantics gets stuck if the small-step semantics
 yields an error.
 ›
  
lemma small_big_append: "small_step π cs₁ = Some cs₂ ==> π: cs₂ ==> s₃ ==> π: cs₁ ==> s₃"
  apply (induction π cs₁ arbitrary: cs₂ s₃ rule: small_step.induct)
  apply (auto split: option.splits if_splits)
  done

lemma smalls_big_append: "small_steps π cs₁ (Some cs₂) ==> π: cs₂ ==> s₃ ==> π: cs₁ ==> s₃"
  apply (induction π cs₁ "Some cs₂" arbitrary: cs₂ rule: small_steps.induct)
  apply (auto intro: small_big_append)
  done

lemma small_imp_big:
  assumes "small_steps π cs₁ (Some (SKIP,s₂))" 
  shows "π: cs₁ ==> s₂"
  using smalls_big_append[OF assms]
  by auto
  
lemma small_steps_skip_term[simp]: "small_steps π (SKIP, s) cs' ⟷ cs'=Some (SKIP,s)"  
  apply rule
  subgoal
    apply (induction π "(SKIP,s)" cs' arbitrary: s rule: small_steps.induct)
    by (auto intro: small_steps.intros)
  by (auto intro: small_steps.intros)
    
lemma small_seq: "[c≠SKIP; small_step π (c,s) = Some (c',s')] ==> small_step π (c;;cx,s) = Some (c';;cx,s')"  
  apply (induction π "(c,s)" arbitrary: c s c' s' rule: small_step.induct)
  apply auto
  done
  
lemma smalls_seq: "[small_steps π (c,s) (Some (c',s'))] ==> small_steps π (c;;cx,s) (Some (c';;cx,s'))"
  apply (induction π "(c,s)" "Some (c',s')" arbitrary: c s c' s' rule: small_steps.induct)
  apply (auto dest: small_seq intro: small_steps.intros)
  by (metis option.simps(1) prod.simps(1) small_seq small_step.simps(31) small_steps.intros(3))

lemma small_pscope:  
  "[c≠SKIP; small_step π' (c,s) = Some (c',s')] ==> small_step π (PScope π' c,s) = Some (PScope π' c',s')"
  apply (induction π "(c,s)" arbitrary: c s c' s' rule: small_step.induct)
  apply auto 
  done
    
lemma smalls_pscope:   
  "small_steps π' (c, s) (Some (c', s')) ==> small_steps π (PScope π' c, s) (Some (PScope π' c',s'))"
  apply (induction π' "(c,s)" "(Some (c', s'))" arbitrary: c s rule: small_steps.induct)
  apply auto
  by (metis (no_types, opaque_lifting) option.inject prod.inject small_pscope small_steps.simps small_steps_append small_steps_skip_term)
  
  
  
lemma big_imp_small:
  assumes "π: cs ==> t"
  shows "small_steps π cs (Some (SKIP,t))"
  using assms
proof induction
  case (Skip π s)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (AssignIdx π x i a s)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (ArrayCpy π x y s)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (ArrayClear π x s)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (Seq π c₁ s₁ s₂ c₂ s₃)
  then show ?case
    by (meson small_step.simps(5) small_steps.intros(3) small_steps_append smalls_seq)
next
  case (IfTrue b s π c₁ t c₂)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (IfFalse b s π c₂ t c₁)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (Scope π c s s')
  then show ?case 
  by (meson small_step.simps(17) small_step.simps(4) small_step.simps(5) small_steps.intros(1) small_steps.intros(3) small_steps_append smalls_seq)
next
  case (WhileFalse b s π c)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (WhileTrue b s₁ π c s₂ s₃)
  then show ?case 
  proof -
    have "∀ca p. (small_steps π p (Some (SKIP, s₃)) ∨ Some (ca, s₂) ≠ Some (WHILE b DO c, s₂)) ∨ small_step π p ≠ Some (c;; ca, s₁)"
      by (metis (no_types) WhileTrue.IH(1) WhileTrue.IH(2) small_step.simps(5) small_steps.intros(3) small_steps_append smalls_seq)
    then have "∀ca cb cc. (small_steps π (IF b THEN cc ELSE ca, s₁) (Some (SKIP, s₃)) ∨ Some (cb, s₂) ≠ Some (WHILE b DO c, s₂)) ∨ Some (cc, s₁) ≠ Some (c;; cb, s₁)"
      using WhileTrue.hyps(1) by force
    then show ?thesis
      using small_step.simps(18) small_steps.intros(3) by blast
  qed
  
next
  case (PCall π p c s t)
  then show ?case by (auto 0 4 intro: small_steps.intros)
next
  case (PScope π' c s t π)
  then show ?case 
    by (meson small_step.simps(20) small_steps.simps small_steps_append smalls_pscope)
  
next
  case (Assign_Locals π l s)
  then show ?case by (auto 0 4 intro: small_steps.intros)
qed

  
text ‹The big-step semantics yields a state ‹t›, iff and only iff there is a transition
 of the small-step semantics to ‹(SKIP,t).›
 ›
theorem big_eq_small: "π: cs==>t ⟷ small_steps π cs (Some (SKIP,t))"
  using big_imp_small small_imp_big by blast

lemma small_steps_determ: 
  assumes "small_steps π cs None"  
  shows "¬small_steps π cs (Some (SKIP, t))"  
  using assms
  apply (induction π cs "None::(com×state) option" arbitrary: t rule: small_steps.induct)
  apply (auto elim: small_steps.cases)
  done

text ‹If the small-step semantics reaches a failure state, the big-step semantics gets stuck.›    
corollary small_imp_big_fail: 
  assumes "small_steps π cs None"
  shows "∄t. π: cs ==> t"
  using assms
  by (auto simp: big_eq_small small_steps_determ)
   
  
  
subsection ‹Weakest Precondition›  

text ‹The following definitions are made wrt.\ a fixed program ‹π›, which becomes the first
 parameter of the defined constants when the context is left.›
context
  fixes π :: program
begin
  
  text ‹Weakest precondition:
 ‹c› terminates with a state that satisfies ‹Q›, when started from ‹s›.›
  definition "wp c Q s ≡ ∃t. π: (c,s) ==> t ∧ Q t"
    ― ‹Note that this definition exploits that the semantics is deterministic!
 In general, we must ensure absence of infinite executions›

  text ‹Weakest liberal precondition:
 If ‹c› terminates when started from ‹s›, the new state satisfies ‹Q›.›
  definition "wlp c Q s ≡ ∀t. π:(c,s) ==> t ⟶ Q t"
  
  subsubsection ‹Basic Properties›
  
  context 
    notes [abs_def,simp] = wp_def wlp_def
  begin
    lemma wp_imp_wlp: "wp c Q s ==> wlp c Q s"
      using big_step_determ by force
      
    lemma wlp_and_term_imp_wp: "wlp c Q s ∧ π:(c,s) ==> t ==> wp c Q s" by auto    
    
    lemma wp_equiv: "c ∼ c' ==> wp c = wp c'" by auto
    lemma wp_conseq: "wp c P s ==> [∧s. P s ==> Q s] ==> wp c Q s" by auto
    
    lemma wlp_equiv: "c ∼ c' ==> wlp c = wlp c'" by auto
    lemma wlp_conseq: "wlp c P s ==> [∧s. P s ==> Q s] ==> wlp c Q s" by auto
    
      
  
  subsubsection ‹Unfold Rules›
    lemma wp_skip_eq: "wp SKIP Q s = Q s" by auto
    lemma wp_assign_idx_eq: "wp (x[i]::=a) Q s = Q (s(x:=(s x)(aval i s := aval a s)))" by auto
    lemma wp_arraycpy_eq: "wp (x[]::=a) Q s = Q (s(x:=s a))" by auto
    lemma wp_arrayinit_eq: "wp (CLEAR x[]) Q s = Q (s(x:=(λ_. 0)))" by auto
    lemma wp_assign_locals_eq: "wp (Assign_Locals l) Q s = Q <l|s>" by auto
    lemma wp_seq_eq: "wp (c₁;;c₂) Q s = wp c₁ (wp c₂ Q) s" by auto
    lemma wp_if_eq: "wp (IF b THEN c₁ ELSE c₂) Q s
      = (if bval b s then wp c₁ Q s else wp c₂ Q s)" by auto
    
    lemma wp_scope_eq: "wp (SCOPE c) Q s = wp c (λs'. Q <s|s'>) <<>|s>" by auto
    lemma wp_pcall_eq: "π p = Some c ==> wp (PCall p) Q s = wp c Q s" by auto 
    
    lemmas wp_eq = wp_skip_eq wp_assign_idx_eq wp_arraycpy_eq wp_arrayinit_eq 
      wp_assign_locals_eq wp_seq_eq wp_scope_eq
    lemmas wp_eq' = wp_eq wp_if_eq
    
    lemma wlp_skip_eq: "wlp SKIP Q s = Q s" by auto
    lemma wlp_assign_idx_eq: "wlp (x[i]::=a) Q s = Q (s(x:=(s x)(aval i s := aval a s)))" by auto
    lemma wlp_arraycpy_eq: "wlp (x[]::=a) Q s = Q (s(x:=s a))" by auto
    lemma wlp_arrayinit_eq: "wlp (CLEAR x[]) Q s = Q (s(x:=(λ_. 0)))" by auto
    lemma wlp_assign_locals_eq: "wlp (Assign_Locals l) Q s = Q <l|s>" by auto
    lemma wlp_seq_eq: "wlp (c₁;;c₂) Q s = wlp c₁ (wlp c₂ Q) s" by auto
    lemma wlp_if_eq: "wlp (IF b THEN c₁ ELSE c₂) Q s
      = (if bval b s then wlp c₁ Q s else wlp c₂ Q s)" by auto

    lemma wlp_scope_eq: "wlp (SCOPE c) Q s = wlp c (λs'. Q <s|s'>) <<>|s>" by auto
    lemma wlp_pcall_eq: "π p = Some c ==> wlp (PCall p) Q s = wlp c Q s" by auto 
      
          
    lemmas wlp_eq = wlp_skip_eq wlp_assign_idx_eq wlp_arraycpy_eq wlp_arrayinit_eq 
      wlp_assign_locals_eq wlp_seq_eq wlp_scope_eq
    lemmas wlp_eq' = wlp_eq wlp_if_eq
  end
  
  lemma wlp_while_unfold: "wlp (WHILE b DO c) Q s = (if bval b s then wlp c (wlp (WHILE b DO c) Q) s else Q s)"
    apply (subst wlp_equiv[OF while_unfold])
    apply (simp add: wlp_eq')
    done
  
  lemma wp_while_unfold: "wp (WHILE b DO c) Q s = (if bval b s then wp c (wp (WHILE b DO c) Q) s else Q s)"
    apply (subst wp_equiv[OF while_unfold])
    apply (simp add: wp_eq')
    done
    
end ― ‹Context fixing program›

text ‹Unfold rules for procedure scope›
lemma wp_pscope_eq: "wp π (PScope π' c) Q s = wp π' (c) Q s"
  unfolding wp_def by auto

lemma wlp_pscope_eq: "wlp π (PScope π' c) Q s = wlp π' (c) Q s"
  unfolding wlp_def by auto
  
subsubsection ‹Weakest precondition and Program Equivalence›
text ‹The following three statements are equivalent:
 🪙 The commands ‹c› and ‹c'› are equivalent
 🪙 The weakest preconditions are equivalent, for all procedure environments
 🪙 The weakest liberal preconditions are equivalent, for all procedure environments
 ›

lemma wp_equiv_iff: "(∀π. wp π c = wp π c') ⟷ c ∼ c'"
  unfolding equiv_c_def
  using big_step_determ unfolding wp_def
  by (auto; metis)

lemma wlp_equiv_iff: "(∀π. wlp π c = wlp π c') ⟷ c ∼ c'" 
  unfolding equiv_c_def wlp_def
  by (auto; metis (no_types, opaque_lifting))


subsubsection ‹While Loops and Weakest Precondition›  

text ‹Exchanging the loop condition by an equivalent one, and the loop
 body by one with the same weakest precondition, does not change the weakest
 precondition of the loop.›  
lemma sim_while_wp_aux:
  assumes "bval b = bval b'" 
  assumes "wp π c = wp π c'" 
  assumes "π: (WHILE b DO c, s) ==> t"
  shows "π: (WHILE b' DO c', s) ==> t"
  using assms(3,2)
  apply (induction π "WHILE b DO c" s t)
  apply (auto simp: assms(1))
  by (metis WhileTrue big_step_determ wp_def)
        
lemma sim_while_wp: "bval b = bval b' ==> wp π c = wp π c' ==> wp π (WHILE b DO c) = wp π (WHILE b' DO c')"
  apply (intro ext)
  apply (auto 0 3 simp: wp_def intro: sim_while_wp_aux)
  done

text ‹The same lemma for weakest liberal preconditions.›  
lemma sim_while_wlp_aux:
  assumes "bval b = bval b'" 
  assumes "wlp π c = wlp π c'" 
  assumes "π: (WHILE b DO c, s) ==> t"
  shows "π: (WHILE b' DO c', s) ==> t"
  using assms(3,2)
  apply (induction π "WHILE b DO c" s t)
  apply (auto simp: assms(1,2))
  by (metis WhileTrue wlp_def)
        
lemma sim_while_wlp: "bval b = bval b' ==> wlp π c = wlp π c' ==> wlp π (WHILE b DO c) = wlp π (WHILE b' DO c')"
  apply (intro ext)
  apply (auto 0 3 simp: wlp_def intro: sim_while_wlp_aux)
  done
  
      
subsection ‹Invariants for While-Loops›
  text ‹We prove the standard invariant rules for while loops.
 We first prove them in a slightly non-standard form, summarizing the
 loop step and loop exit assumptions. Then, we derive the standard form
 with separate assumptions for step and loop exit.
 ›
    
  subsubsection ‹Partial Correctness›
  lemma wlp_whileI':
    assumes INIT: "I s₀"
    assumes STEP: "∧s. I s ==> (if bval b s then wlp π c I s else Q s)"
    shows "wlp π (WHILE b DO c) Q s₀"
    unfolding wlp_def
  proof clarify
    fix t
    assume "π: (WHILE b DO c, s₀) ==> t"
    thus "Q t" using INIT STEP
    proof (induction π "WHILE b DO c" s₀ t rule: big_step_induct)
      case (WhileFalse s) with STEP show "Q s" by auto
    next
      case (WhileTrue s₁ π s₂ s₃)
      note STEP' = WhileTrue.prems(2)
      
      from STEP'[OF ‹I s₁›] ‹bval b s₁› have "wlp π c I s₁" by simp
      with ‹π: (c, s₁) ==> s₂› have "I s₂" unfolding wlp_def by blast
      moreover have ‹I s₂ ==> Q s₃› using STEP' WhileTrue.hyps(5) by blast 
      ultimately show "Q s₃" by blast
    qed
  qed

  (* Short proof (not the shortest possible one ;) ) *)
  lemma 
    assumes INIT: "I s₀"
    assumes STEP: "∧s. I s ==> (if bval b s then wlp π c I s else Q s)"
    shows "wlp π (WHILE b DO c) Q s₀"
    using STEP
    unfolding wlp_def
    apply clarify subgoal premises prems for t
      using prems(2,1) INIT
      by (induction π "WHILE b DO c" s₀ t rule: big_step_induct; meson)
    done
    
  subsubsection ‹Total Correctness›
  text ‹For total correctness, each step must decrease the state wrt.~a well-founded relation.›
    
  lemma wp_whileI':
    assumes WF: "wf R"
    assumes INIT: "I s₀"
    assumes STEP: "∧s. I s ==> (if bval b s then wp π c (λs'. I s' ∧ (s',s)∈R) s else Q s)"
    shows "wp π (WHILE b DO c) Q s₀"
    using WF INIT 
  proof (induction rule: wf_induct_rule[where a=s₀]) (* Instantiation required to avoid strange HO-unification problem! *)
    case (less s)
    show "wp π (WHILE b DO c) Q s" 
    proof (rule wp_while_unfold[THEN iffD2])
      show "if bval b s then wp π c (wp π (WHILE b DO c) Q) s else Q s" 
      proof (split if_split; intro allI impI conjI)
        assume [simp]: "bval b s"
        
        from STEP ‹I s› have "wp π c (λs'. I s' ∧ (s',s)∈R) s" by simp
        thus "wp π c (wp π (WHILE b DO c) Q) s" proof (rule wp_conseq)
          fix s' assume "I s' ∧ (s',s)∈R"
          with less.IH show "wp π (WHILE b DO c) Q s'" by blast
        qed
      next
        assume [simp]: "¬bval b s"
        from STEP ‹I s› show "Q s" by simp
      qed
    qed
  qed

  (* Short Proof *)  
  lemma 
    assumes WF: "wf R"
    assumes INIT: "I s₀"
    assumes STEP: "∧s. I s ==> (if bval b s then wp π c (λs'. I s' ∧ (s',s)∈R) s else Q s)"
    shows "wp π (WHILE b DO c) Q s₀"
    using WF INIT 
    apply (induction rule: wf_induct_rule[where a=s₀])
    apply (subst wp_while_unfold)
    by (smt STEP wp_conseq)
    
    
  subsubsection ‹Standard Forms of While Rules›  
  lemma wlp_whileI:
    assumes INIT: "I s₀"
    assumes STEP: "∧s. [I s; bval b s ] ==> wlp π c I s"
    assumes FINAL: "∧s. [ I s; ¬bval b s ] ==> Q s"
    shows "wlp π (WHILE b DO c) Q s₀"
    using assms wlp_whileI' by auto
    
    
  lemma wp_whileI:
    assumes WF: "wf R"
    assumes INIT: "I s₀"
    assumes STEP: "∧s. [I s; bval b s ] ==> wp π c (λs'. I s' ∧ (s',s)∈R) s"
    assumes FINAL: "∧s. [ I s; ¬bval b s ] ==> Q s"
    shows "wp π (WHILE b DO c) Q s₀"
    using assms wp_whileI' by auto


subsection ‹Modularity of Programs›    
text ‹Adding more procedures does not change the semantics of the existing ones.›

lemma map_leD: "m⊆_mm' ==> m x = Some v ==> m' x = Some v"
  by (metis domI map_le_def)
  
lemma big_step_mono_prog:
  assumes "π ⊆_m π'"  
  assumes "π:(c,s) ==> t"
  shows "π':(c,s) ==> t"
  using assms(2,1)
  apply (induction π c s t rule: big_step_induct)
  by (auto dest: map_leD)
    
  
text ‹Wrapping a set of recursive procedures into a procedure scope›  
lemma localize_recursion:
  "π': (PScope π c, s) ==> t ⟷ π:(c,s) ==> t"
  by auto
  
  
  
subsection ‹Strongest Postcondition›  

context fixes π :: program begin
  definition "sp P c t ≡ ∃s. P s ∧ π: (c,s) ==> t"

  context notes [simp] = sp_def[abs_def] begin
  
    text ‹Intuition: There exists an old value ‹vx› for the assigned variable›
    lemma sp_arraycpy_eq: "sp P (x[]::=y) t ⟷ (∃vx. let s = t(x:=vx) in t x = s y ∧ P s)" 
      apply (auto simp: big_step_simps)
       apply (intro exI conjI, assumption, auto) []
      apply (intro exI conjI, assumption, auto) []
      done
    
    text ‹Version with renaming of assigned variable›
    lemma sp_arraycpy_eq': "sp P (x[]::=y) t ⟷ t x = t y ∧ (∃vx. P (t(x:=vx,y:=t x)))" 
      apply (auto simp: big_step_simps)
       apply (metis fun_upd_triv)
      apply (intro exI conjI, assumption) 
      apply auto
      done
      
      
    lemma sp_skip_eq: "sp P SKIP t ⟷ P t" by auto
    lemma sp_seq_eq: "sp P (c₁;;c₂) t ⟷ sp (sp P c₁) c₂ t" by auto
    
  end  
end
  
subsection ‹Hoare-Triples›    

text ‹A Hoare-triple summarizes the precondition, command, and postcondition.›
        
definition HT 
  where "HT π P c Q ≡ (∀s₀. P s₀ ⟶ wp π c (Q s₀) s₀)"

definition HT_partial
  where "HT_partial π P c Q ≡ (∀s₀. P s₀ ⟶ wlp π c (Q s₀) s₀)"

text ‹Consequence rule---strengthen the precondition, weaken the postcondition.›  
lemma HT_conseq: 
  assumes "HT π P c Q"
  assumes "∧s. P' s ==> P s"
  assumes "∧s₀ s. [P s₀; P' s₀; Q s₀ s ] ==> Q' s₀ s"
  shows "HT π P' c Q'"
  using assms unfolding HT_def by (blast intro: wp_conseq)

lemma HT_partial_conseq: 
  assumes "HT_partial π P c Q"
  assumes "∧s. P' s ==> P s"
  assumes "∧s₀ s. [P s₀; P' s₀; Q s₀ s ] ==> Q' s₀ s"
  shows "HT_partial π P' c Q'"
  using assms unfolding HT_partial_def by (blast intro: wlp_conseq)
  
  
text ‹Simple rule for presentation in lecture: Use a Hoare-triple during VCG.›
lemma wp_modularity_rule:
  "[HT π P c Q; P s; (∧s'. Q s s' ==> Q' s')] ==> wp π c Q' s"
  unfolding HT_def
  by (blast intro: wp_conseq)


subsubsection ‹Sets of Hoare-Triples›  
type_synonym htset = "((state ==> bool) × com × (state ==> state ==> bool)) set"

definition "HTset π Θ ≡ ∀(P,c,Q)∈Θ. HT π P c Q"
    
definition "HTset_r r π Θ ≡ ∀(P,c,Q)∈Θ. HT π (λs. r c s ∧ P s) c Q"
    
subsubsection ‹Deriving Parameter Frame Adjustment Rules›

text ‹The following rules can be used to derive Hoare-triples when adding
 prologue and epilogue code, and wrapping the command into a scope.
 
 This will be used to implement the local variables and parameter passing protocol
 of procedures.
 ›

text ‹ Intuition:
 New precondition is weakest one we need to ensure ‹P› after prologue.
 ›
lemma adjust_prologue:
  assumes "HT π P body Q"
  shows "HT π (wp π prologue P) (prologue;;body) (λs₀ s. wp π prologue (λs₀. Q s₀ s) s₀)"
  using assms
  unfolding HT_def
  apply (auto simp: wp_eq)
  using wp_def by fastforce

text ‹ Intuition:
 New postcondition is strongest one we can get from ‹Q› after epilogue.
 
 We have to be careful with non-terminating epilogue, though!
 ›  
lemma adjust_epilogue:
  assumes "HT π P body Q"  
  assumes TERMINATES: "∀s. ∃t. π: (epilogue,s) ==> t"
  shows "HT π P (body;;epilogue) (λs₀. sp π (Q s₀) epilogue)"
  using assms
  unfolding HT_def
  apply (simp add: wp_eq)
  apply (force simp: sp_def wp_def)
  done
  
text ‹Intuition:
 Scope can be seen as assignment of locals before and after inner command.
 Thus, this rule is a combined forward and backward assignment rule, for
 the epilogue ‹locals:=<>\› and the prologue ‹locals:=old_locals›.
 ›  
lemma adjust_scope:
  assumes "HT π P body Q"
  shows "HT π (λs. P <<>|s>) (SCOPE body) (λs₀ s. ∃l. Q (<<>|s₀>) (<l|s>))"
  using assms unfolding HT_def
  apply (auto simp: wp_eq combine_nest)
  apply (auto simp: wp_def) 
  by (metis combine_collapse)

subsubsection ‹Proof for Recursive Specifications›

text ‹Prove correct any set of Hoare-triples, e.g., mutually recursive ones.›
lemma HTsetI:    
  assumes "wf R"
  assumes RL: "∧P c Q s₀. [ HTset_r (λc' s'. ((c',s'),(c,s₀))∈R ) π Θ; (P,c,Q)∈Θ; P s₀ ] ==> wp π c (Q s₀) s₀"
  shows "HTset π Θ"
  unfolding HTset_def HT_def 
proof clarsimp
  fix P c Q s₀
  assume "(P,c,Q)∈Θ" "P s₀"
  with ‹wf R› show "wp π c (Q s₀) s₀"
    apply (induction "(c,s₀)" arbitrary: c s₀ P Q)
    using RL unfolding HTset_r_def HT_def
    by blast
    
qed  
    

lemma HT_simple_recursiveI:
  assumes "wf R"
  assumes "∧s. [HT π (λs'. (f s', f s)∈R ∧ P s') c Q; P s ] ==> wp π c (Q s) s"
  shows "HT π P c Q"
  using HTsetI[where R="inv_image R (f o snd)" and π=π and Θ = "{(P,c,Q)}"] assms
  by (auto simp: HTset_r_def HTset_def)


lemma HT_simple_recursive_procI:
  assumes "wf R"
  assumes "∧s. [HT π (λs'. (f s', f s)∈R ∧ P s') (PCall p) Q; P s ] ==> wp π (PCall p) (Q s) s"
  shows "HT π P (PCall p) Q"
  using HTsetI[where R="inv_image R (f o snd)" and π=π and Θ = "{(P,PCall p,Q)}"] assms
  by (auto simp: HTset_r_def HTset_def)
  
  
    
lemma
  assumes "wf R"
  assumes "∧s P p Q. [
    ∧P' p' Q'. (P',p',Q')∈Θ
      ==> HT π (λs'. ((p',s'),(p,s))∈R ∧ P' s') (PCall p') Q';
    (P,p,Q)∈Θ; P s
  ] ==> wp π (PCall p) (Q s) s"
  shows "∀(P,p,Q)∈Θ. HT π P (PCall p) Q"  
proof -

  have "HTset π {(P, PCall p, Q) |P p Q. (P, p, Q) ∈ Θ}"
    apply (rule HTsetI[where R="inv_image R (λx. case x of (PCall p,s) ==> (p,s))"])
    subgoal using ‹wf R› by simp
    subgoal for P c Q s
      apply clarsimp
      apply (rule assms(2)[where P=P])
        apply simp_all
      unfolding HTset_r_def
      proof goal_cases
        case (1 p P' p' Q')
        
        from "1"(1)[rule_format, of "(P',PCall p',Q')", simplified] "1"(2-)
          show ?case by auto
      qed
    done
    
  thus ?thesis by (auto simp: HTset_def)
qed
    

subsection ‹Completeness of While-Rule›

text ‹Idea: Use ‹wlp› as invariant›
lemma wlp_whileI'_complete:
  assumes "wlp π (WHILE b DO c) Q s₀"
  obtains I where
    "I s₀"
    "∧s. I s ==> if bval b s then wlp π c I s else Q s"
proof
  let ?I = "wlp π (WHILE b DO c) Q"
  {
    show "?I s₀" by fact
  next
    fix s
    assume "?I s"
    then show "if bval b s then wlp π c ?I s else Q s"
      apply (subst (asm) wlp_while_unfold) 
      .
  }  
qed
   
text ‹Idea: Remaining loop iterations as variant›

inductive count_it for π b c where
  "¬bval b s ==> count_it π b c s 0"
| "[bval b s; π: (c,s) ==> s'; count_it π b c s' n ] ==> count_it π b c s (Suc n )"  

lemma count_it_determ:
  "count_it π b c s n ==> count_it π b c s n' ==> n' = n"
  apply (induction arbitrary: n' rule: count_it.induct)
  subgoal using count_it.cases by blast 
  subgoal by (metis big_step_determ count_it.cases)
  done

lemma count_it_ex:   
  assumes "π: (WHILE b DO c,s) ==> t"
  shows "∃n. count_it π b c s n"
  using assms
  apply (induction π "WHILE b DO c" s t arbitrary: b c)
   apply (auto intro: count_it.intros)
  done

definition "variant π b c s ≡ THE n. count_it π b c s n"  

lemma variant_decreases:
  assumes STEPB: "bval b s" 
  assumes STEPC: "π: (c,s) ==> s'" 
  assumes TERM: "π: (WHILE b DO c,s') ==> t"
  shows "variant π b c s' < variant π b c s"
proof -
  from count_it_ex[OF TERM] obtain n' where CI': "count_it π b c s' n'" ..
  moreover from count_it.intros(2)[OF STEPB STEPC this] have "count_it π b c s (Suc n')" .
  ultimately have "variant π b c s' = n'" "variant π b c s = Suc n'" 
    unfolding variant_def using count_it_determ by blast+
  thus ?thesis by simp 
qed

lemma wp_whileI'_complete:
  fixes π b c
  defines "R≡measure (variant π b c)"
  assumes "wp π (WHILE b DO c) Q s₀"
  obtains I where
    "wf R"
    "I s₀"
    "∧s. I s ==> if bval b s then wp π c (λs'. I s' ∧ (s',s)∈R) s else Q s"
proof   
  show ‹wf R› unfolding R_def by auto
  let ?I = "wp π (WHILE b DO c) Q"
  {
    show "?I s₀" by fact
  next
    fix s
    assume "?I s"
    then show "if bval b s then wp π c (λs'. ?I s' ∧ (s',s)∈R) s else Q s"
      apply (subst (asm) wp_while_unfold) 
      apply clarsimp
      by (auto simp: wp_def R_def intro: variant_decreases)
      
  }  
qed  
    
    
      
  
  
end