1.1 --- a/src/HOL/Nominal/Nominal.thy Sat Sep 03 15:09:51 2011 -0700
1.2 +++ b/src/HOL/Nominal/Nominal.thy Sat Sep 03 15:37:41 2011 -0700
1.3 @@ -10,7 +10,7 @@
1.4 ("nominal_primrec.ML")
1.5 ("nominal_inductive.ML")
1.6 ("nominal_inductive2.ML")
1.7 -begin
1.8 +begin
1.9
1.10 section {* Permutations *}
1.11 (*======================*)
1.12 @@ -27,7 +27,7 @@
1.13 datatype 'a noption = nSome 'a | nNone
1.14
1.15 (* a "private" copy of the product type used in the nominal induct method *)
1.16 -datatype ('a,'b) nprod = nPair 'a 'b
1.17 +datatype ('a, 'b) nprod = nPair 'a 'b
1.18
1.19 (* an auxiliary constant for the decision procedure involving *)
1.20 (* permutations (to avoid loops when using perm-compositions) *)
1.21 @@ -39,7 +39,7 @@
1.22 perm_fun \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)" (unchecked)
1.23 perm_bool \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool" (unchecked)
1.24 perm_unit \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit" (unchecked)
1.25 - perm_prod \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" (unchecked)
1.26 + perm_prod \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" (unchecked)
1.27 perm_list \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" (unchecked)
1.28 perm_option \<equiv> "perm :: 'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" (unchecked)
1.29 perm_char \<equiv> "perm :: 'x prm \<Rightarrow> char \<Rightarrow> char" (unchecked)
1.30 @@ -53,9 +53,8 @@
1.31 definition
1.32 perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
1.33
1.34 -primrec perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
1.35 - true_eqvt: "perm_bool pi True = True"
1.36 -| false_eqvt: "perm_bool pi False = False"
1.37 +definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
1.38 + perm_bool_def: "perm_bool pi b = b"
1.39
1.40 primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" where
1.41 "perm_unit pi () = ()"
1.42 @@ -89,11 +88,16 @@
1.43
1.44 end
1.45
1.46 -
1.47 (* permutations on booleans *)
1.48 -lemma perm_bool:
1.49 - shows "pi\<bullet>(b::bool) = b"
1.50 - by (cases b) auto
1.51 +lemmas perm_bool = perm_bool_def
1.52 +
1.53 +lemma true_eqvt [simp]:
1.54 + "pi \<bullet> True \<longleftrightarrow> True"
1.55 + by (simp add: perm_bool_def)
1.56 +
1.57 +lemma false_eqvt [simp]:
1.58 + "pi \<bullet> False \<longleftrightarrow> False"
1.59 + by (simp add: perm_bool_def)
1.60
1.61 lemma perm_boolI:
1.62 assumes a: "P"
2.1 --- a/src/HOL/Nominal/nominal_atoms.ML Sat Sep 03 15:09:51 2011 -0700
2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Sep 03 15:37:41 2011 -0700
2.3 @@ -747,9 +747,9 @@
2.4 |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
2.5 |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
2.6 |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
2.7 - |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
2.8 - |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
2.9 - |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
2.10 + |> discrete_pt_inst @{type_name bool} @{thm perm_bool_def}
2.11 + |> discrete_fs_inst @{type_name bool} @{thm perm_bool_def}
2.12 + |> discrete_cp_inst @{type_name bool} @{thm perm_bool_def}
2.13 |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
2.14 |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
2.15 |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
3.1 --- a/src/HOL/Nominal/nominal_inductive.ML Sat Sep 03 15:09:51 2011 -0700
3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Sep 03 15:37:41 2011 -0700
3.3 @@ -32,7 +32,7 @@
3.4
3.5 val fresh_prod = @{thm fresh_prod};
3.6
3.7 -val perm_bool = mk_meta_eq @{thm perm_bool};
3.8 +val perm_bool = mk_meta_eq @{thm perm_bool_def};
3.9 val perm_boolI = @{thm perm_boolI};
3.10 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
3.11 (Drule.strip_imp_concl (cprop_of perm_boolI))));
4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 03 15:09:51 2011 -0700
4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 03 15:37:41 2011 -0700
4.3 @@ -36,7 +36,7 @@
4.4
4.5 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
4.6
4.7 -val perm_bool = mk_meta_eq @{thm perm_bool};
4.8 +val perm_bool = mk_meta_eq @{thm perm_bool_def};
4.9 val perm_boolI = @{thm perm_boolI};
4.10 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
4.11 (Drule.strip_imp_concl (cprop_of perm_boolI))));