25 section {* Strong Exhausts Lemma and Strong Induction Lemma via Induct_schema *}

    26 

    27 lemma strong_exhaust:

    28   fixes c::"'a::fs"

    29   assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P"

    30   and     "\<And>lam1 lam2 ca. \<lbrakk>c = ca; y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" 

    31   and     "\<And>name lam ca. \<lbrakk>c = ca; atom name \<sharp> ca; y = Lam name lam\<rbrakk> \<Longrightarrow> P"

    32   shows "P"

    33 apply(rule_tac y="y" in lam.exhaust)

    34 apply(rule assms(1))

    35 apply(auto)[2]

    36 apply(rule assms(2))

    37 apply(auto)[2]

    38 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q")

    39 apply(erule exE)

    40 apply(erule conjE)

    41 apply(rule assms(3))

    42 apply(rule refl)

    43 apply(simp add: atom_eqvt)

    44 apply(clarify)

    45 apply(drule supp_perm_eq[symmetric])

    46 apply(simp)

    47 apply(rule at_set_avoiding2_atom)

    48 apply(simp add: finite_supp)

    49 apply(simp add: finite_supp)

    50 apply(simp add: lam.fresh)

    51 done

    52 

    53 

    54 lemma strong_induct:

    55   fixes c::"'a::fs"

    56   assumes a1: "\<And>name c. P c (Var name)"

    57   and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"

    58   and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"

    59   shows "P c lam"

    60 using assms

    61 apply(induction_schema)

    62 apply(rule_tac y="lam" in strong_exhaust)

    63 apply(blast)

    64 apply(blast)

    65 apply(blast)

    66 apply(relation "measure (\<lambda>(x,y). size y)")

    67 apply(auto)[1]

    68 apply(simp add: lam.size)

    69 apply(simp add: lam.size)

    70 apply(simp add: lam.size)

    71 done