26 thm ty_tys.size_eqvt |
26 thm ty_tys.size_eqvt |
27 thm ty_tys.supports |
27 thm ty_tys.supports |
28 thm ty_tys.supp |
28 thm ty_tys.supp |
29 thm ty_tys.fresh |
29 thm ty_tys.fresh |
30 |
30 |
|
31 fun |
|
32 lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty" |
|
33 where |
|
34 "lookup [] Y = Var Y" |
|
35 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)" |
|
36 |
|
37 lemma lookup_eqvt[eqvt]: |
|
38 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
|
39 apply(induct Ts T rule: lookup.induct) |
|
40 apply(simp_all) |
|
41 done |
|
42 |
|
43 nominal_primrec |
|
44 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
|
45 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
|
46 where |
|
47 "subst \<theta> (Var X) = lookup \<theta> X" |
|
48 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
|
49 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
50 term subst_substs_sumC |
|
51 term Inl |
|
52 thm subst_substs_graph.induct |
|
53 thm subst_substs_graph.intros |
|
54 thm Projl.simps |
|
55 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
|
56 apply(simp add: eqvt_def) |
|
57 apply(rule allI) |
|
58 apply(simp add: permute_fun_def permute_bool_def) |
|
59 apply(rule ext) |
|
60 apply(rule ext) |
|
61 apply(rule iffI) |
|
62 apply(drule_tac x="p" in meta_spec) |
|
63 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
64 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
65 apply(simp) |
|
66 apply(drule_tac x="-p" in meta_spec) |
|
67 apply(drule_tac x="x" in meta_spec) |
|
68 apply(drule_tac x="xa" in meta_spec) |
|
69 apply(simp) |
|
70 thm subst_substs_graph.induct |
|
71 thm subst_substs_graph.intros |
|
72 thm Projl.simps |
|
73 apply(erule subst_substs_graph.induct) |
|
74 apply(perm_simp) |
|
75 apply(rule subst_substs_graph.intros) |
|
76 apply(simp only: eqvts) |
|
77 thm Projl.simps |
|
78 term Inl |
|
79 term Inr |
|
80 apply(perm_simp) |
|
81 thm subst_substs_graph.intros |
|
82 thm Projl.simps |
|
83 oops |
|
84 |
31 |
85 |
32 section {* defined as two separate nominal datatypes *} |
86 section {* defined as two separate nominal datatypes *} |
33 |
87 |
34 nominal_datatype ty2 = |
88 nominal_datatype ty2 = |
35 Var2 "name" |
89 Var2 "name" |
50 thm tys2.supports |
104 thm tys2.supports |
51 thm tys2.supp |
105 thm tys2.supp |
52 thm tys2.fresh |
106 thm tys2.fresh |
53 |
107 |
54 fun |
108 fun |
55 lookup :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2" |
109 lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2" |
56 where |
110 where |
57 "lookup [] Y = Var2 Y" |
111 "lookup2 [] Y = Var2 Y" |
58 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)" |
112 | "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)" |
59 |
113 |
60 lemma lookup_eqvt[eqvt]: |
114 lemma lookup2_eqvt[eqvt]: |
61 shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)" |
115 shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)" |
62 apply(induct Ts T rule: lookup.induct) |
116 apply(induct Ts T rule: lookup2.induct) |
63 apply(simp_all) |
117 apply(simp_all) |
64 done |
118 done |
65 |
119 |
66 function |
120 nominal_primrec |
67 subst :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2" |
121 subst :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2" |
68 where |
122 where |
69 "subst \<theta> (Var2 X) = lookup \<theta> X" |
123 "subst \<theta> (Var2 X) = lookup2 \<theta> X" |
70 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)" |
124 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)" |
|
125 defer |
71 apply(case_tac x) |
126 apply(case_tac x) |
72 apply(simp) |
127 apply(simp) |
73 apply(rule_tac y="b" in ty2.exhaust) |
128 apply(rule_tac y="b" in ty2.exhaust) |
74 apply(blast) |
129 apply(blast) |
75 apply(blast) |
130 apply(blast) |
76 apply(simp_all add: ty2.distinct) |
131 apply(simp_all add: ty2.distinct) |
77 apply(simp add: ty2.eq_iff) |
132 apply(simp add: ty2.eq_iff) |
78 apply(simp add: ty2.eq_iff) |
133 apply(simp add: ty2.eq_iff) |
|
134 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
|
135 apply(simp add: eqvt_def) |
|
136 apply(rule allI) |
|
137 apply(simp add: permute_fun_def permute_bool_def) |
|
138 apply(rule ext) |
|
139 apply(rule ext) |
|
140 apply(rule iffI) |
|
141 apply(drule_tac x="p" in meta_spec) |
|
142 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
143 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
144 apply(simp) |
|
145 apply(drule_tac x="-p" in meta_spec) |
|
146 apply(drule_tac x="x" in meta_spec) |
|
147 apply(drule_tac x="xa" in meta_spec) |
|
148 apply(simp) |
|
149 apply(erule subst_graph.induct) |
|
150 apply(perm_simp) |
|
151 apply(rule subst_graph.intros) |
|
152 apply(perm_simp) |
|
153 apply(rule subst_graph.intros) |
|
154 apply(assumption) |
|
155 apply(assumption) |
79 done |
156 done |
80 |
157 |
81 termination |
158 termination |
82 apply(relation "measure (size o snd)") |
159 apply(relation "measure (size o snd)") |
83 apply(simp_all add: ty2.size) |
160 apply(simp_all add: ty2.size) |
84 done |
161 done |
85 |
162 |
86 lemma subst_eqvt[eqvt]: |
163 lemma subst_eqvt[eqvt]: |
87 shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)" |
164 shows "(p \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)" |
88 apply(induct \<theta> T rule: subst.induct) |
165 apply(induct \<theta> T rule: subst.induct) |
89 apply(simp_all add: lookup_eqvt) |
166 apply(simp_all add: lookup2_eqvt) |
90 done |
167 done |
91 |
168 |
92 lemma j: |
169 lemma j: |
93 assumes "a \<sharp> Ts" " a \<sharp> X" |
170 assumes "a \<sharp> Ts" " a \<sharp> X" |
94 shows "a \<sharp> lookup Ts X" |
171 shows "a \<sharp> lookup2 Ts X" |
95 using assms |
172 using assms |
96 apply(induct Ts X rule: lookup.induct) |
173 apply(induct Ts X rule: lookup2.induct) |
97 apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair) |
174 apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair) |
98 done |
175 done |
99 |
176 |
100 lemma i: |
177 lemma i: |
101 assumes "a \<sharp> t" " a \<sharp> \<theta>" |
178 assumes "a \<sharp> t" " a \<sharp> \<theta>" |