src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
changeset 40774 0437dbc127b3
parent 39159 0dec18004e75
child 40945 b8703f63bfb2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,292 @@
     1.4 +(*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
     1.5 +    Author:     Olaf Müller
     1.6 +*)
     1.7 +
     1.8 +header {* Correctness of Simulations in HOLCF/IOA *}
     1.9 +
    1.10 +theory SimCorrectness
    1.11 +imports Simulations
    1.12 +begin
    1.13 +
    1.14 +definition
    1.15 +  (* Note: s2 instead of s1 in last argument type !! *)
    1.16 +  corresp_ex_simC :: "('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs
    1.17 +                   -> ('s2 => ('a,'s2)pairs)" where
    1.18 +  "corresp_ex_simC A R = (fix$(LAM h ex. (%s. case ex of
    1.19 +      nil =>  nil
    1.20 +    | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
    1.21 +                                 T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
    1.22 +                             in
    1.23 +                                (@cex. move A cex s a T')
    1.24 +                                 @@ ((h$xs) T'))
    1.25 +                        $x) )))"
    1.26 +
    1.27 +definition
    1.28 +  corresp_ex_sim :: "('a,'s2)ioa => (('s1 *'s2)set) =>
    1.29 +                      ('a,'s1)execution => ('a,'s2)execution" where
    1.30 +  "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
    1.31 +                            in
    1.32 +                               (S',(corresp_ex_simC A R$(snd ex)) S')"
    1.33 +
    1.34 +
    1.35 +subsection "corresp_ex_sim"
    1.36 +
    1.37 +lemma corresp_ex_simC_unfold: "corresp_ex_simC A R  = (LAM ex. (%s. case ex of
    1.38 +       nil =>  nil
    1.39 +     | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
    1.40 +                                  T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
    1.41 +                              in
    1.42 +                                 (@cex. move A cex s a T')
    1.43 +                               @@ ((corresp_ex_simC A R $xs) T'))
    1.44 +                         $x) ))"
    1.45 +apply (rule trans)
    1.46 +apply (rule fix_eq2)
    1.47 +apply (simp only: corresp_ex_simC_def)
    1.48 +apply (rule beta_cfun)
    1.49 +apply (simp add: flift1_def)
    1.50 +done
    1.51 +
    1.52 +lemma corresp_ex_simC_UU: "(corresp_ex_simC A R$UU) s=UU"
    1.53 +apply (subst corresp_ex_simC_unfold)
    1.54 +apply simp
    1.55 +done
    1.56 +
    1.57 +lemma corresp_ex_simC_nil: "(corresp_ex_simC A R$nil) s = nil"
    1.58 +apply (subst corresp_ex_simC_unfold)
    1.59 +apply simp
    1.60 +done
    1.61 +
    1.62 +lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s =
    1.63 +           (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
    1.64 +            in
    1.65 +             (@cex. move A cex s a T')
    1.66 +              @@ ((corresp_ex_simC A R$xs) T'))"
    1.67 +apply (rule trans)
    1.68 +apply (subst corresp_ex_simC_unfold)
    1.69 +apply (simp add: Consq_def flift1_def)
    1.70 +apply simp
    1.71 +done
    1.72 +
    1.73 +
    1.74 +declare corresp_ex_simC_UU [simp] corresp_ex_simC_nil [simp] corresp_ex_simC_cons [simp]
    1.75 +
    1.76 +
    1.77 +subsection "properties of move"
    1.78 +
    1.79 +declare Let_def [simp del]
    1.80 +
    1.81 +lemma move_is_move_sim:
    1.82 +   "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>
    1.83 +      let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
    1.84 +      (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'"
    1.85 +apply (unfold is_simulation_def)
    1.86 +
    1.87 +(* Does not perform conditional rewriting on assumptions automatically as
    1.88 +   usual. Instantiate all variables per hand. Ask Tobias?? *)
    1.89 +apply (subgoal_tac "? t' ex. (t,t') :R & move A ex s' a t'")
    1.90 +prefer 2
    1.91 +apply simp
    1.92 +apply (erule conjE)
    1.93 +apply (erule_tac x = "s" in allE)
    1.94 +apply (erule_tac x = "s'" in allE)
    1.95 +apply (erule_tac x = "t" in allE)
    1.96 +apply (erule_tac x = "a" in allE)
    1.97 +apply simp
    1.98 +(* Go on as usual *)
    1.99 +apply (erule exE)
   1.100 +apply (drule_tac x = "t'" and P = "%t'. ? ex. (t,t') :R & move A ex s' a t'" in someI)
   1.101 +apply (erule exE)
   1.102 +apply (erule conjE)
   1.103 +apply (simp add: Let_def)
   1.104 +apply (rule_tac x = "ex" in someI)
   1.105 +apply (erule conjE)
   1.106 +apply assumption
   1.107 +done
   1.108 +
   1.109 +declare Let_def [simp]
   1.110 +
   1.111 +lemma move_subprop1_sim:
   1.112 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
   1.113 +    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
   1.114 +     is_exec_frag A (s',@x. move A x s' a T')"
   1.115 +apply (cut_tac move_is_move_sim)
   1.116 +defer
   1.117 +apply assumption+
   1.118 +apply (simp add: move_def)
   1.119 +done
   1.120 +
   1.121 +lemma move_subprop2_sim:
   1.122 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
   1.123 +    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
   1.124 +    Finite (@x. move A x s' a T')"
   1.125 +apply (cut_tac move_is_move_sim)
   1.126 +defer
   1.127 +apply assumption+
   1.128 +apply (simp add: move_def)
   1.129 +done
   1.130 +
   1.131 +lemma move_subprop3_sim:
   1.132 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
   1.133 +    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
   1.134 +     laststate (s',@x. move A x s' a T') = T'"
   1.135 +apply (cut_tac move_is_move_sim)
   1.136 +defer
   1.137 +apply assumption+
   1.138 +apply (simp add: move_def)
   1.139 +done
   1.140 +
   1.141 +lemma move_subprop4_sim:
   1.142 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
   1.143 +    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
   1.144 +      mk_trace A$((@x. move A x s' a T')) =
   1.145 +        (if a:ext A then a>>nil else nil)"
   1.146 +apply (cut_tac move_is_move_sim)
   1.147 +defer
   1.148 +apply assumption+
   1.149 +apply (simp add: move_def)
   1.150 +done
   1.151 +
   1.152 +lemma move_subprop5_sim:
   1.153 +   "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
   1.154 +    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
   1.155 +      (t,T'):R"
   1.156 +apply (cut_tac move_is_move_sim)
   1.157 +defer
   1.158 +apply assumption+
   1.159 +apply (simp add: move_def)
   1.160 +done
   1.161 +
   1.162 +
   1.163 +subsection {* TRACE INCLUSION Part 1: Traces coincide *}
   1.164 +
   1.165 +subsubsection "Lemmata for <=="
   1.166 +
   1.167 +(* ------------------------------------------------------
   1.168 +                 Lemma 1 :Traces coincide
   1.169 +   ------------------------------------------------------- *)
   1.170 +
   1.171 +declare split_if [split del]
   1.172 +lemma traces_coincide_sim [rule_format (no_asm)]:
   1.173 +  "[|is_simulation R C A; ext C = ext A|] ==>
   1.174 +         !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
   1.175 +             mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
   1.176 +
   1.177 +apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
   1.178 +(* cons case *)
   1.179 +apply auto
   1.180 +apply (rename_tac ex a t s s')
   1.181 +apply (simp add: mk_traceConc)
   1.182 +apply (frule reachable.reachable_n)
   1.183 +apply assumption
   1.184 +apply (erule_tac x = "t" in allE)
   1.185 +apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
   1.186 +apply (simp add: move_subprop5_sim [unfolded Let_def]
   1.187 +  move_subprop4_sim [unfolded Let_def] split add: split_if)
   1.188 +done
   1.189 +declare split_if [split]
   1.190 +
   1.191 +
   1.192 +(* ----------------------------------------------------------- *)
   1.193 +(*               Lemma 2 : corresp_ex_sim is execution         *)
   1.194 +(* ----------------------------------------------------------- *)
   1.195 +
   1.196 +
   1.197 +lemma correspsim_is_execution [rule_format (no_asm)]:
   1.198 + "[| is_simulation R C A |] ==>
   1.199 +  !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
   1.200 +  --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
   1.201 +
   1.202 +apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
   1.203 +(* main case *)
   1.204 +apply auto
   1.205 +apply (rename_tac ex a t s s')
   1.206 +apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1)
   1.207 +
   1.208 +(* Finite *)
   1.209 +apply (erule move_subprop2_sim [unfolded Let_def])
   1.210 +apply assumption+
   1.211 +apply (rule conjI)
   1.212 +
   1.213 +(* is_exec_frag *)
   1.214 +apply (erule move_subprop1_sim [unfolded Let_def])
   1.215 +apply assumption+
   1.216 +apply (rule conjI)
   1.217 +
   1.218 +(* Induction hypothesis  *)
   1.219 +(* reachable_n looping, therefore apply it manually *)
   1.220 +apply (erule_tac x = "t" in allE)
   1.221 +apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
   1.222 +apply simp
   1.223 +apply (frule reachable.reachable_n)
   1.224 +apply assumption
   1.225 +apply (simp add: move_subprop5_sim [unfolded Let_def])
   1.226 +(* laststate *)
   1.227 +apply (erule move_subprop3_sim [unfolded Let_def, symmetric])
   1.228 +apply assumption+
   1.229 +done
   1.230 +
   1.231 +
   1.232 +subsection "Main Theorem: TRACE - INCLUSION"
   1.233 +
   1.234 +(* -------------------------------------------------------------------------------- *)
   1.235 +
   1.236 +  (* generate condition (s,S'):R & S':starts_of A, the first being intereting
   1.237 +     for the induction cases concerning the two lemmas correpsim_is_execution and
   1.238 +     traces_coincide_sim, the second for the start state case.
   1.239 +     S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C  *)
   1.240 +
   1.241 +lemma simulation_starts:
   1.242 +"[| is_simulation R C A; s:starts_of C |]
   1.243 +  ==> let S' = @s'. (s,s'):R & s':starts_of A in
   1.244 +      (s,S'):R & S':starts_of A"
   1.245 +  apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def)
   1.246 +  apply (erule conjE)+
   1.247 +  apply (erule ballE)
   1.248 +  prefer 2 apply (blast)
   1.249 +  apply (erule exE)
   1.250 +  apply (rule someI2)
   1.251 +  apply assumption
   1.252 +  apply blast
   1.253 +  done
   1.254 +
   1.255 +lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1, standard]
   1.256 +lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2, standard]
   1.257 +
   1.258 +
   1.259 +lemma trace_inclusion_for_simulations:
   1.260 +  "[| ext C = ext A; is_simulation R C A |]
   1.261 +           ==> traces C <= traces A"
   1.262 +
   1.263 +  apply (unfold traces_def)
   1.264 +
   1.265 +  apply (simp (no_asm) add: has_trace_def2)
   1.266 +  apply auto
   1.267 +
   1.268 +  (* give execution of abstract automata *)
   1.269 +  apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
   1.270 +
   1.271 +  (* Traces coincide, Lemma 1 *)
   1.272 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.273 +  apply (rename_tac s ex)
   1.274 +  apply (simp (no_asm) add: corresp_ex_sim_def)
   1.275 +  apply (rule_tac s = "s" in traces_coincide_sim)
   1.276 +  apply assumption+
   1.277 +  apply (simp add: executions_def reachable.reachable_0 sim_starts1)
   1.278 +
   1.279 +  (* corresp_ex_sim is execution, Lemma 2 *)
   1.280 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.281 +  apply (simp add: executions_def)
   1.282 +  apply (rename_tac s ex)
   1.283 +
   1.284 +  (* start state *)
   1.285 +  apply (rule conjI)
   1.286 +  apply (simp add: sim_starts2 corresp_ex_sim_def)
   1.287 +
   1.288 +  (* is-execution-fragment *)
   1.289 +  apply (simp add: corresp_ex_sim_def)
   1.290 +  apply (rule_tac s = s in correspsim_is_execution)
   1.291 +  apply assumption
   1.292 +  apply (simp add: reachable.reachable_0 sim_starts1)
   1.293 +  done
   1.294 +
   1.295 +end