theory Lambda
imports "../Parser"
begin

atom_decl name

nominal_datatype lm =
  Vr "name"
| Ap "lm" "lm"
| Lm x::"name" l::"lm"  bind x in l

lemmas supp_fn' = lm.fv[simplified lm.supp]

(* 
  Old way of establishing strong induction
  principles by chosing a fresh name.
*)
lemma
  fixes c::"'a::fs"
  assumes a1: "\<And>name c. P c (Vr name)"
  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
  shows "P c lm"
proof -
  have "\<And>p. P c (p \<bullet> lm)"
    apply(induct lm arbitrary: c rule: lm.induct)
    apply(simp only: lm.perm)
    apply(rule a1)
    apply(simp only: lm.perm)
    apply(rule a2)
    apply(assumption)
    apply(assumption)
    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
    defer
    apply(simp add: fresh_def)
    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
    apply(simp add: supp_Pair finite_supp)
    apply(blast)
    apply(erule exE)
    apply(rule_tac t="p \<bullet> Lm name lm" and 
                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
    apply(simp del: lm.perm)
    apply(subst lm.perm)
    apply(subst (2) lm.perm)
    apply(rule flip_fresh_fresh)
    apply(simp add: fresh_def)
    apply(simp only: supp_fn')
    apply(simp)
    apply(simp add: fresh_Pair)
    apply(simp)
    apply(rule a3)
    apply(simp add: fresh_Pair)
    apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
    apply(simp)
    done
  then have "P c (0 \<bullet> lm)" by blast
  then show "P c lm" by simp
qed

(* 
  New way of establishing strong induction
  principles by using a appropriate permutation.
*)
lemma
  fixes c::"'a::fs"
  assumes a1: "\<And>name c. P c (Vr name)"
  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
  shows "P c lm"
proof -
  have "\<And>p. P c (p \<bullet> lm)"
    apply(induct lm arbitrary: c rule: lm.induct)
    apply(simp only: lm.perm)
    apply(rule a1)
    apply(simp only: lm.perm)
    apply(rule a2)
    apply(assumption)
    apply(assumption)
    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
    apply(erule exE)
    apply(rule_tac t="p \<bullet> Lm name lm" and 
                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
    defer
    apply(simp add: lm.perm)
    apply(rule a3)
    apply(simp add: eqvts fresh_star_def)
    apply(drule_tac x="q + p" in meta_spec)
    apply(simp)
    apply(rule at_set_avoiding2)
    apply(simp add: finite_supp)
    apply(simp add: finite_supp)
    apply(simp add: finite_supp)
    apply(simp only: lm.perm atom_eqvt)
    apply(simp add: fresh_star_def fresh_def supp_fn')
    apply(rule supp_perm_eq)
    apply(simp)
    done
  then have "P c (0 \<bullet> lm)" by blast
  then show "P c lm" by simp
qed

end