src/HOL/IOA/Solve.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 7499 23e090051cb8
child 17288 aa3833fb7bee
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/IOA/Solve.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 
     6 Weak possibilities mapping (abstraction)
     7 *)
     8 
     9 open Solve; 
    10 
    11 Addsimps [mk_trace_thm,trans_in_actions];
    12 
    13 Goalw [is_weak_pmap_def,traces_def]
    14   "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
    15 \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
    16 
    17   by (simp_tac(simpset() addsimps [has_trace_def])1);
    18   by Safe_tac;
    19   by (rename_tac "ex1 ex2" 1);
    20 
    21   (* choose same trace, therefore same NF *)
    22   by (res_inst_tac[("x","mk_trace  C ex1")] exI 1);
    23   by (Asm_full_simp_tac 1);
    24 
    25   (* give execution of abstract automata *)
    26   by (res_inst_tac[("x","(mk_trace A ex1,%i. f (ex2 i))")] bexI 1);
    27 
    28   (* Traces coincide *)
    29    by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
    30 
    31   (* Use lemma *)
    32   by (ftac states_of_exec_reachable 1);
    33 
    34   (* Now show that it's an execution *)
    35   by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
    36   by Safe_tac;
    37 
    38   (* Start states map to start states *)
    39   by (dtac bspec 1);
    40   by (atac 1);
    41 
    42   (* Show that it's an execution fragment *)
    43   by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
    44   by Safe_tac;
    45 
    46   by (eres_inst_tac [("x","ex2 n")] allE 1);
    47   by (eres_inst_tac [("x","ex2 (Suc n)")] allE 1);
    48   by (eres_inst_tac [("x","a")] allE 1);
    49   by (Asm_full_simp_tac 1);
    50 qed "trace_inclusion";
    51 
    52 (* Lemmata *)
    53 
    54 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    55   by (fast_tac (claset() addDs prems) 1);
    56 val imp_conj_lemma = result();
    57 
    58 
    59 (* fist_order_tautology of externals_of_par *)
    60 goal IOA.thy "a:externals(asig_of(A1||A2)) =    \
    61 \  (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) |  \
    62 \  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
    63 \  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
    64 by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
    65  by (Fast_tac 1);
    66 val externals_of_par_extra = result(); 
    67 
    68 Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
    69 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    70 by (etac bexE 1);
    71 by (res_inst_tac [("x",
    72    "(filter_oseq (%a. a:actions(asig_of(C1))) \
    73 \                (fst ex),                                                \
    74 \    %i. fst (snd ex i))")]  bexI 1);
    75 (* fst(s) is in projected execution *)
    76  by (Force_tac 1);
    77 (* projected execution is indeed an execution *)
    78 by (asm_full_simp_tac
    79       (simpset() delcongs [if_weak_cong]
    80 		 addsimps [executions_def,is_execution_fragment_def,
    81 			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
    82                  addsplits [option.split]) 1);
    83 qed"comp1_reachable";
    84 
    85 
    86 (* Exact copy of proof of comp1_reachable for the second 
    87    component of a parallel composition.     *)
    88 Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    89 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    90 by (etac bexE 1);
    91 by (res_inst_tac [("x",
    92    "(filter_oseq (%a. a:actions(asig_of(C2)))\
    93 \                (fst ex),                                                \
    94 \    %i. snd (snd ex i))")]  bexI 1);
    95 (* fst(s) is in projected execution *)
    96  by (Force_tac 1);
    97 (* projected execution is indeed an execution *)
    98 by (asm_full_simp_tac
    99       (simpset() delcongs [if_weak_cong]
   100 		 addsimps [executions_def,is_execution_fragment_def,
   101 			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
   102                  addsplits [option.split]) 1);
   103 qed"comp2_reachable";
   104 
   105 Delsplits [split_if]; Delcongs [if_weak_cong];
   106 
   107 (* THIS THEOREM IS NEVER USED (lcp)
   108    Composition of possibility-mappings *)
   109 Goalw [is_weak_pmap_def]
   110      "[| is_weak_pmap f C1 A1; \
   111 \        externals(asig_of(A1))=externals(asig_of(C1));\
   112 \        is_weak_pmap g C2 A2;  \
   113 \        externals(asig_of(A2))=externals(asig_of(C2)); \
   114 \        compat_ioas C1 C2; compat_ioas A1 A2  |]     \
   115 \  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
   116  by (rtac conjI 1);
   117 (* start_states *)
   118  by (asm_full_simp_tac (simpset() addsimps [par_def, starts_of_def]) 1);
   119 (* transitions *)
   120 by (REPEAT (rtac allI 1));
   121 by (rtac imp_conj_lemma 1);
   122 by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
   123 by (simp_tac (simpset() addsimps [par_def]) 1);
   124 by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
   125 by (stac split_if 1);
   126 by (rtac conjI 1);
   127 by (rtac impI 1); 
   128 by (etac disjE 1);
   129 (* case 1      a:e(A1) | a:e(A2) *)
   130 by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
   131                                     ext_is_act]) 1);
   132 by (etac disjE 1);
   133 (* case 2      a:e(A1) | a~:e(A2) *)
   134 by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
   135              ext_is_act,ext1_ext2_is_not_act2]) 1);
   136 (* case 3      a:~e(A1) | a:e(A2) *)
   137 by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable,
   138              ext_is_act,ext1_ext2_is_not_act1]) 1);
   139 (* case 4      a:~e(A1) | a~:e(A2) *)
   140 by (rtac impI 1);
   141 by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
   142 (* delete auxiliary subgoal *)
   143 by (Asm_full_simp_tac 2);
   144 by (Fast_tac 2);
   145 by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
   146                  addsplits [split_if]) 1);
   147 by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   148 	   asm_full_simp_tac(simpset() addsimps[comp1_reachable,
   149 						comp2_reachable])1));
   150 qed"fxg_is_weak_pmap_of_product_IOA";
   151 
   152 
   153 Goal "[| reachable (rename C g) s |] ==> reachable C s";
   154 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
   155 by (etac bexE 1);
   156 by (res_inst_tac [("x",
   157    "((%i. case (fst ex i) \
   158 \         of None => None\
   159 \          | Some(x) => g x) ,snd ex)")]  bexI 1);
   160 by (Simp_tac 1);
   161 (* execution is indeed an execution of C *)
   162 by (asm_full_simp_tac
   163       (simpset() addsimps [executions_def,is_execution_fragment_def,
   164                           par_def,starts_of_def,trans_of_def,rename_def]
   165                 addsplits [option.split]) 1);
   166 by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
   167 qed"reachable_rename_ioa";
   168 
   169 
   170 Goal "[| is_weak_pmap f C A |]\
   171 \                      ==> (is_weak_pmap f (rename C g) (rename A g))";
   172 by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
   173 by (rtac conjI 1);
   174 by (asm_full_simp_tac (simpset() addsimps [rename_def,starts_of_def]) 1);
   175 by (REPEAT (rtac allI 1));
   176 by (rtac imp_conj_lemma 1);
   177 by (simp_tac (simpset() addsimps [rename_def]) 1);
   178 by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
   179 by Safe_tac;
   180 by (stac split_if 1);
   181  by (rtac conjI 1);
   182  by (rtac impI 1);
   183  by (etac disjE 1);
   184  by (etac exE 1);
   185 by (etac conjE 1);
   186 (* x is input *)
   187  by (dtac sym 1);
   188  by (dtac sym 1);
   189 by (Asm_full_simp_tac 1);
   190 by (REPEAT (hyp_subst_tac 1));
   191 by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   192 by (assume_tac 1);
   193 by (Asm_full_simp_tac 1);
   194 (* x is output *)
   195  by (etac exE 1);
   196 by (etac conjE 1);
   197  by (dtac sym 1);
   198  by (dtac sym 1);
   199 by (Asm_full_simp_tac 1);
   200 by (REPEAT (hyp_subst_tac 1));
   201 by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   202 by (assume_tac 1);
   203 by (Asm_full_simp_tac 1);
   204 (* x is internal *)
   205 by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] 
   206 	               addcongs [conj_cong]) 1);
   207 by (rtac impI 1);
   208 by (etac conjE 1);
   209 by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
   210 by Auto_tac;
   211 qed"rename_through_pmap";
   212 
   213 Addsplits [split_if];
   214 Addcongs  [if_weak_cong];