NikDenNaiveExercise.thy

theory NikDenNaiveExercise

imports NikInstructions

begin

text ‹The denotation of an instruction is a relation between states.›

type_synonym instr_den = ‹state rel› ― ‹same as ‹(state × state) set››

fun nik_den:: ‹instruction ⇒ instr_den› (‹⟦ _ ⟧›)
where
  Nop_den:    ‹⟦Nop⟧ = Id›
| Var_den:    ‹⟦var v⟧ = {(s, s'). s' = s(v:=0)}›
| Assign_den: ‹⟦v<-val⟧ = Id› ― ‹FIX ME›
― ‹Hint for the next one: 
  O is the composition of relations (like o is the composition of functions):
  ⟦ (a, b) ∈ r ; (b, c) ∈ s ⟧ ⟹ (a, c) ∈ r O s
›
| Seq_den:    ‹⟦i1;; i2⟧ = Id O Id› ― ‹FIX ME›
| Alt_den:    ‹⟦if c then iT else iF fi⟧ = Id› ― ‹FIX ME›
| While_den:  ‹⟦while c do body done⟧ = Id› ― ‹FIX ME›
end

RecursionExercise.thy

theory RecursionExercise
imports Main
begin

text ‹Define the factorial›
fun f :: ‹nat => nat›
where
   ‹f 0 = 1›
 | ‹f (Suc n) = undefined› ― ‹FIX ME›

text ‹Some checks›
value ‹f 0›
value ‹f 1›
value ‹f 5›


text ‹Define the functor whose fixed point is the factorial›
definition Fact :: ‹(nat => nat) => (nat => nat)›
where
   ‹Fact u ≡ undefined› ― ‹FIX ME›

text ‹
  Check what happens with successive applications 
  of the functor to the null function.
  ^^ is the composition power: f^^n = f ∘ f ∘ ... ∘ f n times
›
text ‹A function that always returns the special Isabelle/HOL constant 'undefined'›
abbreviation ‹undef ≡ (λn. undefined)›

value ‹Fact undef›
value ‹(Fact undef) 0›
value ‹(Fact (Fact undef)) 1›
value ‹((Fact^^2) undef) 1›
value ‹((Fact^^3) undef) 2›
value ‹((Fact^^4) undef) 3›
value ‹((Fact^^5) undef) 4›
value ‹((Fact^^6) undef) 5›

text ‹Show that f is a fixed point of Fact›
lemma ‹Fact f = f›
  sorry


text ‹Non constructive definition of the factorial›
function g ::‹nat ⇒ nat›
where
  ‹g 0 = 1›
| ‹g (Suc n) = undefined› ― ‹FIX ME›

text ‹Define the matching functor›
definition G :: ‹(nat => nat) => (nat => nat)›
where
   ‹G u ≡ undefined› ― ‹FIX ME›


text ‹
  Check what happens with successive applications 
  of the functor to the null function.
›
value ‹(G undef) 0›
value ‹((G^^10) undef) 1› (* Cannot build g *)

text ‹
  The factorial f is also a fixed point of G,
  but we cannot use G^^i to approximate it.
›
lemma ‹G f = f›
  sorry

text ‹Conjecture de Syracuse›
fun h :: ‹nat ⇒ nat›
where
  ‹h n = undefined› ― ‹FIX ME›

text ‹Some checks...›
value ‹h 0›
value ‹h 2›
value ‹h (1+1)›

text ‹Definition of the matching functor›
definition Syr :: ‹(nat => nat) => (nat => nat)›
where
  ‹Syr u ≡ undefined› ― ‹FIX ME›

text ‹Find the right power P to be able to terminate each call›
value ‹Syr undef 0›
value ‹Syr undef 1›
value ‹(Syr^^P) undef 2›
value ‹(Syr^^P) undef 3›
value ‹(Syr^^P) undef 4›
value ‹(Syr^^P) undef 5›
value ‹(Syr^^P) undef 6›

text ‹Show that λn. 1 a fixed point of Syr›
lemma ‹Syr (λn. 1) = (λn. 1)›
  sorry

end

FacExercise.thy

theory FacExercise

imports Main

begin
section ‹Fixed point semantics›

text ‹
  In this theory, we consider functions as relations, which are sets of pairs
  of elements: a ℛ b is the same as (a, b) ∈ {(x, y). x ℛ y}.
›
text ‹
  Fac is a functor, which takes a partial function int ⇒ int
  and yields a more defined partial function.
  Starting from the function defined nowhere (the empty set {}), it
  yields {(0,1)} which is a partial function that gives the factorial of 0.
  Given a partial function interpreted as a set of (n, n!) pairs, it yields
  a partial function defining the (n+1, (n+1)!) pairs using:
    n! = n (n-1)!, which leads to: (n+1)! = (n+1)n!
›
text ‹
▪ {}
▪ Fac {} = {(0,1)}
▪ Fac (Fac {}) = Fac {(0,1)} = {(0,1), (1, 1*1)}
▪ Fac (Fac (Fac {})) = Fac {(0,1), (1, 1)} = {(0,1), (1, 1*1), (2, 2*1)}
▪ Fac (Fac (Fac (Fac {}))) = Fac {(0,1), (1, 1), (2, 2)} = {(0,1), (1, 1*1), (2, 2*1), (3, 3*2)}
›

definition Fac:: ‹int rel ⇒  int rel›
where
  ‹Fac f ≡ {(0,1)} ∪ image (λ(n, fac_n). undefined ― ‹FIX ME›) f›

text ‹
  Applying Fac ten times to the empty set yields a partial function
  which gives the factorial of 0 .. 9 *)
›
value ‹(Fac ^^ 1) {}›
value ‹(Fac ^^ 2) {}›
value ‹(Fac ^^ 3) {}›
value ‹(Fac ^^ 4) {}›
value ‹(Fac ^^ 5) {}›

value ‹(Fac ^^ 10){}›

text ‹Definition of the factorial as the least fixed point of Fac›
definition fac:: ‹int rel›
where
  ‹fac ≡ lfp Fac›

text ‹
  In order to use this definition, we have to prove that Fac 
  is monotone, i.e. that it always adds information
›
lemma mono_Fac: ‹mono Fac›
  sorry


thm funpow_simps_right
text ‹
  Each time we apply Fac to an approximation of fac, we get a better approximation.
  Show that we can compute 3! using the 4th approximation of the factorial
›
lemma Fac_3 : ‹(3, 6) ∈ (Fac ^^ Suc(Suc(Suc(Suc 0)))){}›
  sorry

lemma Four_suc:‹4 = (Suc (Suc (Suc (Suc 0))))› by simp

lemma Fac_3' : ‹(3, 6) ∈ (Fac^^4){}›
  sorry

text ‹Show that any iteration of Fac on the empty set is an approximation of fac›
lemma fac_approx : ‹(Fac ^^ (n::nat)){} ⊆ fac›
  sorry

thm Set.subsetD
thm Set.subsetD[OF fac_approx]
thm Set.subsetD[OF fac_approx, of _ 4]

text ‹Show that 6 is 3!›
lemma fac_3 : ‹(3, 6) ∈ fac›
  sorry

end

NikDenotational.thy

theory NikDenotational

imports NikInstructions

begin
text ‹The denotation of an instruction is a relation between states.›
type_synonym instr_den = ‹state rel›

text ‹
  A functor to define the semantics of while as a least fixed point.
  This functor receives the condition of the loop and the denotation of its body
  and returns a function which associates to a denotation:
    - the identity denotation if the condition evaluates to false
    - the composition of the denotation of the body and the denotation given 
      as argument if the condition evaluates to true.
  This definition matches Nop (whose denotation is the identity) when the 
  condition of the loop is false, and the sequence of the previous executions
  of the body and a new execution of the body when the condition is true.
  The denotation of the while loop is the least fixed point of this functor, 
  which is reached in a finite number of iterations of the functor when the
  loop terminates. Greater fixed points are not suitable as denotations of the
  while loop because they could make unwanted modifications of the state.

  O is the composition of relations (like o is the composition of functions):
  (a, b) ∈ r ⟹ (b, c) ∈ s ⟹ (a, c) ∈ r O s
›
definition while_func:: ‹(state ⇒ bool) ⇒ instr_den ⇒ (instr_den ⇒ instr_den)›
where
  ‹while_func cond body_den ≡ (
    λw_den. {(pre, post).
              if cond pre then
                (pre, post) ∈ body_den O w_den
              else post = pre
            })›

text ‹A fixed point exists if the while_func functor  is monotone›
lemma while_mono: ‹mono (while_func cond_den body_den)›
(* unfolding while_func_def mono_def by auto *)
apply(unfold while_func_def)
apply(unfold mono_def)
apply(auto)
done

text ‹More detailed proof›
lemma while_mono2: ‹mono (while_func cond_den body_den)›
proof
  fix x::instr_den and y::instr_den
  assume ‹x ⊆ y›
  thus ‹while_func cond_den body_den x ⊆ while_func cond_den body_den y›
       unfolding while_func_def by auto
qed

fun nik_den:: ‹instruction ⇒ instr_den› (‹⟦ _ ⟧›)
where
  Nop_den:    ‹⟦Nop⟧ = Id›
| Var_den:    ‹⟦var v⟧ = {(s, s'). s' = s(v:=0)}›
| Assign_den: ‹⟦v<-val⟧ = {(s, s'). s' = s(v:=evaluate val s)}›
| Seq_den:    ‹⟦i1;; i2⟧ = ⟦i1⟧ O ⟦i2⟧›
| Alt_den:    ‹⟦if c then iT else iF fi⟧ =
                {(s, s').
                 if evalbool c s then
                   (s, s') ∈ ⟦iT⟧
                 else
                   (s, s') ∈ ⟦iF⟧
                }›
| While_den:  ‹⟦while c do body done⟧ = lfp (while_func (evalbool c) ⟦body⟧)›

text ‹Simple check›
lemma ‹⟦''x''<-N 2⟧ = {(s, s'). s'=s(''x'':=2)}›
by simp

end

NikDenLoops.thy

theory NikDenLoops

imports NikDenotational

begin

text ‹Consider an infinite loop over a Nop›
abbreviation inf_nop where ‹inf_nop ≡ (while B True do Nop done)›

text ‹Show that the while functor applied to the denotation of this loop is the identity›
lemma w_true_nop_id: ‹while_func (evalbool (B True)) ⟦Nop⟧ = (λw. w)›
unfolding while_func_def by simp

text ‹
  Therefore, any denotation is a fixed point of the while functor for this loop.
  Choosing the least one amounts to choosing the empty denotation: this loop
  never terminates so it defines no relation between states.
›
thm lfp_lowerbound
lemma empty_lfp: ‹lfp (λw. w) = {}›
proof
  have ‹(λw. w) {} ⊆ {}› ..
  thus ‹lfp (λw. w) ⊆ {}› using lfp_lowerbound[of ‹λw. w› ‹{}›] by simp
next
  show ‹{} ⊆ lfp (λw. w)› by simp
qed

lemma ‹⟦while B True do Nop done⟧ = {}›
 using empty_lfp w_true_nop_id by simp

text ‹Consider a no-loop over a Nop›
abbreviation nop_loop where ‹nop_loop ≡ (while B False do Nop done)›

text ‹Show that the condition of the loop is always false›
lemma w_nop_loop: ‹while_func (evalbool (B False)) ⟦Nop⟧
                    = while_func (λs. False) Id›
unfolding while_func_def by simp

text ‹Show that this loop does nothing›
lemma w_nop_loop_ok: ‹while_func (evalbool (B False)) ⟦Nop⟧
                      = (λw. {(pre, post). post=pre})›
  using w_nop_loop unfolding while_func_def by simp

text ‹Finally, show that the no-loop behaves as Nop›
lemma ‹⟦while B False do Nop done⟧ = ⟦Nop⟧›
  unfolding While_den lfp_def using w_nop_loop_ok by auto


text ‹Generalization to a loop with anything inside the body›
lemma w_no_loop: ‹while_func (evalbool (B False)) ⟦instr⟧
                    = while_func (λs. False) ⟦instr⟧›
unfolding while_func_def by simp

text ‹Show that this loop does nothing›
lemma w_no_loop_ok: ‹while_func (evalbool (B False)) ⟦instr⟧
                      = (λw. {(pre, post). post=pre})›
  using w_nop_loop unfolding while_func_def by simp

text ‹Finally, show that the no-loop behaves as Nop›
lemma ‹⟦while B False do instr done⟧ = ⟦Nop⟧›
  unfolding While_den lfp_def using w_no_loop_ok by auto


end

NikDenBig.thy

theory NikDenBig

imports NikDenotational NikBigStepProperties

begin

text ‹Equivalence between while loop and unrolled while loop›
lemma unroll_while: ‹⟦ while c do body done ⟧ = ⟦ if c then body;; while c do body done else Nop fi ⟧›
proof -
  let ?w = ‹while c do body done›
  let ?wf = ‹while_func (evalbool c) ⟦ body ⟧›
  from While_den have ‹⟦ ?w ⟧ = lfp ?wf› .
  also have ‹... = ?wf (lfp ?wf)› by (rule lfp_unfold[OF while_mono])
  also have ‹... = ?wf ⟦ ?w ⟧› by simp
  also have ‹... = {(pre, post). if (evalbool c) pre
                                 then (pre,post) ∈ ⟦ body ⟧ O ⟦ ?w ⟧
                                 else post = pre }› unfolding while_func_def ..
  also have ‹... = {(pre, post). if (evalbool c) pre
                                 then (pre, post) ∈ ⟦ body ;; ?w ⟧
                                 else post = pre }› using Seq_den by simp
  also have ‹... = ⟦ if c then body;; ?w else Nop fi ⟧› by auto
  finally show ?thesis .
qed

text ‹Show that the big step semantics is included in the denotational semantics›
lemma big_step_in_den: ‹(prog, pre) ↝ post ⟹ (pre, post) ∈ ⟦ prog ⟧›
proof (induction rule: big_step_induct) print_cases
  case WhileFalse thus ?case using unroll_while by simp
next
  case WhileTrue print_facts
  show ?case unfolding unroll_while using WhileTrue by auto
qed auto

text ‹Show that the denotational semantics is included in the big step semantics›
lemma den_in_big_step: ‹(pre, post) ∈ ⟦ instr ⟧ ⟹ (instr, pre) ↝ post›
proof (induction instr arbitrary: pre post) print_cases
  case Nop thus ?case by auto
next
  case (VarDecl v) thus ?case (* by force *)
  proof -
    from VarDecl and nik_den.simps(2) have ‹post = pre(v:=0)› by auto
    thus ?thesis by blast
  qed
next
  case (Assign v val) thus ?case
  proof -
    from Assign and nik_den.simps(3) have ‹post = pre(v:=evaluate val pre)› by auto
    thus ?thesis by blast
  qed
next
  case (Alternative cond iT iF) thus ?case
  proof (cases ‹evalbool cond pre›)
    case True
    then show ?thesis
      using Alternative.IH(1) Alternative.prems IfTrue by simp
  next
    case False
    then show ?thesis
      using Alternative.IH(2) Alternative.prems IfFalse by simp
  qed
next
  case (Seq i1 i2) thus ?case (* by force *) print_facts
  proof -
    from Seq.prems obtain p where
        ‹(pre, p) ∈ ⟦ i1 ⟧›
    and ‹(p, post) ∈ ⟦ i2 ⟧› by auto
    thus ?thesis using Seq.IH by blast
  qed
next
  case (While cond body) print_facts
    let ?bigw = ‹{(s, s'). (while cond do body done, s) ↝ s'}›
    let ?wf = ‹while_func (evalbool cond) ⟦ body ⟧›
    have ‹?wf ?bigw ⊆ ?bigw› unfolding while_func_def using While.IH by auto
    from lfp_lowerbound[of ?wf, OF this] and While.prems show ?case by auto
qed

text ‹Finally, show the equivalence of the two semantics›
theorem den_is_big_step: ‹((instr, pre) ↝ post) = ((pre, post) ∈ ⟦ instr ⟧)›
  using big_step_in_den den_in_big_step by blast

end