src/HOL/HOLCF/IOA/ex/TrivEx2.thy
changeset 62002 f1599e98c4d0
parent 61999 89291b5d0ede
child 62004 8c6226d88ced
equal deleted inserted replaced
62001:1f2788fb0b8b 62002:f1599e98c4d0
     1 (*  Title:      HOL/HOLCF/IOA/ex/TrivEx2.thy
     1 (*  Title:      HOL/HOLCF/IOA/ex/TrivEx2.thy
     2     Author:     Olaf Müller
     2     Author:     Olaf Müller
     3 *)
     3 *)
     4 
     4 
     5 section {* Trivial Abstraction Example with fairness *}
     5 section \<open>Trivial Abstraction Example with fairness\<close>
     6 
     6 
     7 theory TrivEx2
     7 theory TrivEx2
     8 imports IOA Abstraction
     8 imports IOA Abstraction
     9 begin
     9 begin
    10 
    10 
    56 
    56 
    57 lemma h_abs_is_abstraction:
    57 lemma h_abs_is_abstraction:
    58 "is_abstraction h_abs C_ioa A_ioa"
    58 "is_abstraction h_abs C_ioa A_ioa"
    59 apply (unfold is_abstraction_def)
    59 apply (unfold is_abstraction_def)
    60 apply (rule conjI)
    60 apply (rule conjI)
    61 txt {* start states *}
    61 txt \<open>start states\<close>
    62 apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
    62 apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
    63 txt {* step case *}
    63 txt \<open>step case\<close>
    64 apply (rule allI)+
    64 apply (rule allI)+
    65 apply (rule imp_conj_lemma)
    65 apply (rule imp_conj_lemma)
    66 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
    66 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
    67 apply (induct_tac "a")
    67 apply (induct_tac "a")
    68 apply (simp (no_asm) add: h_abs_def)
    68 apply (simp (no_asm) add: h_abs_def)
    79 
    79 
    80 lemma h_abs_is_liveabstraction:
    80 lemma h_abs_is_liveabstraction:
    81 "is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
    81 "is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
    82 apply (unfold is_live_abstraction_def)
    82 apply (unfold is_live_abstraction_def)
    83 apply auto
    83 apply auto
    84 txt {* is_abstraction *}
    84 txt \<open>is_abstraction\<close>
    85 apply (rule h_abs_is_abstraction)
    85 apply (rule h_abs_is_abstraction)
    86 txt {* temp_weakening *}
    86 txt \<open>temp_weakening\<close>
    87 apply abstraction
    87 apply abstraction
    88 apply (erule Enabled_implication)
    88 apply (erule Enabled_implication)
    89 done
    89 done
    90 
    90 
    91 
    91