Congruence rules use == in premises now.
authornipkow
Fri Feb 20 17:56:39 1998 +0100 (1998-02-20)
changeset 4640ac6cf9f18653
parent 4639 bc6e2936a293
child 4641 70a50c2a920f
Congruence rules use == in premises now.
New class linord.
src/HOL/Nat.thy
src/HOL/NatDef.ML
src/HOL/Ord.ML
src/HOL/Ord.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Nat.thy	Fri Feb 20 17:33:14 1998 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Feb 20 17:56:39 1998 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4  
     1.5  
     1.6  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
     1.7 +instance nat :: linorder (nat_le_linear)
     1.8  
     1.9  consts
    1.10    "^"           :: ['a::power,nat] => 'a            (infixr 80)
     2.1 --- a/src/HOL/NatDef.ML	Fri Feb 20 17:33:14 1998 +0100
     2.2 +++ b/src/HOL/NatDef.ML	Fri Feb 20 17:56:39 1998 +0100
     2.3 @@ -588,7 +588,15 @@
     2.4  by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
     2.5  qed "nat_less_le";
     2.6  
     2.7 -(** max **)
     2.8 +(* Axiom 'linorder_linear' of class 'linorder': *)
     2.9 +goal thy "(m::nat) <= n | n <= m";
    2.10 +by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    2.11 +by (cut_facts_tac [less_linear] 1);
    2.12 +by(Blast_tac 1);
    2.13 +qed "nat_le_linear";
    2.14 +
    2.15 +
    2.16 +(** max
    2.17  
    2.18  goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
    2.19  by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
    2.20 @@ -612,7 +620,7 @@
    2.21  by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
    2.22  by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
    2.23  qed "min_le_iff_disj";
    2.24 -
    2.25 + **)
    2.26  
    2.27  (** LEAST -- the least number operator **)
    2.28  
    2.29 @@ -624,8 +632,6 @@
    2.30  goalw thy [Least_def]
    2.31    "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
    2.32  by (simp_tac (simpset() addsimps [lemma]) 1);
    2.33 -by (rtac eq_reflection 1);
    2.34 -by (rtac refl 1);
    2.35  qed "Least_nat_def";
    2.36  
    2.37  val [prem1,prem2] = goalw thy [Least_nat_def]
     3.1 --- a/src/HOL/Ord.ML	Fri Feb 20 17:33:14 1998 +0100
     3.2 +++ b/src/HOL/Ord.ML	Fri Feb 20 17:56:39 1998 +0100
     3.3 @@ -54,3 +54,38 @@
     3.4  by (Asm_simp_tac 1);
     3.5  by (blast_tac (claset() addIs [order_antisym]) 1);
     3.6  qed "min_leastR";
     3.7 +
     3.8 +
     3.9 +section "Linear/Total Orders";
    3.10 +
    3.11 +goal thy "!!x::'a::linorder. x<y | x=y | y<x";
    3.12 +by (simp_tac (simpset() addsimps [order_less_le]) 1);
    3.13 +by(cut_facts_tac [linorder_linear] 1);
    3.14 +by (Blast_tac 1);
    3.15 +qed "linorder_less_linear";
    3.16 +
    3.17 +goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
    3.18 +by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
    3.19 +by(cut_facts_tac [linorder_linear] 1);
    3.20 +by (blast_tac (claset() addIs [order_trans]) 1);
    3.21 +qed "le_max_iff_disj";
    3.22 +
    3.23 +goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
    3.24 +by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
    3.25 +by(cut_facts_tac [linorder_linear] 1);
    3.26 +by (blast_tac (claset() addIs [order_trans]) 1);
    3.27 +qed "max_le_iff_conj";
    3.28 +
    3.29 +goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
    3.30 +by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
    3.31 +by(cut_facts_tac [linorder_linear] 1);
    3.32 +by (blast_tac (claset() addIs [order_trans]) 1);
    3.33 +qed "le_min_iff_conj";
    3.34 +
    3.35 +goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
    3.36 +by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
    3.37 +by(cut_facts_tac [linorder_linear] 1);
    3.38 +by (blast_tac (claset() addIs [order_trans]) 1);
    3.39 +qed "min_le_iff_disj";
    3.40 +
    3.41 +
     4.1 --- a/src/HOL/Ord.thy	Fri Feb 20 17:33:14 1998 +0100
     4.2 +++ b/src/HOL/Ord.thy	Fri Feb 20 17:56:39 1998 +0100
     4.3 @@ -45,4 +45,7 @@
     4.4    order_antisym "[| x <= y; y <= x |] ==> x = y"
     4.5    order_less_le "x < y = (x <= y & x ~= y)"
     4.6  
     4.7 +axclass linorder < order
     4.8 +  linorder_linear "x <= y | y <= x"
     4.9 +
    4.10  end
     5.1 --- a/src/HOL/simpdata.ML	Fri Feb 20 17:33:14 1998 +0100
     5.2 +++ b/src/HOL/simpdata.ML	Fri Feb 20 17:56:39 1998 +0100
     5.3 @@ -52,6 +52,9 @@
     5.4  val DelIffs = seq delIff
     5.5  end;
     5.6  
     5.7 +qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
     5.8 +  (fn [prem] => [rewtac prem, rtac refl 1]);
     5.9 +
    5.10  local
    5.11  
    5.12    fun prover s = prove_goal HOL.thy s (K [blast_tac HOL_cs 1]);
    5.13 @@ -95,7 +98,7 @@
    5.14   [ "(x=x) = True",
    5.15     "(~True) = False", "(~False) = True", "(~ ~ P) = P",
    5.16     "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    5.17 -   "(True=P) = P", "(P=True) = P",
    5.18 +   "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    5.19     "(True --> P) = P", "(False --> P) = True", 
    5.20     "(P --> True) = True", "(P --> P) = True",
    5.21     "(P --> False) = (~P)", "(P --> ~P) = (~P)",
    5.22 @@ -115,11 +118,15 @@
    5.23  
    5.24  (*Add congruence rules for = (instead of ==) *)
    5.25  infix 4 addcongs delcongs;
    5.26 -fun ss addcongs congs = ss addeqcongs 
    5.27 -                        (map standard (congs RL [eq_reflection]));
    5.28  
    5.29 -fun ss delcongs congs = ss deleqcongs 
    5.30 -                        (map standard (congs RL [eq_reflection]));
    5.31 +fun mk_meta_cong rl =
    5.32 +  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
    5.33 +  handle THM _ =>
    5.34 +  error("Premises and conclusion of congruence rules must be =-equalities");
    5.35 +
    5.36 +fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs);
    5.37 +
    5.38 +fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs);
    5.39  
    5.40  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
    5.41  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    5.42 @@ -241,9 +248,6 @@
    5.43  qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
    5.44   (K [rtac refl 1]);
    5.45  
    5.46 -qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
    5.47 -  (fn [prem] => [rewtac prem, rtac refl 1]);
    5.48 -
    5.49  qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
    5.50   (K [Blast_tac 1]);
    5.51  
    5.52 @@ -370,10 +374,10 @@
    5.53     ("All", [spec]), ("True", []), ("False", []),
    5.54     ("If", [if_bool_eq RS iffD1])];
    5.55  
    5.56 -fun unsafe_solver prems = FIRST'[resolve_tac (TrueI::refl::prems),
    5.57 +fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
    5.58  				 atac, etac FalseE];
    5.59  (*No premature instantiation of variables during simplification*)
    5.60 -fun   safe_solver prems = FIRST'[match_tac (TrueI::refl::prems),
    5.61 +fun   safe_solver prems = FIRST'[match_tac (reflexive_thm::TrueI::prems),
    5.62  				 eq_assume_tac, ematch_tac [FalseE]];
    5.63  
    5.64  val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac