isabelle: src/HOL/HOLCF/IOA/Storage/Correctness.thy@16375b493b64 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40945 diff changeset	1	(* Title: HOL/HOLCF/IOA/Storage/Correctness.thy
40945 b8703f63bfb2 recoded latin1 as utf8; wenzelm parents: 40774 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

author	hoelzl
	Tue, 17 May 2011 11:47:36 +0200
changeset 42861	16375b493b64
parent 42151	4da4fc77664b
child 58270	16648edf16e3
permissions	-rw-r--r--