src/HOL/HOLCF/IOA/Storage/Correctness.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 36452 src/HOLCF/IOA/Storage/Correctness.thy@d37c6eed8117
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 (*  Title:      HOL/IOA/example/Correctness.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 header {* Correctness Proof *}
     6 
     7 theory Correctness
     8 imports SimCorrectness Spec Impl
     9 begin
    10 
    11 default_sort type
    12 
    13 definition
    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                         (! l:used. l < k) & b=c}"
    20 
    21 declare 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 
    29 lemma issimulation:
    30       "is_simulation sim_relation impl_ioa spec_ioa"
    31 apply (simp (no_asm) add: is_simulation_def)
    32 apply (rule conjI)
    33 txt {* start states *}
    34 apply (auto)[1]
    35 apply (rule_tac x = " ({},False) " in exI)
    36 apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def)
    37 txt {* main-part *}
    38 apply (rule allI)+
    39 apply (rule imp_conj_lemma)
    40 apply (rename_tac k b used c k' b' a)
    41 apply (induct_tac "a")
    42 apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def)
    43 apply auto
    44 txt {* NEW *}
    45 apply (rule_tac x = "(used,True)" in exI)
    46 apply simp
    47 apply (rule transition_is_ex)
    48 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
    49 txt {* LOC *}
    50 apply (rule_tac x = " (used Un {k},False) " in exI)
    51 apply (simp add: less_SucI)
    52 apply (rule transition_is_ex)
    53 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
    54 apply fast
    55 txt {* FREE *}
    56 apply (rule_tac x = " (used - {nat},c) " in exI)
    57 apply simp
    58 apply (rule transition_is_ex)
    59 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
    60 done
    61 
    62 
    63 lemma implementation:
    64 "impl_ioa =<| spec_ioa"
    65 apply (unfold ioa_implements_def)
    66 apply (rule conjI)
    67 apply (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)
    69 apply (rule trace_inclusion_for_simulations)
    70 apply (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)
    72 apply (rule issimulation)
    73 done
    74 
    75 end