primrec (unchecked);
authorwenzelm
Sat May 20 23:36:56 2006 +0200 (2006-05-20)
changeset 196870a7c6d78ad6b
parent 19686 83611262823e
child 19688 877b763ded7e
primrec (unchecked);
src/HOL/Nominal/Examples/SN.thy
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Sat May 20 23:36:55 2006 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Sat May 20 23:36:56 2006 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4      TVar "string"
     1.5    | TArr "ty" "ty" (infix "\<rightarrow>" 200)
     1.6  
     1.7 -primrec
     1.8 +primrec (unchecked)
     1.9   "pi\<bullet>(TVar s) = TVar s"
    1.10   "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"
    1.11  
     2.1 --- a/src/HOL/Nominal/Nominal.thy	Sat May 20 23:36:55 2006 +0200
     2.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat May 20 23:36:56 2006 +0200
     2.3 @@ -42,15 +42,11 @@
     2.4    by (auto simp add: perm_set_def)
     2.5  
     2.6  (* permutation on units and products *)
     2.7 -defs (unchecked overloaded)
     2.8 -  perm_unit_def: "pi\<bullet>u == (case u of () \<Rightarrow> ())"
     2.9 -  perm_prod_def: "pi\<bullet>p == prod_rec (\<lambda>a b pi. (pi \<bullet> a, pi \<bullet> b)) p pi"
    2.10 -
    2.11 -lemma [simp]:
    2.12 -  "pi\<bullet>() = ()" by (simp add: perm_unit_def)
    2.13 -
    2.14 -lemma [simp]:
    2.15 -  "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)" by (simp add: perm_prod_def)
    2.16 +primrec (unchecked perm_unit)
    2.17 +  "pi\<bullet>()    = ()"
    2.18 +  
    2.19 +primrec (unchecked perm_prod)
    2.20 +  "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"
    2.21  
    2.22  lemma perm_fst:
    2.23    "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
    2.24 @@ -61,13 +57,9 @@
    2.25   by (cases x) simp
    2.26  
    2.27  (* permutation on lists *)
    2.28 -defs (unchecked overloaded)
    2.29 -  perm_list_def: "pi\<bullet>list \<equiv> list_rec (\<lambda>_. []) (\<lambda>x _ xs pi. pi\<bullet>x # xs pi) list pi"
    2.30 -
    2.31 -lemma
    2.32 -  perm_nil_def [simp]:  "pi\<bullet>[]     = []" and
    2.33 -  perm_cons_def [simp]: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    2.34 -  by (simp_all add: perm_list_def)
    2.35 +primrec (unchecked perm_list)
    2.36 +  perm_nil_def:  "pi\<bullet>[]     = []"
    2.37 +  perm_cons_def: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    2.38  
    2.39  lemma perm_append:
    2.40    fixes pi :: "'x prm"
    2.41 @@ -87,7 +79,7 @@
    2.42    perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    2.43  
    2.44  (* permutation on bools *)
    2.45 -primrec (perm_bool)
    2.46 +primrec (unchecked perm_bool)
    2.47    perm_true_def:  "pi\<bullet>True  = True"
    2.48    perm_false_def: "pi\<bullet>False = False"
    2.49  
    2.50 @@ -96,32 +88,22 @@
    2.51    by (cases b) auto
    2.52  
    2.53  (* permutation on options *)
    2.54 -defs (unchecked overloaded)
    2.55 -  perm_option_def: "pi\<bullet>opt \<equiv> option_rec (\<lambda>_. None) (\<lambda>x pi. Some (pi \<bullet> x)) opt pi"
    2.56 -lemma
    2.57 -  perm_some_def [simp]:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)" and
    2.58 -  perm_none_def [simp]:  "pi\<bullet>None    = None"
    2.59 -  by (simp_all add: perm_option_def)
    2.60 +primrec (unchecked perm_option)
    2.61 +  perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
    2.62 +  perm_none_def:  "pi\<bullet>None    = None"
    2.63  
    2.64  (* a "private" copy of the option type used in the abstraction function *)
    2.65  datatype 'a noption = nSome 'a | nNone
    2.66  
    2.67 -defs (unchecked overloaded)
    2.68 -  perm_noption_def: "pi\<bullet>opt \<equiv> noption_rec (\<lambda>x pi. nSome (pi \<bullet> x)) (\<lambda>_. nNone) opt pi"
    2.69 -
    2.70 -lemma
    2.71 -  perm_nSome_def [simp]: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)" and
    2.72 -  perm_nNone_def [simp]: "pi\<bullet>nNone    = nNone"
    2.73 -  by (simp_all add: perm_noption_def)
    2.74 +primrec (unchecked perm_noption)
    2.75 +  perm_nSome_def: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
    2.76 +  perm_nNone_def: "pi\<bullet>nNone    = nNone"
    2.77  
    2.78  (* a "private" copy of the product type used in the nominal induct method *)
    2.79  datatype ('a,'b) nprod = nPair 'a 'b
    2.80  
    2.81 -defs (unchecked overloaded)
    2.82 -  perm_nprod_def: "pi\<bullet>p \<equiv> nprod_rec (\<lambda>x1 x2 pi. nPair (pi \<bullet> x1) (pi \<bullet> x2)) p pi"
    2.83 -lemma [simp]:
    2.84 -  "pi\<bullet>(nPair x1 x2)  = nPair (pi\<bullet>x1) (pi\<bullet>x2)"
    2.85 -  by (simp add: perm_nprod_def)
    2.86 +primrec (unchecked perm_nprod)
    2.87 +  perm_nProd_def: "pi\<bullet>(nPair x1 x2)  = nPair (pi\<bullet>x1) (pi\<bullet>x2)"
    2.88  
    2.89  (* permutation on characters (used in strings) *)
    2.90  defs (unchecked overloaded)