src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 39159 src/HOLCF/IOA/meta_theory/SimCorrectness.thy@0dec18004e75
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
mueller@4565
     1
(*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
wenzelm@12218
     2
    Author:     Olaf Müller
mueller@4565
     3
*)
mueller@4565
     4
wenzelm@17233
     5
header {* Correctness of Simulations in HOLCF/IOA *}
mueller@4565
     6
wenzelm@17233
     7
theory SimCorrectness
wenzelm@17233
     8
imports Simulations
wenzelm@17233
     9
begin
wenzelm@17233
    10
wenzelm@25135
    11
definition
mueller@4565
    12
  (* Note: s2 instead of s1 in last argument type !! *)
wenzelm@25135
    13
  corresp_ex_simC :: "('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs
wenzelm@25135
    14
                   -> ('s2 => ('a,'s2)pairs)" where
wenzelm@25135
    15
  "corresp_ex_simC A R = (fix$(LAM h ex. (%s. case ex of
mueller@4565
    16
      nil =>  nil
mueller@4565
    17
    | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
wenzelm@17233
    18
                                 T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
mueller@4565
    19
                             in
mueller@4565
    20
                                (@cex. move A cex s a T')
nipkow@10835
    21
                                 @@ ((h$xs) T'))
nipkow@10835
    22
                        $x) )))"
wenzelm@17233
    23
wenzelm@25135
    24
definition
wenzelm@25135
    25
  corresp_ex_sim :: "('a,'s2)ioa => (('s1 *'s2)set) =>
wenzelm@25135
    26
                      ('a,'s1)execution => ('a,'s2)execution" where
wenzelm@25135
    27
  "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
wenzelm@25135
    28
                            in
wenzelm@25135
    29
                               (S',(corresp_ex_simC A R$(snd ex)) S')"
wenzelm@25135
    30
wenzelm@19741
    31
wenzelm@19741
    32
subsection "corresp_ex_sim"
wenzelm@19741
    33
wenzelm@25135
    34
lemma corresp_ex_simC_unfold: "corresp_ex_simC A R  = (LAM ex. (%s. case ex of
wenzelm@25135
    35
       nil =>  nil
wenzelm@25135
    36
     | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
wenzelm@25135
    37
                                  T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
wenzelm@25135
    38
                              in
wenzelm@25135
    39
                                 (@cex. move A cex s a T')
wenzelm@25135
    40
                               @@ ((corresp_ex_simC A R $xs) T'))
wenzelm@19741
    41
                         $x) ))"
wenzelm@19741
    42
apply (rule trans)
wenzelm@19741
    43
apply (rule fix_eq2)
wenzelm@25135
    44
apply (simp only: corresp_ex_simC_def)
wenzelm@19741
    45
apply (rule beta_cfun)
wenzelm@19741
    46
apply (simp add: flift1_def)
wenzelm@19741
    47
done
wenzelm@19741
    48
wenzelm@19741
    49
lemma corresp_ex_simC_UU: "(corresp_ex_simC A R$UU) s=UU"
wenzelm@19741
    50
apply (subst corresp_ex_simC_unfold)
wenzelm@19741
    51
apply simp
wenzelm@19741
    52
done
wenzelm@19741
    53
wenzelm@19741
    54
lemma corresp_ex_simC_nil: "(corresp_ex_simC A R$nil) s = nil"
wenzelm@19741
    55
apply (subst corresp_ex_simC_unfold)
wenzelm@19741
    56
apply simp
wenzelm@19741
    57
done
wenzelm@19741
    58
wenzelm@25135
    59
lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s =
wenzelm@25135
    60
           (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
wenzelm@25135
    61
            in
wenzelm@25135
    62
             (@cex. move A cex s a T')
wenzelm@19741
    63
              @@ ((corresp_ex_simC A R$xs) T'))"
wenzelm@19741
    64
apply (rule trans)
wenzelm@19741
    65
apply (subst corresp_ex_simC_unfold)
wenzelm@19741
    66
apply (simp add: Consq_def flift1_def)
wenzelm@19741
    67
apply simp
wenzelm@19741
    68
done
wenzelm@19741
    69
wenzelm@19741
    70
wenzelm@19741
    71
declare corresp_ex_simC_UU [simp] corresp_ex_simC_nil [simp] corresp_ex_simC_cons [simp]
wenzelm@19741
    72
wenzelm@19741
    73
wenzelm@19741
    74
subsection "properties of move"
wenzelm@19741
    75
wenzelm@19741
    76
declare Let_def [simp del]
wenzelm@19741
    77
wenzelm@25135
    78
lemma move_is_move_sim:
wenzelm@25135
    79
   "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>
wenzelm@25135
    80
      let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
wenzelm@19741
    81
      (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'"
wenzelm@19741
    82
apply (unfold is_simulation_def)
wenzelm@19741
    83
wenzelm@19741
    84
(* Does not perform conditional rewriting on assumptions automatically as
wenzelm@19741
    85
   usual. Instantiate all variables per hand. Ask Tobias?? *)
wenzelm@19741
    86
apply (subgoal_tac "? t' ex. (t,t') :R & move A ex s' a t'")
wenzelm@19741
    87
prefer 2
wenzelm@19741
    88
apply simp
wenzelm@19741
    89
apply (erule conjE)
wenzelm@19741
    90
apply (erule_tac x = "s" in allE)
wenzelm@19741
    91
apply (erule_tac x = "s'" in allE)
wenzelm@19741
    92
apply (erule_tac x = "t" in allE)
wenzelm@19741
    93
apply (erule_tac x = "a" in allE)
wenzelm@19741
    94
apply simp
wenzelm@19741
    95
(* Go on as usual *)
wenzelm@19741
    96
apply (erule exE)
wenzelm@19741
    97
apply (drule_tac x = "t'" and P = "%t'. ? ex. (t,t') :R & move A ex s' a t'" in someI)
wenzelm@19741
    98
apply (erule exE)
wenzelm@19741
    99
apply (erule conjE)
wenzelm@19741
   100
apply (simp add: Let_def)
wenzelm@19741
   101
apply (rule_tac x = "ex" in someI)
wenzelm@19741
   102
apply (erule conjE)
wenzelm@19741
   103
apply assumption
wenzelm@19741
   104
done
wenzelm@19741
   105
wenzelm@19741
   106
declare Let_def [simp]
wenzelm@19741
   107
wenzelm@25135
   108
lemma move_subprop1_sim:
wenzelm@25135
   109
   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
wenzelm@25135
   110
    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
wenzelm@19741
   111
     is_exec_frag A (s',@x. move A x s' a T')"
wenzelm@19741
   112
apply (cut_tac move_is_move_sim)
wenzelm@19741
   113
defer
wenzelm@19741
   114
apply assumption+
wenzelm@19741
   115
apply (simp add: move_def)
wenzelm@19741
   116
done
wenzelm@19741
   117
wenzelm@25135
   118
lemma move_subprop2_sim:
wenzelm@25135
   119
   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
wenzelm@25135
   120
    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
wenzelm@19741
   121
    Finite (@x. move A x s' a T')"
wenzelm@19741
   122
apply (cut_tac move_is_move_sim)
wenzelm@19741
   123
defer
wenzelm@19741
   124
apply assumption+
wenzelm@19741
   125
apply (simp add: move_def)
wenzelm@19741
   126
done
wenzelm@19741
   127
wenzelm@25135
   128
lemma move_subprop3_sim:
wenzelm@25135
   129
   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
wenzelm@25135
   130
    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
wenzelm@19741
   131
     laststate (s',@x. move A x s' a T') = T'"
wenzelm@19741
   132
apply (cut_tac move_is_move_sim)
wenzelm@19741
   133
defer
wenzelm@19741
   134
apply assumption+
wenzelm@19741
   135
apply (simp add: move_def)
wenzelm@19741
   136
done
wenzelm@19741
   137
wenzelm@25135
   138
lemma move_subprop4_sim:
wenzelm@25135
   139
   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
wenzelm@25135
   140
    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
wenzelm@25135
   141
      mk_trace A$((@x. move A x s' a T')) =
wenzelm@19741
   142
        (if a:ext A then a>>nil else nil)"
wenzelm@19741
   143
apply (cut_tac move_is_move_sim)
wenzelm@19741
   144
defer
wenzelm@19741
   145
apply assumption+
wenzelm@19741
   146
apply (simp add: move_def)
wenzelm@19741
   147
done
wenzelm@19741
   148
wenzelm@25135
   149
lemma move_subprop5_sim:
wenzelm@25135
   150
   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
wenzelm@25135
   151
    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
wenzelm@19741
   152
      (t,T'):R"
wenzelm@19741
   153
apply (cut_tac move_is_move_sim)
wenzelm@19741
   154
defer
wenzelm@19741
   155
apply assumption+
wenzelm@19741
   156
apply (simp add: move_def)
wenzelm@19741
   157
done
wenzelm@19741
   158
wenzelm@19741
   159
wenzelm@19741
   160
subsection {* TRACE INCLUSION Part 1: Traces coincide *}
wenzelm@19741
   161
wenzelm@19741
   162
subsubsection "Lemmata for <=="
wenzelm@19741
   163
wenzelm@19741
   164
(* ------------------------------------------------------
wenzelm@19741
   165
                 Lemma 1 :Traces coincide
wenzelm@19741
   166
   ------------------------------------------------------- *)
wenzelm@19741
   167
wenzelm@19741
   168
declare split_if [split del]
wenzelm@25135
   169
lemma traces_coincide_sim [rule_format (no_asm)]:
wenzelm@25135
   170
  "[|is_simulation R C A; ext C = ext A|] ==>
wenzelm@25135
   171
         !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
wenzelm@19741
   172
             mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
wenzelm@19741
   173
wenzelm@39159
   174
apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
wenzelm@19741
   175
(* cons case *)
haftmann@26359
   176
apply auto
wenzelm@19741
   177
apply (rename_tac ex a t s s')
wenzelm@19741
   178
apply (simp add: mk_traceConc)
wenzelm@19741
   179
apply (frule reachable.reachable_n)
wenzelm@19741
   180
apply assumption
wenzelm@19741
   181
apply (erule_tac x = "t" in allE)
wenzelm@19741
   182
apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
wenzelm@19741
   183
apply (simp add: move_subprop5_sim [unfolded Let_def]
wenzelm@19741
   184
  move_subprop4_sim [unfolded Let_def] split add: split_if)
wenzelm@19741
   185
done
wenzelm@19741
   186
declare split_if [split]
wenzelm@19741
   187
wenzelm@19741
   188
wenzelm@19741
   189
(* ----------------------------------------------------------- *)
wenzelm@19741
   190
(*               Lemma 2 : corresp_ex_sim is execution         *)
wenzelm@19741
   191
(* ----------------------------------------------------------- *)
wenzelm@19741
   192
wenzelm@19741
   193
wenzelm@25135
   194
lemma correspsim_is_execution [rule_format (no_asm)]:
wenzelm@25135
   195
 "[| is_simulation R C A |] ==>
wenzelm@25135
   196
  !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
wenzelm@19741
   197
  --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
wenzelm@19741
   198
wenzelm@27208
   199
apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
wenzelm@19741
   200
(* main case *)
haftmann@26359
   201
apply auto
wenzelm@19741
   202
apply (rename_tac ex a t s s')
wenzelm@19741
   203
apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1)
wenzelm@19741
   204
wenzelm@19741
   205
(* Finite *)
wenzelm@19741
   206
apply (erule move_subprop2_sim [unfolded Let_def])
wenzelm@19741
   207
apply assumption+
wenzelm@19741
   208
apply (rule conjI)
wenzelm@19741
   209
wenzelm@19741
   210
(* is_exec_frag *)
wenzelm@19741
   211
apply (erule move_subprop1_sim [unfolded Let_def])
wenzelm@19741
   212
apply assumption+
wenzelm@19741
   213
apply (rule conjI)
wenzelm@19741
   214
wenzelm@19741
   215
(* Induction hypothesis  *)
wenzelm@19741
   216
(* reachable_n looping, therefore apply it manually *)
wenzelm@19741
   217
apply (erule_tac x = "t" in allE)
wenzelm@19741
   218
apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
wenzelm@19741
   219
apply simp
wenzelm@19741
   220
apply (frule reachable.reachable_n)
wenzelm@19741
   221
apply assumption
wenzelm@19741
   222
apply (simp add: move_subprop5_sim [unfolded Let_def])
wenzelm@19741
   223
(* laststate *)
wenzelm@19741
   224
apply (erule move_subprop3_sim [unfolded Let_def, symmetric])
wenzelm@19741
   225
apply assumption+
wenzelm@19741
   226
done
wenzelm@19741
   227
wenzelm@19741
   228
wenzelm@19741
   229
subsection "Main Theorem: TRACE - INCLUSION"
wenzelm@19741
   230
wenzelm@19741
   231
(* -------------------------------------------------------------------------------- *)
wenzelm@19741
   232
wenzelm@19741
   233
  (* generate condition (s,S'):R & S':starts_of A, the first being intereting
wenzelm@19741
   234
     for the induction cases concerning the two lemmas correpsim_is_execution and
wenzelm@19741
   235
     traces_coincide_sim, the second for the start state case.
wenzelm@19741
   236
     S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C  *)
wenzelm@19741
   237
wenzelm@25135
   238
lemma simulation_starts:
wenzelm@25135
   239
"[| is_simulation R C A; s:starts_of C |]
wenzelm@25135
   240
  ==> let S' = @s'. (s,s'):R & s':starts_of A in
wenzelm@19741
   241
      (s,S'):R & S':starts_of A"
wenzelm@19741
   242
  apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def)
wenzelm@19741
   243
  apply (erule conjE)+
wenzelm@19741
   244
  apply (erule ballE)
wenzelm@19741
   245
  prefer 2 apply (blast)
wenzelm@19741
   246
  apply (erule exE)
wenzelm@19741
   247
  apply (rule someI2)
wenzelm@19741
   248
  apply assumption
wenzelm@19741
   249
  apply blast
wenzelm@19741
   250
  done
wenzelm@19741
   251
wenzelm@19741
   252
lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1, standard]
wenzelm@19741
   253
lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2, standard]
wenzelm@19741
   254
wenzelm@19741
   255
wenzelm@25135
   256
lemma trace_inclusion_for_simulations:
wenzelm@25135
   257
  "[| ext C = ext A; is_simulation R C A |]
wenzelm@19741
   258
           ==> traces C <= traces A"
wenzelm@19741
   259
wenzelm@19741
   260
  apply (unfold traces_def)
wenzelm@19741
   261
wenzelm@19741
   262
  apply (simp (no_asm) add: has_trace_def2)
haftmann@26359
   263
  apply auto
wenzelm@19741
   264
wenzelm@19741
   265
  (* give execution of abstract automata *)
wenzelm@19741
   266
  apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
wenzelm@19741
   267
wenzelm@19741
   268
  (* Traces coincide, Lemma 1 *)
wenzelm@27208
   269
  apply (tactic {* pair_tac @{context} "ex" 1 *})
wenzelm@19741
   270
  apply (rename_tac s ex)
wenzelm@19741
   271
  apply (simp (no_asm) add: corresp_ex_sim_def)
wenzelm@19741
   272
  apply (rule_tac s = "s" in traces_coincide_sim)
wenzelm@19741
   273
  apply assumption+
wenzelm@19741
   274
  apply (simp add: executions_def reachable.reachable_0 sim_starts1)
wenzelm@19741
   275
wenzelm@19741
   276
  (* corresp_ex_sim is execution, Lemma 2 *)
wenzelm@27208
   277
  apply (tactic {* pair_tac @{context} "ex" 1 *})
wenzelm@19741
   278
  apply (simp add: executions_def)
wenzelm@19741
   279
  apply (rename_tac s ex)
wenzelm@19741
   280
wenzelm@19741
   281
  (* start state *)
wenzelm@19741
   282
  apply (rule conjI)
wenzelm@19741
   283
  apply (simp add: sim_starts2 corresp_ex_sim_def)
wenzelm@19741
   284
wenzelm@19741
   285
  (* is-execution-fragment *)
wenzelm@19741
   286
  apply (simp add: corresp_ex_sim_def)
wenzelm@19741
   287
  apply (rule_tac s = s in correspsim_is_execution)
wenzelm@19741
   288
  apply assumption
wenzelm@19741
   289
  apply (simp add: reachable.reachable_0 sim_starts1)
wenzelm@19741
   290
  done
wenzelm@17233
   291
wenzelm@17233
   292
end