isabelle: src/HOL/Lex/NAe.ML@c63612ffb186 (annotated)

4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	1	(* Title: HOL/Lex/NAe.ML
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	2	ID: $Id$
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	3	Author: Tobias Nipkow
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	4	Copyright 1998 TUM
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	5	*)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	6
5118 6b995dad8a9d Removed leading !! in goals. nipkow parents: 5069 diff changeset	7	Goal "steps A w O (eps A)^* = steps A w";
8442 96023903c2df case_tac now subsumes both boolean and datatype cases; wenzelm parents: 8423 diff changeset	8	by (case_tac "w" 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	9	by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	10	qed_spec_mp "steps_epsclosure";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	11	Addsimps [steps_epsclosure];
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	12
5118 6b995dad8a9d Removed leading !! in goals. nipkow parents: 5069 diff changeset	13	Goal "[\| (p,q) : (eps A)^*; (q,r) : steps A w \|] ==> (p,r) : steps A w";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	14	by (rtac (steps_epsclosure RS equalityE) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	15	by (Blast_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	16	qed "in_steps_epsclosure";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	17
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4900 diff changeset	18	Goal "(eps A)^* O steps A w = steps A w";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	19	by (induct_tac "w" 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	20	by (Simp_tac 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	21	by (asm_simp_tac (simpset() addsimps [O_assoc RS sym]) 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	22	qed "epsclosure_steps";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	23
5118 6b995dad8a9d Removed leading !! in goals. nipkow parents: 5069 diff changeset	24	Goal "[\| (p,q) : steps A w; (q,r) : (eps A)^* \|] ==> (p,r) : steps A w";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	25	by (rtac (epsclosure_steps RS equalityE) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	26	by (Blast_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	27	qed "in_epsclosure_steps";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	28
5118 6b995dad8a9d Removed leading !! in goals. nipkow parents: 5069 diff changeset	29	Goal "steps A (v@w) = steps A w O steps A v";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	30	by (induct_tac "v" 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	31	by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	32	qed "steps_append";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	33	Addsimps [steps_append];
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	34
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4900 diff changeset	35	Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	36	by (rtac (steps_append RS equalityE) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	37	by (Blast_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	38	qed "in_steps_append";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	39	AddIffs [in_steps_append];
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	40
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	41	(* Equivalence of steps and delta
10834 a7897aebbffc * empty log message * nipkow parents: 8442 diff changeset	42	(* Use "(? x : f ` A. P x) = (? a:A. P(f x))" ?? *)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4900 diff changeset	43	Goal "!p. (p,q) : steps A w = (q : delta A w p)";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	44	by (induct_tac "w" 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	45	by (Simp_tac 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	46	by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5118 diff changeset	47	by (Blast_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	48	qed_spec_mp "steps_equiv_delta";
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	49	*)

author	wenzelm
	Wed, 08 May 2002 12:15:30 +0200
changeset 13122	c63612ffb186
parent 10834	a7897aebbffc
permissions	-rw-r--r--