src/HOL/Nominal/Nominal.thy

 
 section {* permutation equality *}
 (*==============================*)
 
 constdefs
-  prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool"  (" _ \<sim> _ " [80,80] 80)
-  "pi1 \<sim> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
+  prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool"  (" _ \<triangleq> _ " [80,80] 80)
+  "pi1 \<triangleq> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
 
 section {* Support, Freshness and Supports*}
 (*========================================*)
 constdefs
    supp :: "'a \<Rightarrow> ('x set)"  

 (* properties for being a permutation type *)
 constdefs 
   "pt TYPE('a) TYPE('x) \<equiv> 
      (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 
      (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 
-     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<sim> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
+     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<triangleq> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
 
 (* properties for being an atom type *)
 constdefs 
   "at TYPE('x) \<equiv> 
      (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and>

 
 lemma at_prm_rev_eq:
   fixes pi1 :: "'x prm"
   and   pi2 :: "'x prm"
   assumes at: "at TYPE('x)"
-  shows a: "((rev pi1) \<sim> (rev pi2)) = (pi1 \<sim> pi2)"
+  shows a: "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)"
 proof (simp add: prm_eq_def, auto)
   fix x
   assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp
   hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at])
   hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
-  thus "pi1 \<bullet> x  =  pi2 \<bullet> x" by simp
+  thus "pi1\<bullet>x  =  pi2\<bullet>x" by simp
 next
   fix x
   assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
   hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp
   hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at])

   
 lemma at_prm_rev_eq1:
   fixes pi1 :: "'x prm"
   and   pi2 :: "'x prm"
   assumes at: "at TYPE('x)"
-  shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1) \<sim> (rev pi2)"
+  shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
   by (simp add: at_prm_rev_eq[OF at])
 
 lemma at_ds1:
   fixes a  :: "'x"
   assumes at: "at TYPE('x)"
-  shows "[(a,a)] \<sim> []"
+  shows "[(a,a)] \<triangleq> []"
   by (force simp add: prm_eq_def at_calc[OF at])
 
 lemma at_ds2: 
   fixes pi :: "'x prm"
   and   a  :: "'x"
   and   b  :: "'x"
   assumes at: "at TYPE('x)"
-  shows "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<sim> ([(a,b)]@pi)"
+  shows "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<triangleq> ([(a,b)]@pi)"
   by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
       at_rev_pi[OF at] at_calc[OF at])
 
 lemma at_ds3: 
   fixes a  :: "'x"
   and   b  :: "'x"
   and   c  :: "'x"
   assumes at: "at TYPE('x)"
   and     a:  "distinct [a,b,c]"
-  shows "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]"
+  shows "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]"
   using a by (force simp add: prm_eq_def at_calc[OF at])
 
 lemma at_ds4: 
   fixes a  :: "'x"
   and   b  :: "'x"
   and   pi  :: "'x prm"
   assumes at: "at TYPE('x)"
-  shows "(pi@[(a,(rev pi)\<bullet>b)]) \<sim> ([(pi\<bullet>a,b)]@pi)"
+  shows "(pi@[(a,(rev pi)\<bullet>b)]) \<triangleq> ([(pi\<bullet>a,b)]@pi)"
   by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
       at_pi_rev[OF at] at_rev_pi[OF at])
 
 lemma at_ds5: 
   fixes a  :: "'x"
   and   b  :: "'x"
   assumes at: "at TYPE('x)"
-  shows "[(a,b)] \<sim> [(b,a)]"
+  shows "[(a,b)] \<triangleq> [(b,a)]"
   by (force simp add: prm_eq_def at_calc[OF at])
 
 lemma at_ds6: 
   fixes a  :: "'x"
   and   b  :: "'x"
   and   c  :: "'x"
   assumes at: "at TYPE('x)"
   and     a: "distinct [a,b,c]"
-  shows "[(a,c),(a,b)] \<sim> [(b,c),(a,c)]"
+  shows "[(a,c),(a,b)] \<triangleq> [(b,c),(a,c)]"
   using a by (force simp add: prm_eq_def at_calc[OF at])
 
 lemma at_ds7:
   fixes pi :: "'x prm"
   assumes at: "at TYPE('x)"
-  shows "((rev pi)@pi) \<sim> []"
+  shows "((rev pi)@pi) \<triangleq> []"
   by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at])
 
 lemma at_ds8_aux:
   fixes pi :: "'x prm"
   and   a  :: "'x"

   fixes pi1 :: "'x prm"
   and   pi2 :: "'x prm"
   and   a  :: "'x"
   and   b  :: "'x"
   assumes at: "at TYPE('x)"
-  shows "(pi1@pi2) \<sim> ((pi1\<bullet>pi2)@pi1)"
+  shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)"
 apply(induct_tac pi2)
 apply(simp add: prm_eq_def)
 apply(auto simp add: prm_eq_def)
 apply(simp add: at2[OF at])
 apply(drule_tac x="aa" in spec)

   fixes pi1 :: "'x prm"
   and   pi2 :: "'x prm"
   and   a  :: "'x"
   and   b  :: "'x"
   assumes at: "at TYPE('x)"
-  shows " ((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
+  shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
 apply(induct_tac pi2)
 apply(simp add: prm_eq_def)
 apply(auto simp add: prm_eq_def)
 apply(simp add: at_append[OF at])
 apply(simp add: at2[OF at] at1[OF at])

 lemma pt3:
   fixes pi1::"'x prm"
   and   pi2::"'x prm"
   and   x  ::"'a"
   assumes a: "pt TYPE('a) TYPE('x)"
-  shows "pi1 \<sim> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
+  shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
   using a by (simp add: pt_def)
 
 lemma pt3_rev:
   fixes pi1::"'x prm"
   and   pi2::"'x prm"
   and   x  ::"'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
+  shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])
 
 section {* composition properties *}
 (* ============================== *)
 lemma cp1:

 lemma pt_list_prm_eq: 
   fixes pi1 :: "'x prm"
   and   pi2 :: "'x prm"
   and   xs  :: "'a list"
   assumes pt: "pt TYPE('a) TYPE ('x)"
-  shows "pi1 \<sim> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
+  shows "pi1 \<triangleq> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
 apply(induct_tac xs)
 apply(simp_all add: prm_eq_def pt3[OF pt])
 done
 
 lemma pt_list_inst:

   shows  "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
 apply(auto simp only: pt_def)
 apply(simp_all add: perm_fun_def)
 apply(simp add: pt1[OF pta] pt1[OF ptb])
 apply(simp add: pt2[OF pta] pt2[OF ptb])
-apply(subgoal_tac "(rev pi1) \<sim> (rev pi2)")(*A*)
+apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*)
 apply(simp add: pt3[OF pta] pt3[OF ptb])
 (*A*)
 apply(simp add: at_prm_rev_eq[OF at])
 done
 

   and   x  :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
 proof -
-  have "((rev pi)@pi) \<sim> ([]::'x prm)" by (simp add: at_ds7[OF at])
+  have "((rev pi)@pi) \<triangleq> ([]::'x prm)" by (simp add: at_ds7[OF at])
   hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
   thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
 qed
 
 lemma pt_pi_rev:

   and     at: "at TYPE ('x)"
   and     a1: "a\<sharp>x" and a2: "b\<sharp>x" 
   shows "[(a,b)]\<bullet>x=x"
 proof (cases "a=b")
   assume c1: "a=b"
-  have "[(a,a)] \<sim> []" by (rule at_ds1[OF at])
-  hence "[(a,b)] \<sim> []" using c1 by simp
+  have "[(a,a)] \<triangleq> []" by (rule at_ds1[OF at])
+  hence "[(a,b)] \<triangleq> []" using c1 by simp
   hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
   thus ?thesis by (simp only: pt1[OF pt])
 next
   assume c2: "a\<noteq>b"
   from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)

       and eq2: "[(b,c)]\<bullet>x = x" 
       and ineq: "a\<noteq>c \<and> b\<noteq>c"
     by (force)
   hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp 
   hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric])
-  from c2 ineq have "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]" by (simp add: at_ds3[OF at])
+  from c2 ineq have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" by (simp add: at_ds3[OF at])
   hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt])
   thus ?thesis using eq3 by simp
 qed
 
 lemma pt_perm_compose:

   and   x  :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 
 proof -
-  have "(pi2@pi1) \<sim> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
+  have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
   hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
   thus ?thesis by (simp add: pt2[OF pt])
 qed
 
 lemma pt_perm_compose_rev:

   and   x  :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
   shows "(rev pi2)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)" 
 proof -
-  have "((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
+  have "((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
   hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt])
   thus ?thesis by (simp add: pt2[OF pt])
 qed
 
 section {* facts about supports *}

 	have "c\<sharp>x = c\<sharp>y" using a2 a5 by (force simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at])
 	moreover 
 	have "c\<sharp>y \<longrightarrow> [(a,c)]\<bullet>x = [(b,c)]\<bullet>y" 
 	proof (intro strip)
 	  assume a6: "c\<sharp>y"
-	  have "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]" using a1 a5 by (force intro: at_ds3[OF at])
+	  have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" using a1 a5 by (force intro: at_ds3[OF at])
 	  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>y)) = [(a,b)]\<bullet>y" 
 	    by (simp add: pt2[OF pt, symmetric] pt3[OF pt])
  	  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = [(a,b)]\<bullet>y" using a3 a6 
 	    by (simp add: pt_fresh_fresh[OF pt, OF at])
 	  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = x" using a2 by simp