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