Up to index of Isabelle/HOLCF/IOA/ABP
theory Correctness(* Title: HOLCF/IOA/ABP/Correctness.thy ID: $Id: Correctness.thy,v 1.5 2005/09/03 14:50:22 wenzelm Exp $ Author: Olaf Müller *) header {* The main correctness proof: System_fin implements System *} theory Correctness imports IOA Env Impl Impl_finite begin consts reduce :: "'a list => 'a list" abs :: 'c system_ioa :: "('m action, bool * 'm impl_state)ioa" system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" primrec reduce_Nil: "reduce [] = []" reduce_Cons: "reduce(x#xs) = (case xs of [] => [x] | y#ys => (if (x=y) then reduce xs else (x#(reduce xs))))" defs system_def: "system_ioa == (env_ioa || impl_ioa)" system_fin_def: "system_fin_ioa == (env_ioa || impl_fin_ioa)" abs_def: "abs == (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))" axioms sys_IOA: "IOA system_ioa" sys_fin_IOA: "IOA system_fin_ioa" ML {* use_legacy_bindings (the_context ()) *} end
theorem hd_is_reduce_hd:
s ≠ [] --> hd s = hd (reduce s)
theorem rev_red_not_nil:
l ≠ [] ==> reverse (reduce l) ≠ []
theorem last_ind_on_first:
l ≠ [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))
theorem reduce_hd:
if x = hd (reverse (reduce l)) ∧ reduce l ≠ [] then reduce (l @ [x]) = reduce l else reduce (l @ [x]) = reduce l @ [x]
theorem channel_abstraction:
is_weak_ref_map reduce ch_ioa ch_fin_ioa
theorem sender_abstraction:
is_weak_ref_map reduce srch_ioa srch_fin_ioa
theorem receiver_abstraction:
is_weak_ref_map reduce rsch_ioa rsch_fin_ioa
theorem sender_unchanged:
is_weak_ref_map (%id. id) sender_ioa sender_ioa
theorem receiver_unchanged:
is_weak_ref_map (%id. id) receiver_ioa receiver_ioa
theorem env_unchanged:
is_weak_ref_map (%id. id) env_ioa env_ioa