adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
authorChristian Urban <urbanc@in.tum.de>
Sat Apr 25 21:42:05 2009 +0200 (2009-04-25)
changeset 30983e54777ab68bd
parent 30977 0e8e8903ff4e
child 30984 e6349035148a
child 30986 047fa04a9fe8
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Sat Apr 25 08:34:30 2009 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Apr 25 21:42:05 2009 +0200
     1.3 @@ -23,20 +23,93 @@
     1.4    perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
     1.5    swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
     1.6  
     1.7 +(* a "private" copy of the option type used in the abstraction function *)
     1.8 +datatype 'a noption = nSome 'a | nNone
     1.9 +
    1.10 +(* a "private" copy of the product type used in the nominal induct method *)
    1.11 +datatype ('a,'b) nprod = nPair 'a 'b
    1.12 +
    1.13  (* an auxiliary constant for the decision procedure involving *) 
    1.14 -(* permutations (to avoid loops when using perm-composition)  *)
    1.15 +(* permutations (to avoid loops when using perm-compositions)  *)
    1.16  constdefs
    1.17    "perm_aux pi x \<equiv> pi\<bullet>x"
    1.18  
    1.19 -(* permutation on functions *)
    1.20 -defs (unchecked overloaded)
    1.21 -  perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    1.22 -
    1.23 -(* permutation on bools *)
    1.24 -primrec (unchecked perm_bool)
    1.25 -  true_eqvt:  "pi\<bullet>True  = True"
    1.26 -  false_eqvt: "pi\<bullet>False = False"
    1.27 -
    1.28 +(* permutation operations *)
    1.29 +overloading
    1.30 +  perm_fun    \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)"   (unchecked)
    1.31 +  perm_bool   \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool"           (unchecked)
    1.32 +  perm_unit   \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit"           (unchecked)
    1.33 +  perm_prod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"     (unchecked)
    1.34 +  perm_list   \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"     (unchecked)
    1.35 +  perm_option \<equiv> "perm :: 'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" (unchecked)
    1.36 +  perm_char   \<equiv> "perm :: 'x prm \<Rightarrow> char \<Rightarrow> char"           (unchecked)
    1.37 +  perm_nat    \<equiv> "perm :: 'x prm \<Rightarrow> nat \<Rightarrow> nat"             (unchecked)
    1.38 +  perm_int    \<equiv> "perm :: 'x prm \<Rightarrow> int \<Rightarrow> int"             (unchecked)
    1.39 +
    1.40 +  perm_noption \<equiv> "perm :: 'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"   (unchecked)
    1.41 +  perm_nprod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked)
    1.42 +begin
    1.43 +
    1.44 +definition
    1.45 +  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    1.46 +
    1.47 +fun
    1.48 +  perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool"
    1.49 +where
    1.50 +  true_eqvt:  "perm_bool pi True  = True"
    1.51 +| false_eqvt: "perm_bool pi False = False"
    1.52 +
    1.53 +fun
    1.54 +  perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" 
    1.55 +where 
    1.56 +  "perm_unit pi () = ()"
    1.57 +  
    1.58 +fun
    1.59 +  perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"
    1.60 +where
    1.61 +  "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
    1.62 +
    1.63 +fun
    1.64 +  perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.65 +where
    1.66 +  nil_eqvt:  "perm_list pi []     = []"
    1.67 +| cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    1.68 +
    1.69 +fun
    1.70 +  perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option"
    1.71 +where
    1.72 +  some_eqvt:  "perm_option pi (Some x) = Some (pi\<bullet>x)"
    1.73 +| none_eqvt:  "perm_option pi None     = None"
    1.74 +
    1.75 +definition
    1.76 +  perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char"
    1.77 +where
    1.78 +  perm_char_def: "perm_char pi c \<equiv> c"
    1.79 +
    1.80 +definition
    1.81 +  perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat"
    1.82 +where
    1.83 +  perm_nat_def: "perm_nat pi i \<equiv> i"
    1.84 +
    1.85 +definition
    1.86 +  perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int"
    1.87 +where
    1.88 +  perm_int_def: "perm_int pi i \<equiv> i"
    1.89 +
    1.90 +fun
    1.91 +  perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"
    1.92 +where
    1.93 +  nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    1.94 +| nnone_eqvt:  "perm_noption pi nNone     = nNone"
    1.95 +
    1.96 +fun
    1.97 +  perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod"
    1.98 +where
    1.99 +  "perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)"
   1.100 +end
   1.101 +
   1.102 +
   1.103 +(* permutations on booleans *)
   1.104  lemma perm_bool:
   1.105    shows "pi\<bullet>(b::bool) = b"
   1.106    by (cases b) auto
   1.107 @@ -54,8 +127,7 @@
   1.108  lemma if_eqvt:
   1.109    fixes pi::"'a prm"
   1.110    shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))"
   1.111 -apply(simp add: perm_fun_def)
   1.112 -done
   1.113 +  by (simp add: perm_fun_def)
   1.114  
   1.115  lemma imp_eqvt:
   1.116    shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
   1.117 @@ -82,13 +154,7 @@
   1.118    shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
   1.119    by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] expand_fun_eq)
   1.120  
   1.121 -(* permutation on units and products *)
   1.122 -primrec (unchecked perm_unit)
   1.123 -  "pi\<bullet>() = ()"
   1.124 -  
   1.125 -primrec (unchecked perm_prod)
   1.126 -  "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
   1.127 -
   1.128 +(* permutations on products *)
   1.129  lemma fst_eqvt:
   1.130    "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
   1.131   by (cases x) simp
   1.132 @@ -98,10 +164,6 @@
   1.133   by (cases x) simp
   1.134  
   1.135  (* permutation on lists *)
   1.136 -primrec (unchecked perm_list)
   1.137 -  nil_eqvt:  "pi\<bullet>[]     = []"
   1.138 -  cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
   1.139 -
   1.140  lemma append_eqvt:
   1.141    fixes pi :: "'x prm"
   1.142    and   l1 :: "'a list"
   1.143 @@ -115,41 +177,12 @@
   1.144    shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
   1.145    by (induct l) (simp_all add: append_eqvt)
   1.146  
   1.147 -(* permutation on options *)
   1.148 -
   1.149 -primrec (unchecked perm_option)
   1.150 -  some_eqvt:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
   1.151 -  none_eqvt:  "pi\<bullet>None    = None"
   1.152 -
   1.153 -(* a "private" copy of the option type used in the abstraction function *)
   1.154 -datatype 'a noption = nSome 'a | nNone
   1.155 -
   1.156 -primrec (unchecked perm_noption)
   1.157 -  nSome_eqvt: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
   1.158 -  nNone_eqvt: "pi\<bullet>nNone    = nNone"
   1.159 -
   1.160 -(* a "private" copy of the product type used in the nominal induct method *)
   1.161 -datatype ('a,'b) nprod = nPair 'a 'b
   1.162 -
   1.163 -primrec (unchecked perm_nprod)
   1.164 -  perm_nProd_def: "pi\<bullet>(nPair x1 x2)  = nPair (pi\<bullet>x1) (pi\<bullet>x2)"
   1.165 -
   1.166 -(* permutation on characters (used in strings) *)
   1.167 -defs (unchecked overloaded)
   1.168 -  perm_char_def: "pi\<bullet>(c::char) \<equiv> c"
   1.169 -
   1.170 +(* permutation on characters and strings *)
   1.171  lemma perm_string:
   1.172    fixes s::"string"
   1.173    shows "pi\<bullet>s = s"
   1.174 -by (induct s)(auto simp add: perm_char_def)
   1.175 -
   1.176 -(* permutation on ints *)
   1.177 -defs (unchecked overloaded)
   1.178 -  perm_int_def:    "pi\<bullet>(i::int) \<equiv> i"
   1.179 -
   1.180 -(* permutation on nats *)
   1.181 -defs (unchecked overloaded)
   1.182 -  perm_nat_def:    "pi\<bullet>(i::nat) \<equiv> i"
   1.183 +  by (induct s)(auto simp add: perm_char_def)
   1.184 +
   1.185  
   1.186  section {* permutation equality *}
   1.187  (*==============================*)
   1.188 @@ -221,46 +254,38 @@
   1.189  
   1.190  lemma supp_bool:
   1.191    fixes x  :: "bool"
   1.192 -  shows "supp (x) = {}"
   1.193 -  apply(case_tac "x")
   1.194 -  apply(simp_all add: supp_def)
   1.195 -done
   1.196 +  shows "supp x = {}"
   1.197 +  by (cases "x") (simp_all add: supp_def)
   1.198  
   1.199  lemma supp_some:
   1.200    fixes x :: "'a"
   1.201    shows "supp (Some x) = (supp x)"
   1.202 -  apply(simp add: supp_def)
   1.203 -  done
   1.204 +  by (simp add: supp_def)
   1.205  
   1.206  lemma supp_none:
   1.207    fixes x :: "'a"
   1.208    shows "supp (None) = {}"
   1.209 -  apply(simp add: supp_def)
   1.210 -  done
   1.211 +  by (simp add: supp_def)
   1.212  
   1.213  lemma supp_int:
   1.214    fixes i::"int"
   1.215    shows "supp (i) = {}"
   1.216 -  apply(simp add: supp_def perm_int_def)
   1.217 -  done
   1.218 +  by (simp add: supp_def perm_int_def)
   1.219  
   1.220  lemma supp_nat:
   1.221    fixes n::"nat"
   1.222 -  shows "supp (n) = {}"
   1.223 -  apply(simp add: supp_def perm_nat_def)
   1.224 -  done
   1.225 +  shows "(supp n) = {}"
   1.226 +  by (simp add: supp_def perm_nat_def)
   1.227  
   1.228  lemma supp_char:
   1.229    fixes c::"char"
   1.230 -  shows "supp (c) = {}"
   1.231 -  apply(simp add: supp_def perm_char_def)
   1.232 -  done
   1.233 +  shows "(supp c) = {}"
   1.234 +  by (simp add: supp_def perm_char_def)
   1.235    
   1.236  lemma supp_string:
   1.237    fixes s::"string"
   1.238 -  shows "supp (s) = {}"
   1.239 -apply(simp add: supp_def perm_string)
   1.240 -done
   1.241 +  shows "(supp s) = {}"
   1.242 +  by (simp add: supp_def perm_string)
   1.243  
   1.244  lemma fresh_set_empty:
   1.245    shows "a\<sharp>{}"
   1.246 @@ -344,7 +369,6 @@
   1.247    by (simp add: fresh_def supp_bool)
   1.248  
   1.249  text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
   1.250 -
   1.251  lemma fresh_unit_elim: 
   1.252    shows "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
   1.253    by (simp add: fresh_def supp_unit)
   1.254 @@ -393,7 +417,7 @@
   1.255  lemma fresh_star_prod_list:
   1.256    fixes xs::"'a list"
   1.257    shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
   1.258 -by (auto simp add: fresh_star_def fresh_prod)
   1.259 +  by (auto simp add: fresh_star_def fresh_prod)
   1.260  
   1.261  lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
   1.262