tuned;
authorwenzelm
Thu Apr 28 11:47:01 2016 +0200 (2016-04-28 ago)
changeset 630670a8a75e400da
parent 63066 4b0ad6c5d1ca
child 63068 8b9401bfd9fd
tuned;
src/HOL/Induct/Sigma_Algebra.thy
src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
src/HOL/Unix/Unix.thy
src/HOL/ex/Functions.thy
     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.6    read:
     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.25 -  unlink:
    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.52 +| unlink:
    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.75    readdir:
    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