tuned specifications and proofs
authorhaftmann
Sat Sep 03 17:32:34 2011 +0200 (2011-09-03 ago)
changeset 44683daeb538c57bf
parent 44671 7f0b4515588a
child 44684 8dde3352d5c4
tuned specifications and proofs
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Sep 02 16:58:00 2011 -0700
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Sep 03 17:32:34 2011 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  (* an auxiliary constant for the decision procedure involving *) 
     1.5  (* permutations (to avoid loops when using perm-compositions)  *)
     1.6  definition
     1.7 -  "perm_aux pi x \<equiv> pi\<bullet>x"
     1.8 +  "perm_aux pi x = pi\<bullet>x"
     1.9  
    1.10  (* overloaded permutation operations *)
    1.11  overloading
    1.12 @@ -51,61 +51,42 @@
    1.13  begin
    1.14  
    1.15  definition
    1.16 -  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    1.17 -
    1.18 -fun
    1.19 -  perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool"
    1.20 -where
    1.21 +  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    1.22 +
    1.23 +primrec perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    1.24    true_eqvt:  "perm_bool pi True  = True"
    1.25  | false_eqvt: "perm_bool pi False = False"
    1.26  
    1.27 -fun
    1.28 -  perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" 
    1.29 -where 
    1.30 +primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    1.31    "perm_unit pi () = ()"
    1.32    
    1.33 -fun
    1.34 -  perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"
    1.35 -where
    1.36 +primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
    1.37    "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
    1.38  
    1.39 -fun
    1.40 -  perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.41 -where
    1.42 +primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.43    nil_eqvt:  "perm_list pi []     = []"
    1.44  | cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    1.45  
    1.46 -fun
    1.47 -  perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option"
    1.48 -where
    1.49 +primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where
    1.50    some_eqvt:  "perm_option pi (Some x) = Some (pi\<bullet>x)"
    1.51  | none_eqvt:  "perm_option pi None     = None"
    1.52  
    1.53 -definition
    1.54 -  perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char"
    1.55 -where
    1.56 -  perm_char_def: "perm_char pi c \<equiv> c"
    1.57 -
    1.58 -definition
    1.59 -  perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat"
    1.60 -where
    1.61 -  perm_nat_def: "perm_nat pi i \<equiv> i"
    1.62 -
    1.63 -definition
    1.64 -  perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int"
    1.65 -where
    1.66 -  perm_int_def: "perm_int pi i \<equiv> i"
    1.67 -
    1.68 -fun
    1.69 -  perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"
    1.70 -where
    1.71 +definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
    1.72 +  perm_char_def: "perm_char pi c = c"
    1.73 +
    1.74 +definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
    1.75 +  perm_nat_def: "perm_nat pi i = i"
    1.76 +
    1.77 +definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
    1.78 +  perm_int_def: "perm_int pi i = i"
    1.79 +
    1.80 +primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
    1.81    nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    1.82  | nnone_eqvt:  "perm_noption pi nNone     = nNone"
    1.83  
    1.84 -fun
    1.85 -  perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod"
    1.86 -where
    1.87 +primrec perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" where
    1.88    "perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)"
    1.89 +
    1.90  end
    1.91  
    1.92  
    1.93 @@ -188,18 +169,18 @@
    1.94  (*==============================*)
    1.95  
    1.96  definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) where
    1.97 -  "pi1 \<triangleq> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
    1.98 +  "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)"
    1.99  
   1.100  section {* Support, Freshness and Supports*}
   1.101  (*========================================*)
   1.102  definition supp :: "'a \<Rightarrow> ('x set)" where  
   1.103 -   "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
   1.104 +   "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
   1.105  
   1.106  definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) where
   1.107 -   "a \<sharp> x \<equiv> a \<notin> supp x"
   1.108 +   "a \<sharp> x \<longleftrightarrow> a \<notin> supp x"
   1.109  
   1.110  definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) where
   1.111 -   "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
   1.112 +   "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))"
   1.113  
   1.114  (* lemmas about supp *)
   1.115  lemma supp_fresh_iff: 
   1.116 @@ -1731,7 +1712,7 @@
   1.117    hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 
   1.118      by (force dest: Diff_infinite_finite)
   1.119    hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
   1.120 -    by (metis Collect_def finite_set set_empty2)
   1.121 +    by (metis finite_set set_empty2)
   1.122    hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
   1.123    then obtain c 
   1.124      where eq1: "[(a,c)]\<bullet>x = x"