# HG changeset patch # User paulson # Date 1103274946 -3600 # Node ID e28853da5df5852d5edcf566d61d8673f49bd059 # Parent b488b290eccb0f238daf44206c86ff719e0bf9c5 removed two looping simplifications in SetInterval.thy; deleted the .ML file diff -r b488b290eccb -r e28853da5df5 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Dec 17 10:15:10 2004 +0100 +++ b/src/HOL/IsaMakefile Fri Dec 17 10:15:46 2004 +0100 @@ -95,7 +95,7 @@ Refute.thy ROOT.ML \ Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \ Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\ - Set.ML Set.thy SetInterval.ML SetInterval.thy \ + Set.ML Set.thy SetInterval.thy \ Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \ Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \ diff -r b488b290eccb -r e28853da5df5 src/HOL/SetInterval.ML --- a/src/HOL/SetInterval.ML Fri Dec 17 10:15:10 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,55 +0,0 @@ -(* Title: HOL/SetInterval.ML - ID: $Id$ - Author: Clemens Ballarin - Copyright 2002 TU Muenchen -*) - -(* Legacy ML bindings *) - -val Compl_atLeast = thm "Compl_atLeast"; -val Compl_atMost = thm "Compl_atMost"; -val Compl_greaterThan = thm "Compl_greaterThan"; -val Compl_lessThan = thm "Compl_lessThan"; -val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV"; -val UN_atLeast_UNIV = thm "UN_atLeast_UNIV"; -val UN_atMost_UNIV = thm "UN_atMost_UNIV"; -val UN_lessThan_UNIV = thm "UN_lessThan_UNIV"; -val atLeastAtMost_def = thm "atLeastAtMost_def"; -val atLeastAtMost_iff = thm "atLeastAtMost_iff"; -val atLeastLessThan_def = thm "atLeastLessThan_def"; -val atLeastLessThan_iff = thm "atLeastLessThan_iff"; -val atLeast_0 = thm "atLeast_0"; -val atLeast_Suc = thm "atLeast_Suc"; -val atLeast_def = thm "atLeast_def"; -val atLeast_iff = thm "atLeast_iff"; -val atMost_0 = thm "atMost_0"; -val atMost_Int_atLeast = thm "atMost_Int_atLeast"; -val atMost_Suc = thm "atMost_Suc"; -val atMost_def = thm "atMost_def"; -val atMost_iff = thm "atMost_iff"; -val greaterThanAtMost_def = thm "greaterThanAtMost_def"; -val greaterThanAtMost_iff = thm "greaterThanAtMost_iff"; -val greaterThanLessThan_def = thm "greaterThanLessThan_def"; -val greaterThanLessThan_iff = thm "greaterThanLessThan_iff"; -val greaterThan_0 = thm "greaterThan_0"; -val greaterThan_Suc = thm "greaterThan_Suc"; -val greaterThan_def = thm "greaterThan_def"; -val greaterThan_iff = thm "greaterThan_iff"; -val ivl_disj_int = thms "ivl_disj_int"; -val ivl_disj_int_one = thms "ivl_disj_int_one"; -val ivl_disj_int_singleton = thms "ivl_disj_int_singleton"; -val ivl_disj_int_two = thms "ivl_disj_int_two"; -val ivl_disj_un = thms "ivl_disj_un"; -val ivl_disj_un_one = thms "ivl_disj_un_one"; -val ivl_disj_un_singleton = thms "ivl_disj_un_singleton"; -val ivl_disj_un_two = thms "ivl_disj_un_two"; -val lessThan_0 = thm "lessThan_0"; -val lessThan_Suc = thm "lessThan_Suc"; -val lessThan_Suc_atMost = thm "lessThan_Suc_atMost"; -val lessThan_def = thm "lessThan_def"; -val lessThan_iff = thm "lessThan_iff"; -val single_Diff_lessThan = thm "single_Diff_lessThan"; - -val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite"; -val finite_atMost = thm "finite_atMost"; -val finite_lessThan = thm "finite_lessThan"; diff -r b488b290eccb -r e28853da5df5 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Fri Dec 17 10:15:10 2004 +0100 +++ b/src/HOL/SetInterval.thy Fri Dec 17 10:15:46 2004 +0100 @@ -87,7 +87,7 @@ lemma lessThan_iff [iff]: "(i: lessThan k) = (i atLeast y) = (y \ (x::'a::order))" -by (blast intro: order_trans) + "(atLeast x \ atLeast y) = (y \ (x::'a::order))" +by (blast intro: order_trans) lemma atLeast_eq_iff [iff]: - "(atLeast x = atLeast y) = (x = (y::'a::linorder))" + "(atLeast x = atLeast y) = (x = (y::'a::linorder))" by (blast intro: order_antisym order_trans) lemma greaterThan_subset_iff [iff]: - "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" -apply (auto simp add: greaterThan_def) - apply (subst linorder_not_less [symmetric], blast) + "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" +apply (auto simp add: greaterThan_def) + apply (subst linorder_not_less [symmetric], blast) done lemma greaterThan_eq_iff [iff]: - "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" -apply (rule iffI) - apply (erule equalityE) - apply (simp add: greaterThan_subset_iff order_antisym, simp) + "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" +apply (rule iffI) + apply (erule equalityE) + apply (simp_all add: greaterThan_subset_iff) done -lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))" +lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::order))" by (blast intro: order_trans) -lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" +lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" by (blast intro: order_antisym order_trans) lemma lessThan_subset_iff [iff]: - "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" -apply (auto simp add: lessThan_def) - apply (subst linorder_not_less [symmetric], blast) + "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" +apply (auto simp add: lessThan_def) + apply (subst linorder_not_less [symmetric], blast) done lemma lessThan_eq_iff [iff]: - "(lessThan x = lessThan y) = (x = (y::'a::linorder))" -apply (rule iffI) - apply (erule equalityE) - apply (simp add: lessThan_subset_iff order_antisym, simp) + "(lessThan x = lessThan y) = (x = (y::'a::linorder))" +apply (rule iffI) + apply (erule equalityE) + apply (simp_all add: lessThan_subset_iff) done @@ -279,9 +279,9 @@ text{*Not a simprule because the RHS is too messy.*} lemma atLeastLessThanSuc: "{m.. n then insert n {m.. u ==> +lemma image_atLeastZeroLessThan_int: "0 \ u ==> {(0::int)..i < Suc n. b i) = b n + (\i < n. b i)" by (simp add:lessThan_Suc) + +ML +{* +val Compl_atLeast = thm "Compl_atLeast"; +val Compl_atMost = thm "Compl_atMost"; +val Compl_greaterThan = thm "Compl_greaterThan"; +val Compl_lessThan = thm "Compl_lessThan"; +val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV"; +val UN_atLeast_UNIV = thm "UN_atLeast_UNIV"; +val UN_atMost_UNIV = thm "UN_atMost_UNIV"; +val UN_lessThan_UNIV = thm "UN_lessThan_UNIV"; +val atLeastAtMost_def = thm "atLeastAtMost_def"; +val atLeastAtMost_iff = thm "atLeastAtMost_iff"; +val atLeastLessThan_def = thm "atLeastLessThan_def"; +val atLeastLessThan_iff = thm "atLeastLessThan_iff"; +val atLeast_0 = thm "atLeast_0"; +val atLeast_Suc = thm "atLeast_Suc"; +val atLeast_def = thm "atLeast_def"; +val atLeast_iff = thm "atLeast_iff"; +val atMost_0 = thm "atMost_0"; +val atMost_Int_atLeast = thm "atMost_Int_atLeast"; +val atMost_Suc = thm "atMost_Suc"; +val atMost_def = thm "atMost_def"; +val atMost_iff = thm "atMost_iff"; +val greaterThanAtMost_def = thm "greaterThanAtMost_def"; +val greaterThanAtMost_iff = thm "greaterThanAtMost_iff"; +val greaterThanLessThan_def = thm "greaterThanLessThan_def"; +val greaterThanLessThan_iff = thm "greaterThanLessThan_iff"; +val greaterThan_0 = thm "greaterThan_0"; +val greaterThan_Suc = thm "greaterThan_Suc"; +val greaterThan_def = thm "greaterThan_def"; +val greaterThan_iff = thm "greaterThan_iff"; +val ivl_disj_int = thms "ivl_disj_int"; +val ivl_disj_int_one = thms "ivl_disj_int_one"; +val ivl_disj_int_singleton = thms "ivl_disj_int_singleton"; +val ivl_disj_int_two = thms "ivl_disj_int_two"; +val ivl_disj_un = thms "ivl_disj_un"; +val ivl_disj_un_one = thms "ivl_disj_un_one"; +val ivl_disj_un_singleton = thms "ivl_disj_un_singleton"; +val ivl_disj_un_two = thms "ivl_disj_un_two"; +val lessThan_0 = thm "lessThan_0"; +val lessThan_Suc = thm "lessThan_Suc"; +val lessThan_Suc_atMost = thm "lessThan_Suc_atMost"; +val lessThan_def = thm "lessThan_def"; +val lessThan_iff = thm "lessThan_iff"; +val single_Diff_lessThan = thm "single_Diff_lessThan"; + +val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite"; +val finite_atMost = thm "finite_atMost"; +val finite_lessThan = thm "finite_lessThan"; +*} + end