src/HOL/Lex/RegExp2NA.ML

Refined arithmetic.

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

(******************************************************)
(*                       atom                         *)
(******************************************************)

Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
by(Simp_tac 1);
qed "fin_atom";

Goalw [atom_def] "start (atom a) = [True]";
by(Simp_tac 1);
qed "start_atom";

Goalw [atom_def,step_def]
 "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
by(Simp_tac 1);
qed "in_step_atom_Some";
Addsimps [in_step_atom_Some];

Goal
 "([False],[False]) : steps (atom a) w = (w = [])";
by (induct_tac "w" 1);
 by(Simp_tac 1);
by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
qed "False_False_in_steps_atom";

Goal
 "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
by (induct_tac "w" 1);
 by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
by(asm_full_simp_tac (simpset()
     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
qed "start_fin_in_steps_atom";

Goal
 "accepts (atom a) w = (w = [a])";
by(simp_tac(simpset() addsimps
       [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
qed "accepts_atom";


(******************************************************)
(*                      union                         *)
(******************************************************)

(***** True/False ueber fin anheben *****)

Goalw [union_def] 
 "!L R. fin (union L R) (True#p) = fin L p";
by (Simp_tac 1);
qed_spec_mp "fin_union_True";

Goalw [union_def] 
 "!L R. fin (union L R) (False#p) = fin R p";
by (Simp_tac 1);
qed_spec_mp "fin_union_False";

AddIffs [fin_union_True,fin_union_False];

(***** True/False ueber step anheben *****)

Goalw [union_def,step_def]
"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
by (Simp_tac 1);
by(Blast_tac 1);
qed_spec_mp "True_in_step_union";

Goalw [union_def,step_def]
"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
by (Simp_tac 1);
by(Blast_tac 1);
qed_spec_mp "False_in_step_union";

AddIffs [True_in_step_union,False_in_step_union];


(***** True/False ueber steps anheben *****)

Goal
 "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
by (induct_tac "w" 1);
by (ALLGOALS Force_tac);
qed_spec_mp "lift_True_over_steps_union";

Goal 
 "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
by (induct_tac "w" 1);
by (ALLGOALS Force_tac);
qed_spec_mp "lift_False_over_steps_union";

AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];


(** From the start  **)

Goalw [union_def,step_def]
 "!L R. (start(union L R),q) : step(union L R) a = \
\       (? p. (q = True#p & (start L,p) : step L a) | \
\             (q = False#p & (start R,p) : step R a))";
by(Simp_tac 1);
by(Blast_tac 1);
qed_spec_mp "start_step_union";
AddIffs [start_step_union];

Goal
 "(start(union L R), q) : steps (union L R) w = \
\ ( (w = [] & q = start(union L R)) | \
\   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
\                     q = False # p & (start R,p) : steps R w)))";
by(exhaust_tac "w" 1);
 by (Asm_simp_tac 1);
 by(Blast_tac 1);
by (Asm_simp_tac 1);
by(Blast_tac 1);
qed "steps_union";

Goalw [union_def]
 "!L R. fin (union L R) (start(union L R)) = \
\       (fin L (start L) | fin R (start R))";
by(Simp_tac 1);
qed_spec_mp "fin_start_union";
AddIffs [fin_start_union];

Goal
 "accepts (union L R) w = (accepts L w | accepts R w)";
by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
(* get rid of case_tac: *)
by(case_tac "w = []" 1);
by(Auto_tac);
qed "accepts_union";
AddIffs [accepts_union];

(******************************************************)
(*                      conc                        *)
(******************************************************)

(** True/False in fin **)

Goalw [conc_def]
 "!L R. fin (conc L R) (True#p) = (fin L p & fin R (start R))";
by (Simp_tac 1);
qed_spec_mp "fin_conc_True";

Goalw [conc_def] 
 "!L R. fin (conc L R) (False#p) = fin R p";
by (Simp_tac 1);
qed "fin_conc_False";

AddIffs [fin_conc_True,fin_conc_False];

(** True/False in step **)

Goalw [conc_def,step_def]
 "!L R. (True#p,q) : step (conc L R) a = \
\       ((? r. q=True#r & (p,r): step L a) | \
\        (fin L p & (? r. q=False#r & (start R,r) : step R a)))";
by (Simp_tac 1);
by(Blast_tac 1);
qed_spec_mp "True_step_conc";

Goalw [conc_def,step_def]
 "!L R. (False#p,q) : step (conc L R) a = \
\       (? r. q = False#r & (p,r) : step R a)";
by (Simp_tac 1);
by(Blast_tac 1);
qed_spec_mp "False_step_conc";

AddIffs [True_step_conc, False_step_conc];

(** False in steps **)

Goal
 "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
by (induct_tac "w" 1);
by (ALLGOALS Force_tac);
qed_spec_mp "False_steps_conc";
AddIffs [False_steps_conc];

(** True in steps **)

Goal
 "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
by(induct_tac "w" 1);
 by (Simp_tac 1);
by (Simp_tac 1);
by(Blast_tac 1);
qed_spec_mp "True_True_steps_concI";

Goal
 "!L R. (True#p,False#q) : step (conc L R) a = \
\       (fin L p & (start R,q) : step R a)";
by(Simp_tac 1);
qed "True_False_step_conc";
AddIffs [True_False_step_conc];

Goal
 "!p. (True#p,q) : steps (conc L R) w --> \
\     ((? r. (p,r) : steps L w & q = True#r)  | \
\  (? u a v. w = u@a#v & \
\            (? r. (p,r) : steps L u & fin L r & \
\            (? s. (start R,s) : step R a & \
\            (? t. (s,t) : steps R v & q = False#t)))))";
by(induct_tac "w" 1);
 by(Simp_tac 1);
by(Simp_tac 1);
by(clarify_tac (claset() delrules [disjCI]) 1);
be disjE 1;
 by(clarify_tac (claset() delrules [disjCI]) 1);
 by(etac allE 1 THEN mp_tac 1);
 be disjE 1;
  by (Blast_tac 1);
 br disjI2 1;
 by (Clarify_tac 1);
 by(Simp_tac 1);
 by(res_inst_tac[("x","a#u")] exI 1);
 by(Simp_tac 1);
 by (Blast_tac 1);
br disjI2 1;
by (Clarify_tac 1);
by(Simp_tac 1);
by(res_inst_tac[("x","[]")] exI 1);
by(Simp_tac 1);
by (Blast_tac 1);
qed_spec_mp "True_steps_concD";

Goal
 "(True#p,q) : steps (conc L R) w = \
\ ((? r. (p,r) : steps L w & q = True#r)  | \
\  (? u a v. w = u@a#v & \
\            (? r. (p,r) : steps L u & fin L r & \
\            (? s. (start R,s) : step R a & \
\            (? t. (s,t) : steps R v & q = False#t)))))";
by(force_tac (claset() addDs [True_steps_concD]
     addIs [True_True_steps_concI],simpset()) 1);
qed "True_steps_conc";

(** starting from the start **)

Goalw [conc_def]
  "!L R. start(conc L R) = True#start L";
by(Simp_tac 1);
qed_spec_mp "start_conc";

Goalw [conc_def]
 "!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | \
\                          (? s. p = False#s & fin R s))";
by (simp_tac (simpset() addsplits [list.split]) 1);
by (Blast_tac 1);
qed_spec_mp "final_conc";

Goal
 "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
by (simp_tac (simpset() addsimps
     [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
br iffI 1;
 by (Clarify_tac 1);
 be disjE 1;
  by (Clarify_tac 1);
  be disjE 1;
   by(res_inst_tac [("x","w")] exI 1);
   by(Simp_tac 1);
   by(Blast_tac 1);
  by(Blast_tac 1);
 be disjE 1;
  by(Blast_tac 1);
 by (Clarify_tac 1);
 by(res_inst_tac [("x","u")] exI 1);
 by(Simp_tac 1);
 by(Blast_tac 1);
by (Clarify_tac 1);
by(exhaust_tac "v" 1);
 by(Asm_full_simp_tac 1);
 by(Blast_tac 1);
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
qed "accepts_conc";

(******************************************************)
(*                     epsilon                        *)
(******************************************************)

Goalw [epsilon_def,step_def] "step epsilon a = {}";
by(Simp_tac 1);
by(Blast_tac 1);
qed "step_epsilon";
Addsimps [step_epsilon];

Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
by(induct_tac "w" 1);
by(Auto_tac);
qed "steps_epsilon";

Goal "accepts epsilon w = (w = [])";
by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
by(simp_tac (simpset() addsimps [epsilon_def]) 1);
qed "accepts_epsilon";
AddIffs [accepts_epsilon];

(******************************************************)
(*                       plus                         *)
(******************************************************)

Goalw [plus_def] "!A. start (plus A) = start A";
by(Simp_tac 1);
qed_spec_mp "start_plus";
Addsimps [start_plus];

Goalw [plus_def] "!A. fin (plus A) = fin A";
by(Simp_tac 1);
qed_spec_mp "fin_plus";
AddIffs [fin_plus];

Goalw [plus_def,step_def]
  "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
by(Simp_tac 1);
qed_spec_mp "step_plusI";

Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
by(induct_tac "w" 1);
 by(Simp_tac 1);
by(Simp_tac 1);
by(blast_tac (claset() addIs [step_plusI]) 1);
qed_spec_mp "steps_plusI";

Goalw [plus_def,step_def]
 "!A. (p,r): step (plus A) a = \
\     ( (p,r): step A a | fin A p & (start A,r) : step A a )";
by(Simp_tac 1);
qed_spec_mp "step_plus_conv";
AddIffs [step_plus_conv];

Goal
 "[| (start A,q) : steps A u; u ~= []; fin A p |] \
\ ==> (p,q) : steps (plus A) u";
by(exhaust_tac "u" 1);
 by(Blast_tac 1);
by(Asm_full_simp_tac 1);
by(blast_tac (claset() addIs [steps_plusI]) 1);
qed "fin_steps_plusI";

(* reverse list induction! Complicates matters for conc? *)
Goal
 "!r. (start A,r) : steps (plus A) w --> \
\     (? us v. w = concat us @ v & \
\              (!u:set us. u ~= [] & accepts A u) & \
\              (start A,r) : steps A v)";
by(rev_induct_tac "w" 1);
 by (Simp_tac 1);
 by(res_inst_tac [("x","[]")] exI 1);
 by (Simp_tac 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by(etac allE 1 THEN mp_tac 1);
by (Clarify_tac 1);
be disjE 1;
 by(res_inst_tac [("x","us")] exI 1);
 by(Asm_simp_tac 1);
 by(Blast_tac 1);
by(exhaust_tac "v" 1);
 by(res_inst_tac [("x","us")] exI 1);
 by(Asm_full_simp_tac 1);
by(res_inst_tac [("x","us@[v]")] exI 1);
by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
by(Blast_tac 1);
qed_spec_mp "start_steps_plusD";

Goal
 "!r. (start A,r) : steps (plus A) w --> \
\     (? us v. w = concat us @ v & \
\              (!u:set us. accepts A u) & \
\              (start A,r) : steps A v)";
by(rev_induct_tac "w" 1);
 by (Simp_tac 1);
 by(res_inst_tac [("x","[]")] exI 1);
 by (Simp_tac 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by(etac allE 1 THEN mp_tac 1);
by (Clarify_tac 1);
be disjE 1;
 by(res_inst_tac [("x","us")] exI 1);
 by(Asm_simp_tac 1);
 by(Blast_tac 1);
by(res_inst_tac [("x","us@[v]")] exI 1);
by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
by(Blast_tac 1);
qed_spec_mp "start_steps_plusD";

Goal
 "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
by(rev_induct_tac "us" 1);
 by(Simp_tac 1);
by(rename_tac "u us" 1);
by(Simp_tac 1);
by (Clarify_tac 1);
by(case_tac "us = []" 1);
 by(Asm_full_simp_tac 1);
 by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
by (Clarify_tac 1);
by(case_tac "u = []" 1);
 by(Asm_full_simp_tac 1);
 by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
by(Asm_full_simp_tac 1);
by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
qed_spec_mp "steps_star_cycle";

Goal
 "accepts (plus A) w = \
\ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
br iffI 1;
 by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
 by (Clarify_tac 1);
 bd start_steps_plusD 1;
 by (Clarify_tac 1);
 by(res_inst_tac [("x","us@[v]")] exI 1);
 by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
 by(Blast_tac 1);
by(blast_tac (claset() addIs [steps_star_cycle]) 1);
qed "accepts_plus";
AddIffs [accepts_plus];

(******************************************************)
(*                       star                         *)
(******************************************************)

Goalw [star_def]
"accepts (star A) w = \
\ (? us. (!u : set us. accepts A u) & w = concat us)";
br iffI 1;
 by (Clarify_tac 1);
 be disjE 1;
  by(res_inst_tac [("x","[]")] exI 1);
  by(Simp_tac 1);
  by(Blast_tac 1);
 by(Blast_tac 1);
by(Force_tac 1);
qed "accepts_star";

(***** Correctness of r2n *****)

Goal
 "!w. accepts (rexp2na r) w = (w : lang r)";
by(induct_tac "r" 1);
    by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
  by(Asm_simp_tac 1);
 by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
qed_spec_mp "accepts_rexp2na";