author  huffman 
Sat, 27 Nov 2010 16:08:10 0800  
changeset 40774  0437dbc127b3 
parent 36452  src/HOLCF/IOA/Storage/Correctness.thy@d37c6eed8117 
child 40945  b8703f63bfb2 
permissions  rwrr 
6008  1 
(* Title: HOL/IOA/example/Correctness.thy 
12218  2 
Author: Olaf Müller 
6008  3 
*) 
4 

17244  5 
header {* Correctness Proof *} 
6008  6 

17244  7 
theory Correctness 
8 
imports SimCorrectness Spec Impl 

9 
begin 

6008  10 

36452  11 
default_sort type 
6008  12 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19740
diff
changeset

13 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19740
diff
changeset

14 
sim_relation :: "((nat * bool) * (nat set * bool)) set" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19740
diff
changeset

15 
"sim_relation = {qua. let c = fst qua; a = snd qua ; 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19740
diff
changeset

16 
k = fst c; b = snd c; 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19740
diff
changeset

17 
used = fst a; c = snd a 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19740
diff
changeset

18 
in 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19740
diff
changeset

19 
(! l:used. l < k) & b=c}" 
6008  20 

19740  21 
declare split_paired_Ex [simp del] 
22 

23 

24 
(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive 

25 
simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans 

26 
Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired, 

27 
as this can be done globally *) 

28 

29 
lemma issimulation: 

30 
"is_simulation sim_relation impl_ioa spec_ioa" 

31 
apply (simp (no_asm) add: is_simulation_def) 

32 
apply (rule conjI) 

33 
txt {* start states *} 

26359  34 
apply (auto)[1] 
19740  35 
apply (rule_tac x = " ({},False) " in exI) 
27361  36 
apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def) 
19740  37 
txt {* mainpart *} 
38 
apply (rule allI)+ 

39 
apply (rule imp_conj_lemma) 

40 
apply (rename_tac k b used c k' b' a) 

41 
apply (induct_tac "a") 

27361  42 
apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def) 
26359  43 
apply auto 
19740  44 
txt {* NEW *} 
45 
apply (rule_tac x = "(used,True)" in exI) 

46 
apply simp 

47 
apply (rule transition_is_ex) 

27361  48 
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) 
19740  49 
txt {* LOC *} 
50 
apply (rule_tac x = " (used Un {k},False) " in exI) 

51 
apply (simp add: less_SucI) 

52 
apply (rule transition_is_ex) 

27361  53 
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) 
19740  54 
apply fast 
55 
txt {* FREE *} 

56 
apply (rule_tac x = " (used  {nat},c) " in exI) 

57 
apply simp 

58 
apply (rule transition_is_ex) 

27361  59 
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) 
19740  60 
done 
61 

62 

63 
lemma implementation: 

64 
"impl_ioa =< spec_ioa" 

65 
apply (unfold ioa_implements_def) 

66 
apply (rule conjI) 

27361  67 
apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def 
19740  68 
asig_outputs_def asig_of_def asig_inputs_def) 
69 
apply (rule trace_inclusion_for_simulations) 

27361  70 
apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def 
19740  71 
externals_def asig_outputs_def asig_of_def asig_inputs_def) 
72 
apply (rule issimulation) 

73 
done 

17244  74 

75 
end 