# HG changeset patch # User haftmann # Date 1161594307 -7200 # Node ID 5061e3e56484f775c9200aeed44ddc5566b7255b # Parent e694285770a24bcc0533c665e1c5314e2eedb77a cleanup in ML setup code diff -r e694285770a2 -r 5061e3e56484 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Mon Oct 23 11:05:06 2006 +0200 +++ b/src/HOL/Orderings.thy Mon Oct 23 11:05:07 2006 +0200 @@ -235,6 +235,83 @@ subsection {* Reasoning tools setup *} +ML {* +local + +fun decomp_gen sort thy (Trueprop $ t) = + let fun of_sort t = let val T = type_of t in + (* exclude numeric types: linear arithmetic subsumes transitivity *) + T <> HOLogic.natT andalso T <> HOLogic.intT andalso + T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) end + fun dec (Const ("Not", _) $ t) = ( + case dec t of + NONE => NONE + | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) + | dec (Const ("op =", _) $ t1 $ t2) = + if of_sort t1 + then SOME (t1, "=", t2) + else NONE + | dec (Const ("Orderings.less_eq", _) $ t1 $ t2) = + if of_sort t1 + then SOME (t1, "<=", t2) + else NONE + | dec (Const ("Orderings.less", _) $ t1 $ t2) = + if of_sort t1 + then SOME (t1, "<", t2) + else NONE + | dec _ = NONE + in dec t end; + +in + +structure Quasi_Tac = Quasi_Tac_Fun ( +(* The setting up of Quasi_Tac serves as a demo. Since there is no + class for quasi orders, the tactics Quasi_Tac.trans_tac and + Quasi_Tac.quasi_tac are not of much use. *) + struct + val le_trans = thm "order_trans"; + val le_refl = thm "order_refl"; + val eqD1 = thm "order_eq_refl"; + val eqD2 = thm "sym" RS thm "order_eq_refl"; + val less_reflE = thm "order_less_irrefl" RS thm "notE"; + val less_imp_le = thm "order_less_imp_le"; + val le_neq_trans = thm "order_le_neq_trans"; + val neq_le_trans = thm "order_neq_le_trans"; + val less_imp_neq = thm "less_imp_neq"; + val decomp_trans = decomp_gen ["Orderings.order"]; + val decomp_quasi = decomp_gen ["Orderings.order"]; + + end); + +structure Order_Tac = Order_Tac_Fun ( + struct + val less_reflE = thm "order_less_irrefl" RS thm "notE"; + val le_refl = thm "order_refl"; + val less_imp_le = thm "order_less_imp_le"; + val not_lessI = thm "linorder_not_less" RS thm "iffD2"; + val not_leI = thm "linorder_not_le" RS thm "iffD2"; + val not_lessD = thm "linorder_not_less" RS thm "iffD1"; + val not_leD = thm "linorder_not_le" RS thm "iffD1"; + val eqI = thm "order_antisym"; + val eqD1 = thm "order_eq_refl"; + val eqD2 = thm "sym" RS thm "order_eq_refl"; + val less_trans = thm "order_less_trans"; + val less_le_trans = thm "order_less_le_trans"; + val le_less_trans = thm "order_le_less_trans"; + val le_trans = thm "order_trans"; + val le_neq_trans = thm "order_le_neq_trans"; + val neq_le_trans = thm "order_neq_le_trans"; + val less_imp_neq = thm "less_imp_neq"; + val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; + val not_sym = thm "not_sym"; + val decomp_part = decomp_gen ["Orderings.order"]; + val decomp_lin = decomp_gen ["Orderings.linorder"]; + + end); + +end; +*} + setup {* let @@ -281,111 +358,18 @@ "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less; in - - (fn thy => (Simplifier.change_simpset_of thy - (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy)) - + (fn thy => (Simplifier.change_simpset_of thy + (fn ss => ss + addsimprocs [antisym_le, antisym_less] + addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac)) + addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac))) + (* Adding the transitivity reasoners also as safe solvers showed a slight + speed up, but the reasoning strength appears to be not higher (at least + no breaking of additional proofs in the entire HOL distribution, as + of 5 March 2004, was observed). *); thy)) end *} -ML_setup {* - -(* The setting up of Quasi_Tac serves as a demo. Since there is no - class for quasi orders, the tactics Quasi_Tac.trans_tac and - Quasi_Tac.quasi_tac are not of much use. *) - -fun decomp_gen sort thy (Trueprop $ t) = - let fun of_sort t = let val T = type_of t in - (* exclude numeric types: linear arithmetic subsumes transitivity *) - T <> HOLogic.natT andalso T <> HOLogic.intT andalso - T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) end - fun dec (Const ("Not", _) $ t) = ( - case dec t of - NONE => NONE - | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) - | dec (Const ("op =", _) $ t1 $ t2) = - if of_sort t1 - then SOME (t1, "=", t2) - else NONE - | dec (Const ("Orderings.less_eq", _) $ t1 $ t2) = - if of_sort t1 - then SOME (t1, "<=", t2) - else NONE - | dec (Const ("Orderings.less", _) $ t1 $ t2) = - if of_sort t1 - then SOME (t1, "<", t2) - else NONE - | dec _ = NONE - in dec t end; - -structure Quasi_Tac = Quasi_Tac_Fun ( - struct - val le_trans = thm "order_trans"; - val le_refl = thm "order_refl"; - val eqD1 = thm "order_eq_refl"; - val eqD2 = thm "sym" RS thm "order_eq_refl"; - val less_reflE = thm "order_less_irrefl" RS thm "notE"; - val less_imp_le = thm "order_less_imp_le"; - val le_neq_trans = thm "order_le_neq_trans"; - val neq_le_trans = thm "order_neq_le_trans"; - val less_imp_neq = thm "less_imp_neq"; - val decomp_trans = decomp_gen ["Orderings.order"]; - val decomp_quasi = decomp_gen ["Orderings.order"]; - - end); (* struct *) - -structure Order_Tac = Order_Tac_Fun ( - struct - val less_reflE = thm "order_less_irrefl" RS thm "notE"; - val le_refl = thm "order_refl"; - val less_imp_le = thm "order_less_imp_le"; - val not_lessI = thm "linorder_not_less" RS thm "iffD2"; - val not_leI = thm "linorder_not_le" RS thm "iffD2"; - val not_lessD = thm "linorder_not_less" RS thm "iffD1"; - val not_leD = thm "linorder_not_le" RS thm "iffD1"; - val eqI = thm "order_antisym"; - val eqD1 = thm "order_eq_refl"; - val eqD2 = thm "sym" RS thm "order_eq_refl"; - val less_trans = thm "order_less_trans"; - val less_le_trans = thm "order_less_le_trans"; - val le_less_trans = thm "order_le_less_trans"; - val le_trans = thm "order_trans"; - val le_neq_trans = thm "order_le_neq_trans"; - val neq_le_trans = thm "order_neq_le_trans"; - val less_imp_neq = thm "less_imp_neq"; - val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; - val not_sym = thm "not_sym"; - val decomp_part = decomp_gen ["Orderings.order"]; - val decomp_lin = decomp_gen ["Orderings.linorder"]; - - end); (* struct *) - -change_simpset (fn ss => ss - addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac)) - addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac))); - (* Adding the transitivity reasoners also as safe solvers showed a slight - speed up, but the reasoning strength appears to be not higher (at least - no breaking of additional proofs in the entire HOL distribution, as - of 5 March 2004, was observed). *) -*} - -(* Optional setup of methods *) - -(* -method_setup trans_partial = - {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *} - {* transitivity reasoner for partial orders *} -method_setup trans_linear = - {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *} - {* transitivity reasoner for linear orders *} -*) - -(* -declare order.order_refl [simp del] order_less_irrefl [simp del] - -can currently not be removed, abel_cancel relies on it. -*) - subsection {* Bounded quantifiers *}