src/HOL/Bali/Table.thy
author wenzelm
Mon, 28 Jan 2002 18:50:23 +0100
changeset 12857 a4386cc9b1c3
parent 12854 00d4a435777f
child 12858 6214f03d6d27
permissions -rw-r--r--
tuned header;
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
    Copyright   1997 Technische Universitaet Muenchen
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Abstract tables and their implementation as lists *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
theory Table = Basis:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item definition of table: infinite map vs. list vs. finite set
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
      list chosen, because:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
  \begin{itemize} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
  \item[+]  a priori finite
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
  \item[+]  lookup is more operational than for finite set
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
  \item[-]  not very abstract, but function table converts it to abstract 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
            mapping
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\item coding of lookup result: Some/None vs. value/arbitrary
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
   Some/None chosen, because:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
  \item[++] makes definedness check possible (applies also to finite set),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
     which is important for the type standard, hiding/overriding, etc.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
     (though it may perhaps be possible at least for the operational semantics
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
      to treat programs as infinite, i.e. where classes, fields, methods etc.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
      of any name are considered to be defined)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
  \item[-]  sometimes awkward case distinctions, alleviated by operator 'the'
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
types ('a, 'b) table    (* table with key type 'a and contents type 'b *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
      = "'a \<leadsto> 'b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
      ('a, 'b) tables   (* non-unique table with key 'a and contents 'b *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
      = "'a \<Rightarrow> 'b set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
section "map of / table of"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
  table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"    (* concrete table *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
  "table_of" == "map_of"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
  (type)"'a \<leadsto> 'b"       <= (type)"'a \<Rightarrow> 'b Option.option"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
  (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
(* ### To map *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
lemma override_find_left[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
"n k = None \<Longrightarrow> (m ++ n) k = m k"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
by (simp add: override_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
section {* Conditional Override *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
cond_override:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
  "('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
    61
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
(* when merging tables old and new, only override an entry of table old when  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
   the condition cond holds *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
"cond_override cond old new \<equiv>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
 \<lambda> k.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
  (case new k of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
     None         \<Rightarrow> old k                       
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
   | Some new_val \<Rightarrow> (case old k of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
                        None         \<Rightarrow> Some new_val          
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
                      | Some old_val \<Rightarrow> (if cond new_val old_val
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
                                         then Some new_val     
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
                                         else Some old_val)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
lemma cond_override_empty1[simp]: "cond_override c empty t = t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
by (simp add: cond_override_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
lemma cond_override_empty2[simp]: "cond_override c t empty = t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
by (simp add: cond_override_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
lemma cond_override_None[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
 "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
by (simp add: cond_override_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
lemma cond_override_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
 "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
  \<Longrightarrow> (cond_override C old new) k = Some nv"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
by (auto simp add: cond_override_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
lemma cond_override_noOverride:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
 "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
  \<Longrightarrow> (cond_override C old new) k = Some ov"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
by (auto simp add: cond_override_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
by (auto simp add: cond_override_def dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
lemma finite_dom_cond_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
 "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
apply (rule_tac B="dom s \<union> dom t" in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
apply (rule dom_cond_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
by (rule finite_UnI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
section {* Filter on Tables *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
"filter_tab c t \<equiv> \<lambda> k. (case t k of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
                           None   \<Rightarrow> None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
                         | Some x \<Rightarrow> if c k x then Some x else None)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
by (simp add: filter_tab_def empty_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
by (simp add: expand_fun_eq filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
by (simp add: expand_fun_eq filter_tab_def empty_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
by (auto simp add: filter_tab_def ran_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
apply (auto simp add: filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
apply (drule sym, blast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
lemma finite_range_filter_tab:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
  "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
apply (rule_tac B="range t \<union> {None} " in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
apply (rule filter_tab_range_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
apply (auto intro: finite_UnI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
lemma filter_tab_SomeD[dest!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
"filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
by (auto simp add: filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
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
   140
by (simp add: filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
lemma filter_tab_all_True: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
 "\<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
   144
apply (auto simp add: filter_tab_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
lemma filter_tab_all_True_Some:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
 "\<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
   149
by (auto simp add: filter_tab_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
apply (simp add: filter_tab_def expand_fun_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
by (auto simp add: filter_tab_def dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
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
   159
by (auto simp add: expand_fun_eq filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
lemma finite_dom_filter_tab:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
"finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply (rule_tac B="dom t" in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
by (rule filter_tab_dom_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
lemma filter_tab_weaken:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
  \<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
   170
 \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply (auto simp add: filter_tab_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
lemma cond_override_filter: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
  "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
    \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
        (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
   \<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
    cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
    = filter_tab filterC (cond_override overC t s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
section {* Misc. *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
apply (erule make_imp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
apply (induct l)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
lemma Ball_set_tableD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
apply (frule Ball_set_table)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
declare map_of_SomeD [elim]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
lemma table_of_Some_in_set:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
"table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
lemma set_get_eq: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
  "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
apply (fast dest!: weak_map_of_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
done
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))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
apply (rule injI)
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))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
apply (simp only: map_of_override [THEN sym])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
apply (rule override_Some_iff)
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)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
  (* variant for unique table: *)
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)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
  (* variant for a unique table and conditional overriding: *)
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