--- 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 *}
--- 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)
--- 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