# HG changeset patch
# User wenzelm
# Date 1201298725 -3600
# Node ID 0cb35fa9c6fa8d56b34ca1da19d186355d9d0209
# Parent  4a584b094abaa67848324887759f413cc8b05f23
modernized primrec;

diff -r 4a584b094aba -r 0cb35fa9c6fa src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Fri Jan 25 23:05:24 2008 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Fri Jan 25 23:05:25 2008 +0100
@@ -16,39 +16,39 @@
   | App dB dB (infixl "\<degree>" 200)
   | Abs dB
 
-consts
-  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
+primrec
   lift :: "[dB, nat] => dB"
+where
+    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
+  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
+  | "lift (Abs s) k = Abs (lift s (k + 1))"
 
 primrec
-  "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
-  "lift (s \<degree> t) k = lift s k \<degree> lift t k"
-  "lift (Abs s) k = Abs (lift s (k + 1))"
-
-primrec  (* FIXME base names *)
-  subst_Var: "(Var i)[s/k] =
-    (if k < i then Var (i - 1) else if i = k then s else Var i)"
-  subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
-  subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
+  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
+where (* FIXME base names *)
+    subst_Var: "(Var i)[s/k] =
+      (if k < i then Var (i - 1) else if i = k then s else Var i)"
+  | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
+  | subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
 
 declare subst_Var [simp del]
 
 text {* Optimized versions of @{term subst} and @{term lift}. *}
 
-consts
-  substn :: "[dB, dB, nat] => dB"
+primrec
   liftn :: "[nat, dB, nat] => dB"
+where
+    "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
+  | "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
+  | "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
 
 primrec
-  "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
-  "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
-  "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
-
-primrec
-  "substn (Var i) s k =
-    (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
-  "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
-  "substn (Abs t) s k = Abs (substn t s (k + 1))"
+  substn :: "[dB, dB, nat] => dB"
+where
+    "substn (Var i) s k =
+      (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
+  | "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
+  | "substn (Abs t) s k = Abs (substn t s (k + 1))"
 
 
 subsection {* Beta-reduction *}
diff -r 4a584b094aba -r 0cb35fa9c6fa src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Fri Jan 25 23:05:24 2008 +0100
+++ b/src/HOL/Lambda/Type.thy	Fri Jan 25 23:05:25 2008 +0100
@@ -56,12 +56,14 @@
   "e \<turnstile> t \<degree> u : T"
   "e \<turnstile> Abs t : T"
 
-consts
+primrec
   typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
-
-abbreviation
-  funs :: "type list \<Rightarrow> type \<Rightarrow> type"  (infixr "=>>" 200) where
-  "Ts =>> T == foldr Fun Ts T"
+where
+    "typings e [] Ts = (Ts = [])"
+  | "typings e (t # ts) Ts =
+      (case Ts of
+        [] \<Rightarrow> False
+      | T # Ts \<Rightarrow> e \<turnstile> t : T \<and> typings e ts Ts)"
 
 abbreviation
   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
@@ -69,15 +71,14 @@
   "env ||- ts : Ts == typings env ts Ts"
 
 notation (latex)
-  funs  (infixr "\<Rrightarrow>" 200) and
   typings_rel  ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
 
-primrec
-  "(e \<tturnstile> [] : Ts) = (Ts = [])"
-  "(e \<tturnstile> (t # ts) : Ts) =
-    (case Ts of
-      [] \<Rightarrow> False
-    | T # Ts \<Rightarrow> e \<turnstile> t : T \<and> e \<tturnstile> ts : Ts)"
+abbreviation
+  funs :: "type list \<Rightarrow> type \<Rightarrow> type"  (infixr "=>>" 200) where
+  "Ts =>> T == foldr Fun Ts T"
+
+notation (latex)
+  funs  (infixr "\<Rrightarrow>" 200)
 
 
 subsection {* Some examples *}
@@ -123,11 +124,11 @@
   apply simp+
   done
 
-lemma rev_exhaust2 [case_names Nil snoc, extraction_expand]:
-  "(xs = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>ys y. xs = ys @ [y] \<Longrightarrow> P) \<Longrightarrow> P"
+lemma rev_exhaust2 [extraction_expand]:
+  obtains (Nil) "xs = []"  |  (snoc) ys y where "xs = ys @ [y]"
   -- {* Cannot use @{text rev_exhaust} from the @{text List}
     theory, since it is not constructive *}
-  apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> P")
+  apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> thesis")
   apply (erule_tac x="rev xs" in allE)
   apply simp
   apply (rule allI)
diff -r 4a584b094aba -r 0cb35fa9c6fa src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Fri Jan 25 23:05:24 2008 +0100
+++ b/src/HOL/Unix/Unix.thy	Fri Jan 25 23:05:25 2008 +0100
@@ -303,29 +303,29 @@
   to all kinds of system-calls.
 *}
 
-consts
+primrec
   uid_of :: "operation \<Rightarrow> uid"
-primrec
-  "uid_of (Read uid text path) = uid"
-  "uid_of (Write uid text path) = uid"
-  "uid_of (Chmod uid perms path) = uid"
-  "uid_of (Creat uid perms path) = uid"
-  "uid_of (Unlink uid path) = uid"
-  "uid_of (Mkdir uid path perms) = uid"
-  "uid_of (Rmdir uid path) = uid"
-  "uid_of (Readdir uid names path) = uid"
+where
+    "uid_of (Read uid text path) = uid"
+  | "uid_of (Write uid text path) = uid"
+  | "uid_of (Chmod uid perms path) = uid"
+  | "uid_of (Creat uid perms path) = uid"
+  | "uid_of (Unlink uid path) = uid"
+  | "uid_of (Mkdir uid path perms) = uid"
+  | "uid_of (Rmdir uid path) = uid"
+  | "uid_of (Readdir uid names path) = uid"
 
-consts
+primrec
   path_of :: "operation \<Rightarrow> path"
-primrec
-  "path_of (Read uid text path) = path"
-  "path_of (Write uid text path) = path"
-  "path_of (Chmod uid perms path) = path"
-  "path_of (Creat uid perms path) = path"
-  "path_of (Unlink uid path) = path"
-  "path_of (Mkdir uid perms path) = path"
-  "path_of (Rmdir uid path) = path"
-  "path_of (Readdir uid names path) = path"
+where
+    "path_of (Read uid text path) = path"
+  | "path_of (Write uid text path) = path"
+  | "path_of (Chmod uid perms path) = path"
+  | "path_of (Creat uid perms path) = path"
+  | "path_of (Unlink uid path) = path"
+  | "path_of (Mkdir uid perms path) = path"
+  | "path_of (Rmdir uid path) = path"
+  | "path_of (Readdir uid names path) = path"
 
 text {*
   \medskip Note that we have omitted explicit @{text Open} and @{text