header {*

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

        Hw08_\<guillemotleft>your name\<guillemotright>

*}

theory Hw08
  imports Nominal
begin

section {* Task 1 (easy) *}

text {* 

  Below I defined substitution, beta-reduction and the 
  transitive closure of beta-reduction. 

*}

atom_decl name

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

consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)

nominal_primrec
  "(Var x)[y::=s] = (if x=y then s else (Var x))"
  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done

inductive 
  "beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _")
where
  b1[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^isub>\<beta> App t2 s"
| b2[intro]: "s1 \<longrightarrow>\<^isub>\<beta> s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^isub>\<beta> App t s2"
| b3[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^isub>\<beta> Lam [x].t2"
| b4[intro]: "App (Lam [x].t) s \<longrightarrow>\<^isub>\<beta> t[x::=s]"

inductive 
  "beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _")
where
  bs1[intro]: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t"
| bs2[intro]: "t \<longrightarrow>\<^isub>\<beta> s \<Longrightarrow> t \<longrightarrow>\<^isub>\<beta>\<^sup>* s"
| bs3[intro]: "\<lbrakk>t1\<longrightarrow>\<^isub>\<beta>\<^sup>* t2; t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3"

text {*

  Show the two lemmas establishing the fact that 
  the beta-star-reduction is preserved under 
  the term constructors.

  Hint: since the introduction rules of the
  inductive definitions are labelled with "intro",
  Isabelle is already aware of them (you do no
  need to say intro: beta.intros).

  Hint: The second lemma might have to be established 
  using "two" side-lemmas.

*}


lemma Beta_Lam_cong: 
  assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
  shows "Lam [x].t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam [x].t2"
using a by (induct) (blast)+

lemma Beta_App_cong_aux: 
  assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" 
  shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
    and "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
using a by (induct) (blast)+

lemma Beta_App_cong: 
  assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2" 
  shows "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
using a by (blast intro: Beta_App_cong_aux)


section {* Task 2 (easy) *}

text {* 
  
  Give a detailed Isar proof for the formula
  (\<forall>x. P x) \<longrightarrow> (\<exists>x. P x).
  
  Hint: The rules needed for dealing with the 
  quantifiers are

  thm allE
  thm exI
  
  Hint: Use the notes

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

*}

lemma "(\<forall>x. P x) \<longrightarrow> (\<exists>x. P x)"
proof -
  { assume "\<forall>x. P x"
    then have "P t" by (rule allE)
    then have "\<exists>x. P x" by (rule exI)
  }
  then show "(\<forall>x. P x) \<longrightarrow> (\<exists>x. P x)" by (rule impI)
qed


text {*

  Task 3 (hard)

  Permutations are lists of pairs of names. Below I defined how 
  such a permutation operates on names (remember Lecture 7). 

*}

fun
  perm :: "(name\<times>name) list \<Rightarrow> name \<Rightarrow> name" ("_ \<circ> _") 
where
  "[] \<circ> x = x"
| "((z,y)#pi) \<circ> x = (if pi \<circ> x = z then y else (if pi \<circ> x = y then z else pi \<circ> x))"

text {* 
  
  Since permutations are represented as list, the inverse of
  a permutation is the reversal of the list. For example

        permutation             its inverse

        [(a,c)(a,d)]            [(a,d),(a,c)] 
      
  Lemmas l1 and l2 show how both permutations operate on the
  names a, b, c and d. You can notice that in the argument
  and result in the first lemma are reversed in the second.
  (The reason is that permutations are bijections.)
   
*}

lemma l1:
  assumes a: "distinct [a,b,c,d]"
  shows "[(a,c),(a,d)] \<circ> a = d"
  and   "[(a,c),(a,d)] \<circ> b = b"
  and   "[(a,c),(a,d)] \<circ> c = a"
  and   "[(a,c),(a,d)] \<circ> d = c"
using a by (auto)

lemma l2:
  assumes a: "distinct [a,b,c,d]"
  shows "[(a,d),(a,c)] \<circ> a = c"
  and   "[(a,d),(a,c)] \<circ> b = b"
  and   "[(a,d),(a,c)] \<circ> c = d"
  and   "[(a,d),(a,c)] \<circ> d = a"
using a by (auto)

text {*

  The task is to show the general fact that applying a permutation
  and its inverse to a name is the identity. 

  Hint: you might need a lemma about appended permutations.

*}

lemma pi_append:
  shows "(pi1@pi2) \<circ> x = pi1 \<circ> (pi2 \<circ> x)"
by (induct pi1) (auto)

lemma 
  shows "(rev pi) \<circ> (pi \<circ> x) = x"
by (induct pi) (auto simp add: pi_append)

text {* 

  Task 4: (hard)

  Below I define contexts having a single hole
  and the operation of filling a lambda-term into
  that hole. Prove the lemma showing that for every
  reduction, there must be a context which uniquely
  identifies where the reduction occurred. 

*} 

datatype ctx = 
    Hole ("\<box>" 1000)  
  | CAppL "ctx" "lam"
  | CAppR "lam" "ctx" 
  | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100) 

fun
  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>")
where
  "\<box>\<lbrakk>t\<rbrakk> = t"
| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 

lemma
  assumes a: "t \<longrightarrow>\<^isub>\<beta> t'"
  shows "\<exists>C x s1 s2. t = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t' = C\<lbrakk>s1[x::=s2]\<rbrakk>"
using a
by (induct) (metis b1 b2 b3 b4 filling.simps)+

lemma
  assumes a: "t \<longrightarrow>\<^isub>\<beta> t'"
  shows "\<exists>C x s1 s2. t = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t' = C\<lbrakk>s1[x::=s2]\<rbrakk>"
using a
proof (induct)
  case (b1 t1 t2 s)
  have "\<exists>C x s1 s2. t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by fact
  then obtain C x s1 s2 where "t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by blast
  then have "App t1 s = (CAppL C s)\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> App t2 s = (CAppL C s)\<lbrakk>s1[x::=s2]\<rbrakk>" by simp
  then show "\<exists>C x s1 s2. App t1 s = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> App t2 s = C\<lbrakk>s1[x::=s2]\<rbrakk>" by blast
next
  case (b2 t1 t2 s)
  have "\<exists>C x s1 s2. t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by fact
  then obtain C x s1 s2 where "t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by blast
  then have "App s t1 = (CAppR s C)\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> App s t2 = (CAppR s C)\<lbrakk>s1[x::=s2]\<rbrakk>" by simp
  then show "\<exists>C x s1 s2. App s t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> App s t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by blast
next
  case (b3 t1 t2 y)
  have "\<exists>C x s1 s2. t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by fact
  then obtain C x s1 s2 where "t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by blast
  then have "Lam [y].t1 = (CLam [y].C)\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> Lam [y].t2 = (CLam [y].C)\<lbrakk>s1[x::=s2]\<rbrakk>" by simp
  then show "\<exists>C x s1 s2. Lam [y].t1 = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> Lam [y].t2 = C\<lbrakk>s1[x::=s2]\<rbrakk>" by blast
next
  case (b4 y t s)
  then have "App (Lam [y].t) s = \<box>\<lbrakk>App (Lam [y].t) s\<rbrakk> \<and> t[y::=s] = \<box>\<lbrakk>t[y::=s]\<rbrakk>" by simp
  then show "\<exists>C x s1 s2. App (Lam [y].t) s = C\<lbrakk>App (Lam [x].s1) s2\<rbrakk> \<and> t[y::=s] = C\<lbrakk>s1[x::=s2]\<rbrakk>" 
    by blast
qed

text {* 

  Task 5: (?)

  Prove the follwoing lemma. 

  Hint: Think carefully about the induction.

*}

lemma 
  assumes a: "t \<longrightarrow>\<^isub>\<beta> t'"
  shows "C\<lbrakk>t\<rbrakk> \<longrightarrow>\<^isub>\<beta> C\<lbrakk>t'\<rbrakk>"
using a
by (induct C) (auto)

end