author  wenzelm 
Wed, 30 Dec 2015 22:09:44 +0100  
changeset 62004  8c6226d88ced 
parent 62002  f1599e98c4d0 
child 62009  ecb5212d5885 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/IOA/ex/TrivEx2.thy 
40945  2 
Author: Olaf MÃ¼ller 
6470  3 
*) 
4 

62002  5 
section \<open>Trivial Abstraction Example with fairness\<close> 
17244  6 

7 
theory TrivEx2 

8 
imports IOA Abstraction 

9 
begin 

6470  10 

58310  11 
datatype action = INC 
6470  12 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

13 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

14 
C_asig :: "action signature" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

15 
"C_asig = ({},{INC},{})" 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

16 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

17 
C_trans :: "(action, nat)transition set" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

18 
"C_trans = 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

19 
{tr. let s = fst(tr); 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

20 
t = snd(snd(tr)) 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

21 
in case fst(snd(tr)) 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

22 
of 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

23 
INC => t = Suc(s)}" 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

24 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

25 
C_ioa :: "(action, nat)ioa" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

26 
"C_ioa = (C_asig, {0}, C_trans,{},{})" 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

27 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

28 
C_live_ioa :: "(action, nat)live_ioa" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

29 
"C_live_ioa = (C_ioa, WF C_ioa {INC})" 
6470  30 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

31 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

32 
A_asig :: "action signature" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

33 
"A_asig = ({},{INC},{})" 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

34 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

35 
A_trans :: "(action, bool)transition set" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

36 
"A_trans = 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

37 
{tr. let s = fst(tr); 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

38 
t = snd(snd(tr)) 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

39 
in case fst(snd(tr)) 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

40 
of 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

41 
INC => t = True}" 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

42 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

43 
A_ioa :: "(action, bool)ioa" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

44 
"A_ioa = (A_asig, {False}, A_trans,{},{})" 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

45 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

46 
A_live_ioa :: "(action, bool)live_ioa" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

47 
"A_live_ioa = (A_ioa, WF A_ioa {INC})" 
6470  48 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

49 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

50 
h_abs :: "nat => bool" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

51 
"h_abs n = (n~=0)" 
6470  52 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

53 
axiomatization where 
62004  54 
MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)" 
6470  55 

19740  56 

57 
lemma h_abs_is_abstraction: 

58 
"is_abstraction h_abs C_ioa A_ioa" 

59 
apply (unfold is_abstraction_def) 

60 
apply (rule conjI) 

62002  61 
txt \<open>start states\<close> 
19740  62 
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def) 
62002  63 
txt \<open>step case\<close> 
19740  64 
apply (rule allI)+ 
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) 

67 
apply (induct_tac "a") 

68 
apply (simp (no_asm) add: h_abs_def) 

69 
done 

70 

71 

72 
lemma 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 

80 
lemma h_abs_is_liveabstraction: 

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) 

83 
apply auto 

62002  84 
txt \<open>is_abstraction\<close> 
19740  85 
apply (rule h_abs_is_abstraction) 
62002  86 
txt \<open>temp_weakening\<close> 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
25135
diff
changeset

87 
apply abstraction 
19740  88 
apply (erule Enabled_implication) 
89 
done 

90 

91 

92 
lemma TrivEx2_abstraction: 

62004  93 
"validLIOA C_live_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)" 
19740  94 
apply (unfold C_live_ioa_def) 
95 
apply (rule AbsRuleT2) 

96 
apply (rule h_abs_is_liveabstraction) 

97 
apply (rule MC_result) 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
25135
diff
changeset

98 
apply abstraction 
19740  99 
apply (simp add: h_abs_def) 
100 
done 

17244  101 

102 
end 