# HG changeset patch # User blanchet # Date 1263980299 -3600 # Node ID fb90752a92713de79610f54ee719118d72749cdb # Parent c4f04bee79f3c93944ecf5e613f11ed0d3574afc# Parent 440605046777b668745aa2b599bd25a5ad224f00 merged diff -r c4f04bee79f3 -r fb90752a9271 NEWS --- a/NEWS Wed Jan 20 10:38:06 2010 +0100 +++ b/NEWS Wed Jan 20 10:38:19 2010 +0100 @@ -38,6 +38,7 @@ INTER_fold_inter ~> INFI_fold_inf UNION_fold_union ~> SUPR_fold_sup +* Added transpose to List.thy. *** ML *** diff -r c4f04bee79f3 -r fb90752a9271 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/FOL/FOL.thy Wed Jan 20 10:38:19 2010 +0100 @@ -383,6 +383,8 @@ val atomize = @{thms induct_atomize} val rulify = @{thms induct_rulify} val rulify_fallback = @{thms induct_rulify_fallback} + fun dest_def _ = NONE + fun trivial_tac _ = no_tac ); *} diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Wed Jan 20 10:38:19 2010 +0100 @@ -1581,14 +1581,10 @@ { (*JE: we now apply the induction hypothesis with some additional facts required*) from f_in_P deg_g_le_deg_f show ?thesis - proof (induct n \ "deg R f" arbitrary: "f" rule: nat_less_induct) - fix n f - assume hypo: "\mx. x \ carrier P \ - deg R g \ deg R x \ - m = deg R x \ - (\q r (k::nat). q \ carrier P \ r \ carrier P \ lcoeff g (^) k \\<^bsub>P\<^esub> x = g \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> r & (r = \\<^bsub>P\<^esub> | deg R r < deg R g))" - and prem: "n = deg R f" and f_in_P [simp]: "f \ carrier P" - and deg_g_le_deg_f: "deg R g \ deg R f" + proof (induct "deg R f" arbitrary: "f" rule: less_induct) + case less + note f_in_P [simp] = `f \ carrier P` + and deg_g_le_deg_f = `deg R g \ deg R f` let ?k = "1::nat" and ?r = "(g \\<^bsub>P\<^esub> (monom P (lcoeff f) (deg R f - deg R g))) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> (lcoeff g \\<^bsub>P\<^esub> f)" and ?q = "monom P (lcoeff f) (deg R f - deg R g)" show "\ q r (k::nat). q \ carrier P \ r \ carrier P \ lcoeff g (^) k \\<^bsub>P\<^esub> f = g \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> r & (r = \\<^bsub>P\<^esub> | deg R r < deg R g)" @@ -1631,13 +1627,13 @@ { (*JE: now it only remains the case where the induction hypothesis can be used.*) (*JE: we first prove that the degree of the remainder is smaller than the one of f*) - have deg_remainder_l_f: "deg R (\\<^bsub>P\<^esub> ?r) < n" + have deg_remainder_l_f: "deg R (\\<^bsub>P\<^esub> ?r) < deg R f" proof - have "deg R (\\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp also have "\ < deg R f" proof (rule deg_lcoeff_cancel) show "deg R (\\<^bsub>P\<^esub> (lcoeff g \\<^bsub>P\<^esub> f)) \ deg R f" - using deg_smult_ring [of "lcoeff g" f] using prem + using deg_smult_ring [of "lcoeff g" f] using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp show "deg R (g \\<^bsub>P\<^esub> ?q) \ deg R f" using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f @@ -1651,7 +1647,7 @@ using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\i. coeff P g i \ lcoeff f)"] unfolding Pi_def using deg_g_le_deg_f by force qed (simp_all add: deg_f_nzero) - finally show "deg R (\\<^bsub>P\<^esub> ?r) < n" unfolding prem . + finally show "deg R (\\<^bsub>P\<^esub> ?r) < deg R f" . qed moreover have "\\<^bsub>P\<^esub> ?r \ carrier P" by simp moreover obtain m where deg_rem_eq_m: "deg R (\\<^bsub>P\<^esub> ?r) = m" by auto @@ -1660,7 +1656,7 @@ ultimately obtain q' r' k' where rem_desc: "lcoeff g (^) (k'::nat) \\<^bsub>P\<^esub> (\\<^bsub>P\<^esub> ?r) = g \\<^bsub>P\<^esub> q' \\<^bsub>P\<^esub> r'"and rem_deg: "(r' = \\<^bsub>P\<^esub> \ deg R r' < deg R g)" and q'_in_carrier: "q' \ carrier P" and r'_in_carrier: "r' \ carrier P" - using hypo by blast + using less by blast (*JE: we now prove that the new quotient, remainder and exponent can be used to get the quotient, remainder and exponent of the long division theorem*) show ?thesis diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Bali/Basis.thy Wed Jan 20 10:38:19 2010 +0100 @@ -1,7 +1,5 @@ (* Title: HOL/Bali/Basis.thy - ID: $Id$ Author: David von Oheimb - *) header {* Definitions extending HOL as logical basis of Bali *} @@ -66,8 +64,6 @@ "\ \ a b c. \(a,b)\r; (a,c)\r\ \ b=c; (a,x)\r\<^sup>*; (a,y)\r\<^sup>*\ \ (x,y)\r\<^sup>* \ (y,x)\r\<^sup>*" proof - - note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1] - note converse_rtranclE = converse_rtranclE [consumes 1] assume unique: "\ a b c. \(a,b)\r; (a,c)\r\ \ b=c" assume "(a,x)\r\<^sup>*" then show "(a,y)\r\<^sup>* \ (x,y)\r\<^sup>* \ (y,x)\r\<^sup>*" @@ -110,13 +106,6 @@ apply (auto dest: rtrancl_into_trancl1) done -(* ### To Transitive_Closure *) -theorems converse_rtrancl_induct - = converse_rtrancl_induct [consumes 1,case_names Id Step] - -theorems converse_trancl_induct - = converse_trancl_induct [consumes 1,case_names Single Step] - (* context (theory "Set") *) lemma Ball_weaken:"\Ball s P;\ x. P x\Q x\\Ball s Q" by auto diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Bali/DeclConcepts.thy Wed Jan 20 10:38:19 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Bali/DeclConcepts.thy - ID: $Id$ Author: Norbert Schirmer *) header {* Advanced concepts on Java declarations like overriding, inheritance, @@ -2282,74 +2281,47 @@ done lemma superclasses_mono: -"\G\C \\<^sub>C D;ws_prog G; class G C = Some c; - \ C c. \class G C = Some c;C\Object\ \ \ sc. class G (super c) = Some sc; - x\superclasses G D -\ \ x\superclasses G C" -proof - - - assume ws: "ws_prog G" and - cls_C: "class G C = Some c" and - wf: "\C c. \class G C = Some c; C \ Object\ - \ \sc. class G (super c) = Some sc" - assume clsrel: "G\C\\<^sub>C D" - thus "\ c. \class G C = Some c; x\superclasses G D\\ - x\superclasses G C" (is "PROP ?P C" - is "\ c. ?CLS C c \ ?SUP D \ ?SUP C") - proof (induct ?P C rule: converse_trancl_induct) - fix C c - assume "G\C\\<^sub>C\<^sub>1D" "class G C = Some c" "x \ superclasses G D" - with wf ws show "?SUP C" - by (auto intro: no_subcls1_Object - simp add: superclasses_rec subcls1_def) - next - fix C S c - assume clsrel': "G\C \\<^sub>C\<^sub>1 S" "G\S \\<^sub>C D" - and hyp : "\ s. \class G S = Some s; x \ superclasses G D\ - \ x \ superclasses G S" - and cls_C': "class G C = Some c" - and x: "x \ superclasses G D" - moreover note wf ws - moreover from calculation - have "?SUP S" - by (force intro: no_subcls1_Object simp add: subcls1_def) - moreover from calculation - have "super c = S" - by (auto intro: no_subcls1_Object simp add: subcls1_def) - ultimately show "?SUP C" - by (auto intro: no_subcls1_Object simp add: superclasses_rec) - qed + assumes clsrel: "G\C\\<^sub>C D" + and ws: "ws_prog G" + and cls_C: "class G C = Some c" + and wf: "\C c. \class G C = Some c; C \ Object\ + \ \sc. class G (super c) = Some sc" + and x: "x\superclasses G D" + shows "x\superclasses G C" using clsrel cls_C x +proof (induct arbitrary: c rule: converse_trancl_induct) + case (base C) + with wf ws show ?case + by (auto intro: no_subcls1_Object + simp add: superclasses_rec subcls1_def) +next + case (step C S) + moreover note wf ws + moreover from calculation + have "x\superclasses G S" + by (force intro: no_subcls1_Object simp add: subcls1_def) + moreover from calculation + have "super c = S" + by (auto intro: no_subcls1_Object simp add: subcls1_def) + ultimately show ?case + by (auto intro: no_subcls1_Object simp add: superclasses_rec) qed lemma subclsEval: -"\G\C \\<^sub>C D;ws_prog G; class G C = Some c; - \ C c. \class G C = Some c;C\Object\ \ \ sc. class G (super c) = Some sc - \ \ D\superclasses G C" -proof - - note converse_trancl_induct - = converse_trancl_induct [consumes 1,case_names Single Step] - assume - ws: "ws_prog G" and - cls_C: "class G C = Some c" and - wf: "\C c. \class G C = Some c; C \ Object\ - \ \sc. class G (super c) = Some sc" - assume clsrel: "G\C\\<^sub>C D" - thus "\ c. class G C = Some c\ D\superclasses G C" - (is "PROP ?P C" is "\ c. ?CLS C c \ ?SUP C") - proof (induct ?P C rule: converse_trancl_induct) - fix C c - assume "G\C \\<^sub>C\<^sub>1 D" "class G C = Some c" - with ws wf show "?SUP C" - by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def) - next - fix C S c - assume "G\C \\<^sub>C\<^sub>1 S" "G\S\\<^sub>C D" - "\s. class G S = Some s \ D \ superclasses G S" - "class G C = Some c" - with ws wf show "?SUP C" - by - (rule superclasses_mono, - auto dest: no_subcls1_Object simp add: subcls1_def ) - qed + assumes clsrel: "G\C\\<^sub>C D" + and ws: "ws_prog G" + and cls_C: "class G C = Some c" + and wf: "\C c. \class G C = Some c; C \ Object\ + \ \sc. class G (super c) = Some sc" + shows "D\superclasses G C" using clsrel cls_C +proof (induct arbitrary: c rule: converse_trancl_induct) + case (base C) + with ws wf show ?case + by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def) +next + case (step C S) + with ws wf show ?case + by - (rule superclasses_mono, + auto dest: no_subcls1_Object simp add: subcls1_def ) qed end diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Bali/WellForm.thy Wed Jan 20 10:38:19 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Bali/WellForm.thy - ID: $Id$ Author: David von Oheimb and Norbert Schirmer *) @@ -1409,8 +1408,7 @@ from clsC ws show "methd G C sig = Some m \ G\(mdecl (sig,mthd m)) declared_in (declclass m)" - (is "PROP ?P C") - proof (induct ?P C rule: ws_class_induct') + proof (induct C rule: ws_class_induct') case Object assume "methd G Object sig = Some m" with wf show ?thesis @@ -1755,28 +1753,20 @@ lemma ballE': "\x\A. P x \ (x \ A \ Q) \ (P x \ Q) \ Q" by blast lemma subint_widen_imethds: - "\G\I\I J; wf_prog G; is_iface G J; jm \ imethds G J sig\ \ - \ im \ imethds G I sig. is_static im = is_static jm \ + assumes irel: "G\I\I J" + and wf: "wf_prog G" + and is_iface: "is_iface G J" + and jm: "jm \ imethds G J sig" + shows "\im \ imethds G I sig. is_static im = is_static jm \ accmodi im = accmodi jm \ G\resTy im\resTy jm" -proof - - assume irel: "G\I\I J" and - wf: "wf_prog G" and - is_iface: "is_iface G J" - from irel show "jm \ imethds G J sig \ ?thesis" - (is "PROP ?P I" is "PROP ?Prem J \ ?Concl I") - proof (induct ?P I rule: converse_rtrancl_induct) - case Id - assume "jm \ imethds G J sig" - then show "?Concl J" by (blast elim: bexI') + using irel jm +proof (induct rule: converse_rtrancl_induct) + case base + then show ?case by (blast elim: bexI') next - case Step - fix I SI - assume subint1_I_SI: "G\I \I1 SI" and - subint_SI_J: "G\SI \I J" and - hyp: "PROP ?P SI" and - jm: "jm \ imethds G J sig" - from subint1_I_SI + case (step I SI) + from `G\I \I1 SI` obtain i where ifI: "iface G I = Some i" and SI: "SI \ set (isuperIfs i)" @@ -1784,10 +1774,10 @@ let ?newMethods = "(Option.set \ table_of (map (\(sig, mh). (sig, I, mh)) (imethods i)))" - show "?Concl I" + show ?case proof (cases "?newMethods sig = {}") case True - with ifI SI hyp wf jm + with ifI SI step wf show "?thesis" by (auto simp add: imethds_rec) next @@ -1816,7 +1806,7 @@ wf_SI: "wf_idecl G (SI,si)" by (auto dest!: wf_idecl_supD is_acc_ifaceD dest: wf_prog_idecl) - from jm hyp + from step obtain sim::"qtname \ mhead" where sim: "sim \ imethds G SI sig" and eq_static_sim_jm: "is_static sim = is_static jm" and @@ -1841,7 +1831,6 @@ show ?thesis by auto qed - qed qed (* Tactical version *) @@ -1974,30 +1963,20 @@ from clsC ws show "\ m d. \methd G C sig = Some m; class G (declclass m) = Some d\ \ table_of (methods d) sig = Some (mthd m)" - (is "PROP ?P C") - proof (induct ?P C rule: ws_class_induct) + proof (induct rule: ws_class_induct) case Object - fix m d - assume "methd G Object sig = Some m" - "class G (declclass m) = Some d" with wf show "?thesis m d" by auto next - case Subcls - fix C c m d - assume hyp: "PROP ?P (super c)" - and m: "methd G C sig = Some m" - and declC: "class G (declclass m) = Some d" - and clsC: "class G C = Some c" - and nObj: "C \ Object" + case (Subcls C c) let ?newMethods = "table_of (map (\(s, m). (s, C, m)) (methods c)) sig" show "?thesis m d" proof (cases "?newMethods") case None - from None clsC nObj ws m declC - show "?thesis" by (auto simp add: methd_rec) (rule hyp) + from None ws Subcls + show "?thesis" by (auto simp add: methd_rec) (rule Subcls) next case Some - from Some clsC nObj ws m declC + from Some ws Subcls show "?thesis" by (auto simp add: methd_rec dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Wed Jan 20 10:38:19 2010 +0100 @@ -69,8 +69,9 @@ |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #> Seq.maps (fn (names, st) => CASES - (Rule_Cases.make_common false - (ProofContext.theory_of ctxt, Thm.prop_of st) names) + (Rule_Cases.make_common + (ProofContext.theory_of ctxt, + Thm.prop_of (Rule_Cases.internalize_params st)) names) Tactical.all_tac st)) in val setup_boogie_cases = Method.setup @{binding boogie_cases} diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Code_Numeral.thy Wed Jan 20 10:38:19 2010 +0100 @@ -83,7 +83,7 @@ then have "\n. P (of_nat n) \ P (Suc_code_numeral (of_nat n))" . then have step: "\n. P (of_nat n) \ P (of_nat (Suc n))" by simp from init step have "P (of_nat (nat_of k))" - by (induct "nat_of k") simp_all + by (induct ("nat_of k")) simp_all then show "P k" by simp qed simp_all @@ -100,7 +100,7 @@ fix k have "code_numeral_size k = nat_size (nat_of k)" by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all) - also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all + also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all finally show "code_numeral_size k = nat_of k" . qed @@ -296,8 +296,11 @@ setup {* fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} - false false) ["SML", "Haskell", "Scala"] - #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml" + false false Code_Printer.str) ["SML", "Haskell"] + #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} + false true Code_Printer.str "OCaml" + #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} + false false Code_Printer.str "Scala" *} code_reserved SML Int int @@ -323,9 +326,10 @@ (Scala infixl 8 "*") code_const div_mod_code_numeral - (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))") - (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))") + (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))") + (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") (Haskell "divMod") + (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))") code_const "eq_class.eq \ code_numeral \ code_numeral \ bool" (SML "!((_ : Int.int) = _)") @@ -337,12 +341,12 @@ (SML "Int.<=/ ((_),/ (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") - (Scala infix 4 "<=") + (Scala infixl 4 "<=") code_const "op < \ code_numeral \ code_numeral \ bool" (SML "Int.bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_by_zero,field})" shows "p = 0\<^sub>p" using nq eq -proof (induct n\"maxindex p" arbitrary: p n0 rule: nat_less_induct) - fix n p n0 - assume H: "\mp n0. isnpolyh p n0 \ - (\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)) \ m = maxindex p \ p = 0\<^sub>p" - and np: "isnpolyh p n0" and zp: "\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" and n: "n = maxindex p" - {assume nz: "n = 0" - then obtain c where "p = C c" using n np by (cases p, auto) +proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) + case less + note np = `isnpolyh p n0` and zp = `\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)` + {assume nz: "maxindex p = 0" + then obtain c where "p = C c" using np by (cases p, auto) with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp} moreover - {assume nz: "n \ 0" + {assume nz: "maxindex p \ 0" let ?h = "head p" let ?hd = "decrpoly ?h" let ?ihd = "maxindex ?hd" @@ -1005,24 +1003,23 @@ hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast from maxindex_coefficients[of p] coefficients_head[of p, symmetric] - have mihn: "maxindex ?h \ n" unfolding n by auto - with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < n" by auto + have mihn: "maxindex ?h \ maxindex p" by auto + with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p" by auto {fix bs:: "'a list" assume bs: "wf_bs bs ?hd" let ?ts = "take ?ihd bs" let ?rs = "drop ?ihd bs" have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp have bs_ts_eq: "?ts@ ?rs = bs" by simp from wf_bs_decrpoly[OF ts] have tsh: " \x. wf_bs (x#?ts) ?h" by simp - from ihd_lt_n have "ALL x. length (x#?ts) \ n" by simp - with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast - hence "\ x. wf_bs ((x#?ts) @ xs) p" using n unfolding wf_bs_def by simp + from ihd_lt_n have "ALL x. length (x#?ts) \ maxindex p" by simp + with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast + hence "\ x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp with zp have "\ x. Ipoly ((x#?ts) @ xs) p = 0" by blast hence "\ x. Ipoly (x#(?ts @ xs)) p = 0" by simp with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a] have "\x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) hence "\ c \ set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" - thm poly_zero using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff) with coefficients_head[of p, symmetric] have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp @@ -1031,7 +1028,7 @@ with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\?hd\\<^sub>p\<^bsup>bs\<^esup> = 0" by simp } then have hdz: "\bs. wf_bs bs ?hd \ \?hd\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast - from H[rule_format, OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast + from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast hence "?h = 0\<^sub>p" by simp with head_nz[OF np] have "p = 0\<^sub>p" by simp} ultimately show "p = 0\<^sub>p" by blast @@ -1357,8 +1354,8 @@ (polydivide_aux (a,n,p,k,s) = (k',r) \ (k' \ k) \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))" using ns -proof(induct d\"degree s" arbitrary: s k k' r n1 rule: nat_less_induct) - fix d s k k' r n1 +proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct) + case less let ?D = "polydivide_aux_dom" let ?dths = "?D (a, n, p, k, s)" let ?qths = "\q n1. isnpolyh q n1 \ (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" @@ -1366,20 +1363,13 @@ \ (\nr. isnpolyh r nr) \ ?qths" let ?ths = "?dths \ ?qrths" let ?b = "head s" - let ?p' = "funpow (d - n) shift1 p" - let ?xdn = "funpow (d - n) shift1 1\<^sub>p" + let ?p' = "funpow (degree s - n) shift1 p" + let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p" let ?akk' = "a ^\<^sub>p (k' - k)" - assume H: "\mx xa xb xc xd. - isnpolyh x xd \ - m = degree x \ ?D (a, n, p, xa, x) \ - (polydivide_aux (a, n, p, xa, x) = (xb, xc) \ - xa \ xb \ (degree xc = 0 \ degree xc < degree p) \ - (\ nr. isnpolyh xc nr) \ - (\q n1. isnpolyh q n1 \ a ^\<^sub>p xb - xa *\<^sub>p x = p *\<^sub>p q +\<^sub>p xc))" - and ns: "isnpolyh s n1" and ds: "d = degree s" + note ns = `isnpolyh s n1` from np have np0: "isnpolyh p 0" using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp - have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="d -n"] isnpoly_def by simp + have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def by simp have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def) from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap @@ -1391,31 +1381,31 @@ hence ?ths using dom by blast} moreover {assume sz: "s \ 0\<^sub>p" - {assume dn: "d < n" - with sz ds have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) - from polydivide_aux.psimps[OF dom] sz dn ds + {assume dn: "degree s < n" + with sz have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) + from polydivide_aux.psimps[OF dom] sz dn have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp) with dom have ?ths by blast} moreover - {assume dn': "\ d < n" hence dn: "d \ n" by arith + {assume dn': "\ degree s < n" hence dn: "degree s \ n" by arith have degsp': "degree s = degree ?p'" - using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp + using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp {assume ba: "?b = a" hence headsp': "head s = head ?p'" using ap headp' by simp have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp - from ds degree_polysub_samehead[OF ns np' headsp' degsp'] - have "degree (s -\<^sub>p ?p') < d \ s -\<^sub>p ?p' = 0\<^sub>p" by simp + from degree_polysub_samehead[OF ns np' headsp' degsp'] + have "degree (s -\<^sub>p ?p') < degree s \ s -\<^sub>p ?p' = 0\<^sub>p" by simp moreover - {assume deglt:"degree (s -\<^sub>p ?p') < d" - from H[rule_format, OF deglt nr,simplified] + {assume deglt:"degree (s -\<^sub>p ?p') < degree s" + from less(1)[OF deglt nr] have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast have dom: ?dths apply (rule polydivide_aux_real_domintros) - using ba ds dn' domsp by simp_all - from polydivide_aux.psimps[OF dom] sz dn' ba ds + using ba dn' domsp by simp_all + from polydivide_aux.psimps[OF dom] sz dn' ba have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')" by (simp add: Let_def) {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)" - from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified] + from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1] have kk': "k \ k'" and nr:"\nr. isnpolyh r nr" and dr: "degree r = 0 \ degree r < degree p" and q1:"\q nq. isnpolyh q nq \ (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto @@ -1434,19 +1424,19 @@ Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" by (simp add: ring_simps) hence " \(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) + Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) + Ipoly bs p * Ipoly bs q + Ipoly bs r" by (auto simp only: funpow_shift1_1) hence "\(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) + Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps) hence "\(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp + Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp with isnpolyh_unique[OF nakks' nqr'] have "a ^\<^sub>p (k' - k) *\<^sub>p s = - p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast + p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast hence ?qths using nq' - apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI) + apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI) apply (rule_tac x="0" in exI) by simp with kk' nr dr have "k \ k' \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ ?qths" by blast } hence ?qrths by blast @@ -1456,25 +1446,23 @@ hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" apply (simp) by (rule polydivide_aux_real_domintros, simp_all) have dom: ?dths apply (rule polydivide_aux_real_domintros) - using ba ds dn' domsp by simp_all + using ba dn' domsp by simp_all from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"] have " \(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp hence "\(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp by (simp only: funpow_shift1_1) simp hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)" - from polydivide_aux.psimps[OF dom] sz dn' ba ds + from polydivide_aux.psimps[OF dom] sz dn' ba have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')" by (simp add: Let_def) also have "\ = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp - with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] + with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths apply auto apply (rule exI[where x="?xdn"]) - apply auto - apply (rule polymul_commute) - apply simp_all + apply (auto simp add: polymul_commute[of p]) done} with dom have ?ths by blast} ultimately have ?ths by blast } @@ -1488,31 +1476,30 @@ polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] funpow_shift1_nz[OF pnz] by simp_all from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz - polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"] + polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"] have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" using head_head[OF ns] funpow_shift1_head[OF np pnz] polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] by (simp add: ap) from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] head_nz[OF np] pnz sz ap[symmetric] - funpow_shift1_nz[OF pnz, where n="d - n"] + funpow_shift1_nz[OF pnz, where n="degree s - n"] polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns] - ndp ds[symmetric] dn + ndp dn have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') " by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree) - {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d" + {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s" have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))" - using H[rule_format, OF dth nth, simplified] by blast - have dom: ?dths - using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros) - using ba ds dn' by simp_all + using less(1)[OF dth nth] by blast + have dom: ?dths using ba dn' th + by - (rule polydivide_aux_real_domintros, simp_all) from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']] ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)" - from h1 polydivide_aux.psimps[OF dom] sz dn' ba ds + from h1 polydivide_aux.psimps[OF dom] sz dn' ba have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)" by (simp add: Let_def) - with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"] + with less(1)[OF dth nasbp', of "Suc k" k' r] obtain q nq nr where kk': "Suc k \ k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" and dr: "degree r = 0 \ degree r < degree p" and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto @@ -1524,7 +1511,7 @@ hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" by (simp add: ring_simps power_Suc) hence "Ipoly bs a ^ (k' - k) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" - by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"]) + by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" by (simp add: ring_simps)} hence ieq:"\(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = @@ -1546,13 +1533,13 @@ {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" apply (simp) by (rule polydivide_aux_real_domintros, simp_all) - have dom: ?dths using sz ba dn' ds domsp + have dom: ?dths using sz ba dn' domsp by - (rule polydivide_aux_real_domintros, simp_all) {fix bs :: "'a::{ring_char_0,division_by_zero,field} list" from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" - by (simp add: funpow_shift1_1[where n="d - n" and p="p"]) + by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp } hence hth: "\ (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. @@ -1562,7 +1549,7 @@ polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], simplified ap] by simp {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)" - from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] + from h1 sz ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def) with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq @@ -1573,7 +1560,7 @@ hence ?qrths by blast with dom have ?ths by blast} ultimately have ?ths using degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] - head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] + head_nz[OF np] pnz sz ap[symmetric] by (simp add: degree_eq_degreen0[symmetric]) blast } ultimately have ?ths by blast } diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Extraction.thy Wed Jan 20 10:38:19 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Extraction.thy - ID: $Id$ Author: Stefan Berghofer, TU Muenchen *) @@ -28,11 +27,13 @@ allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 notE' impE' impE iffE imp_cong simp_thms eq_True eq_False induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq - induct_atomize induct_rulify induct_rulify_fallback + induct_atomize induct_atomize' induct_rulify induct_rulify' + induct_rulify_fallback induct_trueI True_implies_equals TrueE lemmas [extraction_expand_def] = induct_forall_def induct_implies_def induct_equal_def induct_conj_def + induct_true_def induct_false_def datatype sumbool = Left | Right diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/GCD.thy Wed Jan 20 10:38:19 2010 +0100 @@ -16,7 +16,7 @@ another extension of the notions to the integers, and added a number of results to "Primes" and "GCD". IntPrimes also defined and developed the congruence relations on the integers. The notion was extended to -the natural numbers by Chiaeb. +the natural numbers by Chaieb. Jeremy Avigad combined all of these, made everything uniform for the natural numbers and the integers, and added a number of new theorems. @@ -25,7 +25,7 @@ *) -header {* Greates common divisor and least common multiple *} +header {* Greatest common divisor and least common multiple *} theory GCD imports Fact Parity @@ -1074,34 +1074,35 @@ assumes c: " \a b. P (a::nat) b \ P b a" and z: "\a. P a 0" and add: "\a b. P a b \ P a (a + b)" shows "P a b" -proof(induct n\"a+b" arbitrary: a b rule: nat_less_induct) - fix n a b - assume H: "\m < n. \a b. m = a + b \ P a b" "n = a + b" +proof(induct "a + b" arbitrary: a b rule: less_induct) + case less have "a = b \ a < b \ b < a" by arith moreover {assume eq: "a= b" from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp} moreover {assume lt: "a < b" - hence "a + b - a < n \ a = 0" using H(2) by arith + hence "a + b - a < a + b \ a = 0" by arith moreover {assume "a =0" with z c have "P a b" by blast } moreover - {assume ab: "a + b - a < n" - have th0: "a + b - a = a + (b - a)" using lt by arith - from add[rule_format, OF H(1)[rule_format, OF ab th0]] - have "P a b" by (simp add: th0[symmetric])} + {assume "a + b - a < a + b" + also have th0: "a + b - a = a + (b - a)" using lt by arith + finally have "a + (b - a) < a + b" . + then have "P a (a + (b - a))" by (rule add[rule_format, OF less]) + then have "P a b" by (simp add: th0[symmetric])} ultimately have "P a b" by blast} moreover {assume lt: "a > b" - hence "b + a - b < n \ b = 0" using H(2) by arith + hence "b + a - b < a + b \ b = 0" by arith moreover {assume "b =0" with z c have "P a b" by blast } moreover - {assume ab: "b + a - b < n" - have th0: "b + a - b = b + (a - b)" using lt by arith - from add[rule_format, OF H(1)[rule_format, OF ab th0]] - have "P b a" by (simp add: th0[symmetric]) + {assume "b + a - b < a + b" + also have th0: "b + a - b = b + (a - b)" using lt by arith + finally have "b + (a - b) < a + b" . + then have "P b (b + (a - b))" by (rule add[rule_format, OF less]) + then have "P b a" by (simp add: th0[symmetric]) hence "P a b" using c by blast } ultimately have "P a b" by blast} ultimately show "P a b" by blast diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/HOL.thy Wed Jan 20 10:38:19 2010 +0100 @@ -1398,6 +1398,8 @@ induct_implies where "induct_implies A B == A \ B" induct_equal where "induct_equal x y == x = y" induct_conj where "induct_conj A B == A \ B" + induct_true where "induct_true == True" + induct_false where "induct_false == False" lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\x. P x))" by (unfold atomize_all induct_forall_def) @@ -1411,10 +1413,13 @@ lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)" by (unfold atomize_conj induct_conj_def) -lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq +lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq +lemmas induct_atomize = induct_atomize' induct_equal_eq +lemmas induct_rulify' [symmetric, standard] = induct_atomize' lemmas induct_rulify [symmetric, standard] = induct_atomize lemmas induct_rulify_fallback = induct_forall_def induct_implies_def induct_equal_def induct_conj_def + induct_true_def induct_false_def lemma induct_forall_conj: "induct_forall (\x. induct_conj (A x) (B x)) = @@ -1436,7 +1441,8 @@ lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry -hide const induct_forall induct_implies induct_equal induct_conj +lemma induct_trueI: "induct_true" + by (simp add: induct_true_def) text {* Method setup. *} @@ -1445,12 +1451,93 @@ ( val cases_default = @{thm case_split} val atomize = @{thms induct_atomize} - val rulify = @{thms induct_rulify} + val rulify = @{thms induct_rulify'} val rulify_fallback = @{thms induct_rulify_fallback} + fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u) + | dest_def _ = NONE + val trivial_tac = match_tac @{thms induct_trueI} ) *} -setup Induct.setup +setup {* + Induct.setup #> + Context.theory_map (Induct.map_simpset (fn ss => ss + setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #> + map (Simplifier.rewrite_rule (map Thm.symmetric + @{thms induct_rulify_fallback induct_true_def induct_false_def}))) + addsimprocs + [Simplifier.simproc @{theory} "swap_induct_false" + ["induct_false ==> PROP P ==> PROP Q"] + (fn _ => fn _ => + (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) => + if P <> Q then SOME Drule.swap_prems_eq else NONE + | _ => NONE)), + Simplifier.simproc @{theory} "induct_equal_conj_curry" + ["induct_conj P Q ==> PROP R"] + (fn _ => fn _ => + (fn _ $ (_ $ P) $ _ => + let + fun is_conj (@{const induct_conj} $ P $ Q) = + is_conj P andalso is_conj Q + | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true + | is_conj @{const induct_true} = true + | is_conj @{const induct_false} = true + | is_conj _ = false + in if is_conj P then SOME @{thm induct_conj_curry} else NONE end + | _ => NONE))])) +*} + +text {* Pre-simplification of induction and cases rules *} + +lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == 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]) +next + 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" + unfolding induct_equal_def +proof + assume R: "!!x. t = x ==> PROP P x" + show "PROP P t" by (rule R [OF refl]) +next + 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" + unfolding induct_false_def induct_true_def + by (iprover intro: equal_intr_rule) + +lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P" + unfolding induct_true_def +proof + assume R: "True \ PROP P" + from TrueI show "PROP P" by (rule R) +next + assume "PROP P" + then show "PROP P" . +qed + +lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true" + unfolding induct_true_def + by (iprover intro: equal_intr_rule) + +lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true" + unfolding induct_true_def + by (iprover intro: equal_intr_rule) + +lemma [induct_simp]: "induct_implies induct_true P == P" + by (simp add: induct_implies_def induct_true_def) + +lemma [induct_simp]: "(x = x) = True" + by (rule simp_thms) + +hide const induct_forall induct_implies induct_equal induct_conj induct_true induct_false use "~~/src/Tools/induct_tacs.ML" setup InductTacs.setup diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Induct/Common_Patterns.thy --- a/src/HOL/Induct/Common_Patterns.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Induct/Common_Patterns.thy Wed Jan 20 10:38:19 2010 +0100 @@ -73,7 +73,7 @@ show "P (a x)" sorry next case (Suc n) - note hyp = `\x. A (a x) \ n = a x \ P (a x)` + note hyp = `\x. n = a x \ A (a x) \ P (a x)` and prem = `A (a x)` and defn = `Suc n = a x` show "P (a x)" sorry diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Isar_Examples/Puzzle.thy --- a/src/HOL/Isar_Examples/Puzzle.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Isar_Examples/Puzzle.thy Wed Jan 20 10:38:19 2010 +0100 @@ -22,17 +22,16 @@ proof (rule order_antisym) { fix n show "n \ f n" - proof (induct k \ "f n" arbitrary: n rule: less_induct) - case (less k n) - then have hyp: "\m. f m < f n \ m \ f m" by (simp only:) + proof (induct "f n" arbitrary: n rule: less_induct) + case less show "n \ f n" proof (cases n) case (Suc m) from f_ax have "f (f m) < f n" by (simp only: Suc) - with hyp have "f m \ f (f m)" . + with less have "f m \ f (f m)" . also from f_ax have "\ < f n" by (simp only: Suc) finally have "f m < f n" . - with hyp have "m \ f m" . + with less have "m \ f m" . also note `\ < f n` finally have "m < f n" . then have "n \ f n" by (simp only: Suc) diff -r c4f04bee79f3 -r fb90752a9271 src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Wed Jan 20 10:38:06 2010 +0100 +++ b/src/HOL/Library/Code_Integer.thy Wed Jan 20 10:38:19 2010 +0100 @@ -18,13 +18,16 @@ (SML "IntInf.int") (OCaml "Big'_int.big'_int") (Haskell "Integer") + (Scala "BigInt") code_instance int :: eq (Haskell -) setup {* fold (Numeral.add_code @{const_name number_int_inst.number_of_int} - true true) ["SML", "OCaml", "Haskell"] + true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"] + #> Numeral.add_code @{const_name number_int_inst.number_of_int} + true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala" *} code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1" @@ -40,63 +43,80 @@ and "error/ \"Min\"" and "error/ \"Bit0\"" and "error/ \"Bit1\"") + (Scala "!error(\"Pls\")" + and "!error(\"Min\")" + and "!error(\"Bit0\")" + and "!error(\"Bit1\")") + code_const Int.pred (SML "IntInf.- ((_), 1)") (OCaml "Big'_int.pred'_big'_int") (Haskell "!(_/ -/ 1)") + (Scala "!(_/ -/ 1)") code_const Int.succ (SML "IntInf.+ ((_), 1)") (OCaml "Big'_int.succ'_big'_int") (Haskell "!(_/ +/ 1)") + (Scala "!(_/ +/ 1)") code_const "op + \ int \ int \ int" (SML "IntInf.+ ((_), (_))") (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") + (Scala infixl 7 "+") code_const "uminus \ int \ int" (SML "IntInf.~") (OCaml "Big'_int.minus'_big'_int") (Haskell "negate") + (Scala "!(- _)") code_const "op - \ int \ int \ int" (SML "IntInf.- ((_), (_))") (OCaml "Big'_int.sub'_big'_int") (Haskell infixl 6 "-") + (Scala infixl 7 "-") code_const "op * \ int \ int \ int" (SML "IntInf.* ((_), (_))") (OCaml "Big'_int.mult'_big'_int") (Haskell infixl 7 "*") + (Scala infixl 8 "*") code_const pdivmod - (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))") - (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))") - (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))") + (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") + (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") + (Haskell "divMod/ (abs _)/ (abs _))") + (Scala "!(_.abs '/% _.abs)") code_const "eq_class.eq \ int \ int \