theory Sem04
imports "Lambda"
begin

text {******************************************************************
  
  Formalising Barendregt's Proof of the Substitution Lemma
  --------------------------------------------------------

  Barendregt's proof needs in the variable case a case distinction.
  One way to do this in Isar is to use blocks. A block is some sequent
  or reasoning steps enclosed in curly braces

  { \<dots>

    have "statement"
  }

  Such a block can contain local assumptions like

  { assume "A"
    assume "B"
    \<dots>
    have "C" by \<dots>
  }

  Where "C" is the last have-statement in this block. The behaviour 
  of such a block to the 'outside' is the implication

   \<lbrakk>A; B\<rbrakk> \<Longrightarrow> "C" 

  Now if we want to prove a property "smth" using the case-distinctions
  P\<^isub>1, P\<^isub>2 and P\<^isub>3 then we can use the following reasoning:

    { assume "P\<^isub>1"
      \<dots>
      have "smth"
    }
    moreover
    { assume "P\<^isub>2"
      \<dots>
      have "smth"
    }
    moreover
    { assume "P\<^isub>3"
      \<dots>
      have "smth"
    }
    ultimately have "smth" by blast

  The blocks establish the implications

    P\<^isub>1 \<Longrightarrow> smth
    P\<^isub>2 \<Longrightarrow> smth
    P\<^isub>3 \<Longrightarrow> smth

  If we know that P\<^isub>1, P\<^isub>2 and P\<^isub>3 cover all the cases, that is P\<^isub>1 \<or> P\<^isub>2 \<or> P\<^isub>3 is
  true, then we have 'ultimately' established the property "smth" 
  
*}

text {******************************************************************
  
  Exercise
  --------

  Fill in the cases 1.2 and 1.3 and the equational reasoning 
  in the lambda-case.
*}

thm forget[no_vars] 
thm fresh_fact[no_vars] 

lemma 
  assumes a: "x\<noteq>y"
  and     b: "x\<sharp>L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a b
proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
  case (Var z)
  have a1: "x\<noteq>y" by fact
  have a2: "x\<sharp>L" by fact
  show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
  proof -
    { (*Case 1.1*)
      assume c1: "z=x"
      have "(1)": "?LHS = N[y::=L]" using c1 by simp
      have "(2)": "?RHS = N[y::=L]" using c1 a1 by simp
      have "?LHS = ?RHS" using "(1)" "(2)" by simp
    }
    moreover 
    { (*Case 1.2*)
      assume c2: "z=y" "z\<noteq>x" 
      
      have "?LHS = ?RHS" sorry
    }
    moreover 
    { (*Case 1.3*)
      assume c3: "z\<noteq>x" "z\<noteq>y"
      
      have "?LHS = ?RHS" sorry
    }
    ultimately show "?LHS = ?RHS" by blast
  qed
next
  case (Lam z M1) (* case 2: lambdas *)
  have ih: "\<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
  have a1: "x\<noteq>y" by fact
  have a2: "x\<sharp>L" by fact
  have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact+
  then have b: "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
  show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
  proof - 
    have "?LHS = \<dots>" sorry

    also have "\<dots> = ?RHS" sorry
    finally show "?LHS = ?RHS" by simp
  qed
next
  case (App M1 M2) (* case 3: applications *)
  then show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
qed

text {* 
  Again the strong induction principle enables Isabelle to find
  the proof of the substitution lemma automatically. 
*}

lemma substitution_lemma_version:  
  assumes asm: "x\<noteq>y" "x\<sharp>L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
  using asm 
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
   (auto simp add: fresh_fact forget)

text {******************************************************************
  
  Proof for the Strong Induction Principle
  ----------------------------------------

*}

lemma lam_strong_induct:
  fixes c::"'a::fs_name"
  assumes a1: "\<And>x c. P c (Var x)"
  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P c (App t1 t2)"
  and     a3: "\<And>x t c. \<lbrakk>x\<sharp>c; \<And>c. P c t\<rbrakk> \<Longrightarrow> P c Lam [x].t"
  shows "P c t"
proof -
  have "\<forall>(pi::name prm) c. P c (pi\<bullet>t)"
  proof (induct t rule: lam.induct)
    case (Lam x t)
    have ih: "\<forall>(pi::name prm) c. P c (pi\<bullet>t)" by fact
    { fix pi::"name prm" and c::"'a::fs_name"
      obtain y::"name" where fc: "y\<sharp>(pi\<bullet>x,pi\<bullet>t,c)" 
	by (rule exists_fresh, auto simp add: fs_name1)
      from ih have "\<forall>c. P c (([(y,pi\<bullet>x)]@pi)\<bullet>t)" by simp
      then have "\<forall>c. P c ([(y,pi\<bullet>x)]\<bullet>(pi\<bullet>t))" by (auto simp only: pt_name2)
      with a3 have "P c (Lam [y].[(y,pi\<bullet>x)]\<bullet>(pi\<bullet>t))" using fc by (simp)
      moreover
      have "Lam [y].[(y,pi\<bullet>x)]\<bullet>(pi\<bullet>t) = Lam [(pi\<bullet>x)].(pi\<bullet>t)" 
	using fc by (simp add: lam.inject alpha fresh_atm fresh_prod)
      ultimately have "P c (Lam [(pi\<bullet>x)].(pi\<bullet>t))" by simp
    }
    then have "\<forall>(pi::name prm) c. P c (Lam [(pi\<bullet>x)].(pi\<bullet>t))" by auto    
    then show "\<forall>(pi::name prm) c. P c (pi\<bullet>(Lam [x].t))" by simp
  qed (auto intro: a1 a2)
  then have "P c (([]::name prm)\<bullet>t)" by blast
  then show "P c t" by simp
qed

text {*

  Support
  -------
*}

lemma
  shows "supp (t\<^isub>1,t\<^isub>2) = supp t\<^isub>1 \<union> ((supp t\<^isub>2)::atom set)"
proof -
 have "supp (t\<^isub>1,t\<^isub>2) = {a. inf {b. [(a,b)]\<bullet>(t\<^isub>1,t\<^isub>2) \<noteq> (t\<^isub>1,t\<^isub>2)}}" 
    by (simp add: supp_def)
 also have "\<dots> = {a. inf {b. ([(a,b)]\<bullet>t\<^isub>1,[(a,b)]\<bullet>t\<^isub>2) \<noteq> (t\<^isub>1,t\<^isub>2)}}" by simp
 also have "\<dots> = {a. inf {b. [(a,b)]\<bullet>t\<^isub>1 \<noteq> t\<^isub>1 \<or> [(a,b)]\<bullet>t\<^isub>2 \<noteq> t\<^isub>2}}" by simp
 also have "\<dots> = {a. inf ({b. [(a,b)]\<bullet>t\<^isub>1 \<noteq> t\<^isub>1} \<union> {b. [(a,b)]\<bullet>t\<^isub>2 \<noteq> t\<^isub>2})}" 
    by (simp only: Collect_disj_eq)
 also have "\<dots> = {a. (inf {b. [(a,b)]\<bullet>t\<^isub>1 \<noteq> t\<^isub>1})\<or>(inf {b. [(a,b)]\<bullet>t\<^isub>2 \<noteq> t\<^isub>2})}"
    by simp
 also have "\<dots> = {a. inf {b. [(a,b)]\<bullet>t\<^isub>1 \<noteq> t\<^isub>1}}\<union>{a. inf {b. [(a,b)]\<bullet>t\<^isub>2 \<noteq> t\<^isub>2}}"
    by (simp only: Collect_disj_eq)
 also have "\<dots> = supp t\<^isub>1 \<union> supp t\<^isub>2" by (simp add: supp_def)
 finally show "supp (t\<^isub>1,t\<^isub>2) = supp t\<^isub>1 \<union> ((supp t\<^isub>2)::atom set)" by simp
qed


end