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 thm Set.set_mp Set.subsetD |
7 datatype foo = |
|
8 Foo1 |
|
9 | Foo2 bar |
|
10 and bar = |
|
11 Bar |
|
12 |
|
13 ML {* #induct (Datatype_Data.the_info @{theory} "TypeSchemes.bar") *} |
|
14 |
8 |
15 |
9 atom_decl name |
16 atom_decl name |
10 |
17 |
11 (* defined as a single nominal datatype *) |
18 (* defined as a single nominal datatype *) |
12 |
19 |
14 Var "name" |
21 Var "name" |
15 | Fun "ty" "ty" |
22 | Fun "ty" "ty" |
16 and tys = |
23 and tys = |
17 All xs::"name fset" ty::"ty" bind (set+) xs in ty |
24 All xs::"name fset" ty::"ty" bind (set+) xs in ty |
18 |
25 |
|
26 ML {* |
|
27 get_all_info @{context} |
|
28 *} |
|
29 |
|
30 ML {* |
|
31 get_info @{context} "TypeSchemes.ty" |
|
32 *} |
|
33 |
|
34 ML {* |
|
35 #strong_exhaust (the_info @{context} "TypeSchemes.tys") |
|
36 *} |
|
37 |
19 thm ty_tys.distinct |
38 thm ty_tys.distinct |
20 thm ty_tys.induct |
39 thm ty_tys.induct |
21 thm ty_tys.inducts |
40 thm ty_tys.inducts |
22 thm ty_tys.exhaust ty_tys.strong_exhaust |
41 thm ty_tys.exhaust |
|
42 thm ty_tys.strong_exhaust |
23 thm ty_tys.fv_defs |
43 thm ty_tys.fv_defs |
24 thm ty_tys.bn_defs |
44 thm ty_tys.bn_defs |
25 thm ty_tys.perm_simps |
45 thm ty_tys.perm_simps |
26 thm ty_tys.eq_iff |
46 thm ty_tys.eq_iff |
27 thm ty_tys.fv_bn_eqvt |
47 thm ty_tys.fv_bn_eqvt |
81 apply (subst test3) |
101 apply (subst test3) |
82 defer |
102 defer |
83 apply (subst test3) |
103 apply (subst test3) |
84 defer |
104 defer |
85 apply rule*) |
105 apply rule*) |
|
106 thm subst_substs_graph.intros |
86 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
107 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
87 apply(simp add: eqvt_def) |
108 apply(simp add: eqvt_def) |
88 apply(rule allI) |
109 apply(rule allI) |
89 apply(simp add: permute_fun_def permute_bool_def) |
110 apply(simp add: permute_fun_def permute_bool_def) |
90 apply(rule ext) |
111 apply(rule ext) |