--- a/src/HOL/Induct/Sigma_Algebra.thy Thu Apr 28 11:34:26 2016 +0200
+++ b/src/HOL/Induct/Sigma_Algebra.thy Thu Apr 28 11:47:01 2016 +0200
@@ -14,12 +14,13 @@
\<sigma>}-algebra over a given set of sets.
\<close>
-inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
+inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set"
+ for A :: "'a set set"
where
- basic: "a \<in> A \<Longrightarrow> a \<in> \<sigma>_algebra A"
+ basic: "a \<in> \<sigma>_algebra A" if "a \<in> A"
| UNIV: "UNIV \<in> \<sigma>_algebra A"
-| complement: "a \<in> \<sigma>_algebra A \<Longrightarrow> -a \<in> \<sigma>_algebra A"
-| Union: "(\<And>i::nat. a i \<in> \<sigma>_algebra A) \<Longrightarrow> (\<Union>i. a i) \<in> \<sigma>_algebra A"
+| complement: "- a \<in> \<sigma>_algebra A" if "a \<in> \<sigma>_algebra A"
+| Union: "(\<Union>i. a i) \<in> \<sigma>_algebra A" if "\<And>i::nat. a i \<in> \<sigma>_algebra A"
text \<open>
The following basic facts are consequences of the closure properties
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Apr 28 11:34:26 2016 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Apr 28 11:47:01 2016 +0200
@@ -20,7 +20,7 @@
for A :: "'a set set"
where
empty: "{} \<in> tiling A"
-| Un: "a \<in> A \<Longrightarrow> t \<in> tiling A \<Longrightarrow> a \<subseteq> - t \<Longrightarrow> a \<union> t \<in> tiling A"
+| Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
text \<open>The union of two disjoint tilings is a tiling.\<close>
--- a/src/HOL/Unix/Unix.thy Thu Apr 28 11:34:26 2016 +0200
+++ b/src/HOL/Unix/Unix.thy Thu Apr 28 11:47:01 2016 +0200
@@ -342,46 +342,43 @@
("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
where
read:
- "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
- root \<midarrow>(Read uid text path)\<rightarrow> root" |
- "write":
- "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>
- root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root" |
-
- chmod:
- "access root path uid {} = Some file \<Longrightarrow>
- uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
- root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
- (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root" |
-
- creat:
- "path = parent_path @ [name] \<Longrightarrow>
- access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
- access root path uid {} = None \<Longrightarrow>
- root \<midarrow>(Creat uid perms path)\<rightarrow> update path
- (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root" |
- unlink:
- "path = parent_path @ [name] \<Longrightarrow>
- access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
- access root path uid {} = Some (Val plain) \<Longrightarrow>
- root \<midarrow>(Unlink uid path)\<rightarrow> update path None root" |
-
- mkdir:
- "path = parent_path @ [name] \<Longrightarrow>
- access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
- access root path uid {} = None \<Longrightarrow>
- root \<midarrow>(Mkdir uid perms path)\<rightarrow> update path
- (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root" |
+ "root \<midarrow>(Read uid text path)\<rightarrow> root"
+ if "access root path uid {Readable} = Some (Val (att, text))"
+| "write":
+ "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
+ if "access root path uid {Writable} = Some (Val (att, text'))"
+| chmod:
+ "root \<midarrow>(Chmod uid perms path)\<rightarrow>
+ update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
+ if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
+| creat:
+ "root \<midarrow>(Creat uid perms path)\<rightarrow>
+ update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = None"
+| unlink:
+ "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = Some (Val plain)"
+| mkdir:
+ "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
+ update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = None"
+|
rmdir:
- "path = parent_path @ [name] \<Longrightarrow>
- access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
- access root path uid {} = Some (Env att' empty) \<Longrightarrow>
- root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root" |
-
+ "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = Some (Env att' empty)"
+|
readdir:
- "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow>
- names = dom dir \<Longrightarrow>
- root \<midarrow>(Readdir uid names path)\<rightarrow> root"
+ "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
+ if "access root path uid {Readable} = Some (Env att dir)"
+ and "names = dom dir"
text \<open>
\<^medskip>
@@ -487,7 +484,7 @@
("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
where
nil: "root \<Midarrow>[]\<Rightarrow> root"
-| cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''"
+| cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
text \<open>
\<^medskip>
--- a/src/HOL/ex/Functions.thy Thu Apr 28 11:34:26 2016 +0200
+++ b/src/HOL/ex/Functions.thy Thu Apr 28 11:47:01 2016 +0200
@@ -125,8 +125,8 @@
where
"gcd3 x 0 = x"
| "gcd3 0 y = y"
-| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
-| "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
+| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
+| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y"
apply (case_tac x, case_tac a, auto)
apply (case_tac ba, auto)
done