isabelle: src/HOL/IMP/Natural.ML@4966dae8fa62 (annotated)

1700 afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	1	(* Title: HOL/IMP/Natural.ML
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	2	ID: $Id$
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	3	Author: Tobias Nipkow & Larry Paulson, TUM
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	4	Copyright 1996 TUM
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	5	*)
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	6
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	7	open Natural;
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	8
1973 8c94c9a5be10 Converted proofs to use default clasets. nipkow parents: 1958 diff changeset	9	AddIs evalc.intrs;
8c94c9a5be10 Converted proofs to use default clasets. nipkow parents: 1958 diff changeset	10
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 5789 diff changeset	11	val evalc_elim_cases =
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 5789 diff changeset	12	map evalc.mk_cases
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 5789 diff changeset	13	["<SKIP,s> -c-> t",
9241 f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 6162 diff changeset	14	"<x:==a,s> -c-> t",
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 5789 diff changeset	15	"<c1;c2, s> -c-> t",
a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 5789 diff changeset	16	"<IF b THEN c1 ELSE c2, s> -c-> t"];
1700 afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	17
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 5789 diff changeset	18	val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
1700 afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	19
1973 8c94c9a5be10 Converted proofs to use default clasets. nipkow parents: 1958 diff changeset	20	AddSEs evalc_elim_cases;
1700 afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	21
afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	22	(* evaluation of com is deterministic *)
5117 7b5efef2ca74 Removed leading !! in goals. nipkow parents: 5069 diff changeset	23	Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
1730 1c7f793fc374 Updated for new form of induction rules paulson parents: 1700 diff changeset	24	by (etac evalc.induct 1);
1958 6f20ecbd87cb Now uses thin_tac paulson parents: 1730 diff changeset	25	by (thin_tac "<?c,s2> -c-> s1" 7);
9241 f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 6162 diff changeset	26	(blast_tac needs Unify.search_bound, trace_bound ::= 40)
4241 3f3f87c6fe3b Got rid of some slow deepen_tac calls paulson parents: 4089 diff changeset	27	by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
1700 afd3b60660db Natural and Transition semantics. nipkow parents: diff changeset	28	qed_spec_mp "com_det";

author	wenzelm
	Thu, 29 Nov 2001 01:51:06 +0100
changeset 12325	4966dae8fa62
parent 9556	dcdcfb0545e0
permissions	-rw-r--r--