# 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 (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 (rule_tac x="λ_. [0]" in exI)
apply (rule conjI; clarsimp)
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"])