equal
deleted
inserted
replaced
36 |
36 |
37 nominal_datatype tys2 = |
37 nominal_datatype tys2 = |
38 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
38 All2 xs::"name fset" ty::"ty2" bind (res) xs in ty |
39 |
39 |
40 thm tys2.distinct |
40 thm tys2.distinct |
41 thm tys2.induct |
41 thm tys2.induct tys2.strong_induct |
42 thm tys2.exhaust tys2.strong_exhaust |
42 thm tys2.exhaust tys2.strong_exhaust |
43 thm tys2.fv_defs |
43 thm tys2.fv_defs |
44 thm tys2.bn_defs |
44 thm tys2.bn_defs |
45 thm tys2.perm_simps |
45 thm tys2.perm_simps |
46 thm tys2.eq_iff |
46 thm tys2.eq_iff |
47 thm tys2.fv_bn_eqvt |
47 thm tys2.fv_bn_eqvt |
48 thm tys2.size_eqvt |
48 thm tys2.size_eqvt |
49 thm tys2.supports |
49 thm tys2.supports |
50 thm tys2.supp |
50 thm tys2.supp |
51 thm tys2.fresh |
51 thm tys2.fresh |
52 |
|
53 lemma strong_induct: |
|
54 fixes c::"'a::fs" |
|
55 assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)" |
|
56 shows "P c tys" |
|
57 using assms |
|
58 apply(induction_schema) |
|
59 apply(rule_tac y="tys" in tys2.strong_exhaust) |
|
60 apply(blast) |
|
61 apply(relation "measure (\<lambda>(x,y). size y)") |
|
62 apply(simp_all add: tys2.size) |
|
63 done |
|
64 |
52 |
65 |
53 |
66 text {* Some Tests *} |
54 text {* Some Tests *} |
67 |
55 |
68 lemma |
56 lemma |