wneuper/isa: src/HOL/IMPP/Natural.thy@a6dc1769fdda (annotated)

oheimb@8177	1	(* Title: HOL/IMPP/Natural.thy
oheimb@8177	2	ID: $Id$
oheimb@8177	3	Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
oheimb@8177	4	Copyright 1999 TUM
oheimb@8177	5	*)
oheimb@8177	6
wenzelm@17477	7	header {* Natural semantics of commands *}
wenzelm@17477	8
wenzelm@17477	9	theory Natural
wenzelm@17477	10	imports Com
wenzelm@17477	11	begin
oheimb@8177	12
oheimb@8177	13	( Execution of commands )
oheimb@8177	14
oheimb@8177	15	consts
oheimb@8177	16	newlocs :: locals
wenzelm@17477	17	setlocs :: "state => locals => state"
wenzelm@17477	18	getlocs :: "state => locals"
wenzelm@17477	19	update :: "state => vname => val => state" ("_/[_/::=/_]" [900,0,0] 900)
wenzelm@27362	20
wenzelm@27362	21	abbreviation
wenzelm@27362	22	loc :: "state => locals" ("_<_>" [75,0] 75) where
wenzelm@27362	23	"s<X> == getlocs s X"
oheimb@8177	24
berghofe@23746	25	inductive
berghofe@23746	26	evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51)
berghofe@23746	27	where
wenzelm@17477	28	Skip: "<SKIP,s> -c-> s"
oheimb@8177	29
berghofe@23746	30	\| Assign: "<X :== a,s> -c-> s[X::=a s]"
oheimb@8177	31
berghofe@23746	32	\| Local: "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
wenzelm@17477	33	<LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
oheimb@8177	34
berghofe@23746	35	\| Semi: "[\| <c0,s0> -c-> s1; <c1,s1> -c-> s2 \|] ==>
wenzelm@17477	36	<c0;; c1, s0> -c-> s2"
oheimb@8177	37
berghofe@23746	38	\| IfTrue: "[\| b s; <c0,s> -c-> s1 \|] ==>
wenzelm@17477	39	<IF b THEN c0 ELSE c1, s> -c-> s1"
oheimb@8177	40
berghofe@23746	41	\| IfFalse: "[\| ~b s; <c1,s> -c-> s1 \|] ==>
wenzelm@17477	42	<IF b THEN c0 ELSE c1, s> -c-> s1"
oheimb@8177	43
berghofe@23746	44	\| WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
oheimb@8177	45
berghofe@23746	46	\| WhileTrue: "[\| b s0; <c,s0> -c-> s1; <WHILE b DO c, s1> -c-> s2 \|] ==>
wenzelm@17477	47	<WHILE b DO c, s0> -c-> s2"
oheimb@8177	48
berghofe@23746	49	\| Body: "<the (body pn), s0> -c-> s1 ==>
wenzelm@17477	50	<BODY pn, s0> -c-> s1"
oheimb@8177	51
berghofe@23746	52	\| Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
wenzelm@17477	53	<X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
wenzelm@17477	54	[X::=s1<Res>]"
oheimb@8177	55
berghofe@23746	56	inductive
berghofe@23746	57	evaln :: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51)
berghofe@23746	58	where
wenzelm@17477	59	Skip: "<SKIP,s> -n-> s"
oheimb@8177	60
berghofe@23746	61	\| Assign: "<X :== a,s> -n-> s[X::=a s]"
oheimb@8177	62
berghofe@23746	63	\| Local: "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
wenzelm@17477	64	<LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
oheimb@8177	65
berghofe@23746	66	\| Semi: "[\| <c0,s0> -n-> s1; <c1,s1> -n-> s2 \|] ==>
wenzelm@17477	67	<c0;; c1, s0> -n-> s2"
oheimb@8177	68
berghofe@23746	69	\| IfTrue: "[\| b s; <c0,s> -n-> s1 \|] ==>
wenzelm@17477	70	<IF b THEN c0 ELSE c1, s> -n-> s1"
oheimb@8177	71
berghofe@23746	72	\| IfFalse: "[\| ~b s; <c1,s> -n-> s1 \|] ==>
wenzelm@17477	73	<IF b THEN c0 ELSE c1, s> -n-> s1"
oheimb@8177	74
berghofe@23746	75	\| WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
oheimb@8177	76
berghofe@23746	77	\| WhileTrue: "[\| b s0; <c,s0> -n-> s1; <WHILE b DO c, s1> -n-> s2 \|] ==>
wenzelm@17477	78	<WHILE b DO c, s0> -n-> s2"
oheimb@8177	79
berghofe@23746	80	\| Body: "<the (body pn), s0> - n-> s1 ==>
wenzelm@17477	81	<BODY pn, s0> -Suc n-> s1"
oheimb@8177	82
berghofe@23746	83	\| Call: "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
wenzelm@17477	84	<X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
wenzelm@17477	85	[X::=s1<Res>]"
wenzelm@17477	86
wenzelm@17477	87
wenzelm@17477	88	inductive_cases evalc_elim_cases:
wenzelm@17477	89	"<SKIP,s> -c-> t" "<X:==a,s> -c-> t" "<LOCAL Y:=a IN c,s> -c-> t"
wenzelm@17477	90	"<c1;;c2,s> -c-> t" "<IF b THEN c1 ELSE c2,s> -c-> t"
wenzelm@17477	91	"<BODY P,s> -c-> s1" "<X:=CALL P(a),s> -c-> s1"
wenzelm@17477	92
wenzelm@17477	93	inductive_cases evaln_elim_cases:
wenzelm@17477	94	"<SKIP,s> -n-> t" "<X:==a,s> -n-> t" "<LOCAL Y:=a IN c,s> -n-> t"
wenzelm@17477	95	"<c1;;c2,s> -n-> t" "<IF b THEN c1 ELSE c2,s> -n-> t"
wenzelm@17477	96	"<BODY P,s> -n-> s1" "<X:=CALL P(a),s> -n-> s1"
wenzelm@17477	97
wenzelm@17477	98	inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
wenzelm@17477	99	inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
wenzelm@17477	100
wenzelm@19803	101	declare evalc.intros [intro]
wenzelm@19803	102	declare evaln.intros [intro]
wenzelm@19803	103
wenzelm@19803	104	declare evalc_elim_cases [elim!]
wenzelm@19803	105	declare evaln_elim_cases [elim!]
wenzelm@19803	106
wenzelm@19803	107	(* evaluation of com is deterministic *)
wenzelm@19803	108	lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
wenzelm@19803	109	apply (erule evalc.induct)
wenzelm@19803	110	apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
wenzelm@24178	111	(blast needs unify_search_bound = 40)
wenzelm@19803	112	apply (best elim: evalc_WHILE_case)+
wenzelm@19803	113	done
wenzelm@19803	114
wenzelm@19803	115	lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
wenzelm@19803	116	apply (erule evaln.induct)
wenzelm@19803	117	apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *})
wenzelm@19803	118	done
wenzelm@19803	119
wenzelm@19803	120	lemma Suc_le_D_lemma: "[\| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) \|] ==> P m'"
wenzelm@19803	121	apply (frule Suc_le_D)
wenzelm@19803	122	apply blast
wenzelm@19803	123	done
wenzelm@19803	124
wenzelm@19803	125	lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
wenzelm@19803	126	apply (erule evaln.induct)
wenzelm@19803	127	apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *})
wenzelm@19803	128	apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
wenzelm@19803	129	done
wenzelm@19803	130
wenzelm@19803	131	lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
wenzelm@19803	132	apply (erule evaln_nonstrict)
wenzelm@19803	133	apply auto
wenzelm@19803	134	done
wenzelm@19803	135
wenzelm@19803	136	lemma evaln_max2: "[\| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 \|] ==>
wenzelm@19803	137	? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2"
wenzelm@19803	138	apply (cut_tac m = "n1" and n = "n2" in nat_le_linear)
wenzelm@19803	139	apply (blast dest: evaln_nonstrict)
wenzelm@19803	140	done
wenzelm@19803	141
wenzelm@19803	142	lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
wenzelm@19803	143	apply (erule evalc.induct)
wenzelm@19803	144	apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
wenzelm@19803	145	apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *})
wenzelm@19803	146	apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
wenzelm@19803	147	done
wenzelm@19803	148
wenzelm@19803	149	lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
wenzelm@19803	150	apply (fast elim: evalc_evaln evaln_evalc)
wenzelm@19803	151	done
wenzelm@17477	152
oheimb@8177	153	end

author	wenzelm
	Wed, 25 Jun 2008 22:01:34 +0200
changeset 27362	a6dc1769fdda
parent 24178	4ff1dc2aa18d
child 39406	0dec18004e75
permissions	-rw-r--r--