1(*  Title:      HOL/HOLCF/IOA/ex/TrivEx.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Trivial Abstraction Example\<close>
6
7theory TrivEx
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,{},{})"
27
28definition
29  A_asig :: "action signature" where
30  "A_asig = ({},{INC},{})"
31definition
32  A_trans :: "(action, bool)transition set" where
33  "A_trans =
34   {tr. let s = fst(tr);
35            t = snd(snd(tr))
36        in case fst(snd(tr))
37        of
38        INC       => t = True}"
39definition
40  A_ioa :: "(action, bool)ioa" where
41  "A_ioa = (A_asig, {False}, A_trans,{},{})"
42
43definition
44  h_abs :: "nat => bool" where
45  "h_abs n = (n~=0)"
46
47axiomatization where
48  MC_result: "validIOA A_ioa (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
49
50lemma h_abs_is_abstraction:
51  "is_abstraction h_abs C_ioa A_ioa"
52apply (unfold is_abstraction_def)
53apply (rule conjI)
54txt \<open>start states\<close>
55apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
56txt \<open>step case\<close>
57apply (rule allI)+
58apply (rule imp_conj_lemma)
59apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
60apply (induct_tac "a")
61apply (simp add: h_abs_def)
62done
63
64lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
65apply (rule AbsRuleT1)
66apply (rule h_abs_is_abstraction)
67apply (rule MC_result)
68apply abstraction
69apply (simp add: h_abs_def)
70done
71
72end
73