src/HOL/Lex/NAe.ML

Goal: tuned pris;

(*  Title:      HOL/Lex/NAe.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1998 TUM
*)

Goal "steps A w O (eps A)^* = steps A w";
by (exhaust_tac "w" 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
qed_spec_mp "steps_epsclosure";
Addsimps [steps_epsclosure];

Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
by (rtac (steps_epsclosure RS equalityE) 1);
by (Blast_tac 1);
qed "in_steps_epsclosure";

Goal "(eps A)^* O steps A w = steps A w";
by (induct_tac "w" 1);
 by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [O_assoc RS sym]) 1);
qed "epsclosure_steps";

Goal "[| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
by (rtac (epsclosure_steps RS equalityE) 1);
by (Blast_tac 1);
qed "in_epsclosure_steps";

Goal "steps A (v@w) = steps A w  O  steps A v";
by (induct_tac "v" 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
qed "steps_append";
Addsimps [steps_append];

Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
by (rtac (steps_append RS equalityE) 1);
by (Blast_tac 1);
qed "in_steps_append";
AddIffs [in_steps_append];

(* Equivalence of steps and delta
(* Use "(? x : f `` A. P x) = (? a:A. P(f x))" ?? *)
Goal "!p. (p,q) : steps A w = (q : delta A w p)";
by (induct_tac "w" 1);
 by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
by (Blast_tac 1);
qed_spec_mp "steps_equiv_delta";
*)