theory Calculation move to Set;
authorwenzelm
Fri Nov 02 22:01:58 2001 +0100 (2001-11-02)
changeset 12020a24373086908
parent 12019 abe9b7c6016e
child 12021 8809efda06d3
theory Calculation move to Set;
src/HOL/IsaMakefile
src/HOL/PreList.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Nov 02 22:01:07 2001 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Nov 02 22:01:58 2001 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4    $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \
     1.5    $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
     1.6    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
     1.7 -  $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
     1.8 +  $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
     1.9    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
    1.10    Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
    1.11    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
     2.1 --- a/src/HOL/PreList.thy	Fri Nov 02 22:01:07 2001 +0100
     2.2 +++ b/src/HOL/PreList.thy	Fri Nov 02 22:01:58 2001 +0100
     2.3 @@ -9,7 +9,10 @@
     2.4  
     2.5  theory PreList =
     2.6    Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
     2.7 -  Relation_Power + Calculation + SVC_Oracle:
     2.8 +  Relation_Power + SVC_Oracle:
     2.9 +
    2.10 +(*belongs to theory Divides*)
    2.11 +declare dvd_trans [trans]
    2.12  
    2.13  (*belongs to theory Wellfounded_Recursion*)
    2.14  declare wf_induct [induct set: wf]
     3.1 --- a/src/HOL/Set.thy	Fri Nov 02 22:01:07 2001 +0100
     3.2 +++ b/src/HOL/Set.thy	Fri Nov 02 22:01:58 2001 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      HOL/Set.thy
     3.5      ID:         $Id$
     3.6 -    Author:     Tobias Nipkow
     3.7 -    Copyright   1993  University of Cambridge
     3.8 +    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    3.10  *)
    3.11  
    3.12  header {* Set theory for higher-order logic *}
    3.13 @@ -575,7 +575,7 @@
    3.14    by (unfold Un_def) blast
    3.15  
    3.16  
    3.17 -section {* Binary intersection -- Int *}
    3.18 +subsection {* Binary intersection -- Int *}
    3.19  
    3.20  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    3.21    by (unfold Int_def) blast
    3.22 @@ -593,7 +593,7 @@
    3.23    by simp
    3.24  
    3.25  
    3.26 -section {* Set difference *}
    3.27 +subsection {* Set difference *}
    3.28  
    3.29  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
    3.30    by (unfold set_diff_def) blast
    3.31 @@ -904,4 +904,185 @@
    3.32    apply (auto elim: monoD intro!: order_antisym)
    3.33    done
    3.34  
    3.35 +
    3.36 +section {* Transitivity rules for calculational reasoning *}
    3.37 +
    3.38 +lemma forw_subst: "a = b ==> P b ==> P a"
    3.39 +  by (rule ssubst)
    3.40 +
    3.41 +lemma back_subst: "P a ==> a = b ==> P b"
    3.42 +  by (rule subst)
    3.43 +
    3.44 +lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
    3.45 +  by (rule subsetD)
    3.46 +
    3.47 +lemma set_mp: "A <= B ==> x:A ==> x:B"
    3.48 +  by (rule subsetD)
    3.49 +
    3.50 +lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
    3.51 +  by (simp add: order_less_le)
    3.52 +
    3.53 +lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
    3.54 +  by (simp add: order_less_le)
    3.55 +
    3.56 +lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
    3.57 +  by (rule order_less_asym)
    3.58 +
    3.59 +lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
    3.60 +  by (rule subst)
    3.61 +
    3.62 +lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
    3.63 +  by (rule ssubst)
    3.64 +
    3.65 +lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
    3.66 +  by (rule subst)
    3.67 +
    3.68 +lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
    3.69 +  by (rule ssubst)
    3.70 +
    3.71 +lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
    3.72 +  (!!x y. x < y ==> f x < f y) ==> f a < c"
    3.73 +proof -
    3.74 +  assume r: "!!x y. x < y ==> f x < f y"
    3.75 +  assume "a < b" hence "f a < f b" by (rule r)
    3.76 +  also assume "f b < c"
    3.77 +  finally (order_less_trans) show ?thesis .
    3.78 +qed
    3.79 +
    3.80 +lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
    3.81 +  (!!x y. x < y ==> f x < f y) ==> a < f c"
    3.82 +proof -
    3.83 +  assume r: "!!x y. x < y ==> f x < f y"
    3.84 +  assume "a < f b"
    3.85 +  also assume "b < c" hence "f b < f c" by (rule r)
    3.86 +  finally (order_less_trans) show ?thesis .
    3.87 +qed
    3.88 +
    3.89 +lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
    3.90 +  (!!x y. x <= y ==> f x <= f y) ==> f a < c"
    3.91 +proof -
    3.92 +  assume r: "!!x y. x <= y ==> f x <= f y"
    3.93 +  assume "a <= b" hence "f a <= f b" by (rule r)
    3.94 +  also assume "f b < c"
    3.95 +  finally (order_le_less_trans) show ?thesis .
    3.96 +qed
    3.97 +
    3.98 +lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
    3.99 +  (!!x y. x < y ==> f x < f y) ==> a < f c"
   3.100 +proof -
   3.101 +  assume r: "!!x y. x < y ==> f x < f y"
   3.102 +  assume "a <= f b"
   3.103 +  also assume "b < c" hence "f b < f c" by (rule r)
   3.104 +  finally (order_le_less_trans) show ?thesis .
   3.105 +qed
   3.106 +
   3.107 +lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
   3.108 +  (!!x y. x < y ==> f x < f y) ==> f a < c"
   3.109 +proof -
   3.110 +  assume r: "!!x y. x < y ==> f x < f y"
   3.111 +  assume "a < b" hence "f a < f b" by (rule r)
   3.112 +  also assume "f b <= c"
   3.113 +  finally (order_less_le_trans) show ?thesis .
   3.114 +qed
   3.115 +
   3.116 +lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
   3.117 +  (!!x y. x <= y ==> f x <= f y) ==> a < f c"
   3.118 +proof -
   3.119 +  assume r: "!!x y. x <= y ==> f x <= f y"
   3.120 +  assume "a < f b"
   3.121 +  also assume "b <= c" hence "f b <= f c" by (rule r)
   3.122 +  finally (order_less_le_trans) show ?thesis .
   3.123 +qed
   3.124 +
   3.125 +lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
   3.126 +  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
   3.127 +proof -
   3.128 +  assume r: "!!x y. x <= y ==> f x <= f y"
   3.129 +  assume "a <= f b"
   3.130 +  also assume "b <= c" hence "f b <= f c" by (rule r)
   3.131 +  finally (order_trans) show ?thesis .
   3.132 +qed
   3.133 +
   3.134 +lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
   3.135 +  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
   3.136 +proof -
   3.137 +  assume r: "!!x y. x <= y ==> f x <= f y"
   3.138 +  assume "a <= b" hence "f a <= f b" by (rule r)
   3.139 +  also assume "f b <= c"
   3.140 +  finally (order_trans) show ?thesis .
   3.141 +qed
   3.142 +
   3.143 +lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
   3.144 +  (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
   3.145 +proof -
   3.146 +  assume r: "!!x y. x <= y ==> f x <= f y"
   3.147 +  assume "a <= b" hence "f a <= f b" by (rule r)
   3.148 +  also assume "f b = c"
   3.149 +  finally (ord_le_eq_trans) show ?thesis .
   3.150 +qed
   3.151 +
   3.152 +lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
   3.153 +  (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
   3.154 +proof -
   3.155 +  assume r: "!!x y. x <= y ==> f x <= f y"
   3.156 +  assume "a = f b"
   3.157 +  also assume "b <= c" hence "f b <= f c" by (rule r)
   3.158 +  finally (ord_eq_le_trans) show ?thesis .
   3.159 +qed
   3.160 +
   3.161 +lemma ord_less_eq_subst: "a < b ==> f b = c ==>
   3.162 +  (!!x y. x < y ==> f x < f y) ==> f a < c"
   3.163 +proof -
   3.164 +  assume r: "!!x y. x < y ==> f x < f y"
   3.165 +  assume "a < b" hence "f a < f b" by (rule r)
   3.166 +  also assume "f b = c"
   3.167 +  finally (ord_less_eq_trans) show ?thesis .
   3.168 +qed
   3.169 +
   3.170 +lemma ord_eq_less_subst: "a = f b ==> b < c ==>
   3.171 +  (!!x y. x < y ==> f x < f y) ==> a < f c"
   3.172 +proof -
   3.173 +  assume r: "!!x y. x < y ==> f x < f y"
   3.174 +  assume "a = f b"
   3.175 +  also assume "b < c" hence "f b < f c" by (rule r)
   3.176 +  finally (ord_eq_less_trans) show ?thesis .
   3.177 +qed
   3.178 +
   3.179 +text {*
   3.180 +  Note that this list of rules is in reverse order of priorities.
   3.181 +*}
   3.182 +
   3.183 +lemmas basic_trans_rules [trans] =
   3.184 +  order_less_subst2
   3.185 +  order_less_subst1
   3.186 +  order_le_less_subst2
   3.187 +  order_le_less_subst1
   3.188 +  order_less_le_subst2
   3.189 +  order_less_le_subst1
   3.190 +  order_subst2
   3.191 +  order_subst1
   3.192 +  ord_le_eq_subst
   3.193 +  ord_eq_le_subst
   3.194 +  ord_less_eq_subst
   3.195 +  ord_eq_less_subst
   3.196 +  forw_subst
   3.197 +  back_subst
   3.198 +  rev_mp
   3.199 +  mp
   3.200 +  set_rev_mp
   3.201 +  set_mp
   3.202 +  order_neq_le_trans
   3.203 +  order_le_neq_trans
   3.204 +  order_less_trans
   3.205 +  order_less_asym'
   3.206 +  order_le_less_trans
   3.207 +  order_less_le_trans
   3.208 +  order_trans
   3.209 +  order_antisym
   3.210 +  ord_le_eq_trans
   3.211 +  ord_eq_le_trans
   3.212 +  ord_less_eq_trans
   3.213 +  ord_eq_less_trans
   3.214 +  trans
   3.215 +
   3.216  end