--- 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
--- 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 \<equiv> 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 ("\<bar>_\<bar>")
-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 \<equiv> 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:
+ "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> 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: "\<exists>!x. P x"
+ and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> 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: "(\<not> True) = False"
+ and not_False_eq_True: "(\<not> 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) = (\<not> 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 \<Longrightarrow> PROP P) \<equiv> PROP P"
+proof
+ assume prem: "True \<Longrightarrow> PROP P"
+ from prem [OF TrueI] show "PROP P" .
+next
+ assume "PROP P"
+ show "PROP P" .
+qed
+
+lemma uncurry:
+ assumes "P \<longrightarrow> Q \<longrightarrow> R"
+ shows "P \<and> Q \<longrightarrow> R"
+ using prems by blast
+
+lemma iff_allI:
+ assumes "\<And>x. P x = Q x"
+ shows "(\<forall>x. P x) = (\<forall>x. Q x)"
+ using prems by blast
+
+lemma iff_exI:
+ assumes "\<And>x. P x = Q x"
+ shows "(\<exists>x. P x) = (\<exists>x. Q x)"
+ using prems by blast
+
+lemma all_comm:
+ "(\<forall>x y. P x y) = (\<forall>y x. P x y)"
+ by blast
+
+lemma ex_comm:
+ "(\<exists>x y. P x y) = (\<exists>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 \<Longrightarrow> x = u"
+ and "\<not> c \<Longrightarrow> 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 \<equiv> u) \<equiv> (t \<equiv> 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 \<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 {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: "\<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)"
-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 == \<forall>x. P x"
induct_implies where "induct_implies A B == A \<longrightarrow> 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: "\<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)"
+ 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
--- 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
--- 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;
--- 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;