equal
deleted
inserted
replaced
4 |
4 |
5 section {*** Type Schemes ***} |
5 section {*** Type Schemes ***} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 declare [[STEPS = 100]] |
9 (* defined as a single nominal datatype *) |
10 |
10 |
11 nominal_datatype ty = |
11 nominal_datatype ty = |
12 Var "name" |
12 Var "name" |
13 | Fun "ty" "ty" |
13 | Fun "ty" "ty" |
14 and tys = |
14 and tys = |
24 thm ty_tys.fv_bn_eqvt |
24 thm ty_tys.fv_bn_eqvt |
25 thm ty_tys.size_eqvt |
25 thm ty_tys.size_eqvt |
26 thm ty_tys.supports |
26 thm ty_tys.supports |
27 thm ty_tys.fsupp |
27 thm ty_tys.fsupp |
28 |
28 |
|
29 (* defined as two separate nominal datatypes *) |
|
30 |
29 nominal_datatype ty2 = |
31 nominal_datatype ty2 = |
30 Var2 "name" |
32 Var2 "name" |
31 | Fun2 "ty2" "ty2" |
33 | Fun2 "ty2" "ty2" |
32 |
34 |
33 nominal_datatype tys2 = |
35 nominal_datatype tys2 = |
48 |
50 |
49 |
51 |
50 text {* *} |
52 text {* *} |
51 |
53 |
52 (* |
54 (* |
53 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *} |
|
54 |
|
55 lemma strong_induct: |
55 lemma strong_induct: |
56 assumes a1: "\<And>name b. P b (Var name)" |
56 assumes a1: "\<And>name b. P b (Var name)" |
57 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
57 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
58 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
58 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
59 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
59 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
72 apply clarify |
72 apply clarify |
73 apply(rule_tac t="p \<bullet> All fset ty" and |
73 apply(rule_tac t="p \<bullet> All fset ty" and |
74 s="pa \<bullet> (p \<bullet> All fset ty)" in subst) |
74 s="pa \<bullet> (p \<bullet> All fset ty)" in subst) |
75 apply (rule supp_perm_eq) |
75 apply (rule supp_perm_eq) |
76 apply assumption |
76 apply assumption |
77 apply (simp only: ty_tys.perm) |
77 apply (simp only: ty_tys.perm_simps) |
78 apply (rule a3) |
78 apply (rule a3) |
79 apply(erule_tac x="(pa + p)" in allE) |
79 apply(erule_tac x="(pa + p)" in allE) |
80 apply simp |
80 apply simp |
81 apply (simp add: eqvts eqvts_raw) |
81 apply (simp add: eqvts eqvts_raw) |
82 apply (rule at_set_avoiding2) |
82 apply (rule at_set_avoiding2) |
87 apply(simp add: eqvts) |
87 apply(simp add: eqvts) |
88 apply(simp add: permute_fun_def atom_eqvt) |
88 apply(simp add: permute_fun_def atom_eqvt) |
89 apply (simp add: fresh_star_def) |
89 apply (simp add: fresh_star_def) |
90 apply clarify |
90 apply clarify |
91 apply (simp add: fresh_def) |
91 apply (simp add: fresh_def) |
92 apply (simp add: ty_tys_supp) |
92 apply(auto) |
|
93 apply (simp add: ty_tys.supp) |
93 done |
94 done |
94 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
95 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
95 then show ?thesis by simp |
96 then show ?thesis by simp |
96 qed |
97 qed |
97 |
98 |