author  wenzelm 
Wed, 30 Dec 2015 21:57:52 +0100  
changeset 62002  f1599e98c4d0 
parent 61999  89291b5d0ede 
child 62004  8c6226d88ced 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/IOA/ex/TrivEx.thy 
40945  2 
Author: Olaf MÃ¼ller 
6470  3 
*) 
4 

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

7 
theory TrivEx 

8 
imports 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,{},{})" 
6470  27 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

41 
"A_ioa = (A_asig, {False}, A_trans,{},{})" 
6470  42 

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

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

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

45 
"h_abs n = (n~=0)" 
6470  46 

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

47 
axiomatization where 
61999  48 
MC_result: "validIOA A_ioa (\<diamond>\<box><%(b,a,c). b>)" 
6470  49 

19740  50 
lemma h_abs_is_abstraction: 
51 
"is_abstraction h_abs C_ioa A_ioa" 

52 
apply (unfold is_abstraction_def) 

53 
apply (rule conjI) 

62002  54 
txt \<open>start states\<close> 
19740  55 
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def) 
62002  56 
txt \<open>step case\<close> 
19740  57 
apply (rule allI)+ 
58 
apply (rule imp_conj_lemma) 

59 
apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def) 

60 
apply (induct_tac "a") 

61 
apply (simp add: h_abs_def) 

62 
done 

63 

61999  64 
lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box><%(n,a,m). n~=0>)" 
19740  65 
apply (rule AbsRuleT1) 
66 
apply (rule h_abs_is_abstraction) 

67 
apply (rule MC_result) 

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

68 
apply abstraction 
19740  69 
apply (simp add: h_abs_def) 
70 
done 

17244  71 

72 
end 