src/HOL/Bali/Table.thy
author nipkow
Wed, 04 Mar 2009 10:47:20 +0100
changeset 30235 58d147683393
parent 24194 96013f81faef
child 34939 44294cfecb1d
permissions -rw-r--r--
Made Option a separate theory and renamed option_map to Option.map
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Table.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
header {* Abstract tables and their implementation as lists *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     7
theory Table imports Basis begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\item definition of table: infinite map vs. list vs. finite set
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
      list chosen, because:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
  \begin{itemize} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
  \item[+]  a priori finite
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
  \item[+]  lookup is more operational than for finite set
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
  \item[-]  not very abstract, but function table converts it to abstract 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
            mapping
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
\item coding of lookup result: Some/None vs. value/arbitrary
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
   Some/None chosen, because:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  \item[++] makes definedness check possible (applies also to finite set),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
     which is important for the type standard, hiding/overriding, etc.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
     (though it may perhaps be possible at least for the operational semantics
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
      to treat programs as infinite, i.e. where classes, fields, methods etc.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
      of any name are considered to be defined)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
  \item[-]  sometimes awkward case distinctions, alleviated by operator 'the'
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    33
types ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
14134
0fdf5708c7a8 Replaced \<leadsto> by \<rightharpoonup>
nipkow
parents: 14025
diff changeset
    34
      = "'a \<rightharpoonup> 'b"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    35
      ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
      = "'a \<Rightarrow> 'b set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
section "map of / table of"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
syntax
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    42
  table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   --{* concrete table *}
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    43
  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
  "table_of" == "map_of"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
  
24194
96013f81faef re-eliminated Option.thy
haftmann
parents: 24038
diff changeset
    47
  (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Datatype.option"
14134
0fdf5708c7a8 Replaced \<leadsto> by \<rightharpoonup>
nipkow
parents: 14025
diff changeset
    48
  (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
(* ### To map *)
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13688
diff changeset
    51
lemma map_add_find_left[simp]:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
"n k = None \<Longrightarrow> (m ++ n) k = m k"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13688
diff changeset
    53
by (simp add: map_add_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
section {* Conditional Override *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
cond_override:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
  "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    60
--{* when merging tables old and new, only override an entry of table old when  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    61
   the condition cond holds *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
"cond_override cond old new \<equiv>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
 \<lambda> k.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
  (case new k of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
     None         \<Rightarrow> old k                       
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
   | Some new_val \<Rightarrow> (case old k of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
                        None         \<Rightarrow> Some new_val          
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
                      | Some old_val \<Rightarrow> (if cond new_val old_val
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
                                         then Some new_val     
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
                                         else Some old_val)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
lemma cond_override_empty1[simp]: "cond_override c empty t = t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
by (simp add: cond_override_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
lemma cond_override_empty2[simp]: "cond_override c t empty = t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
by (simp add: cond_override_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
lemma cond_override_None[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
 "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
by (simp add: cond_override_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
lemma cond_override_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
 "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
  \<Longrightarrow> (cond_override C old new) k = Some nv"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
by (auto simp add: cond_override_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
lemma cond_override_noOverride:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
 "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
  \<Longrightarrow> (cond_override C old new) k = Some ov"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
by (auto simp add: cond_override_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
by (auto simp add: cond_override_def dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
lemma finite_dom_cond_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
 "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
apply (rule_tac B="dom s \<union> dom t" in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
apply (rule dom_cond_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
by (rule finite_UnI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
section {* Filter on Tables *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
"filter_tab c t \<equiv> \<lambda> k. (case t k of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
                           None   \<Rightarrow> None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
                         | Some x \<Rightarrow> if c k x then Some x else None)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
by (simp add: filter_tab_def empty_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
by (simp add: expand_fun_eq filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
by (simp add: expand_fun_eq filter_tab_def empty_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
by (auto simp add: filter_tab_def ran_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
apply (auto simp add: filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
apply (drule sym, blast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
lemma finite_range_filter_tab:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
  "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply (rule_tac B="range t \<union> {None} " in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
apply (rule filter_tab_range_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
apply (auto intro: finite_UnI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
lemma filter_tab_SomeD[dest!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
"filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
by (auto simp add: filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
by (simp add: filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
lemma filter_tab_all_True: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
 "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
apply (auto simp add: filter_tab_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
lemma filter_tab_all_True_Some:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
 "\<lbrakk>\<forall> k y. t k = Some y \<longrightarrow> p k y; t k = Some v\<rbrakk> \<Longrightarrow> filter_tab p t k = Some v"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
by (auto simp add: filter_tab_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   149
lemma filter_tab_all_False: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   150
 "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   151
by (auto simp add: filter_tab_def expand_fun_eq)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   152
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
apply (simp add: filter_tab_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
by (auto simp add: filter_tab_def dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
by (auto simp add: expand_fun_eq filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
lemma finite_dom_filter_tab:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
"finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
apply (rule_tac B="dom t" in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
by (rule filter_tab_dom_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
lemma filter_tab_weaken:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
  \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
 \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13585
diff changeset
   173
apply (force simp add: filter_tab_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
lemma cond_override_filter: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
  "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
    \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
        (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
   \<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
    cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
    = filter_tab filterC (cond_override overC t s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   185
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
section {* Misc. *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y"
24038
18182c4aec9e replaced make_imp by rev_mp;
wenzelm
parents: 18447
diff changeset
   189
apply (erule rev_mp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
apply (induct l)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
lemma Ball_set_tableD: 
30235
58d147683393 Made Option a separate theory and renamed option_map to Option.map
nipkow
parents: 24194
diff changeset
   197
  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
apply (frule Ball_set_table)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
declare map_of_SomeD [elim]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
lemma table_of_Some_in_set:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
"table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
lemma set_get_eq: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
  "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 16417
diff changeset
   209
by (auto dest!: weak_map_of_SomeI)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
13585
db4005b40cc6 Converted Fun to Isar style.
paulson
parents: 13337
diff changeset
   212
apply (rule inj_onI)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
lemma table_of_mapconst_SomeI:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
  "\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
   table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
apply (induct t)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
lemma table_of_mapconst_NoneI:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
  "\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
   table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
apply (induct t)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
   table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
lemma table_of_remap_SomeD [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
  "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
  table_of t (k, k') = Some x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
lemma table_of_mapf_Some [rule_format (no_asm)]: "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
  table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<longrightarrow> (table_of t k = None)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
   \<longrightarrow> C = snd ek \<and> table_of t (fst ek) = Some x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
 (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13688
diff changeset
   277
apply (simp)
d9b155757dc8 *** empty log message ***
nipkow
parents: 13688
diff changeset
   278
apply (rule map_add_Some_iff)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
  "table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
apply (induct xs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
apply (auto del: map_of_SomeD intro!: map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
  Un_tables      :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
  overrides_t    :: "('a, 'b) tables     \<Rightarrow> ('a, 'b) tables \<Rightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
                     ('a, 'b) tables"             (infixl "\<oplus>\<oplus>" 100)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
  hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hidings _ entails _" 20)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   294
  --{* variant for unique table: *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hiding _ entails _"  20)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   297
  --{* variant for a unique table and conditional overriding: *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
  cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
                          \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
                          ("_ hiding _ under _ entails _"  20)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
  Un_tables_def:       "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
  overrides_t_def:     "s \<oplus>\<oplus> t        \<equiv> \<lambda>k. if t k = {} then s k else t k"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
  hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
  hiding_entails_def:  "t hiding  s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
  cond_hiding_entails_def: "t hiding  s under C entails R
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
                            \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
section "Untables"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
lemma Un_tablesI [intro]:  "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
apply (simp add: Un_tables_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
lemma Un_tablesD [dest!]: "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
apply (simp add: Un_tables_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
apply (unfold Un_tables_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
section "overrides"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
apply (unfold overrides_t_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
apply (unfold overrides_t_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
lemma overrides_t_Some_iff: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
 "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
by (simp add: overrides_t_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
by (simp add: overrides_t_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
by (simp add: overrides_t_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
section "hiding entails"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
lemma hiding_entailsD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
  "\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
by (simp add: hiding_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
lemma empty_hiding_entails: "empty hiding s entails R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
by (simp add: hiding_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
lemma hiding_empty_entails: "t hiding empty entails R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
by (simp add: hiding_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
declare empty_hiding_entails [simp] hiding_empty_entails [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
section "cond hiding entails"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
lemma cond_hiding_entailsD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
"\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
by (simp add: cond_hiding_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
by (simp add: cond_hiding_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
by (simp add: cond_hiding_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
by (simp add: hidings_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
apply (unfold hidings_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
lemma empty_hidings_entails: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
  "(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
by (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
(*###TO Map?*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
  atleast_free :: "('a ~=> 'b) => nat => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
primrec
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
 "atleast_free m 0       = True"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
 atleast_free_Suc: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
 "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
lemma atleast_free_weaken [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
  "!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
apply (induct_tac "n")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
apply (drule atleast_free_Suc [THEN iffD1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
lemma atleast_free_SucI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
"[| h a = None; !obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
by force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
declare fun_upd_apply [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
" !m a. m a = None --> (!c. atleast_free (m(a|->c)) n) -->  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
  (!b d. a ~= b --> atleast_free (m(b|->d)) n)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
apply (induct_tac "n")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
apply (rule_tac x = "a" in exI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
apply  (rule conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
apply  (force simp add: fun_upd_apply)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
apply (erule_tac V = "m a = None" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
apply (subst fun_upd_twist)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
apply  (erule not_sym)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
apply (rename_tac "ba")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
apply (drule_tac x = "ba" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
apply (tactic "smp_tac 2 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
apply (erule (1) notE impE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
apply (case_tac "aa = b")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
apply fast+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
declare fun_upd_apply [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
apply (case_tac "aa = a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
apply (erule atleast_free_SucD_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
declare atleast_free_Suc [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
end