# HG changeset patch # User wenzelm # Date 1452723918 -3600 # Node ID 1221f2a469450535f913714f05b00efc5f0ac8d0 # Parent 8ffc4d0e652dd3c40fd474eacf725493b2fdd0a2 tuned syntax; diff -r 8ffc4d0e652d -r 1221f2a46945 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Wed Jan 13 23:07:06 2016 +0100 +++ b/src/HOL/Unix/Unix.thy Wed Jan 13 23:25:18 2016 +0100 @@ -484,10 +484,10 @@ \ inductive transitions :: "file \ operation list \ file \ bool" - ("_ =_\ _" [90, 1000, 90] 100) + ("_ \_\ _" [90, 1000, 90] 100) where - nil: "root =[]\ root" -| cons: "root \x\ root' \ root' =xs\ root'' \ root =(x # xs)\ root''" + nil: "root \[]\ root" +| cons: "root \x\ root' \ root' \xs\ root'' \ root \(x # xs)\ root''" text \ \<^medskip> @@ -495,24 +495,24 @@ ones, according to the recursive structure of lists. \ -lemma transitions_nil_eq: "root =[]\ root' = (root = root')" +lemma transitions_nil_eq: "root \[]\ root' \ root = root'" proof - assume "root =[]\ root'" + assume "root \[]\ root'" then show "root = root'" by cases simp_all next assume "root = root'" - then show "root =[]\ root'" by (simp only: transitions.nil) + then show "root \[]\ root'" by (simp only: transitions.nil) qed lemma transitions_cons_eq: - "root =(x # xs)\ root'' = (\root'. root \x\ root' \ root' =xs\ root'')" + "root \(x # xs)\ root'' \ (\root'. root \x\ root' \ root' \xs\ root'')" proof - assume "root =(x # xs)\ root''" - then show "\root'. root \x\ root' \ root' =xs\ root''" + assume "root \(x # xs)\ root''" + then show "\root'. root \x\ root' \ root' \xs\ root''" by cases auto next - assume "\root'. root \x\ root' \ root' =xs\ root''" - then show "root =(x # xs)\ root''" + assume "\root'. root \x\ root' \ root' \xs\ root''" + then show "root \(x # xs)\ root''" by (blast intro: transitions.cons) qed @@ -522,18 +522,18 @@ transition system (see \secref{sec:unix-single-trans}). \ -lemma transitions_nilD: "root =[]\ root' \ root' = root" +lemma transitions_nilD: "root \[]\ root' \ root' = root" by (simp add: transitions_nil_eq) lemma transitions_consD: - assumes list: "root =(x # xs)\ root''" + assumes list: "root \(x # xs)\ root''" and hd: "root \x\ root'" - shows "root' =xs\ root''" + shows "root' \xs\ root''" proof - - from list obtain r' where r': "root \x\ r'" and root'': "r' =xs\ root''" + from list obtain r' where r': "root \x\ r'" and root'': "r' \xs\ root''" by cases simp_all from r' hd have "r' = root'" by (rule transition_uniq) - with root'' show "root' =xs\ root''" by simp + with root'' show "root' \xs\ root''" by simp qed text \ @@ -541,12 +541,12 @@ The following fact shows how an invariant @{term Q} of single transitions with property @{term P} may be transferred to iterated transitions. The proof is rather obvious by rule induction over the definition of @{term - "root =xs\ root'"}. + "root \xs\ root'"}. \ lemma transitions_invariant: assumes r: "\r x r'. r \x\ r' \ Q r \ P x \ Q r'" - and trans: "root =xs\ root'" + and trans: "root \xs\ root'" shows "Q root \ \x \ set xs. P x \ Q root'" using trans proof induct @@ -568,7 +568,7 @@ \ theorem transitions_type_safe: - assumes "root =xs\ root'" + assumes "root \xs\ root'" and "\att dir. root = Env att dir" shows "\att dir. root' = Env att dir" using transition_type_safe and assms @@ -608,7 +608,7 @@ certain state if there is a result state reached by an iterated transition. \ -definition "can_exec root xs = (\root'. root =xs\ root')" +definition "can_exec root xs \ (\root'. root \xs\ root')" lemma can_exec_nil: "can_exec root []" unfolding can_exec_def by (blast intro: transitions.intros) @@ -624,7 +624,7 @@ \ lemma can_exec_snocD: "can_exec root (xs @ [y]) - \ \root' root''. root =xs\ root' \ root' \y\ root''" + \ \root' root''. root \xs\ root' \ root' \y\ root''" proof (induct xs arbitrary: root) case Nil then show ?case @@ -633,12 +633,12 @@ case (Cons x xs) from \can_exec root ((x # xs) @ [y])\ obtain r root'' where x: "root \x\ r" and - xs_y: "r =(xs @ [y])\ root''" + xs_y: "r \(xs @ [y])\ root''" by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq) from xs_y Cons.hyps obtain root' r' - where xs: "r =xs\ root'" and y: "root' \y\ r'" + where xs: "r \xs\ root'" and y: "root' \y\ r'" unfolding can_exec_def by blast - from x xs have "root =(x # xs)\ root'" + from x xs have "root \(x # xs)\ root'" by (rule transitions.cons) with y show ?case by blast qed @@ -744,9 +744,9 @@ theorem general_procedure: assumes cannot_y: "\r r'. Q r \ r \y\ r' \ False" - and init_inv: "\root. init users =bs\ root \ Q root" + and init_inv: "\root. init users \bs\ root \ Q root" and preserve_inv: "\r x r'. r \x\ r' \ Q r \ P x \ Q r'" - and init_result: "init users =bs\ root" + and init_result: "init users \bs\ root" shows "\ (\xs. (\x \ set xs. P x) \ can_exec root (xs @ [y]))" proof - { @@ -754,7 +754,7 @@ assume Ps: "\x \ set xs. P x" assume can_exec: "can_exec root (xs @ [y])" then obtain root' root'' where - xs: "root =xs\ root'" and y: "root' \y\ root''" + xs: "root \xs\ root'" and y: "root' \y\ root''" by (blast dest: can_exec_snocD) from init_result have "Q root" by (rule init_inv) from preserve_inv xs this Ps have "Q root'" @@ -827,7 +827,7 @@ \ definition - "invariant root path = + "invariant root path \ (\att dir. access root path user\<^sub>1 {} = Some (Env att dir) \ dir \ empty \ user\<^sub>1 \ owner att \ @@ -876,7 +876,7 @@ qed lemma - assumes init: "init users =bogus\ root" + assumes init: "init users \bogus\ root" shows init_invariant: "invariant root bogus_path" supply eval = facts access_def init_def using init @@ -1042,7 +1042,7 @@ \ corollary - assumes bogus: "init users =bogus\ root" + assumes bogus: "init users \bogus\ root" shows "\ (\xs. (\x \ set xs. uid_of x = user\<^sub>1) \ can_exec root (xs @ [Rmdir user\<^sub>1 [user\<^sub>1, name\<^sub>1]]))" proof -