some more primrec
authorhaftmann
Wed Jan 02 15:14:20 2008 +0100 (2008-01-02)
changeset 2576549580bd58a21
parent 25764 878c37886eed
child 25766 6960410f134d
some more primrec
src/HOL/Complex/ex/MIR.thy
src/HOL/Library/State_Monad.thy
src/HOL/SizeChange/Interpretation.thy
     1.1 --- a/src/HOL/Complex/ex/MIR.thy	Wed Jan 02 15:14:17 2008 +0100
     1.2 +++ b/src/HOL/Complex/ex/MIR.thy	Wed Jan 02 15:14:20 2008 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  declare real_of_int_floor_cancel [simp del]
     1.6  
     1.7 -fun alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where 
     1.8 +primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where 
     1.9    "alluopairs [] = []"
    1.10  | "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
    1.11  
    1.12 @@ -173,7 +173,7 @@
    1.13    | Mul int num | Floor num| CF int num num
    1.14  
    1.15    (* A size for num to make inductive proofs simpler*)
    1.16 -fun num_size :: "num \<Rightarrow> nat" where
    1.17 +primrec num_size :: "num \<Rightarrow> nat" where
    1.18   "num_size (C c) = 1"
    1.19  | "num_size (Bound n) = 1"
    1.20  | "num_size (Neg a) = 1 + num_size a"
    1.21 @@ -185,7 +185,7 @@
    1.22  | "num_size (Floor a) = 1 + num_size a"
    1.23  
    1.24    (* Semantics of numeral terms (num) *)
    1.25 -fun Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where
    1.26 +primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where
    1.27    "Inum bs (C c) = (real c)"
    1.28  | "Inum bs (Bound n) = bs!n"
    1.29  | "Inum bs (CN n c a) = (real c) * (bs!n) + (Inum bs a)"
    1.30 @@ -272,7 +272,7 @@
    1.31  by (induct p rule: fmsize.induct) simp_all
    1.32  
    1.33    (* Semantics of formulae (fm) *)
    1.34 -fun Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool" where
    1.35 +primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool" where
    1.36    "Ifm bs T = True"
    1.37  | "Ifm bs F = False"
    1.38  | "Ifm bs (Lt a) = (Inum bs a < 0)"
    1.39 @@ -322,39 +322,32 @@
    1.40  
    1.41  
    1.42    (* Quantifier freeness *)
    1.43 -consts qfree:: "fm \<Rightarrow> bool"
    1.44 -recdef qfree "measure size"
    1.45 +fun qfree:: "fm \<Rightarrow> bool" where
    1.46    "qfree (E p) = False"
    1.47 -  "qfree (A p) = False"
    1.48 -  "qfree (NOT p) = qfree p" 
    1.49 -  "qfree (And p q) = (qfree p \<and> qfree q)" 
    1.50 -  "qfree (Or  p q) = (qfree p \<and> qfree q)" 
    1.51 -  "qfree (Imp p q) = (qfree p \<and> qfree q)" 
    1.52 -  "qfree (Iff p q) = (qfree p \<and> qfree q)"
    1.53 -  "qfree p = True"
    1.54 +  | "qfree (A p) = False"
    1.55 +  | "qfree (NOT p) = qfree p" 
    1.56 +  | "qfree (And p q) = (qfree p \<and> qfree q)" 
    1.57 +  | "qfree (Or  p q) = (qfree p \<and> qfree q)" 
    1.58 +  | "qfree (Imp p q) = (qfree p \<and> qfree q)" 
    1.59 +  | "qfree (Iff p q) = (qfree p \<and> qfree q)"
    1.60 +  | "qfree p = True"
    1.61  
    1.62    (* Boundedness and substitution *)
    1.63 -consts 
    1.64 -  numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
    1.65 -  bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
    1.66 -  numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *)
    1.67 -  subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
    1.68 -primrec
    1.69 +primrec numbound0 :: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
    1.70    "numbound0 (C c) = True"
    1.71 -  "numbound0 (Bound n) = (n>0)"
    1.72 -  "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)"
    1.73 -  "numbound0 (Neg a) = numbound0 a"
    1.74 -  "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
    1.75 -  "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
    1.76 -  "numbound0 (Mul i a) = numbound0 a"
    1.77 -  "numbound0 (Floor a) = numbound0 a"
    1.78 -  "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)" 
    1.79 +  | "numbound0 (Bound n) = (n>0)"
    1.80 +  | "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)"
    1.81 +  | "numbound0 (Neg a) = numbound0 a"
    1.82 +  | "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
    1.83 +  | "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
    1.84 +  | "numbound0 (Mul i a) = numbound0 a"
    1.85 +  | "numbound0 (Floor a) = numbound0 a"
    1.86 +  | "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)" 
    1.87 +
    1.88  lemma numbound0_I:
    1.89    assumes nb: "numbound0 a"
    1.90    shows "Inum (b#bs) a = Inum (b'#bs) a"
    1.91 -using nb
    1.92 -by (induct a rule: numbound0.induct) (auto simp add: nth_pos2)
    1.93 -
    1.94 +  using nb by (induct a) (auto simp add: nth_pos2)
    1.95  
    1.96  lemma numbound0_gen: 
    1.97    assumes nb: "numbound0 t" and ti: "isint t (x#bs)"
    1.98 @@ -367,41 +360,41 @@
    1.99      by (simp add: isint_def)
   1.100  qed
   1.101  
   1.102 -primrec
   1.103 +primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
   1.104    "bound0 T = True"
   1.105 -  "bound0 F = True"
   1.106 -  "bound0 (Lt a) = numbound0 a"
   1.107 -  "bound0 (Le a) = numbound0 a"
   1.108 -  "bound0 (Gt a) = numbound0 a"
   1.109 -  "bound0 (Ge a) = numbound0 a"
   1.110 -  "bound0 (Eq a) = numbound0 a"
   1.111 -  "bound0 (NEq a) = numbound0 a"
   1.112 -  "bound0 (Dvd i a) = numbound0 a"
   1.113 -  "bound0 (NDvd i a) = numbound0 a"
   1.114 -  "bound0 (NOT p) = bound0 p"
   1.115 -  "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   1.116 -  "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   1.117 -  "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   1.118 -  "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   1.119 -  "bound0 (E p) = False"
   1.120 -  "bound0 (A p) = False"
   1.121 +  | "bound0 F = True"
   1.122 +  | "bound0 (Lt a) = numbound0 a"
   1.123 +  | "bound0 (Le a) = numbound0 a"
   1.124 +  | "bound0 (Gt a) = numbound0 a"
   1.125 +  | "bound0 (Ge a) = numbound0 a"
   1.126 +  | "bound0 (Eq a) = numbound0 a"
   1.127 +  | "bound0 (NEq a) = numbound0 a"
   1.128 +  | "bound0 (Dvd i a) = numbound0 a"
   1.129 +  | "bound0 (NDvd i a) = numbound0 a"
   1.130 +  | "bound0 (NOT p) = bound0 p"
   1.131 +  | "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   1.132 +  | "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   1.133 +  | "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   1.134 +  | "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   1.135 +  | "bound0 (E p) = False"
   1.136 +  | "bound0 (A p) = False"
   1.137  
   1.138  lemma bound0_I:
   1.139    assumes bp: "bound0 p"
   1.140    shows "Ifm (b#bs) p = Ifm (b'#bs) p"
   1.141 -using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   1.142 -by (induct p rule: bound0.induct) (auto simp add: nth_pos2)
   1.143 -
   1.144 -primrec
   1.145 + using bp numbound0_I [where b="b" and bs="bs" and b'="b'"]
   1.146 +  by (induct p) (auto simp add: nth_pos2)
   1.147 +
   1.148 +primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where
   1.149    "numsubst0 t (C c) = (C c)"
   1.150 -  "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   1.151 -  "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))"
   1.152 -  "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)"
   1.153 -  "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   1.154 -  "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   1.155 -  "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 
   1.156 -  "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   1.157 -  "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
   1.158 +  | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   1.159 +  | "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))"
   1.160 +  | "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)"
   1.161 +  | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   1.162 +  | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   1.163 +  | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 
   1.164 +  | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   1.165 +  | "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
   1.166  
   1.167  lemma numsubst0_I:
   1.168    shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   1.169 @@ -412,30 +405,29 @@
   1.170    shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   1.171    by (induct t) (simp_all add: nth_pos2 numbound0_I[OF nb, where b="b" and b'="b'"])
   1.172  
   1.173 -
   1.174 -primrec
   1.175 +primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   1.176    "subst0 t T = T"
   1.177 -  "subst0 t F = F"
   1.178 -  "subst0 t (Lt a) = Lt (numsubst0 t a)"
   1.179 -  "subst0 t (Le a) = Le (numsubst0 t a)"
   1.180 -  "subst0 t (Gt a) = Gt (numsubst0 t a)"
   1.181 -  "subst0 t (Ge a) = Ge (numsubst0 t a)"
   1.182 -  "subst0 t (Eq a) = Eq (numsubst0 t a)"
   1.183 -  "subst0 t (NEq a) = NEq (numsubst0 t a)"
   1.184 -  "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   1.185 -  "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   1.186 -  "subst0 t (NOT p) = NOT (subst0 t p)"
   1.187 -  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   1.188 -  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   1.189 -  "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   1.190 -  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   1.191 +  | "subst0 t F = F"
   1.192 +  | "subst0 t (Lt a) = Lt (numsubst0 t a)"
   1.193 +  | "subst0 t (Le a) = Le (numsubst0 t a)"
   1.194 +  | "subst0 t (Gt a) = Gt (numsubst0 t a)"
   1.195 +  | "subst0 t (Ge a) = Ge (numsubst0 t a)"
   1.196 +  | "subst0 t (Eq a) = Eq (numsubst0 t a)"
   1.197 +  | "subst0 t (NEq a) = NEq (numsubst0 t a)"
   1.198 +  | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   1.199 +  | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   1.200 +  | "subst0 t (NOT p) = NOT (subst0 t p)"
   1.201 +  | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   1.202 +  | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   1.203 +  | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   1.204 +  | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   1.205  
   1.206  lemma subst0_I: assumes qfp: "qfree p"
   1.207    shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"
   1.208    using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
   1.209    by (induct p) (simp_all add: nth_pos2 )
   1.210  
   1.211 -consts 
   1.212 +consts
   1.213    decrnum:: "num \<Rightarrow> num" 
   1.214    decr :: "fm \<Rightarrow> fm"
   1.215  
   1.216 @@ -495,21 +487,22 @@
   1.217  
   1.218  lemma numsubst0_numbound0: assumes nb: "numbound0 t"
   1.219    shows "numbound0 (numsubst0 t a)"
   1.220 -using nb by (induct a rule: numsubst0.induct, auto)
   1.221 +using nb by (induct a, auto)
   1.222  
   1.223  lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
   1.224    shows "bound0 (subst0 t p)"
   1.225 -using qf numsubst0_numbound0[OF nb] by (induct p  rule: subst0.induct, auto)
   1.226 +using qf numsubst0_numbound0[OF nb] by (induct p, auto)
   1.227  
   1.228  lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
   1.229  by (induct p, simp_all)
   1.230  
   1.231  
   1.232 -constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
   1.233 -  "djf f p q \<equiv> (if q=T then T else if q=F then f p else 
   1.234 +definition djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where
   1.235 +  "djf f p q = (if q=T then T else if q=F then f p else 
   1.236    (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or fp q))"
   1.237 -constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
   1.238 -  "evaldjf f ps \<equiv> foldr (djf f) ps F"
   1.239 +
   1.240 +definition evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where
   1.241 +  "evaldjf f ps = foldr (djf f) ps F"
   1.242  
   1.243  lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)"
   1.244  by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
     2.1 --- a/src/HOL/Library/State_Monad.thy	Wed Jan 02 15:14:17 2008 +0100
     2.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Jan 02 15:14:20 2008 +0100
     2.3 @@ -259,12 +259,13 @@
     2.4    lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
     2.5    "lift f x = return (f x)"
     2.6  
     2.7 -fun
     2.8 +primrec
     2.9    list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    2.10    "list f [] = id"
    2.11  | "list f (x#xs) = (do f x; list f xs done)"
    2.12  
    2.13 -fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
    2.14 +primrec
    2.15 +  list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
    2.16    "list_yield f [] = return []"
    2.17  | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    2.18    
    2.19 @@ -277,29 +278,29 @@
    2.20  lemma list_cong [fundef_cong, recdef_cong]:
    2.21    "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
    2.22      \<Longrightarrow> list f xs = list g ys"
    2.23 -proof (induct f xs arbitrary: g ys rule: list.induct)
    2.24 -  case 1 then show ?case by simp
    2.25 +proof (induct xs arbitrary: ys)
    2.26 +  case Nil then show ?case by simp
    2.27  next
    2.28 -  case (2 f x xs g)
    2.29 -  from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
    2.30 +  case (Cons x xs)
    2.31 +  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
    2.32    then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
    2.33 -  with 2 have "list f xs = list g xs" by auto
    2.34 -  with 2 have "list f (x # xs) = list g (x # xs)" by auto
    2.35 -  with 2 show "list f (x # xs) = list g ys" by auto
    2.36 +  with Cons have "list f xs = list g xs" by auto
    2.37 +  with Cons have "list f (x # xs) = list g (x # xs)" by auto
    2.38 +  with Cons show "list f (x # xs) = list g ys" by auto
    2.39  qed
    2.40  
    2.41  lemma list_yield_cong [fundef_cong, recdef_cong]:
    2.42    "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
    2.43      \<Longrightarrow> list_yield f xs = list_yield g ys"
    2.44 -proof (induct f xs arbitrary: g ys rule: list_yield.induct)
    2.45 -  case 1 then show ?case by simp
    2.46 +proof (induct xs arbitrary: ys)
    2.47 +  case Nil then show ?case by simp
    2.48  next
    2.49 -  case (2 f x xs g)
    2.50 -  from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
    2.51 +  case (Cons x xs)
    2.52 +  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
    2.53    then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
    2.54 -  with 2 have "list_yield f xs = list_yield g xs" by auto
    2.55 -  with 2 have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
    2.56 -  with 2 show "list_yield f (x # xs) = list_yield g ys" by auto
    2.57 +  with Cons have "list_yield f xs = list_yield g xs" by auto
    2.58 +  with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
    2.59 +  with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
    2.60  qed
    2.61  
    2.62  text {*
     3.1 --- a/src/HOL/SizeChange/Interpretation.thy	Wed Jan 02 15:14:17 2008 +0100
     3.2 +++ b/src/HOL/SizeChange/Interpretation.thy	Wed Jan 02 15:14:20 2008 +0100
     3.3 @@ -64,7 +64,7 @@
     3.4  where
     3.5    "in_cdesc (\<Gamma>, r, l) x y = (\<exists>q. x = r q \<and> y = l q \<and> \<Gamma> q)"
     3.6  
     3.7 -fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
     3.8 +primrec mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
     3.9  where
    3.10    "mk_rel [] x y = False"
    3.11  | "mk_rel (c#cs) x y =