| products/sources/formale sprachen/Isabelle/HOL/HOLCF/IOA/Storage/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Correctness.thy Sprache: IsabelleOriginal von: Isabelle© |
|
||||||
|
(* 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 lemma implementation: "impl_ioa =<| spec_ioa" apply (unfold ioa_implements_def) apply (rule conjI) apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def asig_outputs_def asig_of_def asig_inputs_def) apply (rule trace_inclusion_for_simulations) apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def externals_def asig_outputs_def asig_of_def asig_inputs_def) apply (rule issimulation) done end ¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
