Quot/Nominal/Abs.thy
changeset 1087 bb7f4457091a
parent 1063 b93b631570ca
child 1089 66097fe4942a
equal deleted inserted replaced
1084:40e3e6a6076f 1087:bb7f4457091a
     1 theory Abs
     1 theory Abs
     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd"
     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd"
     3 begin
     3 begin
     4 
     4 
     5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
     5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
     6 lemma in_permute_iff:
       
     7   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
       
     8 apply(unfold mem_def permute_fun_def)[1]
       
     9 apply(simp add: permute_bool_def) 
       
    10 done
       
    11 
       
    12 lemma fresh_plus:
       
    13   fixes p q::perm
       
    14   shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
       
    15   unfolding fresh_def
       
    16   using supp_plus_perm
       
    17   by(auto)
       
    18 
       
    19 lemma fresh_star_plus:
     6 lemma fresh_star_plus:
    20   fixes p q::perm
     7   fixes p q::perm
    21   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
     8   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
    22   unfolding fresh_star_def
     9   unfolding fresh_star_def
    23   by (simp add: fresh_plus)
    10   by (simp add: fresh_plus_perm)
    24 
    11 
    25 
    12 
    26 lemma fresh_star_permute_iff:
    13 lemma fresh_star_permute_iff:
    27   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
    14   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
    28 apply(simp add: fresh_star_def)
    15 apply(simp add: fresh_star_def)
    32 apply(simp add: eqvts del: permute_eqvt)
    19 apply(simp add: eqvts del: permute_eqvt)
    33 apply(simp add: fresh_permute_iff)
    20 apply(simp add: fresh_permute_iff)
    34 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
    21 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
    35 apply(simp)
    22 apply(simp)
    36 apply(drule_tac x="- p \<bullet> xa" in bspec)
    23 apply(drule_tac x="- p \<bullet> xa" in bspec)
    37 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
    24 apply(rule_tac ?p1="p" in mem_permute_iff[THEN iffD1])
    38 apply(simp)
    25 apply(simp)
    39 apply(simp)
    26 apply(simp)
    40 done
    27 done
    41 
       
    42 lemma fresh_minus_perm:
       
    43   fixes p::perm
       
    44   shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
       
    45   apply(simp add: fresh_def)
       
    46   apply(simp only: supp_minus_perm)
       
    47   done
       
    48 
    28 
    49 fun
    29 fun
    50   alpha_gen 
    30   alpha_gen 
    51 where
    31 where
    52   alpha_gen[simp del]:
    32   alpha_gen[simp del]: