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