isabelle: src/HOL/UNITY/Traces.ML@1861a564d7e2 (annotated)

5111 8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	1	(* Title: HOL/UNITY/Traces
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	2	ID: $Id$
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	4	Copyright 1998 University of Cambridge
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	5
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	6	Definitions of
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	7	* traces: the possible execution traces
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	8	* reachable: the set of reachable states
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	9
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	10	*)
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 5069 diff changeset	11
5253 82a5ca6290aa New record type of programs paulson parents: 5240 diff changeset	12	Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}";
82a5ca6290aa New record type of programs paulson parents: 5240 diff changeset	13	by Safe_tac;
82a5ca6290aa New record type of programs paulson parents: 5240 diff changeset	14	by (etac traces.induct 2);
82a5ca6290aa New record type of programs paulson parents: 5240 diff changeset	15	be reachable.induct 1;
82a5ca6290aa New record type of programs paulson parents: 5240 diff changeset	16	by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
82a5ca6290aa New record type of programs paulson parents: 5240 diff changeset	17	qed "reachable_equiv_traces";
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	18
5313 1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union paulson parents: 5277 diff changeset	19	Goal "acts <= Acts prg ==> stable acts (reachable prg)";
5240 bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac paulson parents: 5232 diff changeset	20	by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac paulson parents: 5232 diff changeset	21	qed "stable_reachable";
bbcd79ef7cf2 Constant "invariant" and new constrains_tac, ensures_tac paulson parents: 5232 diff changeset	22

author	paulson
	Thu, 13 Aug 1998 18:06:40 +0200
changeset 5313	1861a564d7e2
parent 5277	e4297d03e5d2
child 5423	c57c87628bb4
permissions	-rw-r--r--