# HG changeset patch # User haftmann # Date 1164631359 -3600 # Node ID 9c9fdf4c2949bcf718d0be5ee0b77a6da64e1b3f # Parent 268b6bed0cc87ef31fe9d096ac32e40ceebabb29 moved order arities for fun and bool to Fun/Orderings diff -r 268b6bed0cc8 -r 9c9fdf4c2949 src/HOL/FixedPoint.thy --- 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 \ Q" - less_bool_def: "P < Q == (P::bool) <= Q \ P \ Q" - -theorem le_boolI: "(P \ Q) \ P <= Q" - by (simp add: le_bool_def) - -theorem le_boolI': "P \ Q \ P <= Q" - by (simp add: le_bool_def) - -theorem le_boolE: "P <= Q \ P \ (Q \ R) \ R" - by (simp add: le_bool_def) - -theorem le_boolD: "P <= Q \ P \ 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 == \x. f x <= g x" - less_fun_def: "f < g == (f::'a\'b::ord) <= g \ f \ g" - -theorem le_funI: "(\x. f x <= g x) \ f <= g" - by (simp add: le_fun_def) - -theorem le_funE: "f <= g \ (f x <= g x \ P) \ P" - by (simp add: le_fun_def) - -theorem le_funD: "f <= g \ f x <= g x" - by (simp add: le_fun_def) - text {* Handy introduction and elimination rules for @{text "\"} 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 == (\x. Meet {y. EX f:A. y = f x})" instance "fun" :: (type, comp_lat) comp_lat diff -r 268b6bed0cc8 -r 9c9fdf4c2949 src/HOL/Fun.thy --- 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 \ g \ \x. f x \ g x" + less_fun_def: "f < g \ f \ g \ f \ g" + by default + (auto simp add: le_fun_def less_fun_def intro: order_trans, rule ext, auto intro: order_antisym) + +lemma le_funI: "(\x. f x \ g x) \ f \ g" + unfolding le_fun_def by simp + +lemma le_funE: "f \ g \ (f x \ g x \ P) \ P" + unfolding le_fun_def by simp + +lemma le_funD: "f \ g \ f x \ 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.*} diff -r 268b6bed0cc8 -r 9c9fdf4c2949 src/HOL/HOL.thy --- 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 \ Q True" - and "~P \ Q False" - shows "Q P" -proof (tactic {* HOL.case_tac "P" 1 *}) - assume P - then show "Q P" by simp -next - assume "\ 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: "\x y z. f (f x y) z = f x (f y z)" and - c: "\x y. f x y = f y x" - shows "f x (f y z) = f y (f x z)" + fixes f (infix "\" 60) + assumes a: "\x y z. (x \ y) \ z = x \ (y \ z)" and + c: "\x y. x \ y = y \ x" + shows "x \ (y \ z) = y \ (x \ z)" by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]]) end