tuned
authorhaftmann
Mon Sep 05 22:02:32 2011 +0200 (2011-09-05)
changeset 448339c6bd6204143
parent 44720 f3a8c19708c8
child 44834 242348d1b6d3
tuned
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Sep 05 14:42:31 2011 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Sep 05 22:02:32 2011 +0200
     1.3 @@ -51,16 +51,16 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
     1.8 +  "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
     1.9  
    1.10  definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    1.11 -  perm_bool_def: "perm_bool pi b = b"
    1.12 +  "perm_bool pi b = b"
    1.13  
    1.14  primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    1.15    "perm_unit pi () = ()"
    1.16    
    1.17  primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
    1.18 -  "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
    1.19 +  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
    1.20  
    1.21  primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.22    nil_eqvt:  "perm_list pi []     = []"
    1.23 @@ -71,13 +71,13 @@
    1.24  | none_eqvt:  "perm_option pi None     = None"
    1.25  
    1.26  definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
    1.27 -  perm_char_def: "perm_char pi c = c"
    1.28 +  "perm_char pi c = c"
    1.29  
    1.30  definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
    1.31 -  perm_nat_def: "perm_nat pi i = i"
    1.32 +  "perm_nat pi i = i"
    1.33  
    1.34  definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
    1.35 -  perm_int_def: "perm_int pi i = i"
    1.36 +  "perm_int pi i = i"
    1.37  
    1.38  primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
    1.39    nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    1.40 @@ -962,7 +962,7 @@
    1.41    fixes pi::"'y prm"
    1.42    and   x ::"'x set"
    1.43    assumes dj: "disjoint TYPE('x) TYPE('y)"
    1.44 -  shows "(pi\<bullet>x)=x" 
    1.45 +  shows "pi\<bullet>x=x" 
    1.46    using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
    1.47  
    1.48  lemma dj_perm_perm_forget:
    1.49 @@ -1028,7 +1028,7 @@
    1.50  qed
    1.51  
    1.52  lemma pt_unit_inst:
    1.53 -  shows  "pt TYPE(unit) TYPE('x)"
    1.54 +  shows "pt TYPE(unit) TYPE('x)"
    1.55    by (simp add: pt_def)
    1.56  
    1.57  lemma pt_prod_inst: