isabelle: src/HOL/TLA/Buffer/Buffer.ML@600f1c93124f (annotated)

3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	1	(*
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	2	File: Buffer.ML
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	3	Author: Stephan Merz
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4	Copyright: 1997 University of Munich
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	5
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6	Simple FIFO buffer (theorems and proofs)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7	*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	8
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9	(* ---------------------------- Data lemmas ---------------------------- *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5525 diff changeset	11	context List.thy;
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	12	goal List.thy "xs ~= [] --> tl xs ~= xs";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3861 diff changeset	13	by (auto_tac (claset(), simpset() addsimps [neq_Nil_conv]));
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	14	qed_spec_mp "tl_not_self";
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5525 diff changeset	15	context Buffer.thy;
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	16
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5525 diff changeset	17	Addsimps [tl_not_self];
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	18
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	19	(* ---------------------------- Action lemmas ---------------------------- *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	20
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21	(* Dequeue is visible *)
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5525 diff changeset	22	Goal "\|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3861 diff changeset	23	by (auto_tac (claset(), simpset() addsimps [angle_def,Deq_def]));
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	24	qed "Deq_visible";
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26	(* Enabling condition for dequeue -- NOT NEEDED *)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4089 diff changeset	27	Goalw [temp_rewrite Deq_visible]
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5525 diff changeset	28	"!!q. basevars (ic,q,oc) ==> \|- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])";
9517 f58863b1406a tuned version by Stephan Merz (unbatchified etc.); wenzelm parents: 6255 diff changeset	29	by (force_tac (claset() addSEs [base_enabled,enabledE],
f58863b1406a tuned version by Stephan Merz (unbatchified etc.); wenzelm parents: 6255 diff changeset	30	simpset() addsimps [Deq_def]) 1);
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	31	qed "Deq_enabled";
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	32
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	33	(* For the left-to-right implication, we don't need the base variable stuff *)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4089 diff changeset	34	Goalw [temp_rewrite Deq_visible]
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 5525 diff changeset	35	"\|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q ~= #[])";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3861 diff changeset	36	by (auto_tac (claset() addSEs [enabledE], simpset() addsimps [Deq_def]));
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	37	qed "Deq_enabledE";

author	wenzelm
	Wed, 07 Aug 2002 20:05:43 +0200
changeset 13476	600f1c93124f
parent 9517	f58863b1406a
child 13601	fd3e3d6b37b2
permissions	-rw-r--r--