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