Commit [8f950e] default Maximize Restore History

merged

nipkow nipkow 2010-04-20

1 2 > >> (Page 1 of 2)
added thys/Functional-Automata/Regular_Set.thy
removed thys/Functional-Automata/RegExp.thy
changed thys/Functional-Automata/RegSet_of_nat_DA.thy
changed thys/Functional-Automata/RegExp2NAe.thy
changed thys/Functional-Automata/AutoRegExp.thy
changed thys/Functional-Automata/RegExp2NA.thy
changed thys/Category/Functors.thy
changed thys/Category/NatTrans.thy
changed thys/Category/Cat.thy
changed thys/Category/Yoneda.thy
changed thys/Category/HomFunctors.thy
changed thys/Jinja/Compiler/Correctness2.thy
changed thys/Collections/Userguide.thy
changed thys/Collections/RBTMapImpl.thy
changed thys/Slicing/JinjaVM/JVMCFG.thy
changed thys/Presburger-Automata/Presburger_Automata.thy
changed thys/JinjaThreads/Common/Aux.thy
changed thys/BDD/LevellistProof.thy
changed thys/BDD/RepointProof.thy
changed thys/BDD/NormalizeTotalProof.thy
changed thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy
changed thys/LinearQuantifierElim/Thys/QEdlo.thy
changed thys/LinearQuantifierElim/Thys/DLO.thy
copied thys/Functional-Automata/RegSet.thy -> thys/Functional-Automata/Regular_Exp.thy
thys/Functional-Automata/Regular_Set.thy Diff Switch to side-by-side view
Loading...
thys/Functional-Automata/RegSet_of_nat_DA.thy Diff Switch to side-by-side view
Loading...
thys/Functional-Automata/RegExp2NAe.thy Diff Switch to side-by-side view
Loading...
thys/Functional-Automata/AutoRegExp.thy Diff Switch to side-by-side view
Loading...
thys/Functional-Automata/RegExp2NA.thy Diff Switch to side-by-side view
Loading...
thys/Category/Functors.thy Diff Switch to side-by-side view
Loading...
thys/Category/NatTrans.thy Diff Switch to side-by-side view
Loading...
thys/Category/Cat.thy Diff Switch to side-by-side view
Loading...
thys/Category/Yoneda.thy Diff Switch to side-by-side view
Loading...
thys/Category/HomFunctors.thy Diff Switch to side-by-side view
Loading...
thys/Jinja/Compiler/Correctness2.thy Diff Switch to side-by-side view
Loading...
thys/Collections/Userguide.thy Diff Switch to side-by-side view
Loading...
thys/Collections/RBTMapImpl.thy Diff Switch to side-by-side view
Loading...
thys/Slicing/JinjaVM/JVMCFG.thy Diff Switch to side-by-side view
Loading...
thys/Presburger-Automata/Presburger_Automata.thy Diff Switch to side-by-side view
Loading...
thys/JinjaThreads/Common/Aux.thy Diff Switch to side-by-side view
Loading...
thys/BDD/LevellistProof.thy Diff Switch to side-by-side view
Loading...
thys/BDD/RepointProof.thy Diff Switch to side-by-side view
Loading...
thys/BDD/NormalizeTotalProof.thy Diff Switch to side-by-side view
Loading...
thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy Diff Switch to side-by-side view
Loading...
thys/LinearQuantifierElim/Thys/QEdlo.thy Diff Switch to side-by-side view
Loading...
thys/LinearQuantifierElim/Thys/DLO.thy Diff Switch to side-by-side view
Loading...
thys/Functional-Automata/RegSet.thy to thys/Functional-Automata/Regular_Exp.thy
--- a/thys/Functional-Automata/RegSet.thy
+++ b/thys/Functional-Automata/Regular_Exp.thy
@@ -1,39 +1,28 @@
-(*  ID:         $Id: RegSet.thy,v 1.7 2007-07-22 20:44:19 makarius Exp $
+(*  ID:         $Id: RegExp.thy,v 1.5 2004-08-19 10:54:14 nipkow Exp $
     Author:     Tobias Nipkow
     Copyright   1998 TUM
 *)
 
-header "Regular sets"
+header "Regular expressions"
 
-theory RegSet
-imports Main
+theory Regular_Exp
+imports Regular_Set
 begin
 
-definition
- conc :: "'a list set => 'a list set => 'a list set" where
-"conc A B = {xs@ys | xs ys. xs:A & ys:B}"
+datatype 'a rexp =
+  Zero |
+  One |
+  Atom 'a |
+  Plus "('a rexp)" "('a rexp)" |
+  Times "('a rexp)" "('a rexp)" |
+  Star "('a rexp)"
 
-inductive_set
-  star :: "'a list set => 'a list set"
-  for A :: "'a list set"
-where
-  NilI[iff]:   "[] : star A"
-| ConsI[intro,simp]:  "[| a:A; as : star A |] ==> a@as : star A"
-
-lemma concat_in_star: "!xs: set xss. xs:S ==> concat xss : star S"
-by (induct xss) simp_all
-
-lemma in_star:
- "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))"
-apply (rule iffI)
- apply (erule star.induct)
-  apply (rule_tac x = "[]" in exI)
-  apply simp
- apply clarify
- apply (rule_tac x = "a#us" in exI)
- apply simp
-apply clarify
-apply (simp add: concat_in_star)
-done
+primrec lang :: "'a rexp => 'a list set" where
+"lang Zero = {}" |
+"lang One = {[]}" |
+"lang (Atom a) = {[a]}" |
+"lang (Plus el er) = (lang el) Un (lang er)" |
+"lang (Times el er) = conc (lang el) (lang er)" |
+"lang (Star e) = star(lang e)"
 
 end
1 2 > >> (Page 1 of 2)