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 2385 fe25a3ffeb14
parent 2324 9038c9549073
child 2402 80db544a37ea
equal deleted inserted replaced
2384:841b7e34e70a 2385:fe25a3ffeb14 
    41 notation
 
    41 notation
 
    42   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
 
    42   alpha_gen ("_ \<approx>gen _ _ _ _" [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 (* monos *)
 
    46 section {* Mono *}
 
       
    47 
    47 lemma [mono]: 
    48 lemma [mono]: 
    48   shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
 
    49   shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
 
    49   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"
 
    50   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"
 
    51   by (case_tac [!] bs, case_tac [!] cs) 
    52   by (case_tac [!] bs, case_tac [!] cs) 
    52      (auto simp add: le_fun_def le_bool_def alphas)
 
    53      (auto simp add: le_fun_def le_bool_def alphas)
 
    53 
    54 
    54 (* equivariance *)
 
    55 section {* Equivariance *}
 
    55 lemma alpha_gen_eqvt[eqvt]:
 
    56 
       
    57 lemma alpha_eqvt[eqvt]:
 
    56   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>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)"
 
    57   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)"
 
    58   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)" 
    59   unfolding alphas
 
    61   unfolding alphas
 
    60   unfolding permute_eqvt[symmetric]
 
    62   unfolding permute_eqvt[symmetric]
 
    61   unfolding set_eqvt[symmetric]
 
    63   unfolding set_eqvt[symmetric]
 
    62   unfolding permute_fun_app_eq[symmetric]
 
    64   unfolding permute_fun_app_eq[symmetric]
 
    63   unfolding Diff_eqvt[symmetric]
 
    65   unfolding Diff_eqvt[symmetric]
 
    64   by (auto simp add: permute_bool_def fresh_star_permute_iff)
 
    66   by (auto simp add: permute_bool_def fresh_star_permute_iff)
 
    65 
    67 
    66 (* equivalence *)
 
    68 
    67 lemma alpha_gen_refl:
 
    69 section {* Equivalence *}
 
       
    70 
       
    71 lemma alpha_refl:
 
    68   assumes a: "R x x"
 
    72   assumes a: "R x x"
 
    69   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
 
    73   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
 
    70   and   "(bs, x) \<approx>res R f 0 (bs, x)"
 
    74   and   "(bs, x) \<approx>res R f 0 (bs, x)"
 
    71   and   "(cs, x) \<approx>lst R f 0 (cs, x)"
 
    75   and   "(cs, x) \<approx>lst R f 0 (cs, x)"
 
    72   using a 
    76   using a 
    73   unfolding alphas
 
    77   unfolding alphas
 
    74   unfolding fresh_star_def
 
    78   unfolding fresh_star_def
 
    75   by (simp_all add: fresh_zero_perm)
 
    79   by (simp_all add: fresh_zero_perm)
 
    76 
    80 
    77 lemma alpha_gen_sym:
 
    81 lemma alpha_sym:
 
    78   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"
 
    79   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>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
 
    80   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)"
 
    81   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)"
 
    82   unfolding alphas fresh_star_def
 
    86   unfolding alphas fresh_star_def
 
    83   using a
 
    87   using a
 
    84   by (auto simp add:  fresh_minus_perm)
 
    88   by (auto simp add:  fresh_minus_perm)
 
    85 
    89 
    86 lemma alpha_gen_sym_eqvt:
 
    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"
 
       
    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)"
 
       
    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)"
 
       
    95   using a
 
       
    96   unfolding alphas fresh_star_def
 
       
    97   by (simp_all add: fresh_plus_perm)
 
       
    98 
       
    99 lemma alpha_sym_eqvt:
 
    87   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)" 
    88   and     b: "p \<bullet> R = R"
 
   101   and     b: "p \<bullet> R = R"
 
    89   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>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" 
    90   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)" 
    91   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)"
 
    92 apply(auto intro!: alpha_gen_sym)
 
   105 apply(auto intro!: alpha_sym)
 
    93 apply(drule_tac [!] a)
 
   106 apply(drule_tac [!] a)
 
    94 apply(rule_tac [!] p="p" in permute_boolE)
 
   107 apply(rule_tac [!] p="p" in permute_boolE)
 
    95 apply(perm_simp add: permute_minus_cancel b)
 
   108 apply(perm_simp add: permute_minus_cancel b)
 
    96 apply(assumption)
 
   109 apply(assumption)
 
    97 apply(perm_simp add: permute_minus_cancel b)
 
   110 apply(perm_simp add: permute_minus_cancel b)
 
    98 apply(assumption)
 
   111 apply(assumption)
 
    99 apply(perm_simp add: permute_minus_cancel b)
 
   112 apply(perm_simp add: permute_minus_cancel b)
 
   100 apply(assumption)
 
   113 apply(assumption)
 
   101 done
 
   114 done
 
   102 
   115 
   103 lemma alpha_gen_trans:
 
       
   104   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
 
       
   105   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)"
 
       
   106   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)"
 
       
   107   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)"
 
       
   108   using a
 
       
   109   unfolding alphas fresh_star_def
 
       
   110   by (simp_all add: fresh_plus_perm)
 
       
   111 
       
   112 
       
   113 lemma alpha_gen_trans_eqvt:
 
   116 lemma alpha_gen_trans_eqvt:
 
   114   assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
 
   117   assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
 
   115   and     a: "(bs, x) \<approx>gen R f p (cs, y)" 
   118   and     a: "(bs, x) \<approx>gen R f p (cs, y)" 
   116   and     d: "q \<bullet> R = R"
 
   119   and     d: "q \<bullet> R = R"
 
   117   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)"
 
   118   shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
 
   121   shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
 
   119 apply(rule alpha_gen_trans)
 
   122 apply(rule alpha_trans)
 
   120 defer
 
   123 defer
 
   121 apply(rule a)
 
   124 apply(rule a)
 
   122 apply(rule b)
 
   125 apply(rule b)
 
   123 apply(drule c)
 
   126 apply(drule c)
 
   124 apply(rule_tac p="q" in permute_boolE)
 
   127 apply(rule_tac p="q" in permute_boolE)
 
   134   assumes  b: "(cs, y) \<approx>res R f q (ds, z)"
 
   137   assumes  b: "(cs, y) \<approx>res R f q (ds, z)"
 
   135   and     a: "(bs, x) \<approx>res R f p (cs, y)" 
   138   and     a: "(bs, x) \<approx>res R f p (cs, y)" 
   136   and     d: "q \<bullet> R = R"
 
   139   and     d: "q \<bullet> R = R"
 
   137   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
 
   140   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
 
   138   shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
 
   141   shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
 
   139 apply(rule alpha_gen_trans)
 
   142 apply(rule alpha_trans)
 
   140 defer
 
   143 defer
 
   141 apply(rule a)
 
   144 apply(rule a)
 
   142 apply(rule b)
 
   145 apply(rule b)
 
   143 apply(drule c)
 
   146 apply(drule c)
 
   144 apply(rule_tac p="q" in permute_boolE)
 
   147 apply(rule_tac p="q" in permute_boolE)
 
   154   assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
 
   157   assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
 
   155   and     a: "(bs, x) \<approx>lst R f p (cs, y)" 
   158   and     a: "(bs, x) \<approx>lst R f p (cs, y)" 
   156   and     d: "q \<bullet> R = R"
 
   159   and     d: "q \<bullet> R = R"
 
   157   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
 
   160   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
 
   158   shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
 
   161   shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
 
   159 apply(rule alpha_gen_trans)
 
   162 apply(rule alpha_trans)
 
   160 defer
 
   163 defer
 
   161 apply(rule a)
 
   164 apply(rule a)
 
   162 apply(rule b)
 
   165 apply(rule b)
 
   163 apply(drule c)
 
   166 apply(drule c)
 
   164 apply(rule_tac p="q" in permute_boolE)
 
   167 apply(rule_tac p="q" in permute_boolE)
 
   170 apply(simp add: permute_eqvt[symmetric])
 
   173 apply(simp add: permute_eqvt[symmetric])
 
   171 done
 
   174 done
 
   172 
   175 
   173 lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
   176 lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
   174 
   177 
   175 lemma test:
 
       
   176   shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
 
       
   177   and   "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
 
       
   178   and   "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
 
       
   179   by (simp_all add: alphas)
 
       
   180 
       
   181 
   178 
   182 section {* General Abstractions *}
 
   179 section {* General Abstractions *}
 
   183 
   180 
   184 fun
 
   181 fun
 
   185   alpha_abs 
   182   alpha_abs 
   203   alpha_abs (infix "\<approx>abs" 50) and
 
   200   alpha_abs (infix "\<approx>abs" 50) and
 
   204   alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
 
   201   alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
 
   205   alpha_abs_res (infix "\<approx>abs'_res" 50)
 
   202   alpha_abs_res (infix "\<approx>abs'_res" 50)
 
   206 
   203 
   207 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
 
   204 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
 
       
   205 
   208 
   206 
   209 lemma alphas_abs_refl:
 
   207 lemma alphas_abs_refl:
 
   210   shows "(bs, x) \<approx>abs (bs, x)"
 
   208   shows "(bs, x) \<approx>abs (bs, x)"
 
   211   and   "(bs, x) \<approx>abs_res (bs, x)"
 
   209   and   "(bs, x) \<approx>abs_res (bs, x)"
 
   212   and   "(cs, x) \<approx>abs_lst (cs, x)" 
   210   and   "(cs, x) \<approx>abs_lst (cs, x)" 
   282 lemma [quot_respect]:
 
   280 lemma [quot_respect]:
 
   283   shows "(op= ===> op= ===> alpha_abs) Pair Pair"
 
   281   shows "(op= ===> op= ===> alpha_abs) Pair Pair"
 
   284   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
 
   282   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
 
   285   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
 
   283   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
 
   286   unfolding fun_rel_def
 
   284   unfolding fun_rel_def
 
   287   by (auto intro: alphas_abs_refl simp only:)
 
   285   by (auto intro: alphas_abs_refl)
 
   288 
   286 
   289 lemma [quot_respect]:
 
   287 lemma [quot_respect]:
 
   290   shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
 
   288   shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
 
   291   and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
 
   289   and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
 
   292   and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
 
   290   and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
 
   303 
   301 
   304 lemma abs_eq_iff:
 
   302 lemma abs_eq_iff:
 
   305   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
 
   303   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
 
   306   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)"
 
   307   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)"
 
   308   unfolding alphas_abs
 
   306   unfolding alphas_abs by (lifting alphas_abs)
 
   309   by (lifting alphas_abs)
 
       
   310 
   307 
   311 instantiation abs_gen :: (pt) pt
 
   308 instantiation abs_gen :: (pt) pt
 
   312 begin
 
   309 begin
 
   313 
   310 
   314 quotient_definition
 
   311 quotient_definition
 
   370   done
 
   367   done
 
   371 
   368 
   372 end
 
   369 end
 
   373 
   370 
   374 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
 
   371 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
 
       
   372 
   375 
   373 
   376 lemma abs_swap1:
 
   374 lemma abs_swap1:
 
   377   assumes a1: "a \<notin> (supp x) - bs"
 
   375   assumes a1: "a \<notin> (supp x) - bs"
 
   378   and     a2: "b \<notin> (supp x) - bs"
 
   376   and     a2: "b \<notin> (supp x) - bs"
 
   379   shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
 
   377   shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
 
   403      (auto simp add: supp_perm swap_atom)
 
   401      (auto simp add: supp_perm swap_atom)
 
   404 
   402 
   405 lemma abs_supports:
 
   403 lemma abs_supports:
 
   406   shows "((supp x) - as) supports (Abs as x)"
 
   404   shows "((supp x) - as) supports (Abs as x)"
 
   407   and   "((supp x) - as) supports (Abs_res as x)"
 
   405   and   "((supp x) - as) supports (Abs_res as x)"
 
   408   and   "((supp x) - (set bs)) supports (Abs_lst bs x)"
 
   406   and   "((supp x) - set bs) supports (Abs_lst bs x)"
 
   409   unfolding supports_def
 
   407   unfolding supports_def
 
   410   unfolding permute_abs
 
   408   unfolding permute_abs
 
   411   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
   409   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
   412 
   410 
   413 function
 
   411 function
 
   523   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)"
 
   524   unfolding fresh_def
 
   522   unfolding fresh_def
 
   525   unfolding supp_abs
 
   523   unfolding supp_abs
 
   526   by auto
 
   524   by auto
 
   527 
   525 
       
   526 fun
 
       
   527   prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
 
       
   528 where
 
       
   529   "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"
 
       
   530 
       
   531 definition 
       
   532   prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
 
       
   533 where
 
       
   534  "prod_alpha = prod_rel"
 
       
   535 
       
   536 
       
   537 lemma [quot_respect]:
 
       
   538   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
 
       
   539   by auto
 
       
   540 
       
   541 lemma [quot_preserve]:
 
       
   542   assumes q1: "Quotient R1 abs1 rep1"
 
       
   543   and     q2: "Quotient R2 abs2 rep2"
 
       
   544   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
 
       
   545   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
       
   546 
       
   547 lemma [mono]: 
       
   548   shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
 
       
   549   unfolding prod_alpha_def
 
       
   550   by auto
 
       
   551 
       
   552 lemma [eqvt]: 
       
   553   shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
 
       
   554   unfolding prod_alpha_def
 
       
   555   unfolding prod_rel.simps
 
       
   556   by (perm_simp) (rule refl)
 
       
   557 
       
   558 lemma [eqvt]: 
       
   559   shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
 
       
   560   unfolding prod_fv.simps
 
       
   561   by (perm_simp) (rule refl)
 
       
   562 
       
   563 
       
   564 
       
   565 
       
   566 
       
   567 
       
   568 
       
   569 
       
   570 
       
   571 
       
   572 
       
   573 
   528 section {* BELOW is stuff that may or may not be needed *}
 
   574 section {* BELOW is stuff that may or may not be needed *}
 
   529 
   575 
   530 lemma supp_atom_image:
 
   576 lemma supp_atom_image:
 
   531   fixes as::"'a::at_base set"
 
   577   fixes as::"'a::at_base set"
 
   532   shows "supp (atom ` as) = supp as"
 
   578   shows "supp (atom ` as) = supp as"
 
   577   "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
 
   623   "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
 
   578      (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
 
   624      (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
 
   579      R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
 
   625      R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
 
   580 by (simp add: alphas)
 
   626 by (simp add: alphas)
 
   581 
   627 
   582 lemma alpha_gen_simpler:
 
       
   583   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
 
       
   584   and fin_fv: "finite (f x)"
 
       
   585   and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
 
       
   586   shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
 
       
   587      (f x - bs) \<sharp>* pi \<and>
 
       
   588      R (pi \<bullet> x) y \<and>
 
       
   589      pi \<bullet> bs = cs"
 
       
   590   apply rule
 
       
   591   unfolding alpha_gen
 
       
   592   apply clarify
 
       
   593   apply (erule conjE)+
 
       
   594   apply (simp)
 
       
   595   apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
 
       
   596   apply (rule sym)
 
       
   597   apply simp
 
       
   598   apply (rule supp_perm_eq)
 
       
   599   apply (subst supp_finite_atom_set)
 
       
   600   apply (rule finite_Diff)
 
       
   601   apply (rule fin_fv)
 
       
   602   apply (assumption)
 
       
   603   apply (simp add: eqvts fv_eqvt)
 
       
   604   apply (subst fv_rsp)
 
       
   605   apply assumption
 
       
   606   apply (simp)
 
       
   607   done
 
       
   608 
       
   609 lemma alpha_lst_simpler:
 
       
   610   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
 
       
   611   and fin_fv: "finite (f x)"
 
       
   612   and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
 
       
   613   shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
 
       
   614      (f x - set bs) \<sharp>* pi \<and>
 
       
   615      R (pi \<bullet> x) y \<and>
 
       
   616      pi \<bullet> bs = cs"
 
       
   617   apply rule
 
       
   618   unfolding alpha_lst
 
       
   619   apply clarify
 
       
   620   apply (erule conjE)+
 
       
   621   apply (simp)
 
       
   622   apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
 
       
   623   apply (rule sym)
 
       
   624   apply simp
 
       
   625   apply (rule supp_perm_eq)
 
       
   626   apply (subst supp_finite_atom_set)
 
       
   627   apply (rule finite_Diff)
 
       
   628   apply (rule fin_fv)
 
       
   629   apply (assumption)
 
       
   630   apply (simp add: eqvts fv_eqvt)
 
       
   631   apply (subst fv_rsp)
 
       
   632   apply assumption
 
       
   633   apply (simp)
 
       
   634   done
 
       
   635 
       
   636 fun
 
       
   637   prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
 
       
   638 where
 
       
   639   "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
 
       
   640 
       
   641 definition 
       
   642   prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
 
       
   643 where
 
       
   644  "prod_alpha = prod_rel"
 
       
   645 
       
   646 
       
   647 lemma [quot_respect]:
 
       
   648   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
 
       
   649   by auto
 
       
   650 
       
   651 lemma [quot_preserve]:
 
       
   652   assumes q1: "Quotient R1 abs1 rep1"
 
       
   653   and     q2: "Quotient R2 abs2 rep2"
 
       
   654   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
 
       
   655   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
       
   656 
       
   657 lemma [mono]: 
       
   658   shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
 
       
   659   unfolding prod_alpha_def
 
       
   660   by auto
 
       
   661 
       
   662 lemma [eqvt]: 
       
   663   shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
 
       
   664   unfolding prod_alpha_def
 
       
   665   unfolding prod_rel.simps
 
       
   666   by (perm_simp) (rule refl)
 
       
   667 
       
   668 lemma [eqvt]: 
       
   669   shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
 
       
   670   unfolding prod_fv.simps
 
       
   671   by (perm_simp) (rule refl)
 
       
   672 
       
   673 
   628 
   674 end
 
   629 end
 
   675 
   630
nominal2