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;
mueller@6008
     1
(*  Title:      HOL/IOA/example/Correctness.thy
wenzelm@12218
     2
    Author:     Olaf Müller
mueller@6008
     3
*)
mueller@6008
     4
wenzelm@17244
     5
header {* Correctness Proof *}
mueller@6008
     6
wenzelm@17244
     7
theory Correctness
wenzelm@17244
     8
imports SimCorrectness Spec Impl
wenzelm@17244
     9
begin
mueller@6008
    10
wenzelm@36452
    11
default_sort type
mueller@6008
    12
wenzelm@25131
    13
definition
wenzelm@25131
    14
  sim_relation :: "((nat * bool) * (nat set * bool)) set" where
wenzelm@25131
    15
  "sim_relation = {qua. let c = fst qua; a = snd qua ;
wenzelm@25131
    16
                            k = fst c;   b = snd c;
wenzelm@25131
    17
                            used = fst a; c = snd a
wenzelm@25131
    18
                        in
wenzelm@25131
    19
                        (! l:used. l < k) & b=c}"
mueller@6008
    20
wenzelm@19740
    21
declare split_paired_Ex [simp del]
wenzelm@19740
    22
wenzelm@19740
    23
wenzelm@19740
    24
(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive
wenzelm@19740
    25
         simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans
wenzelm@19740
    26
   Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired,
wenzelm@19740
    27
         as this can be done globally *)
wenzelm@19740
    28
wenzelm@19740
    29
lemma issimulation:
wenzelm@19740
    30
      "is_simulation sim_relation impl_ioa spec_ioa"
wenzelm@19740
    31
apply (simp (no_asm) add: is_simulation_def)
wenzelm@19740
    32
apply (rule conjI)
wenzelm@19740
    33
txt {* start states *}
haftmann@26359
    34
apply (auto)[1]
wenzelm@19740
    35
apply (rule_tac x = " ({},False) " in exI)
wenzelm@27361
    36
apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def)
wenzelm@19740
    37
txt {* main-part *}
wenzelm@19740
    38
apply (rule allI)+
wenzelm@19740
    39
apply (rule imp_conj_lemma)
wenzelm@19740
    40
apply (rename_tac k b used c k' b' a)
wenzelm@19740
    41
apply (induct_tac "a")
wenzelm@27361
    42
apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def)
haftmann@26359
    43
apply auto
wenzelm@19740
    44
txt {* NEW *}
wenzelm@19740
    45
apply (rule_tac x = "(used,True)" in exI)
wenzelm@19740
    46
apply simp
wenzelm@19740
    47
apply (rule transition_is_ex)
wenzelm@27361
    48
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
wenzelm@19740
    49
txt {* LOC *}
wenzelm@19740
    50
apply (rule_tac x = " (used Un {k},False) " in exI)
wenzelm@19740
    51
apply (simp add: less_SucI)
wenzelm@19740
    52
apply (rule transition_is_ex)
wenzelm@27361
    53
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
wenzelm@19740
    54
apply fast
wenzelm@19740
    55
txt {* FREE *}
wenzelm@19740
    56
apply (rule_tac x = " (used - {nat},c) " in exI)
wenzelm@19740
    57
apply simp
wenzelm@19740
    58
apply (rule transition_is_ex)
wenzelm@27361
    59
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
wenzelm@19740
    60
done
wenzelm@19740
    61
wenzelm@19740
    62
wenzelm@19740
    63
lemma implementation:
wenzelm@19740
    64
"impl_ioa =<| spec_ioa"
wenzelm@19740
    65
apply (unfold ioa_implements_def)
wenzelm@19740
    66
apply (rule conjI)
wenzelm@27361
    67
apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def
wenzelm@19740
    68
  asig_outputs_def asig_of_def asig_inputs_def)
wenzelm@19740
    69
apply (rule trace_inclusion_for_simulations)
wenzelm@27361
    70
apply (simp (no_asm) add: impl_sig_def spec_sig_def impl_ioa_def spec_ioa_def
wenzelm@19740
    71
  externals_def asig_outputs_def asig_of_def asig_inputs_def)
wenzelm@19740
    72
apply (rule issimulation)
wenzelm@19740
    73
done
wenzelm@17244
    74
wenzelm@17244
    75
end