src/HOLCF/IOA/ex/TrivEx2.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/IOA/ex/TrivEx2.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,102 +0,0 @@
     1.4 -(*  Title:      HOLCF/IOA/TrivEx.thy
     1.5 -    Author:     Olaf Müller
     1.6 -*)
     1.7 -
     1.8 -header {* Trivial Abstraction Example with fairness *}
     1.9 -
    1.10 -theory TrivEx2
    1.11 -imports IOA Abstraction
    1.12 -begin
    1.13 -
    1.14 -datatype action = INC
    1.15 -
    1.16 -definition
    1.17 -  C_asig :: "action signature" where
    1.18 -  "C_asig = ({},{INC},{})"
    1.19 -definition
    1.20 -  C_trans :: "(action, nat)transition set" where
    1.21 -  "C_trans =
    1.22 -   {tr. let s = fst(tr);
    1.23 -            t = snd(snd(tr))
    1.24 -        in case fst(snd(tr))
    1.25 -        of
    1.26 -        INC       => t = Suc(s)}"
    1.27 -definition
    1.28 -  C_ioa :: "(action, nat)ioa" where
    1.29 -  "C_ioa = (C_asig, {0}, C_trans,{},{})"
    1.30 -definition
    1.31 -  C_live_ioa :: "(action, nat)live_ioa" where
    1.32 -  "C_live_ioa = (C_ioa, WF C_ioa {INC})"
    1.33 -
    1.34 -definition
    1.35 -  A_asig :: "action signature" where
    1.36 -  "A_asig = ({},{INC},{})"
    1.37 -definition
    1.38 -  A_trans :: "(action, bool)transition set" where
    1.39 -  "A_trans =
    1.40 -   {tr. let s = fst(tr);
    1.41 -            t = snd(snd(tr))
    1.42 -        in case fst(snd(tr))
    1.43 -        of
    1.44 -        INC       => t = True}"
    1.45 -definition
    1.46 -  A_ioa :: "(action, bool)ioa" where
    1.47 -  "A_ioa = (A_asig, {False}, A_trans,{},{})"
    1.48 -definition
    1.49 -  A_live_ioa :: "(action, bool)live_ioa" where
    1.50 -  "A_live_ioa = (A_ioa, WF A_ioa {INC})"
    1.51 -
    1.52 -definition
    1.53 -  h_abs :: "nat => bool" where
    1.54 -  "h_abs n = (n~=0)"
    1.55 -
    1.56 -axiomatization where
    1.57 -  MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
    1.58 -
    1.59 -
    1.60 -lemma h_abs_is_abstraction:
    1.61 -"is_abstraction h_abs C_ioa A_ioa"
    1.62 -apply (unfold is_abstraction_def)
    1.63 -apply (rule conjI)
    1.64 -txt {* start states *}
    1.65 -apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
    1.66 -txt {* step case *}
    1.67 -apply (rule allI)+
    1.68 -apply (rule imp_conj_lemma)
    1.69 -apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
    1.70 -apply (induct_tac "a")
    1.71 -apply (simp (no_asm) add: h_abs_def)
    1.72 -done
    1.73 -
    1.74 -
    1.75 -lemma Enabled_implication:
    1.76 -    "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"
    1.77 -  apply (unfold Enabled_def enabled_def h_abs_def A_ioa_def C_ioa_def A_trans_def
    1.78 -    C_trans_def trans_of_def)
    1.79 -  apply auto
    1.80 -  done
    1.81 -
    1.82 -
    1.83 -lemma h_abs_is_liveabstraction:
    1.84 -"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
    1.85 -apply (unfold is_live_abstraction_def)
    1.86 -apply auto
    1.87 -txt {* is_abstraction *}
    1.88 -apply (rule h_abs_is_abstraction)
    1.89 -txt {* temp_weakening *}
    1.90 -apply abstraction
    1.91 -apply (erule Enabled_implication)
    1.92 -done
    1.93 -
    1.94 -
    1.95 -lemma TrivEx2_abstraction:
    1.96 -  "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"
    1.97 -apply (unfold C_live_ioa_def)
    1.98 -apply (rule AbsRuleT2)
    1.99 -apply (rule h_abs_is_liveabstraction)
   1.100 -apply (rule MC_result)
   1.101 -apply abstraction
   1.102 -apply (simp add: h_abs_def)
   1.103 -done
   1.104 -
   1.105 -end