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