equal
deleted
inserted
replaced
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 section {*** Type Schemes ***} |
5 section {*** Type Schemes ***} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
|
8 |
8 |
9 |
9 (* defined as a single nominal datatype *) |
10 (* defined as a single nominal datatype *) |
10 |
11 |
11 nominal_datatype ty = |
12 nominal_datatype ty = |
12 Var "name" |
13 Var "name" |
46 thm tys2.fv_bn_eqvt |
47 thm tys2.fv_bn_eqvt |
47 thm tys2.size_eqvt |
48 thm tys2.size_eqvt |
48 thm tys2.supports |
49 thm tys2.supports |
49 thm tys2.supp |
50 thm tys2.supp |
50 thm tys2.fresh |
51 thm tys2.fresh |
|
52 |
|
53 |
|
54 lemma strong_exhaust: |
|
55 fixes c::"'a::fs" |
|
56 assumes "\<And>names ty. \<lbrakk>fset (map_fset atom names) \<sharp>* c; y = All2 names ty\<rbrakk> \<Longrightarrow> P" |
|
57 shows "P" |
|
58 apply(rule_tac y="y" in tys2.exhaust) |
|
59 apply(rename_tac names ty2) |
|
60 apply(subgoal_tac "\<exists>q. (q \<bullet> (fset (map_fset atom names))) \<sharp>* c \<and> supp (All2 names ty2) \<sharp>* q") |
|
61 apply(erule exE) |
|
62 apply(perm_simp) |
|
63 apply(erule conjE) |
|
64 apply(rule assms(1)) |
|
65 apply(assumption) |
|
66 apply(clarify) |
|
67 apply(drule supp_perm_eq[symmetric]) |
|
68 apply(simp) |
|
69 thm at_set_avoiding |
|
70 apply(rule at_set_avoiding2) |
|
71 apply(simp add: finite_supp) |
|
72 apply(simp add: finite_supp) |
|
73 apply(simp add: finite_supp) |
|
74 apply(simp) |
|
75 apply(simp add: fresh_star_def) |
|
76 apply(simp add: tys2.fresh) |
|
77 done |
|
78 |
|
79 |
|
80 lemma strong_induct: |
|
81 fixes c::"'a::fs" |
|
82 assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)" |
|
83 shows "P c tys" |
|
84 using assms |
|
85 apply(induction_schema) |
|
86 apply(rule_tac y="tys" in strong_exhaust) |
|
87 apply(blast) |
|
88 apply(relation "measure (\<lambda>(x,y). size y)") |
|
89 apply(simp_all add: tys2.size) |
|
90 done |
51 |
91 |
52 |
92 |
53 text {* *} |
93 text {* *} |
54 |
94 |
55 (* |
95 (* |