src/HOL/HOLCF/IOA/ex/TrivEx.thy
changeset 62002 f1599e98c4d0
parent 61999 89291b5d0ede
child 62004 8c6226d88ced
equal deleted inserted replaced
62001:1f2788fb0b8b 62002:f1599e98c4d0
     1 (*  Title:      HOL/HOLCF/IOA/ex/TrivEx.thy
     1 (*  Title:      HOL/HOLCF/IOA/ex/TrivEx.thy
     2     Author:     Olaf Müller
     2     Author:     Olaf Müller
     3 *)
     3 *)
     4 
     4 
     5 section {* Trivial Abstraction Example *}
     5 section \<open>Trivial Abstraction Example\<close>
     6 
     6 
     7 theory TrivEx
     7 theory TrivEx
     8 imports Abstraction
     8 imports Abstraction
     9 begin
     9 begin
    10 
    10 
    49 
    49 
    50 lemma h_abs_is_abstraction:
    50 lemma h_abs_is_abstraction:
    51   "is_abstraction h_abs C_ioa A_ioa"
    51   "is_abstraction h_abs C_ioa A_ioa"
    52 apply (unfold is_abstraction_def)
    52 apply (unfold is_abstraction_def)
    53 apply (rule conjI)
    53 apply (rule conjI)
    54 txt {* start states *}
    54 txt \<open>start states\<close>
    55 apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
    55 apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
    56 txt {* step case *}
    56 txt \<open>step case\<close>
    57 apply (rule allI)+
    57 apply (rule allI)+
    58 apply (rule imp_conj_lemma)
    58 apply (rule imp_conj_lemma)
    59 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
    59 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
    60 apply (induct_tac "a")
    60 apply (induct_tac "a")
    61 apply (simp add: h_abs_def)
    61 apply (simp add: h_abs_def)