src/HOL/Library/Option_ord.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon, 26 Mar 2018 16:14:16 +0200
changeset 67951 655aa11359dc
parent 67829 2a6ef5ba4822
child 68980 5717fbc55521
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Option_ord.thy
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     3
*)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Canonical order on option type\<close>
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     6
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     7
theory Option_ord
67006
b1278ed3cd46 prefer main entry points of HOL;
wenzelm
parents: 66453
diff changeset
     8
imports Main
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
     9
begin
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    10
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    11
notation
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    12
  bot ("\<bottom>") and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    13
  top ("\<top>") and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    14
  inf  (infixl "\<sqinter>" 70) and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    15
  sup  (infixl "\<squnion>" 65) and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    16
  Inf  ("\<Sqinter>_" [900] 900) and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    17
  Sup  ("\<Squnion>_" [900] 900)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    18
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 60679
diff changeset
    19
syntax
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    20
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    21
  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    22
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    23
  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    24
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
    25
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    26
instantiation option :: (preorder) preorder
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    27
begin
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    28
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    29
definition less_eq_option where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 30662
diff changeset
    30
  "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    31
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    32
definition less_option where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 30662
diff changeset
    33
  "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    34
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    35
lemma less_eq_option_None [simp]: "None \<le> x"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    36
  by (simp add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    37
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    38
lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    39
  by simp
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    40
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    41
lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    42
  by (cases x) (simp_all add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    43
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    44
lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    45
  by (simp add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    46
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    47
lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    48
  by (simp add: less_eq_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    49
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    50
lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    51
  by (simp add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    52
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    53
lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    54
  by (cases x) (simp_all add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    55
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    56
lemma less_option_None_Some [simp]: "None < Some x"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    57
  by (simp add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    58
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    59
lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    60
  by simp
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    61
26258
20dfaa28e5e5 *** empty log message ***
haftmann
parents: 26241
diff changeset
    62
lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    63
  by (simp add: less_option_def)
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    64
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    65
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    66
  by standard
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    67
    (auto simp add: less_eq_option_def less_option_def less_le_not_le
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    68
      elim: order_trans split: option.splits)
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    69
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    70
end
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    71
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    72
instance option :: (order) order
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    73
  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    74
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    75
instance option :: (linorder) linorder
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    76
  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    77
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 49190
diff changeset
    78
instantiation option :: (order) order_bot
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    79
begin
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    80
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    81
definition bot_option where "\<bottom> = None"
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    82
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    83
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    84
  by standard (simp add: bot_option_def)
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    85
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    86
end
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    87
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 49190
diff changeset
    88
instantiation option :: (order_top) order_top
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    89
begin
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    90
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    91
definition top_option where "\<top> = Some \<top>"
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    92
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    93
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    94
  by standard (simp add: top_option_def less_eq_option_def split: option.split)
26241
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    95
b7d8c2338585 added Option_ord.thy
haftmann
parents:
diff changeset
    96
end
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
    97
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    98
instance option :: (wellorder) wellorder
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    99
proof
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   100
  fix P :: "'a option \<Rightarrow> bool"
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   101
  fix z :: "'a option"
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   102
  assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   103
  have "P None" by (rule H) simp
67091
1393c2340eec more symbols;
wenzelm
parents: 67006
diff changeset
   104
  then have P_Some [case_names Some]: "P z" if "\<And>x. z = Some x \<Longrightarrow> (P \<circ> Some) x" for z
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   105
    using \<open>P None\<close> that by (cases z) simp_all
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   106
  show "P z"
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   107
  proof (cases z rule: P_Some)
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   108
    case (Some w)
67091
1393c2340eec more symbols;
wenzelm
parents: 67006
diff changeset
   109
    show "(P \<circ> Some) w"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   110
    proof (induct rule: less_induct)
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   111
      case (less x)
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   112
      have "P (Some x)"
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   113
      proof (rule H)
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   114
        fix y :: "'a option"
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   115
        assume "y < Some x"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   116
        show "P y"
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   117
        proof (cases y rule: P_Some)
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   118
          case (Some v)
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   119
          with \<open>y < Some x\<close> have "v < x" by simp
67091
1393c2340eec more symbols;
wenzelm
parents: 67006
diff changeset
   120
          with less show "(P \<circ> Some) v" .
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   121
        qed
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   122
      qed
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   123
      then show ?case by simp
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   124
    qed
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   125
  qed
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   126
qed
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   127
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   128
instantiation option :: (inf) inf
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   129
begin
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   130
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   131
definition inf_option where
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   132
  "x \<sqinter> y = (case x of None \<Rightarrow> None | Some x \<Rightarrow> (case y of None \<Rightarrow> None | Some y \<Rightarrow> Some (x \<sqinter> y)))"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   133
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   134
lemma inf_None_1 [simp, code]: "None \<sqinter> y = None"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   135
  by (simp add: inf_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   136
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   137
lemma inf_None_2 [simp, code]: "x \<sqinter> None = None"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   138
  by (cases x) (simp_all add: inf_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   139
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   140
lemma inf_Some [simp, code]: "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   141
  by (simp add: inf_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   142
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   143
instance ..
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   144
30662
396be15b95d5 added instances for bot, top, wellorder
haftmann
parents: 28562
diff changeset
   145
end
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   146
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   147
instantiation option :: (sup) sup
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   148
begin
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   149
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   150
definition sup_option where
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   151
  "x \<squnion> y = (case x of None \<Rightarrow> y | Some x' \<Rightarrow> (case y of None \<Rightarrow> x | Some y \<Rightarrow> Some (x' \<squnion> y)))"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   152
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   153
lemma sup_None_1 [simp, code]: "None \<squnion> y = y"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   154
  by (simp add: sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   155
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   156
lemma sup_None_2 [simp, code]: "x \<squnion> None = x"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   157
  by (cases x) (simp_all add: sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   158
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   159
lemma sup_Some [simp, code]: "Some x \<squnion> Some y = Some (x \<squnion> y)"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   160
  by (simp add: sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   161
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   162
instance ..
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   163
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   164
end
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   165
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   166
instance option :: (semilattice_inf) semilattice_inf
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   167
proof
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   168
  fix x y z :: "'a option"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   169
  show "x \<sqinter> y \<le> x"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   170
    by (cases x, simp_all, cases y, simp_all)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   171
  show "x \<sqinter> y \<le> y"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   172
    by (cases x, simp_all, cases y, simp_all)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   173
  show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   174
    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   175
qed
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   176
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   177
instance option :: (semilattice_sup) semilattice_sup
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   178
proof
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   179
  fix x y z :: "'a option"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   180
  show "x \<le> x \<squnion> y"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   181
    by (cases x, simp_all, cases y, simp_all)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   182
  show "y \<le> x \<squnion> y"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   183
    by (cases x, simp_all, cases y, simp_all)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   184
  fix x y z :: "'a option"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   185
  show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   186
    by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   187
qed
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   188
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   189
instance option :: (lattice) lattice ..
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   191
instance option :: (lattice) bounded_lattice_bot ..
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   192
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   193
instance option :: (bounded_lattice_top) bounded_lattice_top ..
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   194
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   195
instance option :: (bounded_lattice_top) bounded_lattice ..
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   196
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   197
instance option :: (distrib_lattice) distrib_lattice
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   198
proof
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   199
  fix x y z :: "'a option"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   200
  show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   201
    by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   202
qed
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   203
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   204
instantiation option :: (complete_lattice) complete_lattice
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   205
begin
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   206
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   207
definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   208
  "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   209
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   210
lemma None_in_Inf [simp]: "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   211
  by (simp add: Inf_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   212
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   213
definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   214
  "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   215
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   216
lemma empty_Sup [simp]: "\<Squnion>{} = None"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   217
  by (simp add: Sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   218
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   219
lemma singleton_None_Sup [simp]: "\<Squnion>{None} = None"
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   220
  by (simp add: Sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   221
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   222
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   223
proof
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   224
  fix x :: "'a option" and A
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   225
  assume "x \<in> A"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   226
  then show "\<Sqinter>A \<le> x"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   227
    by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   228
next
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   229
  fix z :: "'a option" and A
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   230
  assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   231
  show "z \<le> \<Sqinter>A"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   232
  proof (cases z)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   233
    case None then show ?thesis by simp
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   234
  next
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   235
    case (Some y)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   236
    show ?thesis
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   237
      by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   238
  qed
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   239
next
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   240
  fix x :: "'a option" and A
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   241
  assume "x \<in> A"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   242
  then show "x \<le> \<Squnion>A"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   243
    by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   244
next
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   245
  fix z :: "'a option" and A
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   246
  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   247
  show "\<Squnion>A \<le> z "
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   248
  proof (cases z)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   249
    case None
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   250
    with * have "\<And>x. x \<in> A \<Longrightarrow> x = None" by (auto dest: less_eq_option_None_is_None)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   251
    then have "A = {} \<or> A = {None}" by blast
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   252
    then show ?thesis by (simp add: Sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   253
  next
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   254
    case (Some y)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   255
    from * have "\<And>w. Some w \<in> A \<Longrightarrow> Some w \<le> z" .
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   256
    with Some have "\<And>w. w \<in> Option.these A \<Longrightarrow> w \<le> y"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   257
      by (simp add: in_these_eq)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   258
    then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   259
    with Some show ?thesis by (simp add: Sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   260
  qed
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 49190
diff changeset
   261
next
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 49190
diff changeset
   262
  show "\<Squnion>{} = (\<bottom>::'a option)"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   263
    by (auto simp: bot_option_def)
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 49190
diff changeset
   264
  show "\<Sqinter>{} = (\<top>::'a option)"
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   265
    by (auto simp: top_option_def Inf_option_def)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   266
qed
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   267
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   268
end
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   269
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   270
lemma Some_Inf:
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   271
  "Some (\<Sqinter>A) = \<Sqinter>(Some ` A)"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   272
  by (auto simp add: Inf_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   273
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   274
lemma Some_Sup:
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   275
  "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>A) = \<Squnion>(Some ` A)"
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   276
  by (auto simp add: Sup_option_def)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   277
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   278
lemma Some_INF:
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   279
  "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 52729
diff changeset
   280
  using Some_Inf [of "f ` A"] by (simp add: comp_def)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   281
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   282
lemma Some_SUP:
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   283
  "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 52729
diff changeset
   284
  using Some_Sup [of "f ` A"] by (simp add: comp_def)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   285
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   286
lemma option_Inf_Sup: "INFIMUM (A::('a::complete_distrib_lattice option) set set) Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   287
proof (cases "{} \<in> A")
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   288
  case True
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   289
  then show ?thesis
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   290
    by (rule INF_lower2, simp_all)
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   291
next
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   292
  case False
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   293
  from this have X: "{} \<notin> A"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   294
    by simp
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   295
  then show ?thesis
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   296
  proof (cases "{None} \<in> A")
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   297
    case True
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   298
    then show ?thesis
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   299
      by (rule INF_lower2, simp_all)
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   300
  next
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   301
    case False
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   302
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   303
    {fix y
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   304
      assume A: "y \<in> A"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   305
      have "Sup (y - {None}) = Sup y"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   306
        by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   307
      from A and this have "(\<exists>z. y - {None} = z - {None} \<and> z \<in> A) \<and> \<Squnion>y = \<Squnion>(y - {None})"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   308
        by auto
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   309
    }
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   310
    from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})"
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   311
      by (auto simp add: image_def)
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   312
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   313
    have [simp]: "\<And>y. y \<in> A \<Longrightarrow> \<exists>ya. {ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} 
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   314
          = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   315
      by (rule exI, auto)
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   316
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   317
    have [simp]: "\<And>y. y \<in> A \<Longrightarrow>
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   318
         (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} 
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   319
          = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   320
      apply (safe, blast)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   321
      by (rule arg_cong [of _ _ Sup], auto)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   322
    {fix y
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   323
      assume [simp]: "y \<in> A"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   324
      have "\<exists>x. (\<exists>y. x = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} = \<Squnion>x"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   325
      and "\<exists>x. (\<exists>y. x = y - {None} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} = \<Squnion>{y. \<exists>xa. xa \<in> x \<and> (\<exists>y. xa = Some y) \<and> y = the xa}"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   326
         apply (rule exI [of _ "{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"], simp)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   327
        by (rule exI [of _ "y - {None}"], simp)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   328
    }
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   329
    from this have C: "(\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} =  (Sup ` {the ` (y - {None}) |y. y \<in> A})"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   330
      by (simp add: image_def Option.these_def, safe, simp_all)
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   331
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   332
    have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False"
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   333
      by (drule spec [of _ "\<lambda> Y . SOME x . x \<in> Y"], simp add: X some_in_eq)
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   334
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   335
    define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   336
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   337
    have G: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> x . x \<in> Y - {None}"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   338
      by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   339
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   340
    have F: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> (Y - {None})"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   341
      by (metis F_def G empty_iff some_in_eq)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   342
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   343
    have "Some \<bottom> \<le> Inf (F ` A)"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   344
      by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff 
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   345
          less_eq_option_Some singletonI)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   346
      
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   347
    from this have "Inf (F ` A) \<noteq> None"
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   348
      by (cases "\<Sqinter>x\<in>A. F x", simp_all)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   349
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   350
    from this have "Inf (F ` A) \<noteq> None \<and> Inf (F ` A) \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   351
      using F by auto
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   352
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   353
    from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   354
      by blast
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   355
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   356
    from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   357
      by blast
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   358
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   359
    have [simp]: "((\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x) = None) = False"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   360
      by (metis (no_types, lifting) E Sup_option_def \<open>\<exists>x. x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}\<close> 
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   361
          ex_in_conv option.simps(3))
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   362
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   363
    have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}) 
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   364
        = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   365
      by (metis image_image these_image_Some_eq)
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   366
    {
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   367
      fix f
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   368
      assume A: "\<And> Y . (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<Longrightarrow> f Y \<in> Y"
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   369
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   370
      have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (xa - {None}))"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   371
        by  (simp add: image_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   372
      from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x\<in>A. f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (x - {None}))"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   373
        by blast
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   374
      have "\<And>xa. xa \<in> A \<Longrightarrow> f (the ` (xa - {None})) = f {y. \<exists>a \<in> xa - {None}. y = the a} \<and> xa \<in> A"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   375
        by (simp add: image_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   376
      from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x. f (the ` (xa - {None})) = f {y. \<exists>a\<in>x - {None}. y = the a} \<and> x \<in> A"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   377
        by blast
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   378
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   379
      {
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   380
        fix Y
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   381
        have "Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   382
          using A [of "the ` (Y - {None})"] apply (simp add: image_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   383
          using option.collapse by fastforce
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   384
      }
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   385
      from this have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   386
        by blast
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   387
      have [simp]: "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A}"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   388
        by (simp add: Setcompr_eq_image)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   389
      
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   390
      have [simp]: "\<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A} = \<Sqinter>x"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   391
        apply (rule exI [of _ "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}"], safe)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   392
        by (rule exI [of _ "(\<lambda> Y . Some (f (the ` (Y - {None})))) "], safe, simp_all)
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   393
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   394
      {
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   395
        fix xb
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   396
        have "xb \<in> A \<Longrightarrow> (\<Sqinter>x\<in>{{ya. \<exists>x\<in>y - {None}. ya = the x} |y. y \<in> A}. f x) \<le> f {y. \<exists>x\<in>xb - {None}. y = the x}"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   397
          apply (rule INF_lower2 [of "{y. \<exists>x\<in>xb - {None}. y = the x}"])
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   398
          by blast+
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   399
      }
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   400
      from this have [simp]: "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   401
        apply (simp add: Inf_option_def image_def Option.these_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   402
        by (rule Inf_greatest, clarsimp)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   403
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   404
      have [simp]: "the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None})))) \<in> Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   405
        apply (simp add:  Option.these_def image_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   406
        apply (rule exI [of _ "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))"], simp)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   407
        by (simp add: Inf_option_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   408
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   409
      have "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   410
        by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   411
    }
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   412
    from this have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   413
      (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   414
      by blast
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   415
    
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   416
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   417
    have [simp]: "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow>  x \<noteq> {} \<and> x \<noteq> {None}"
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   418
      using F by fastforce
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   419
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   420
    have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   421
      by (subst A, simp)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   422
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   423
    also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. if x = {} \<or> x = {None} then None else Some (\<Squnion>Option.these x))"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   424
      by (simp add: Sup_option_def)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   425
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   426
    also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   427
      using G by fastforce
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   428
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   429
    also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   430
      by (simp add: Inf_option_def, safe)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   431
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   432
    also have "... =  Some (\<Sqinter> ((\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   433
      by (simp add: B)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   434
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   435
    also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y \<in> A}))"
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   436
      by (unfold C, simp)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   437
    thm Inf_Sup
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   438
    also have "... = Some (\<Squnion>x\<in>{f ` {the ` (y - {None}) |y. y \<in> A} |f. \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y}. \<Sqinter>x) "
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   439
      by (simp add: Inf_Sup)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   440
  
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   441
    also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
67951
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   442
    proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   443
      case None
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   444
      then show ?thesis by (simp add: less_eq_option_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   445
    next
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   446
      case (Some a)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   447
      then show ?thesis
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   448
        apply simp
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   449
        apply (rule Sup_least, safe)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   450
        apply (simp add: Sup_option_def)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   451
        apply (cases "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   452
        by (drule X, simp)
655aa11359dc Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
Manuel Eberl <eberlm@in.tum.de>
parents: 67829
diff changeset
   453
    qed
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   454
    finally show ?thesis by simp
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   455
  qed
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   456
qed
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   457
67829
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   458
instance option :: (complete_distrib_lattice) complete_distrib_lattice
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   459
  by (standard, simp add: option_Inf_Sup)
2a6ef5ba4822 Changes to complete distributive lattices due to Viorel Preoteasa
Manuel Eberl <eberlm@in.tum.de>
parents: 67091
diff changeset
   460
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   461
instance option :: (complete_linorder) complete_linorder ..
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   462
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   463
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   464
no_notation
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   465
  bot ("\<bottom>") and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   466
  top ("\<top>") and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   467
  inf  (infixl "\<sqinter>" 70) and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   468
  sup  (infixl "\<squnion>" 65) and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   469
  Inf  ("\<Sqinter>_" [900] 900) and
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   470
  Sup  ("\<Squnion>_" [900] 900)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   471
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 60679
diff changeset
   472
no_syntax
49190
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   473
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   474
  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   475
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   476
  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   477
e1e1d427747d lattice instances for option type
haftmann
parents: 43815
diff changeset
   478
end