header "Exam COMP4161 S2/2008"

theory Solution
  (* HoareAbort.thy is available from
     http://www.cse.unsw.edu.au/~cs4161/HoareAbort.thy *)
  imports HoareAbort
begin

(* refer to the questions in http://www.cse.unsw.edu.au/~cs4161/exam.pdf *)

section "Question 1: Lambda Calculus"
-- ----------------------------------

text {*
  You can provide the answers in this text comment:

(a): (15 = 9 + 6) marks
  i: the \<beta>\<eta> normal form is x:
  (\<lambda>z x y. z x y) (\<lambda>x y. x) x (f x) \<rightarrow> 
  (\<lambda>x y. (\<lambda>x y. x) x y) x (f x) \<rightarrow>
  (\<lambda>y. (\<lambda>x y. x) x y) (f x) \<rightarrow>
  (\<lambda>x y. x) x (f x) \<rightarrow>
  (\<lambda>y. x) (f x) \<rightarrow>
  x

  ii: the \<beta>\<eta> normal form is \<lambda>x. x:
  (\<lambda>x f. f (x x f)) (\<lambda>x f. f (x x f)) (\<lambda>f x. x) \<rightarrow>
  (\<lambda>f. f ((\<lambda>x f. f (x x f)) (\<lambda>x f. f (x x f)) f)) (\<lambda>f x. x) \<rightarrow>
  (\<lambda>f x. x) ((\<lambda>x f. f (x x f)) (\<lambda>x f. f (x x f)) f) \<rightarrow>
  \<lambda>x. x

(b): (10 = 7 + 3 marks)
  i: ( (\<lambda>z x y. z x y) (\<lambda>x y. x) x (f x) )
  there exists a type, it is 'a (the type of x), same as the \<beta> reduct

  ii: ( (\<lambda>x f. f (x x f)) (\<lambda>x f. f (x x f)) (\<lambda>f x. x) )
  there exists no type, but the \<beta> reduct has type 'a \<Rightarrow> a'
*}


section "Question 2: Balanced Parentheses"
-- ---------------------------------------


subsection "(a)" (* 5 marks *)

datatype paren = L | R

inductive_set 
  S :: "paren list set"
where
  (* replace appropriately: *)
  empty: "[] \<in> S" |
  LR: "xs \<in> S \<Longrightarrow> L # xs @ [R] \<in> S" |
  app: "\<lbrakk> xs \<in> S; ys \<in> S \<rbrakk> \<Longrightarrow> xs @ ys \<in> S"

-- "test cases, replace appropriately, add 2 more"

lemma LR_S [intro!, simp]: "[L,R] \<in> S"
  apply (insert empty)
  apply (drule LR)
  apply simp
  done

lemma "[L,R,L,R] \<in> S"
  apply (insert empty)
  apply (drule LR)
  apply (drule app)
  apply (insert empty)
  apply (erule LR)
  apply simp
  done

subsection "(b)" (* 6 marks *)

fun is_bal :: "paren list \<Rightarrow> nat \<Rightarrow> bool"
where
  "is_bal [] n = (n = 0)" |
  "is_bal (L#xs) n = is_bal xs (Suc n)" |
  "is_bal (R#xs) 0 = False" |
  "is_bal (R#xs) (Suc n) = is_bal xs n"

-- "test cases, add 3 more, at least two negative"

lemma "is_bal [L,R,R] 1" by simp

lemma "is_bal [L,R,L,R] 0" by simp

lemma "\<not>is_bal [L,L,R] 0" by simp

lemma "\<not>is_bal [L,R,R] 2" by (simp add: nat_number)

subsection "(c)" (* 6 marks *)

lemma is_bal_app_Suc [rule_format, simp]:
  "is_bal xs n \<longrightarrow> is_bal (xs @ [R]) (Suc n)"
  by (induct xs n rule: is_bal.induct) auto

lemma is_bal_app_n [rule_format, simp]:
  "is_bal xs n \<longrightarrow> is_bal ys 0 \<longrightarrow> is_bal (xs @ ys) n"
  by (induct xs n rule: is_bal.induct) auto

lemma set_is_bal:
  "xs \<in> S \<Longrightarrow> is_bal xs 0"
  by (erule S.induct) auto

subsection "(d)" (* 8 marks *) 

lemma replicate_append_cons [simp]:
  "replicate n x @ x # xs = x # replicate n x @ xs"
  by (induct n) auto

lemma S_append [rule_format]:
  "zs \<in> S \<Longrightarrow> (\<forall>xs ys. zs = ys @ xs \<longrightarrow> ys @ L # R # xs \<in> S)"
  apply (erule S.induct)
    apply clarsimp
   apply clarsimp  
   apply (case_tac ys)
    apply clarsimp
    apply (subgoal_tac "[L,R] @ L # xs @ [R] \<in> S")
     apply simp
    apply (rule app)
     apply (rule LR_S)
    apply (erule LR)
   apply clarsimp
   apply (clarsimp simp: append_eq_append_conv2) 
   apply (erule disjE)
    apply clarsimp
    apply (erule allE, erule allE, erule impE, rule refl)
    apply (drule_tac xs=" list @ L # R # us" in LR)
    apply simp
   apply clarsimp
   apply (case_tac us)
    apply clarsimp
    apply (drule app)
     apply (rule LR_S)
    apply (drule LR)
    apply simp
   apply clarsimp
   apply (drule LR)
   apply (drule app)
    apply (rule LR_S)
   apply simp
  apply clarsimp
  apply (clarsimp simp: append_eq_append_conv2)
  apply (erule disjE)
   apply clarsimp
   apply (subgoal_tac "(ysa @ L # R # us) @ ys \<in> S")
    apply simp
   apply (rule app)
    prefer 2
    apply assumption
   apply simp
  apply clarsimp
  apply (erule app)
  apply simp
  done

lemma S_appendD:
  "xs @ ys \<in> S \<Longrightarrow> xs @ L # R # ys \<in> S"
  by (erule S_append, rule refl)

lemma is_bal_replicate [rule_format]:
  "is_bal xs n \<longrightarrow> replicate n L @ xs \<in> S"
  apply (induct_tac xs n rule: is_bal.induct)
     apply clarsimp
     apply (rule empty)
    apply clarsimp
   apply clarsimp
  apply clarsimp
  apply (drule S_appendD)
  apply simp
  done
  
lemma is_bal_then_set:
  "is_bal xs 0 \<Longrightarrow> xs \<in> S"
  apply (drule is_bal_replicate)
  apply simp
  done


section "Question 3: Hoare Logic"
-- ------------------------------

subsection "(a)"

(* 
  We use the syntax of Week 12, Mon: 
  Variables are just names without special syntax, but they have to be declared 
  as variables in the Hoare triple.
*)

-- "Example:"
lemma 
  "VARS i n (m::nat)
  {i = x}  
  m := 1;
  WHILE 0 < i 
  INV {m = n^(x - i) \<and> i \<le> x} 
  DO 
    i := i - 1; 
    m := m * n 
  OD 
  {m = n^x}"
  apply vcg
    apply simp
   apply clarsimp
   apply (simp add: Suc_diff_le)
  apply clarsimp
  done


subsection "(a)"

text {* (9 marks)
  Provide the answer in this text comment:

  The program computes the square root of a. 

  The result value of n is the smallest integer greater than
  or equal to the square root of a, or alternatively  
  0 < a \<longrightarrow> (n - 1)^2 \<le> a \<le> n^2. (For a = 0, n = 0).
*}


subsection "(b)" (* 9 marks *)

text {*
  Provide the answer in this text comment:

  The main invariant is:

          k=n*n \<and> 
          m=n+n  \<and> 
          (\<forall>p. a \<le> p*p \<longrightarrow> n\<le>p)

  Or, alternatively instead of the last conjunct:
          (n - 1) * (n - 1) < a 


  Some traces:

a = 11:
n = 1, k = 1, m = 2
n = 2, k = 4, m = 4
n = 3, k = 9, m = 6
n = 4, k = 16, m = 8
end: n = 4, k = 16, m = 8

a = 16:
n = 1, k = 1, m = 2
n = 2, k = 4, m = 4
n = 3, k = 9, m = 6
n = 4, k = 16, m = 8
end: n = 4, k = 16, m = 8

*}


subsection "(c)" (* 7 marks *)

(* solution courtesy of June: *)
lemma 
  "VARS a (n::nat) m (k::nat) 
  {True} 
    n := 0;  m := 0;  k := 0;
    WHILE k < a 
    INV { k=n*n \<and> m=n+n  \<and> (\<forall>p::nat. a\<le> p*p \<longrightarrow> n\<le>p) }
    DO
      n := n + 1;
      k := k + m + 1;
      m := m + 2
    OD
  { a \<le> n*n \<and> (\<forall>p::nat. a\<le> p*p \<longrightarrow> n\<le>p)}"
  apply vcg
    apply simp
   apply simp
   apply (clarsimp simp add: Nat_Numeral.power2_eq_square [symmetric])
   apply (subgoal_tac "n\<twosuperior><p\<twosuperior>")
    prefer 2 
    apply simp
   apply (fastsimp dest!: Nat_Numeral.power2_less_imp_less)
  apply simp
  done

(* also fine is: *)
lemma 
  "VARS a (n::nat) m (k::nat) 
  {True} 
    n := 0;  m := 0;  k := 0;
    WHILE k < a 
    INV { k = n * n \<and> 
          ((0 < a \<longrightarrow> (n - 1) * (n - 1) < a) \<and> (a = 0 \<longrightarrow> n = 0)) \<and> 
          m = n + n }
    DO
      n := n + 1;
      k := k + m + 1;
      m := m + 2
    OD
  { (0 < a \<longrightarrow> (n - 1) * (n - 1) < a \<and> a \<le> n*n) \<and> (a = 0 \<longrightarrow> n = 0)}"
  apply vcg 
    apply simp
   apply clarsimp
  apply clarsimp
  done

(* simpler version without a = 0 or \<le> instead of < is ok as well *)

section "Question 4: Calculational Reasoning"
-- ------------------------------------------

(* 
  You don't have to use the locale provided below if you find it
  confusing, you can also state the assumptions separately as in 
  the lecture.

  To make typing easier, the syntax for the inverse element and for 
  "one" is different to the demo file in the lecture. It is just the 
  word "inv" and the normal number "1".

  Tip: the operator \<cdot> can be typed in ProofGeneral as 
       . C-,    (dot followed by control-comma)
*)


locale group =
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> ('a::one)"  (infixl "\<cdot>" 70)
  fixes inv :: "'a \<Rightarrow> 'a" ("(_\<^sup>-)" [1000] 999) 

  assumes assoc: "\<And>x y z. (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
  assumes left_inv: "\<And>x. inv x \<cdot> x = 1"
  assumes left_one: "\<And>x. 1 \<cdot> x = x"


context group
begin

lemma right_inv: "x \<cdot> inv x = 1"
proof -
  have "x \<cdot> x\<^sup>- = 1 \<cdot> (x \<cdot> x\<^sup>-)" by (simp only: left_one)
  also have "\<dots> = 1 \<cdot> x \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>- \<cdot> x \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (x\<^sup>- \<cdot> x) \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> 1 \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (1 \<cdot> x\<^sup>-)" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>-" by (simp only: left_one)
  also have "\<dots> = 1" by (simp only: left_inv)
  finally show ?thesis .
qed

(* 8 marks *)
lemma right_one:
  "x \<cdot> 1 = x"
proof -
  have "x \<cdot> 1 = x \<cdot> (inv x \<cdot> x)" by (simp add: left_inv)
  also
  have "\<dots> = (x \<cdot> inv x) \<cdot> x" by (simp add: assoc)
  also
  have "x \<cdot> inv x = 1" by (simp add: right_inv)
  finally
  show ?thesis by (simp add: left_one)
qed

(* 9 marks *)
lemma unique_div:
  "\<exists>!x. a \<cdot> x = b"
proof
  show "a \<cdot> (inv a \<cdot> b) = b"
    by (simp add: assoc [symmetric] right_inv left_one)
next
  fix x
  assume b: "a \<cdot> x = b"
  show "x = inv a \<cdot> b"
    by (simp add: b [symmetric] assoc [symmetric] left_inv left_one)
qed

(* 8 marks *)
lemma cancel_left:
  "a \<cdot> x = a \<cdot> y \<Longrightarrow> x = y"
proof -
  assume "a \<cdot> x = a \<cdot> y"
  hence "inv a \<cdot> (a \<cdot> x) = inv a \<cdot> (a \<cdot> y)" by simp
  thus ?thesis
    by (simp add: assoc [symmetric] left_inv left_one)
qed 

end

end