src/HOL/MicroJava/BV/Err.thy
author nipkow
Mon, 26 Mar 2001 19:37:31 +0200
changeset 11225 01181fdbc9f0
parent 11085 b830bf10bf71
child 11549 e7265e70fd7c
permissions -rw-r--r--
simplified proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     1
(*  Title:      HOL/BCV/Err.thy
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     2
    ID:         $Id$
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     3
    Author:     Tobias Nipkow
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     4
    Copyright   2000 TUM
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     5
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     6
The error type
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     7
*)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     8
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
     9
header "The Error Type"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    10
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    11
theory Err = Semilat:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    12
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    13
datatype 'a err = Err | OK 'a
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    14
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    15
types 'a ebinop = "'a => 'a => 'a err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    16
      'a esl =    "'a set * 'a ord * 'a ebinop"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    17
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    18
consts
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    19
  ok_val :: "'a err => 'a"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    20
primrec
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    21
  "ok_val (OK x) = x"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    22
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    23
constdefs
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    24
 lift :: "('a => 'b err) => ('a err => 'b err)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    25
"lift f e == case e of Err => Err | OK x => f x"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    26
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    27
 lift2 :: "('a => 'b => 'c err) => 'a err => 'b err => 'c err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    28
"lift2 f e1 e2 ==
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    29
 case e1 of Err  => Err
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    30
          | OK x => (case e2 of Err => Err | OK y => f x y)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    31
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    32
 le :: "'a ord => 'a err ord"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    33
"le r e1 e2 ==
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    34
        case e2 of Err => True |
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    35
                   OK y => (case e1 of Err => False | OK x => x <=_r y)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    36
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    37
 sup :: "('a => 'b => 'c) => ('a err => 'b err => 'c err)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    38
"sup f == lift2(%x y. OK(x +_f y))"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    39
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    40
 err :: "'a set => 'a err set"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    41
"err A == insert Err {x . ? y:A. x = OK y}"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    42
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    43
 esl :: "'a sl => 'a esl"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    44
"esl == %(A,r,f). (A,r, %x y. OK(f x y))"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    45
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    46
 sl :: "'a esl => 'a err sl"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    47
"sl == %(A,r,f). (err A, le r, lift2 f)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    48
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    49
syntax
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    50
 err_semilat :: "'a esl => bool"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    51
translations
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    52
"err_semilat L" == "semilat(Err.sl L)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    53
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    54
10812
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10496
diff changeset
    55
consts
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10496
diff changeset
    56
  strict  :: "('a => 'b err) => ('a err => 'b err)"
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10496
diff changeset
    57
primrec
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10496
diff changeset
    58
  "strict f Err    = Err"
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10496
diff changeset
    59
  "strict f (OK x) = f x"
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10496
diff changeset
    60
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
    61
lemma strict_Some [simp]: 
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
    62
  "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
    63
  by (cases x, auto)
10812
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10496
diff changeset
    64
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    65
lemma not_Err_eq:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    66
  "(x \<noteq> Err) = (\<exists>a. x = OK a)" 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    67
  by (cases x) auto
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    68
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    69
lemma not_OK_eq:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    70
  "(\<forall>y. x \<noteq> OK y) = (x = Err)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    71
  by (cases x) auto  
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    72
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    73
lemma unfold_lesub_err:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    74
  "e1 <=_(le r) e2 == le r e1 e2"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    75
  by (simp add: lesub_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    76
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    77
lemma le_err_refl:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    78
  "!x. x <=_r x ==> e <=_(Err.le r) e"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    79
apply (unfold lesub_def Err.le_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    80
apply (simp split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    81
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    82
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    83
lemma le_err_trans [rule_format]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    84
  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    85
apply (unfold unfold_lesub_err le_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    86
apply (simp split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    87
apply (blast intro: order_trans)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    88
done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    89
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    90
lemma le_err_antisym [rule_format]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    91
  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    92
apply (unfold unfold_lesub_err le_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    93
apply (simp split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    94
apply (blast intro: order_antisym)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    95
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    96
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    97
lemma OK_le_err_OK:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    98
  "(OK x <=_(le r) OK y) = (x <=_r y)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
    99
  by (simp add: unfold_lesub_err le_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   100
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   101
lemma order_le_err [iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   102
  "order(le r) = order r"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   103
apply (rule iffI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   104
 apply (subst order_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   105
 apply (blast dest: order_antisym OK_le_err_OK [THEN iffD2]
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   106
              intro: order_trans OK_le_err_OK [THEN iffD1])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   107
apply (subst order_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   108
apply (blast intro: le_err_refl le_err_trans le_err_antisym
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   109
             dest: order_refl)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   110
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   111
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   112
lemma le_Err [iff]:  "e <=_(le r) Err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   113
  by (simp add: unfold_lesub_err le_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   114
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   115
lemma Err_le_conv [iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   116
 "Err <=_(le r) e  = (e = Err)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   117
  by (simp add: unfold_lesub_err le_def  split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   118
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   119
lemma le_OK_conv [iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   120
  "e <=_(le r) OK x  =  (? y. e = OK y & y <=_r x)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   121
  by (simp add: unfold_lesub_err le_def split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   122
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   123
lemma OK_le_conv:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   124
 "OK x <=_(le r) e  =  (e = Err | (? y. e = OK y & x <=_r y))"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   125
  by (simp add: unfold_lesub_err le_def split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   126
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   127
lemma top_Err [iff]: "top (le r) Err";
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   128
  by (simp add: top_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   129
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   130
lemma OK_less_conv [rule_format, iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   131
  "OK x <_(le r) e = (e=Err | (? y. e = OK y & x <_r y))"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   132
  by (simp add: lesssub_def lesub_def le_def split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   133
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   134
lemma not_Err_less [rule_format, iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   135
  "~(Err <_(le r) x)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   136
  by (simp add: lesssub_def lesub_def le_def split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   137
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   138
lemma semilat_errI:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   139
  "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   140
apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   141
apply (simp split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   142
done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   143
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   144
lemma err_semilat_eslI: 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   145
  "!!L. semilat L ==> err_semilat(esl L)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   146
apply (unfold sl_def esl_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   147
apply (simp (no_asm_simp) only: split_tupled_all)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   148
apply (simp add: semilat_errI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   149
done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   150
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   151
lemma acc_err [simp, intro!]:  "acc r ==> acc(le r)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   152
apply (unfold acc_def lesub_def le_def lesssub_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   153
apply (simp add: wf_eq_minimal split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   154
apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   155
apply (case_tac "Err : Q")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   156
 apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   157
apply (erule_tac x = "{a . OK a : Q}" in allE)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   158
apply (case_tac "x")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   159
 apply fast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   160
apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   161
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   162
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   163
lemma Err_in_err [iff]: "Err : err A"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   164
  by (simp add: err_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   165
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   166
lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   167
  by (auto simp add: err_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   168
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   169
section {* lift *}
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   170
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   171
lemma lift_in_errI:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   172
  "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   173
apply (unfold lift_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   174
apply (simp split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   175
apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   176
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   177
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   178
lemma Err_lift2 [simp]: 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   179
  "Err +_(lift2 f) x = Err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   180
  by (simp add: lift2_def plussub_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   181
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   182
lemma lift2_Err [simp]: 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   183
  "x +_(lift2 f) Err = Err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   184
  by (simp add: lift2_def plussub_def split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   185
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   186
lemma OK_lift2_OK [simp]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   187
  "OK x +_(lift2 f) OK y = x +_f y"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   188
  by (simp add: lift2_def plussub_def split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   189
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   190
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   191
section {* sup *}
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   192
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   193
lemma Err_sup_Err [simp]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   194
  "Err +_(Err.sup f) x = Err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   195
  by (simp add: plussub_def Err.sup_def Err.lift2_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   196
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   197
lemma Err_sup_Err2 [simp]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   198
  "x +_(Err.sup f) Err = Err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   199
  by (simp add: plussub_def Err.sup_def Err.lift2_def split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   200
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   201
lemma Err_sup_OK [simp]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   202
  "OK x +_(Err.sup f) OK y = OK(x +_f y)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   203
  by (simp add: plussub_def Err.sup_def Err.lift2_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   204
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   205
lemma Err_sup_eq_OK_conv [iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   206
  "(Err.sup f ex ey = OK z) = (? x y. ex = OK x & ey = OK y & f x y = z)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   207
apply (unfold Err.sup_def lift2_def plussub_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   208
apply (rule iffI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   209
 apply (simp split: err.split_asm)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   210
apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   211
apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   212
done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   213
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   214
lemma Err_sup_eq_Err [iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   215
  "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   216
apply (unfold Err.sup_def lift2_def plussub_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   217
apply (simp split: err.split)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   218
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   219
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   220
section {* semilat (err A) (le r) f *}
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   221
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   222
lemma semilat_le_err_Err_plus [simp]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   223
  "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   224
  by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   225
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   226
lemma semilat_le_err_plus_Err [simp]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   227
  "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   228
  by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   229
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   230
lemma semilat_le_err_OK1:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   231
  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   232
  ==> x <=_r z";
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   233
apply (rule OK_le_err_OK [THEN iffD1])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   234
apply (erule subst)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   235
apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   236
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   237
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   238
lemma semilat_le_err_OK2:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   239
  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   240
  ==> y <=_r z"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   241
apply (rule OK_le_err_OK [THEN iffD1])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   242
apply (erule subst)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   243
apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   244
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   245
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   246
lemma eq_order_le:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   247
  "[| x=y; order r |] ==> x <=_r y"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   248
apply (unfold order_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   249
apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   250
done
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   251
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   252
lemma OK_plus_OK_eq_Err_conv [simp]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   253
  "[| x:A; y:A; semilat(err A, le r, fe) |] ==> 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   254
  ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   255
proof -
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   256
  have plus_le_conv3: "!!A x y z f r. 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   257
    [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   258
    ==> x <=_r z \<and> y <=_r z"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   259
    by (rule plus_le_conv [THEN iffD1])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   260
  case antecedent
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   261
  thus ?thesis
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   262
  apply (rule_tac iffI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   263
   apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   264
   apply (drule OK_le_err_OK [THEN iffD2])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   265
   apply (drule OK_le_err_OK [THEN iffD2])
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   266
   apply (drule semilat_lub)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   267
        apply assumption
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   268
       apply assumption
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   269
      apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   270
     apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   271
    apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   272
   apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   273
  apply (case_tac "(OK x) +_fe (OK y)")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   274
   apply assumption
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   275
  apply (rename_tac z)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   276
  apply (subgoal_tac "OK z: err A")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   277
  apply (drule eq_order_le)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   278
    apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   279
   apply (blast dest: plus_le_conv3) 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   280
  apply (erule subst)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   281
  apply (blast intro: closedD)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   282
  done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   283
qed
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   284
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   285
section {* semilat (err(Union AS)) *}
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   286
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   287
(* FIXME? *)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   288
lemma all_bex_swap_lemma [iff]:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   289
  "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   290
  by blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   291
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   292
lemma closed_err_Union_lift2I: 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   293
  "[| !A:AS. closed (err A) (lift2 f); AS ~= {}; 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   294
      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   295
  ==> closed (err(Union AS)) (lift2 f)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   296
apply (unfold closed_def err_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   297
apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   298
apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   299
apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   300
apply fast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   301
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   302
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   303
text {* 
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   304
  If @{term "AS = {}"} the thm collapses to
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   305
  @{prop "order r & closed {Err} f & Err +_f Err = Err"}
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   306
  which may not hold 
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10812
diff changeset
   307
*}
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   308
lemma err_semilat_UnionI:
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   309
  "[| !A:AS. err_semilat(A, r, f); AS ~= {}; 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   310
      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   311
  ==> err_semilat(Union AS, r, f)"
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   312
apply (unfold semilat_def sl_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   313
apply (simp add: closed_err_Union_lift2I)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   314
apply (rule conjI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   315
 apply blast
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   316
apply (simp add: err_def)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   317
apply (rule conjI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   318
 apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   319
 apply (rename_tac A a u B b)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   320
 apply (case_tac "A = B")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   321
  apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   322
 apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   323
apply (rule conjI)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   324
 apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   325
 apply (rename_tac A a u B b)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   326
 apply (case_tac "A = B")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   327
  apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   328
 apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   329
apply clarify
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   330
apply (rename_tac A ya yb B yd z C c a b)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   331
apply (case_tac "A = B")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   332
 apply (case_tac "A = C")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   333
  apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   334
 apply (rotate_tac -1)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   335
 apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   336
apply (rotate_tac -1)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   337
apply (case_tac "B = C")
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   338
 apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   339
apply (rotate_tac -1)
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   340
apply simp
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   341
done 
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   342
f2d304bdf3cc BCV integration (first step)
kleing
parents:
diff changeset
   343
end