Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Abs.thy
changeset 2469 4a6e78bd9de9
parent 2468 7b1470b55936
child 2471 894599a50af3
equal deleted inserted replaced
2468:7b1470b55936 2469:4a6e78bd9de9 
     6         "Quotient_List"
 
     6         "Quotient_List"
 
     7         "Quotient_Product" 
     7         "Quotient_Product" 
     8 begin
 
     8 begin
 
     9 
     9 
    10 fun
 
    10 fun
 
    11   alpha_gen 
    11   alpha_set 
    12 where
 
    12 where
 
    13   alpha_gen[simp del]:
 
    13   alpha_set[simp del]:
 
    14   "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> 
    14   "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow> 
    15      f x - bs = f y - cs \<and> 
    15      f x - bs = f y - cs \<and> 
    16      (f x - bs) \<sharp>* pi \<and> 
    16      (f x - bs) \<sharp>* pi \<and> 
    17      R (pi \<bullet> x) y \<and>
 
    17      R (pi \<bullet> x) y \<and>
 
    18      pi \<bullet> bs = cs"
 
    18      pi \<bullet> bs = cs"
 
    19 
    19 
    34      f x - set bs = f y - set cs \<and> 
    34      f x - set bs = f y - set cs \<and> 
    35      (f x - set bs) \<sharp>* pi \<and> 
    35      (f x - set bs) \<sharp>* pi \<and> 
    36      R (pi \<bullet> x) y \<and>
 
    36      R (pi \<bullet> x) y \<and>
 
    37      pi \<bullet> bs = cs"
 
    37      pi \<bullet> bs = cs"
 
    38 
    38 
    39 lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
 
    39 lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
 
    40 
    40 
    41 notation
 
    41 notation
 
    42   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
 
    42   alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and
 
    43   alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
 
    43   alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
 
    44   alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
    44   alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
    45 
    45 
    46 section {* Mono *}
 
    46 section {* Mono *}
 
    47 
    47 
    48 lemma [mono]: 
    48 lemma [mono]: 
    49   shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
 
    49   shows "R1 \<le> R2 \<Longrightarrow> alpha_set bs R1 \<le> alpha_set bs R2"
 
    50   and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
 
    50   and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
 
    51   and   "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
 
    51   and   "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
 
    52   by (case_tac [!] bs, case_tac [!] cs) 
    52   by (case_tac [!] bs, case_tac [!] cs) 
    53      (auto simp add: le_fun_def le_bool_def alphas)
 
    53      (auto simp add: le_fun_def le_bool_def alphas)
 
    54 
    54 
    55 section {* Equivariance *}
 
    55 section {* Equivariance *}
 
    56 
    56 
    57 lemma alpha_eqvt[eqvt]:
 
    57 lemma alpha_eqvt[eqvt]:
 
    58   shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
 
    58   shows "(bs, x) \<approx>set R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>set (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
 
    59   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
 
    59   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
 
    60   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
    60   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
    61   unfolding alphas
 
    61   unfolding alphas
 
    62   unfolding permute_eqvt[symmetric]
 
    62   unfolding permute_eqvt[symmetric]
 
    63   unfolding set_eqvt[symmetric]
 
    63   unfolding set_eqvt[symmetric]
 
    68 
    68 
    69 section {* Equivalence *}
 
    69 section {* Equivalence *}
 
    70 
    70 
    71 lemma alpha_refl:
 
    71 lemma alpha_refl:
 
    72   assumes a: "R x x"
 
    72   assumes a: "R x x"
 
    73   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
 
    73   shows "(bs, x) \<approx>set R f 0 (bs, x)"
 
    74   and   "(bs, x) \<approx>res R f 0 (bs, x)"
 
    74   and   "(bs, x) \<approx>res R f 0 (bs, x)"
 
    75   and   "(cs, x) \<approx>lst R f 0 (cs, x)"
 
    75   and   "(cs, x) \<approx>lst R f 0 (cs, x)"
 
    76   using a 
    76   using a 
    77   unfolding alphas
 
    77   unfolding alphas
 
    78   unfolding fresh_star_def
 
    78   unfolding fresh_star_def
 
    79   by (simp_all add: fresh_zero_perm)
 
    79   by (simp_all add: fresh_zero_perm)
 
    80 
    80 
    81 lemma alpha_sym:
 
    81 lemma alpha_sym:
 
    82   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
 
    82   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
 
    83   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
 
    83   shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
 
    84   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
 
    84   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
 
    85   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
 
    85   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
 
    86   unfolding alphas fresh_star_def
 
    86   unfolding alphas fresh_star_def
 
    87   using a
 
    87   using a
 
    88   by (auto simp add:  fresh_minus_perm)
 
    88   by (auto simp add:  fresh_minus_perm)
 
    89 
    89 
    90 lemma alpha_trans:
 
    90 lemma alpha_trans:
 
    91   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
 
    91   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
 
    92   shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
 
    92   shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)"
 
    93   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
 
    93   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
 
    94   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
 
    94   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
 
    95   using a
 
    95   using a
 
    96   unfolding alphas fresh_star_def
 
    96   unfolding alphas fresh_star_def
 
    97   by (simp_all add: fresh_plus_perm)
 
    97   by (simp_all add: fresh_plus_perm)
 
    98 
    98 
    99 lemma alpha_sym_eqvt:
 
    99 lemma alpha_sym_eqvt:
 
   100   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 
   100   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 
   101   and     b: "p \<bullet> R = R"
 
   101   and     b: "p \<bullet> R = R"
 
   102   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" 
   102   shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)" 
   103   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" 
   103   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" 
   104   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
 
   104   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
 
   105 apply(auto intro!: alpha_sym)
 
   105 apply(auto intro!: alpha_sym)
 
   106 apply(drule_tac [!] a)
 
   106 apply(drule_tac [!] a)
 
   107 apply(rule_tac [!] p="p" in permute_boolE)
 
   107 apply(rule_tac [!] p="p" in permute_boolE)
 
   111 apply(assumption)
 
   111 apply(assumption)
 
   112 apply(perm_simp add: permute_minus_cancel b)
 
   112 apply(perm_simp add: permute_minus_cancel b)
 
   113 apply(assumption)
 
   113 apply(assumption)
 
   114 done
 
   114 done
 
   115 
   115 
   116 lemma alpha_gen_trans_eqvt:
 
   116 lemma alpha_set_trans_eqvt:
 
   117   assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
 
   117   assumes b: "(cs, y) \<approx>set R f q (ds, z)"
 
   118   and     a: "(bs, x) \<approx>gen R f p (cs, y)" 
   118   and     a: "(bs, x) \<approx>set R f p (cs, y)" 
   119   and     d: "q \<bullet> R = R"
 
   119   and     d: "q \<bullet> R = R"
 
   120   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
 
   120   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
 
   121   shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
 
   121   shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
 
   122 apply(rule alpha_trans)
 
   122 apply(rule alpha_trans)
 
   123 defer
 
   123 defer
 
   124 apply(rule a)
 
   124 apply(rule a)
 
   125 apply(rule b)
 
   125 apply(rule b)
 
   126 apply(drule c)
 
   126 apply(drule c)
 
   171 apply(drule_tac p="q" in permute_boolI)
 
   171 apply(drule_tac p="q" in permute_boolI)
 
   172 apply(perm_simp add: permute_minus_cancel d)
 
   172 apply(perm_simp add: permute_minus_cancel d)
 
   173 apply(simp add: permute_eqvt[symmetric])
 
   173 apply(simp add: permute_eqvt[symmetric])
 
   174 done
 
   174 done
 
   175 
   175 
   176 lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
   176 lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
   177 
   177 
   178 
   178 
   179 section {* General Abstractions *}
 
   179 section {* General Abstractions *}
 
   180 
   180 
   181 fun
 
   181 fun
 
   182   alpha_abs 
   182   alpha_abs_set 
   183 where
 
   183 where
 
   184   [simp del]:
 
   184   [simp del]:
 
   185   "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
   185   "alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
 
   186 
   186 
   187 fun
 
   187 fun
 
   188   alpha_abs_lst
 
   188   alpha_abs_lst
 
   189 where
 
   189 where
 
   190   [simp del]:
 
   190   [simp del]:
 
   195 where
 
   195 where
 
   196   [simp del]:
 
   196   [simp del]:
 
   197   "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
 
   197   "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
 
   198 
   198 
   199 notation
 
   199 notation
 
   200   alpha_abs (infix "\<approx>abs" 50) and
 
   200   alpha_abs_set (infix "\<approx>abs'_set" 50) and
 
   201   alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
 
   201   alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
 
   202   alpha_abs_res (infix "\<approx>abs'_res" 50)
 
   202   alpha_abs_res (infix "\<approx>abs'_res" 50)
 
   203 
   203 
   204 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
 
   204 lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
 
   205 
   205 
   206 
   206 
   207 lemma alphas_abs_refl:
 
   207 lemma alphas_abs_refl:
 
   208   shows "(bs, x) \<approx>abs (bs, x)"
 
   208   shows "(bs, x) \<approx>abs_set (bs, x)"
 
   209   and   "(bs, x) \<approx>abs_res (bs, x)"
 
   209   and   "(bs, x) \<approx>abs_res (bs, x)"
 
   210   and   "(cs, x) \<approx>abs_lst (cs, x)" 
   210   and   "(cs, x) \<approx>abs_lst (cs, x)" 
   211   unfolding alphas_abs
 
   211   unfolding alphas_abs
 
   212   unfolding alphas
 
   212   unfolding alphas
 
   213   unfolding fresh_star_def
 
   213   unfolding fresh_star_def
 
   214   by (rule_tac [!] x="0" in exI)
 
   214   by (rule_tac [!] x="0" in exI)
 
   215      (simp_all add: fresh_zero_perm)
 
   215      (simp_all add: fresh_zero_perm)
 
   216 
   216 
   217 lemma alphas_abs_sym:
 
   217 lemma alphas_abs_sym:
 
   218   shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (bs, x)"
 
   218   shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"
 
   219   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
 
   219   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
 
   220   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
 
   220   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
 
   221   unfolding alphas_abs
 
   221   unfolding alphas_abs
 
   222   unfolding alphas
 
   222   unfolding alphas
 
   223   unfolding fresh_star_def
 
   223   unfolding fresh_star_def
 
   224   by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
 
   224   by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
 
   225      (auto simp add: fresh_minus_perm)
 
   225      (auto simp add: fresh_minus_perm)
 
   226 
   226 
   227 lemma alphas_abs_trans:
 
   227 lemma alphas_abs_trans:
 
   228   shows "\<lbrakk>(bs, x) \<approx>abs (cs, y); (cs, y) \<approx>abs (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs (ds, z)"
 
   228   shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"
 
   229   and   "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"
 
   229   and   "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"
 
   230   and   "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"
 
   230   and   "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"
 
   231   unfolding alphas_abs
 
   231   unfolding alphas_abs
 
   232   unfolding alphas
 
   232   unfolding alphas
 
   233   unfolding fresh_star_def
 
   233   unfolding fresh_star_def
 
   234   apply(erule_tac [!] exE, erule_tac [!] exE)
 
   234   apply(erule_tac [!] exE, erule_tac [!] exE)
 
   235   apply(rule_tac [!] x="pa + p" in exI)
 
   235   apply(rule_tac [!] x="pa + p" in exI)
 
   236   by (simp_all add: fresh_plus_perm)
 
   236   by (simp_all add: fresh_plus_perm)
 
   237 
   237 
   238 lemma alphas_abs_eqvt:
 
   238 lemma alphas_abs_eqvt:
 
   239   shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs (p \<bullet> cs, p \<bullet> y)"
 
   239   shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_set (p \<bullet> cs, p \<bullet> y)"
 
   240   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
 
   240   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
 
   241   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
 
   241   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
 
   242   unfolding alphas_abs
 
   242   unfolding alphas_abs
 
   243   unfolding alphas
 
   243   unfolding alphas
 
   244   unfolding set_eqvt[symmetric]
 
   244   unfolding set_eqvt[symmetric]
 
   247   apply(erule_tac [!] exE)
 
   247   apply(erule_tac [!] exE)
 
   248   apply(rule_tac [!] x="p \<bullet> pa" in exI)
 
   248   apply(rule_tac [!] x="p \<bullet> pa" in exI)
 
   249   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
   249   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
   250 
   250 
   251 quotient_type 
   251 quotient_type 
   252     'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
 
   252     'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
 
   253 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
 
   253 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
 
   254 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
 
   254 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
 
   255   apply(rule_tac [!] equivpI)
 
   255   apply(rule_tac [!] equivpI)
 
   256   unfolding reflp_def symp_def transp_def
 
   256   unfolding reflp_def symp_def transp_def
 
   257   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
   257   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
   258 
   258 
   259 quotient_definition
 
   259 quotient_definition
 
   260   Abs ("[_]set. _" [60, 60] 60)
 
   260   Abs_set ("[_]set. _" [60, 60] 60)
 
   261 where
 
   261 where
 
   262   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
 
   262   "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
 
   263 is
 
   263 is
 
   264   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
   264   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
   265 
   265 
   266 quotient_definition
 
   266 quotient_definition
 
   267   Abs_res ("[_]res. _" [60, 60] 60)
 
   267   Abs_res ("[_]res. _" [60, 60] 60)
 
   276   "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
 
   276   "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
 
   277 is
 
   277 is
 
   278   "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
 
   278   "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
 
   279 
   279 
   280 lemma [quot_respect]:
 
   280 lemma [quot_respect]:
 
   281   shows "(op= ===> op= ===> alpha_abs) Pair Pair"
 
   281   shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
 
   282   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
 
   282   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
 
   283   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
 
   283   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
 
   284   unfolding fun_rel_def
 
   284   unfolding fun_rel_def
 
   285   by (auto intro: alphas_abs_refl)
 
   285   by (auto intro: alphas_abs_refl)
 
   286 
   286 
   287 lemma [quot_respect]:
 
   287 lemma [quot_respect]:
 
   288   shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
 
   288   shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
 
   289   and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
 
   289   and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
 
   290   and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
 
   290   and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
 
   291   unfolding fun_rel_def
 
   291   unfolding fun_rel_def
 
   292   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
   292   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
   293 
   293 
   294 lemma abs_exhausts:
 
   294 lemma abs_exhausts:
 
   295   shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
 
   295   shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
 
   296   and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
 
   296   and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
 
   297   and   "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
 
   297   and   "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
 
   298   by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
 
   298   by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
 
   299               prod.exhaust[where 'a="atom set" and 'b="'a"]
 
   299               prod.exhaust[where 'a="atom set" and 'b="'a"]
 
   300               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
   300               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
   301 
   301 
   302 lemma abs_eq_iff:
 
   302 lemma abs_eq_iff:
 
   303   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
 
   303   shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (cs, y)"
 
   304   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
 
   304   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
 
   305   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
 
   305   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
 
   306   unfolding alphas_abs by (lifting alphas_abs)
 
   306   unfolding alphas_abs by (lifting alphas_abs)
 
   307 
   307 
   308 instantiation abs_gen :: (pt) pt
 
   308 instantiation abs_set :: (pt) pt
 
   309 begin
 
   309 begin
 
   310 
   310 
   311 quotient_definition
 
   311 quotient_definition
 
   312   "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
 
   312   "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
 
   313 is
 
   313 is
 
   314   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
   314   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
   315 
   315 
   316 lemma permute_Abs[simp]:
 
   316 lemma permute_Abs[simp]:
 
   317   fixes x::"'a::pt"  
   317   fixes x::"'a::pt"  
   318   shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
 
   318   shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
 
   319   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
   319   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
   320 
   320 
   321 instance
 
   321 instance
 
   322   apply(default)
 
   322   apply(default)
 
   323   apply(case_tac [!] x rule: abs_exhausts(1))
 
   323   apply(case_tac [!] x rule: abs_exhausts(1))
 
   372 
   372 
   373 
   373 
   374 lemma abs_swap1:
 
   374 lemma abs_swap1:
 
   375   assumes a1: "a \<notin> (supp x) - bs"
 
   375   assumes a1: "a \<notin> (supp x) - bs"
 
   376   and     a2: "b \<notin> (supp x) - bs"
 
   376   and     a2: "b \<notin> (supp x) - bs"
 
   377   shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
 
   377   shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
 
   378   and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
 
   378   and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
 
   379   unfolding abs_eq_iff
 
   379   unfolding abs_eq_iff
 
   380   unfolding alphas_abs
 
   380   unfolding alphas_abs
 
   381   unfolding alphas
 
   381   unfolding alphas
 
   382   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
   382   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
   399   using a1 a2
 
   399   using a1 a2
 
   400   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
 
   400   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
 
   401      (auto simp add: supp_perm swap_atom)
 
   401      (auto simp add: supp_perm swap_atom)
 
   402 
   402 
   403 lemma abs_supports:
 
   403 lemma abs_supports:
 
   404   shows "((supp x) - as) supports (Abs as x)"
 
   404   shows "((supp x) - as) supports (Abs_set as x)"
 
   405   and   "((supp x) - as) supports (Abs_res as x)"
 
   405   and   "((supp x) - as) supports (Abs_res as x)"
 
   406   and   "((supp x) - set bs) supports (Abs_lst bs x)"
 
   406   and   "((supp x) - set bs) supports (Abs_lst bs x)"
 
   407   unfolding supports_def
 
   407   unfolding supports_def
 
   408   unfolding permute_abs
 
   408   unfolding permute_abs
 
   409   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
   409   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
   410 
   410 
   411 function
 
   411 function
 
   412   supp_gen  :: "('a::pt) abs_gen \<Rightarrow> atom set"
 
   412   supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set"
 
   413 where
 
   413 where
 
   414   "supp_gen (Abs as x) = supp x - as"
 
   414   "supp_set (Abs_set as x) = supp x - as"
 
   415 apply(case_tac x rule: abs_exhausts(1))
 
   415 apply(case_tac x rule: abs_exhausts(1))
 
   416 apply(simp)
 
   416 apply(simp)
 
   417 apply(simp add: abs_eq_iff alphas_abs alphas)
 
   417 apply(simp add: abs_eq_iff alphas_abs alphas)
 
   418 done
 
   418 done
 
   419 
   419 
   420 termination supp_gen 
   420 termination supp_set 
   421   by (auto intro!: local.termination)
 
   421   by (auto intro!: local.termination)
 
   422 
   422 
   423 function
 
   423 function
 
   424   supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
 
   424   supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
 
   425 where
 
   425 where
 
   443 
   443 
   444 termination supp_lst 
   444 termination supp_lst 
   445   by (auto intro!: local.termination)
 
   445   by (auto intro!: local.termination)
 
   446 
   446 
   447 lemma [eqvt]:
 
   447 lemma [eqvt]:
 
   448   shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
 
   448   shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
 
   449   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
 
   449   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
 
   450   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
 
   450   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
 
   451   apply(case_tac x rule: abs_exhausts(1))
 
   451   apply(case_tac x rule: abs_exhausts(1))
 
   452   apply(simp add: supp_eqvt Diff_eqvt)
 
   452   apply(simp add: supp_eqvt Diff_eqvt)
 
   453   apply(case_tac y rule: abs_exhausts(2))
 
   453   apply(case_tac y rule: abs_exhausts(2))
 
   455   apply(case_tac z rule: abs_exhausts(3))
 
   455   apply(case_tac z rule: abs_exhausts(3))
 
   456   apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
 
   456   apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
 
   457   done
 
   457   done
 
   458 
   458 
   459 lemma aux_fresh:
 
   459 lemma aux_fresh:
 
   460   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
 
   460   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"
 
   461   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
 
   461   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
 
   462   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
 
   462   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
 
   463   by (rule_tac [!] fresh_fun_eqvt_app)
 
   463   by (rule_tac [!] fresh_fun_eqvt_app)
 
   464      (simp_all only: eqvts_raw)
 
   464      (simp_all only: eqvts_raw)
 
   465 
   465 
   466 lemma supp_abs_subset1:
 
   466 lemma supp_abs_subset1:
 
   467   assumes a: "finite (supp x)"
 
   467   assumes a: "finite (supp x)"
 
   468   shows "(supp x) - as \<subseteq> supp (Abs as x)"
 
   468   shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
 
   469   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
 
   469   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
 
   470   and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
 
   470   and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
 
   471   unfolding supp_conv_fresh
 
   471   unfolding supp_conv_fresh
 
   472   by (auto dest!: aux_fresh)
 
   472   by (auto dest!: aux_fresh)
 
   473      (simp_all add: fresh_def supp_finite_atom_set a)
 
   473      (simp_all add: fresh_def supp_finite_atom_set a)
 
   474 
   474 
   475 lemma supp_abs_subset2:
 
   475 lemma supp_abs_subset2:
 
   476   assumes a: "finite (supp x)"
 
   476   assumes a: "finite (supp x)"
 
   477   shows "supp (Abs as x) \<subseteq> (supp x) - as"
 
   477   shows "supp (Abs_set as x) \<subseteq> (supp x) - as"
 
   478   and   "supp (Abs_res as x) \<subseteq> (supp x) - as"
 
   478   and   "supp (Abs_res as x) \<subseteq> (supp x) - as"
 
   479   and   "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
 
   479   and   "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
 
   480   by (rule_tac [!] supp_is_subset)
 
   480   by (rule_tac [!] supp_is_subset)
 
   481      (simp_all add: abs_supports a)
 
   481      (simp_all add: abs_supports a)
 
   482 
   482 
   483 lemma abs_finite_supp:
 
   483 lemma abs_finite_supp:
 
   484   assumes a: "finite (supp x)"
 
   484   assumes a: "finite (supp x)"
 
   485   shows "supp (Abs as x) = (supp x) - as"
 
   485   shows "supp (Abs_set as x) = (supp x) - as"
 
   486   and   "supp (Abs_res as x) = (supp x) - as"
 
   486   and   "supp (Abs_res as x) = (supp x) - as"
 
   487   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
 
   487   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
 
   488   by (rule_tac [!] subset_antisym)
 
   488   by (rule_tac [!] subset_antisym)
 
   489      (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
 
   489      (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
 
   490 
   490 
   491 lemma supp_abs:
 
   491 lemma supp_abs:
 
   492   fixes x::"'a::fs"
 
   492   fixes x::"'a::fs"
 
   493   shows "supp (Abs as x) = (supp x) - as"
 
   493   shows "supp (Abs_set as x) = (supp x) - as"
 
   494   and   "supp (Abs_res as x) = (supp x) - as"
 
   494   and   "supp (Abs_res as x) = (supp x) - as"
 
   495   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
 
   495   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
 
   496   by (rule_tac [!] abs_finite_supp)
 
   496   by (rule_tac [!] abs_finite_supp)
 
   497      (simp_all add: finite_supp)
 
   497      (simp_all add: finite_supp)
 
   498 
   498 
   499 instance abs_gen :: (fs) fs
 
   499 instance abs_set :: (fs) fs
 
   500   apply(default)
 
   500   apply(default)
 
   501   apply(case_tac x rule: abs_exhausts(1))
 
   501   apply(case_tac x rule: abs_exhausts(1))
 
   502   apply(simp add: supp_abs finite_supp)
 
   502   apply(simp add: supp_abs finite_supp)
 
   503   done
 
   503   done
 
   504 
   504 
   514   apply(simp add: supp_abs finite_supp)
 
   514   apply(simp add: supp_abs finite_supp)
 
   515   done
 
   515   done
 
   516 
   516 
   517 lemma abs_fresh_iff:
 
   517 lemma abs_fresh_iff:
 
   518   fixes x::"'a::fs"
 
   518   fixes x::"'a::fs"
 
   519   shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
 
   519   shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
 
   520   and   "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
 
   520   and   "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
 
   521   and   "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
 
   521   and   "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
 
   522   unfolding fresh_def
 
   522   unfolding fresh_def
 
   523   unfolding supp_abs
 
   523   unfolding supp_abs
 
   524   by auto
 
   524   by auto
 
   525 
   525 
   526 lemma Abs_eq_iff:
 
   526 lemma Abs_eq_iff:
 
   527   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
 
   527   shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
 
   528   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
 
   528   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
 
   529   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
 
   529   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
 
   530   by (lifting alphas_abs)
 
   530   by (lifting alphas_abs)
 
   531 
   531 
   532 
   532
nominal2