faster metis calls
authorpaulson
Fri Nov 23 17:37:56 2007 +0100 (2007-11-23)
changeset 25457ba2bcae7aafd
parent 25456 6f79698f294d
child 25458 ba8f5e4fa336
faster metis calls
src/HOL/MetisExamples/BT.thy
src/HOL/MetisExamples/Message.thy
     1.1 --- a/src/HOL/MetisExamples/BT.thy	Thu Nov 22 14:51:34 2007 +0100
     1.2 +++ b/src/HOL/MetisExamples/BT.thy	Fri Nov 23 17:37:56 2007 +0100
     1.3 @@ -171,7 +171,7 @@
     1.4  lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
     1.5    apply (induct t)
     1.6    apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
     1.7 -  apply (metis add_commute bt_map.simps(2) n_leaves.simps(2))
     1.8 +  apply (metis bt_map.simps(2) n_leaves.simps(2))
     1.9    done
    1.10  
    1.11  
    1.12 @@ -179,7 +179,7 @@
    1.13  lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
    1.14    apply (induct t)
    1.15    apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
    1.16 -  apply (metis append_eq_append_conv2 inorder.simps(1) postorder.simps(2) preorder.simps(2) reflect.simps(2) rev_append rev_is_rev_conv rev_singleton_conv rev_swap rotate_simps)
    1.17 +  apply (metis Cons_eq_append_conv monoid_append.add_0_left postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
    1.18    done
    1.19  
    1.20  ML {*ResAtp.problem_name := "BT__inorder_reflect"*}
    1.21 @@ -193,7 +193,7 @@
    1.22  lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
    1.23    apply (induct t)
    1.24    apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
    1.25 -  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rotate1_def self_append_conv2)
    1.26 +  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2)
    1.27    done
    1.28  
    1.29  text {*
     2.1 --- a/src/HOL/MetisExamples/Message.thy	Thu Nov 22 14:51:34 2007 +0100
     2.2 +++ b/src/HOL/MetisExamples/Message.thy	Fri Nov 23 17:37:56 2007 +0100
     2.3 @@ -253,7 +253,7 @@
     2.4  
     2.5  ML{*ResAtp.problem_name := "Message__parts_cut"*}
     2.6  lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
     2.7 -by (metis Un_subset_iff Un_upper1 Un_upper2 insert_subset parts_Un parts_increasing parts_trans) 
     2.8 +by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
     2.9  
    2.10  
    2.11