src/HOLCF/IOA/meta_theory/RefMappings.thy
author wenzelm
Sun Oct 21 16:27:42 2007 +0200 (2007-10-21)
changeset 25135 4f8176c940cf
parent 19741 f65265d71426
child 26306 ed3375ac152d
permissions -rw-r--r--
modernized specifications ('definition', 'axiomatization');
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
mueller@3275
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@3071
     4
*)
mueller@3071
     5
wenzelm@17233
     6
header {* Refinement Mappings in HOLCF/IOA *}
mueller@3071
     7
wenzelm@17233
     8
theory RefMappings
wenzelm@17233
     9
imports Traces
wenzelm@17233
    10
begin
wenzelm@17233
    11
wenzelm@17233
    12
defaultsort type
mueller@3071
    13
wenzelm@25135
    14
definition
wenzelm@25135
    15
  move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
wenzelm@25135
    16
  "move ioa ex s a t =
wenzelm@17233
    17
    (is_exec_frag ioa (s,ex) &  Finite ex &
wenzelm@17233
    18
     laststate (s,ex)=t  &
nipkow@10835
    19
     mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
mueller@3071
    20
wenzelm@25135
    21
definition
wenzelm@25135
    22
  is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    23
  "is_ref_map f C A =
wenzelm@25135
    24
   ((!s:starts_of(C). f(s):starts_of(A)) &
wenzelm@17233
    25
   (!s t a. reachable C s &
wenzelm@17233
    26
            s -a--C-> t
wenzelm@25135
    27
            --> (? ex. move A ex (f s) a (f t))))"
wenzelm@17233
    28
wenzelm@25135
    29
definition
wenzelm@25135
    30
  is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    31
  "is_weak_ref_map f C A =
wenzelm@25135
    32
   ((!s:starts_of(C). f(s):starts_of(A)) &
wenzelm@17233
    33
   (!s t a. reachable C s &
wenzelm@17233
    34
            s -a--C-> t
wenzelm@17233
    35
            --> (if a:ext(C)
mueller@3071
    36
                 then (f s) -a--A-> (f t)
wenzelm@25135
    37
                 else (f s)=(f t))))"
mueller@3071
    38
wenzelm@19741
    39
wenzelm@19741
    40
subsection "transitions and moves"
wenzelm@19741
    41
wenzelm@19741
    42
wenzelm@19741
    43
lemma transition_is_ex: "s -a--A-> t ==> ? ex. move A ex s a t"
wenzelm@19741
    44
apply (rule_tac x = " (a,t) >>nil" in exI)
wenzelm@19741
    45
apply (simp add: move_def)
wenzelm@19741
    46
done
wenzelm@19741
    47
wenzelm@19741
    48
wenzelm@19741
    49
lemma nothing_is_ex: "(~a:ext A) & s=t ==> ? ex. move A ex s a t"
wenzelm@19741
    50
apply (rule_tac x = "nil" in exI)
wenzelm@19741
    51
apply (simp add: move_def)
wenzelm@19741
    52
done
wenzelm@19741
    53
wenzelm@19741
    54
wenzelm@19741
    55
lemma ei_transitions_are_ex: "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A)  
wenzelm@19741
    56
         ==> ? ex. move A ex s a s''"
wenzelm@19741
    57
apply (rule_tac x = " (a,s') >> (a',s'') >>nil" in exI)
wenzelm@19741
    58
apply (simp add: move_def)
wenzelm@19741
    59
done
wenzelm@19741
    60
wenzelm@19741
    61
wenzelm@19741
    62
lemma eii_transitions_are_ex: "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) & 
wenzelm@19741
    63
      (~a2:ext A) & (~a3:ext A) ==>  
wenzelm@19741
    64
      ? ex. move A ex s1 a1 s4"
wenzelm@19741
    65
apply (rule_tac x = " (a1,s2) >> (a2,s3) >> (a3,s4) >>nil" in exI)
wenzelm@19741
    66
apply (simp add: move_def)
wenzelm@19741
    67
done
wenzelm@19741
    68
wenzelm@19741
    69
wenzelm@19741
    70
subsection "weak_ref_map and ref_map"
wenzelm@19741
    71
wenzelm@19741
    72
lemma imp_conj_lemma: 
wenzelm@19741
    73
  "[| ext C = ext A;  
wenzelm@19741
    74
     is_weak_ref_map f C A |] ==> is_ref_map f C A"
wenzelm@19741
    75
apply (unfold is_weak_ref_map_def is_ref_map_def)
wenzelm@19741
    76
apply (tactic "safe_tac set_cs")
wenzelm@19741
    77
apply (case_tac "a:ext A")
wenzelm@19741
    78
apply (rule transition_is_ex)
wenzelm@19741
    79
apply (simp (no_asm_simp))
wenzelm@19741
    80
apply (rule nothing_is_ex)
wenzelm@19741
    81
apply simp
wenzelm@19741
    82
done
wenzelm@19741
    83
wenzelm@19741
    84
wenzelm@19741
    85
lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R"
wenzelm@19741
    86
  by blast
wenzelm@19741
    87
wenzelm@19741
    88
declare split_if [split del]
wenzelm@19741
    89
declare if_weak_cong [cong del]
wenzelm@19741
    90
wenzelm@19741
    91
lemma rename_through_pmap: "[| is_weak_ref_map f C A |]  
wenzelm@19741
    92
      ==> (is_weak_ref_map f (rename C g) (rename A g))"
wenzelm@19741
    93
apply (simp add: is_weak_ref_map_def)
wenzelm@19741
    94
apply (rule conjI)
wenzelm@19741
    95
(* 1: start states *)
wenzelm@19741
    96
apply (simp add: rename_def rename_set_def starts_of_def)
wenzelm@19741
    97
(* 2: reachable transitions *)
wenzelm@19741
    98
apply (rule allI)+
wenzelm@19741
    99
apply (rule imp_conj_lemma)
wenzelm@19741
   100
apply (simp (no_asm) add: rename_def rename_set_def)
wenzelm@19741
   101
apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
wenzelm@19741
   102
apply safe
wenzelm@19741
   103
apply (simplesubst split_if)
wenzelm@19741
   104
 apply (rule conjI)
wenzelm@19741
   105
 apply (rule impI)
wenzelm@19741
   106
 apply (erule disjE)
wenzelm@19741
   107
 apply (erule exE)
wenzelm@19741
   108
apply (erule conjE)
wenzelm@19741
   109
(* x is input *)
wenzelm@19741
   110
 apply (drule sym)
wenzelm@19741
   111
 apply (drule sym)
wenzelm@19741
   112
apply simp
wenzelm@19741
   113
apply hypsubst+
wenzelm@19741
   114
apply (frule reachable_rename)
wenzelm@19741
   115
apply simp
wenzelm@19741
   116
(* x is output *)
wenzelm@19741
   117
 apply (erule exE)
wenzelm@19741
   118
apply (erule conjE)
wenzelm@19741
   119
 apply (drule sym)
wenzelm@19741
   120
 apply (drule sym)
wenzelm@19741
   121
apply simp
wenzelm@19741
   122
apply hypsubst+
wenzelm@19741
   123
apply (frule reachable_rename)
wenzelm@19741
   124
apply simp
wenzelm@19741
   125
(* x is internal *)
wenzelm@19741
   126
apply (frule reachable_rename)
wenzelm@19741
   127
apply auto
wenzelm@19741
   128
done
wenzelm@19741
   129
wenzelm@19741
   130
declare split_if [split]
wenzelm@19741
   131
declare if_weak_cong [cong]
mueller@4559
   132
mueller@3071
   133
end