# HG changeset patch
# User nipkow
# Date 894538943 -7200
# Node ID a4301a63bf5c788b5c2f1f62cbd174f0208fb827
# Parent  447d6b2956ba1332700f9cbf63c592030571bf0a
Got rid of NAe.delta

diff -r 447d6b2956ba -r a4301a63bf5c src/HOL/Lex/Automata.ML
--- a/src/HOL/Lex/Automata.ML	Wed May 06 13:01:45 1998 +0200
+++ b/src/HOL/Lex/Automata.ML	Thu May 07 13:02:23 1998 +0200
@@ -22,12 +22,12 @@
 (*** Direct equivalence of NAe and DA ***)
 
 goalw thy [nae2da_def]
- "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = lift(NAe.delta A w) Q";
+ "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
 by(induct_tac "w" 1);
- by(ALLGOALS Asm_simp_tac);
- by(Blast_tac 1);
+ by (Simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
 by(Blast_tac 1);
-qed_spec_mp "espclosure_DA_delta_is_lift_NAe_delta";
+qed_spec_mp "espclosure_DA_delta_is_steps";
 
 goalw thy [nae2da_def]
  "fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
@@ -36,8 +36,7 @@
 
 goalw thy [NAe.accepts_def,DA.accepts_def]
   "NAe.accepts A w = DA.accepts (nae2da A) w";
-by(simp_tac (simpset() addsimps [lemma,steps_equiv_delta,
-     espclosure_DA_delta_is_lift_NAe_delta]) 1);
+by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
 by(simp_tac (simpset() addsimps [nae2da_def]) 1);
 by(Blast_tac 1);
 qed "NAe_DA_equiv";
diff -r 447d6b2956ba -r a4301a63bf5c src/HOL/Lex/NAe.ML
--- a/src/HOL/Lex/NAe.ML	Wed May 06 13:01:45 1998 +0200
+++ b/src/HOL/Lex/NAe.ML	Thu May 07 13:02:23 1998 +0200
@@ -42,7 +42,7 @@
 qed "in_steps_append";
 AddIffs [in_steps_append];
 
-(** Equivalence of steps and delta **)
+(* Equivalence of steps and delta
 (* Use "(? x : f `` A. P x) = (? a:A. P(f x))" ?? *)
 goal thy "!p. (p,q) : steps A w = (q : delta A w p)";
 by (induct_tac "w" 1);
@@ -50,3 +50,4 @@
 by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
 by(Blast_tac 1);
 qed_spec_mp "steps_equiv_delta";
+*)
diff -r 447d6b2956ba -r a4301a63bf5c src/HOL/Lex/NAe.thy
--- a/src/HOL/Lex/NAe.thy	Wed May 06 13:01:45 1998 +0200
+++ b/src/HOL/Lex/NAe.thy	Thu May 07 13:02:23 1998 +0200
@@ -22,13 +22,14 @@
 "steps A [] = (eps A)^*"
 "steps A (a#w) = steps A w  O  step A (Some a)  O  (eps A)^*"
 
+constdefs
+ accepts :: ('a,'s)nae => 'a list => bool
+"accepts A w == ? q. (start A,q) : steps A w & fin A q"
+
+(* not really used:
 consts delta :: "('a,'s)nae => 'a list => 's => 's set"
 primrec delta list
 "delta A [] s = (eps A)^* ^^ {s}"
 "delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
-
-constdefs
- accepts :: ('a,'s)nae => 'a list => bool
-"accepts A w == ? q. (start A,q) : steps A w & fin A q"
-
+*)
 end