(* Title: HOL/HOLCF/IOA/Storage/Correctness.thy Author: Olaf Müller
*)
section \<open>Correctness Proof\<close>
theory Correctness imports IOA.SimCorrectness Spec Impl begin
default_sort type
definition
sim_relation :: "((nat * bool) * (nat set * bool)) set"where "sim_relation = {qua. let c = fst qua; a = snd qua ;
k = fst c; b = snd c;
used = fst a; c = snd a in
(\<forall>l\<in>used. l < k) \<and> b=c}"
declare split_paired_Ex [simp del]
(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired,
as this can be done globally *)
lemma issimulation: "is_simulation sim_relation impl_ioa spec_ioa" apply (simp (no_asm) add: is_simulation_def) apply (rule conjI) txt\<open>start states\<close> apply (auto)[1] apply (rule_tac x = " ({},False) "in exI) apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def) txt\<open>main-part\<close> apply (rule allI)+ apply (rule imp_conj_lemma) apply (rename_tac k b used c k' b' a) apply (induct_tac "a") apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def) apply auto txt\<open>NEW\<close> apply (rule_tac x = "(used,True)"in exI) apply simp apply (rule transition_is_ex) apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) txt\<open>LOC\<close> apply (rule_tac x = " (used Un {k},False) "in exI) apply (simp add: less_SucI) apply (rule transition_is_ex) apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) apply fast txt\<open>FREE\<close> apply (rename_tac nat, rule_tac x = " (used - {nat},c) "in exI) apply simp apply (rule transition_is_ex) apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def) done
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
