(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹Examples›

theory Examples
imports
  "../OG_Syntax"
begin

record test =
  x :: nat
  y :: nat

text ‹This is a sequence of two commands, the first being an assign
 protected by two guards. The guards use booleans as their faults.›
definition
  "test_guard ≡ {True} (True, {🚫x=0}),
                       (False, {(0::nat)=0}) ⟼ {True} 🚫y := 0;;
                      {True} 🚫x := 0"

lemma
  "Γ, Θ |⊨_{True}
    COBEGIN test_guard {True},{True}
         ∥ {True} 🚫y:=0 {True}, {True}
    COEND {True},{True}"
  unfolding test_guard_def
  apply oghoare (*11 subgoals*)
           apply simp_all
  done

definition
  "test_try_throw ≡ TRY {True} 🚫y := 0;;
                      {True} THROW
                     CATCH {True} 🚫x := 0
                     END"


subsection ‹Parameterized Examples›

subsubsection ‹Set Elements of an Array to Zero›

record Example1 =
  ex1_a :: "nat → nat"

lemma Example1: 
 "Γ, Θ|⊨!!!_F{True}
   COBEGIN SCHEME [0≤i<n] {True} 🚫ex1_a:=🚫ex1_a (i:=0) {🚫ex1_a i=0}, {False} COEND
  {∀i < n. 🚫ex1_a i = 0}, X"
  apply oghoare (* 7 subgoals *)
        apply (simp ; fail)+
 done

text ‹Same example but with a Call.›
definition
   "Example1'a ≡ {True} 🚫ex1_a:=🚫ex1_a (0:=0)"

definition
   "Example1'b ≡ {True} 🚫ex1_a:=🚫ex1_a (1:=0)"

definition "Example1' ≡
  COBEGIN Example1'a {🚫ex1_a 0=0}, {False}
         ∥
         {True} SCALL 0 0
         {🚫ex1_a 1=0}, {False}
  COEND"

definition "Γ' = Map.empty(0 ↦ com Example1'b)"
definition "Θ' = Map.empty(0 :: nat ↦ [ann Example1'b])"

lemma Example1_proc_simp[unfolded Example1'b_def oghoare_simps]:
 "Γ' 0 = Some (com (Example1'b))"
 "Θ' 0 = Some ([ ann(Example1'b)])"
 "[ ann(Example1'b)]!0 = ann(Example1'b)"
 by (simp add: Γ'_def Θ'_def)+

lemma Example1':
notes Example1_proc_simp[proc_simp]
shows
 "Γ', Θ' |⊨_F Example1' {∀i < 2. 🚫ex1_a i = 0}, {False}"
  unfolding Example1'_def 
  apply simp
  unfolding Example1'a_def Example1'b_def
  apply oghoare (*12 subgoals*)
             apply simp+
   using less_2_cases apply blast
  apply simp
  apply (erule disjE ; clarsimp)
done

type_synonym routine = nat

text ‹Same example but with a Call.›
record Example2 =
  ex2_n :: "routine → nat"
  ex2_a :: "nat → string"

definition
  Example2'n :: "routine → (Example2, string × nat, 'f) ann_com"
where
  "Example2'n i ≡ {🚫ex2_n i= i} 🚫ex2_a:=🚫ex2_a((🚫ex2_n i):='''')"

lemma Example2'n_map_of_simps[simp]:
  "i < n ==>
    map_of (map (λi. ((p, i), g i)) [0..<n])
       (p, i) = Some (g i)"
  apply (rule map_of_is_SomeI)
   apply (clarsimp simp: distinct_map o_def)
   apply (meson inj_onI prod.inject)
  apply clarsimp
  done

definition "Γ'' n ≡
  map_of (map (λi. ((''f'', i), com (Example2'n i))) [0..<n])"

definition "Θ'' n ≡
  map_of (map (λi. ((''f'', i), [ann (Example2'n i)])) [0..<n])"

lemma  Example2'n_proc_simp[unfolded Example2'n_def oghoare_simps]:
 "i<n ==> Γ'' n (''f'',i) = Some ( com(Example2'n i))"
 "i<n ==> Θ'' n (''f'',i) = Some ([ ann(Example2'n i)])"
 "[ ann(Example2'n i)]!0 = ann(Example2'n i)"
 by (simp add: Γ''_def Θ''_def)+

lemmas Example2'n_proc_simp[proc_simp add]

lemma Example2:
notes Example2'n_proc_simp[proc_simp]
shows
 "Γ'' n, Θ'' n
 |⊨!!!_F{True}
   COBEGIN SCHEME [0≤i<n]
     {True}
       CALLX (λs. s(ex2_n:=(ex2_n s)(i:=i))) {🚫ex2_n i = i} (''f'', i) 0
       (λs t. t(ex2_n:= (ex2_n t)(i:=(ex2_n s) i))) (λx y. Skip)
       {🚫ex2_a (🚫ex2_n i)='''' ∧ 🚫ex2_n i = i} {🚫ex2_a i=''''} {False} {False}
     {🚫ex2_a i=''''}, {False}
   COEND
  {∀i < n. 🚫ex2_a i = ''''}, {False}"
  unfolding Example2'n_def ann_call_def call_def block_def 
  apply oghoare (* 113 subgoals *)
  apply (clarsimp ; fail)+
 done

lemmas Example2'n_proc_simp[proc_simp del]

text ‹Same example with lists as auxiliary variables.›

record Example2_list =
  ex2_A :: "nat list"

lemma Example2_list: 
 "Γ, Θ |⊨!!!_F{n < length 🚫ex2_A}
   COBEGIN
     SCHEME [0≤i<n] {n < length 🚫ex2_A} 🚫ex2_A:=🚫ex2_A[i:=0] {🚫ex2_A!i=0},{False}
   COEND
    {∀i < n. 🚫ex2_A!i = 0}, X"
  apply oghoare (*7 subgoals*)
        apply force+
 done


lemma exceptions_example:
  "Γ, Θ |⊨_F
   TRY
   {True } 🚫y := 0;;
   { 🚫y = 0 } THROW
   CATCH
     {🚫y = 0} 🚫x := 🚫y + 1
   END
   { 🚫x = 1 ∧ 🚫y = 0}, {False}"
  by oghoare simp_all

lemma guard_example:
  "Γ, Θ |⊨_{42,66}
  {True} (42, {🚫x=0}),
   (66, {🚫y=0}) ⟼ {🚫x = 0}
   🚫y := 0;;
   {True} 🚫x := 0
  { 🚫x = 0}, {False}"
  apply oghoare (*6 subgoals*)
       apply simp_all
 done

subsubsection ‹Peterson's mutex algorithm I (from Hoare-Parallel) ›

text ‹Eike Best. "Semantics of Sequential and Parallel Programs", page 217.›

record Petersons_mutex_1 =
 pr1 :: nat
 pr2 :: nat
 in1 :: bool
 in2 :: bool
 hold :: nat

lemma peterson_thread_1:
 "Γ, Θ |⊨_F {🚫pr1=0 ∧ ¬🚫in1} WHILE True INV {🚫pr1=0 ∧ ¬🚫in1}
  DO
  {🚫pr1=0 ∧ ¬🚫in1} ⟨🚫in1:=True,, 🚫pr1:=1 ⟩;;
  {🚫pr1=1 ∧ 🚫in1} ⟨🚫hold:=1,, 🚫pr1:=2 ⟩;;
  {🚫pr1=2 ∧ 🚫in1 ∧ (🚫hold=1 ∨ 🚫hold=2 ∧ 🚫pr2=2)}
  AWAIT (¬🚫in2 ∨ ¬(🚫hold=1)) THEN
     🚫pr1:=3
  END;;
  {🚫pr1=3 ∧ 🚫in1 ∧ (🚫hold=1 ∨ 🚫hold=2 ∧ 🚫pr2=2)}
   ⟨🚫in1:=False,,🚫pr1:=0⟩
  OD {🚫pr1=0 ∧ ¬🚫in1},{False}
"
  apply oghoare (*7 subgoals*)
        apply (((auto)[1]) ; fail)+
 done


lemma peterson_thread_2:
 "Γ, Θ |⊨_F {🚫pr2=0 ∧ ¬🚫in2}
  WHILE True INV {🚫pr2=0 ∧ ¬🚫in2}
  DO
  {🚫pr2=0 ∧ ¬🚫in2} ⟨🚫in2:=True,, 🚫pr2:=1 ⟩;;
  \<lbrace>\<acute>pr2=1 \<and> \<acute>in2\<rbrace> \<langle> \<acute>hold:=2,, \<acute>pr2:=2 \<rangle> ;;
  \<lbrace>\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
  AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3 END;;
  \<lbrace>\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
    \<langle>\<acute>in2:=False,, \<acute>pr2:=0\<rangle>
  OD \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>,\<lbrace>False\<rbrace>
 "
  apply oghoare (*7 subgoals*)
  by auto

lemma Petersons_mutex_1:
  "\<Gamma>, \<Theta> |\<tturnstile>\<^bsub>/F\<^esub> \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 \<rbrace>
  COBEGIN
  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<rbrace>  WHILE True INV \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>
  DO
  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace> \<langle> \<acute>in1:=True,, \<acute>pr1:=1 \<rangle>;;
  \<lbrace>\<acute>pr1=1 \<and> \<acute>in1\<rbrace>  \<langle> \<acute>hold:=1,,  \<acute>pr1:=2 \<rangle>;;
  \<lbrace>\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> (\<acute>hold=2 \<and> \<acute>pr2=2))\<rbrace>
  AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN \<acute>pr1:=3  END;;
  \<lbrace>\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> (\<acute>hold=2 \<and> \<acute>pr2=2))\<rbrace>
   \<langle> \<acute>in1:=False,, \<acute>pr1:=0\<rangle>
  OD \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>,\<lbrace>False\<rbrace>
  \<parallel>
  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
  WHILE True INV \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
  DO
  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace> \<langle> \<acute>in2:=True,, \<acute>pr2:=1 \<rangle>;;
  \<lbrace>\<acute>pr2=1 \<and> \<acute>in2\<rbrace> \<langle> \<acute>hold:=2,, \<acute>pr2:=2 \<rangle> ;;
  \<lbrace>\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
  AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3 END;;
  \<lbrace>\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
    \<langle> \<acute>in2:=False,, \<acute>pr2:=0\<rangle>
  OD \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>,\<lbrace>False\<rbrace>
  COEND
  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>,\<lbrace>False\<rbrace>"
  apply oghoare
\<comment> \<open>81 verification conditions.\<close>
  by auto

end