regexp: Regular_Exp.thy@70395e3fd99f (annotated)

170 b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	1	(* Author: Tobias Nipkow
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	2	Copyright 1998 TUM
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	3	*)
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	4
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	5	header "Regular expressions"
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	6
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	7	theory Regular_Exp
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	8	imports Regular_Set
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	9	begin
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	10
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	11	datatype 'a rexp =
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	12	Zero \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	13	One \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	14	Atom 'a \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	15	Plus "('a rexp)" "('a rexp)" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	16	Times "('a rexp)" "('a rexp)" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	17	Star "('a rexp)"
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	18
203 5d724fe0e096 changes according to afp-submission urbanc parents: 170 diff changeset	19	primrec lang :: "'a rexp => 'a lang" where
170 b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	20	"lang Zero = {}" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	21	"lang One = {[]}" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	22	"lang (Atom a) = {[a]}" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	23	"lang (Plus r s) = (lang r) Un (lang s)" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	24	"lang (Times r s) = conc (lang r) (lang s)" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	25	"lang (Star r) = star(lang r)"
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	26
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	27	primrec atoms :: "'a rexp \<Rightarrow> 'a set"
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	28	where
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	29	"atoms Zero = {}" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	30	"atoms One = {}" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	31	"atoms (Atom a) = {a}" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	32	"atoms (Plus r s) = atoms r \<union> atoms s" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	33	"atoms (Times r s) = atoms r \<union> atoms s" \|
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	34	"atoms (Star r) = atoms r"
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	35
b1258b7d2789 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic urbanc parents: diff changeset	36	end

author	urbanc
	Mon, 30 Jan 2012 08:55:27 +0000
changeset 269	70395e3fd99f
parent 203	5d724fe0e096
child 379	8c4b6fb43ebe
permissions	-rw-r--r--