--- 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)
--- 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) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
by(simp add: update_def inorder_upd)
-
lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
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: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -142,21 +141,18 @@
subsection \<open>Balancedness\<close>
lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> 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 \<Longrightarrow> bal (update x y t)"
by (simp add: update_def bal_upd)
-
lemma height_del: "bal t \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> bal(delete x t)"
by(simp add: delete_def bal_tree\<^sub>d_del)
--- 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) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps2)
+by (induction t) (auto simp: elems_simps2 split!: if_splits)
subsubsection \<open>Functional correctness of insert:\<close>
lemma inorder_ins:
"sorted(inorder t) \<Longrightarrow> 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) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
@@ -271,8 +271,8 @@
lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
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: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -297,7 +297,7 @@
end
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> 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 \<Longrightarrow> 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:
"\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
@@ -495,8 +495,7 @@
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> 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 \<Longrightarrow> bal(delete x t)"
by(simp add: delete_def bal_tree\<^sub>d_del)
--- 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: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
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: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -99,7 +99,7 @@
subsection \<open>Balancedness\<close>
lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> 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 \<Longrightarrow> bal (update x y t)"
by (simp add: update_def bal_upd)
--- 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: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
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: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -217,7 +217,7 @@
end
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> 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. *}
--- 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;
--- 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 _ =