summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 06 Apr 2015 12:37:21 +0200 | |

changeset 59929 | a090551e5ec8 |

parent 59927 | 251fa1530de1 |

child 59930 | bdbc4b761c31 |

tuned;

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions | |

src/Tools/induct.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/HOL.thy Sat Apr 04 22:22:38 2015 +0200 +++ b/src/HOL/HOL.thy Mon Apr 06 12:37:21 2015 +0200 @@ -1365,44 +1365,32 @@ subsubsection {* Generic cases and induction *} text {* Rule projections: *} - ML {* structure Project_Rule = Project_Rule ( val conjunct1 = @{thm conjunct1} val conjunct2 = @{thm conjunct2} val mp = @{thm mp} -) +); *} -definition induct_forall where - "induct_forall P == \<forall>x. P x" - -definition induct_implies where - "induct_implies A B == A \<longrightarrow> B" - -definition induct_equal where - "induct_equal x y == x = y" +definition "induct_forall P \<equiv> \<forall>x. P x" +definition "induct_implies A B \<equiv> A \<longrightarrow> B" +definition "induct_equal x y \<equiv> x = y" +definition "induct_conj A B \<equiv> A \<and> B" +definition "induct_true \<equiv> True" +definition "induct_false \<equiv> False" -definition induct_conj where - "induct_conj A B == A \<and> B" - -definition induct_true where - "induct_true == True" - -definition induct_false where - "induct_false == False" - -lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))" +lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))" by (unfold atomize_all induct_forall_def) -lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)" +lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop (induct_implies A B)" by (unfold atomize_imp induct_implies_def) -lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)" +lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop (induct_equal x y)" by (unfold atomize_eq induct_equal_def) -lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)" +lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop (induct_conj A B)" by (unfold atomize_conj induct_conj_def) lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq @@ -1413,7 +1401,6 @@ induct_forall_def induct_implies_def induct_equal_def induct_conj_def induct_true_def induct_false_def - lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) = induct_conj (induct_forall A) (induct_forall B)" by (unfold induct_forall_def induct_conj_def) iprover @@ -1422,13 +1409,15 @@ induct_conj (induct_implies C A) (induct_implies C B)" by (unfold induct_implies_def induct_conj_def) iprover -lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)" +lemma induct_conj_curry: "(induct_conj A B \<Longrightarrow> PROP C) \<equiv> (A \<Longrightarrow> B \<Longrightarrow> PROP C)" proof - assume r: "induct_conj A B ==> PROP C" and A B - show "PROP C" by (rule r) (simp add: induct_conj_def `A` `B`) + assume r: "induct_conj A B \<Longrightarrow> PROP C" + assume ab: A B + show "PROP C" by (rule r) (simp add: induct_conj_def ab) next - assume r: "A ==> B ==> PROP C" and "induct_conj A B" - show "PROP C" by (rule r) (simp_all add: `induct_conj A B` [unfolded induct_conj_def]) + assume r: "A \<Longrightarrow> B \<Longrightarrow> PROP C" + assume ab: "induct_conj A B" + show "PROP C" by (rule r) (simp_all add: ab [unfolded induct_conj_def]) qed lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry @@ -1484,52 +1473,54 @@ text {* Pre-simplification of induction and cases rules *} -lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t" +lemma [induct_simp]: "(\<And>x. induct_equal x t \<Longrightarrow> PROP P x) \<equiv> PROP P t" unfolding induct_equal_def proof - assume R: "!!x. x = t ==> PROP P x" - show "PROP P t" by (rule R [OF refl]) + assume r: "\<And>x. x = t \<Longrightarrow> PROP P x" + show "PROP P t" by (rule r [OF refl]) next - fix x assume "PROP P t" "x = t" + fix x + assume "PROP P t" "x = t" then show "PROP P x" by simp qed -lemma [induct_simp]: "(!!x. induct_equal t x ==> PROP P x) == PROP P t" +lemma [induct_simp]: "(\<And>x. induct_equal t x \<Longrightarrow> PROP P x) \<equiv> PROP P t" unfolding induct_equal_def proof - assume R: "!!x. t = x ==> PROP P x" - show "PROP P t" by (rule R [OF refl]) + assume r: "\<And>x. t = x \<Longrightarrow> PROP P x" + show "PROP P t" by (rule r [OF refl]) next - fix x assume "PROP P t" "t = x" + fix x + assume "PROP P t" "t = x" then show "PROP P x" by simp qed -lemma [induct_simp]: "(induct_false ==> P) == Trueprop induct_true" +lemma [induct_simp]: "(induct_false \<Longrightarrow> P) \<equiv> Trueprop induct_true" unfolding induct_false_def induct_true_def by (iprover intro: equal_intr_rule) -lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P" +lemma [induct_simp]: "(induct_true \<Longrightarrow> PROP P) \<equiv> PROP P" unfolding induct_true_def proof - assume R: "True \<Longrightarrow> PROP P" - from TrueI show "PROP P" by (rule R) + assume "True \<Longrightarrow> PROP P" + then show "PROP P" using TrueI . next assume "PROP P" then show "PROP P" . qed -lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true" +lemma [induct_simp]: "(PROP P \<Longrightarrow> induct_true) \<equiv> Trueprop induct_true" unfolding induct_true_def by (iprover intro: equal_intr_rule) -lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true" +lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true" unfolding induct_true_def by (iprover intro: equal_intr_rule) -lemma [induct_simp]: "induct_implies induct_true P == P" +lemma [induct_simp]: "induct_implies induct_true P \<equiv> P" by (simp add: induct_implies_def induct_true_def) -lemma [induct_simp]: "(x = x) = True" +lemma [induct_simp]: "x = x \<longleftrightarrow> True" by (rule simp_thms) hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false

--- a/src/Tools/induct.ML Sat Apr 04 22:22:38 2015 +0200 +++ b/src/Tools/induct.ML Mon Apr 06 12:37:21 2015 +0200 @@ -162,7 +162,7 @@ val rearrange_eqs_simproc = Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"] - (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.global_cterm_of (Proof_Context.theory_of ctxt) t)); + (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t)); (* rotate k premises to the left by j, skipping over first j premises *) @@ -515,7 +515,7 @@ (** induct method **) -val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}]; +val conjunction_congs = @{thms Pure.all_conjunction imp_conjunction}; (* atomize *) @@ -549,7 +549,7 @@ rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN' rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN' Goal.conjunction_tac THEN_ALL_NEW - (rewrite_goal_tac ctxt [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac ctxt); + (rewrite_goal_tac ctxt @{thms Pure.conjunction_imp} THEN' Goal.norm_hhf_tac ctxt); (* prepare rule *)