12 Var "name" |
12 Var "name" |
13 | Fun "t" "t" |
13 | Fun "t" "t" |
14 and tyS = |
14 and tyS = |
15 All xs::"name fset" ty::"t" bind xs in ty |
15 All xs::"name fset" ty::"t" bind xs in ty |
16 |
16 |
17 lemma size_eqvt: "size (pi \<bullet> x) = size x" |
17 lemma size_eqvt_raw: |
18 sorry (* Can this be shown? *) |
18 "size (pi \<bullet> t :: t_raw) = size t" |
|
19 "size (pi \<bullet> ts :: tyS_raw) = size ts" |
|
20 apply (induct rule: t_raw_tyS_raw.inducts) |
|
21 apply simp_all |
|
22 done |
19 |
23 |
20 instantiation t and tyS :: size begin |
24 instantiation t and tyS :: size begin |
21 |
25 |
22 quotient_definition |
26 quotient_definition |
23 "size_t :: t \<Rightarrow> nat" |
27 "size_t :: t \<Rightarrow> nat" |
34 "alpha_tyS_raw a b \<Longrightarrow> size a = size b" |
38 "alpha_tyS_raw a b \<Longrightarrow> size a = size b" |
35 apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts) |
39 apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts) |
36 apply (simp_all only: t_raw_tyS_raw.size) |
40 apply (simp_all only: t_raw_tyS_raw.size) |
37 apply (simp_all only: alpha_gen) |
41 apply (simp_all only: alpha_gen) |
38 apply clarify |
42 apply clarify |
39 apply (simp_all only: size_eqvt) |
43 apply (simp_all only: size_eqvt_raw) |
40 done |
44 done |
41 |
45 |
42 lemma [quot_respect]: |
46 lemma [quot_respect]: |
43 "(alpha_t_raw ===> op =) size size" |
47 "(alpha_t_raw ===> op =) size size" |
44 "(alpha_tyS_raw ===> op =) size size" |
48 "(alpha_tyS_raw ===> op =) size size" |
71 |
75 |
72 lemma induct: |
76 lemma induct: |
73 assumes a1: "\<And>name b. P b (Var name)" |
77 assumes a1: "\<And>name b. P b (Var name)" |
74 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
78 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
75 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)" |
79 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)" |
76 shows "P (a :: 'a :: pt) t \<and> P' d ts " |
80 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
77 proof - |
81 proof - |
78 have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))" |
82 have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))" |
79 apply (rule t_tyS.induct) |
83 apply (rule t_tyS.induct) |
80 apply (simp add: a1) |
84 apply (simp add: a1) |
81 apply (simp) |
85 apply (simp) |
83 apply (rule a2) |
87 apply (rule a2) |
84 apply simp |
88 apply simp |
85 apply simp |
89 apply simp |
86 apply (rule allI) |
90 apply (rule allI) |
87 apply (rule allI) |
91 apply (rule allI) |
88 apply(subgoal_tac "\<exists>new::name fset. fset_to_set (fmap atom new) \<sharp>* (d, All (p \<bullet> fset) (p \<bullet> t)) |
92 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)") |
89 \<and> fcard new = fcard fset") |
|
90 apply clarify |
93 apply clarify |
91 (*apply(rule_tac t="p \<bullet> All fset t" and |
94 apply(rule_tac t="p \<bullet> TySch.All fset t" and |
92 s="(((p \<bullet> fset) \<leftrightarrow> new) + p) \<bullet> All fset t" in subst) |
95 s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst) |
|
96 apply (rule supp_perm_eq) |
|
97 apply assumption |
|
98 apply (simp only: t_tyS.perm) |
93 apply (rule a3) |
99 apply (rule a3) |
94 apply simp_all*) |
100 apply(erule_tac x="(pa + p)" in allE) |
95 sorry |
101 apply simp |
|
102 apply (simp add: eqvts eqvts_raw) |
|
103 apply (rule at_set_avoiding2) |
|
104 apply (simp add: fin_fset_to_set) |
|
105 apply (simp add: finite_supp) |
|
106 apply (simp add: eqvts finite_supp) |
|
107 apply (subst atom_eqvt_raw[symmetric]) |
|
108 apply (subst fmap_eqvt[symmetric]) |
|
109 apply (subst fset_to_set_eqvt[symmetric]) |
|
110 apply (simp only: fresh_star_permute_iff) |
|
111 apply (simp add: fresh_star_def) |
|
112 apply clarify |
|
113 apply (simp add: fresh_def) |
|
114 apply (simp add: t_tyS_supp) |
|
115 done |
96 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
116 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
97 then show ?thesis by simp |
117 then show ?thesis by simp |
98 qed |
118 qed |
99 |
119 |
100 lemma |
120 lemma |