summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 25 Jan 2008 23:05:25 +0100 | |

changeset 25974 | 0cb35fa9c6fa |

parent 25973 | 4a584b094aba |

child 25975 | bcb1e9b7644b |

modernized primrec;

--- 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