15 type_synonym |
15 type_synonym |
16 'x prm = "('x \<times> 'x) list" |
16 'x prm = "('x \<times> 'x) list" |
17 |
17 |
18 (* polymorphic constants for permutation and swapping *) |
18 (* polymorphic constants for permutation and swapping *) |
19 consts |
19 consts |
20 perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80) |
20 perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr \<open>\<bullet>\<close> 80) |
21 swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" |
21 swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" |
22 |
22 |
23 (* a "private" copy of the option type used in the abstraction function *) |
23 (* a "private" copy of the option type used in the abstraction function *) |
24 datatype 'a noption = nSome 'a | nNone |
24 datatype 'a noption = nSome 'a | nNone |
25 |
25 |
185 |
185 |
186 |
186 |
187 section \<open>permutation equality\<close> |
187 section \<open>permutation equality\<close> |
188 (*==============================*) |
188 (*==============================*) |
189 |
189 |
190 definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) where |
190 definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (\<open> _ \<triangleq> _ \<close> [80,80] 80) where |
191 "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)" |
191 "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)" |
192 |
192 |
193 section \<open>Support, Freshness and Supports\<close> |
193 section \<open>Support, Freshness and Supports\<close> |
194 (*========================================*) |
194 (*========================================*) |
195 definition supp :: "'a \<Rightarrow> ('x set)" where |
195 definition supp :: "'a \<Rightarrow> ('x set)" where |
196 "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}" |
196 "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}" |
197 |
197 |
198 definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) where |
198 definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" (\<open>_ \<sharp> _\<close> [80,80] 80) where |
199 "a \<sharp> x \<longleftrightarrow> a \<notin> supp x" |
199 "a \<sharp> x \<longleftrightarrow> a \<notin> supp x" |
200 |
200 |
201 definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) where |
201 definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl \<open>supports\<close> 80) where |
202 "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))" |
202 "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))" |
203 |
203 |
204 (* lemmas about supp *) |
204 (* lemmas about supp *) |
205 lemma supp_fresh_iff: |
205 lemma supp_fresh_iff: |
206 fixes x :: "'a" |
206 fixes x :: "'a" |
384 shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x" |
384 shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x" |
385 and "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y" |
385 and "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y" |
386 by (simp_all add: fresh_prod) |
386 by (simp_all add: fresh_prod) |
387 |
387 |
388 ML \<open> |
388 ML \<open> |
389 val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs; |
389 val mksimps_pairs = (\<^const_name>\<open>Nominal.fresh\<close>, @{thms fresh_prodD}) :: mksimps_pairs; |
390 \<close> |
390 \<close> |
391 declaration \<open>fn _ => |
391 declaration \<open>fn _ => |
392 Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs)) |
392 Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs)) |
393 \<close> |
393 \<close> |
394 |
394 |
2412 |
2412 |
2413 section \<open>generalisation of freshness to lists and sets of atoms\<close> |
2413 section \<open>generalisation of freshness to lists and sets of atoms\<close> |
2414 (*================================================================*) |
2414 (*================================================================*) |
2415 |
2415 |
2416 consts |
2416 consts |
2417 fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100) |
2417 fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>_ \<sharp>* _\<close> [100,100] 100) |
2418 |
2418 |
2419 overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool" |
2419 overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool" |
2420 begin |
2420 begin |
2421 definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)" |
2421 definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)" |
2422 end |
2422 end |
2949 assumes pt: "pt TYPE('a) TYPE('x)" |
2949 assumes pt: "pt TYPE('a) TYPE('x)" |
2950 and at: "at TYPE('x)" |
2950 and at: "at TYPE('x)" |
2951 shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)" |
2951 shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)" |
2952 by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at]) |
2952 by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at]) |
2953 |
2953 |
2954 definition abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" ("[_]._" [100,100] 100) where |
2954 definition abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" (\<open>[_]._\<close> [100,100] 100) where |
2955 "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))" |
2955 "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))" |
2956 |
2956 |
2957 (* FIXME: should be called perm_if and placed close to the definition of permutations on bools *) |
2957 (* FIXME: should be called perm_if and placed close to the definition of permutations on bools *) |
2958 lemma abs_fun_if: |
2958 lemma abs_fun_if: |
2959 fixes pi :: "'x prm" |
2959 fixes pi :: "'x prm" |
3383 where |
3383 where |
3384 ABS_in: "(abs_fun a x)\<in>ABS_set" |
3384 ABS_in: "(abs_fun a x)\<in>ABS_set" |
3385 |
3385 |
3386 definition "ABS = ABS_set" |
3386 definition "ABS = ABS_set" |
3387 |
3387 |
3388 typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) = |
3388 typedef ('x, 'a) ABS (\<open>\<guillemotleft>_\<guillemotright>_\<close> [1000,1000] 1000) = |
3389 "ABS::('x\<Rightarrow>('a noption)) set" |
3389 "ABS::('x\<Rightarrow>('a noption)) set" |
3390 morphisms Rep_ABS Abs_ABS |
3390 morphisms Rep_ABS Abs_ABS |
3391 unfolding ABS_def |
3391 unfolding ABS_def |
3392 proof |
3392 proof |
3393 fix x::"'a" and a::"'x" |
3393 fix x::"'a" and a::"'x" |