La structure d'un programme Niklaus est la suivante :

program <nom_programme>;
var <var1>, <var2>, ..., <varn>;
{
  // corps du programme
}

Les variables de Niklaus sont du type entier. Les littéraux et les variables peuvent être combinés en expressions à l'aide des quatre opérateurs arithmétiques usuels (+, -, *, /) et des parenthèses.

Pour la condition des instructions de boucle et d'alternative, les expressions peuvent être comparées avec <, <=, =, <>, > et >=.

Les instructions de Niklaus sont :

read <var>

write <var>

<var>:=<expression>

if (<condition>) <instr1> else <instr2>

while (<condition>) <instruction>

Les instructions peuvent être groupées en une instruction en les plaçant entre accolades.

Exemple :

program PGCD;
var a, b;
{
  read a;
  read b;
  while (a <> b) {
    if (a > b) {
      a := a - b;
    } else {
      b := b - a;
    }
  }
  write a;
}

theory NikExpressions
(*
 *  Niklaus arithmetic expressions.
 *
 *  An expression maybe: 
 *  - a constant integer value,
 *  - a variable,
 *  - the sum, difference, product or quotient of two expressions
 *)
imports Main

begin
type_synonym val = int            (* type of the expression value *)
type_synonym varname = string     (* type of the name of a variable *)
(* For evaluating expressions with variables, we need an environment 
   that tells us the value of the variables. So an environment is
   a function from variable names to values. *)
type_synonym environment = "varname ⇒ val"

(* Abstract syntax of the expressions in Niklaus (aka meta-model) *)
datatype expression =
    Value val                  ("N")              (* so N 2 is the number 2 *)
  | Variable varname           ("V")              (* so V ''x'' is the variable ''x'' *)
  | Sum expression expression  (infixr ".+." 65)  (* we add dots to avoid confusion with *)
  | Diff expression expression (infixr ".-." 65)  (* the +, -, * and ÷ predefined operators *)
  | Prod expression expression (infixr ".*." 75)
  | Quot expression expression (infixr ".÷." 75)

(*
 *  Semantics of expressions
 *  We associate an integer value to an expression in an environment that
 *  gives the value of variables.
 *  This semantics is compositional: the semantics of an expression is
 *  given in terms of the semantics of its parts.
 *)
fun evaluate:: "expression ⇒ environment ⇒ val"
where
    "evaluate (N v) env = v"      (* the value of a number is this number *)
  | "evaluate (V n) env = env n"  (* the value of a varible is given by the environment *)
  (* Niklaus arithmetic operations are mapped to the usual operations on integers *)
  | "evaluate (a .+. b) env = evaluate a env + evaluate b env"
  | "evaluate (a .-. b) env = evaluate a env - evaluate b env"
  | "evaluate (a .*. b) env = evaluate a env * evaluate b env"
  | "evaluate (a .÷. b) env = evaluate a env div evaluate b env"

(* A few checks *)
value "evaluate (N 2 .+. N 3) (λx. 0)"
value "evaluate (V ''x'' .+. N 3) ((λu. 0)(''x'':=5))"

end

theory NikExprSimplify
(*
 * Simplification of Niklaus arithmetic expressions
 *)
imports NikExpressions

begin

(*
 * Simplifying an expression amounts to replacing:
 *  - all constant expressions by their value (e.g. N 2 .+. N 3 by N 5)
 *  - N 0 .+. x and x .+. N 0 by x
 *  - N 0 .*. x and x .*. N 0 by N 0
 *  - N 1 .*. x and x .*. N 1 by x
 *  - N 0 .÷. x by N 0
 *  - x .÷. N 1 by x
 *)
fun simplify:: "expression ⇒ expression"
where
    (* A binary operator can be simplified if both arguments simplify to numbers *)
    "simplify (a .+. b) = (
       let (u', v') = (simplify a, simplify b) in
       if u' = (N 0) then v'
       else if v' = (N 0) then u'
       else
       case (u', v') of
           (N va, N vb) ⇒ N (va + vb)  (* arguments are numbers ⇒ compute the result *)
         | (sa, sb) ⇒ sa .+. sb        (* else return the sum of the simplified arguments *)
    )"
  | (* Other cases ... *)
  (* Other expressions (variables and constants) cannot be simplified and are left as is *)
  | "simplify expr = expr"

(* Some checks *)
value "simplify ((N 2) .*. (N 3))"
value "simplify (N 2 .*. N 1 .+. V ''x'')"
value "simplify (N 0 .*. (N 1 .+. V ''x''))"
value "simplify ((N 2 .-. N 2) .*. (N 1 .+. V ''x''))"

(* Proof that simplify does not change the semantics of expressions *)
theorem "evaluate (simplify expr) env = evaluate expr env"
(* by (induction expr, auto split:expression.split) *)
sorry

(* A predicate telling whether an expression is optimal, i.e. does not
   contain any operator applied to constants. *)
fun optimal_expr :: "expression ⇒ bool"
where
    "optimal_expr (N a) = True"
  | "optimal_expr (V x) = True"
  | (* Other cases... *)

(* Check that optimal_expr behaves as expected *)
value "optimal_expr (N 3)"
value "optimal_expr (N 3 .+. V ''x'')"
value "optimal_expr (N 3 .+. N 5)"
value "optimal_expr ((N 3 .+. V ''x'') .*. V ''y'')"
value "optimal_expr ((N 3 .+. N 2) .*. V ''y'')"

(* Prove that simplify yields optimal expressions *)
theorem "optimal_expr (simplify expr)"
sorry

end

theory NikBoolExpr
(*
 *  Niklaus boolean expressions (conditions for if and while)
 *)
imports NikExpressions

begin

(* 
 *  A boolean expression may consist in the comparison 
 *  of two arithmetic expressions or in a boolean value
 *)
datatype boolexp = 
    Equals expression expression       (infix ".=." 55)
  | Differs expression expression      (infix ".≠." 55)
  | LowerThan expression expression    (infix ".<." 55)
  | LowerEqual expression expression   (infix ".≤." 55)
  | GreaterThan expression expression  (infix ".>." 55)
  | GreaterEqual expression expression (infix ".≥." 55)
  | Boolean bool                       ("B")

(* Semantics of boolean expressions is mapped to the usual operators on integers *)
fun evalbool :: "boolexp ⇒ environment ⇒ bool"
where
    "evalbool (e1 .=. e2) env =  (evaluate e1 env = evaluate e2 env)"
 |  "evalbool (e1 .≠. e2) env =  (evaluate e1 env ≠ evaluate e2 env)"
 |  "evalbool (e1 .<. e2) env =  (evaluate e1 env < evaluate e2 env)"
 |  "evalbool (e1 .≤. e2) env =  (evaluate e1 env ≤ evaluate e2 env)"
 |  "evalbool (e1 .>. e2) env =  (evaluate e1 env > evaluate e2 env)"
 |  "evalbool (e1 .≥. e2) env =  (evaluate e1 env ≥ evaluate e2 env)"
 |  "evalbool (B b) env = b"

(* Checks on some expressions *)
value "evalbool (N 2 .+. V ''x'' .=. N 4) ((λx.0)(''x'':=5))"
value "evalbool (N 2 .+. V ''x'' .=. N 4)  ((λx.0)(''x'':=2))"
value "evalbool (B True) (λx. 0)"

end

theory NikInstructions
(*
 *  Abstract syntax of the instructions in Niklaus
 *)
imports NikExpressions NikBoolExpr

begin

(*
 * Without the Read and Write instructions, the state 
 * of the Niklaus execution machine is reduced to the
 * environment (valuation of the variables)
 *)
type_synonym state = "environment"

(*
 *  Instructions are:
 *    - Nop, does nothing, useful for if _ then _ else when a branch is empty
 *    - VarDecl v (abbreviated into "var v"), declares a variable (initial value is 0)
 *    - Seq i1 i2 (abbreviated as "i1;; i2) executes i1 and i2 in sequence
 *    - Alternative c i1 i2 ("if c then i1 else i2 fi"), executes i1 if c is true, else executes i2
 *    - While c body ("while c do body done"), executes body if c is true, then executes itself again
 *)
datatype instruction = 
    Nop
  | VarDecl varname                ("var")
  | Assign varname expression      ("_ <- _" [1000, 65] 65)
  | Seq instruction instruction    ("_ ;; _" [65, 60] 60)
  | Alternative boolexp instruction instruction
                                   ("if _ then _ else _ fi")
  | While boolexp instruction      ("while _ do _ done")

(* Check that we can write some simple instructions with this syntax *)
term "var ''x''"
term "if V ''x'' .<. N 2 then ''x'' <- N 2 else Write ''x'' fi"

end

theory NikOpNaive
imports NikInstructions

begin
(*
 *  Naïve attempt to define the semantics of the instructions
 *  using a recursive function.
 *  This function cannot be defined properly because in case
 *  of a while, it is impossible to prove the termination of
 *  the function.
 *  The proper way to do this is explained in theories 
 *  NikSmallStep and NikBigStep.
 *)
fun execute:: "instruction ⇒ state ⇒ state"
where
    "execute Nop s = s"
  | "execute (var v) s = s(v:=0)" 
  | "execute (v <- e) s = s(v:=evaluate e s)"
  | "execute (i1;; i2) s = (
       let post1 = (execute i1 s) in
       (execute i2 post1) )"
  | "execute (if c then i1 else i2 fi) s = 
       (if (evalbool c s) then (execute i1 s) else (execute i2 s))"
  | "execute (while c do body done) s = 
       (if (evalbool c s) then
          let post = (execute body s) in
            (execute (while c do body done) post)
        else s )"
(* No way to prove termination! *)
termination sorry

end

theory NikBigStep
(*
 *  Big step operative semantics of Niklaus
 *)
imports NikInstructions

begin
(*
 *  In big step semantics, we define a relation between a pair (instruction, state) 
 *  and the state reached after executing the instruction from the original state.
 *  (i, s) and s' are in relation if by executing instruction i in state s we reach
 *  state s'.
 *
 *  Defining a relation r amounts to defining a predicate that takes two arguments and returns:
 *  - True is the arguments are in relation
 *  - False is they are not
 *
 *  Here, we use an inductive definition, which tells which pairs of (instruction, state)
 *  and state are in relation. We cannot use a function (see theory NikInstructions) 
 *  because we cannot prove its termination.
 *  The infix notation (i, s) ↝ s', which states that (i, s) and s' are in relation,
 *  can be read as "executing i in state s leads to state s'".
 *)
inductive big_step :: "(instruction × state) ⇒ state ⇒ bool" (infix "↝" 55)
where
    Nop: "(Nop, s) ↝ s" 
  | VDecl: "(var v, s) ↝ s(v:=0)"
  | Assign: "(v <- e, s) ↝ s(v:=evaluate e s)"
  | Seq: "⟦(i1, s) ↝ s'; (i2, s') ↝ s''⟧
          ⟹ (i1;; i2, s) ↝ s''"
  | IfTrue: "⟦(evalbool c s); (instrTrue, s) ↝ s'⟧
         ⟹ (if c then instrTrue else instrFalse fi, s) ↝ s'"
  | IfFalse: "⟦(¬evalbool c s); (instrFalse, s) ↝ s'⟧
         ⟹ (if c then instrTrue else instrFalse fi, s) ↝ s'"
  | WhileFalse: "(¬evalbool c s) ⟹ (while c do instr done, s) ↝ s"
  | WhileTrue: "⟦(evalbool c s); (instr, s) ↝ s';
                 (while c do instr done, s') ↝ s''⟧
             ⟹ (while c do instr done, s) ↝ s''"

print_theorems

(* Somme proofs to check that this works properly *)

(* P[of t1 t2 ... tn] substitutes t1, t2, ... tn to the n first schematic variables of P *)
thm VDecl
thm VDecl[of "''x''" "s"]
thm VDecl[where v="''x''" and s="s"]

lemma "(var ''x'', s) ↝ s(''x'' := 0)"
by (rule VDecl[of "''x''" "s"])

(* The same lemma, but we let the unifier find substitutions *)
lemma "(var ''x'', s) ↝ s(''x'' := 0)"
by (rule VDecl)

(* We can even let Isabelle find the rule by itself... *)
lemma "(var ''x'', s) ↝ s(''x'' := 0)" ..

thm Assign
print_statement Assign
lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)"
(* Here, we cannot apply the Assign rule directly, because this rule expects
   a term in the form "evaluate e pre". We introduce a subgoal of the right form: *)
apply (subgoal_tac "(''x'' <- N 3, s) ↝ s(''x'' := evaluate (N 3) s)")
(* By simplification, we discharge the first goal *)
apply (simp)
(* We can now apply the Assign rule *)
apply (rule Assign)
done

(* Same lemma, with an Isar structured proof *)
lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)"
proof -
  from evaluate.simps(1)[symmetric] have "3 = evaluate (N 3) s"  .
  then show ?thesis using Assign[where v="''x''" and e="(N 3)"]  by simp
qed

(* The same lemma again, with a less detailed Isar structured proof *)
lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)"
proof -
  have "3 = evaluate (N 3) s"  by simp
  then show ?thesis using Assign[where e="(N 3)"] by simp
qed

(* Yet another proof using the metis tactic *)
lemma "(''x'' <- N 3, s) ↝ s(''x'' := 3)"
  using Assign evaluate.simps(1) by metis

(* In a schematic goal, schematic variables will be determined during the proof.
   Here, we will find the final state ?s'
 *)
schematic_goal ex1:  (* use schematic_lemma in versions of Isabelle previous to 2016 *)
  "(''x'' <- N 3 ;; ''y'' <- V ''x'', s) ↝ ?s'"
(* Applying the Seq rule goes backward to the premisses of the lemma *)
apply (rule Seq)
(* The Assign rule discharges the first premisse *)
apply (rule Assign)
(* simp simplifies evaluate (N 3) s *)
apply (simp)
(* The Assign rule discharges the second premisse *)
apply (rule Assign)
done
(* ?s' was determined during this proof, we can get its value in the simplified form of the lemma *)
thm ex1
thm ex1[simplified]

(* Computing the GCD of 2 and 3 by successive subtractions *)
schematic_goal gcd2_3:
"   (''a''<- N 2;; ''b''<- N 3;;
    while V ''a'' .≠. V ''b'' do
      if V ''a'' .<. V ''b'' then
        ''b''<- V ''b'' .-.V ''a''
      else
        ''a''<- V ''a'' .-. V ''b''
      fi
    done,
    λx.0) ↝ ?s
"
apply(rule Seq)
apply(rule Assign)
apply simp
apply(rule Seq)
apply(rule Assign)
apply simp
apply(rule WhileTrue)
apply simp
apply(rule IfTrue)
apply simp
apply(rule Assign)
apply simp
apply(rule WhileTrue)
apply simp
apply(rule IfFalse)
apply simp
apply(rule Assign)
apply simp
apply(rule WhileFalse)
apply simp
done
thm gcd2_3

(* To avoid to much copy-pasting, we define an abbreviation *)
abbreviation "GCD_2_3 ≡ 
''a'' <- N 2 ;; ''b'' <- N 3 ;;
    while V ''a'' .≠. V ''b'' do
      if V ''a'' .<. V ''b'' then
        ''b'' <- V ''b'' .-. V ''a''
      else
        ''a'' <- V ''a'' .-. V ''b''
      fi
    done
"

(* Generate code for predicate big_step *)
code_pred big_step .

(* Compute the result of a program using this generated code *)
values "{res. (GCD_2_3, λx.0) ↝ res }"

(* Use map to display the value of a and b in the environment of the result *)
values "{map res [''a'', ''b'']|res. (GCD_2_3, λx.0) ↝ res }"

(* Equivalence of instructions *)
abbreviation equiv_instr :: "instruction ⇒ instruction ⇒ bool"
where "equiv_instr i1 i2 ≡ (∀ pre post. (i1, pre) ↝ post = (i2, pre) ↝ post)"

(* Proof automation *)
thm big_step.intros
declare big_step.intros [intro]
thm big_step.induct (* Standard induction rule *)
(* Allow splitting of arguments in lemmas *)
lemmas big_step_induct = big_step.induct[split_format(complete)]

(* Rule inversion *)
inductive_cases NopElim[elim!]: "(Nop, s) ↝ s'"
thm NopElim
inductive_cases VDeclElim[elim!]: "(var x, s) ↝ s'"
thm VDeclElim
inductive_cases AssignElim[elim!]: "(x <- e, s) ↝ s'"
thm AssignElim
inductive_cases SeqElim[elim!]: "(i1;; i2, s) ↝ s'"
thm SeqElim
inductive_cases AltElim[elim!]: "(if c then i1 else i2 fi, s) ↝ s'"
thm AltElim
inductive_cases WhileElim[elim]: "(while c do body done, s) ↝ s'"
thm WhileElim


lemma "(if c then Nop else Nop, pre) ↝ post ⟹ pre = post"
by auto

lemma "equiv_instr (if c then i else i fi) i"
by auto

lemma unfold_while: "equiv_instr (while cond do body done)
                   (if cond then body;; while cond do body done else Nop fi)"
by auto

(* Prove that the big step semantics is deterministic *)
lemma Nik_deterministic: "⟦ (prog, s) ↝ s';
                            (prog, s) ↝ s''⟧
                         ⟹ s'' = s'"
by (induction arbitrary: s'' rule: big_step_induct, blast+)

(* More detailed proof: we give some hints about why it is true in the different cases *)
lemma Nik_deterministic2: "⟦ (prog, s) ↝ s';
                             (prog, s) ↝ s''
                           ⟧ ⟹ s'' = s'"
proof (induction arbitrary: s'' rule: big_step.induct[split_format(complete)])
  print_cases
  case Nop thus ?case by (rule NopElim)
next
  case VDecl thus ?case by (rule VDeclElim)
next
  case Assign thus ?case by (rule AssignElim)
next
  case Seq  print_facts
  thm SeqElim Seq.prems SeqElim[OF Seq.prems] Seq.IH(1) SeqElim[OF Seq.prems, OF Seq.IH(1)]
  thm SeqElim Seq.prems SeqElim[OF Seq.prems] Seq.IH(2) SeqElim[OF Seq.prems, OF Seq.IH(2)]
  from SeqElim[OF Seq.prems, OF Seq.IH(1)]
   and SeqElim[OF Seq.prems, OF Seq.IH(2)] show ?case by simp
next
  case IfTrue print_facts
  from AltElim[OF IfTrue.prems, OF IfTrue.IH] show ?case by (simp add: IfTrue(1))
next
  case IfFalse print_facts
  from AltElim[OF IfFalse.prems, OF IfFalse.IH] show ?case by (simp add: IfFalse(1,3,4))
next
  case WhileFalse print_facts
  show ?case using WhileFalse.hyps WhileFalse.prems by auto
next
  case WhileTrue print_facts
  show ?case using WhileTrue.IH WhileTrue.hyps(1) WhileTrue.prems by auto
qed

(* Very detailed proof, almost like on the blackboard. *)
lemma Nik_deterministic3: "⟦ (prog, s) ↝ s';
                             (prog, s) ↝ s''
                           ⟧ ⟹ s'' = s'"
proof (induction arbitrary: s'' rule: big_step.induct[split_format(complete)])
  print_cases
  case (Nop pre)
  from `(Nop, pre) ↝ s''` show "s'' = pre" by (rule NopElim)
next
  case (VDecl v pre)
  from `(var v, pre) ↝ s''` show "s'' = pre(v := 0)" by (rule VDeclElim)
next
  case (Assign v e pre)
  from `(v <- e, pre) ↝ s''` show "s'' = pre(v := evaluate e pre)" by (rule AssignElim)
next
  case (Seq i1 pre p' i2 post)
  from `(i1 ;; i2, pre) ↝ s''` have "∃q. (i1, pre) ↝ q ∧ (i2, q) ↝ s''" by blast
  then obtain q where q1:"(i1, pre) ↝ q" and q2:"(i2, q) ↝ s''" by blast
  from q1 and Seq.IH(1) have "q = p'" by simp
  with q2 and Seq.IH(2) show "s'' = post" by simp
next
  case (IfTrue c pre i1 post i2) print_facts
  from `(if c then i1 else i2 fi, pre) ↝ s''` and `evalbool c pre` have "(i1, pre) ↝ s''" by blast
  with IfTrue.IH show "s'' = post" .
next
  case (IfFalse c pre i2 post i1)
  from `(if c then i1 else i2 fi, pre) ↝ s''` and `¬ evalbool c pre` have "(i2, pre) ↝ s''" by blast
  with IfFalse.IH show "s'' = post" .
next
  case (WhileFalse c pre body) print_facts
  from `(while c do body done, pre) ↝ s''` and `¬ evalbool c pre` show "s'' = pre" by blast
next
  case (WhileTrue c pre body p' post) print_facts
  from `(while c do body done, pre) ↝ s''` and `evalbool c pre`
    have "∃q. (body, pre) ↝ q ∧ (while c do body done, q) ↝ s''" by blast
  then obtain q where q1:"(body, pre) ↝ q" and q2:"(while c do body done, q) ↝ s''" by blast
  from q1 and WhileTrue.IH(1) have "q = p'" by simp
  with q2 and WhileTrue.IH(2) show "s'' = post" by simp
qed

end

theory NikDenNaive

imports NikInstructions

begin

(* 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⟧ = {(s, s'). s' = s(v:=evaluate val s)}"
| Seq_den:    "⟦i1;; i2⟧ = ⟦i1⟧ O ⟦i2⟧"
(*
  O is the composition of relations (like o is the composition of functions):
  ⟦ (a, b) ∈ r ; (b, c) ∈ s ⟧ ⟹ (a, c) ∈ r O s
*)
| 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⟧ = 
               {(s, s').
                if evalbool c s then
                  (s, s') ∈ ⟦body ;; while c do body done⟧
                else
                  s = s'
               }
              "
(* Same issue as with the naive operational semantics : no proof of termination. *)
end

theory recursion
imports Main
begin

fun f :: "nat => nat"
where
   "f 0 = 1"
 | "f (Suc n) = (Suc n) * f n"


definition Fact :: "(nat => nat) => (nat => nat)"
where
   "Fact u ≡ (λn. (case n of
                     0 ⇒ 1
                   | Suc p ⇒ n * (u p)
                  )
             )"

value "int (f 5)"

value "Fact (λ x.(x))"
value "int ((Fact (λ x.(x))) 0)"
value "int ((Fact (Fact (λ x.(x)))) 1)"
value "int (((Fact^^2) (λ x.(x))) 1)"
value "int (((Fact^^3) (λ x.(x))) 2)"
value "int (((Fact^^4) (λ x.(x))) 3)"
value "int (((Fact^^5) (λ x.(x))) 4)"
value "int (((Fact^^6) (λ x.(x))) 5)"

(* n! is a fixed point of Fac, it is the limit of Fac^^i *)

function h :: "nat => nat"
where
   "h 0 = 1"
 | "h 1 = 1"
 | "h (n+n) = h n"
 | "h n = h (n+n+n+1)"
apply(auto)
sorry

value "h 0"
value "h 2"
value "h (1+1)"

definition Syr :: "(nat => nat) => (nat => nat)"
where
  "Syr u ≡ (λn. (if n = 0 then 1 
                 else if n = 1 then 1
                 else if (n mod 2) = 0 then u (n div 2)
                 else u (Suc (3*n))
                )
           )"

value "int (Syr (λx. 0) 0)"
value "int (Syr (λx. 0) 1)"
value "int ((Syr^^2) (λx. 0) 2)" (* 1 recursive call 2 → 1 *)
value "int ((Syr^^8) (λx. 0) 3)" (* 7 recursive calls 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1 *)
value "int ((Syr^^3) (λx. 0) 4)" (* 2 recursive calls 4 → 2 → 1 *)
value "int ((Syr^^6) (λx. 0) 5)" (* 5 recursive calls 5 → 16 → 8 → 4 → 2 → 1 *)
value "int ((Syr^^9) (λx. 0) 6)" (* 8 recursive calls 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1 *)

(* is λn. 1 a fixed point of Syr? *)

end

theory fac

imports Main
(*
 *  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}.
 *)
begin
(*
 * 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!
 *)
definition Fac:: "int rel ⇒  int rel"
where
  "Fac f = {(0,1)} ∪ image (λ(n,fac_n). (n+1, (n+1) * fac_n)) f"

(* Applying Fac ten times to the empty set yields a partial function
   which gives the factorial of 0 .. 9 *)
value "(Fac ^^ 10){}"

(* Definition of the factorial as the least fixed point of Fac *)
definition fac:: "int rel"
where
  "fac = lfp Fac"

(* In order to use this definition, we have to prove that Fac 
   is monotone, i.e. that it always adds information *)
lemma "mono Fac"
apply (unfold mono_def)
apply (unfold Fac_def)
apply auto
done

(* More structured proof *)
lemma mono_Fac: "mono Fac"
proof (unfold mono_def, intro allI impI)
  fix x::"int rel" and y::"int rel"
  assume inc: "x ⊆ y"
  thus "Fac x ⊆ Fac y" unfolding Fac_def by auto
qed

thm funpow_simps_right
(* 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)))){}"
apply (simp add: funpow_simps_right(2))
apply (unfold Fac_def)
apply simp
done
(* by(simp add: funpow_simps_right(2),auto simp: Fac_def) *)

(* Show that any iteration of Fac on the empty set is an approximation of fac *)
lemma fac_approx : "(Fac ^^ (n::nat)){} ⊆ fac"
apply (unfold fac_def)
proof (induction n) print_cases
  case 0 show ?case by simp
next 
  case (Suc n) show ?case
     apply simp
thm lfp_unfold
thm lfp_unfold[OF mono_Fac]
     apply (subst lfp_unfold[OF mono_Fac])
thm monoD
     apply (rule  Orderings.order_class.monoD[OF mono_Fac])
     apply (rule Suc.IH)
     done
qed

lemma "(Fac ^^ (n::nat)){} ⊆ fac"
proof (induction n) print_cases
  case 0 show ?case by simp
next 
  case (Suc n)
    have "(Fac ^^ (Suc n)) {} = Fac ((Fac ^^ n) {})" by simp
    also from Suc.IH have "... ⊆ Fac fac" using monoD[OF mono_Fac] by simp
    also have "... = fac" unfolding fac_def using lfp_unfold[OF mono_Fac] by simp
    finally show ?case .
qed

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

(* Show that 6 is 3! *)
lemma fac_3 : "(3, 6) ∈ fac"
apply (rule Set.subsetD[OF fac_approx, of _ "Suc(Suc(Suc(Suc 0)))"])
apply (simp add: funpow_simps_right(2))
apply (unfold Fac_def)
apply simp
done

end

theory NikDenotational

imports NikInstructions

begin
(* The denotation of an instruction is a relation between states. *)
type_synonym instr_den = "state rel"

(*
  A functor to define the semantics of while as a least fixed point.
  This functor takes the condition and the denotation of the body of the while loop
  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 have 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
                              })"

(* Existence of the fixed point: proving that while_func 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

(* 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⟧)"

lemma "⟦''x''<-N 2⟧ = {(s, s'). s'=s(''x'':=2)}"
by simp

(* Consider an infinite loop over a Nop *)
abbreviation inf_nop where "inf_nop ≡ (while B True do Nop done)"

(* 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 *)
proof -
  have "while_func (evalbool (B True)) ⟦Nop⟧ = while_func (λs. True) Id"
    unfolding while_func_def using Nop_den evalbool.simps(7)[of "True"] by simp
  also have "... = (λw. w)" unfolding while_func_def by simp
  finally show ?thesis .
qed

(*
  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 *)
proof -
  from nik_den.simps(6) have
    "⟦inf_nop⟧ = lfp (while_func (evalbool (B True)) ⟦Nop⟧)" by simp
  also from w_true_nop_id have "... = lfp (λw .w)" by simp
  also from empty_lfp have "... = {}" .
  finally show ?thesis .
qed

(* Consider a no-loop over a Nop *)
abbreviation nop_loop where "nop_loop ≡ (while B False do Nop done)"

(* 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

(* Show that this loop does nothing *)
lemma w_nop_loop_ok: "while_func (evalbool (B False)) ⟦Nop⟧ = (λw. {(pre, post). post=pre})"
proof -
  from w_nop_loop have "while_func (evalbool (B False)) ⟦Nop⟧ = while_func (λs. False) Id" .
  also have "... = (λw. {(pre, post). post=pre})"
    unfolding while_func_def by simp
  finally show ?thesis .
qed


lemma "⟦while B False do Nop done⟧ = ⟦Nop⟧"
(* unfolding nik_den.simps(6) lfp_def using w_nop_loop_ok by auto *)
apply (insert nik_den.simps(6))
apply simp
apply (insert w_nop_loop_ok)
apply simp
apply (unfold lfp_def)
apply auto
done

end

theory NikDenBig

imports NikDenotational NikBigStep

begin

(* 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

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

(* Make big step semantics a relation *)
abbreviation big_step_rel:: "instruction ⇒ instr_den"
where "big_step_rel instr ≡ {(pre, post). (instr, pre) ↝ post}"


lemma den_in_big_step: "(pre, post) ∈ ⟦ instr ⟧ ⟹ (pre, post) ∈ big_step_rel instr"
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
    hence "(pre, post) ∈ big_step_rel (var v)" by auto
    thus ?thesis .
  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
    hence "(pre, post) ∈ big_step_rel (v <- val)" by auto
    thus ?thesis .
  qed
next
  case (Alternative cond iT iF) thus ?case
  apply (unfold nik_den.simps(5))
  apply simp
  apply(case_tac "evalbool cond pre")
  apply auto
  done
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
    hence "(pre, p) ∈ big_step_rel i1" 
    and "(p, post) ∈ big_step_rel i2"
    using Seq.IH by auto
    hence "(pre, post) ∈ big_step_rel (i1;; i2)" by auto
    thus ?thesis .
  qed
next
  case (While cond body) print_facts
    let ?bigw = "big_step_rel (while cond do body done)"
    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

theorem den_is_big_step: "((instr, pre) ↝ post) = ((pre, post) ∈ ⟦ instr ⟧)"
(* by (auto simp add: big_step_in_den den_in_big_step[simplified]) *)
proof -
  have "(pre, post) ∈ big_step_rel instr ⟹ (instr, pre) ↝ post" by simp
  moreover from den_in_big_step have "(pre, post) ∈ ⟦ instr ⟧ ⟹ (pre, post) ∈ big_step_rel instr " .
  ultimately have 1: "(pre, post) ∈ ⟦ instr ⟧ ⟹ (instr, pre) ↝ post" .
  from big_step_in_den have 2: "(instr, pre) ↝ post ⟹ (pre, post) ∈ ⟦ instr ⟧" .
  from 1 and 2 show ?thesis by auto
qed

end

theory NikAxiomatic

imports NikBigStep

begin

(* Type for an assertion on a state of the execution machine *)
type_synonym assertion = "state ⇒ bool"

(* Definition of a valid Hoare pre/post assertion *)
definition hoare_valid:: "assertion ⇒ instruction ⇒ assertion ⇒ bool" ("⊨ {_} _ {_}" 50)
where
  "⊨ {P} c {Q} = (∀s t. P s ∧ (c, s) ↝ t ⟶ Q t)"

(* Substitution of an expression to a variable in a state *)
abbreviation state_subst:: "expression ⇒ varname ⇒ state ⇒ state"
where "state_subst e v s ≡ s(v:= evaluate e s)"

(* Substitution of an expression to a variable in an assertion *)
abbreviation assert_subst:: "assertion ⇒ expression ⇒ varname ⇒ assertion" ("_[with _ for _]" [1000,0,0] 999)
where
  "P[with e for x] ≡ P ∘ (state_subst e x)"

(* Semantic rules for the Hoare semantics of Niklaus *)
inductive hoare_sem:: "assertion ⇒ instruction ⇒ assertion ⇒ bool" ("⊢ {_} _ {_}" 50)
where
  Nop:   "⊢ {P} Nop {P}"
| VDecl: "⊢ {P[with (N 0) for v]} var v {P}"
| Assign:"⊢ {P[with u for v]} v <- u {P}"
| Seq:   "⟦ ⊢ {P} i1 {Q} ; ⊢ {Q} i2 {R} ⟧ ⟹ ⊢ {P} i1;; i2 {R}"
| If:    "⟦ ⊢ {λs. P s ∧ (evalbool c s)} iT {Q}; ⊢ {λs. P s ∧ ¬ (evalbool c s)} iF {Q} ⟧
          ⟹ ⊢ {P} if c then iT else iF fi {Q}"
| While: "⊢ {λs. P s ∧ evalbool c s} body {P} 
          ⟹ ⊢ {P} while c do body done {λs. P s ∧ ¬(evalbool c s)}"
| Conseq:"⟦∀s. P' s ⟶ P s; ⊢ {P} instr {Q}; ∀s. Q s ⟶ Q' s⟧ ⟹ ⊢ {P'} instr {Q'}"

(* For proof automation, add these rules to simp and intro rules *)
lemmas[simp, intro!] = Nop VDecl Assign Seq If

(* Generate elimination rules *)
inductive_cases NopAxElim[elim!]:"⊢ {P} Nop {P}"
inductive_cases VDeclAxElim[elim!]:"⊢ {P[with (N 0) for v]} var v {P}"
inductive_cases AssignAxElim[elim!]:"⊢ {P[with u for v]} v <- u {P}"
inductive_cases SeqAxElim[elim!]:"⊢ {P} i1;; i2 {R}"
inductive_cases IfAxElim[elim!]:"⊢ {P} if c then iT else iF fi {Q}"
inductive_cases WhileAxElim[elim]:"⊢ {P} while c do body done {λs. P s ∧ ¬(evalbool c s)}"
inductive_cases ConseqAxElim[elim]:"⊢ {P'} instr {Q'}"

(* The following two lemmas are easier to use than Conseq *)
(* We can always use a stronger precondition *)
lemma strengthen_pre:
  "⟦ ∀s. P' s ⟶ P s;  ⊢ {P} instr {Q} ⟧ ⟹ ⊢ {P'} instr {Q}"
by (rule Conseq, auto)

(* We can always get a weaker postcondition *)
lemma weaken_post:
  "⟦ ⊢ {P} instr {Q};  ∀s. Q s ⟶ Q' s ⟧ ⟹  ⊢ {P} instr {Q'}"
by (rule Conseq, auto)

(* Small example *)
lemma "⊢ {λs. True} ''x'' <- N 2 {λs. s ''x'' = 2}"
apply (rule strengthen_pre[of "λs. True" "(λs. (s ''x'' = 2))[with N 2 for ''x'']"])
apply simp
apply (rule Assign)
done

thm Assign
thm strengthen_pre
thm strengthen_pre[OF _ Assign]
(* Easier to use assignment rule *)
lemma Assign': "∀s. P s ⟶ (Q[with u for v]) s ⟹ ⊢ {P} v <- u {Q}"
apply (rule strengthen_pre[OF _ Assign])
apply (simp)
done

(* Same example with the new Assignment rule *)
lemma "⊢ {λs. True} ''x'' <- N 2 {λs. s ''x'' = 2}"
apply (rule Assign')
apply simp
done

(* Same thing for the While rule *)
lemma While':
assumes "⊢ {λs. P s ∧ evalbool c s} body {P}" and "∀s. P s ∧ ¬ evalbool c s ⟶ Q s"
shows "⊢ {P} while c do body done {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])

thm weaken_post
thm While
end

theory NikPGCD

imports NikAxiomatic PGCD

begin
(* Proof that Euclid's algorithm programmed in Niklaus computes the GCD of two integers *)

(* First, the if_then_else in the loop *)
abbreviation if_x_y:: "instruction"
where "if_x_y ≡ 
      if V ''x'' .<. V ''y'' then
        ''y'' <- V ''y'' .-. V ''x''
      else
        ''x'' <- V ''x'' .-. V ''y''
      fi"

(* Prove that this if_then_else preserves gcd *)
lemma gcd_if:
  "⊢ {λs. is_gcd (s ''x'') (s ''y'') k}
      if_x_y
     {λs. is_gcd (s ''x'') (s ''y'') k}"
apply (rule If)
apply (rule Assign')
apply simp
apply (insert is_gcd_b_a)
apply simp

apply (rule Assign')
apply simp
apply (insert is_gcd_a_b)
apply simp
done

(* The while loop *)
abbreviation while_x_y:: "instruction"
where "while_x_y ≡ while V ''x'' .≠. V ''y'' do if_x_y done"

(* Prove that this loop preserves gcd *)
lemma gcd_while:
  "⊢ {λs. is_gcd (s ''x'') (s ''y'') k}
       while_x_y
     {λs. is_gcd (s ''x'') (s ''y'') k ∧ (s ''x'') = (s ''y'')}"
apply (rule While')
apply simp
apply (rule strengthen_pre[OF _ gcd_if])
apply simp
apply simp
apply auto
done

(* Useful lemma for concluding *)
lemma final_gcd: "is_gcd x y k ∧ x = y ⟹ is_gcd x y x"
by (insert is_gcd_a_a_a, auto)

(* Prove that at the end of the loop, x is the gcd of x and y *)
lemma gcd_while2:
  "⊢ {λs. is_gcd (s ''x'') (s ''y'') k}
       while_x_y
     {λs. is_gcd (s ''x'') (s ''y'') (s ''x'')}"
apply (rule weaken_post[OF gcd_while])
apply (insert final_gcd)
apply auto
done

end

theory PGCD

imports Main

begin

definition divides:: "int ⇒ int ⇒ bool"
where "divides a b = (∃k::int. b = k * a)"

definition common_div :: "int => int => int => bool"
where "common_div a b k ≡ divides k a ∧ divides k b"

definition is_gcd :: "int => int => int => bool" 
where "is_gcd a b g ≡ common_div a b g 
                      ∧ (∀p::int. common_div a b p ⟶ divides p g)"

theorem is_gcd_a_a_a: "is_gcd a a a"
by (simp add: common_div_def divides_def is_gcd_def)

(* More detailed proof *)
theorem "is_gcd a a a"
proof -
  from divides_def have "divides a a" by simp
  hence 1:"common_div a a a" using common_div_def by simp
  {fix p assume "common_div a a p"
   hence "divides p a" using common_div_def by simp
  }
  with 1 show ?thesis using is_gcd_def by simp
qed

theorem common_div_a_b:
  "common_div a b k ⟶ common_div (a-b) b k"
by (metis common_div_def divides_def int_distrib(3))

(* More detailed proof *)
theorem "common_div a b k ⟶ common_div (a-b) b k"
proof
  assume "common_div a b k"
  hence 1: "divides k a ∧ divides k b" using common_div_def by simp
  hence "(∃pa::int. a = pa*k) ∧ (∃pb::int. b = pb*k)" using divides_def by simp
  then obtain pa pb where "a = pa*k" and "b = pb*k" by auto
  hence "(a-b) = (pa-pb) * k" by (simp add: int_distrib)
  hence "divides k (a-b)" using divides_def by simp
  thus "common_div (a-b) b k" using 1 and common_div_def by simp
qed

theorem common_div_commutes:
  "common_div a b k = common_div b a k"
using common_div_def by auto

(* Other proof *)
theorem "common_div a b k = common_div b a k"
proof
  assume "common_div a b k"
  from this and common_div_def show "common_div b a k" by simp
next
  assume "common_div b a k"
  from this and common_div_def show "common_div a b k" by simp
qed

theorem is_gcd_commutes:
  "is_gcd a b k = is_gcd b a k"
by (simp add: common_div_commutes is_gcd_def)

(* Other proof *)
theorem "is_gcd a b k = is_gcd b a k"
proof
  assume "is_gcd a b k"
  then show "is_gcd b a k" using is_gcd_def and common_div_commutes by simp
next
  assume "is_gcd b a k"
  then show "is_gcd a b k" using is_gcd_def and common_div_commutes by simp
qed

theorem is_gcd_a_b:
  "is_gcd a b k ⟶ is_gcd (a-b) b k"
proof
  assume h: "is_gcd a b k"
  hence "common_div a b k" using is_gcd_def by simp
  hence 1: "common_div (a-b) b k" using common_div_a_b by simp
  (* Show that any other common divisor of (a-b) and b divides k *)
  { fix p
	  assume h': "common_div (a-b) b p"
	  hence "(∃pab::int. (a-b) = pab * p) ∧ (∃pb::int. b = pb * p)" using common_div_def and divides_def by simp
	  then obtain pab pb where "(a-b) = pab * p" and "b = pb * p" by auto
	  hence "(a-b) + b = pab * p + pb * p" by simp
	  hence "a = pab * p + pb * p" by simp
	  hence "a = (pab+pb) * p" using int_distrib by simp
	  hence "divides p a" using divides_def by simp
	  hence "common_div a b p" using h' and common_div_def by simp
	  hence "divides p k" using h and is_gcd_def by simp
  }
  hence "∀p::int. common_div (a-b) b p ⟶ divides p k" by simp
  thus "is_gcd (a-b) b k" using 1 and is_gcd_def by simp
qed

theorem is_gcd_b_a:
  "is_gcd a b k ⟶ is_gcd a (b-a) k"
using is_gcd_a_b is_gcd_commutes by auto

(* More detailed proof *)
theorem "is_gcd a b k ⟶ is_gcd a (b-a) k"
proof
  assume "is_gcd a b k"
  hence "is_gcd b a k" using is_gcd_commutes by simp
  hence "is_gcd (b-a) a k" using is_gcd_a_b by simp
  thus "is_gcd a (b-a) k" using is_gcd_commutes by simp
qed

end

theory NikAxSoundComplete

imports NikAxiomatic

begin

(*
  We gave the rules to derive Hoare triplets: ⊢ {P} instr {Q}.
  Is this definition sound and complete?
    - soundness: if a Hoare triplet is derivable, it is valid?
    - completeness: if a Hoare triplet is valid, is it derivable?
*)

(* Soundness : if a Hoare triplet is derivable, it is valid *)
theorem axiomatic_sound:"⊢ {P} instr {Q} ⟹ ⊨ {P} instr {Q}"
proof(induction rule: hoare_sem.induct)
  case (While P cond body) (* this is the only difficult case *)
  { 
    fix s t
    have "(while cond do body done, s) ↝ t  ⟹  P s  ⟹  P t ∧ ¬ evalbool cond t"
    proof (induction "while cond do body done" s t rule: big_step_induct)
      case WhileFalse thus ?case by blast
    next
      case WhileTrue thus ?case
        using While.IH unfolding hoare_valid_def by blast
    qed
  }
  thus ?case unfolding hoare_valid_def by blast
qed (unfold hoare_valid_def, auto) (* the other cases are solved by auto *)

(*
  Completeness : every valid Hoare triplet is derivable
  For this, we need to introduce the notion of weakest precondition.
  For a given instruction and postcondition, this is the precondition
  which makes the postcondition hold on any state that can be reached
  by executing the instruction.
*)
(* Weakest precondition for validating postcondition Q after executing instruction instr *)
definition weakestpre :: "instruction ⇒ assertion ⇒ assertion"
where "weakestpre instr Q = (λs. ∀t. (instr,s) ↝ t  ⟶  Q t)"

(* Find the weakest precondition for each instruction *)
lemma wp_Nop[simp]: "weakestpre Nop Q = Q"
unfolding weakestpre_def by auto

lemma wp_Decl[simp]: "weakestpre (var x) Q = Q[with (N 0) for x]"
unfolding weakestpre_def
apply (rule ext) (* two functions are equal if they take the same value for all inputs *)
apply (auto)
done

lemma wp_Assign[simp]: "weakestpre (x <- a) Q = Q[with a for x]"
unfolding weakestpre_def
apply (rule ext)
apply (auto)
done

lemma wp_Seq[simp]: "weakestpre (c⇩1;;c⇩2) Q = weakestpre c⇩1 (weakestpre c⇩2 Q)"
unfolding weakestpre_def
by auto

lemma wp_If[simp]:
 "weakestpre (if cond then iT else iF fi) Q =
 (λs. if evalbool cond s then weakestpre iT Q s else weakestpre iF Q s)"
unfolding weakestpre_def
by auto

(* Show that the wekeast precondition does not change when unfolding a while loop *)
lemma wp_While_unfold:
 "weakestpre (while cond do body done) Q s =
  weakestpre (if cond then body ;; while cond do body done else Nop fi) Q s"
unfolding weakestpre_def
using unfold_while by auto

lemma wp_While_True[simp]: "evalbool cond s ⟹
  weakestpre (while cond do body done) Q s = weakestpre (body;; while cond do body done) Q s"
by(simp add: wp_While_unfold)

lemma wp_While_False[simp]: "¬ evalbool cond s ⟹ weakestpre (while cond do body done) Q s = Q s"
by(simp add: wp_While_unfold)

(* Show that the weakest precondition is a valid precondition *)
lemma weakestpre_is_pre: "⊢ {weakestpre instr Q} instr {Q}"
proof (induction instr arbitrary: Q)print_cases
  case VarDecl thus ?case using hoare_sem.VDecl wp_Decl by presburger
next
  case Alternative thus ?case by (auto intro: Conseq)
next
  case (While cond body)
  let ?w = "while cond do body done"
  show "⊢ {weakestpre ?w Q} ?w {Q}"
  proof(rule While')
    show "⊢ {λs. weakestpre ?w Q s ∧ evalbool cond s} body {weakestpre ?w Q}"
    proof(rule strengthen_pre[OF _ While.IH])
      show "∀s. weakestpre ?w Q s ∧ evalbool cond s ⟶ weakestpre body (weakestpre ?w Q) s" by auto
    qed
    show "∀s. weakestpre ?w Q s ∧ ¬ evalbool cond s ⟶ Q s" by auto
  qed
qed auto

(* We can now show that the axiomatic semantics of Niklaus is complete with regard 
   to the validity of Hoare triplets (defined in terms of big step semantics) *)
theorem axiomatic_complete:
  assumes "⊨ {P} instr {Q}"
  shows   "⊢ {P} instr {Q}"
proof (rule strengthen_pre)
  show "∀s. P s ⟶ weakestpre instr Q s" using assms
    by (simp add: hoare_valid_def weakestpre_def)
  show "⊢ {weakestpre instr Q} instr {Q}" by (rule weakestpre_is_pre)
qed

(* So the axiomatic semantics is sound and complete *)
corollary axiomatic_sound_complete: "⊢ {P} instr {Q} ⟷ ⊨ {P} instr {Q}"
using axiomatic_sound and axiomatic_complete by auto

end