theory Foo1imports "../Nominal2" begintext {* Contrived example that has more than one binding function*}atom_decl namenominal_datatype foo: trm = Var "name"| App "trm" "trm"| Lam x::"name" t::"trm" bind x in t| Let1 a::"assg" t::"trm" bind "bn1 a" in t| Let2 a::"assg" t::"trm" bind "bn2 a" in t| Let3 a::"assg" t::"trm" bind "bn3 a" in t| Let4 a::"assg'" t::"trm" bind (set) "bn4 a" in tand assg = As "name" "name" "trm"and assg' = BNil| BAs "name" "assg'"binder bn1::"assg \<Rightarrow> atom list" and bn2::"assg \<Rightarrow> atom list" and bn3::"assg \<Rightarrow> atom list" and bn4::"assg' \<Rightarrow> atom set"where "bn1 (As x y t) = [atom x]"| "bn2 (As x y t) = [atom y]"| "bn3 (As x y t) = [atom x, atom y]"| "bn4 (BNil) = {}"| "bn4 (BAs a as) = {atom a} \<union> bn4 as"thm foo.permute_bnthm foo.perm_bn_alphathm foo.perm_bn_simpsthm foo.bn_finitethm foo.distinctthm foo.inductthm foo.inductsthm foo.exhaustthm foo.fv_defsthm foo.bn_defsthm foo.perm_simpsthm foo.eq_iffthm foo.fv_bn_eqvtthm foo.size_eqvtthm foo.supportsthm foo.fsuppthm foo.suppthm foo.freshthm foo.bn_finitelemma strong_exhaust1: fixes c::"'a::fs" assumes "\<exists>name. y = Var name \<Longrightarrow> P" and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" and "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P" and "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P" and "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P" and "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P" shows "P"oopslemma strong_exhaust2: fixes c::"'a::fs" assumes "\<And>name. y = Var name \<Longrightarrow> P" and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" shows "P"oopslemma strong_exhaust1: fixes c::"'a::fs" assumes "\<And>name. y = Var name \<Longrightarrow> P" and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" shows "P"oops lemma strong_exhaust2: assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" shows "P"apply(rule_tac y="as" in foo.exhaust(2))apply(rule assms(1))apply(assumption)donelemma strong_exhaust3: assumes "as' = BNil \<Longrightarrow> P" and "\<And>a as. as' = BAs a as \<Longrightarrow> P" shows "P"apply(rule_tac y="as'" in foo.exhaust(3))apply(rule assms(1))apply(assumption)apply(rule assms(2))apply(assumption)donelemma fixes t::trm and as::assg and as'::assg' and c::"'a::fs" assumes a1: "\<And>x c. P1 c (Var x)" and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" and a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)" and a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)" and a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)" and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" and a9: "\<And>c. P3 c (BNil)" and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" shows "P1 c t" "P2 c as" "P3 c as'"oops(*using assmsapply(induction_schema)apply(rule_tac y="t" and c="c" in strong_exhaust1)apply(simp_all)[7]apply(rule_tac as="as" in strong_exhaust2)apply(simp)apply(rule_tac as'="as'" in strong_exhaust3)apply(simp_all)[2]apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))")apply(simp_all add: foo.size)done*)end