equal
deleted
inserted
replaced
12 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *} |
12 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *} |
13 print_theorems |
13 print_theorems |
14 |
14 |
15 datatype tyS = |
15 datatype tyS = |
16 All "name set" "ty" |
16 All "name set" "ty" |
|
17 |
|
18 lemma support_image: "supp (atom ` (s :: (('a :: at) set))) = supp s" |
|
19 apply (simp add: supp_def) |
|
20 apply (simp add: eqvts eqvts_raw) |
|
21 (* apply (metis COMBC_def Collect_def Collect_mem_eq atom_name_def_raw finite finite_imageI obtain_at_base rangeI)*) |
|
22 sorry |
|
23 |
|
24 lemma atom_image_swap_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at) set); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn" |
|
25 apply (simp add: fresh_def) |
|
26 apply (simp add: support_image) |
|
27 apply (fold fresh_def) |
|
28 apply (simp add: swap_fresh_fresh) |
|
29 done |
|
30 |
|
31 lemma "\<lbrakk>a \<sharp> atom ` fun; a \<sharp> t; b \<sharp> atom ` fun; b \<sharp> t\<rbrakk> \<Longrightarrow> All ((a \<rightleftharpoons> b) \<bullet> fun) t = All fun t" |
|
32 apply (simp add: atom_image_swap_fresh) |
|
33 done |
17 |
34 |
18 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *} |
35 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *} |
19 print_theorems |
36 print_theorems |
20 |
37 |
21 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty") |
38 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty") |