src/HOL/Lex/Regset_of_auto.ML

expandshort;

Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
Addsimps [image_eqI];

AddIffs [star.NilI];
Addsimps [star.ConsI];
AddIs [star.ConsI];

(* Lists *)

(*
(* could go into List. Needs WF_Rel as ancestor. *)
(* Induction over the length of a list: *)
val prems = goal thy
 "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
     wf_induct 1);
by (Simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
by (eresolve_tac prems 1);
qed "list_length_induct";
*)

goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
by (exhaust_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
qed "butlast_empty";
AddIffs [butlast_empty];

goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
by (induct_tac "xss" 1);
 by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
                           addsplits [expand_if]) 1);
by (rtac conjI 1);
 by (Clarify_tac 1);
 by (rtac conjI 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
 by (subgoal_tac "xs=[]" 1);
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
 by (Blast_tac 1);
by (blast_tac (claset() addDs [in_set_butlastD]) 1);
qed_spec_mp "in_set_butlast_concatI";

(* Regular sets *)

goal thy "(!xs: set xss. xs:A) --> concat xss : star A";
by (induct_tac "xss" 1);
by (ALLGOALS Asm_full_simp_tac);
qed_spec_mp "concat_in_star";

(* The main lemma:
   how to decompose a trace into a prefix, a list of loops and a suffix.
*)
goal thy "!i. k : set(trace A i xs) --> (? pref mids suf. \
\ xs = pref @ concat mids @ suf & \
\ deltas A pref i = k & (!n:set(butlast(trace A i pref)). n ~= k) & \
\ (!mid:set mids. (deltas A mid k = k) & \
\                 (!n:set(butlast(trace A k mid)). n ~= k)) & \
\ (!n:set(butlast(trace A k suf)). n ~= k))";
by (induct_tac "xs" 1);
 by (Simp_tac 1);
by (rename_tac "a as" 1);
by (rtac allI 1);
by (case_tac "A a i = k" 1);
 by (strip_tac 1);
 by (res_inst_tac[("x","[a]")]exI 1);
 by (Asm_full_simp_tac 1);
 by (case_tac "k : set(trace A (A a i) as)" 1);
  by (etac allE 1);
  by (etac impE 1);
   by (assume_tac 1);
  by (REPEAT(etac exE 1));
  by (res_inst_tac[("x","pref#mids")]exI 1);
  by (res_inst_tac[("x","suf")]exI 1);
  by (Asm_full_simp_tac 1);
 by (res_inst_tac[("x","[]")]exI 1);
 by (res_inst_tac[("x","as")]exI 1);
 by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addDs [in_set_butlastD]) 1);
by (Asm_simp_tac 1);
by (rtac conjI 1);
 by (Blast_tac 1);
by (strip_tac 1);
by (etac allE 1);
by (etac impE 1);
 by (assume_tac 1);
by (REPEAT(etac exE 1));
by (res_inst_tac[("x","a#pref")]exI 1);
by (res_inst_tac[("x","mids")]exI 1);
by (res_inst_tac[("x","suf")]exI 1);
by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
qed_spec_mp "decompose";

goal thy "!i. length(trace A i xs) = length xs";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "length_trace";
Addsimps [length_trace];

goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "deltas_append";
Addsimps [deltas_append];

goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "trace_append";
Addsimps [trace_append];

goal thy "(!xs: set xss. deltas A xs i = i) --> \
\         trace A i (concat xss) = concat (map (trace A i) xss)";
by (induct_tac "xss" 1);
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "trace_concat";
Addsimps [trace_concat];

goal thy "!i. (trace A i xs = []) = (xs = [])";
by (exhaust_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "trace_is_Nil";
Addsimps [trace_is_Nil];

goal thy "(trace A i xs = n#ns) = \
\         (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)";
by (exhaust_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
qed_spec_mp "trace_is_Cons_conv";
Addsimps [trace_is_Cons_conv];

goal thy "!i. set(trace A i xs) = \
\ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
by (induct_tac "xs" 1);
 by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
qed "set_trace_conv";

goal thy
 "(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k";
by (induct_tac "mids" 1);
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "deltas_concat";
Addsimps [deltas_concat];

goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
by (etac nat_neqE 1);
by (ALLGOALS trans_tac);
val lemma = result();


goal thy
 "!i j xs. xs : regset_of A i j k = \
\          ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
by (induct_tac "k" 1);
 by (simp_tac (simpset() addcongs [conj_cong]
                        addsplits [expand_if,split_list_case]) 1);
by (strip_tac 1);
by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
by (rtac iffI 1);
 by (etac disjE 1);
  by (Asm_simp_tac 1);
 by (REPEAT(eresolve_tac[exE,conjE] 1));
 by (Asm_full_simp_tac 1);
 by (subgoal_tac
      "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
  by (asm_simp_tac (simpset() addsplits [expand_if]
       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
 by (etac star.induct 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (simpset() addsplits [expand_if]
       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
by (case_tac "k : set(butlast(trace A i xs))" 1);
 by (rtac disjI1 2);
 by (blast_tac (claset() addIs [lemma]) 2);
by (rtac disjI2 1);
by (dtac (in_set_butlastD RS decompose) 1);
by (Clarify_tac 1);
by (res_inst_tac [("x","pref")] exI 1);
by (Asm_full_simp_tac 1);
by (rtac conjI 1);
 by (rtac ballI 1);
 by (rtac lemma 1);
  by (Asm_simp_tac 2);
 by (EVERY[dtac bspec 1, atac 2]);
 by (Asm_simp_tac 1);
by (res_inst_tac [("x","concat mids")] exI 1);
by (Simp_tac 1);
by (rtac conjI 1);
 by (rtac concat_in_star 1);
 by (Asm_simp_tac 1);
 by (rtac ballI 1);
 by (rtac ballI 1);
 by (rtac lemma 1);
  by (Asm_simp_tac 2);
 by (EVERY[dtac bspec 1, atac 2]);
 by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
by (rtac ballI 1);
by (rtac lemma 1);
 by (Asm_simp_tac 2);
by (EVERY[dtac bspec 1, atac 2]);
by (Asm_simp_tac 1);
qed_spec_mp "regset_of_spec";

goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \
\         !i. i < k --> (!n:set(trace A i xs). n < k)";
by (induct_tac "xs" 1);
 by (ALLGOALS Simp_tac);
by (Blast_tac 1);
qed_spec_mp "trace_below";

goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \
\         regset_of A i j k = {xs. deltas A xs i = j}";
by (rtac set_ext 1);
by (simp_tac (simpset() addsimps [regset_of_spec]) 1);
by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
qed "regset_of_below";