author haftmann Sat Sep 03 17:32:34 2011 +0200 (2011-09-03 ago) changeset 44683 daeb538c57bf parent 44671 7f0b4515588a child 44684 8dde3352d5c4
tuned specifications and proofs
```     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.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"
```