# HG changeset patch # User nipkow # Date 1470754836 -7200 # Node ID 6f38b7abb648b0ada0a9e1e0a0702f8b526e5e38 # Parent 1e7c5bbea36dd2dd56705630f8e456de91b9788a introduced aggressive splitter "split!" diff -r 1e7c5bbea36d -r 6f38b7abb648 src/HOL/Data_Structures/AA_Set.thy --- a/src/HOL/Data_Structures/AA_Set.thy Sun Aug 07 12:10:49 2016 +0200 +++ b/src/HOL/Data_Structures/AA_Set.thy Tue Aug 09 17:00:36 2016 +0200 @@ -329,7 +329,7 @@ from lDown_tDouble and r obtain rrlv rrr rra rrl where rr :"rr = Node rrlv rrr rra rrl" by (cases rr) auto from lDown_tDouble show ?thesis unfolding adjust_def r rr - apply (cases rl) apply (auto simp add: invar.simps(2)) + apply (cases rl) apply (auto simp add: invar.simps(2) split!: if_split) using lDown_tDouble by (auto simp: split_case lvl_0_iff elim:lvl.elims split: tree.split) qed (auto simp: split_case invar.simps(2) adjust_def split: tree.splits) diff -r 1e7c5bbea36d -r 6f38b7abb648 src/HOL/Data_Structures/Tree234_Map.thy --- a/src/HOL/Data_Structures/Tree234_Map.thy Sun Aug 07 12:10:49 2016 +0200 +++ b/src/HOL/Data_Structures/Tree234_Map.thy Tue Aug 09 17:00:36 2016 +0200 @@ -127,12 +127,11 @@ "sorted1(inorder t) \ inorder(update a b t) = upd_list a b (inorder t)" by(simp add: update_def inorder_upd) - lemma inorder_del: "\ bal t ; sorted1(inorder t) \ \ inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" by(induction t rule: del.induct) - ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+ -(* 200 secs (2015) *) + (auto simp: del_list_simps inorder_nodes del_minD split!: if_splits prod.splits) +(* 30 secs (2016) *) lemma inorder_delete: "\ bal t ; sorted1(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" @@ -142,21 +141,18 @@ subsection \Balancedness\ lemma bal_upd: "bal t \ bal (tree\<^sub>i(upd x y t)) \ height(upd x y t) = height t" -by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *) +by (induct t) (auto, auto split!: if_split up\<^sub>i.split) (* 20 secs (2015) *) lemma bal_update: "bal t \ bal (update x y t)" by (simp add: update_def bal_upd) - lemma height_del: "bal t \ height(del x t) = height t" by(induction x t rule: del.induct) - (auto simp add: heights height_del_min split: prod.split) -(* 20 secs (2015) *) + (auto simp add: heights height_del_min split!: if_split prod.split) lemma bal_tree\<^sub>d_del: "bal t \ bal(tree\<^sub>d(del x t))" by(induction x t rule: del.induct) - (auto simp: bals bal_del_min height_del height_del_min split: prod.split) -(* 100 secs (2015) *) + (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split) corollary bal_delete: "bal t \ bal(delete x t)" by(simp add: delete_def bal_tree\<^sub>d_del) diff -r 1e7c5bbea36d -r 6f38b7abb648 src/HOL/Data_Structures/Tree234_Set.thy --- a/src/HOL/Data_Structures/Tree234_Set.thy Sun Aug 07 12:10:49 2016 +0200 +++ b/src/HOL/Data_Structures/Tree234_Set.thy Tue Aug 09 17:00:36 2016 +0200 @@ -206,14 +206,14 @@ by (induction t) (auto simp: elems_simps1 ball_Un) lemma isin_set: "sorted(inorder t) \ isin t x = (x \ elems (inorder t))" -by (induction t) (auto simp: elems_simps2) +by (induction t) (auto simp: elems_simps2 split!: if_splits) subsubsection \Functional correctness of insert:\ lemma inorder_ins: "sorted(inorder t) \ inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)" -by(induction t) (auto, auto simp: ins_list_simps split: up\<^sub>i.splits) +by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits) lemma inorder_insert: "sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" @@ -271,8 +271,8 @@ lemma inorder_del: "\ bal t ; sorted(inorder t) \ \ inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" by(induction t rule: del.induct) - (auto simp: inorder_nodes del_list_simps del_minD split: prod.splits) - (* 150 secs (2015) *) + (auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits) + (* 30 secs (2016) *) lemma inorder_delete: "\ bal t ; sorted(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" @@ -297,7 +297,7 @@ end lemma bal_ins: "bal t \ bal (tree\<^sub>i(ins a t)) \ height(ins a t) = height t" -by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *) +by (induct t) (auto split!: if_split up\<^sub>i.split) text{* Now an alternative proof (by Brian Huffman) that runs faster because @@ -486,7 +486,7 @@ lemma height_del: "bal t \ height(del x t) = height t" by(induction x t rule: del.induct) - (auto simp add: heights height_del_min split: prod.split) + (auto simp add: heights height_del_min split!: if_split prod.split) lemma bal_del_min: "\ del_min t = (x, t'); bal t; height t > 0 \ \ bal (tree\<^sub>d t')" @@ -495,8 +495,7 @@ lemma bal_tree\<^sub>d_del: "bal t \ bal(tree\<^sub>d(del x t))" by(induction x t rule: del.induct) - (auto simp: bals bal_del_min height_del height_del_min split: prod.split) -(* 60 secs (2015) *) + (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split) corollary bal_delete: "bal t \ bal(delete x t)" by(simp add: delete_def bal_tree\<^sub>d_del) diff -r 1e7c5bbea36d -r 6f38b7abb648 src/HOL/Data_Structures/Tree23_Map.thy --- a/src/HOL/Data_Structures/Tree23_Map.thy Sun Aug 07 12:10:49 2016 +0200 +++ b/src/HOL/Data_Structures/Tree23_Map.thy Tue Aug 09 17:00:36 2016 +0200 @@ -89,7 +89,7 @@ lemma inorder_del: "\ bal t ; sorted1(inorder t) \ \ inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" by(induction t rule: del.induct) - (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits) + (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits) corollary inorder_delete: "\ bal t ; sorted1(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" @@ -99,7 +99,7 @@ subsection \Balancedness\ lemma bal_upd: "bal t \ bal (tree\<^sub>i(upd x y t)) \ height(upd x y t) = height t" -by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *) +by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *) corollary bal_update: "bal t \ bal (update x y t)" by (simp add: update_def bal_upd) diff -r 1e7c5bbea36d -r 6f38b7abb648 src/HOL/Data_Structures/Tree23_Set.thy --- a/src/HOL/Data_Structures/Tree23_Set.thy Sun Aug 07 12:10:49 2016 +0200 +++ b/src/HOL/Data_Structures/Tree23_Set.thy Tue Aug 09 17:00:36 2016 +0200 @@ -191,7 +191,7 @@ lemma inorder_del: "\ bal t ; sorted(inorder t) \ \ inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" by(induction t rule: del.induct) - (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits) + (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits) lemma inorder_delete: "\ bal t ; sorted(inorder t) \ \ inorder(delete x t) = del_list x (inorder t)" @@ -217,7 +217,7 @@ end lemma bal_ins: "bal t \ bal (tree\<^sub>i(ins a t)) \ height(ins a t) = height t" -by (induct t) (auto split: up\<^sub>i.split) (* 15 secs in 2015 *) +by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *) text{* Now an alternative proof (by Brian Huffman) that runs faster because two properties (balance and height) are combined in one predicate. *} diff -r 1e7c5bbea36d -r 6f38b7abb648 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Sun Aug 07 12:10:49 2016 +0200 +++ b/src/HOL/Tools/simpdata.ML Tue Aug 09 17:00:36 2016 +0200 @@ -152,6 +152,7 @@ val contrapos = @{thm contrapos_nn} val contrapos2 = @{thm contrapos_pp} val notnotD = @{thm notnotD} + val safe_tac = Classical.safe_tac ); val split_tac = Splitter.split_tac; diff -r 1e7c5bbea36d -r 6f38b7abb648 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Sun Aug 07 12:10:49 2016 +0200 +++ b/src/Provers/splitter.ML Tue Aug 09 17:00:36 2016 +0200 @@ -19,6 +19,7 @@ val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *) val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *) val notnotD : thm (* "~ ~ P ==> P" *) + val safe_tac : Proof.context -> tactic end signature SPLITTER = @@ -33,9 +34,8 @@ val split_inside_tac: Proof.context -> thm list -> int -> tactic val split_asm_tac : Proof.context -> thm list -> int -> tactic val add_split: thm -> Proof.context -> Proof.context + val add_split_bang: thm -> Proof.context -> Proof.context val del_split: thm -> Proof.context -> Proof.context - val split_add: attribute - val split_del: attribute val split_modifiers : Method.modifier parser list end; @@ -435,12 +435,20 @@ fun split_name (name, T) asm = "split " ^ (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T; -fun add_split split ctxt = +fun gen_add_split bang split ctxt = let val (name, asm) = split_thm_info split - fun tac ctxt' = (if asm then split_asm_tac else split_tac) ctxt' [split] + fun tac ctxt' = + (if asm then split_asm_tac ctxt' [split] + else if bang + then split_tac ctxt' [split] THEN_ALL_NEW + TRY o (SELECT_GOAL (Data.safe_tac ctxt')) + else split_tac ctxt' [split]) in Simplifier.addloop (ctxt, (split_name name asm, tac)) end; +val add_split = gen_add_split false; +val add_split_bang = gen_add_split true; + fun del_split split ctxt = let val (name, asm) = split_thm_info split in Simplifier.delloop (ctxt, split_name name asm) end; @@ -450,20 +458,26 @@ val splitN = "split"; -val split_add = Simplifier.attrib add_split; +fun split_add bang = Simplifier.attrib (gen_add_split bang); val split_del = Simplifier.attrib del_split; -val _ = - Theory.setup - (Attrib.setup @{binding split} - (Attrib.add_del split_add split_del) "declare case split rule"); +val opt_bang = Scan.optional (Args.bang >> K true) false; + +val add_del = + Scan.lift (Args.add |-- opt_bang >> split_add + || Args.del >> K split_del || opt_bang >> split_add); + +val _ = Theory.setup + (Attrib.setup @{binding split} add_del "declare case split rule"); (* methods *) val split_modifiers = - [Args.$$$ splitN -- Args.colon >> K (Method.modifier split_add @{here}), - Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}), + [Args.$$$ splitN -- Args.colon >> K (Method.modifier (split_add false) @{here}), + Args.$$$ splitN -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}), + Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier (split_add false) @{here}), + Args.$$$ splitN -- Args.add -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}), Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})]; val _ =