header "Exam COMP4161 S2/2008"

theory Exam 
  (* 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):
  i: 
  (\<lambda>z x y. z x y) (\<lambda>x y. x) x (f x) \<rightarrow> ?


  ii: 
  (\<lambda>x f. f (x x f)) (\<lambda>x f. f (x x f)) (\<lambda>f x. x) \<rightarrow> ?



(b):
  i: ( (\<lambda>z x y. z x y) (\<lambda>x y. x) x (f x) )


  ii: ( (\<lambda>x f. f (x x f)) (\<lambda>x f. f (x x f)) (\<lambda>f x. x) )


*}


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


subsection "(a)"

datatype paren = L | R

inductive_set 
  S :: "paren list set"
where
  (* replace appropriately: *)
  my_rule: "_ \<in> S"


(* 
  You will find that sometimes you need to reformulate lists 
  slightly such that for instance the rules for S become applicable. 
  You can achieve that with subgoal_tac (or Isar):
*)
lemma example:
  assumes some_rule: "\<And>xs ys. \<lbrakk> xs \<in> Z; ys \<in> Z \<rbrakk> \<Longrightarrow> xs @ y # ys \<in> Z"
  shows "\<lbrakk> xs \<in> Z; ys \<in> Z \<rbrakk> \<Longrightarrow> xs @ [y] @ ys \<in> Z"
  -- "some_rule doesn't apply, so we reformulate"
  apply (subgoal_tac "xs @ y # ys \<in> Z")
   -- "with the new statement as assumption, simp solves the problem"
   apply simp
  -- "now we need to prove the new statement"
  apply (rule some_rule, assumption, assumption)
  done


-- "test cases, prove appropriately, add 1 more"

lemma LR_S [intro!, simp]:
  "[L,R] \<in> S"
  apply (rule my_rule)
  done


subsection "(b)"

fun is_bal :: "paren list \<Rightarrow> nat \<Rightarrow> bool"
where
  (* replace appropriately: *)
  "is_bal _ _ = False"

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

(* 
  If you are using numbers greater than 1, you might need the lemma 
  "nat_number" to convert into (Suc _) form.
*) 

lemma "is_bal [L,R,R] 1"
  apply simp
  oops



subsection "(c)"

(* You will need to prove intermediate lemmas about is_bal to 
   prove this one *)

lemma set_is_bal:
  "xs \<in> S \<Longrightarrow> is_bal xs 0"
  oops


subsection "(d)"

(* 
  Below are some lemma statements that might help you in proving
  is_bal_then_set.
  
  You might also find the following two lemmas useful. 
*)
thm append_eq_append_conv2

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

(* Start proof: *)

(* this proof is a bit longer .. *)
lemma S_append [rule_format]:
  "zs \<in> S \<Longrightarrow> (\<forall>xs ys. zs = ys @ xs \<longrightarrow> ys @ L # R # xs \<in> S)"
  sorry

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"
  sorry

theorem is_bal_then_set:
  "is_bal xs 0 \<Longrightarrow> xs \<in> S"
  oops

corollary is_bal_is_set:
  "is_bal xs 0 = (xs \<in> S)"
  oops


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 {*
  Provide the answer in this text comment:

*}


subsection "(b)"

text {*
  Provide the answer in this text comment:

*}


subsection "(c)"

(* replace appropriately and prove: *)
lemma 
  "VARS a (n::nat) m (k::nat) 
  {P} 
    n := 0;  m := 0;  k := 0;
    WHILE k < a 
    INV { your_invariant }
    DO
      n := n + 1;
      k := k + m + 1;
      m := m + 2
    OD
  {Q}"
  apply vcg
  oops


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 "one" is different 
  to the demo file in the lecture. It is just the normal number "1".
  Also, instead of "x\<^sup>-" you can equivalently just type "inv x".

  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_one:
  "x \<cdot> 1 = x"
  oops

lemma unique_div:
  "\<exists>!x. a \<cdot> x = b"
  oops

lemma cancel_left:
  "a \<cdot> x = a \<cdot> y \<Longrightarrow> x = y"
  oops

end

end