39 nominal_datatype tys2 = |
38 nominal_datatype tys2 = |
40 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
39 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
41 |
40 |
42 thm tys2.distinct |
41 thm tys2.distinct |
43 thm tys2.induct |
42 thm tys2.induct |
44 thm tys2.exhaust |
43 thm tys2.exhaust tys2.strong_exhaust |
45 thm tys2.fv_defs |
44 thm tys2.fv_defs |
46 thm tys2.bn_defs |
45 thm tys2.bn_defs |
47 thm tys2.perm_simps |
46 thm tys2.perm_simps |
48 thm tys2.eq_iff |
47 thm tys2.eq_iff |
49 thm tys2.fv_bn_eqvt |
48 thm tys2.fv_bn_eqvt |
50 thm tys2.size_eqvt |
49 thm tys2.size_eqvt |
51 thm tys2.supports |
50 thm tys2.supports |
52 thm tys2.supp |
51 thm tys2.supp |
53 thm tys2.fresh |
52 thm tys2.fresh |
54 |
53 |
55 |
|
56 lemma strong_exhaust: |
|
57 fixes c::"'a::fs" |
|
58 assumes "\<And>names ty. \<lbrakk>fset (map_fset atom names) \<sharp>* c; y = All2 names ty\<rbrakk> \<Longrightarrow> P" |
|
59 shows "P" |
|
60 apply(rule_tac y="y" in tys2.exhaust) |
|
61 apply(rename_tac names ty2) |
|
62 apply(subgoal_tac "\<exists>q. (q \<bullet> (fset (map_fset atom names))) \<sharp>* c \<and> supp (All2 names ty2) \<sharp>* q") |
|
63 apply(erule exE) |
|
64 apply(perm_simp) |
|
65 apply(erule conjE) |
|
66 apply(rule assms(1)) |
|
67 apply(assumption) |
|
68 apply(clarify) |
|
69 apply(drule supp_perm_eq[symmetric]) |
|
70 apply(simp) |
|
71 apply(rule at_set_avoiding2) |
|
72 apply(simp add: finite_supp) |
|
73 apply(simp add: finite_supp) |
|
74 apply(simp add: finite_supp) |
|
75 apply(simp) |
|
76 apply(simp add: fresh_star_def) |
|
77 apply(simp add: tys2.fresh) |
|
78 done |
|
79 |
|
80 |
|
81 lemma strong_induct: |
54 lemma strong_induct: |
82 fixes c::"'a::fs" |
55 fixes c::"'a::fs" |
83 assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)" |
56 assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)" |
84 shows "P c tys" |
57 shows "P c tys" |
85 using assms |
58 using assms |
86 apply(induction_schema) |
59 apply(induction_schema) |
87 apply(rule_tac y="tys" in strong_exhaust) |
60 apply(rule_tac y="tys" in tys2.strong_exhaust) |
88 apply(blast) |
61 apply(blast) |
89 apply(relation "measure (\<lambda>(x,y). size y)") |
62 apply(relation "measure (\<lambda>(x,y). size y)") |
90 apply(simp_all add: tys2.size) |
63 apply(simp_all add: tys2.size) |
91 done |
64 done |
92 |
65 |