src/HOL/Nominal/Nominal.thy

   ("nominal_permeq.ML")
   ("nominal_fresh_fun.ML")
   ("nominal_primrec.ML")
   ("nominal_inductive.ML")
   ("nominal_inductive2.ML")
-begin 
+begin
 
 section {* Permutations *}
 (*======================*)
 
 type_synonym 

 
 (* a "private" copy of the option type used in the abstraction function *)
 datatype 'a noption = nSome 'a | nNone
 
 (* a "private" copy of the product type used in the nominal induct method *)
-datatype ('a,'b) nprod = nPair 'a 'b
+datatype ('a, 'b) nprod = nPair 'a 'b
 
 (* an auxiliary constant for the decision procedure involving *) 
 (* permutations (to avoid loops when using perm-compositions)  *)
 definition
   "perm_aux pi x = pi\<bullet>x"

 (* overloaded permutation operations *)
 overloading
   perm_fun    \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)"   (unchecked)
   perm_bool   \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool"           (unchecked)
   perm_unit   \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit"           (unchecked)
-  perm_prod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"     (unchecked)
+  perm_prod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"    (unchecked)
   perm_list   \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"     (unchecked)
   perm_option \<equiv> "perm :: 'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" (unchecked)
   perm_char   \<equiv> "perm :: 'x prm \<Rightarrow> char \<Rightarrow> char"           (unchecked)
   perm_nat    \<equiv> "perm :: 'x prm \<Rightarrow> nat \<Rightarrow> nat"             (unchecked)
   perm_int    \<equiv> "perm :: 'x prm \<Rightarrow> int \<Rightarrow> int"             (unchecked)

 begin
 
 definition
   perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
 
-primrec perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
-  true_eqvt:  "perm_bool pi True  = True"
-| false_eqvt: "perm_bool pi False = False"
+definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
+  perm_bool_def: "perm_bool pi b = b"
 
 primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
   "perm_unit pi () = ()"
   
 primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where

 primrec perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" where
   "perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)"
 
 end
 
-
 (* permutations on booleans *)
-lemma perm_bool:
-  shows "pi\<bullet>(b::bool) = b"
-  by (cases b) auto
+lemmas perm_bool = perm_bool_def
+
+lemma true_eqvt [simp]:
+  "pi \<bullet> True \<longleftrightarrow> True"
+  by (simp add: perm_bool_def)
+
+lemma false_eqvt [simp]:
+  "pi \<bullet> False \<longleftrightarrow> False"
+  by (simp add: perm_bool_def)
 
 lemma perm_boolI:
   assumes a: "P"
   shows "pi\<bullet>P"
   using a by (simp add: perm_bool)