Adc2017.thy

theory Adc2017
imports Main
begin

section {* States *}

type_synonym id = string
type_synonym state = "id ⇒ nat"

definition empty :: "state" where
  "empty _ = 0"

no_syntax
  "_maplet"  :: "['a, 'a] ⇒ maplet"             ("_ /↦/ _")

fun update :: "state ⇒ id ⇒ nat ⇒ state" ("_[_ ↦ _]" [80,80,80] 80) where
  "update st x n y = (if x = y then n else st y)"

section {* Arithmetic and Boolean Expressions *}

subsection {* Syntax *}

datatype aexp = ANum nat | AId id | APlus aexp aexp | AMinus aexp aexp | AMult aexp aexp
datatype bexp = BTrue | BFalse | BEq aexp aexp | BLeq aexp aexp | BAnd bexp bexp | BNot bexp

subsection {* Evaluation *}

fun aeval :: "state ⇒ aexp ⇒ nat" where
  "aeval st (ANum n) = n"
  | "aeval st (AId x) = st x"
  | "aeval st (APlus a1 a2) = aeval st a1 + aeval st a2"
  | "aeval st (AMinus a1 a2) = aeval st a1 - aeval st a2"
  | "aeval st (AMult a1 a2) = aeval st a1 * aeval st a2"

fun beval :: "state ⇒ bexp ⇒ bool" where
  "beval st BTrue = True"
  | "beval st BFalse = False"
  | "beval st (BEq a1 a2) = (aeval st a1 = aeval st a2)"
  | "beval st (BLeq a1 a2) = (aeval st a1 ≤ aeval st a2)"
  | "beval st (BNot b) = (¬ beval st b)"
  | "beval st (BAnd b1 b2) = (beval st b1 ∧ beval st b2)"

fun bool_to_bexp :: "bool ⇒ bexp" where
  "bool_to_bexp b = (if b then BTrue else BFalse)"
  
section {* Commands *}

subsection {* Syntax *}

datatype com = CSkip | CAssign id aexp | CSeq com com | CIf bexp com com | CWhile bexp com

notation
  CSkip ("SKIP") and
  CAssign ("_ ::= _" [50,50] 90) and
  CSeq (infixr ";;" 30) and
  CIf ("IF _ THEN _ ELSE _" 80) and
  CWhile ("WHILE _ DO _" 90)

section {* Small-step operational semantics *}

subsection {* Definition *}

inductive csmall :: "com ⇒ state ⇒ com ⇒ state ⇒ bool" ("<_,_> ⟶ <_,_>" [10,10,10,10] 90) where
  S_AssNum: "<x ::= ANum n , st> ⟶ <SKIP , st [x ↦ n]>"
| S_AssStep: "<x ::= a , st> ⟶ <x ::= ANum (aeval st a) , st>"
| S_SeqSkip: "<SKIP ;; c , st> ⟶ <c,st>"
| S_SeqStep: "<c1,st> ⟶ <c1',st'> ⟹ <c1 ;; c2 , st> ⟶ <c1' ;; c2 , st'>"
| S_IfTrue: "<IF BTrue THEN c1 ELSE c2 , st> ⟶ <c1 , st>"
| S_IfFalse: "<IF BFalse THEN c1 ELSE c2 , st> ⟶ <c2 , st>"
| S_IfStep: "<IF b THEN c1 ELSE c2 , st> ⟶ <IF (bool_to_bexp (beval st b)) THEN c1 ELSE c2 , st>"
| S_WHILE: "<WHILE b DO c , st> ⟶ <IF b THEN c ;; WHILE b DO c ELSE SKIP , st>"

section {* Big-step operational semantics *}

subsection {* Definition *}

inductive cbig :: "com ⇒ state ⇒ state ⇒ bool" ("<_,_> ⇓ _" [10,10,10] 70) where
  B_Skip: "<SKIP,st> ⇓ st"
| B_Ass: "<x ::= a , st> ⇓ (st [x ↦ aeval st a])"
| B_Seq: "⟦ <c1,st1> ⇓ st2; <c2,st2> ⇓ st3 ⟧ ⟹ <c1 ;; c2 , st1> ⇓ st3"
| B_IfTrue: "⟦ beval st b = True; <c1,st> ⇓ st' ⟧ ⟹ <IF b THEN c1 ELSE c2 , st> ⇓ st'"
| B_IfFalse: "⟦ beval st b = False; <c2,st> ⇓ st' ⟧ ⟹ <IF b THEN c1 ELSE c2 , st> ⇓ st'"
| B_WhileFalse: "beval st b = False ⟹ <WHILE b DO c , st> ⇓ st"
| B_WhileStep: "⟦ beval st b = True; <c,st> ⇓ st'; <WHILE b DO c , st'> ⇓ st'' ⟧ ⟹ <WHILE b DO c , st> ⇓ st''"

subsection {* Coherent lemmas *}

lemma coh_B_Skip:
  assumes "<SKIP,st> ⇓ st'"
  shows "st = st'"
using cbig.cases [OF assms] by auto

lemma coh_B_Ass:
  assumes "<x ::= a , st> ⇓ st'"
  shows "st' = st [x ↦ aeval st a]"
using cbig.cases [OF assms] by auto

lemma coh_B_Seq:
  assumes "<c1 ;; c2 , st> ⇓ st'"
  obtains st'' where "<c1 , st> ⇓ st''" and "<c2 , st''> ⇓ st'"
proof-
  have "<c1 ;; c2 , st> ⇓ st' ⟹ ∃st''. (<c1 , st> ⇓ st'') ∧ (<c2 , st''> ⇓ st')"
    by (cases rule: cbig.cases, auto)
  then obtain st'' where "<c1 , st> ⇓ st''" and "<c2 , st''> ⇓ st'"
    by (simp add: assms, auto)
  then show ?thesis
    using that by blast
qed

lemma coh_B_IfTrue:
  assumes "<IF b THEN c1 ELSE c2 , st> ⇓ st'"
  and "beval st b = True"
  shows "<c1 , st> ⇓ st'"
proof-
  have "<IF b THEN c1 ELSE c2 , st> ⇓ st' ⟹ <c1,st> ⇓ st'"
    apply (cases rule: cbig.cases, auto)
    using assms(2) apply auto
    done
  then show ?thesis by (simp add: assms(1))
qed

lemma coh_B_IfFalse:
  assumes "<IF b THEN c1 ELSE c2 , st> ⇓ st'"
  and "beval st b = False"
  shows "<c2 , st> ⇓ st'"
proof-
  have "<IF b THEN c1 ELSE c2 , st> ⇓ st' ⟹ <c2,st> ⇓ st'"
    apply (cases rule: cbig.cases, auto)
    using assms(2) apply auto
    done
  then show ?thesis by (simp add: assms(1))
qed

lemma coh_B_WhileFalse:
  assumes "beval st b = False"
  and "<WHILE b DO c , st> ⇓ st'"
  shows "st = st'"
proof-
  have "<WHILE b DO c , st> ⇓ st' ⟹ st = st'"
    apply (erule cbig.cases, auto)
    apply (simp add: assms(1))
    done
  then show ?thesis by (simp add: assms(2))
qed

lemma coh_B_WhileStep:
  assumes "beval st b = True"
  and "<WHILE b DO c , st> ⇓ st''"
  obtains "st'" where "<c,st> ⇓ st'" and "<WHILE b DO c , st'> ⇓ st''"
proof-
  have "<WHILE b DO c , st> ⇓ st'' ⟹ ∃st'. (<c,st> ⇓ st') ∧ (<WHILE b DO c , st'> ⇓ st'')"
    by (erule cbig.cases, auto simp add: assms(1))
  then obtain "st'" where "<c,st> ⇓ st'" and "<WHILE b DO c , st'> ⇓ st''"
    by (simp add: assms, auto)
  then show ?thesis
    using that by blast
qed

lemma while_induction:
  assumes red: "<WHILE b DO c , st> ⇓ st'"
  and base: "⋀t t'. ⟦ ¬ beval t b; t = t' ⟧ ⟹ P t t'"
  and step: "⋀t t' t''. ⟦ beval t b; <c,t> ⇓ t'; <WHILE b DO c,t'> ⇓ t''; P t' t'' ⟧ ⟹ P t t''"
  shows "P st st'"
proof-
  have "<WHILE b DO c , st> ⇓ st' ⟹ P st st'"
    using cbig.induct [of _ _ _ "λc0 t t'. (WHILE b DO c) = c0 ⟶ P t t'"] apply rule
    apply (auto simp add: base)
    apply (fastforce simp add: step)
    apply (fastforce simp add: step)
    done
  thus ?thesis by (simp add: red) 
qed      
  
subsection {* Determinism *}

lemma cbig_deterministic: "⟦ <c,st> ⇓ st'; <c,st> ⇓ st'' ⟧ ⟹ st' = st''"
proof-
  have "<c,st> ⇓ st' ⟹ (∀st''. (<c,st> ⇓ st'') ⟶ st' = st'')"
    apply (induction rule: cbig.induct)
      apply (simp add: coh_B_Skip)
      apply (rule, rule) using coh_B_Ass apply auto[1]
      apply (rule, rule, erule coh_B_Seq, simp)
      using coh_B_IfTrue apply blast
      using coh_B_IfFalse apply blast
      apply (simp add: coh_B_WhileFalse)
      by (metis coh_B_WhileStep)
  then show "⟦ <c,st> ⇓ st'; <c,st> ⇓ st'' ⟧ ⟹ st' = st''"
    by simp
qed

section {* Properties *}

subsection {* Small-step and Big-step *}

subsubsection {* small-step long reduction *}

inductive csmall_long ("<_,_> ⟶* <_,_>") where
  SL_refl: "<c,st> ⟶* <c,st>"
| SL_trans1: "⟦ <c,st> ⟶ <c',st'>; <c',st'> ⟶* <c'',st''> ⟧ ⟹ <c,st> ⟶* <c'',st''>"

lemma SL_trans: "⟦ <c,st> ⟶* <c',st'>; <c',st'> ⟶* <c'',st''> ⟧ ⟹ <c,st> ⟶* <c'',st''>"
apply (induction arbitrary: c'' st'' rule: csmall_long.induct)
apply simp
apply (blast intro: SL_trans1)
done

lemma SL_SeqStep: "<c1,st> ⟶* <c1',st'> ⟹ <c1;;c2,st> ⟶* <c1';;c2,st'>"
apply (induction arbitrary: c2 rule: csmall_long.induct)
apply (rule SL_refl)
using SL_trans1 S_SeqStep by blast

lemma csmall_step: "⟦ <c,st> ⟶ <c',st'>; <c',st'> ⇓ st'' ⟧ ⟹ <c,st> ⇓ st''"
apply (induction arbitrary: st'' rule: csmall.induct)
  apply (metis B_Ass aeval.simps(1) coh_B_Skip)
  using B_Ass coh_B_Ass apply fastforce
  using B_Seq B_Skip apply blast
  apply (meson B_Seq coh_B_Seq)
  apply (simp add: B_IfTrue)
  apply (simp add: B_IfFalse)
  apply (metis B_IfFalse B_IfTrue beval.simps(1) beval.simps(2) bool_to_bexp.simps coh_B_IfFalse coh_B_IfTrue)
  apply (metis B_WhileFalse B_WhileStep coh_B_IfFalse coh_B_IfTrue coh_B_Seq coh_B_Skip)
  done

lemma csmall_steps: "⟦ <c,st> ⟶* <c',st'>; <c',st'> ⇓ st'' ⟧ ⟹ <c,st> ⇓ st''"
apply (induction arbitrary: st'' rule: csmall_long.induct)
apply simp
apply (simp add: csmall_step)
done

theorem "<c,st> ⟶* <SKIP,st'> ⟷ <c,st> ⇓ st'"
proof rule
  assume hyp: "<c,st> ⟶* <SKIP,st'>"
  have "<SKIP,st'> ⇓ st'" by rule
  then show "<c,st> ⇓ st'"
    by (rule csmall_steps [OF hyp])
next
  show "<c,st> ⇓ st' ⟹ <c,st> ⟶* <SKIP,st'>"
    apply (erule cbig.inducts)
    apply (simp add: SL_refl)
    apply (meson S_AssNum S_AssStep csmall_long.simps)
    using SL_SeqStep SL_trans SL_trans1 S_SeqSkip apply blast
    apply (metis SL_trans1 S_IfStep S_IfTrue bool_to_bexp.simps)
    apply (metis S_IfFalse S_IfStep bool_to_bexp.simps csmall_long.simps)
    apply (metis SL_refl SL_trans1 S_IfFalse S_IfStep S_WHILE bool_to_bexp.simps)
    proof-
      fix st b c st' st''
      assume b: "beval st b = True"
      and "<c,st> ⇓ st'"
      and h: "<c,st> ⟶* <SKIP,st'>"
      and "<WHILE b DO c,st'> ⇓ st''"
      and j: "<WHILE b DO c,st'> ⟶* <SKIP,st''>"
      
      have "<WHILE b DO c,st> ⟶* <IF b THEN c ;; WHILE b DO c ELSE SKIP,st>"
        using SL_refl SL_trans1 S_WHILE by blast
      moreover have "<IF b THEN c ;; WHILE b DO c ELSE SKIP,st> ⟶* <c ;; WHILE b DO c , st>"
        using b by (metis S_IfStep S_IfTrue bool_to_bexp.simps csmall_long.simps)
      moreover have "<c ;; WHILE b DO c , st> ⟶* <SKIP ;; WHILE b DO c , st'>"
        by (rule SL_SeqStep, rule h)
      moreover have "<SKIP ;; WHILE b DO c , st'> ⟶* <WHILE b DO c , st'>"
        by (rule, rule, rule)
      moreover have "<WHILE b DO c , st'> ⟶* <SKIP,st''>"
        by (rule j)
      ultimately show "<WHILE b DO c,st> ⟶* <SKIP,st''>"
        using SL_trans by blast
    qed
qed

end