src/HOL/Orderings.thy
changeset 21091 5061e3e56484
parent 21083 a1de02f047d0
child 21180 f27f12bcafb8
--- 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 *}