isabelle: src/HOL/HOLCF/IOA/NTP/Correctness.thy@99a720d3ed8f (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/IOA/NTP/Correctness.thy
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	5	section \<open>The main correctness proof: Impl implements Spec\<close>
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
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 Impl Spec
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
25131 2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19739 diff changeset	11	definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19739 diff changeset	12	hom :: "'m impl_state => 'm list" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19739 diff changeset	13	"hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation'); wenzelm parents: 19739 diff changeset	14	else tl(sq(sen s)))"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	16	setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	17
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	18	lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	19	and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	20
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	21	declare split_paired_All [simp del]
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	22
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	23
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	24	text \<open>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	25	A lemma about restricting the action signature of the implementation
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	26	to that of the specification.
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	27	\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	28
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	29	lemma externals_lemma:
67613 ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	30	"a\<in>externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) =
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	31	(case a of
67613 ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	32	S_msg(m) \<Rightarrow> True
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	33	\| R_msg(m) \<Rightarrow> True
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	34	\| S_pkt(pkt) \<Rightarrow> False
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	35	\| R_pkt(pkt) \<Rightarrow> False
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	36	\| S_ack(b) \<Rightarrow> False
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	37	\| R_ack(b) \<Rightarrow> False
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	38	\| C_m_s \<Rightarrow> False
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	39	\| C_m_r \<Rightarrow> False
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	40	\| C_r_s \<Rightarrow> False
ce654b0e6d69 more symbols; wenzelm parents: 62390 diff changeset	41	\| C_r_r(m) \<Rightarrow> False)"
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	42	apply (simp (no_asm) add: externals_def restrict_def restrict_asig_def Spec.sig_def asig_projections)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	43
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	44	apply (induct_tac "a")
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	45	apply (simp_all (no_asm) add: actions_def asig_projections)
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	46	txt \<open>2\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	47	apply (simp (no_asm) add: impl_ioas)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	48	apply (simp (no_asm) add: impl_asigs)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	49	apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
35215 a03462cbf86f get rid of warnings about duplicate simp rules in all HOLCF theories huffman parents: 35174 diff changeset	50	apply (simp (no_asm) add: "transitions"(1) unfold_renaming)
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	51	txt \<open>1\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	52	apply (simp (no_asm) add: impl_ioas)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	53	apply (simp (no_asm) add: impl_asigs)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	54	apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	55	done
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	56
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	57	lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	58
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	59
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	60	text \<open>Proof of correctness\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	61	lemma ntp_correct:
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	62	"is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	63	apply (unfold Spec.ioa_def is_weak_ref_map_def)
62390 842917225d56 more canonical names nipkow parents: 62002 diff changeset	64	apply (simp (no_asm) cong del: if_weak_cong split del: if_split add: Correctness.hom_def
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	65	cancel_restrict externals_lemma)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	66	apply (rule conjI)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	67	apply (simp (no_asm) add: hom_ioas)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	68	apply (simp (no_asm_simp) add: sels)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	69	apply (rule allI)+
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	70	apply (rule imp_conj_lemma)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	71
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	72	apply (induct_tac "a")
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	73	apply (simp_all (no_asm_simp) add: hom_ioas)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	74	apply (frule inv4)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	75	apply force
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	76
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	77	apply (frule inv4)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	78	apply (frule inv2)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	79	apply (erule disjE)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	80	apply (simp (no_asm_simp))
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	81	apply force
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	82
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	83	apply (frule inv2)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	84	apply (erule disjE)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	85
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	86	apply (frule inv3)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	87	apply (case_tac "sq (sen (s))=[]")
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	88
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	89	apply (simp add: hom_ioas)
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	90	apply (blast dest!: add_leD1 [THEN leD])
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	91
58270 16648edf16e3 more porting to new datatypes blanchet parents: 51703 diff changeset	92	apply (rename_tac m, case_tac "m = hd (sq (sen (s)))")
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	93
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	94	apply force
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	95
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	96	apply simp
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	97	apply (blast dest!: add_leD1 [THEN leD])
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	98
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	99	apply simp
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	100	done
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	101
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	102	end

author	haftmann
	Thu, 24 Jul 2025 17:46:29 +0200
changeset 82902	99a720d3ed8f
parent 67613	ce654b0e6d69
permissions	-rw-r--r--