src/HOL/Nominal/Nominal.thy
changeset 44689 f247fc952f31
parent 44683 daeb538c57bf
child 44696 4e99277c81f2
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Sat Sep 03 23:38:06 2011 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Sep 03 23:59:36 2011 +0200
     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"