author wenzelm Thu Apr 28 11:47:01 2016 +0200 (2016-04-28 ago) changeset 63067 0a8a75e400da parent 63066 4b0ad6c5d1ca child 63068 8b9401bfd9fd
tuned;
 src/HOL/Induct/Sigma_Algebra.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Mutilated_Checkerboard.thy file | annotate | diff | revisions src/HOL/Unix/Unix.thy file | annotate | diff | revisions src/HOL/ex/Functions.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Induct/Sigma_Algebra.thy	Thu Apr 28 11:34:26 2016 +0200
1.2 +++ b/src/HOL/Induct/Sigma_Algebra.thy	Thu Apr 28 11:47:01 2016 +0200
1.3 @@ -14,12 +14,13 @@
1.4    \<sigma>}-algebra over a given set of sets.
1.5  \<close>
1.6
1.7 -inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
1.8 +inductive_set \<sigma>_algebra :: "'a set set \<Rightarrow> 'a set set"
1.9 +  for A :: "'a set set"
1.10  where
1.11 -  basic: "a \<in> A \<Longrightarrow> a \<in> \<sigma>_algebra A"
1.12 +  basic: "a \<in> \<sigma>_algebra A" if "a \<in> A"
1.13  | UNIV: "UNIV \<in> \<sigma>_algebra A"
1.14 -| complement: "a \<in> \<sigma>_algebra A \<Longrightarrow> -a \<in> \<sigma>_algebra A"
1.15 -| Union: "(\<And>i::nat. a i \<in> \<sigma>_algebra A) \<Longrightarrow> (\<Union>i. a i) \<in> \<sigma>_algebra A"
1.16 +| complement: "- a \<in> \<sigma>_algebra A" if "a \<in> \<sigma>_algebra A"
1.17 +| Union: "(\<Union>i. a i) \<in> \<sigma>_algebra A" if "\<And>i::nat. a i \<in> \<sigma>_algebra A"
1.18
1.19  text \<open>
1.20    The following basic facts are consequences of the closure properties
```
```     2.1 --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Apr 28 11:34:26 2016 +0200
2.2 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Apr 28 11:47:01 2016 +0200
2.3 @@ -20,7 +20,7 @@
2.4    for A :: "'a set set"
2.5  where
2.6    empty: "{} \<in> tiling A"
2.7 -| Un: "a \<in> A \<Longrightarrow> t \<in> tiling A \<Longrightarrow> a \<subseteq> - t \<Longrightarrow> a \<union> t \<in> tiling A"
2.8 +| Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
2.9
2.10
2.11  text \<open>The union of two disjoint tilings is a tiling.\<close>
```
```     3.1 --- a/src/HOL/Unix/Unix.thy	Thu Apr 28 11:34:26 2016 +0200
3.2 +++ b/src/HOL/Unix/Unix.thy	Thu Apr 28 11:47:01 2016 +0200
3.3 @@ -342,46 +342,43 @@
3.4    ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
3.5  where
3.7 -    "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
3.8 -      root \<midarrow>(Read uid text path)\<rightarrow> root" |
3.9 -  "write":
3.10 -    "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>
3.11 -      root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root" |
3.12 -
3.13 -  chmod:
3.14 -    "access root path uid {} = Some file \<Longrightarrow>
3.15 -      uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
3.16 -      root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
3.17 -        (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root" |
3.18 -
3.19 -  creat:
3.20 -    "path = parent_path @ [name] \<Longrightarrow>
3.21 -      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
3.22 -      access root path uid {} = None \<Longrightarrow>
3.23 -      root \<midarrow>(Creat uid perms path)\<rightarrow> update path
3.24 -        (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root" |
3.26 -    "path = parent_path @ [name] \<Longrightarrow>
3.27 -      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
3.28 -      access root path uid {} = Some (Val plain) \<Longrightarrow>
3.29 -      root \<midarrow>(Unlink uid path)\<rightarrow> update path None root" |
3.30 -
3.31 -  mkdir:
3.32 -    "path = parent_path @ [name] \<Longrightarrow>
3.33 -      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
3.34 -      access root path uid {} = None \<Longrightarrow>
3.35 -      root \<midarrow>(Mkdir uid perms path)\<rightarrow> update path
3.36 -        (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root" |
3.37 +    "root \<midarrow>(Read uid text path)\<rightarrow> root"
3.38 +    if "access root path uid {Readable} = Some (Val (att, text))"
3.39 +| "write":
3.40 +    "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
3.41 +    if "access root path uid {Writable} = Some (Val (att, text'))"
3.42 +| chmod:
3.43 +    "root \<midarrow>(Chmod uid perms path)\<rightarrow>
3.44 +      update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
3.45 +    if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
3.46 +| creat:
3.47 +    "root \<midarrow>(Creat uid perms path)\<rightarrow>
3.48 +      update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
3.49 +    if "path = parent_path @ [name]"
3.50 +    and "access root parent_path uid {Writable} = Some (Env att parent)"
3.51 +    and "access root path uid {} = None"
3.53 +    "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
3.54 +    if "path = parent_path @ [name]"
3.55 +    and "access root parent_path uid {Writable} = Some (Env att parent)"
3.56 +    and "access root path uid {} = Some (Val plain)"
3.57 +| mkdir:
3.58 +    "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
3.59 +      update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
3.60 +    if "path = parent_path @ [name]"
3.61 +    and "access root parent_path uid {Writable} = Some (Env att parent)"
3.62 +    and "access root path uid {} = None"
3.63 +|
3.64    rmdir:
3.65 -    "path = parent_path @ [name] \<Longrightarrow>
3.66 -      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
3.67 -      access root path uid {} = Some (Env att' empty) \<Longrightarrow>
3.68 -      root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root" |
3.69 -
3.70 +    "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
3.71 +    if "path = parent_path @ [name]"
3.72 +    and "access root parent_path uid {Writable} = Some (Env att parent)"
3.73 +    and "access root path uid {} = Some (Env att' empty)"
3.74 +|
3.76 -    "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow>
3.77 -      names = dom dir \<Longrightarrow>
3.78 -      root \<midarrow>(Readdir uid names path)\<rightarrow> root"
3.79 +    "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
3.80 +    if "access root path uid {Readable} = Some (Env att dir)"
3.81 +    and "names = dom dir"
3.82
3.83  text \<open>
3.84    \<^medskip>
3.85 @@ -487,7 +484,7 @@
3.86    ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
3.87  where
3.88    nil: "root \<Midarrow>[]\<Rightarrow> root"
3.89 -| cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' \<Midarrow>xs\<Rightarrow> root'' \<Longrightarrow> root \<Midarrow>(x # xs)\<Rightarrow> root''"
3.90 +| cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
3.91
3.92  text \<open>
3.93    \<^medskip>
```
```     4.1 --- a/src/HOL/ex/Functions.thy	Thu Apr 28 11:34:26 2016 +0200
4.2 +++ b/src/HOL/ex/Functions.thy	Thu Apr 28 11:47:01 2016 +0200
4.3 @@ -125,8 +125,8 @@
4.4  where
4.5    "gcd3 x 0 = x"
4.6  | "gcd3 0 y = y"
4.7 -| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
4.8 -| "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
4.9 +| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
4.10 +| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y"
4.11    apply (case_tac x, case_tac a, auto)
4.12    apply (case_tac ba, auto)
4.13    done
```