src/HOL/IOA/Solve.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 39159 0dec18004e75
child 51717 9e7d1c139569
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
oheimb@4530
     1
(*  Title:      HOL/IOA/Solve.thy
mueller@3078
     2
    Author:     Tobias Nipkow & Konrad Slind
mueller@3078
     3
    Copyright   1994  TU Muenchen
mueller@3078
     4
*)
mueller@3078
     5
wenzelm@17288
     6
header {* Weak possibilities mapping (abstraction) *}
wenzelm@17288
     7
wenzelm@17288
     8
theory Solve
wenzelm@17288
     9
imports IOA
wenzelm@17288
    10
begin
mueller@3078
    11
haftmann@35416
    12
definition is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" where
wenzelm@17288
    13
  "is_weak_pmap f C A ==
wenzelm@17288
    14
   (!s:starts_of(C). f(s):starts_of(A)) &
wenzelm@17288
    15
   (!s t a. reachable C s &
wenzelm@17288
    16
            (s,a,t):trans_of(C)
wenzelm@17288
    17
            --> (if a:externals(asig_of(C)) then
wenzelm@17288
    18
                   (f(s),a,f(t)):trans_of(A)
mueller@3078
    19
                 else f(s)=f(t)))"
mueller@3078
    20
wenzelm@19801
    21
declare mk_trace_thm [simp] trans_in_actions [simp]
wenzelm@19801
    22
wenzelm@19801
    23
lemma trace_inclusion: 
wenzelm@19801
    24
  "[| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A));  
wenzelm@19801
    25
           is_weak_pmap f C A |] ==> traces(C) <= traces(A)"
wenzelm@19801
    26
  apply (unfold is_weak_pmap_def traces_def)
wenzelm@19801
    27
wenzelm@19801
    28
  apply (simp (no_asm) add: has_trace_def)
wenzelm@19801
    29
  apply safe
wenzelm@19801
    30
  apply (rename_tac ex1 ex2)
wenzelm@19801
    31
wenzelm@19801
    32
  (* choose same trace, therefore same NF *)
wenzelm@19801
    33
  apply (rule_tac x = "mk_trace C ex1" in exI)
wenzelm@19801
    34
  apply simp
wenzelm@19801
    35
wenzelm@19801
    36
  (* give execution of abstract automata *)
wenzelm@19801
    37
  apply (rule_tac x = "(mk_trace A ex1,%i. f (ex2 i))" in bexI)
wenzelm@19801
    38
wenzelm@19801
    39
  (* Traces coincide *)
wenzelm@19801
    40
   apply (simp (no_asm_simp) add: mk_trace_def filter_oseq_idemp)
wenzelm@19801
    41
wenzelm@19801
    42
  (* Use lemma *)
wenzelm@19801
    43
  apply (frule states_of_exec_reachable)
wenzelm@19801
    44
wenzelm@19801
    45
  (* Now show that it's an execution *)
wenzelm@19801
    46
  apply (simp add: executions_def)
wenzelm@19801
    47
  apply safe
wenzelm@19801
    48
wenzelm@19801
    49
  (* Start states map to start states *)
wenzelm@19801
    50
  apply (drule bspec)
wenzelm@19801
    51
  apply assumption
wenzelm@19801
    52
wenzelm@19801
    53
  (* Show that it's an execution fragment *)
wenzelm@19801
    54
  apply (simp add: is_execution_fragment_def)
wenzelm@19801
    55
  apply safe
wenzelm@19801
    56
wenzelm@19801
    57
  apply (erule_tac x = "ex2 n" in allE)
wenzelm@19801
    58
  apply (erule_tac x = "ex2 (Suc n)" in allE)
wenzelm@19801
    59
  apply (erule_tac x = a in allE)
wenzelm@19801
    60
  apply simp
wenzelm@19801
    61
  done
wenzelm@19801
    62
wenzelm@19801
    63
(* Lemmata *)
wenzelm@19801
    64
wenzelm@19801
    65
lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R"
wenzelm@19801
    66
  by blast
wenzelm@19801
    67
wenzelm@19801
    68
wenzelm@19801
    69
(* fist_order_tautology of externals_of_par *)
wenzelm@19801
    70
lemma externals_of_par_extra:
wenzelm@19801
    71
  "a:externals(asig_of(A1||A2)) =     
wenzelm@19801
    72
   (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |   
wenzelm@19801
    73
   a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |   
wenzelm@19801
    74
   a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))"
wenzelm@19801
    75
  apply (auto simp add: externals_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def)
wenzelm@19801
    76
  done
wenzelm@19801
    77
wenzelm@19801
    78
lemma comp1_reachable: "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)"
wenzelm@19801
    79
  apply (simp add: reachable_def)
wenzelm@19801
    80
  apply (erule bexE)
wenzelm@19801
    81
  apply (rule_tac x =
wenzelm@19801
    82
    "(filter_oseq (%a. a:actions (asig_of (C1))) (fst ex) , %i. fst (snd ex i))" in bexI)
wenzelm@19801
    83
(* fst(s) is in projected execution *)
wenzelm@19801
    84
  apply force
wenzelm@19801
    85
(* projected execution is indeed an execution *)
wenzelm@19801
    86
  apply (simp cong del: if_weak_cong
wenzelm@19801
    87
    add: executions_def is_execution_fragment_def par_def starts_of_def
wenzelm@19801
    88
      trans_of_def filter_oseq_def
wenzelm@19801
    89
    split add: option.split)
wenzelm@19801
    90
  done
wenzelm@19801
    91
wenzelm@19801
    92
wenzelm@19801
    93
(* Exact copy of proof of comp1_reachable for the second
wenzelm@19801
    94
   component of a parallel composition.     *)
wenzelm@19801
    95
lemma comp2_reachable: "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)"
wenzelm@19801
    96
  apply (simp add: reachable_def)
wenzelm@19801
    97
  apply (erule bexE)
wenzelm@19801
    98
  apply (rule_tac x =
wenzelm@19801
    99
    "(filter_oseq (%a. a:actions (asig_of (C2))) (fst ex) , %i. snd (snd ex i))" in bexI)
wenzelm@19801
   100
(* fst(s) is in projected execution *)
wenzelm@19801
   101
  apply force
wenzelm@19801
   102
(* projected execution is indeed an execution *)
wenzelm@19801
   103
  apply (simp cong del: if_weak_cong
wenzelm@19801
   104
    add: executions_def is_execution_fragment_def par_def starts_of_def
wenzelm@19801
   105
    trans_of_def filter_oseq_def
wenzelm@19801
   106
    split add: option.split)
wenzelm@19801
   107
  done
wenzelm@19801
   108
wenzelm@19801
   109
declare split_if [split del] if_weak_cong [cong del]
wenzelm@19801
   110
wenzelm@19801
   111
(*Composition of possibility-mappings *)
wenzelm@19801
   112
lemma fxg_is_weak_pmap_of_product_IOA: 
wenzelm@19801
   113
     "[| is_weak_pmap f C1 A1;  
wenzelm@19801
   114
         externals(asig_of(A1))=externals(asig_of(C1)); 
wenzelm@19801
   115
         is_weak_pmap g C2 A2;   
wenzelm@19801
   116
         externals(asig_of(A2))=externals(asig_of(C2));  
wenzelm@19801
   117
         compat_ioas C1 C2; compat_ioas A1 A2  |]      
wenzelm@19801
   118
   ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"
wenzelm@19801
   119
  apply (unfold is_weak_pmap_def)
wenzelm@19801
   120
  apply (rule conjI)
wenzelm@19801
   121
(* start_states *)
wenzelm@19801
   122
  apply (simp add: par_def starts_of_def)
wenzelm@19801
   123
(* transitions *)
wenzelm@19801
   124
  apply (rule allI)+
wenzelm@19801
   125
  apply (rule imp_conj_lemma)
wenzelm@19801
   126
  apply (simp (no_asm) add: externals_of_par_extra)
wenzelm@19801
   127
  apply (simp (no_asm) add: par_def)
wenzelm@19801
   128
  apply (simp add: trans_of_def)
wenzelm@19801
   129
  apply (simplesubst split_if)
wenzelm@19801
   130
  apply (rule conjI)
wenzelm@19801
   131
  apply (rule impI)
wenzelm@19801
   132
  apply (erule disjE)
wenzelm@19801
   133
(* case 1      a:e(A1) | a:e(A2) *)
wenzelm@19801
   134
  apply (simp add: comp1_reachable comp2_reachable ext_is_act)
wenzelm@19801
   135
  apply (erule disjE)
wenzelm@19801
   136
(* case 2      a:e(A1) | a~:e(A2) *)
wenzelm@19801
   137
  apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act2)
wenzelm@19801
   138
(* case 3      a:~e(A1) | a:e(A2) *)
wenzelm@19801
   139
  apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act1)
wenzelm@19801
   140
(* case 4      a:~e(A1) | a~:e(A2) *)
wenzelm@19801
   141
  apply (rule impI)
wenzelm@19801
   142
  apply (subgoal_tac "a~:externals (asig_of (A1)) & a~:externals (asig_of (A2))")
wenzelm@19801
   143
(* delete auxiliary subgoal *)
wenzelm@19801
   144
  prefer 2
wenzelm@19801
   145
  apply force
wenzelm@19801
   146
  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
wenzelm@19801
   147
  apply (tactic {*
wenzelm@19801
   148
    REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
wenzelm@39159
   149
      asm_full_simp_tac(@{simpset} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *})
wenzelm@19801
   150
  done
wenzelm@19801
   151
wenzelm@19801
   152
wenzelm@19801
   153
lemma reachable_rename_ioa: "[| reachable (rename C g) s |] ==> reachable C s"
wenzelm@19801
   154
  apply (simp add: reachable_def)
wenzelm@19801
   155
  apply (erule bexE)
wenzelm@19801
   156
  apply (rule_tac x = "((%i. case (fst ex i) of None => None | Some (x) => g x) ,snd ex)" in bexI)
wenzelm@19801
   157
  apply (simp (no_asm))
wenzelm@19801
   158
(* execution is indeed an execution of C *)
wenzelm@19801
   159
  apply (simp add: executions_def is_execution_fragment_def par_def
wenzelm@19801
   160
    starts_of_def trans_of_def rename_def split add: option.split)
wenzelm@19801
   161
  apply force
wenzelm@19801
   162
  done
wenzelm@19801
   163
wenzelm@19801
   164
wenzelm@19801
   165
lemma rename_through_pmap: "[| is_weak_pmap f C A |] 
wenzelm@19801
   166
                       ==> (is_weak_pmap f (rename C g) (rename A g))"
wenzelm@19801
   167
  apply (simp add: is_weak_pmap_def)
wenzelm@19801
   168
  apply (rule conjI)
wenzelm@19801
   169
  apply (simp add: rename_def starts_of_def)
wenzelm@19801
   170
  apply (rule allI)+
wenzelm@19801
   171
  apply (rule imp_conj_lemma)
wenzelm@19801
   172
  apply (simp (no_asm) add: rename_def)
wenzelm@19801
   173
  apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
wenzelm@19801
   174
  apply safe
wenzelm@19801
   175
  apply (simplesubst split_if)
wenzelm@19801
   176
  apply (rule conjI)
wenzelm@19801
   177
  apply (rule impI)
wenzelm@19801
   178
  apply (erule disjE)
wenzelm@19801
   179
  apply (erule exE)
wenzelm@19801
   180
  apply (erule conjE)
wenzelm@19801
   181
(* x is input *)
wenzelm@19801
   182
  apply (drule sym)
wenzelm@19801
   183
  apply (drule sym)
wenzelm@19801
   184
  apply simp
wenzelm@19801
   185
  apply hypsubst+
wenzelm@19801
   186
  apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
wenzelm@19801
   187
  apply assumption
wenzelm@19801
   188
  apply simp
wenzelm@19801
   189
(* x is output *)
wenzelm@19801
   190
  apply (erule exE)
wenzelm@19801
   191
  apply (erule conjE)
wenzelm@19801
   192
  apply (drule sym)
wenzelm@19801
   193
  apply (drule sym)
wenzelm@19801
   194
  apply simp
wenzelm@19801
   195
  apply hypsubst+
wenzelm@19801
   196
  apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
wenzelm@19801
   197
  apply assumption
wenzelm@19801
   198
  apply simp
wenzelm@19801
   199
(* x is internal *)
wenzelm@19801
   200
  apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong)
wenzelm@19801
   201
  apply (rule impI)
wenzelm@19801
   202
  apply (erule conjE)
wenzelm@19801
   203
  apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
wenzelm@19801
   204
  apply auto
wenzelm@19801
   205
  done
wenzelm@19801
   206
wenzelm@19801
   207
declare split_if [split] if_weak_cong [cong]
wenzelm@17288
   208
mueller@3078
   209
end