equal
deleted
inserted
replaced
68 "f PN = {}" |
68 "f PN = {}" |
69 | "f (PS x) = {atom x}" |
69 | "f (PS x) = {atom x}" |
70 | "f (PD x y) = {atom x, atom y}" |
70 | "f (PD x y) = {atom x, atom y}" |
71 |
71 |
72 (* compat should be |
72 (* compat should be |
73 compat (PN) pi (PN) \<equiv> TRue |
73 compat (PN) pi (PN) == True |
74 compat (PS x) pi (PS x') \<equiv> pi o x = x' |
74 compat (PS x) pi (PS x') == pi o x = x' |
75 compat (PD p1 p2) pi (PD p1' p2') \<equiv> compat p1 pi p1' \<and> compat p2 pi p2' |
75 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
76 *) |
76 *) |
77 |
77 |
78 |
78 |
79 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
79 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
80 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
80 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
158 bv2 |
158 bv2 |
159 where |
159 where |
160 "bv2 (As x t) = {atom x}" |
160 "bv2 (As x t) = {atom x}" |
161 |
161 |
162 (* compat should be |
162 (* compat should be |
163 compat (As x t) pi (As x' t') \<equiv> pi o x = x' \<and> alpha t t' |
163 compat (As x t) pi (As x' t') == pi o x = x' & alpha t t' |
164 *) |
164 *) |
165 |
165 |
166 |
166 |
167 thm fv_trm2_raw_fv_assign_raw.simps[no_vars] |
167 thm fv_trm2_raw_fv_assign_raw.simps[no_vars] |
168 thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars] |
168 thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars] |
401 binder |
401 binder |
402 bv :: "pat \<Rightarrow> atom set" |
402 bv :: "pat \<Rightarrow> atom set" |
403 where |
403 where |
404 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
404 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
405 |
405 |
|
406 (* |
|
407 compat (K s ts vs) pi (K s' ts' vs') == |
|
408 s = s' & |
|
409 |
|
410 *) |
|
411 |
|
412 |
406 (*thm bv_raw.simps*) |
413 (*thm bv_raw.simps*) |
407 |
414 |
408 (* example 3 from Peter Sewell's bestiary *) |
415 (* example 3 from Peter Sewell's bestiary *) |
409 nominal_datatype exp = |
416 nominal_datatype exp = |
410 VarP "name" |
417 VarP "name" |