src/HOL/Nominal/Nominal.thy
changeset 19972 89c5afe4139a
parent 19869 eba1b9e7c458
child 19986 3e0eababf58d
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Jun 30 18:26:36 2006 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sun Jul 02 17:27:10 2006 +0200
     1.3 @@ -87,6 +87,16 @@
     1.4    shows "pi\<bullet>(b::bool) = b"
     1.5    by (cases b) auto
     1.6  
     1.7 +lemma perm_boolI:
     1.8 +  assumes a: "P"
     1.9 +  shows "pi\<bullet>P"
    1.10 +  using a by (simp add: perm_bool)
    1.11 +
    1.12 +lemma perm_boolE:
    1.13 +  assumes a: "pi\<bullet>P"
    1.14 +  shows "P"
    1.15 +  using a by (simp add: perm_bool)
    1.16 +
    1.17  (* permutation on options *)
    1.18  primrec (unchecked perm_option)
    1.19    perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
    1.20 @@ -865,6 +875,13 @@
    1.21  apply(simp add: supp_def dj_perm_forget[OF dj])
    1.22  done
    1.23  
    1.24 +lemma at_fresh_ineq:
    1.25 +  fixes a :: "'x"
    1.26 +  and   b :: "'y"
    1.27 +  assumes dj: "disjoint TYPE('y) TYPE('x)"
    1.28 +  shows "a\<sharp>b" 
    1.29 +  by (simp add: fresh_def dj_supp[OF dj])
    1.30 +
    1.31  section {* permutation type instances *}
    1.32  (* ===================================*)
    1.33  
    1.34 @@ -1406,6 +1423,15 @@
    1.35    shows  "a\<sharp>x"
    1.36  using a by (simp add: pt_fresh_bij[OF pt, OF at])
    1.37  
    1.38 +lemma pt_fresh_eqvt:
    1.39 +  fixes  pi :: "'x prm"
    1.40 +  and     x :: "'a"
    1.41 +  and     a :: "'x"
    1.42 +  assumes pt: "pt TYPE('a) TYPE('x)"
    1.43 +  and     at: "at TYPE('x)"
    1.44 +  shows "pi\<bullet>(a\<sharp>x) = (pi\<bullet>a)\<sharp>(pi\<bullet>x)"
    1.45 +  by (simp add: perm_bool pt_fresh_bij[OF pt, OF at])
    1.46 +
    1.47  lemma pt_perm_fresh1:
    1.48    fixes a :: "'x"
    1.49    and   b :: "'x"
    1.50 @@ -1556,6 +1582,29 @@
    1.51    thus ?thesis by (simp add: pt2[OF pt])
    1.52  qed
    1.53  
    1.54 +section {* equivaraince for some connectives *}
    1.55 +
    1.56 +lemma pt_all_eqvt:
    1.57 +  fixes  pi :: "'x prm"
    1.58 +  and     x :: "'a"
    1.59 +  assumes pt: "pt TYPE('a) TYPE('x)"
    1.60 +  and     at: "at TYPE('x)"
    1.61 +  shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). (pi\<bullet>P) x)"
    1.62 +apply(auto simp add: perm_bool perm_fun_def)
    1.63 +apply(drule_tac x="pi\<bullet>x" in spec)
    1.64 +apply(simp add: pt_rev_pi[OF pt, OF at])
    1.65 +done
    1.66 +
    1.67 +lemma imp_eqvt:
    1.68 +  fixes pi::"'x prm"
    1.69 +  shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
    1.70 +  by (simp add: perm_bool)
    1.71 +
    1.72 +lemma conj_eqvt:
    1.73 +  fixes pi::"'x prm"
    1.74 +  shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
    1.75 +  by (simp add: perm_bool)
    1.76 +
    1.77  section {* facts about supports *}
    1.78  (*==============================*)
    1.79