# HG changeset patch # User haftmann # Date 1160469324 -7200 # Node ID 34b2c1bb7178dc6c54b648860cc1bae9cb79915a # Parent cf19faf11bbdc4b769a1049e2f4beb3326c60128 cleanup basic HOL bootstrap diff -r cf19faf11bbd -r 34b2c1bb7178 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Tue Oct 10 10:34:43 2006 +0200 +++ b/src/HOL/HOL.ML Tue Oct 10 10:35:24 2006 +0200 @@ -1,30 +1,132 @@ (* legacy ML bindings *) -val choice_eq = thm "choice_eq"; +open HOL; -structure HOL = -struct - val eq_reflection = eq_reflection; - val refl = refl; - val subst = subst; - val ext = ext; - val impI = impI; - val mp = mp; - val True_def = True_def; - val All_def = All_def; - val Ex_def = Ex_def; - val False_def = False_def; - val not_def = not_def; - val and_def = and_def; - val or_def = or_def; - val Ex1_def = Ex1_def; - val iff = iff; - val True_or_False = True_or_False; - val Let_def = Let_def; - val if_def = if_def; -end; - -open HOL; +val ext = thm "ext" +val True_def = thm "True_def" +val All_def = thm "All_def" +val Ex_def = thm "Ex_def" +val False_def = thm "False_def" +val not_def = thm "not_def" +val and_def = thm "and_def" +val or_def = thm "or_def" +val Ex1_def = thm "Ex1_def" +val iff = thm "iff" +val True_or_False = thm "True_or_False" +val Let_def = thm "Let_def" +val if_def = thm "if_def" +val ssubst = thm "ssubst" +val box_equals = thm "box_equals" +val fun_cong = thm "fun_cong" +val cong = thm "cong" +val rev_iffD2 = thm "rev_iffD2" +val rev_iffD1 = thm "rev_iffD1" +val iffE = thm "iffE" +val eqTrueI = thm "eqTrueI" +val eqTrueE = thm "eqTrueE" +val all_dupE = thm "all_dupE" +val FalseE = thm "FalseE" +val False_neq_True = thm "False_neq_True" +val False_not_True = thm "False_not_True" +val True_not_False = thm "True_not_False" +val notI2 = thm "notI2" +val impE = thm "impE" +val not_sym = thm "not_sym" +val rev_contrapos = thm "rev_contrapos" +val conjE = thm "conjE" +val context_conjI = thm "context_conjI" +val disjI1 = thm "disjI1" +val disjI2 = thm "disjI2" +val rev_notE = thm "rev_notE" +val ex1I = thm "ex1I" +val ex1E = thm "ex1E" +val ex1_implies_ex = thm "ex1_implies_ex" +val the_equality = thm "the_equality" +val theI = thm "theI" +val theI' = thm "theI'" +val theI2 = thm "theI2" +val the1_equality = thm "the1_equality" +val excluded_middle = thm "excluded_middle" +val case_split_thm = thm "case_split_thm" +val exCI = thm "exCI" +val choice_eq = thm "choice_eq" +val eq_cong2 = thm "eq_cong2" +val if_cong = thm "if_cong" +val if_weak_cong = thm "if_weak_cong" +val let_weak_cong = thm "let_weak_cong" +val eq_cong2 = thm "eq_cong2" +val if_distrib = thm "if_distrib" +val expand_case = thm "expand_case" +val restrict_to_left = thm "restrict_to_left" +val all_conj_distrib = thm "all_conj_distrib"; +val atomize_not = thm "atomize_not"; +val split_if = thm "split_if"; +val split_if_asm = thm "split_if_asm"; +val rev_conj_cong = thm "rev_conj_cong"; +val not_all = thm "not_all"; +val not_ex = thm "not_ex"; +val not_iff = thm "not_iff"; +val not_imp = thm "not_imp"; +val not_not = thm "not_not"; +val eta_contract_eq = thm "eta_contract_eq"; +val eq_ac = thms "eq_ac"; +val eq_commute = thm "eq_commute"; +val eq_sym_conv = thm "eq_commute"; +val neq_commute = thm "neq_commute"; +val conj_comms = thms "conj_comms"; +val conj_commute = thm "conj_commute"; +val conj_cong = thm "conj_cong"; +val conj_disj_distribL = thm "conj_disj_distribL"; +val conj_disj_distribR = thm "conj_disj_distribR"; +val conj_left_commute = thm "conj_left_commute"; +val disj_comms = thms "disj_comms"; +val disj_commute = thm "disj_commute"; +val disj_cong = thm "disj_cong"; +val disj_conj_distribL = thm "disj_conj_distribL"; +val disj_conj_distribR = thm "disj_conj_distribR"; +val disj_left_commute = thm "disj_left_commute"; +val eq_assoc = thm "eq_assoc"; +val eq_left_commute = thm "eq_left_commute"; +val ex_disj_distrib = thm "ex_disj_distrib"; +val if_P = thm "if_P"; +val if_bool_eq_disj = thm "if_bool_eq_disj"; +val if_def2 = thm "if_bool_eq_conj"; +val if_not_P = thm "if_not_P"; +val if_splits = thms "if_splits"; +val imp_all = thm "imp_all"; +val imp_conjL = thm "imp_conjL"; +val imp_conjR = thm "imp_conjR"; +val imp_disj_not1 = thm "imp_disj_not1"; +val imp_disj_not2 = thm "imp_disj_not2"; +val imp_ex = thm "imp_ex"; +val meta_eq_to_obj_eq = thm "def_imp_eq"; +val ex_simps = thms "ex_simps"; +val all_simps = thms "all_simps"; +val simp_thms = thms "simp_thms"; +val Eq_FalseI = thm "Eq_FalseI"; +val Eq_TrueI = thm "Eq_TrueI"; +val cases_simp = thm "cases_simp"; +val conj_assoc = thm "conj_assoc"; +val de_Morgan_conj = thm "de_Morgan_conj"; +val de_Morgan_disj = thm "de_Morgan_disj"; +val disj_assoc = thm "disj_assoc"; +val disj_not1 = thm "disj_not1"; +val disj_not2 = thm "disj_not2"; +val if_False = thm "if_False"; +val if_True = thm "if_True"; +val if_bool_eq_conj = thm "if_bool_eq_conj"; +val if_cancel = thm "if_cancel"; +val if_eq_cancel = thm "if_eq_cancel"; +val iff_conv_conj_imp = thm "iff_conv_conj_imp"; +val imp_cong = thm "imp_cong"; +val imp_conv_disj = thm "imp_conv_disj"; +val imp_disj1 = thm "imp_disj1"; +val imp_disj2 = thm "imp_disj2"; +val imp_disjL = thm "imp_disjL"; +val simp_impliesI = thm "simp_impliesI"; +val simp_implies_cong = thm "simp_implies_cong"; +val simp_implies_def = thm "simp_implies_def"; +val True_implies_equals = thm "True_implies_equals"; structure HOL = struct diff -r cf19faf11bbd -r 34b2c1bb7178 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Oct 10 10:34:43 2006 +0200 +++ b/src/HOL/HOL.thy Tue Oct 10 10:35:24 2006 +0200 @@ -150,17 +150,6 @@ mp: "[| P-->Q; P |] ==> Q" -text{*Thanks to Stephan Merz*} -theorem subst: - assumes eq: "s = t" and p: "P(s)" - shows "P(t::'a)" -proof - - from eq have meta: "s \ t" - by (rule eq_reflection) - from p show ?thesis - by (unfold meta) -qed - defs True_def: "True == ((%x::bool. x) = (%x. x))" All_def: "All(P) == (P = (%x. True))" @@ -236,7 +225,20 @@ abs ("\_\") -subsection {*Equality*} +subsection {* Fundamental rules *} + +subsubsection {*Equality*} + +text {* Thanks to Stephan Merz *} +lemma subst: + assumes eq: "s = t" and p: "P s" + shows "P t" +proof - + from eq have meta: "s \ t" + by (rule eq_reflection) + from p show ?thesis + by (unfold meta) +qed lemma sym: "s = t ==> t = s" by (erule subst) (rule refl) @@ -247,12 +249,19 @@ lemma trans: "[| r=s; s=t |] ==> r=t" by (erule subst) -lemma def_imp_eq: assumes meq: "A == B" shows "A = B" +lemma def_imp_eq: + assumes meq: "A == B" + shows "A = B" by (unfold meq) (rule refl) +(*a mere copy*) +lemma meta_eq_to_obj_eq: + assumes meq: "A == B" + shows "A = B" + by (unfold meq) (rule refl) -(*Useful with eresolve_tac for proving equalties from known equalities. - a = b +text {* Useful with eresolve\_tac for proving equalties from known equalities. *} + (* a = b | | c = d *) lemma box_equals: "[| a=b; a=c; b=d |] ==> c=d" @@ -271,7 +280,7 @@ by (rule subst) -subsection {*Congruence rules for application*} +subsubsection {*Congruence rules for application*} (*similar to AP_THM in Gordon's HOL*) lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" @@ -290,14 +299,13 @@ apply (rule refl) done - lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)" apply (erule subst)+ apply (rule refl) done -subsection {*Equality of booleans -- iff*} +subsubsection {*Equality of booleans -- iff*} lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q" by (iprover intro: iff [THEN mp, THEN mp] impI prems) @@ -318,7 +326,7 @@ by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1]) -subsection {*True*} +subsubsection {*True*} lemma TrueI: "True" by (unfold True_def) (rule refl) @@ -332,7 +340,7 @@ done -subsection {*Universal quantifier*} +subsubsection {*Universal quantifier*} lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)" apply (unfold All_def) @@ -358,7 +366,7 @@ by (iprover intro: minor major major [THEN spec]) -subsection {*False*} +subsubsection {*False*} (*Depends upon spec; it is impossible to do propositional logic before quantifiers!*) lemma FalseE: "False ==> P" @@ -370,7 +378,7 @@ by (erule eqTrueE [THEN FalseE]) -subsection {*Negation*} +subsubsection {*Negation*} lemma notI: assumes p: "P ==> False" @@ -400,7 +408,7 @@ lemmas notI2 = notE [THEN notI, standard] -subsection {*Implication*} +subsubsection {*Implication*} lemma impE: assumes "P-->Q" "P" "Q ==> R" @@ -438,7 +446,7 @@ apply (erule pq) done -subsection {*Existential quantifier*} +subsubsection {*Existential quantifier*} lemma exI: "P x ==> EX x::'a. P x" apply (unfold Ex_def) @@ -454,7 +462,7 @@ done -subsection {*Conjunction*} +subsubsection {*Conjunction*} lemma conjI: "[| P; Q |] ==> P&Q" apply (unfold and_def) @@ -485,7 +493,7 @@ by (iprover intro: conjI prems) -subsection {*Disjunction*} +subsubsection {*Disjunction*} lemma disjI1: "P ==> P|Q" apply (unfold or_def) @@ -506,8 +514,7 @@ major [unfolded or_def, THEN spec, THEN mp, THEN mp]) -subsection {*Classical logic*} - +subsubsection {*Classical logic*} lemma classical: assumes prem: "~P ==> P" @@ -545,7 +552,7 @@ by (iprover intro: classical p1 p2 notE) -subsection {*Unique existence*} +subsubsection {*Unique existence*} lemma ex1I: assumes prems: "P a" "!!x. P(x) ==> x=a" @@ -575,7 +582,7 @@ done -subsection {*THE: definite description operator*} +subsubsection {*THE: definite description operator*} lemma the_equality: assumes prema: "P a" @@ -628,7 +635,7 @@ done -subsection {*Classical intro rules for disjunction and existential quantifiers*} +subsubsection {*Classical intro rules for disjunction and existential quantifiers*} lemma disjCI: assumes "~Q ==> P" shows "P|Q" @@ -639,8 +646,10 @@ lemma excluded_middle: "~P | P" by (iprover intro: disjCI) -text{*case distinction as a natural deduction rule. Note that @{term "~P"} - is the second case, not the first.*} +text {* + case distinction as a natural deduction rule. + Note that @{term "~P"} is the second case, not the first +*} lemma case_split_thm: assumes prem1: "P ==> Q" and prem2: "~P ==> Q" @@ -649,6 +658,7 @@ apply (erule prem2) apply (erule prem1) done +lemmas case_split = case_split_thm [case_names True False] (*Classical implies (-->) elimination. *) lemma impCE: @@ -687,129 +697,6 @@ done - -subsection {* Theory and package setup *} - -ML -{* -val eq_reflection = thm "eq_reflection" -val refl = thm "refl" -val subst = thm "subst" -val ext = thm "ext" -val impI = thm "impI" -val mp = thm "mp" -val True_def = thm "True_def" -val All_def = thm "All_def" -val Ex_def = thm "Ex_def" -val False_def = thm "False_def" -val not_def = thm "not_def" -val and_def = thm "and_def" -val or_def = thm "or_def" -val Ex1_def = thm "Ex1_def" -val iff = thm "iff" -val True_or_False = thm "True_or_False" -val Let_def = thm "Let_def" -val if_def = thm "if_def" -val sym = thm "sym" -val ssubst = thm "ssubst" -val trans = thm "trans" -val def_imp_eq = thm "def_imp_eq" -val box_equals = thm "box_equals" -val fun_cong = thm "fun_cong" -val arg_cong = thm "arg_cong" -val cong = thm "cong" -val iffI = thm "iffI" -val iffD2 = thm "iffD2" -val rev_iffD2 = thm "rev_iffD2" -val iffD1 = thm "iffD1" -val rev_iffD1 = thm "rev_iffD1" -val iffE = thm "iffE" -val TrueI = thm "TrueI" -val eqTrueI = thm "eqTrueI" -val eqTrueE = thm "eqTrueE" -val allI = thm "allI" -val spec = thm "spec" -val allE = thm "allE" -val all_dupE = thm "all_dupE" -val FalseE = thm "FalseE" -val False_neq_True = thm "False_neq_True" -val notI = thm "notI" -val False_not_True = thm "False_not_True" -val True_not_False = thm "True_not_False" -val notE = thm "notE" -val notI2 = thm "notI2" -val impE = thm "impE" -val rev_mp = thm "rev_mp" -val contrapos_nn = thm "contrapos_nn" -val contrapos_pn = thm "contrapos_pn" -val not_sym = thm "not_sym" -val rev_contrapos = thm "rev_contrapos" -val exI = thm "exI" -val exE = thm "exE" -val conjI = thm "conjI" -val conjunct1 = thm "conjunct1" -val conjunct2 = thm "conjunct2" -val conjE = thm "conjE" -val context_conjI = thm "context_conjI" -val disjI1 = thm "disjI1" -val disjI2 = thm "disjI2" -val disjE = thm "disjE" -val classical = thm "classical" -val ccontr = thm "ccontr" -val rev_notE = thm "rev_notE" -val notnotD = thm "notnotD" -val contrapos_pp = thm "contrapos_pp" -val ex1I = thm "ex1I" -val ex_ex1I = thm "ex_ex1I" -val ex1E = thm "ex1E" -val ex1_implies_ex = thm "ex1_implies_ex" -val the_equality = thm "the_equality" -val theI = thm "theI" -val theI' = thm "theI'" -val theI2 = thm "theI2" -val the1_equality = thm "the1_equality" -val the_sym_eq_trivial = thm "the_sym_eq_trivial" -val disjCI = thm "disjCI" -val excluded_middle = thm "excluded_middle" -val case_split_thm = thm "case_split_thm" -val impCE = thm "impCE" -val impCE = thm "impCE" -val iffCE = thm "iffCE" -val exCI = thm "exCI" - -(* 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 = List.filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t))))) -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) - -(*Obsolete form of disjunctive case analysis*) -fun excluded_middle_tac sP = - res_inst_tac [("Q",sP)] (excluded_middle RS disjE) - -fun case_tac a = res_inst_tac [("P",a)] case_split_thm -*} - -theorems case_split = case_split_thm [case_names True False] - -ML {* -structure ProjectRule = ProjectRuleFun -(struct - val conjunct1 = thm "conjunct1"; - val conjunct2 = thm "conjunct2"; - val mp = thm "mp"; -end) -*} - - subsubsection {* Intuitionistic Reasoning *} lemma impE': @@ -912,14 +799,75 @@ and [symmetric, defn] = atomize_all atomize_imp atomize_eq +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: + "\X. \ x=x; PROP W \ \ PROP W" . + use "cladata.ML" -setup hypsubst_setup -setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *} +ML {* val HOL_cs = HOL.cs *} +setup Hypsubst.hypsubst_setup +setup {* ContextRules.addSWrapper (fn tac => HOL.hyp_subst_tac' ORELSE' tac) *} setup Classical.setup setup ResAtpset.setup -setup clasetup +setup {* fn thy => (Classical.change_claset_of thy (K HOL.cs); thy) *} lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" apply (erule swap) @@ -932,17 +880,33 @@ lemmas [intro?] = ext and [elim?] = ex1_implies_ex +(*Better then ex1E for classical reasoner: needs no quantifier duplication!*) +lemma alt_ex1E: + assumes major: "\!x. P x" + and prem: "\x. \ P x; \y y'. P y \ P y' \ y = y' \ \ R" + 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") +by iprover + use "blastdata.ML" setup Blast.setup +ML {* +structure HOL = +struct -subsubsection {* Simplifier setup *} +open HOL; -lemma meta_eq_to_obj_eq: "x == y ==> x = y" -proof - - assume r: "x == y" - show "x = y" by (unfold r) (rule refl) -qed +fun case_tac a = res_inst_tac [("P", a)] case_split; + +end; +*} + + +subsubsection {* Simplifier *} lemma eta_contract_eq: "(%s. f s) = f" .. @@ -953,9 +917,15 @@ "(P ~= Q) = (P = (~Q))" "(P | ~P) = True" "(~P | P) = True" "(x = x) = True" - "(~True) = False" "(~False) = True" + and not_True_eq_False: "(\ True) = False" + and not_False_eq_True: "(\ False) = True" + and "(~P) ~= P" "P ~= (~P)" - "(True=P) = P" "(P=True) = P" "(False=P) = (~P)" "(P=False) = (~P)" + "(True=P) = P" + and eq_True: "(P = True) = P" + and "(False=P) = (~P)" + and eq_False: "(P = False) = (\ P)" + and "(True --> P) = P" "(False --> P) = True" "(P --> True) = True" "(P --> P) = True" "(P --> False) = (~P)" "(P --> ~P) = (~P)" @@ -1090,9 +1060,6 @@ "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))" by blast -lemma eq_sym_conv: "(x = y) = (y = x)" - by iprover - text {* \medskip if-then-else rules *} @@ -1119,9 +1086,6 @@ lemmas if_splits = split_if split_if_asm -lemma if_def2: "(if Q then x else y) = ((Q --> x) & (~ Q --> y))" - by (rule split_if) - lemma if_cancel: "(if c then x else x) = x" by (simplesubst split_if, blast) @@ -1199,114 +1163,111 @@ text {* \medskip Actual Installation of the Simplifier. *} +lemma True_implies_equals: "(True \ PROP P) \ PROP P" +proof + assume prem: "True \ PROP P" + from prem [OF TrueI] show "PROP P" . +next + assume "PROP P" + show "PROP P" . +qed + +lemma uncurry: + assumes "P \ Q \ R" + shows "P \ Q \ R" + using prems by blast + +lemma iff_allI: + assumes "\x. P x = Q x" + shows "(\x. P x) = (\x. Q x)" + using prems by blast + +lemma iff_exI: + assumes "\x. P x = Q x" + shows "(\x. P x) = (\x. Q x)" + using prems by blast + +lemma all_comm: + "(\x y. P x y) = (\y x. P x y)" + by blast + +lemma ex_comm: + "(\x y. P x y) = (\y x. P x y)" + by blast + use "simpdata.ML" -setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup -setup Splitter.setup setup Clasimp.setup +setup "Simplifier.method_setup Splitter.split_modifiers" +setup simpsetup +setup Splitter.setup +setup Clasimp.setup setup EqSubst.setup +text {* Simplifies x assuming c and y assuming ~c *} +lemma if_cong: + assumes "b = c" + and "c \ x = u" + and "\ c \ y = v" + shows "(if b then x else y) = (if c then u else v)" + unfolding if_def using prems by simp + +text {* Prevents simplification of x and y: + faster and allows the execution of functional programs. *} +lemma if_weak_cong [cong]: + assumes "b = c" + shows "(if b then x else y) = (if c then x else y)" + using prems by (rule arg_cong) + +text {* Prevents simplification of t: much faster *} +lemma let_weak_cong: + assumes "a = b" + shows "(let x = a in t x) = (let x = b in t x)" + using prems by (rule arg_cong) + +text {* To tidy up the result of a simproc. Only the RHS will be simplified. *} +lemma eq_cong2: + assumes "u = u'" + shows "(t \ u) \ (t \ u')" + using prems by simp + +lemma if_distrib: + "f (if c then x else y) = (if c then f x else f y)" + by simp + +text {* For 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 {Integ,Real}/simproc.ML *} +lemma restrict_to_left: + assumes "x = y" + shows "(x = z) = (y = z)" + using prems by simp + -subsubsection {* Code generator setup *} - -types_code - "bool" ("bool") -attach (term_of) {* -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; -*} -attach (test) {* -fun gen_bool i = one_of [false, true]; -*} - "prop" ("bool") -attach (term_of) {* -fun term_of_prop b = - HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); -*} - -consts_code - "Trueprop" ("(_)") - "True" ("true") - "False" ("false") - "Not" ("not") - "op |" ("(_ orelse/ _)") - "op &" ("(_ andalso/ _)") - "HOL.If" ("(if _/ then _/ else _)") +subsubsection {* Generic cases and induction *} -setup {* -let - -fun eq_codegen thy defs gr dep thyname b t = - (case strip_comb t of - (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE - | (Const ("op =", _), [t, u]) => - let - val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); - val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u); - val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) - in - SOME (gr''', Codegen.parens - (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) - end - | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen - thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) - | _ => NONE); - -in - -Codegen.add_codegen "eq_codegen" eq_codegen - -end -*} +text {* Rule projections: *} -setup {* -let - -fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule - (Drule.goals_conv (equal i) Codegen.evaluation_conv)); - -val evaluation_meth = - Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac TrueI 1)); - -in - -Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation") - -end; +ML {* +structure ProjectRule = ProjectRuleFun +(struct + val conjunct1 = thm "conjunct1"; + val conjunct2 = thm "conjunct2"; + val mp = thm "mp"; +end) *} - -subsection {* Other simple lemmas *} - -declare disj_absorb [simp] conj_absorb [simp] - -lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x" -by blast+ - - -theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))" - apply (rule iffI) - apply (rule_tac a = "%x. THE y. P x y" in ex1I) - apply (fast dest!: theI') - apply (fast intro: ext the1_equality [symmetric]) - apply (erule ex1E) - apply (rule allI) - apply (rule ex1I) - apply (erule spec) - apply (erule_tac x = "%z. if z = x then y else f z" in allE) - apply (erule impE) - apply (rule allI) - apply (rule_tac P = "xa = x" in case_split_thm) - 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)" -by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]]) - - -subsection {* Generic cases and induction *} - constdefs induct_forall where "induct_forall P == \x. P x" induct_implies where "induct_implies A B == A \ B" @@ -1369,6 +1330,74 @@ setup InductMethod.setup +subsubsection {* Code generator setup *} + +types_code + "bool" ("bool") +attach (term_of) {* +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; +*} +attach (test) {* +fun gen_bool i = one_of [false, true]; +*} + "prop" ("bool") +attach (term_of) {* +fun term_of_prop b = + HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); +*} + +consts_code + "Trueprop" ("(_)") + "True" ("true") + "False" ("false") + "Not" ("not") + "op |" ("(_ orelse/ _)") + "op &" ("(_ andalso/ _)") + "HOL.If" ("(if _/ then _/ else _)") + +setup {* +let + +fun eq_codegen thy defs gr dep thyname b t = + (case strip_comb t of + (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE + | (Const ("op =", _), [t, u]) => + let + val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); + val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u); + val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) + in + SOME (gr''', Codegen.parens + (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) + end + | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen + thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) + | _ => NONE); + +in + +Codegen.add_codegen "eq_codegen" eq_codegen + +end +*} + +setup {* +let + +fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule + (Drule.goals_conv (equal i) Codegen.evaluation_conv)); + +val evaluation_meth = + Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1)); + +in + +Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation") + +end; +*} + + text {* itself as a code generator datatype *} setup {* @@ -1390,7 +1419,65 @@ setup {* CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")" *} + code_const arbitrary (Haskell target_atom "(error \"arbitrary\")") + +subsection {* Other simple lemmas and lemma duplicates *} + +lemmas eq_sym_conv = eq_commute +lemmas if_def2 = if_bool_eq_conj + +lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x" + by blast+ + +lemma choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))" + apply (rule iffI) + apply (rule_tac a = "%x. THE y. P x y" in ex1I) + apply (fast dest!: theI') + apply (fast intro: ext the1_equality [symmetric]) + apply (erule ex1E) + apply (rule allI) + apply (rule ex1I) + apply (erule spec) + apply (erule_tac x = "%z. if z = x then y else f z" in allE) + apply (erule impE) + apply (rule allI) + apply (rule_tac P = "xa = x" in case_split_thm) + 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)" + by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]]) + + +subsection {* Conclude HOL structure *} + +ML {* +structure HOL = +struct + +open HOL; + +(* 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); + +end; +*} + end diff -r cf19faf11bbd -r 34b2c1bb7178 src/HOL/blastdata.ML --- a/src/HOL/blastdata.ML Tue Oct 10 10:34:43 2006 +0200 +++ b/src/HOL/blastdata.ML Tue Oct 10 10:35:24 2006 +0200 @@ -1,35 +1,29 @@ +Classical.AddSEs [thm "alt_ex1E"]; -(*Better then ex1E for classical reasoner: needs no quantifier duplication!*) -val major::prems = goal (the_context ()) - "[| ?! x. P(x); \ -\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \ -\ |] ==> R"; -by (rtac (major RS ex1E) 1); -by (REPEAT (ares_tac (allI::prems) 1)); -by (etac (dup_elim allE) 1); -by (Fast_tac 1); -qed "alt_ex1E"; - -AddSEs [alt_ex1E]; - -(*** Applying BlastFun to create Blast_tac ***) structure Blast_Data = - struct - type claset = Classical.claset +struct + type claset = Classical.claset val equality_name = "op =" val not_name = "Not" - val notE = notE - val ccontr = ccontr + val notE = HOL.notE + val ccontr = HOL.ccontr val contr_tac = Classical.contr_tac - val dup_intr = Classical.dup_intr + val dup_intr = Classical.dup_intr val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac val claset = Classical.claset - val rep_cs = Classical.rep_cs - val cla_modifiers = Classical.cla_modifiers; + val rep_cs = Classical.rep_cs + val cla_modifiers = Classical.cla_modifiers val cla_meth' = Classical.cla_meth' - end; +end; structure Blast = BlastFun(Blast_Data); -val Blast_tac = Blast.Blast_tac -and blast_tac = Blast.blast_tac; +structure HOL = +struct + +open HOL; + +val Blast_tac = Blast.Blast_tac; +val blast_tac = Blast.blast_tac; + +end; \ No newline at end of file diff -r cf19faf11bbd -r 34b2c1bb7178 src/HOL/cladata.ML --- a/src/HOL/cladata.ML Tue Oct 10 10:34:43 2006 +0200 +++ b/src/HOL/cladata.ML Tue Oct 10 10:35:24 2006 +0200 @@ -6,58 +6,53 @@ Setting up the classical reasoner. *) - -(** Applying HypsubstFun to generate hyp_subst_tac **) -section "Classical Reasoner"; - structure Hypsubst_Data = - struct +struct structure Simplifier = Simplifier - (*Take apart an equality judgement; otherwise raise Match!*) - fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) + fun dest_eq (Const ("op =", T) $ t $ u) = (t, u, domain_type T) val dest_Trueprop = HOLogic.dest_Trueprop val dest_imp = HOLogic.dest_imp - val eq_reflection = eq_reflection - val rev_eq_reflection = def_imp_eq - val imp_intr = impI - val rev_mp = rev_mp - val subst = subst - val sym = sym - val thin_refl = prove_goal (the_context ()) - "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]); - end; + 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 thin_refl = thm "thin_refl"; +end; structure Hypsubst = HypsubstFun(Hypsubst_Data); + +structure Classical_Data = +struct + val mp = HOL.mp + val not_elim = HOL.notE + val classical = HOL.classical + val sizef = Drule.size_of_thm + val hyp_subst_tacs = [Hypsubst.hyp_subst_tac] +end; + +structure Classical = ClassicalFun(Classical_Data); +structure BasicClassical: BASIC_CLASSICAL = Classical; + +structure HOL = +struct + +open HOL; open Hypsubst; +open BasicClassical; (*prevent substitution on bool*) fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false) - (List.nth (Thm.prems_of thm, i - 1)) then hyp_subst_tac i thm else no_tac thm; - - -(*** Applying ClassicalFun to create a classical prover ***) -structure Classical_Data = - struct - val mp = mp - val not_elim = notE - val classical = classical - val sizef = size_of_thm - val hyp_subst_tacs=[hyp_subst_tac] - end; - -structure Classical = ClassicalFun(Classical_Data); - -structure BasicClassical: BASIC_CLASSICAL = Classical; - -open BasicClassical; + (nth (Thm.prems_of thm) (i - 1)) then hyp_subst_tac i thm else no_tac thm; (*Propositional rules*) -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] - addSEs [conjE,disjE,impCE,FalseE,iffCE]; +val prop_cs = empty_cs addSIs [HOL.refl, HOL.TrueI, HOL.conjI, HOL.disjCI, HOL.impI, HOL.notI, HOL.iffI] + addSEs [HOL.conjE, HOL.disjE, HOL.impCE, HOL.FalseE, HOL.iffCE]; (*Quantifier rules*) -val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality] - addSEs [exE] addEs [allE]; +val cs = prop_cs addSIs [HOL.allI, HOL.ex_ex1I] addIs [HOL.exI, HOL.the_equality] + addSEs [HOL.exE] addEs [HOL.allE]; -val clasetup = (fn thy => (change_claset_of thy (fn _ => HOL_cs); thy)); +end; diff -r cf19faf11bbd -r 34b2c1bb7178 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Tue Oct 10 10:34:43 2006 +0200 +++ b/src/HOL/simpdata.ML Tue Oct 10 10:35:24 2006 +0200 @@ -6,93 +6,28 @@ Instantiation of the generic simplifier for HOL. *) -(* legacy ML bindings *) +(* legacy ML bindings - FIXME get rid of this *) val Eq_FalseI = thm "Eq_FalseI"; val Eq_TrueI = thm "Eq_TrueI"; -val all_conj_distrib = thm "all_conj_distrib"; -val all_simps = thms "all_simps"; -val cases_simp = thm "cases_simp"; -val conj_assoc = thm "conj_assoc"; -val conj_comms = thms "conj_comms"; -val conj_commute = thm "conj_commute"; -val conj_cong = thm "conj_cong"; -val conj_disj_distribL = thm "conj_disj_distribL"; -val conj_disj_distribR = thm "conj_disj_distribR"; -val conj_left_commute = thm "conj_left_commute"; val de_Morgan_conj = thm "de_Morgan_conj"; val de_Morgan_disj = thm "de_Morgan_disj"; -val disj_assoc = thm "disj_assoc"; -val disj_comms = thms "disj_comms"; -val disj_commute = thm "disj_commute"; -val disj_cong = thm "disj_cong"; -val disj_conj_distribL = thm "disj_conj_distribL"; -val disj_conj_distribR = thm "disj_conj_distribR"; -val disj_left_commute = thm "disj_left_commute"; -val disj_not1 = thm "disj_not1"; -val disj_not2 = thm "disj_not2"; -val eq_ac = thms "eq_ac"; -val eq_assoc = thm "eq_assoc"; -val eq_commute = thm "eq_commute"; -val eq_left_commute = thm "eq_left_commute"; -val eq_sym_conv = thm "eq_sym_conv"; -val eta_contract_eq = thm "eta_contract_eq"; -val ex_disj_distrib = thm "ex_disj_distrib"; -val ex_simps = thms "ex_simps"; -val if_False = thm "if_False"; -val if_P = thm "if_P"; -val if_True = thm "if_True"; -val if_bool_eq_conj = thm "if_bool_eq_conj"; -val if_bool_eq_disj = thm "if_bool_eq_disj"; -val if_cancel = thm "if_cancel"; -val if_def2 = thm "if_def2"; -val if_eq_cancel = thm "if_eq_cancel"; -val if_not_P = thm "if_not_P"; -val if_splits = thms "if_splits"; val iff_conv_conj_imp = thm "iff_conv_conj_imp"; -val imp_all = thm "imp_all"; val imp_cong = thm "imp_cong"; -val imp_conjL = thm "imp_conjL"; -val imp_conjR = thm "imp_conjR"; val imp_conv_disj = thm "imp_conv_disj"; val imp_disj1 = thm "imp_disj1"; val imp_disj2 = thm "imp_disj2"; val imp_disjL = thm "imp_disjL"; -val imp_disj_not1 = thm "imp_disj_not1"; -val imp_disj_not2 = thm "imp_disj_not2"; -val imp_ex = thm "imp_ex"; -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; -val neq_commute = thm "neq_commute"; -val not_all = thm "not_all"; -val not_ex = thm "not_ex"; -val not_iff = thm "not_iff"; -val not_imp = thm "not_imp"; -val not_not = thm "not_not"; -val rev_conj_cong = thm "rev_conj_cong"; -val simp_impliesE = thm "simp_impliesI"; val simp_impliesI = thm "simp_impliesI"; val simp_implies_cong = thm "simp_implies_cong"; val simp_implies_def = thm "simp_implies_def"; -val simp_thms = thms "simp_thms"; -val split_if = thm "split_if"; -val split_if_asm = thm "split_if_asm"; -val atomize_not = thm"atomize_not"; local -val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R" - (fn prems => [cut_facts_tac prems 1, Blast_tac 1]); - -val iff_allI = allI RS - prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)" - (fn prems => [cut_facts_tac prems 1, Blast_tac 1]) -val iff_exI = allI RS - prove_goal (the_context()) "!x. P x = Q x ==> (? x. P x) = (? x. Q x)" - (fn prems => [cut_facts_tac prems 1, Blast_tac 1]) - -val all_comm = prove_goal (the_context()) "(!x y. P x y) = (!y x. P x y)" - (fn _ => [Blast_tac 1]) -val ex_comm = prove_goal (the_context()) "(? x y. P x y) = (? y x. P x y)" - (fn _ => [Blast_tac 1]) + val uncurry = thm "uncurry" + val iff_allI = thm "iff_allI" + val iff_exI = thm "iff_exI" + val all_comm = thm "all_comm" + val ex_comm = thm "ex_comm" in (*** make simplification procedures for quantifier elimination ***) @@ -109,16 +44,16 @@ val conj = HOLogic.conj val imp = HOLogic.imp (*rules*) - val iff_reflection = eq_reflection - val iffI = iffI - val iff_trans = trans - val conjI= conjI - val conjE= conjE - val impI = impI - val mp = mp + val iff_reflection = HOL.eq_reflection + val iffI = HOL.iffI + val iff_trans = HOL.trans + val conjI= HOL.conjI + val conjE= HOL.conjE + val impI = HOL.impI + val mp = HOL.mp val uncurry = uncurry - val exI = exI - val exE = exE + val exI = HOL.exI + val exE = HOL.exE val iff_allI = iff_allI val iff_exI = iff_exI val all_comm = all_comm @@ -128,63 +63,59 @@ end; val defEX_regroup = - Simplifier.simproc (Theory.sign_of (the_context ())) + Simplifier.simproc (the_context ()) "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; val defALL_regroup = - Simplifier.simproc (Theory.sign_of (the_context ())) + Simplifier.simproc (the_context ()) "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; -(*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***) +(* simproc for proving "(y = x) == False" from premise "~(x = y)" *) val use_neq_simproc = ref true; local - -val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; - -fun neq_prover sg ss (eq $ lhs $ rhs) = -let - fun test thm = (case #prop(rep_thm thm) of + val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI; + fun neq_prover sg ss (eq $ lhs $ rhs) = + let + fun test thm = (case #prop (rep_thm thm) of _ $ (Not $ (eq' $ l' $ r')) => Not = HOLogic.Not andalso eq' = eq andalso r' aconv lhs andalso l' aconv rhs | _ => false) -in - if !use_neq_simproc then - case Library.find_first test (prems_of_ss ss) of NONE => NONE - | SOME thm => SOME (thm RS neq_to_EQ_False) - else NONE -end - + in if !use_neq_simproc then case find_first test (prems_of_ss ss) + of NONE => NONE + | SOME thm => SOME (thm RS neq_to_EQ_False) + else NONE + end in -val neq_simproc = - Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover; +val neq_simproc = Simplifier.simproc (the_context ()) + "neq_simproc" ["x = y"] neq_prover; end; -(*** Simproc for Let ***) +(* Simproc for Let *) val use_let_simproc = ref true; local -val Let_folded = thm "Let_folded"; -val Let_unfold = thm "Let_unfold"; - -val (f_Let_unfold,x_Let_unfold) = + val Let_folded = thm "Let_folded"; + val Let_unfold = thm "Let_unfold"; + val (f_Let_unfold,x_Let_unfold) = let val [(_$(f$x)$_)] = prems_of Let_unfold - in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end -val (f_Let_folded,x_Let_folded) = + in (cterm_of (the_context ()) f,cterm_of (the_context ()) x) end + val (f_Let_folded,x_Let_folded) = let val [(_$(f$x)$_)] = prems_of Let_folded - in (cterm_of (sign_of (the_context ())) f, cterm_of (sign_of (the_context ())) x) end; -val g_Let_folded = - let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end; + in (cterm_of (the_context ()) f, cterm_of (the_context ()) x) end; + val g_Let_folded = + let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (the_context ()) g end; in + val let_simproc = - Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] + Simplifier.simproc (the_context ()) "let_simp" ["Let x f"] (fn sg => fn ss => fn t => let val ctxt = Simplifier.the_context ss; val ([t'],ctxt') = Variable.import_terms false [t] ctxt; @@ -192,7 +123,7 @@ (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *) if not (!use_let_simproc) then NONE else if is_Free x orelse is_Bound x orelse is_Const x - then SOME Let_def + then SOME (thm "Let_def") else let val n = case f of (Abs (x,_,_)) => x | _ => "x"; @@ -221,13 +152,14 @@ end | _ => NONE) end) + end (*** Case splitting ***) (*Make meta-equalities. The operator below is Trueprop*) -fun mk_meta_eq r = r RS eq_reflection; +fun mk_meta_eq r = r RS HOL.eq_reflection; fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; fun mk_eq th = case concl_of th of @@ -238,7 +170,7 @@ (* Expects Trueprop(.) if not == *) fun mk_eq_True r = - SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; + SOME (r RS HOL.meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE; (* Produce theorems of the form (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) @@ -249,7 +181,7 @@ fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q | count_imp _ = 0; val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) - in if j = 0 then meta_eq_to_obj_eq + in if j = 0 then HOL.meta_eq_to_obj_eq else let val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); @@ -263,7 +195,7 @@ (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) (fn prems => EVERY [rewrite_goals_tac [simp_implies_def], - REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) + REPEAT (ares_tac (HOL.meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]) end end; @@ -276,28 +208,19 @@ else error "Conclusion of congruence rules must be =-equality" end); -(* Elimination of True from assumptions: *) - -local fun rd s = read_cterm (the_context()) (s, propT); -in val True_implies_equals = standard' (equal_intr - (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI)) - (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P"))))); -end; - - structure SplitterData = - struct +struct structure Simplifier = Simplifier val mk_eq = mk_eq - val meta_eq_to_iff = meta_eq_to_obj_eq - val iffD = iffD2 - val disjE = disjE - val conjE = conjE - val exE = exE - val contrapos = contrapos_nn - val contrapos2 = contrapos_pp - val notnotD = notnotD - end; + val meta_eq_to_iff = HOL.meta_eq_to_obj_eq + val iffD = HOL.iffD2 + val disjE = HOL.disjE + val conjE = HOL.conjE + val exE = HOL.exE + val contrapos = HOL.contrapos_nn + val contrapos2 = HOL.contrapos_pp + val notnotD = HOL.notnotD +end; structure Splitter = SplitterFun(SplitterData); @@ -310,9 +233,9 @@ val Delsplits = Splitter.Delsplits; val mksimps_pairs = - [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), - ("All", [spec]), ("True", []), ("False", []), - ("HOL.If", [if_bool_eq_conj RS iffD1])]; + [("op -->", [HOL.mp]), ("op &", [thm "conjunct1", thm "conjunct2"]), + ("All", [HOL.spec]), ("True", []), ("False", []), + ("HOL.If", [thm "if_bool_eq_conj" RS HOL.iffD1])]; (* val mk_atomize: (string * thm list) list -> thm -> thm list @@ -336,14 +259,14 @@ fun unsafe_solver_tac prems = (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' - FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE]; + FIRST'[resolve_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), atac, etac HOL.FalseE]; val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; (*No premature instantiation of variables during simplification*) fun safe_solver_tac prems = (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN' - FIRST'[match_tac(reflexive_thm::TrueI::refl::prems), - eq_assume_tac, ematch_tac [FalseE]]; + FIRST'[match_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), + eq_assume_tac, ematch_tac [HOL.FalseE]]; val safe_solver = mk_solver "HOL safe" safe_solver_tac; val HOL_basic_ss = @@ -365,65 +288,42 @@ rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the grounds that it allows simplification of R in the two cases.*) +local + val ex_simps = thms "ex_simps"; + val all_simps = thms "all_simps"; + val simp_thms = thms "simp_thms"; + val cases_simp = thm "cases_simp"; + val conj_assoc = thm "conj_assoc"; + val if_False = thm "if_False"; + val if_True = thm "if_True"; + val disj_assoc = thm "disj_assoc"; + val disj_not1 = thm "disj_not1"; + val if_cancel = thm "if_cancel"; + val if_eq_cancel = thm "if_eq_cancel"; + val True_implies_equals = thm "True_implies_equals"; +in + val HOL_ss = HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *) True_implies_equals, (* prune asms `True' *) if_True, if_False, if_cancel, if_eq_cancel, imp_disjL, conj_assoc, disj_assoc, - de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, - disj_not1, not_all, not_ex, cases_simp, - thm "the_eq_trivial", the_sym_eq_trivial] + de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, thm "not_imp", + disj_not1, thm "not_all", thm "not_ex", cases_simp, + thm "the_eq_trivial", HOL.the_sym_eq_trivial] @ ex_simps @ all_simps @ simp_thms) addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] addcongs [imp_cong, simp_implies_cong] - addsplits [split_if]; + addsplits [thm "split_if"]; + +end; fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); - -(*Simplifies x assuming c and y assuming ~c*) -val prems = Goalw [if_def] - "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \ -\ (if b then x else y) = (if c then u else v)"; -by (asm_simp_tac (HOL_ss addsimps prems) 1); -qed "if_cong"; - -(*Prevents simplification of x and y: faster and allows the execution - of functional programs. NOW THE DEFAULT.*) -Goal "b=c ==> (if b then x else y) = (if c then x else y)"; -by (etac arg_cong 1); -qed "if_weak_cong"; - -(*Prevents simplification of t: much faster*) -Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"; -by (etac arg_cong 1); -qed "let_weak_cong"; - -(*To tidy up the result of a simproc. Only the RHS will be simplified.*) -Goal "u = u' ==> (t==u) == (t==u')"; -by (asm_simp_tac HOL_ss 1); -qed "eq_cong2"; - -Goal "f(if c then x else y) = (if c then f x else f y)"; -by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1); -qed "if_distrib"; - -(*For expand_case_tac*) -val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; -by (case_tac "P" 1); -by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems))); -qed "expand_case"; - -(*This lemma restricts the effect of the rewrite rule u=v to the left-hand - side of an equality. Used in {Integ,Real}/simproc.ML*) -Goal "x=y ==> (x=z) = (y=z)"; -by (asm_simp_tac HOL_ss 1); -qed "restrict_to_left"; - (* default simpset *) val simpsetup = - (fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)); + (fn thy => (change_simpset_of thy (fn _ => HOL_ss); thy)); (*** integration of simplifier with classical reasoner ***) @@ -431,7 +331,7 @@ structure Clasimp = ClasimpFun (structure Simplifier = Simplifier and Splitter = Splitter and Classical = Classical and Blast = Blast - val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE); + val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE); open Clasimp; val HOL_css = (HOL_cs, HOL_ss); @@ -462,20 +362,20 @@ empty_ss setmkeqTrue mk_eq_True setmksimps (mksimps mksimps_pairs) addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj, - not_all,not_ex,not_not]; + thm "not_all", thm "not_ex", thm "not_not"]; fun prem_nnf_tac i st = full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st; in fun refute_tac test prep_tac ref_tac = let val refute_prems_tac = REPEAT_DETERM - (eresolve_tac [conjE, exE] 1 ORELSE + (eresolve_tac [HOL.conjE, HOL.exE] 1 ORELSE filter_prems_tac test 1 ORELSE - etac disjE 1) THEN - ((etac notE 1 THEN eq_assume_tac 1) ORELSE + etac HOL.disjE 1) THEN + ((etac HOL.notE 1 THEN eq_assume_tac 1) ORELSE ref_tac 1); in EVERY'[TRY o filter_prems_tac test, - REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, + REPEAT_DETERM o etac HOL.rev_mp, prep_tac, rtac HOL.ccontr, prem_nnf_tac, SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] end; end;