header {*

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

        Hw10_\<guillemotleft>your name\<guillemotright>

*}

theory Hw10
  imports Nominal
begin

text {*

  Task 1 (easy)

  Below is the definition for lambda-terms and
  substitution. Prove the fact that if a variable,
  say x, is not free in a term L (that is x\<sharp>L)
  then a subtitution does not change the term.

  *}

atom_decl name

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

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

lemma forget: 
  assumes a: "x\<sharp>L"
  shows "L[x::=P] = L"
  using a
proof (nominal_induct L avoiding: x P rule: lam.strong_induct)
  case (Lam y T)
  have fc: "y\<sharp>x" "y\<sharp>P" by fact+
  have ih: "x\<sharp>T \<Longrightarrow> T[x::=P] = T" by fact
  have a: "x\<sharp>Lam [y].T" by fact

  show "(Lam [y].T)[x::=P] = Lam [y].T"


text {*

  Task 2 (hard)

  Below I defined beta-reduction and proved the 
  substitution lemma and the fresh_fact lemma. 
  You should prove that beta-reduction is preserved 
  under substitution.

  Hint: You might need, in additon to the lemmas
  below, the lemmas fresh_prod and fresh_atm.

  *}

inductive 
  "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
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]: "x\<sharp>s \<Longrightarrow> App (Lam [x].t) s \<longrightarrow>\<^isub>\<beta> t[x::=s]"

lemma  subst_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
by (nominal_induct t1 avoiding: x t2 rule: lam.induct)
   (auto simp add: perm_bij fresh_atm fresh_bij)

lemma fresh_fact:
  fixes z::"name"
  shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.induct)
   (auto simp add: abs_fresh fresh_prod fresh_atm)

equivariance Beta
nominal_inductive Beta
  by (auto simp add: abs_fresh fresh_fact)

lemma substitution_lemma:  
  assumes a: "x\<noteq>y" "x\<sharp>u"
  shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
using a by (nominal_induct t avoiding: x y s u rule: lam.induct)
           (auto simp add: fresh_fact forget)

lemma
  assumes a: "t \<longrightarrow>\<^isub>\<beta> t'"
  shows "t[x::=s] \<longrightarrow>\<^isub>\<beta> t'[x::=s]"
using a
proof (nominal_induct t t' avoiding: x s rule: Beta.strong_induct)
oops   

text {*

  Task 3 (easy)
  
  Give detailed Isar-proofs for the following two de Morgan laws.
  
*}

lemma 
  assumes a: "\<not>(\<exists>x. P x)" 
  shows "\<forall>x. \<not>P x"
oops

lemma 
  assumes a: "\<forall>x. \<not>P x"
  shows "\<not>(\<exists>x. P x)"
oops

text {*

  Task  4 (hard)

  Below are the definition for formulae and a 
  provablility judgement. Next are the definitions
  of the functions distr and cnf, which transform
  a formula into a conjunction normal form. A
  formula is in conjuctive normal form if it is of 
  the form

       (P1\<or>*P2\<or>*\<dots>)\<and>*(Q1\<or>*\<dots>)\<and>*\<dots>\<and>*(Z1\<or>*\<dots>)

  The point of this task is to show that if a 
  formula is provable, then so is its conjunctive
  normals form.

  Hint: You might need some of the proved lemmas. 

*}

datatype form =
  Prop "string"
| And  "form" "form" ("_ \<and>* _")
| Or   "form" "form" ("_ \<or>* _")

inductive
  provable :: "form set \<Rightarrow> form \<Rightarrow> bool" ("_ \<Rightarrow>* _")
where
 p1[intro]: "Prop s\<in>\<Gamma> \<Longrightarrow> \<Gamma> \<Rightarrow>* Prop s"
|p2[intro]: "\<lbrakk>\<Gamma> \<Rightarrow>* B; \<Gamma> \<Rightarrow>* C\<rbrakk> \<Longrightarrow> \<Gamma> \<Rightarrow>* B \<and>* C"
|p3[intro]: "\<Gamma> \<Rightarrow>* B \<Longrightarrow> \<Gamma> \<Rightarrow>* B \<or>* C"
|p4[intro]: "\<Gamma> \<Rightarrow>* C \<Longrightarrow> \<Gamma> \<Rightarrow>* B \<or>* C"

lemma p2_elim[dest]: 
  assumes a: "\<Gamma> \<Rightarrow>* B \<and>* C"
  shows "(\<Gamma> \<Rightarrow>* B) \<and> (\<Gamma> \<Rightarrow>* C)"
using a by (cases) (simp_all)

lemma p34_elim[dest]: 
  assumes a: "\<Gamma> \<Rightarrow>* B \<or>* C"
  shows "(\<Gamma> \<Rightarrow>* B) \<or> (\<Gamma> \<Rightarrow>* C)"
using a by (cases) (simp_all)

fun
 distr :: "form \<Rightarrow> form \<Rightarrow> form"
where
 d1: "distr (A \<and>* B) C = (distr A C) \<and>* (distr B C)"
|d2: "distr C (A \<and>* B) = (distr C A) \<and>* (distr C B)"
|d3: "distr A B = A \<or>* B"

fun 
 cnf :: "form \<Rightarrow> form"
where
 c1: "cnf (Prop s) = Prop s"
|c2: "cnf (A \<and>* B) = (cnf A) \<and>* (cnf B)"
|c3: "cnf (A \<or>* B) = distr (cnf A) (cnf B)"

thm distr.simps[no_vars] 
thm distr.induct[no_vars]

lemma a1:
  assumes a: "\<Gamma> \<Rightarrow>* B"
  shows "\<Gamma> \<Rightarrow>* distr B C"
using a 
by (induct B C rule: distr.induct) (auto)

lemma a2:
  assumes a: "\<Gamma> \<Rightarrow>* C"
  shows "\<Gamma> \<Rightarrow>* distr B C"
using a by (induct B C rule: distr.induct) (auto)

lemma 
  assumes a: "\<Gamma> \<Rightarrow>* B"
  shows "\<Gamma> \<Rightarrow>* cnf B"
using a
oops

text {*

  Task 5 (?)

  One is also interested in the other direction
  of the above lemma, that is if a conjunctive
  normalform is provale then so is the corresponding
  formula. Here the induction needs to be done
  via an induction over the functions definition
  (we have not seen this principle in the lectures).

  Hint: The cases in this induction are just 
  called 1 2 and 3.

  *}

thm cnf.induct

lemma a3:
  assumes a: "\<Gamma> \<Rightarrow>* distr B C"
  shows "(\<Gamma> \<Rightarrow>* B) \<or> (\<Gamma> \<Rightarrow>* C)"
using a by (induct B C rule: distr.induct) (auto)

lemma 
  assumes a: "\<Gamma> \<Rightarrow>* cnf B"
  shows "\<Gamma> \<Rightarrow>* B"
using a
proof (induct B rule: cnf.induct)
print_cases
oops 

end