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 1557 fee2389789ad
parent 1544 c6849a634582
child 1558 a5ba76208983
equal deleted inserted replaced
1556:a7072d498723 1557:fee2389789ad 
     1 theory Abs
 
     1 theory Abs
 
     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" "Nominal2_FSet"
 
     2 imports "Nominal2_Atoms" 
       
     3         "Nominal2_Eqvt" 
       
     4         "Nominal2_Supp" 
       
     5         "Nominal2_FSet"
 
       
     6         "../Quotient" 
       
     7         "../Quotient_Product" 
     3 begin
 
     8 begin
 
     4 
       
     5 lemma permute_boolI:
 
       
     6   fixes P::"bool"
 
       
     7   shows "p \<bullet> P \<Longrightarrow> P"
 
       
     8 apply(simp add: permute_bool_def)
 
       
     9 done
 
       
    10 
       
    11 lemma permute_boolE:
 
       
    12   fixes P::"bool"
 
       
    13   shows "P \<Longrightarrow> p \<bullet> P"
 
       
    14 apply(simp add: permute_bool_def)
 
       
    15 done
 
       
    16 
     9 
    17 fun
 
    10 fun
 
    18   alpha_gen 
    11   alpha_gen 
    19 where
 
    12 where
 
    20   alpha_gen[simp del]:
 
    13   alpha_gen[simp del]:
 
    22      f x - bs = f y - cs \<and> 
    15      f x - bs = f y - cs \<and> 
    23      (f x - bs) \<sharp>* pi \<and> 
    16      (f x - bs) \<sharp>* pi \<and> 
    24      R (pi \<bullet> x) y \<and>
 
    17      R (pi \<bullet> x) y \<and>
 
    25      pi \<bullet> bs = cs"
 
    18      pi \<bullet> bs = cs"
 
    26 
    19 
       
    20 fun
 
       
    21   alpha_res
 
       
    22 where
 
       
    23   alpha_res[simp del]:
 
       
    24   "alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow> 
       
    25      f x - bs = f y - cs \<and> 
       
    26      (f x - bs) \<sharp>* pi \<and> 
       
    27      R (pi \<bullet> x) y"
 
       
    28 
       
    29 fun
 
       
    30   alpha_lst
 
       
    31 where
 
       
    32   alpha_lst[simp del]:
 
       
    33   "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow> 
       
    34      f x - set bs = f y - set cs \<and> 
       
    35      (f x - set bs) \<sharp>* pi \<and> 
       
    36      R (pi \<bullet> x) y \<and>
 
       
    37      pi \<bullet> bs = cs"
 
       
    38 
       
    39 lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
 
       
    40 
    27 notation
 
    41 notation
 
    28   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
 
    42   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
 
    29 
    43   alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
 
    30 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
 
    44   alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
    31   by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
 
    45 
       
    46 (* monos *)
 
       
    47 lemma [mono]: 
       
    48   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_lst cs R1 \<le> alpha_lst cs R2"
 
       
    51   by (case_tac [!] bs, case_tac [!] cs) 
       
    52      (auto simp add: le_fun_def le_bool_def alphas)
 
    32 
    53 
    33 lemma alpha_gen_refl:
 
    54 lemma alpha_gen_refl:
 
    34   assumes a: "R x x"
 
    55   assumes a: "R x x"
 
    35   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
 
    56   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
 
    36   using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)
 
    57   and   "(bs, x) \<approx>res R f 0 (bs, x)"
 
       
    58   and   "(cs, x) \<approx>lst R f 0 (cs, x)"
 
       
    59   using a 
       
    60   unfolding alphas
 
       
    61   unfolding fresh_star_def
 
       
    62   by (simp_all add: fresh_zero_perm)
 
    37 
    63 
    38 lemma alpha_gen_sym:
 
    64 lemma alpha_gen_sym:
 
    39   assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
 
    65   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
 
    40   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
 
    66   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
 
    41   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
 
    67   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
 
    42   using a b 
    68   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
 
    43   apply (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
 
    69   using a
 
    44   apply(clarify)
 
    70   unfolding alphas
 
    45   apply(simp)
 
    71   unfolding fresh_star_def
 
    46   done
 
    72   by (auto simp add:  fresh_minus_perm)
 
    47 
    73 
    48 lemma alpha_gen_trans:
 
    74 lemma alpha_gen_trans:
 
    49   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
 
    75   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
 
    50   and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
 
    76   and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
 
    51   and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
 
    77   and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
 
   153   "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
   179   "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
 
   154 
   180 
   155 notation
 
   181 notation
 
   156   alpha_abs ("_ \<approx>abs _")
 
   182   alpha_abs ("_ \<approx>abs _")
 
   157 
   183 
   158 
       
   159 
       
   160 lemma alpha_abs_swap:
 
   184 lemma alpha_abs_swap:
 
   161   assumes a1: "a \<notin> (supp x) - bs"
 
   185   assumes a1: "a \<notin> (supp x) - bs"
 
   162   and     a2: "b \<notin> (supp x) - bs"
 
   186   and     a2: "b \<notin> (supp x) - bs"
 
   163   shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
 
   187   shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
 
   164   apply(simp)
 
   188   apply(simp)
 
   207   apply(rule equivpI)
 
   231   apply(rule equivpI)
 
   208   unfolding reflp_def symp_def transp_def
 
   232   unfolding reflp_def symp_def transp_def
 
   209   apply(simp_all)
 
   233   apply(simp_all)
 
   210   (* refl *)
 
   234   (* refl *)
 
   211   apply(clarify)
 
   235   apply(clarify)
 
   212   apply(rule exI)
 
   236   apply(rule_tac x="0" in exI)
 
   213   apply(rule alpha_gen_refl)
 
   237   apply(rule alpha_gen_refl)
 
   214   apply(simp)
 
   238   apply(simp)
 
   215   (* symm *)
 
   239   (* symm *)
 
   216   apply(clarify)
 
   240   apply(clarify)
 
   217   apply(rule exI)
 
   241   apply(rule_tac x="- p" in exI)
 
   218   apply(rule alpha_gen_sym)
 
   242   apply(rule alpha_gen_sym)
 
       
   243   apply(clarsimp)
 
   219   apply(assumption)
 
   244   apply(assumption)
 
   220   apply(clarsimp)
 
       
   221   (* trans *)
 
   245   (* trans *)
 
   222   apply(clarify)
 
   246   apply(clarify)
 
   223   apply(rule exI)
 
   247   apply(rule_tac x="pa + p" in exI)
 
   224   apply(rule alpha_gen_trans)
 
   248   apply(rule alpha_gen_trans)
 
   225   apply(assumption)
 
   249   apply(assumption)
 
   226   apply(assumption)
 
   250   apply(assumption)
 
   227   apply(simp)
 
   251   apply(simp)
 
   228   done
 
   252   done
 
   616 lemma kk:
 
   640 lemma kk:
 
   617   assumes a: "p \<bullet> x = y"
 
   641   assumes a: "p \<bullet> x = y"
 
   618   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
 
   642   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
 
   619 using a
 
   643 using a
 
   620 apply(auto)
 
   644 apply(auto)
 
   621 apply(rule_tac p="- p" in permute_boolI)
 
   645 apply(rule_tac p="- p" in permute_boolE)
 
   622 apply(simp add: mem_eqvt supp_eqvt)
 
   646 apply(simp add: mem_eqvt supp_eqvt)
 
   623 done
 
   647 done
 
   624 
   648 
   625 lemma ww:
 
   649 lemma ww:
 
   626   assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"
 
   650   assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"
 
   632 apply(drule_tac x="a" in spec)
 
   656 apply(drule_tac x="a" in spec)
 
   633 defer
 
   657 defer
 
   634 apply(rule supp_supports)
 
   658 apply(rule supp_supports)
 
   635 apply(auto)
 
   659 apply(auto)
 
   636 apply(rotate_tac 1)
 
   660 apply(rotate_tac 1)
 
   637 apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
 
   661 apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
 
   638 apply(simp add: mem_eqvt supp_eqvt)
 
   662 apply(simp add: mem_eqvt supp_eqvt)
 
   639 done
 
   663 done
 
   640 
   664 
   641 lemma alpha_abs_sym:
 
   665 lemma alpha_abs_sym:
 
   642   assumes a: "({a}, x) \<approx>abs ({b}, y)"
 
   666   assumes a: "({a}, x) \<approx>abs ({b}, y)"
 
   722 apply(rotate_tac 4)
 
   746 apply(rotate_tac 4)
 
   723 apply(drule_tac alpha_abs_trans)
 
   747 apply(drule_tac alpha_abs_trans)
 
   724 apply(assumption)
 
   748 apply(assumption)
 
   725 apply(drule alpha_equal)
 
   749 apply(drule alpha_equal)
 
   726 apply(simp)
 
   750 apply(simp)
 
   727 apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
 
   751 apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
 
   728 apply(simp add: fresh_eqvt)
 
   752 apply(simp add: fresh_eqvt)
 
   729 apply(simp add: fresh_def)
 
   753 apply(simp add: fresh_def)
 
   730 done
 
   754 done
 
   731 
   755 
   732 lemma alpha_new_old:
 
   756 lemma alpha_new_old:
 
   780   "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
 
   804   "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
 
   781   (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
 
   805   (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
 
   782   \<and> pi \<bullet> bs = cs)"
 
   806   \<and> pi \<bullet> bs = cs)"
 
   783 by (simp add: alpha_gen)
 
   807 by (simp add: alpha_gen)
 
   784 
   808 
   785 (* maybe should be added to Infinite.thy *)
 
       
   786 lemma infinite_Un:
 
       
   787   shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
 
       
   788   by simp
 
       
   789 
   809 
   790 end
 
   810 end
 
   791 
   811
nominal2