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