introduced aggressive splitter "split!"
authornipkow
Tue Aug 09 17:00:36 2016 +0200 (2016-08-09)
changeset 636366f38b7abb648
parent 63625 1e7c5bbea36d
child 63637 9a57baa15e1b
introduced aggressive splitter "split!"
src/HOL/Data_Structures/AA_Set.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Tools/simpdata.ML
src/Provers/splitter.ML
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Sun Aug 07 12:10:49 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Tue Aug 09 17:00:36 2016 +0200
     1.3 @@ -329,7 +329,7 @@
     1.4    from lDown_tDouble and r obtain rrlv rrr rra rrl where
     1.5      rr :"rr = Node rrlv rrr rra rrl" by (cases rr) auto
     1.6    from  lDown_tDouble show ?thesis unfolding adjust_def r rr
     1.7 -    apply (cases rl) apply (auto simp add: invar.simps(2))
     1.8 +    apply (cases rl) apply (auto simp add: invar.simps(2) split!: if_split)
     1.9      using lDown_tDouble by (auto simp: split_case lvl_0_iff  elim:lvl.elims split: tree.split)
    1.10  qed (auto simp: split_case invar.simps(2) adjust_def split: tree.splits)
    1.11  
     2.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Sun Aug 07 12:10:49 2016 +0200
     2.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Tue Aug 09 17:00:36 2016 +0200
     2.3 @@ -127,12 +127,11 @@
     2.4    "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
     2.5  by(simp add: update_def inorder_upd)
     2.6  
     2.7 -
     2.8  lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
     2.9    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    2.10  by(induction t rule: del.induct)
    2.11 -  ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
    2.12 -(* 200 secs (2015) *)
    2.13 +  (auto simp: del_list_simps inorder_nodes del_minD split!: if_splits prod.splits)
    2.14 +(* 30 secs (2016) *)
    2.15  
    2.16  lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    2.17    inorder(delete x t) = del_list x (inorder t)"
    2.18 @@ -142,21 +141,18 @@
    2.19  subsection \<open>Balancedness\<close>
    2.20  
    2.21  lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
    2.22 -by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
    2.23 +by (induct t) (auto, auto split!: if_split up\<^sub>i.split) (* 20 secs (2015) *)
    2.24  
    2.25  lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
    2.26  by (simp add: update_def bal_upd)
    2.27  
    2.28 -
    2.29  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    2.30  by(induction x t rule: del.induct)
    2.31 -  (auto simp add: heights height_del_min split: prod.split)
    2.32 -(* 20 secs (2015) *)
    2.33 +  (auto simp add: heights height_del_min split!: if_split prod.split)
    2.34  
    2.35  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
    2.36  by(induction x t rule: del.induct)
    2.37 -  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
    2.38 -(* 100 secs (2015) *)
    2.39 +  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
    2.40  
    2.41  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
    2.42  by(simp add: delete_def bal_tree\<^sub>d_del)
     3.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Sun Aug 07 12:10:49 2016 +0200
     3.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Tue Aug 09 17:00:36 2016 +0200
     3.3 @@ -206,14 +206,14 @@
     3.4  by (induction t) (auto simp: elems_simps1 ball_Un)
     3.5  
     3.6  lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
     3.7 -by (induction t) (auto simp: elems_simps2)
     3.8 +by (induction t) (auto simp: elems_simps2 split!: if_splits)
     3.9  
    3.10  
    3.11  subsubsection \<open>Functional correctness of insert:\<close>
    3.12  
    3.13  lemma inorder_ins:
    3.14    "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
    3.15 -by(induction t) (auto, auto simp: ins_list_simps split: up\<^sub>i.splits)
    3.16 +by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits)
    3.17  
    3.18  lemma inorder_insert:
    3.19    "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
    3.20 @@ -271,8 +271,8 @@
    3.21  lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    3.22    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    3.23  by(induction t rule: del.induct)
    3.24 -  (auto simp: inorder_nodes del_list_simps del_minD split: prod.splits)
    3.25 -  (* 150 secs (2015) *)
    3.26 +  (auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits)
    3.27 +  (* 30 secs (2016) *)
    3.28  
    3.29  lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    3.30    inorder(delete x t) = del_list x (inorder t)"
    3.31 @@ -297,7 +297,7 @@
    3.32  end
    3.33  
    3.34  lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
    3.35 -by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
    3.36 +by (induct t) (auto split!: if_split up\<^sub>i.split)
    3.37  
    3.38  
    3.39  text{* Now an alternative proof (by Brian Huffman) that runs faster because
    3.40 @@ -486,7 +486,7 @@
    3.41  
    3.42  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    3.43  by(induction x t rule: del.induct)
    3.44 -  (auto simp add: heights height_del_min split: prod.split)
    3.45 +  (auto simp add: heights height_del_min split!: if_split prod.split)
    3.46  
    3.47  lemma bal_del_min:
    3.48    "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
    3.49 @@ -495,8 +495,7 @@
    3.50  
    3.51  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
    3.52  by(induction x t rule: del.induct)
    3.53 -  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
    3.54 -(* 60 secs (2015) *)
    3.55 +  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
    3.56  
    3.57  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
    3.58  by(simp add: delete_def bal_tree\<^sub>d_del)
     4.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Sun Aug 07 12:10:49 2016 +0200
     4.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Tue Aug 09 17:00:36 2016 +0200
     4.3 @@ -89,7 +89,7 @@
     4.4  lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
     4.5    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
     4.6  by(induction t rule: del.induct)
     4.7 -  (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
     4.8 +  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
     4.9  
    4.10  corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    4.11    inorder(delete x t) = del_list x (inorder t)"
    4.12 @@ -99,7 +99,7 @@
    4.13  subsection \<open>Balancedness\<close>
    4.14  
    4.15  lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
    4.16 -by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *)
    4.17 +by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *)
    4.18  
    4.19  corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
    4.20  by (simp add: update_def bal_upd)
     5.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Sun Aug 07 12:10:49 2016 +0200
     5.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Tue Aug 09 17:00:36 2016 +0200
     5.3 @@ -191,7 +191,7 @@
     5.4  lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
     5.5    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
     5.6  by(induction t rule: del.induct)
     5.7 -  (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
     5.8 +  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
     5.9  
    5.10  lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    5.11    inorder(delete x t) = del_list x (inorder t)"
    5.12 @@ -217,7 +217,7 @@
    5.13  end
    5.14  
    5.15  lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
    5.16 -by (induct t) (auto split: up\<^sub>i.split) (* 15 secs in 2015 *)
    5.17 +by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
    5.18  
    5.19  text{* Now an alternative proof (by Brian Huffman) that runs faster because
    5.20  two properties (balance and height) are combined in one predicate. *}
     6.1 --- a/src/HOL/Tools/simpdata.ML	Sun Aug 07 12:10:49 2016 +0200
     6.2 +++ b/src/HOL/Tools/simpdata.ML	Tue Aug 09 17:00:36 2016 +0200
     6.3 @@ -152,6 +152,7 @@
     6.4    val contrapos = @{thm contrapos_nn}
     6.5    val contrapos2 = @{thm contrapos_pp}
     6.6    val notnotD = @{thm notnotD}
     6.7 +  val safe_tac = Classical.safe_tac
     6.8  );
     6.9  
    6.10  val split_tac = Splitter.split_tac;
     7.1 --- a/src/Provers/splitter.ML	Sun Aug 07 12:10:49 2016 +0200
     7.2 +++ b/src/Provers/splitter.ML	Tue Aug 09 17:00:36 2016 +0200
     7.3 @@ -19,6 +19,7 @@
     7.4    val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"            *)
     7.5    val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"            *)
     7.6    val notnotD       : thm (* "~ ~ P ==> P"                           *)
     7.7 +  val safe_tac      : Proof.context -> tactic
     7.8  end
     7.9  
    7.10  signature SPLITTER =
    7.11 @@ -33,9 +34,8 @@
    7.12    val split_inside_tac: Proof.context -> thm list -> int -> tactic
    7.13    val split_asm_tac   : Proof.context -> thm list -> int -> tactic
    7.14    val add_split: thm -> Proof.context -> Proof.context
    7.15 +  val add_split_bang: thm -> Proof.context -> Proof.context
    7.16    val del_split: thm -> Proof.context -> Proof.context
    7.17 -  val split_add: attribute
    7.18 -  val split_del: attribute
    7.19    val split_modifiers : Method.modifier parser list
    7.20  end;
    7.21  
    7.22 @@ -435,12 +435,20 @@
    7.23  fun split_name (name, T) asm = "split " ^
    7.24    (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
    7.25  
    7.26 -fun add_split split ctxt =
    7.27 +fun gen_add_split bang split ctxt =
    7.28    let
    7.29      val (name, asm) = split_thm_info split
    7.30 -    fun tac ctxt' = (if asm then split_asm_tac else split_tac) ctxt' [split]
    7.31 +    fun tac ctxt' =
    7.32 +      (if asm then split_asm_tac ctxt' [split]
    7.33 +       else if bang
    7.34 +            then split_tac ctxt' [split] THEN_ALL_NEW
    7.35 +                 TRY o (SELECT_GOAL (Data.safe_tac ctxt'))
    7.36 +            else split_tac ctxt' [split])
    7.37    in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
    7.38  
    7.39 +val add_split = gen_add_split false;
    7.40 +val add_split_bang = gen_add_split true;
    7.41 +
    7.42  fun del_split split ctxt =
    7.43    let val (name, asm) = split_thm_info split
    7.44    in Simplifier.delloop (ctxt, split_name name asm) end;
    7.45 @@ -450,20 +458,26 @@
    7.46  
    7.47  val splitN = "split";
    7.48  
    7.49 -val split_add = Simplifier.attrib add_split;
    7.50 +fun split_add bang = Simplifier.attrib (gen_add_split bang);
    7.51  val split_del = Simplifier.attrib del_split;
    7.52  
    7.53 -val _ =
    7.54 -  Theory.setup
    7.55 -    (Attrib.setup @{binding split}
    7.56 -      (Attrib.add_del split_add split_del) "declare case split rule");
    7.57 +val opt_bang = Scan.optional (Args.bang >> K true) false;
    7.58 +
    7.59 +val add_del =
    7.60 +  Scan.lift (Args.add |-- opt_bang >> split_add
    7.61 +    || Args.del >> K split_del || opt_bang >> split_add);
    7.62 +
    7.63 +val _ = Theory.setup
    7.64 +  (Attrib.setup @{binding split} add_del "declare case split rule");
    7.65  
    7.66  
    7.67  (* methods *)
    7.68  
    7.69  val split_modifiers =
    7.70 - [Args.$$$ splitN -- Args.colon >> K (Method.modifier split_add @{here}),
    7.71 -  Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
    7.72 + [Args.$$$ splitN -- Args.colon >> K (Method.modifier (split_add false) @{here}),
    7.73 +  Args.$$$ splitN -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}),
    7.74 +  Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier (split_add false) @{here}),
    7.75 +  Args.$$$ splitN -- Args.add -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}),
    7.76    Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
    7.77  
    7.78  val _ =