author  wenzelm 
Tue, 29 Mar 2011 17:47:11 +0200  
changeset 42151  4da4fc77664b 
parent 40945  b8703f63bfb2 
child 58249  180f1b3508ed 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/IOA/ex/TrivEx2.thy 
40945  2 
Author: Olaf MÃ¼ller 
6470  3 
*) 
4 

17244  5 
header {* Trivial Abstraction Example with fairness *} 
6 

7 
theory TrivEx2 

8 
imports IOA Abstraction 

9 
begin 

6470  10 

11 
datatype action = INC 

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 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19740
diff
changeset

54 
MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)" 
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) 

61 
txt {* start states *} 

62 
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def) 

63 
txt {* step case *} 

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 

84 
txt {* is_abstraction *} 

85 
apply (rule h_abs_is_abstraction) 

86 
txt {* temp_weakening *} 

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: 

93 
"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)" 

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 