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