theory Hw07
  imports Nominal
begin


section {* Task 1 (hard) *}

text {* 

  The functions lookup and lookup2 are defined below. 
  Lookup2 takes an element and two lists as arguments. 
  It looks up the element in the first list. If it exists, 
  it takes its association and looks this association up 
  in the second list. If one of the look-ups, fails, then 
  lookup2 fails return None.

  1) Notice how the type of lookup2 reflects the behaviour of 
  this function.

  2) Rewrite lookup2 so that it uses a monad. Use the definition
  c >>= f from the lecture. 

  3) Show that the lookup2 below and your version of lookup2 are 
  equivalent. Hint: the simplifier will normally be sufficient
  to establish the equivalence. However, you need to add the
  lemma option.split to enable the simplifier to analyse 
  case-constructions. For example

     by (simp add: option.split) 

*}

fun
  lookup :: "'a \<Rightarrow> ('a\<times>'b) list \<Rightarrow> 'b option"
where
  "lookup x [] = None"
| "lookup z ((x,y)#xs) = (if x=z then Some y else lookup z xs)"

abbreviation
  lookup2 :: "'a \<Rightarrow> ('a\<times>'b) list \<Rightarrow> ('b\<times>'c) list \<Rightarrow> 'c option"
where
  "lookup2 z xs ys \<equiv> (case (lookup z xs) of
                         None \<Rightarrow> None
                       | Some y \<Rightarrow> lookup y ys)"

abbreviation
  mbind :: "'a option\<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"  ("_ >>= _" [65,65] 65) 
where  
  "c >>= f \<equiv> case c of None \<Rightarrow> None | (Some v) \<Rightarrow> f v"

abbreviation
  lookup2' :: "'a \<Rightarrow> ('a\<times>'b) list \<Rightarrow> ('b\<times>'c) list \<Rightarrow> 'c option"
where
  "lookup2' z xs ys \<equiv> (lookup z xs) >>= (\<lambda>y. lookup y ys)"

lemma 
  shows "lookup2 z xs ys = lookup2' z xs ys"
  by(simp add: option.split)

section {* Task 2 (easy) *}

text {* 
  
  Give a detailed Isar proof for the formula.
  
  Hint: Use the notes

  http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/isar-overview.pdf

*}

lemma "(A \<or> B \<longrightarrow> C) \<longrightarrow> \<not>B \<longrightarrow> \<not>C \<longrightarrow> \<not>A"
proof -
  { assume a: "A \<or> B \<longrightarrow> C"
    { assume b: "\<not>B"
      { assume c: "\<not>C"
	{ assume d: "A"
	  have "A \<or> B" by (rule disjI1)
	  with a have "C" by (rule mp) 
	  with c have "False" by (rule notE)
	}
	then have "\<not>A" by (rule notI)
      }
      then have "\<not>C \<longrightarrow> \<not>A" by (rule impI)
    }
    then have " \<not>B \<longrightarrow> \<not>C \<longrightarrow> \<not>A" by (rule impI)
  }
  then show "(A \<or> B \<longrightarrow> C) \<longrightarrow> \<not>B \<longrightarrow> \<not>C \<longrightarrow> \<not>A" by (rule impI)
qed


section {* Task 3 (easy) *}

text {* 
  
  1) Extend the language and compiler so that it
  also includes addition, multiplication and 
  successor. Make sure the compiler lemma still
  goes through.

  2) Introduce a mistake into the compiler, like
  compiling a multiplication as addition, and
  satisfy yourself that the compiler lemma now
  fails.
  
*}

datatype aexp = 
    V string
  | C nat 
  | Diff aexp aexp  ("_ -- _")
  | Plus aexp aexp  ("_ ++ _")
  | Mult aexp aexp  ("_ ** _")
  | Succ aexp       ("SUCC _")

types
  env = "(string\<times>nat) list"

fun
  eval :: "aexp \<Rightarrow> env \<Rightarrow> nat option"
where
  "eval (C n) env = Some n"
| "eval (V x) env = lookup x env"
| "eval (e1 -- e2) env = (eval e1 env) >>= (\<lambda>n1. (eval e2 env) >>= (\<lambda>n2. Some (n1 - n2)))"
| "eval (e1 ++ e2) env = (eval e1 env) >>= (\<lambda>n1. (eval e2 env) >>= (\<lambda>n2. Some (n1 + n2)))"
| "eval (e1 ** e2) env = (eval e1 env) >>= (\<lambda>n1. (eval e2 env) >>= (\<lambda>n2. Some (n1 * n2)))"
| "eval (SUCC e) env = (eval e env) >>= (\<lambda>n. Some (Suc n))"

datatype inst = 
    PushV string
  | PushC nat 
  | Sub
  | Add
  | Mul
  | Inc

types
 stack = "nat list"

fun (sequential)
  exec_instruc :: "inst \<Rightarrow> env \<Rightarrow> stack \<Rightarrow> stack option"
where
  "exec_instruc (PushC n) env s = Some (n#s)"
| "exec_instruc (PushV x) env s = (lookup x env) >>= (\<lambda>n. Some (n#s))"
| "exec_instruc Sub env (n1#n2#s) = Some ((n2 - n1)#s)"
| "exec_instruc Add env (n1#n2#s) = Some ((n2 + n1)#s)"
| "exec_instruc Mul env (n1#n2#s) = Some ((n2 * n1)#s)"
| "exec_instruc Inc env (n#s)     = Some ((Suc n)#s)"
| "exec_instruc _ _ _ = None"

fun
  exec :: "inst list \<Rightarrow> env \<Rightarrow> stack \<Rightarrow> stack option"
where
  "exec [] env s = Some s"  
| "exec (inst#insts) env s = (exec_instruc inst env s) >>= (exec insts env)"

fun
  compile :: "aexp \<Rightarrow> inst list"
where
  "compile (V n) = [PushV n]"
| "compile (C n) = [PushC n]"
| "compile (e1 -- e2) = (compile e1) @ (compile e2) @ [Sub]"
| "compile (e1 ++ e2) = (compile e1) @ (compile e2) @ [Add]"
| "compile (e1 ** e2) = (compile e1) @ (compile e2) @ [Mul]"
| "compile (SUCC e)   = (compile e) @ [Inc]"

declare option.split[split]

theorem exec_assoc: 
  "(exec (insts1 @ insts2) env s) = (exec insts1 env s) >>= (\<lambda>s1. (exec insts2 env s1))"
by (induct insts1 arbitrary: s) (simp_all)
      
theorem compiler_lemma: 
  "exec (compile exp) env s = (eval exp env) >>= (\<lambda>n.(Some(n#s)))"
by (induct exp arbitrary: s) (simp_all add: exec_assoc)


text {*

  Task 4: (hard)

  Below lambda-terms and the relation not_free
  is defined. The definition of the lambda-terms
  comes automatically with the definition about
  freshness, written _ \<sharp> _. 

  Prove that the relation not_free implies
  the freshness and vice versa.

  Hint: the direction "not_free implies freshness"
  can be proved by rule induction. The other
  direction can be proved by structural induction
  over lambda-terms. This induction principle
  is called

       thm lam.weak_induct

  You also need the lemmas

      thm fresh_atm
      thm abs_fresh

  which deal with _ \<sharp> _. Other lemmas are already
  built into the simplifier.

*}

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam" 
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._")

inductive
  not_free :: "name \<Rightarrow> lam \<Rightarrow> bool" ("_ nf _")
where
  nf_var:  "x\<noteq>y \<Longrightarrow> x nf (Var y)"
| nf_app:  "\<lbrakk>x nf t1; x nf t2\<rbrakk> \<Longrightarrow> x nf (App t1 t2)"
| nf_lam1: "\<lbrakk>x\<noteq>y; x nf t\<rbrakk> \<Longrightarrow> x nf Lam [y].t"
| nf_lam2: "x nf Lam [x].t"

lemma nf_implies_fresh:
  assumes a: "x nf t"
  shows "x\<sharp>t"
using a
by (induct)
   (simp_all add: abs_fresh fresh_atm)


lemma nf_implies_fresh_detailed:
  assumes a: "x nf t"
  shows "x\<sharp>t"
using a
proof (induct)
  case (nf_var x y)
  have "x\<noteq>y" by fact 
  then show "x\<sharp>Var y"  by (simp add: fresh_atm)
next
  case (nf_app x t1 t2)
  have "x\<sharp>t1" "x\<sharp>t2" by fact+
  then show "x\<sharp>App t1 t2" by simp
next
  case (nf_lam1 x y t)
  have "x\<noteq>y" "x\<sharp>t" by fact+
  then show "x\<sharp>Lam [y].t" by (simp add: abs_fresh)
next
  case (nf_lam2 x t)
  show "x\<sharp>Lam [x].t" by (simp add: abs_fresh)
qed

lemma fresh_implies_nf:
  assumes a: "x\<sharp>t"
  shows "x nf t"
using a
by (induct t rule: lam.weak_induct)
   (auto intro: not_free.intros simp add: fresh_atm abs_fresh)

lemma fresh_implies_nf_detailed:
  assumes a: "x\<sharp>t"
  shows "x nf t"
using a
proof (induct t rule: lam.weak_induct)
  case (Var y)
  have "x\<sharp>(Var y)" by fact
  then show "x nf (Var y)" by (simp add: fresh_atm nf_var)
next
  case (App t1 t2)
  have ih1: "x\<sharp>t1 \<Longrightarrow> x nf t1" by fact
  have ih2: "x\<sharp>t2 \<Longrightarrow> x nf t2" by fact
  have "x\<sharp>App t1 t2" by fact
  with ih1 ih2 have "x nf t1" "x nf t2" by simp_all
  then show "x nf (App t1 t2)" by (simp add: nf_app)
next
  case (Lam y t)
  have ih: "x\<sharp>t \<Longrightarrow> x nf t" by fact
  have a: "x\<sharp>Lam [y].t" by fact
  { assume "x=y"
    then have "x nf (Lam [y].t)" by (simp add: nf_lam2)
  }
  moreover
  { assume i: "x\<noteq>y"
    with a have "x\<sharp>t" by (simp add: abs_fresh)
    with ih have "x nf t" by simp
    with i have "x nf (Lam [y].t)" by (simp add: nf_lam1)
  }
  ultimately show "x nf (Lam [y].t)" by blast
qed

end