1(*  Title:      HOL/HOLCF/IOA/Storage/Correctness.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Correctness Proof\<close>
6
7theory Correctness
8imports IOA.SimCorrectness Spec Impl
9begin
10
11default_sort type
12
13definition
14  sim_relation :: "((nat * bool) * (nat set * bool)) set" where
15  "sim_relation = {qua. let c = fst qua; a = snd qua ;
16                            k = fst c;   b = snd c;
17                            used = fst a; c = snd a
18                        in
19                        (\<forall>l\<in>used. l < k) \<and> b=c}"
20
21declare 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
29lemma issimulation:
30      "is_simulation sim_relation impl_ioa spec_ioa"
31apply (simp (no_asm) add: is_simulation_def)
32apply (rule conjI)
33txt \<open>start states\<close>
34apply (auto)[1]
35apply (rule_tac x = " ({},False) " in exI)
36apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def)
37txt \<open>main-part\<close>
38apply (rule allI)+
39apply (rule imp_conj_lemma)
40apply (rename_tac k b used c k' b' a)
41apply (induct_tac "a")
42apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def)
43apply auto
44txt \<open>NEW\<close>
45apply (rule_tac x = "(used,True)" in exI)
46apply simp
47apply (rule transition_is_ex)
48apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
49txt \<open>LOC\<close>
50apply (rule_tac x = " (used Un {k},False) " in exI)
51apply (simp add: less_SucI)
52apply (rule transition_is_ex)
53apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
54apply fast
55txt \<open>FREE\<close>
56apply (rename_tac nat, rule_tac x = " (used - {nat},c) " in exI)
57apply simp
58apply (rule transition_is_ex)
59apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
60done
61
62
63lemma implementation:
64"impl_ioa =<| spec_ioa"
65apply (unfold ioa_implements_def)
66apply (rule conjI)
67apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def
68  asig_outputs_def asig_of_def asig_inputs_def)
69apply (rule trace_inclusion_for_simulations)
70apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def
71  externals_def asig_outputs_def asig_of_def asig_inputs_def)
72apply (rule issimulation)
73done
74
75end
76