Theory Examples

section "Examples"

theory Examples imports DivLogicSoundness

begin

definition pure_loop :: prog where
  "pure_loop = While (λ_. 1) Skip"

lemma pure_loop_correct:
  "pohjola (λs. output_of s = []) pure_loop (λl. l = LNil)"
  unfolding pure_loop_def
  apply (rule p_while1)
  apply (rule_tac x="λi s. True" in exI)
  apply (simp add: ignores_output_def guard_def)
  apply (rule_tac x="λ_. []" in exI, simp)
  done

definition zero :: prog where
  "zero = While (λ_. 1) (Print (λ_. 0))"

definition zero_llist :: "nat llist" where
  "zero_llist = iterates id 0"

lemma zero_correct:
  "pohjola (λs. output_of s = []) zero (λl. l = zero_llist)"
  unfolding zero_def
  apply (rule p_while1)
  apply (rule_tac x="λi s. True" in exI)
  apply (simp add: ignores_output_def guard_def)
  apply (rule_tac x="λ_. [0]" in exI)
  apply (rule conjI; clarsimp)
   apply (simp add: Coinductive_List.inf_llist_def zero_llist_def)
   apply (simp add: lmap_iterates_id)
  apply (rule h_weaken)
    prefer 2
    apply (rule h_print)
  by (auto simp: print_def)

(* example of p_while2 *)
definition ex2 where
  "ex2 = While (λ_. 1) zero"

lemma ex2_correct:
  "pohjola (λs. output_of s = []) ex2 (λl. l = zero_llist)"
  unfolding ex2_def
  apply (rule p_while2[where R="λx y. (x, y) ∈ (measure (λx. 0))" and b="λ_. False"])
     apply (simp_all add: guard_def)
   apply (rule hoare_pre_False)
  apply (rule zero_correct)
  done

end