merged
authorhuffman
Sat Sep 03 15:37:41 2011 -0700 (2011-09-03)
changeset 44694cad98c8f0e35
parent 44693 a9635943a3e9
parent 44689 f247fc952f31
child 44695 075327b8e841
merged
     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))));