--- a/src/HOL/FixedPoint.thy Mon Nov 27 13:42:33 2006 +0100
+++ b/src/HOL/FixedPoint.thy Mon Nov 27 13:42:39 2006 +0100
@@ -120,30 +120,6 @@
subsubsection {* Booleans *}
-instance bool :: ord ..
-
-defs
- le_bool_def: "P <= Q == P \<longrightarrow> Q"
- less_bool_def: "P < Q == (P::bool) <= Q \<and> P \<noteq> Q"
-
-theorem le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P <= Q"
- by (simp add: le_bool_def)
-
-theorem le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P <= Q"
- by (simp add: le_bool_def)
-
-theorem le_boolE: "P <= Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
- by (simp add: le_bool_def)
-
-theorem le_boolD: "P <= Q \<Longrightarrow> P \<longrightarrow> Q"
- by (simp add: le_bool_def)
-
-instance bool :: order
- apply intro_classes
- apply (unfold le_bool_def less_bool_def)
- apply iprover+
- done
-
defs Meet_bool_def: "Meet A == ALL x:A. x"
instance bool :: comp_lat
@@ -201,21 +177,6 @@
subsubsection {* Functions *}
-instance "fun" :: (type, ord) ord ..
-
-defs
- le_fun_def: "f <= g == \<forall>x. f x <= g x"
- less_fun_def: "f < g == (f::'a\<Rightarrow>'b::ord) <= g \<and> f \<noteq> g"
-
-theorem le_funI: "(\<And>x. f x <= g x) \<Longrightarrow> f <= g"
- by (simp add: le_fun_def)
-
-theorem le_funE: "f <= g \<Longrightarrow> (f x <= g x \<Longrightarrow> P) \<Longrightarrow> P"
- by (simp add: le_fun_def)
-
-theorem le_funD: "f <= g \<Longrightarrow> f x <= g x"
- by (simp add: le_fun_def)
-
text {*
Handy introduction and elimination rules for @{text "\<le>"}
on unary and binary predicates
@@ -251,21 +212,6 @@
apply assumption+
done
-instance "fun" :: (type, order) order
- apply intro_classes
- apply (rule le_funI)
- apply (rule order_refl)
- apply (rule le_funI)
- apply (erule le_funE)+
- apply (erule order_trans)
- apply assumption
- apply (rule ext)
- apply (erule le_funE)+
- apply (erule order_antisym)
- apply assumption
- apply (simp add: less_fun_def)
- done
-
defs Meet_fun_def: "Meet A == (\<lambda>x. Meet {y. EX f:A. y = f x})"
instance "fun" :: (type, comp_lat) comp_lat
--- a/src/HOL/Fun.thy Mon Nov 27 13:42:33 2006 +0100
+++ b/src/HOL/Fun.thy Mon Nov 27 13:42:39 2006 +0100
@@ -452,7 +452,29 @@
lemma bij_swap_iff: "bij (swap a b f) = bij f"
by (simp add: bij_def)
-
+
+
+subsection {* Order on functions *}
+
+instance "fun" :: (type, order) order
+ le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
+ less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g"
+ by default
+ (auto simp add: le_fun_def less_fun_def intro: order_trans, rule ext, auto intro: order_antisym)
+
+lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
+ unfolding le_fun_def by simp
+
+lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
+ unfolding le_fun_def by simp
+
+lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
+ unfolding le_fun_def by simp
+
+instance "fun" :: (type, ord) ord ..
+
+
+subsection {* ML legacy bindings *}
text{*The ML section includes some compatibility bindings and a simproc
for function updates, in addition to the usual ML-bindings of theorems.*}
--- a/src/HOL/HOL.thy Mon Nov 27 13:42:33 2006 +0100
+++ b/src/HOL/HOL.thy Mon Nov 27 13:42:39 2006 +0100
@@ -805,61 +805,6 @@
subsection {* Package setup *}
-subsubsection {* Fundamental ML bindings *}
-
-ML {*
-structure HOL =
-struct
- (*FIXME reduce this to a minimum*)
- val eq_reflection = thm "eq_reflection";
- val def_imp_eq = thm "def_imp_eq";
- val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
- val ccontr = thm "ccontr";
- val impI = thm "impI";
- val impCE = thm "impCE";
- val notI = thm "notI";
- val notE = thm "notE";
- val iffI = thm "iffI";
- val iffCE = thm "iffCE";
- val conjI = thm "conjI";
- val conjE = thm "conjE";
- val disjCI = thm "disjCI";
- val disjE = thm "disjE";
- val TrueI = thm "TrueI";
- val FalseE = thm "FalseE";
- val allI = thm "allI";
- val allE = thm "allE";
- val exI = thm "exI";
- val exE = thm "exE";
- val ex_ex1I = thm "ex_ex1I";
- val the_equality = thm "the_equality";
- val mp = thm "mp";
- val rev_mp = thm "rev_mp"
- val classical = thm "classical";
- val subst = thm "subst";
- val refl = thm "refl";
- val sym = thm "sym";
- val trans = thm "trans";
- val arg_cong = thm "arg_cong";
- val iffD1 = thm "iffD1";
- val iffD2 = thm "iffD2";
- val disjE = thm "disjE";
- val conjE = thm "conjE";
- val exE = thm "exE";
- val contrapos_nn = thm "contrapos_nn";
- val contrapos_pp = thm "contrapos_pp";
- val notnotD = thm "notnotD";
- val conjunct1 = thm "conjunct1";
- val conjunct2 = thm "conjunct2";
- val spec = thm "spec";
- val imp_cong = thm "imp_cong";
- val the_sym_eq_trivial = thm "the_sym_eq_trivial";
- val triv_forall_equality = thm "triv_forall_equality";
- val case_split = thm "case_split_thm";
-end
-*}
-
-
subsubsection {* Classical Reasoner setup *}
lemma thin_refl:
@@ -872,20 +817,20 @@
val dest_eq = HOLogic.dest_eq
val dest_Trueprop = HOLogic.dest_Trueprop
val dest_imp = HOLogic.dest_imp
- val eq_reflection = HOL.eq_reflection
- val rev_eq_reflection = HOL.def_imp_eq
- val imp_intr = HOL.impI
- val rev_mp = HOL.rev_mp
- val subst = HOL.subst
- val sym = HOL.sym
+ val eq_reflection = thm "HOL.eq_reflection"
+ val rev_eq_reflection = thm "HOL.def_imp_eq"
+ val imp_intr = thm "HOL.impI"
+ val rev_mp = thm "HOL.rev_mp"
+ val subst = thm "HOL.subst"
+ val sym = thm "HOL.sym"
val thin_refl = thm "thin_refl";
end);
structure Classical = ClassicalFun(
struct
- val mp = HOL.mp
- val not_elim = HOL.notE
- val classical = HOL.classical
+ val mp = thm "HOL.mp"
+ val not_elim = thm "HOL.notE"
+ val classical = thm "HOL.classical"
val sizef = Drule.size_of_thm
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
end);
@@ -931,14 +876,7 @@
allE [elim]
ML {*
-structure HOL =
-struct
-
-open HOL;
-
-val claset = Classical.claset_of (the_context ());
-
-end;
+val HOL_cs = Classical.claset_of (the_context ());
*}
lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
@@ -959,8 +897,8 @@
shows R
apply (rule ex1E [OF major])
apply (rule prem)
-apply (tactic "ares_tac [HOL.allI] 1")+
-apply (tactic "etac (Classical.dup_elim HOL.allE) 1")
+apply (tactic {* ares_tac [thm "allI"] 1 *})+
+apply (tactic {* etac (Classical.dup_elim (thm "allE")) 1 *})
by iprover
ML {*
@@ -969,8 +907,8 @@
type claset = Classical.claset
val equality_name = "op ="
val not_name = "Not"
- val notE = HOL.notE
- val ccontr = HOL.ccontr
+ val notE = thm "HOL.notE"
+ val ccontr = thm "HOL.ccontr"
val contr_tac = Classical.contr_tac
val dup_intr = Classical.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
@@ -979,60 +917,6 @@
val cla_modifiers = Classical.cla_modifiers
val cla_meth' = Classical.cla_meth'
end);
-
-structure HOL =
-struct
-
-open HOL;
-
-val Blast_tac = Blast.Blast_tac;
-val blast_tac = Blast.blast_tac;
-
-fun case_tac a = res_inst_tac [("P", a)] case_split;
-
-(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
-local
- fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
- | wrong_prem (Bound _) = true
- | wrong_prem _ = false;
- val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
-in
- fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
- fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
-end;
-
-fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
-
-fun Trueprop_conv conv ct = (case term_of ct of
- Const ("Trueprop", _) $ _ =>
- let val (ct1, ct2) = Thm.dest_comb ct
- in Thm.combination (Thm.reflexive ct1) (conv ct2) end
- | _ => raise TERM ("Trueprop_conv", []));
-
-fun Equals_conv conv ct = (case term_of ct of
- Const ("op =", _) $ _ $ _ =>
- let
- val ((ct1, ct2), ct3) = (apfst Thm.dest_comb o Thm.dest_comb) ct;
- in Thm.combination (Thm.combination (Thm.reflexive ct1) (conv ct2)) (conv ct3) end
- | _ => conv ct);
-
-fun constrain_op_eq_thms thy thms =
- let
- fun add_eq (Const ("op =", ty)) =
- fold (insert (eq_fst (op =)))
- (Term.add_tvarsT ty [])
- | add_eq _ =
- I
- val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
- val instT = map (fn (v_i, sort) =>
- (Thm.ctyp_of thy (TVar (v_i, sort)),
- Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs;
- in
- thms
- |> map (Thm.instantiate (instT, []))
- end;
-
-end;
*}
setup Blast.setup
@@ -1298,7 +1182,7 @@
use "simpdata.ML"
setup {*
Simplifier.method_setup Splitter.split_modifiers
- #> (fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy))
+ #> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy))
#> Splitter.setup
#> Clasimp.setup
#> EqSubst.setup
@@ -1366,14 +1250,7 @@
and split_if [split]
ML {*
-structure HOL =
-struct
-
-open HOL;
-
-val simpset = Simplifier.simpset_of (the_context ());
-
-end;
+val HOL_ss = Simplifier.simpset_of (the_context ());
*}
text {* Simplifies x assuming c and y assuming ~c *}
@@ -1407,20 +1284,6 @@
"f (if c then x else y) = (if c then f x else f y)"
by simp
-text {* For @{text expand_case_tac} *}
-lemma expand_case:
- assumes "P \<Longrightarrow> Q True"
- and "~P \<Longrightarrow> Q False"
- shows "Q P"
-proof (tactic {* HOL.case_tac "P" 1 *})
- assume P
- then show "Q P" by simp
-next
- assume "\<not> P"
- then have "P = False" by simp
- with prems show "Q P" by simp
-qed
-
text {* This lemma restricts the effect of the rewrite rule u=v to the left-hand
side of an equality. Used in @{text "{Integ,Real}/simproc.ML"} *}
lemma restrict_to_left:
@@ -1529,11 +1392,11 @@
apply (drule_tac [3] x = x in fun_cong, simp_all)
done
-text {* Needs only HOL-lemmas *}
lemma mk_left_commute:
- assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and
- c: "\<And>x y. f x y = f y x"
- shows "f x (f y z) = f y (f x z)"
+ fixes f (infix "\<otimes>" 60)
+ assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
+ c: "\<And>x y. x \<otimes> y = y \<otimes> x"
+ shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
end