--- a/src/HOL/Finite_Set.thy Thu Sep 08 09:25:55 2011 +0200
+++ b/src/HOL/Finite_Set.thy Thu Sep 08 11:31:53 2011 +0200
@@ -486,22 +486,9 @@
end
-instance unit :: finite proof
-qed (simp add: UNIV_unit)
-
-instance bool :: finite proof
-qed (simp add: UNIV_bool)
-
instance prod :: (finite, finite) finite proof
qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
-lemma finite_option_UNIV [simp]:
- "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
- by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
-
-instance option :: (finite) finite proof
-qed (simp add: UNIV_option_conv)
-
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
@@ -519,9 +506,22 @@
qed
qed
+instance bool :: finite proof
+qed (simp add: UNIV_bool)
+
+instance unit :: finite proof
+qed (simp add: UNIV_unit)
+
instance sum :: (finite, finite) finite proof
qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
+lemma finite_option_UNIV [simp]:
+ "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
+ by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
+
+instance option :: (finite) finite proof
+qed (simp add: UNIV_option_conv)
+
subsection {* A basic fold functional for finite sets *}
--- a/src/HOL/Nominal/Nominal.thy Thu Sep 08 09:25:55 2011 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Sep 08 11:31:53 2011 +0200
@@ -50,17 +50,17 @@
perm_nprod \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked)
begin
-definition
- perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
+definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+ "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
- perm_bool_def: "perm_bool pi b = b"
+ "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
- "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
+ "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
nil_eqvt: "perm_list pi [] = []"
@@ -71,13 +71,13 @@
| none_eqvt: "perm_option pi None = None"
definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
- perm_char_def: "perm_char pi c = c"
+ "perm_char pi c = c"
definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
- perm_nat_def: "perm_nat pi i = i"
+ "perm_nat pi i = i"
definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
- perm_int_def: "perm_int pi i = i"
+ "perm_int pi i = i"
primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
nsome_eqvt: "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
@@ -962,7 +962,7 @@
fixes pi::"'y prm"
and x ::"'x set"
assumes dj: "disjoint TYPE('x) TYPE('y)"
- shows "(pi\<bullet>x)=x"
+ shows "pi\<bullet>x=x"
using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
lemma dj_perm_perm_forget:
@@ -1028,7 +1028,7 @@
qed
lemma pt_unit_inst:
- shows "pt TYPE(unit) TYPE('x)"
+ shows "pt TYPE(unit) TYPE('x)"
by (simp add: pt_def)
lemma pt_prod_inst:
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Sep 08 09:25:55 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Sep 08 11:31:53 2011 +0200
@@ -130,7 +130,7 @@
case redex of
(* case pi o f == (%x. pi o (f ((rev pi)o x))) *)
(Const("Nominal.perm",_) $ pi $ f) =>
- (if (applicable_fun f) then SOME perm_fun_def else NONE)
+ (if applicable_fun f then SOME perm_fun_def else NONE)
| _ => NONE
end