Quelle Correctness.thy Sprache: 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

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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:

sprechenden Kalenders