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+
−
+
−
+
−
+
−