# HG changeset patch
# User nipkow
# Date 887993799 -3600
# Node ID ac6cf9f18653990280bf0c5edb332241a4df384d
# Parent  bc6e2936a2936d5bc0e518d5a23ab09b4fec10d7
Congruence rules use == in premises now.
New class linord.

diff -r bc6e2936a293 -r ac6cf9f18653 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Feb 20 17:33:14 1998 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 20 17:56:39 1998 +0100
@@ -23,6 +23,7 @@
 
 
 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
+instance nat :: linorder (nat_le_linear)
 
 consts
   "^"           :: ['a::power,nat] => 'a            (infixr 80)
diff -r bc6e2936a293 -r ac6cf9f18653 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Feb 20 17:33:14 1998 +0100
+++ b/src/HOL/NatDef.ML	Fri Feb 20 17:56:39 1998 +0100
@@ -588,7 +588,15 @@
 by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
 qed "nat_less_le";
 
-(** max **)
+(* Axiom 'linorder_linear' of class 'linorder': *)
+goal thy "(m::nat) <= n | n <= m";
+by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (cut_facts_tac [less_linear] 1);
+by(Blast_tac 1);
+qed "nat_le_linear";
+
+
+(** max
 
 goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
@@ -612,7 +620,7 @@
 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
 qed "min_le_iff_disj";
-
+ **)
 
 (** LEAST -- the least number operator **)
 
@@ -624,8 +632,6 @@
 goalw thy [Least_def]
   "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
 by (simp_tac (simpset() addsimps [lemma]) 1);
-by (rtac eq_reflection 1);
-by (rtac refl 1);
 qed "Least_nat_def";
 
 val [prem1,prem2] = goalw thy [Least_nat_def]
diff -r bc6e2936a293 -r ac6cf9f18653 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Feb 20 17:33:14 1998 +0100
+++ b/src/HOL/Ord.ML	Fri Feb 20 17:56:39 1998 +0100
@@ -54,3 +54,38 @@
 by (Asm_simp_tac 1);
 by (blast_tac (claset() addIs [order_antisym]) 1);
 qed "min_leastR";
+
+
+section "Linear/Total Orders";
+
+goal thy "!!x::'a::linorder. x<y | x=y | y<x";
+by (simp_tac (simpset() addsimps [order_less_le]) 1);
+by(cut_facts_tac [linorder_linear] 1);
+by (Blast_tac 1);
+qed "linorder_less_linear";
+
+goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
+by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by(cut_facts_tac [linorder_linear] 1);
+by (blast_tac (claset() addIs [order_trans]) 1);
+qed "le_max_iff_disj";
+
+goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
+by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by(cut_facts_tac [linorder_linear] 1);
+by (blast_tac (claset() addIs [order_trans]) 1);
+qed "max_le_iff_conj";
+
+goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
+by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by(cut_facts_tac [linorder_linear] 1);
+by (blast_tac (claset() addIs [order_trans]) 1);
+qed "le_min_iff_conj";
+
+goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
+by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
+by(cut_facts_tac [linorder_linear] 1);
+by (blast_tac (claset() addIs [order_trans]) 1);
+qed "min_le_iff_disj";
+
+
diff -r bc6e2936a293 -r ac6cf9f18653 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Fri Feb 20 17:33:14 1998 +0100
+++ b/src/HOL/Ord.thy	Fri Feb 20 17:56:39 1998 +0100
@@ -45,4 +45,7 @@
   order_antisym "[| x <= y; y <= x |] ==> x = y"
   order_less_le "x < y = (x <= y & x ~= y)"
 
+axclass linorder < order
+  linorder_linear "x <= y | y <= x"
+
 end
diff -r bc6e2936a293 -r ac6cf9f18653 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Feb 20 17:33:14 1998 +0100
+++ b/src/HOL/simpdata.ML	Fri Feb 20 17:56:39 1998 +0100
@@ -52,6 +52,9 @@
 val DelIffs = seq delIff
 end;
 
+qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
+  (fn [prem] => [rewtac prem, rtac refl 1]);
+
 local
 
   fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]);
@@ -95,7 +98,7 @@
  [ "(x=x) = True",
    "(~True) = False", "(~False) = True", "(~ ~ P) = P",
    "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
-   "(True=P) = P", "(P=True) = P",
+   "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    "(True --> P) = P", "(False --> P) = True", 
    "(P --> True) = True", "(P --> P) = True",
    "(P --> False) = (~P)", "(P --> ~P) = (~P)",
@@ -115,11 +118,15 @@
 
 (*Add congruence rules for = (instead of ==) *)
 infix 4 addcongs delcongs;
-fun ss addcongs congs = ss addeqcongs 
-                        (map standard (congs RL [eq_reflection]));
 
-fun ss delcongs congs = ss deleqcongs 
-                        (map standard (congs RL [eq_reflection]));
+fun mk_meta_cong rl =
+  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+  handle THM _ =>
+  error("Premises and conclusion of congruence rules must be =-equalities");
+
+fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
+
+fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
 
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
@@ -241,9 +248,6 @@
 qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
  (K [rtac refl 1]);
 
-qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
-  (fn [prem] => [rewtac prem, rtac refl 1]);
-
 qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
  (K [Blast_tac 1]);
 
@@ -370,10 +374,10 @@
    ("All", [spec]), ("True", []), ("False", []),
    ("If", [if_bool_eq RS iffD1])];
 
-fun unsafe_solver prems = FIRST'[resolve_tac (TrueI::refl::prems),
+fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
 				 atac, etac FalseE];
 (*No premature instantiation of variables during simplification*)
-fun   safe_solver prems = FIRST'[match_tac (TrueI::refl::prems),
+fun   safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems),
 				 eq_assume_tac, ematch_tac [FalseE]];
 
 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac