--- a/src/HOL/Nominal/Nominal.thy Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/Nominal.thy Sat Sep 03 23:59:36 2011 +0200
@@ -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"
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Sep 03 23:59:36 2011 +0200
@@ -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}
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sat Sep 03 23:59:36 2011 +0200
@@ -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))));
--- a/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 03 23:59:36 2011 +0200
@@ -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))));