# HG changeset patch
# User huffman
# Date 1315089461 25200
# Node ID cad98c8f0e356747881df79e4c58c2f64acfc9e6
# Parent  a9635943a3e969539d5fdfbaddbb16f18eaad54d# Parent  f247fc952f31682647d0ae2312efc9d266d9f691
merged

diff -r a9635943a3e9 -r cad98c8f0e35 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sat Sep 03 15:09:51 2011 -0700
+++ b/src/HOL/Nominal/Nominal.thy	Sat Sep 03 15:37:41 2011 -0700
@@ -10,7 +10,7 @@
   ("nominal_primrec.ML")
   ("nominal_inductive.ML")
   ("nominal_inductive2.ML")
-begin 
+begin
 
 section {* Permutations *}
 (*======================*)
@@ -27,7 +27,7 @@
 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)  *)
@@ -39,7 +39,7 @@
   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)
@@ -53,9 +53,8 @@
 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 () = ()"
@@ -89,11 +88,16 @@
 
 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"
diff -r a9635943a3e9 -r cad98c8f0e35 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 15:09:51 2011 -0700
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 15:37:41 2011 -0700
@@ -747,9 +747,9 @@
          |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
          |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
          |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
-         |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
-         |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
-         |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
+         |> discrete_pt_inst @{type_name bool} @{thm perm_bool_def}
+         |> discrete_fs_inst @{type_name bool} @{thm perm_bool_def}
+         |> discrete_cp_inst @{type_name bool} @{thm perm_bool_def}
          |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
          |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
          |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
diff -r a9635943a3e9 -r cad98c8f0e35 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sat Sep 03 15:09:51 2011 -0700
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Sep 03 15:37:41 2011 -0700
@@ -32,7 +32,7 @@
 
 val fresh_prod = @{thm fresh_prod};
 
-val perm_bool = mk_meta_eq @{thm perm_bool};
+val perm_bool = mk_meta_eq @{thm perm_bool_def};
 val perm_boolI = @{thm perm_boolI};
 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
   (Drule.strip_imp_concl (cprop_of perm_boolI))));
diff -r a9635943a3e9 -r cad98c8f0e35 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 03 15:09:51 2011 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 03 15:37:41 2011 -0700
@@ -36,7 +36,7 @@
 
 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
 
-val perm_bool = mk_meta_eq @{thm perm_bool};
+val perm_bool = mk_meta_eq @{thm perm_bool_def};
 val perm_boolI = @{thm perm_boolI};
 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
   (Drule.strip_imp_concl (cprop_of perm_boolI))));