Calculation.thy: Setup transitivity rules for calculational proofs.
authorwenzelm
Fri Jun 04 19:57:31 1999 +0200 (1999-06-04)
changeset 67792912aff958bd
parent 6778 2f66eea8a025
child 6780 769cea1985e4
Calculation.thy: Setup transitivity rules for calculational proofs.
src/HOL/Calculation.thy
src/HOL/IsaMakefile
src/HOL/Main.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Calculation.thy	Fri Jun 04 19:57:31 1999 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      HOL/Calculation.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Setup transitivity rules for calculational proofs.
     1.9 +*)
    1.10 +
    1.11 +theory Calculation = Int:
    1.12 +
    1.13 +
    1.14 +theorems[trans] = HOL.trans			(*  =  =  =  *)
    1.15 +theorems[trans] = HOL.ssubst                    (*  =  *  *  *)
    1.16 +theorems[trans] = HOL.subst[COMP swap_prems_rl]	(*  *  =  *  *)
    1.17 +
    1.18 +theorems[trans] = Ord.order_trans		(*  <= <= <= *)
    1.19 +theorems[trans] = Ord.order_less_trans		(*  <  <  <  *)
    1.20 +theorems[trans] = Ord.order_le_less_trans	(*  <= <  <  *)
    1.21 +theorems[trans] = Ord.order_less_le_trans	(*  <  <= <  *)
    1.22 +
    1.23 +theorems[trans] = Divides.dvd_trans		(* dvd dvd dvd *)
    1.24 +
    1.25 +
    1.26 +end
     2.1 --- a/src/HOL/IsaMakefile	Fri Jun 04 19:55:41 1999 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Jun 04 19:57:31 1999 +0200
     2.3 @@ -43,24 +43,24 @@
     2.4    $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
     2.5    $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
     2.6    $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
     2.7 -  Datatype.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
     2.8 -  Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
     2.9 -  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntDef.ML \
    2.10 -  Integ/IntDef.thy Integ/Int.ML Integ/Int.thy Integ/simproc.ML Lfp.ML \
    2.11 -  Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML Nat.thy \
    2.12 -  NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
    2.13 -  Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
    2.14 -  RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    2.15 -  String.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    2.16 -  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    2.17 -  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    2.18 -  Tools/induct_method.ML Tools/inductive_package.ML \
    2.19 -  Tools/primrec_package.ML Tools/recdef_package.ML \
    2.20 -  Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
    2.21 -  Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
    2.22 -  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
    2.23 -  hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
    2.24 -  thy_syntax.ML
    2.25 +  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
    2.26 +  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    2.27 +  Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \
    2.28 +  Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
    2.29 +  Integ/Int.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
    2.30 +  Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
    2.31 +  Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML \
    2.32 +  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    2.33 +  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    2.34 +  Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
    2.35 +  Tools/datatype_package.ML Tools/datatype_prop.ML \
    2.36 +  Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    2.37 +  Tools/inductive_package.ML Tools/primrec_package.ML \
    2.38 +  Tools/recdef_package.ML Tools/record_package.ML \
    2.39 +  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    2.40 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \
    2.41 +  equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \
    2.42 +  subset.ML subset.thy thy_syntax.ML
    2.43  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    2.44  
    2.45  
     3.1 --- a/src/HOL/Main.thy	Fri Jun 04 19:55:41 1999 +0200
     3.2 +++ b/src/HOL/Main.thy	Fri Jun 04 19:57:31 1999 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4  
     3.5  (*theory Main includes everything*)
     3.6  
     3.7 -Main = Bin + Map + Recdef + Record + RelPow + Sexp + String
     3.8 +Main = Bin + Map + Recdef + Record + RelPow + Sexp + String + Calculation