1(*  Title:      HOL/HOLCF/IOA/ex/TrivEx2.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Trivial Abstraction Example with fairness\<close>
6
7theory TrivEx2
8imports IOA.Abstraction
9begin
10
11datatype action = INC
12
13definition
14  C_asig :: "action signature" where
15  "C_asig = ({},{INC},{})"
16definition
17  C_trans :: "(action, nat)transition set" where
18  "C_trans =
19   {tr. let s = fst(tr);
20            t = snd(snd(tr))
21        in case fst(snd(tr))
22        of
23        INC       => t = Suc(s)}"
24definition
25  C_ioa :: "(action, nat)ioa" where
26  "C_ioa = (C_asig, {0}, C_trans,{},{})"
27definition
28  C_live_ioa :: "(action, nat)live_ioa" where
29  "C_live_ioa = (C_ioa, WF C_ioa {INC})"
30
31definition
32  A_asig :: "action signature" where
33  "A_asig = ({},{INC},{})"
34definition
35  A_trans :: "(action, bool)transition set" where
36  "A_trans =
37   {tr. let s = fst(tr);
38            t = snd(snd(tr))
39        in case fst(snd(tr))
40        of
41        INC       => t = True}"
42definition
43  A_ioa :: "(action, bool)ioa" where
44  "A_ioa = (A_asig, {False}, A_trans,{},{})"
45definition
46  A_live_ioa :: "(action, bool)live_ioa" where
47  "A_live_ioa = (A_ioa, WF A_ioa {INC})"
48
49definition
50  h_abs :: "nat => bool" where
51  "h_abs n = (n~=0)"
52
53axiomatization where
54  MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
55
56
57lemma h_abs_is_abstraction:
58"is_abstraction h_abs C_ioa A_ioa"
59apply (unfold is_abstraction_def)
60apply (rule conjI)
61txt \<open>start states\<close>
62apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
63txt \<open>step case\<close>
64apply (rule allI)+
65apply (rule imp_conj_lemma)
66apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
67apply (induct_tac "a")
68apply (simp (no_asm) add: h_abs_def)
69done
70
71
72lemma Enabled_implication:
73    "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"
74  apply (unfold Enabled_def enabled_def h_abs_def A_ioa_def C_ioa_def A_trans_def
75    C_trans_def trans_of_def)
76  apply auto
77  done
78
79
80lemma h_abs_is_liveabstraction:
81"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
82apply (unfold is_live_abstraction_def)
83apply auto
84txt \<open>is_abstraction\<close>
85apply (rule h_abs_is_abstraction)
86txt \<open>temp_weakening\<close>
87apply abstraction
88apply (erule Enabled_implication)
89done
90
91
92lemma TrivEx2_abstraction:
93  "validLIOA C_live_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
94apply (unfold C_live_ioa_def)
95apply (rule AbsRuleT2)
96apply (rule h_abs_is_liveabstraction)
97apply (rule MC_result)
98apply abstraction
99apply (simp add: h_abs_def)
100done
101
102end
103