header {*

  Hand-in on 13 May at noon. Please rename the file 
  and send your solution to me as

        Hw07_\<guillemotleft>your name\<guillemotright>

*}

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"

lemma 
  shows "lookup2 z xs ys = lookup2' z xs ys"
  sorry

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

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  ("_ -- _")

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

datatype inst = 
    PushV string
  | PushC nat 
  | Sub

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 _ _ _ = 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]"

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 shoul are 
  already by known to 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"
sorry

lemma fresh_implies_nf:
  assumes a: "x\<sharp>t"
  shows "x nf t"
sorry


end