Regexp relation definition

regexp.v

(* generated by Ott 0.26 from: regexp.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Ott.ott_list_core.


Import ListNotations.

Section RegExp.

Variable char : Type.

Definition c := char. (*r character *)

Inductive re : Type :=  (*r regexp *)
 | re_zero : re
 | re_unit : re
 | re_char (c5:c)
 | re_plus (r:re) (r':re)
 | re_times (r:re) (r':re)
 | re_star (r:re).

Definition s : Type := list char.
(** definitions *)

(* defns regexp_ins *)
Inductive s_in_regexp_lang : s -> re -> Prop :=    (* defn s_in_regexp_lang *)
 | s_in_regexp_lang_unit : 
     s_in_regexp_lang  []  re_unit
 | s_in_regexp_lang_char : forall (c5:c),
     s_in_regexp_lang  ( c5  :: [])  (re_char c5)
 | s_in_regexp_lang_plus_1 : forall (s5:s) (r1 r2:re),
     s_in_regexp_lang s5 r1 ->
     s_in_regexp_lang s5 (re_plus r1 r2)
 | s_in_regexp_lang_plus_2 : forall (s5:s) (r1 r2:re),
     s_in_regexp_lang s5 r2 ->
     s_in_regexp_lang s5 (re_plus r1 r2)
 | s_in_regexp_lang_times : forall (s5 s':s) (r1 r2:re),
     s_in_regexp_lang s5 r1 ->
     s_in_regexp_lang s' r2 ->
     s_in_regexp_lang  ( s5  ++  s' )  (re_times r1 r2)
 | s_in_regexp_lang_star_1 : forall (r:re),
     s_in_regexp_lang  []  (re_star r)
 | s_in_regexp_lang_star_2 : forall (s5 s':s) (r:re),
     s_in_regexp_lang s5 r ->
     s_in_regexp_lang s' (re_star r) ->
     s_in_regexp_lang  ( s5  ++  s' )  (re_star r).
(** definitions *)

(* defns regexp_ins_c *)
Inductive s_in_regexp_c_lang : s -> re -> c -> Prop :=    (* defn s_in_regexp_c_lang *)
 | s_in_regexp_c_lang_cs : forall (s5:s) (r:re) (c5:c),
     s_in_regexp_lang  (  ( c5  :: [])   ++  s5 )  r ->
          s_in_regexp_c_lang s5 r c5.

End RegExp.

Arguments re_zero [char].
Arguments re_unit [char].
Arguments re_char [char] _.
Arguments re_plus [char] _ _.
Arguments re_times [char] _ _.
Arguments re_star [char] _.