# HG changeset patch # User haftmann # Date 1264062477 -3600 # Node ID d62eddd9e253814e1d28ee0d0e32b1c02582f352 # Parent f4d3daddac42c2fe2337920de7c48ac3941209cc# Parent 156925dd67af736ebe1abb20241d1851ff51bcd7 merged diff -r 156925dd67af -r d62eddd9e253 NEWS --- a/NEWS Sat Jan 16 17:15:28 2010 +0100 +++ b/NEWS Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/FOL/FOL.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Bali/Basis.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Bali/DeclConcepts.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Bali/WellForm.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Code_Numeral.thy Thu Jan 21 09:27:57 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 diff -r 156925dd67af -r d62eddd9e253 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jan 21 09:27:57 2010 +0100 @@ -987,16 +987,14 @@ assumes nq: "isnpolyh p n0" and eq :"\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 156925dd67af -r d62eddd9e253 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Extraction.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/GCD.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/HOL.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Induct/Common_Patterns.thy --- a/src/HOL/Induct/Common_Patterns.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Induct/Common_Patterns.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Isar_Examples/Puzzle.thy --- a/src/HOL/Isar_Examples/Puzzle.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Isar_Examples/Puzzle.thy Thu Jan 21 09:27:57 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 156925dd67af -r d62eddd9e253 src/HOL/Library/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Thu Jan 21 09:27:57 2010 +0100 @@ -621,19 +621,18 @@ done qed -text{* Fundamental theorem of algebral *} +text{* Fundamental theorem of algebra *} lemma fundamental_theorem_of_algebra: assumes nc: "~constant(poly p)" shows "\z::complex. poly p z = 0" using nc -proof(induct n\ "psize p" arbitrary: p rule: nat_less_induct) - fix n fix p :: "complex poly" +proof(induct "psize p" arbitrary: p rule: less_induct) + case less let ?p = "poly p" - assume H: "\mp. \ constant (poly p) \ m = psize p \ (\(z::complex). poly p z = 0)" and nc: "\ constant ?p" and n: "n = psize p" let ?ths = "\z. ?p z = 0" - from nonconstant_length[OF nc] have n2: "n\ 2" by (simp add: n) + from nonconstant_length[OF less(2)] have n2: "psize p \ 2" . from poly_minimum_modulus obtain c where c: "\w. cmod (?p c) \ cmod (?p w)" by blast {assume pc: "?p c = 0" hence ?ths by blast} @@ -649,7 +648,7 @@ using h unfolding constant_def by blast also have "\ = ?p y" using th by auto finally have "?p x = ?p y" .} - with nc have False unfolding constant_def by blast } + with less(2) have False unfolding constant_def by blast } hence qnc: "\ constant (poly q)" by blast from q(2) have pqc0: "?p c = poly q 0" by simp from c pqc0 have cq0: "\w. cmod (poly q 0) \ cmod (?p w)" by simp @@ -682,8 +681,8 @@ from poly_decompose[OF rnc] obtain k a s where kas: "a\0" "k\0" "psize s + k + 1 = psize ?r" "\z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast - {assume "k + 1 = n" - with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto + {assume "psize p = k + 1" + with kas(3) lgqr[symmetric] q(1) have s0:"s=0" by auto {fix w have "cmod (poly ?r w) = cmod (1 + a * w ^ k)" using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)} @@ -691,15 +690,15 @@ from reduce_poly_simple[OF kas(1,2)] have "\w. cmod (poly ?r w) < 1" unfolding hth by blast} moreover - {assume kn: "k+1 \ n" - from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp + {assume kn: "psize p \ k+1" + from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p" by simp have th01: "\ constant (poly (pCons 1 (monom a (k - 1))))" unfolding constant_def poly_pCons poly_monom using kas(1) apply simp by (rule exI[where x=0], rule exI[where x=1], simp) from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))" by (simp add: psize_def degree_monom_eq) - from H[rule_format, OF k1n th01 th02] + from less(1) [OF k1n [simplified th02] th01] obtain w where w: "1 + w^k * a = 0" unfolding poly_pCons poly_monom using kas(2) by (cases k, auto simp add: algebra_simps) diff -r 156925dd67af -r d62eddd9e253 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Library/Polynomial.thy Thu Jan 21 09:27:57 2010 +0100 @@ -1384,7 +1384,7 @@ with k have "degree p = Suc (degree k)" by (simp add: degree_mult_eq del: mult_pCons_left) with `Suc n = degree p` have "n = degree k" by simp - with `k \ 0` have "finite {x. poly k x = 0}" by (rule Suc.hyps) + then have "finite {x. poly k x = 0}" using `k \ 0` by (rule Suc.hyps) then have "finite (insert a {x. poly k x = 0})" by simp then show "finite {x. poly p x = 0}" by (simp add: k uminus_add_conv_diff Collect_disj_eq diff -r 156925dd67af -r d62eddd9e253 src/HOL/Library/Transitive_Closure_Table.thy --- a/src/HOL/Library/Transitive_Closure_Table.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Thu Jan 21 09:27:57 2010 +0100 @@ -17,11 +17,11 @@ assume "r\<^sup>*\<^sup>* x y" then show "\xs. rtrancl_path r x xs y" proof (induct rule: converse_rtranclp_induct) - case 1 + case base have "rtrancl_path r y [] y" by (rule rtrancl_path.base) then show ?case .. next - case (2 x z) + case (step x z) from `\xs. rtrancl_path r z xs y` obtain xs where "rtrancl_path r z xs y" .. with `r x z` have "rtrancl_path r x (z # xs) y" diff -r 156925dd67af -r d62eddd9e253 src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Library/Word.thy Thu Jan 21 09:27:57 2010 +0100 @@ -428,7 +428,7 @@ show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" proof - have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2" - by (induct "length xs",simp_all) + by (induct ("length xs")) simp_all hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2" by simp @@ -2155,13 +2155,13 @@ apply (simp add: bv_extend_def) apply (subst bv_to_nat_dist_append) apply simp - apply (induct "n - length w") + apply (induct ("n - length w")) apply simp_all done lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b" apply (simp add: bv_extend_def) - apply (induct "n - length w") + apply (cases "n - length w") apply simp_all done @@ -2178,7 +2178,7 @@ show ?thesis apply (simp add: bv_to_int_def) apply (simp add: bv_extend_def) - apply (induct "n - length w",simp_all) + apply (induct ("n - length w"), simp_all) done qed diff -r 156925dd67af -r d62eddd9e253 src/HOL/List.thy --- a/src/HOL/List.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/List.thy Thu Jan 21 09:27:57 2010 +0100 @@ -577,13 +577,13 @@ apply fastsimp done -lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" +lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" by simp lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \ x = y)" by simp -lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)" +lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" by simp lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" @@ -2382,7 +2382,6 @@ unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map by (simp add: sup_commute) - subsubsection {* List summation: @{const listsum} and @{text"\"}*} lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" @@ -3194,6 +3193,117 @@ apply auto done +subsubsection{*Transpose*} + +function transpose where +"transpose [] = []" | +"transpose ([] # xss) = transpose xss" | +"transpose ((x#xs) # xss) = + (x # [h. (h#t) \ xss]) # transpose (xs # [t. (h#t) \ xss])" +by pat_completeness auto + +lemma transpose_aux_filter_head: + "concat (map (list_case [] (\h t. [h])) xss) = + map (\xs. hd xs) [ys\xss . ys \ []]" + by (induct xss) (auto split: list.split) + +lemma transpose_aux_filter_tail: + "concat (map (list_case [] (\h t. [t])) xss) = + map (\xs. tl xs) [ys\xss . ys \ []]" + by (induct xss) (auto split: list.split) + +lemma transpose_aux_max: + "max (Suc (length xs)) (foldr (\xs. max (length xs)) xss 0) = + Suc (max (length xs) (foldr (\x. max (length x - Suc 0)) [ys\xss . ys\[]] 0))" + (is "max _ ?foldB = Suc (max _ ?foldA)") +proof (cases "[ys\xss . ys\[]] = []") + case True + hence "foldr (\xs. max (length xs)) xss 0 = 0" + proof (induct xss) + case (Cons x xs) + moreover hence "x = []" by (cases x) auto + ultimately show ?case by auto + qed simp + thus ?thesis using True by simp +next + case False + + have foldA: "?foldA = foldr (\x. max (length x)) [ys\xss . ys \ []] 0 - 1" + by (induct xss) auto + have foldB: "?foldB = foldr (\x. max (length x)) [ys\xss . ys \ []] 0" + by (induct xss) auto + + have "0 < ?foldB" + proof - + from False + obtain z zs where zs: "[ys\xss . ys \ []] = z#zs" by (auto simp: neq_Nil_conv) + hence "z \ set ([ys\xss . ys \ []])" by auto + hence "z \ []" by auto + thus ?thesis + unfolding foldB zs + by (auto simp: max_def intro: less_le_trans) + qed + thus ?thesis + unfolding foldA foldB max_Suc_Suc[symmetric] + by simp +qed + +termination transpose + by (relation "measure (\xs. foldr (\xs. max (length xs)) xs 0 + length xs)") + (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max less_Suc_eq_le) + +lemma transpose_empty: "(transpose xs = []) \ (\x \ set xs. x = [])" + by (induct rule: transpose.induct) simp_all + +lemma length_transpose: + fixes xs :: "'a list list" + shows "length (transpose xs) = foldr (\xs. max (length xs)) xs 0" + by (induct rule: transpose.induct) + (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max + max_Suc_Suc[symmetric] simp del: max_Suc_Suc) + +lemma nth_transpose: + fixes xs :: "'a list list" + assumes "i < length (transpose xs)" + shows "transpose xs ! i = map (\xs. xs ! i) [ys \ xs. i < length ys]" +using assms proof (induct arbitrary: i rule: transpose.induct) + case (3 x xs xss) + def XS == "(x # xs) # xss" + hence [simp]: "XS \ []" by auto + thus ?case + proof (cases i) + case 0 + thus ?thesis by (simp add: transpose_aux_filter_head hd_conv_nth) + next + case (Suc j) + have *: "\xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp + have **: "\xss. (x#xs) # filter (\ys. ys \ []) xss = filter (\ys. ys \ []) ((x#xs)#xss)" by simp + { fix x have "Suc j < length x \ x \ [] \ j < length x - Suc 0" + by (cases x) simp_all + } note *** = this + + have j_less: "j < length (transpose (xs # concat (map (list_case [] (\h t. [t])) xss)))" + using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc) + + show ?thesis + unfolding transpose.simps `i = Suc j` nth_Cons_Suc "3.hyps"[OF j_less] + apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric]) + apply (rule_tac y=x in list.exhaust) + by auto + qed +qed simp_all + +lemma transpose_map_map: + "transpose (map (map f) xs) = map (map f) (transpose xs)" +proof (rule nth_equalityI, safe) + have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)" + by (simp add: length_transpose foldr_map comp_def) + show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp + + fix i assume "i < length (transpose (map (map f) xs))" + thus "transpose (map (map f) xs) ! i = map (map f) (transpose xs) ! i" + by (simp add: nth_transpose filter_map comp_def) +qed subsubsection {* (In)finiteness *} @@ -3405,6 +3515,45 @@ lemma sorted_takeWhile: "sorted xs \ sorted (takeWhile P xs)" apply (subst takeWhile_eq_take) by (rule sorted_take) +lemma sorted_filter: + "sorted (map f xs) \ sorted (map f (filter P xs))" + by (induct xs) (simp_all add: sorted_Cons) + +lemma foldr_max_sorted: + assumes "sorted (rev xs)" + shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)" +using assms proof (induct xs) + case (Cons x xs) + moreover hence "sorted (rev xs)" using sorted_append by auto + ultimately show ?case + by (cases xs, auto simp add: sorted_append max_def) +qed simp + +lemma filter_equals_takeWhile_sorted_rev: + assumes sorted: "sorted (rev (map f xs))" + shows "[x \ xs. t < f x] = takeWhile (\ x. t < f x) xs" + (is "filter ?P xs = ?tW") +proof (rule takeWhile_eq_filter[symmetric]) + let "?dW" = "dropWhile ?P xs" + fix x assume "x \ set ?dW" + then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i" + unfolding in_set_conv_nth by auto + hence "length ?tW + i < length (?tW @ ?dW)" + unfolding length_append by simp + hence i': "length (map f ?tW) + i < length (map f xs)" by simp + have "(map f ?tW @ map f ?dW) ! (length (map f ?tW) + i) \ + (map f ?tW @ map f ?dW) ! (length (map f ?tW) + 0)" + using sorted_rev_nth_mono[OF sorted _ i', of "length ?tW"] + unfolding map_append[symmetric] by simp + hence "f x \ f (?dW ! 0)" + unfolding nth_append_length_plus nth_i + using i preorder_class.le_less_trans[OF le0 i] by simp + also have "... \ t" + using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i] + using hd_conv_nth[of "?dW"] by simp + finally show "\ t < f x" by simp +qed + end lemma sorted_upt[simp]: "sorted[i..xs. max (length xs)) (transpose xs) 0 = length [x \ xs. x \ []]" + (is "?L = ?R") +proof (cases "transpose xs = []") + case False + have "?L = foldr max (map length (transpose xs)) 0" + by (simp add: foldr_map comp_def) + also have "... = length (transpose xs ! 0)" + using False sorted_transpose by (simp add: foldr_max_sorted) + finally show ?thesis + using False by (simp add: nth_transpose) +next + case True + hence "[x \ xs. x \ []] = []" + by (auto intro!: filter_False simp: transpose_empty) + thus ?thesis by (simp add: transpose_empty True) +qed + +lemma length_transpose_sorted: + fixes xs :: "'a list list" + assumes sorted: "sorted (rev (map length xs))" + shows "length (transpose xs) = (if xs = [] then 0 else length (xs ! 0))" +proof (cases "xs = []") + case False + thus ?thesis + using foldr_max_sorted[OF sorted] False + unfolding length_transpose foldr_map comp_def + by simp +qed simp + +lemma nth_nth_transpose_sorted[simp]: + fixes xs :: "'a list list" + assumes sorted: "sorted (rev (map length xs))" + and i: "i < length (transpose xs)" + and j: "j < length [ys \ xs. i < length ys]" + shows "transpose xs ! i ! j = xs ! j ! i" + using j filter_equals_takeWhile_sorted_rev[OF sorted, of i] + nth_transpose[OF i] nth_map[OF j] + by (simp add: takeWhile_nth) + +lemma transpose_column_length: + fixes xs :: "'a list list" + assumes sorted: "sorted (rev (map length xs))" and "i < length xs" + shows "length (filter (\ys. i < length ys) (transpose xs)) = length (xs ! i)" +proof - + have "xs \ []" using `i < length xs` by auto + note filter_equals_takeWhile_sorted_rev[OF sorted, simp] + { fix j assume "j \ i" + note sorted_rev_nth_mono[OF sorted, of j i, simplified, OF this `i < length xs`] + } note sortedE = this[consumes 1] + + have "{j. j < length (transpose xs) \ i < length (transpose xs ! j)} + = {..< length (xs ! i)}" + proof safe + fix j + assume "j < length (transpose xs)" and "i < length (transpose xs ! j)" + with this(2) nth_transpose[OF this(1)] + have "i < length (takeWhile (\ys. j < length ys) xs)" by simp + from nth_mem[OF this] takeWhile_nth[OF this] + show "j < length (xs ! i)" by (auto dest: set_takeWhileD) + next + fix j assume "j < length (xs ! i)" + thus "j < length (transpose xs)" + using foldr_max_sorted[OF sorted] `xs \ []` sortedE[OF le0] + by (auto simp: length_transpose comp_def foldr_map) + + have "Suc i \ length (takeWhile (\ys. j < length ys) xs)" + using `i < length xs` `j < length (xs ! i)` less_Suc_eq_le + by (auto intro!: length_takeWhile_less_P_nth dest!: sortedE) + with nth_transpose[OF `j < length (transpose xs)`] + show "i < length (transpose xs ! j)" by simp + qed + thus ?thesis by (simp add: length_filter_conv_card) +qed + +lemma transpose_column: + fixes xs :: "'a list list" + assumes sorted: "sorted (rev (map length xs))" and "i < length xs" + shows "map (\ys. ys ! i) (filter (\ys. i < length ys) (transpose xs)) + = xs ! i" (is "?R = _") +proof (rule nth_equalityI, safe) + show length: "length ?R = length (xs ! i)" + using transpose_column_length[OF assms] by simp + + fix j assume j: "j < length ?R" + note * = less_le_trans[OF this, unfolded length_map, OF length_filter_le] + from j have j_less: "j < length (xs ! i)" using length by simp + have i_less_tW: "Suc i \ length (takeWhile (\ys. Suc j \ length ys) xs)" + proof (rule length_takeWhile_less_P_nth) + show "Suc i \ length xs" using `i < length xs` by simp + fix k assume "k < Suc i" + hence "k \ i" by auto + with sorted_rev_nth_mono[OF sorted this] `i < length xs` + have "length (xs ! i) \ length (xs ! k)" by simp + thus "Suc j \ length (xs ! k)" using j_less by simp + qed + have i_less_filter: "i < length [ys\xs . j < length ys]" + unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j] + using i_less_tW by (simp_all add: Suc_le_eq) + from j show "?R ! j = xs ! i ! j" + unfolding filter_equals_takeWhile_sorted_rev[OF sorted_transpose, of i] + by (simp add: takeWhile_nth nth_nth_transpose_sorted[OF sorted * i_less_filter]) +qed + +lemma transpose_transpose: + fixes xs :: "'a list list" + assumes sorted: "sorted (rev (map length xs))" + shows "transpose (transpose xs) = takeWhile (\x. x \ []) xs" (is "?L = ?R") +proof - + have len: "length ?L = length ?R" + unfolding length_transpose transpose_max_length + using filter_equals_takeWhile_sorted_rev[OF sorted, of 0] + by simp + + { fix i assume "i < length ?R" + with less_le_trans[OF _ length_takeWhile_le[of _ xs]] + have "i < length xs" by simp + } note * = this + show ?thesis + by (rule nth_equalityI) + (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth) +qed + +theorem transpose_rectangle: + assumes "xs = [] \ n = 0" + assumes rect: "\ i. i < length xs \ length (xs ! i) = n" + shows "transpose xs = map (\ i. map (\ j. xs ! j ! i) [0..xs . i < length ys] = xs" + using rect by (auto simp: in_set_conv_nth intro!: filter_True) } + ultimately show "\i < length ?trans. ?trans ! i = ?map ! i" + by (auto simp: nth_transpose intro: nth_equalityI) +qed subsubsection {* @{text sorted_list_of_set} *} @@ -3448,7 +3744,6 @@ end - subsubsection {* @{text lists}: the list-forming operator over sets *} inductive_set diff -r 156925dd67af -r d62eddd9e253 src/HOL/MicroJava/BV/EffectMono.thy --- a/src/HOL/MicroJava/BV/EffectMono.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/MicroJava/BV/EffectMono.thy Thu Jan 21 09:27:57 2010 +0100 @@ -15,12 +15,13 @@ lemma sup_loc_some [rule_format]: "\y n. (G \ b <=l y) \ n < length y \ y!n = OK t \ - (\t. b!n = OK t \ (G \ (b!n) <=o (y!n)))" (is "?P b") -proof (induct ?P b) - show "?P []" by simp + (\t. b!n = OK t \ (G \ (b!n) <=o (y!n)))" +proof (induct b) + case Nil + show ?case by simp next case (Cons a list) - show "?P (a#list)" + show ?case proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def) fix z zs n assume *: @@ -60,13 +61,14 @@ lemma append_length_n [rule_format]: -"\n. n \ length x \ (\a b. x = a@b \ length a = n)" (is "?P x") -proof (induct ?P x) - show "?P []" by simp +"\n. n \ length x \ (\a b. x = a@b \ length a = n)" +proof (induct x) + case Nil + show ?case by simp next - fix l ls assume Cons: "?P ls" + case (Cons l ls) - show "?P (l#ls)" + show ?case proof (intro allI impI) fix n assume l: "n \ length (l # ls)" diff -r 156925dd67af -r d62eddd9e253 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 21 09:27:57 2010 +0100 @@ -170,8 +170,8 @@ next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s) case (Suc n) fix s::"'a set" and u::"'a \ real" assume IA:"\u s. \2 < card s; \x\V. \y\V. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ V; finite s; - s \ {}; s \ V; setsum u s = 1; n \ card s \ \ (\x\s. u x *\<^sub>R x) \ V" and - as:"Suc n \ card s" "2 < card s" "\x\V. \y\V. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ V" + s \ {}; s \ V; setsum u s = 1; n = card s \ \ (\x\s. u x *\<^sub>R x) \ V" and + as:"Suc n = card s" "2 < card s" "\x\V. \y\V. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ V" "finite s" "s \ {}" "s \ V" "setsum u s = 1" have "\x\s. u x \ 1" proof(rule_tac ccontr) assume " \ (\x\s. u x \ 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto @@ -1345,7 +1345,7 @@ next case False then obtain w where "w\s" by auto show ?thesis unfolding caratheodory[of s] - proof(induct "CARD('n) + 1") + proof(induct ("CARD('n) + 1")) have *:"{x.\sa. finite sa \ sa \ s \ card sa \ 0 \ x \ convex hull sa} = {}" using compact_empty by (auto simp add: convex_hull_empty) case 0 thus ?case unfolding * by simp diff -r 156925dd67af -r d62eddd9e253 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Jan 21 09:27:57 2010 +0100 @@ -3542,17 +3542,9 @@ and sp:"s \ span t" shows "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" using f i sp -proof(induct c\"card(t - s)" arbitrary: s t rule: nat_less_induct) - fix n:: nat and s t :: "('a ^'n) set" - assume H: " \m(x:: ('a ^'n) set) xa. - finite xa \ - independent x \ - x \ span xa \ - m = card (xa - x) \ - (\t'. (card t' = card xa) \ finite t' \ - x \ t' \ t' \ x \ xa \ x \ span t')" - and ft: "finite t" and s: "independent s" and sp: "s \ span t" - and n: "n = card (t - s)" +proof(induct "card (t - s)" arbitrary: s t rule: less_induct) + case less + note ft = `finite t` and s = `independent s` and sp = `s \ span t` let ?P = "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" let ?ths = "\t'. ?P t'" {assume st: "s \ t" @@ -3568,12 +3560,12 @@ {assume st: "\ s \ t" "\ t \ s" from st(2) obtain b where b: "b \ t" "b \ s" by blast from b have "t - {b} - s \ t - s" by blast - then have cardlt: "card (t - {b} - s) < n" using n ft + then have cardlt: "card (t - {b} - s) < card (t - s)" using ft by (auto intro: psubset_card_mono) from b ft have ct0: "card t \ 0" by auto {assume stb: "s \ span(t -{b})" from ft have ftb: "finite (t -{b})" by auto - from H[rule_format, OF cardlt ftb s stb] + from less(1)[OF cardlt ftb s stb] obtain u where u: "card u = card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" and fu: "finite u" by blast let ?w = "insert b u" have th0: "s \ insert b u" using u by blast @@ -3594,8 +3586,8 @@ from stb obtain a where a: "a \ s" "a \ span (t - {b})" by blast have ab: "a \ b" using a b by blast have at: "a \ t" using a ab span_superset[of a "t- {b}"] by auto - have mlt: "card ((insert a (t - {b})) - s) < n" - using cardlt ft n a b by auto + have mlt: "card ((insert a (t - {b})) - s) < card (t - s)" + using cardlt ft a b by auto have ft': "finite (insert a (t - {b}))" using ft by auto {fix x assume xs: "x \ s" have t: "t \ (insert b (insert a (t -{b})))" using b by auto @@ -3608,7 +3600,7 @@ from span_trans[OF bs x] have "x \ span (insert a (t - {b}))" .} then have sp': "s \ span (insert a (t - {b}))" by blast - from H[rule_format, OF mlt ft' s sp' refl] obtain u where + from less(1)[OF mlt ft' s sp'] obtain u where u: "card u = card (insert a (t -{b}))" "finite u" "s \ u" "u \ s \ insert a (t -{b})" "s \ span u" by blast from u a b ft at ct0 have "?P u" by auto @@ -3657,11 +3649,9 @@ assumes sv: "(S::(real^'n) set) \ V" and iS: "independent S" shows "\B. S \ B \ B \ V \ independent B \ V \ span B" using sv iS -proof(induct d\ "CARD('n) - card S" arbitrary: S rule: nat_less_induct) - fix n and S:: "(real^'n) set" - assume H: "\mS \ V. independent S \ m = CARD('n) - card S \ - (\B. S \ B \ B \ V \ independent B \ V \ span B)" - and sv: "S \ V" and i: "independent S" and n: "n = CARD('n) - card S" +proof(induct "CARD('n) - card S" arbitrary: S rule: less_induct) + case less + note sv = `S \ V` and i = `independent S` let ?P = "\B. S \ B \ B \ V \ independent B \ V \ span B" let ?ths = "\x. ?P x" let ?d = "CARD('n)" @@ -3674,11 +3664,11 @@ have th0: "insert a S \ V" using a sv by blast from independent_insert[of a S] i a have th1: "independent (insert a S)" by auto - have mlt: "?d - card (insert a S) < n" - using aS a n independent_bound[OF th1] + have mlt: "?d - card (insert a S) < ?d - card S" + using aS a independent_bound[OF th1] by auto - from H[rule_format, OF mlt th0 th1 refl] + from less(1)[OF mlt th0 th1] obtain B where B: "insert a S \ B" "B \ V" "independent B" " V \ span B" by blast from B have "?P B" by auto diff -r 156925dd67af -r d62eddd9e253 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Nitpick.thy Thu Jan 21 09:27:57 2010 +0100 @@ -29,10 +29,13 @@ typedecl bisim_iterator axiomatization unknown :: 'a + and is_unknown :: "'a \ bool" and undefined_fast_The :: 'a and undefined_fast_Eps :: 'a and bisim :: "bisim_iterator \ 'a \ 'a \ bool" and bisim_iterator_max :: bisim_iterator + and Quot :: "'a \ 'b" + and quot_normal :: "'a \ 'a" and Tha :: "('a \ bool) \ 'a" datatype ('a, 'b) pair_box = PairBox 'a 'b @@ -246,11 +249,12 @@ setup {* Nitpick_Isar.setup *} -hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim - bisim_iterator_max Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec' - wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac - Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac - times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac +hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim + bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf' + wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd + int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac + plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac + of_frac hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def diff -r 156925dd67af -r d62eddd9e253 src/HOL/Nominal/Examples/Class.thy --- a/src/HOL/Nominal/Examples/Class.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Nominal/Examples/Class.thy Thu Jan 21 09:27:57 2010 +0100 @@ -15069,11 +15069,9 @@ assumes a: "(M[a\c>b]) \\<^isub>a M'" "a\b" shows "\M0. M0[a\c>b]=M' \ M \\<^isub>a M0" using a -apply(nominal_induct M\"M[a\c>b]" M' avoiding: M a b rule: a_redu.strong_induct) -apply(simp) +apply(nominal_induct "M[a\c>b]" M' avoiding: M a b rule: a_redu.strong_induct) apply(drule crename_lredu) apply(blast) -apply(simp) apply(drule crename_credu) apply(blast) (* Cut *) @@ -16132,11 +16130,9 @@ assumes a: "(M[x\n>y]) \\<^isub>a M'" "x\y" shows "\M0. M0[x\n>y]=M' \ M \\<^isub>a M0" using a -apply(nominal_induct M\"M[x\n>y]" M' avoiding: M x y rule: a_redu.strong_induct) -apply(simp) +apply(nominal_induct "M[x\n>y]" M' avoiding: M x y rule: a_redu.strong_induct) apply(drule nrename_lredu) apply(blast) -apply(simp) apply(drule nrename_credu) apply(blast) (* Cut *) diff -r 156925dd67af -r d62eddd9e253 src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Nominal/Examples/Fsub.thy Thu Jan 21 09:27:57 2010 +0100 @@ -982,19 +982,18 @@ from `(\@[(TVarB X Q)]@\) \ M <: N` and `\ \ P<:Q` show "(\@[(TVarB X P)]@\) \ M <: N" - proof (induct \\"\@[(TVarB X Q)]@\" M N arbitrary: \ X \ rule: subtype_of.induct) - case (SA_Top _ S \ X \) - then have lh_drv_prm\<^isub>1: "\ (\@[(TVarB X Q)]@\) ok" - and lh_drv_prm\<^isub>2: "S closed_in (\@[(TVarB X Q)]@\)" by simp_all - have rh_drv: "\ \ P <: Q" by fact - hence "P closed_in \" by (simp add: subtype_implies_closed) - with lh_drv_prm\<^isub>1 have "\ (\@[(TVarB X P)]@\) ok" by (simp add: replace_type) + proof (induct "\@[(TVarB X Q)]@\" M N arbitrary: \ X \ rule: subtype_of.induct) + case (SA_Top S \ X \) + from `\ \ P <: Q` + have "P closed_in \" by (simp add: subtype_implies_closed) + with `\ (\@[(TVarB X Q)]@\) ok` have "\ (\@[(TVarB X P)]@\) ok" + by (simp add: replace_type) moreover - from lh_drv_prm\<^isub>2 have "S closed_in (\@[(TVarB X P)]@\)" + from `S closed_in (\@[(TVarB X Q)]@\)` have "S closed_in (\@[(TVarB X P)]@\)" by (simp add: closed_in_def doms_append) ultimately show "(\@[(TVarB X P)]@\) \ S <: Top" by (simp add: subtype_of.SA_Top) next - case (SA_trans_TVar Y S _ N \ X \) + case (SA_trans_TVar Y S N \ X \) then have IH_inner: "(\@[(TVarB X P)]@\) \ S <: N" and lh_drv_prm: "(TVarB Y S) \ set (\@[(TVarB X Q)]@\)" and rh_drv: "\ \ P<:Q" @@ -1020,23 +1019,23 @@ then show "(\@[(TVarB X P)]@\) \ Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto qed next - case (SA_refl_TVar _ Y \ X \) - then have lh_drv_prm\<^isub>1: "\ (\@[(TVarB X Q)]@\) ok" - and lh_drv_prm\<^isub>2: "Y \ ty_dom (\@[(TVarB X Q)]@\)" by simp_all - have "\ \ P <: Q" by fact - hence "P closed_in \" by (simp add: subtype_implies_closed) - with lh_drv_prm\<^isub>1 have "\ (\@[(TVarB X P)]@\) ok" by (simp add: replace_type) + case (SA_refl_TVar Y \ X \) + from `\ \ P <: Q` + have "P closed_in \" by (simp add: subtype_implies_closed) + with `\ (\@[(TVarB X Q)]@\) ok` have "\ (\@[(TVarB X P)]@\) ok" + by (simp add: replace_type) moreover - from lh_drv_prm\<^isub>2 have "Y \ ty_dom (\@[(TVarB X P)]@\)" by (simp add: doms_append) + from `Y \ ty_dom (\@[(TVarB X Q)]@\)` have "Y \ ty_dom (\@[(TVarB X P)]@\)" + by (simp add: doms_append) ultimately show "(\@[(TVarB X P)]@\) \ Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar) next - case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \ X \) + case (SA_arrow S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \ X \) then show "(\@[(TVarB X P)]@\) \ Q\<^isub>1 \ Q\<^isub>2 <: S\<^isub>1 \ S\<^isub>2" by blast next - case (SA_all _ T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \ X \) - from SA_all(2,4,5,6) + case (SA_all T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \ X \) have IH_inner\<^isub>1: "(\@[(TVarB X P)]@\) \ T\<^isub>1 <: S\<^isub>1" - and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\)@[(TVarB X P)]@\) \ S\<^isub>2 <: T\<^isub>2" by force+ + and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\)@[(TVarB X P)]@\) \ S\<^isub>2 <: T\<^isub>2" + by (fastsimp intro: SA_all)+ then show "(\@[(TVarB X P)]@\) \ (\Y<:S\<^isub>1. S\<^isub>2) <: (\Y<:T\<^isub>1. T\<^isub>2)" by auto qed } @@ -1263,7 +1262,7 @@ assumes "\ (\ @ VarB x Q # \) ok" shows "\ (\ @ \) ok" using assms -proof (induct \' \ "\ @ VarB x Q # \" arbitrary: \ \) +proof (induct "\ @ VarB x Q # \" arbitrary: \ \) case valid_nil have "[] = \ @ VarB x Q # \" by fact then have "False" by auto @@ -1314,14 +1313,14 @@ and "\ (\ @ B # \) ok" shows "(\ @ B # \) \ t : T" using assms -proof(nominal_induct \'\ "\ @ \" t T avoiding: \ \ B rule: typing.strong_induct) - case (T_Var x' T \' \'' \') +proof(nominal_induct "\ @ \" t T avoiding: \ \ B rule: typing.strong_induct) + case (T_Var x T) then show ?case by auto next - case (T_App \ t\<^isub>1 T\<^isub>1 T\<^isub>2 t\<^isub>2 \ \) + case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2) then show ?case by force next - case (T_Abs y T\<^isub>1 \' t\<^isub>2 T\<^isub>2 \ \) + case (T_Abs y T\<^isub>1 t\<^isub>2 T\<^isub>2 \ \) then have "VarB y T\<^isub>1 # \ @ \ \ t\<^isub>2 : T\<^isub>2" by simp then have closed: "T\<^isub>1 closed_in (\ @ \)" by (auto dest: typing_ok) @@ -1336,22 +1335,22 @@ apply (rule closed) done then have "\ ((VarB y T\<^isub>1 # \) @ B # \) ok" by simp - then have "(VarB y T\<^isub>1 # \) @ B # \ \ t\<^isub>2 : T\<^isub>2" - by (rule T_Abs) (simp add: T_Abs) + with _ have "(VarB y T\<^isub>1 # \) @ B # \ \ t\<^isub>2 : T\<^isub>2" + by (rule T_Abs) simp then have "VarB y T\<^isub>1 # \ @ B # \ \ t\<^isub>2 : T\<^isub>2" by simp then show ?case by (rule typing.T_Abs) next - case (T_Sub \' t S T \ \) - from `\ (\ @ B # \) ok` and `\' = \ @ \` + case (T_Sub t S T \ \) + from refl and `\ (\ @ B # \) ok` have "\ @ B # \ \ t : S" by (rule T_Sub) - moreover from `\'\S<:T` and `\ (\ @ B # \) ok` + moreover from `(\ @ \)\S<:T` and `\ (\ @ B # \) ok` have "(\ @ B # \)\S<:T" by (rule weakening) (simp add: extends_def T_Sub) ultimately show ?case by (rule typing.T_Sub) next - case (T_TAbs X T\<^isub>1 \' t\<^isub>2 T\<^isub>2 \ \) - then have "TVarB X T\<^isub>1 # \ @ \ \ t\<^isub>2 : T\<^isub>2" by simp - then have closed: "T\<^isub>1 closed_in (\ @ \)" + case (T_TAbs X T\<^isub>1 t\<^isub>2 T\<^isub>2 \ \) + from `TVarB X T\<^isub>1 # \ @ \ \ t\<^isub>2 : T\<^isub>2` + have closed: "T\<^isub>1 closed_in (\ @ \)" by (auto dest: typing_ok) have "\ (TVarB X T\<^isub>1 # \ @ B # \) ok" apply (rule valid_consT) @@ -1364,15 +1363,15 @@ apply (rule closed) done then have "\ ((TVarB X T\<^isub>1 # \) @ B # \) ok" by simp - then have "(TVarB X T\<^isub>1 # \) @ B # \ \ t\<^isub>2 : T\<^isub>2" - by (rule T_TAbs) (simp add: T_TAbs) + with _ have "(TVarB X T\<^isub>1 # \) @ B # \ \ t\<^isub>2 : T\<^isub>2" + by (rule T_TAbs) simp then have "TVarB X T\<^isub>1 # \ @ B # \ \ t\<^isub>2 : T\<^isub>2" by simp then show ?case by (rule typing.T_TAbs) next - case (T_TApp X \' t\<^isub>1 T2 T11 T12 \ \) + case (T_TApp X t\<^isub>1 T2 T11 T12 \ \) have "\ @ B # \ \ t\<^isub>1 : (\X<:T11. T12)" - by (rule T_TApp)+ - moreover from `\'\T2<:T11` and `\ (\ @ B # \) ok` + by (rule T_TApp refl)+ + moreover from `(\ @ \)\T2<:T11` and `\ (\ @ B # \) ok` have "(\ @ B # \)\T2<:T11" by (rule weakening) (simp add: extends_def T_TApp) ultimately show ?case by (rule better_T_TApp) @@ -1393,24 +1392,22 @@ assumes "(\ @ VarB x Q # \) \ S <: T" shows "(\@\) \ S <: T" using assms -proof (induct \' \ "\ @ VarB x Q # \" S T arbitrary: \) - case (SA_Top G' S G) - then have "\ (G @ \) ok" by (auto dest: valid_cons') - moreover have "S closed_in (G @ \)" using SA_Top by (auto dest: closed_in_cons) +proof (induct "\ @ VarB x Q # \" S T arbitrary: \) + case (SA_Top S) + then have "\ (\ @ \) ok" by (auto dest: valid_cons') + moreover have "S closed_in (\ @ \)" using SA_Top by (auto dest: closed_in_cons) ultimately show ?case using subtype_of.SA_Top by auto next - case (SA_refl_TVar G X' G') - then have "\ (G' @ VarB x Q # \) ok" by simp - then have h1:"\ (G' @ \) ok" by (auto dest: valid_cons') - have "X' \ ty_dom (G' @ VarB x Q # \)" using SA_refl_TVar by auto - then have h2:"X' \ ty_dom (G' @ \)" using ty_dom_vrs by auto + case (SA_refl_TVar X) + from `\ (\ @ VarB x Q # \) ok` + have h1:"\ (\ @ \) ok" by (auto dest: valid_cons') + have "X \ ty_dom (\ @ VarB x Q # \)" using SA_refl_TVar by auto + then have h2:"X \ ty_dom (\ @ \)" using ty_dom_vrs by auto show ?case using h1 h2 by auto next - case (SA_all G T1 S1 X S2 T2 G') - have ih1:"TVarB X T1 # G = (TVarB X T1 # G') @ VarB x Q # \ \ ((TVarB X T1 # G') @ \)\S2<:T2" by fact - then have h1:"(TVarB X T1 # (G' @ \))\S2<:T2" using SA_all by auto - have ih2:"G = G' @ VarB x Q # \ \ (G' @ \)\T1<:S1" by fact - then have h2:"(G' @ \)\T1<:S1" using SA_all by auto + case (SA_all T1 S1 X S2 T2) + have h1:"((TVarB X T1 # \) @ \)\S2<:T2" by (fastsimp intro: SA_all) + have h2:"(\ @ \)\T1<:S1" using SA_all by auto then show ?case using h1 h2 by auto qed (auto) @@ -1418,26 +1415,26 @@ assumes H: "\ @ (TVarB X Q) # \ \ t : T" shows "\ \ P <: Q \ \ @ (TVarB X P) # \ \ t : T" using H - proof (nominal_induct \' \ "\ @ (TVarB X Q) # \" t T avoiding: P arbitrary: \ rule: typing.strong_induct) - case (T_Var x T G P D) + proof (nominal_induct "\ @ (TVarB X Q) # \" t T avoiding: P arbitrary: \ rule: typing.strong_induct) + case (T_Var x T P D) then have "VarB x T \ set (D @ TVarB X P # \)" and "\ (D @ TVarB X P # \) ok" by (auto intro: replace_type dest!: subtype_implies_closed) then show ?case by auto next - case (T_App G t1 T1 T2 t2 P D) + case (T_App t1 T1 T2 t2 P D) then show ?case by force next - case (T_Abs x T1 G t2 T2 P D) + case (T_Abs x T1 t2 T2 P D) then show ?case by (fastsimp dest: typing_ok) next - case (T_Sub G t S T D) + case (T_Sub t S T P D) then show ?case using subtype_narrow by fastsimp next - case (T_TAbs X' T1 G t2 T2 P D) + case (T_TAbs X' T1 t2 T2 P D) then show ?case by (fastsimp dest: typing_ok) next - case (T_TApp X' G t1 T2 T11 T12 P D) + case (T_TApp X' t1 T2 T11 T12 P D) then have "D @ TVarB X P # \ \ t1 : Forall X' T12 T11" by fastsimp moreover have "(D @ [TVarB X Q] @ \) \ T2<:T11" using T_TApp by auto then have "(D @ [TVarB X P] @ \) \ T2<:T11" using `\\P<:Q` @@ -1454,8 +1451,8 @@ theorem subst_type: -- {* A.8 *} assumes H: "(\ @ (VarB x U) # \) \ t : T" shows "\ \ u : U \ \ @ \ \ t[x \ u] : T" using H - proof (nominal_induct \' \ "\ @ (VarB x U) # \" t T avoiding: x u arbitrary: \ rule: typing.strong_induct) - case (T_Var y T G x u D) + proof (nominal_induct "\ @ (VarB x U) # \" t T avoiding: x u arbitrary: \ rule: typing.strong_induct) + case (T_Var y T x u D) show ?case proof (cases "x = y") assume eq:"x=y" @@ -1468,23 +1465,23 @@ by (auto simp add:binding.inject dest: valid_cons') qed next - case (T_App G t1 T1 T2 t2 x u D) + case (T_App t1 T1 T2 t2 x u D) then show ?case by force next - case (T_Abs y T1 G t2 T2 x u D) + case (T_Abs y T1 t2 T2 x u D) then show ?case by force next - case (T_Sub G t S T x u D) + case (T_Sub t S T x u D) then have "D @ \ \ t[x \ u] : S" by auto moreover have "(D @ \) \ S<:T" using T_Sub by (auto dest: strengthening) ultimately show ?case by auto next - case (T_TAbs X T1 G t2 T2 x u D) - from `TVarB X T1 # G \ t2 : T2` have "X \ T1" + case (T_TAbs X T1 t2 T2 x u D) + from `TVarB X T1 # D @ VarB x U # \ \ t2 : T2` have "X \ T1" by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh) with `X \ u` and T_TAbs show ?case by fastsimp next - case (T_TApp X G t1 T2 T11 T12 x u D) + case (T_TApp X t1 T2 T11 T12 x u D) then have "(D@\) \T2<:T11" using T_TApp by (auto dest: strengthening) then show "((D @ \) \ ((t1 \\<^sub>\ T2)[x \ u]) : (T12[X \ T2]\<^sub>\))" using T_TApp by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar) @@ -1496,8 +1493,8 @@ assumes H: "(\ @ ((TVarB X Q) # \)) \ S <: T" shows "\ \ P <: Q \ (\[X \ P]\<^sub>e @ \) \ S[X \ P]\<^sub>\ <: T[X \ P]\<^sub>\" using H -proof (nominal_induct \' \ "\ @ TVarB X Q # \" S T avoiding: X P arbitrary: \ rule: subtype_of.strong_induct) - case (SA_Top G S X P D) +proof (nominal_induct "\ @ TVarB X Q # \" S T avoiding: X P arbitrary: \ rule: subtype_of.strong_induct) + case (SA_Top S X P D) then have "\ (D @ TVarB X Q # \) ok" by simp moreover have closed: "P closed_in \" using SA_Top subtype_implies_closed by auto ultimately have "\ (D[X \ P]\<^sub>e @ \) ok" by (rule valid_subst) @@ -1505,17 +1502,18 @@ then have "S[X \ P]\<^sub>\ closed_in (D[X \ P]\<^sub>e @ \)" using closed by (rule subst_closed_in) ultimately show ?case by auto next - case (SA_trans_TVar Y S G T X P D) - have h:"G\S<:T" by fact + case (SA_trans_TVar Y S T X P D) + have h:"(D @ TVarB X Q # \)\S<:T" by fact then have ST: "(D[X \ P]\<^sub>e @ \) \ S[X \ P]\<^sub>\ <: T[X \ P]\<^sub>\" using SA_trans_TVar by auto - from `G\S<:T` have G_ok: "\ G ok" by (rule subtype_implies_ok) + from h have G_ok: "\ (D @ TVarB X Q # \) ok" by (rule subtype_implies_ok) from G_ok and SA_trans_TVar have X\_ok: "\ (TVarB X Q # \) ok" by (auto intro: validE_append) show "(D[X \ P]\<^sub>e @ \) \ Tvar Y[X \ P]\<^sub>\<:T[X \ P]\<^sub>\" proof (cases "X = Y") assume eq: "X = Y" - from eq and SA_trans_TVar have "TVarB Y Q \ set G" by simp - with G_ok have QS: "Q = S" using `TVarB Y S \ set G` by (rule uniqueness_of_ctxt) + from eq and SA_trans_TVar have "TVarB Y Q \ set (D @ TVarB X Q # \)" by simp + with G_ok have QS: "Q = S" using `TVarB Y S \ set (D @ TVarB X Q # \)` + by (rule uniqueness_of_ctxt) from X\_ok have "X \ ty_dom \" and "Q closed_in \" by auto then have XQ: "X \ Q" by (rule closed_in_fresh) note `\\P<:Q` @@ -1552,8 +1550,8 @@ qed qed next - case (SA_refl_TVar G Y X P D) - then have "\ (D @ TVarB X Q # \) ok" by simp + case (SA_refl_TVar Y X P D) + note `\ (D @ TVarB X Q # \) ok` moreover from SA_refl_TVar have closed: "P closed_in \" by (auto dest: subtype_implies_closed) ultimately have ok: "\ (D[X \ P]\<^sub>e @ \) ok" using valid_subst by auto @@ -1571,12 +1569,12 @@ with neq and ok show ?thesis by auto qed next - case (SA_arrow G T1 S1 S2 T2 X P D) + case (SA_arrow T1 S1 S2 T2 X P D) then have h1:"(D[X \ P]\<^sub>e @ \)\T1[X \ P]\<^sub>\<:S1[X \ P]\<^sub>\" using SA_arrow by auto from SA_arrow have h2:"(D[X \ P]\<^sub>e @ \)\S2[X \ P]\<^sub>\<:T2[X \ P]\<^sub>\" using SA_arrow by auto show ?case using subtype_of.SA_arrow h1 h2 by auto next - case (SA_all G T1 S1 Y S2 T2 X P D) + case (SA_all T1 S1 Y S2 T2 X P D) then have Y: "Y \ ty_dom (D @ TVarB X Q # \)" by (auto dest: subtype_implies_ok intro: fresh_dom) moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \)" @@ -1594,13 +1592,13 @@ assumes H: "(D @ TVarB X Q # G) \ t : T" shows "G \ P <: Q \ (D[X \ P]\<^sub>e @ G) \ t[X \\<^sub>\ P] : T[X \ P]\<^sub>\" using H -proof (nominal_induct \'\"(D @ TVarB X Q # G)" t T avoiding: X P arbitrary: D rule: typing.strong_induct) - case (T_Var x T G' X P D') +proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct) + case (T_Var x T X P D') have "G\P<:Q" by fact then have "P closed_in G" using subtype_implies_closed by auto - moreover have "\ (D' @ TVarB X Q # G) ok" using T_Var by auto + moreover note `\ (D' @ TVarB X Q # G) ok` ultimately have "\ (D'[X \ P]\<^sub>e @ G) ok" using valid_subst by auto - moreover have "VarB x T \ set (D' @ TVarB X Q # G)" using T_Var by auto + moreover note `VarB x T \ set (D' @ TVarB X Q # G)` then have "VarB x T \ set D' \ VarB x T \ set G" by simp then have "(VarB x (T[X \ P]\<^sub>\)) \ set (D'[X \ P]\<^sub>e @ G)" proof @@ -1621,25 +1619,25 @@ qed ultimately show ?case by auto next - case (T_App G' t1 T1 T2 t2 X P D') + case (T_App t1 T1 T2 t2 X P D') then have "D'[X \ P]\<^sub>e @ G \ t1[X \\<^sub>\ P] : (T1 \ T2)[X \ P]\<^sub>\" by auto moreover from T_App have "D'[X \ P]\<^sub>e @ G \ t2[X \\<^sub>\ P] : T1[X \ P]\<^sub>\" by auto ultimately show ?case by auto next - case (T_Abs x T1 G' t2 T2 X P D') + case (T_Abs x T1 t2 T2 X P D') then show ?case by force next - case (T_Sub G' t S T X P D') + case (T_Sub t S T X P D') then show ?case using substT_subtype by force next - case (T_TAbs X' G' T1 t2 T2 X P D') + case (T_TAbs X' T1 t2 T2 X P D') then have "X' \ ty_dom (D' @ TVarB X Q # G)" - and "G' closed_in (D' @ TVarB X Q # G)" + and "T1 closed_in (D' @ TVarB X Q # G)" by (auto dest: typing_ok) - then have "X' \ G'" by (rule closed_in_fresh) + then have "X' \ T1" by (rule closed_in_fresh) with T_TAbs show ?case by force next - case (T_TApp X' G' t1 T2 T11 T12 X P D') + case (T_TApp X' t1 T2 T11 T12 X P D') then have "X' \ ty_dom (D' @ TVarB X Q # G)" by (simp add: fresh_dom) moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)" @@ -1824,22 +1822,22 @@ lemma Fun_canonical: -- {* A.14(1) *} assumes ty: "[] \ v : T\<^isub>1 \ T\<^isub>2" shows "val v \ \x t S. v = (\x:S. t)" using ty -proof (induct \\"[]::env" v T\"T\<^isub>1 \ T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2) - case (T_Sub \ t S T) - hence "\ \ S <: T\<^isub>1 \ T\<^isub>2" by simp - then obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \ S\<^isub>2" +proof (induct "[]::env" v "T\<^isub>1 \ T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2) + case (T_Sub t S) + from `[] \ S <: T\<^isub>1 \ T\<^isub>2` + obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \ S\<^isub>2" by cases (auto simp add: T_Sub) - with `val t` and `\ = []` show ?case by (rule T_Sub) + then show ?case using `val t` by (rule T_Sub) qed (auto) lemma TyAll_canonical: -- {* A.14(3) *} fixes X::tyvrs assumes ty: "[] \ v : (\X<:T\<^isub>1. T\<^isub>2)" shows "val v \ \X t S. v = (\X<:S. t)" using ty -proof (induct \\"[]::env" v T\"\X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2) - case (T_Sub \ t S T) - hence "\ \ S <: (\X<:T\<^isub>1. T\<^isub>2)" by simp - then obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\X<:S\<^isub>1. S\<^isub>2)" +proof (induct "[]::env" v "\X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2) + case (T_Sub t S) + from `[] \ S <: (\X<:T\<^isub>1. T\<^isub>2)` + obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\X<:S\<^isub>1. S\<^isub>2)" by cases (auto simp add: T_Sub) then show ?case using T_Sub by auto qed (auto) @@ -1848,8 +1846,8 @@ assumes "[] \ t : T" shows "val t \ (\t'. t \ t')" using assms -proof (induct \ \ "[]::env" t T) - case (T_App \ t\<^isub>1 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2 t\<^isub>2) +proof (induct "[]::env" t T) + case (T_App t\<^isub>1 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2 t\<^isub>2) hence "val t\<^isub>1 \ (\t'. t\<^isub>1 \ t')" by simp thus ?case proof @@ -1875,7 +1873,7 @@ thus ?case by auto qed next - case (T_TApp X \ t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2) + case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2) hence "val t\<^isub>1 \ (\t'. t\<^isub>1 \ t')" by simp thus ?case proof diff -r 156925dd67af -r d62eddd9e253 src/HOL/Nominal/Examples/Pattern.thy --- a/src/HOL/Nominal/Examples/Pattern.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Nominal/Examples/Pattern.thy Thu Jan 21 09:27:57 2010 +0100 @@ -410,37 +410,34 @@ and b: "\ \ u : U" shows "\ @ \ \ t[x\u] : T" using a b proof (nominal_induct \'\"\ @ [(x, U)] @ \" t T avoiding: x u \ rule: typing.strong_induct) - case (Var \' y T x u \) - then have a1: "valid (\ @ [(x, U)] @ \)" - and a2: "(y, T) \ set (\ @ [(x, U)] @ \)" - and a3: "\ \ u : U" by simp_all - from a1 have a4: "valid (\ @ \)" by (rule valid_insert) + case (Var y T x u \) + from `valid (\ @ [(x, U)] @ \)` + have valid: "valid (\ @ \)" by (rule valid_insert) show "\ @ \ \ Var y[x\u] : T" proof cases assume eq: "x = y" - from a1 a2 have "T = U" using eq by (auto intro: context_unique) - with a3 show "\ @ \ \ Var y[x\u] : T" using eq a4 by (auto intro: weakening) + from Var eq have "T = U" by (auto intro: context_unique) + with Var eq valid show "\ @ \ \ Var y[x\u] : T" by (auto intro: weakening) next assume ineq: "x \ y" - from a2 have "(y, T) \ set (\ @ \)" using ineq by simp - then show "\ @ \ \ Var y[x\u] : T" using ineq a4 by auto + from Var ineq have "(y, T) \ set (\ @ \)" by simp + then show "\ @ \ \ Var y[x\u] : T" using ineq valid by auto qed next - case (Tuple \' t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2) - from `\ \ u : U` `\' = \ @ [(x, U)] @ \` + case (Tuple t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2) + from refl `\ \ u : U` have "\ @ \ \ t\<^isub>1[x\u] : T\<^isub>1" by (rule Tuple) - moreover from `\ \ u : U` `\' = \ @ [(x, U)] @ \` + moreover from refl `\ \ u : U` have "\ @ \ \ t\<^isub>2[x\u] : T\<^isub>2" by (rule Tuple) ultimately have "\ @ \ \ \t\<^isub>1[x\u], t\<^isub>2[x\u]\ : T\<^isub>1 \ T\<^isub>2" .. then show ?case by simp next - case (Let p t \' T \' s S) - from `\ \ u : U` `\' = \ @ [(x, U)] @ \` + case (Let p t T \' s S) + from refl `\ \ u : U` have "\ @ \ \ t[x\u] : T" by (rule Let) moreover note `\ p : T \ \'` - moreover from `\' = \ @ [(x, U)] @ \` - have "\' @ \' = (\' @ \) @ [(x, U)] @ \" by simp - with `\ \ u : U` have "(\' @ \) @ \ \ s[x\u] : S" by (rule Let) + moreover have "\' @ (\ @ [(x, U)] @ \) = (\' @ \) @ [(x, U)] @ \" by simp + then have "(\' @ \) @ \ \ s[x\u] : S" using `\ \ u : U` by (rule Let) then have "\' @ \ @ \ \ s[x\u] : S" by simp ultimately have "\ @ \ \ (LET p = t[x\u] IN s[x\u]) : S" by (rule better_T_Let) @@ -448,10 +445,10 @@ by (simp add: fresh_star_def fresh_list_nil fresh_list_cons) ultimately show ?case by simp next - case (Abs y T \' t S) - from `\' = \ @ [(x, U)] @ \` have "(y, T) # \' = ((y, T) # \) @ [(x, U)] @ \" + case (Abs y T t S) + have "(y, T) # \ @ [(x, U)] @ \ = ((y, T) # \) @ [(x, U)] @ \" by simp - with `\ \ u : U` have "((y, T) # \) @ \ \ t[x\u] : S" by (rule Abs) + then have "((y, T) # \) @ \ \ t[x\u] : S" using `\ \ u : U` by (rule Abs) then have "(y, T) # \ @ \ \ t[x\u] : S" by simp then have "\ @ \ \ (\y:T. t[x\u]) : T \ S" by (rule typing.Abs) @@ -459,10 +456,10 @@ by (simp add: fresh_list_nil fresh_list_cons) ultimately show ?case by simp next - case (App \' t\<^isub>1 T S t\<^isub>2) - from `\ \ u : U` `\' = \ @ [(x, U)] @ \` + case (App t\<^isub>1 T S t\<^isub>2) + from refl `\ \ u : U` have "\ @ \ \ t\<^isub>1[x\u] : T \ S" by (rule App) - moreover from `\ \ u : U` `\' = \ @ [(x, U)] @ \` + moreover from refl `\ \ u : U` have "\ @ \ \ t\<^isub>2[x\u] : T" by (rule App) ultimately have "\ @ \ \ (t\<^isub>1[x\u]) \ (t\<^isub>2[x\u]) : S" by (rule typing.App) diff -r 156925dd67af -r d62eddd9e253 src/HOL/Nominal/Examples/SOS.thy --- a/src/HOL/Nominal/Examples/SOS.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Nominal/Examples/SOS.thy Thu Jan 21 09:27:57 2010 +0100 @@ -220,10 +220,10 @@ shows "(\@\) \ e[x::=e'] : T" using a b proof (nominal_induct \\"\@[(x,T')]@\" e T avoiding: e' \ rule: typing.strong_induct) - case (t_Var \' y T e' \) + case (t_Var y T e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" - and a3: "\ \ e' : T'" by simp_all + and a3: "\ \ e' : T'" . from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique) diff -r 156925dd67af -r d62eddd9e253 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Nominal/nominal_induct.ML Thu Jan 21 09:27:57 2010 +0100 @@ -5,7 +5,7 @@ structure NominalInduct: sig - val nominal_induct_tac: Proof.context -> (binding option * term) option list list -> + val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> Rule_Cases.cases_tactic val nominal_induct_method: (Proof.context -> Proof.method) context_parser @@ -74,26 +74,29 @@ else map (tune o #1) (take (p - n) ps) @ xs; in Logic.list_rename_params (ys, prem) end; fun rename_prems prop = - let val (As, C) = Logic.strip_horn (Thm.prop_of rule) + let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename As, C) end; in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; (* nominal_induct_tac *) -fun nominal_induct_tac ctxt def_insts avoiding fixings rules facts = +fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = let val thy = ProofContext.theory_of ctxt; val cert = Thm.cterm_of thy; val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; - val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; + val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; val finish_rule = split_all_tuples #> rename_params_rule true (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding); - fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r); + + fun rule_cases ctxt r = + let val r' = if simp then Induct.simplified_rule ctxt r else r + in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; in (fn i => fn st => rules @@ -102,19 +105,32 @@ |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => (CONJUNCTS (ALLGOALS - (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1)) - THEN' Induct.fix_tac defs_ctxt - (nth concls (j - 1) + more_consumes) - (nth_list fixings (j - 1)))) + let + val adefs = nth_list atomized_defs (j - 1); + val frees = fold (Term.add_frees o prop_of) adefs []; + val xs = nth_list fixings (j - 1); + val k = nth concls (j - 1) + more_consumes + in + Method.insert_tac (more_facts @ adefs) THEN' + (if simp then + Induct.rotate_tac k (length adefs) THEN' + Induct.fix_tac defs_ctxt k + (List.partition (member op = frees) xs |> op @) + else + Induct.fix_tac defs_ctxt k xs) + end) THEN' Induct.inner_atomize_tac) j)) THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' => Induct.guess_instance ctxt (finish_rule (Induct.internalize more_consumes rule)) i st' |> Seq.maps (fn rule' => - CASES (rule_cases rule' cases) + CASES (rule_cases ctxt rule' cases) (Tactic.rtac (rename_params_rule false [] rule') i THEN PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) - THEN_ALL_NEW_CASES Induct.rulify_tac + THEN_ALL_NEW_CASES + ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) + else K all_tac) + THEN_ALL_NEW Induct.rulify_tac) end; @@ -128,11 +144,14 @@ val fixingN = "arbitrary"; (* to be consistent with induct; hopefully this changes again *) val ruleN = "rule"; -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; +val inst = Scan.lift (Args.$$$ "_") >> K NONE || + Args.term >> (SOME o rpair false) || + Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --| + Scan.lift (Args.$$$ ")"); val def_inst = ((Scan.lift (Args.binding --| (Args.$$$ "\" || Args.$$$ "==")) >> SOME) - -- Args.term) >> SOME || + -- (Args.term >> rpair false)) >> SOME || inst >> Option.map (pair NONE); val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => @@ -153,11 +172,11 @@ in val nominal_induct_method = - P.and_list' (Scan.repeat (unless_more_args def_inst)) -- - avoiding -- fixing -- rule_spec >> - (fn (((x, y), z), w) => fn ctxt => + Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) -- + avoiding -- fixing -- rule_spec) >> + (fn (no_simp, (((x, y), z), w)) => fn ctxt => RAW_METHOD_CASES (fn facts => - HEADGOAL (nominal_induct_tac ctxt x y z w facts))); + HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); end; diff -r 156925dd67af -r d62eddd9e253 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Jan 21 09:27:57 2010 +0100 @@ -196,7 +196,7 @@ | add_set (t, T) ((u, U) :: ps) = if T = U then let val S = HOLogic.mk_setT T - in (Const (@{const_name union}, S --> S --> S) $ u $ t, T) :: ps + in (Const (@{const_name sup}, S --> S --> S) $ u $ t, T) :: ps end else (u, U) :: add_set (t, T) ps in diff -r 156925dd67af -r d62eddd9e253 src/HOL/Old_Number_Theory/Legacy_GCD.thy --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Jan 21 09:27:57 2010 +0100 @@ -233,37 +233,39 @@ with gcd_unique[of "gcd u v" x y] show ?thesis by auto qed -lemma ind_euclid: - 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)" +lemma ind_euclid: + 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} + 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 156925dd67af -r d62eddd9e253 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Jan 21 09:27:57 2010 +0100 @@ -341,7 +341,8 @@ ((Binding.empty, flat inject), [iff_add]), ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]), - ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])] + ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]), + ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])] @ named_rules @ unnamed_rules) |> snd |> add_case_tr' case_names diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Jan 21 09:27:57 2010 +0100 @@ -496,14 +496,14 @@ (* problem -> problem -> bool *) fun problems_equivalent (p1 : problem) (p2 : problem) = - #univ_card p1 = #univ_card p2 - andalso #formula p1 = #formula p2 - andalso #bounds p1 = #bounds p2 - andalso #expr_assigns p1 = #expr_assigns p2 - andalso #tuple_assigns p1 = #tuple_assigns p2 - andalso #int_bounds p1 = #int_bounds p2 - andalso filter (is_relevant_setting o fst) (#settings p1) - = filter (is_relevant_setting o fst) (#settings p2) + #univ_card p1 = #univ_card p2 andalso + #formula p1 = #formula p2 andalso + #bounds p1 = #bounds p2 andalso + #expr_assigns p1 = #expr_assigns p2 andalso + #tuple_assigns p1 = #tuple_assigns p2 andalso + #int_bounds p1 = #int_bounds p2 andalso + filter (is_relevant_setting o fst) (#settings p1) + = filter (is_relevant_setting o fst) (#settings p2) (* int -> string *) fun base_name j = @@ -883,8 +883,8 @@ (* string -> bool *) fun is_ident_char s = - Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s - orelse s = "_" orelse s = "'" orelse s = "$" + Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse + s = "_" orelse s = "'" orelse s = "$" (* string list -> string list *) fun strip_blanks [] = [] @@ -950,9 +950,9 @@ -> substring * (int * raw_bound list) list * int list *) fun read_next_outcomes j (s, ps, js) = let val (s1, s2) = Substring.position outcome_marker s in - if Substring.isEmpty s2 - orelse not (Substring.isEmpty (Substring.position problem_marker s1 - |> snd)) then + if Substring.isEmpty s2 orelse + not (Substring.isEmpty (Substring.position problem_marker s1 + |> snd)) then (s, ps, js) else let diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Jan 21 09:27:57 2010 +0100 @@ -188,17 +188,11 @@ orig_t = let val timer = Timer.startRealTimer () - val user_thy = Proof.theory_of state + val thy = Proof.theory_of state + val ctxt = Proof.context_of state val nitpick_thy = ThyInfo.get_theory "Nitpick" - val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy)) - val thy = if nitpick_thy_missing then - Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY" - [nitpick_thy, user_thy] - |> Theory.checkpoint - else - user_thy - val ctxt = Proof.context_of state - |> nitpick_thy_missing ? Context.raw_transfer thy + val _ = Theory.subthy (nitpick_thy, thy) orelse + error "You must import the theory \"Nitpick\" to use Nitpick" val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, @@ -280,8 +274,8 @@ unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} val frees = Term.add_frees assms_t [] - val _ = null (Term.add_tvars assms_t []) - orelse raise NOT_SUPPORTED "schematic type variables" + val _ = null (Term.add_tvars assms_t []) orelse + raise NOT_SUPPORTED "schematic type variables" val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), core_t) = preprocess_term ext_ctxt assms_t val got_all_user_axioms = @@ -325,77 +319,65 @@ val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns (* typ -> bool *) - fun is_free_type_monotonic T = - unique_scope orelse - case triple_lookup (type_match thy) monos T of - SOME (SOME b) => b - | _ => is_bit_type T - orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t - fun is_datatype_monotonic T = + fun is_type_always_monotonic T = + (is_datatype thy T andalso not (is_quot_type thy T) andalso + (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse + is_number_type thy T orelse is_bit_type T + fun is_type_monotonic T = unique_scope orelse case triple_lookup (type_match thy) monos T of SOME (SOME b) => b - | _ => not (is_pure_typedef thy T) orelse is_univ_typedef thy T - orelse is_number_type thy T - orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t - fun is_datatype_deep T = - is_word_type T - orelse exists (curry (op =) T o domain_type o type_of) sel_names + | _ => is_type_always_monotonic T orelse + formulas_monotonic ext_ctxt T def_ts nondef_ts core_t + fun is_deep_datatype T = + is_datatype thy T andalso + (is_word_type T orelse + exists (curry (op =) T o domain_type o type_of) sel_names) val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts) |> sort TermOrd.typ_ord - val _ = if verbose andalso binary_ints = SOME true - andalso exists (member (op =) [nat_T, int_T]) Ts then + val _ = if verbose andalso binary_ints = SOME true andalso + exists (member (op =) [nat_T, int_T]) Ts then print_v (K "The option \"binary_ints\" will be ignored because \ \of the presence of rationals, reals, \"Suc\", \ \\"gcd\", or \"lcm\" in the problem.") else () - val (all_dataTs, all_free_Ts) = - List.partition (is_integer_type orf is_datatype thy) Ts - val (mono_dataTs, nonmono_dataTs) = - List.partition is_datatype_monotonic all_dataTs - val (mono_free_Ts, nonmono_free_Ts) = - List.partition is_free_type_monotonic all_free_Ts - - val interesting_mono_free_Ts = filter_out is_bit_type mono_free_Ts + val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic Ts val _ = - if not unique_scope andalso not (null interesting_mono_free_Ts) then - print_v (fn () => - let - val ss = map (quote o string_for_type ctxt) - interesting_mono_free_Ts - in - "The type" ^ plural_s_for_list ss ^ " " ^ - space_implode " " (serial_commas "and" ss) ^ " " ^ - (if none_true monos then - "passed the monotonicity test" - else - (if length ss = 1 then "is" else "are") ^ - " considered monotonic") ^ - ". Nitpick might be able to skip some scopes." - end) + if verbose andalso not unique_scope then + case filter_out is_type_always_monotonic mono_Ts of + [] => () + | interesting_mono_Ts => + print_v (fn () => + let + val ss = map (quote o string_for_type ctxt) + interesting_mono_Ts + in + "The type" ^ plural_s_for_list ss ^ " " ^ + space_implode " " (serial_commas "and" ss) ^ " " ^ + (if none_true monos then + "passed the monotonicity test" + else + (if length ss = 1 then "is" else "are") ^ + " considered monotonic") ^ + ". Nitpick might be able to skip some scopes." + end) else () - val mono_Ts = mono_dataTs @ mono_free_Ts - val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts - val shallow_dataTs = filter_out is_datatype_deep mono_dataTs + val shallow_dataTs = filter_out is_deep_datatype Ts (* - val _ = priority "Monotonic datatypes:" - val _ = List.app (priority o string_for_type ctxt) mono_dataTs - val _ = priority "Nonmonotonic datatypes:" - val _ = List.app (priority o string_for_type ctxt) nonmono_dataTs - val _ = priority "Monotonic free types:" - val _ = List.app (priority o string_for_type ctxt) mono_free_Ts - val _ = priority "Nonmonotonic free types:" - val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts + val _ = priority "Monotonic types:" + val _ = List.app (priority o string_for_type ctxt) mono_Ts + val _ = priority "Nonmonotonic types:" + val _ = List.app (priority o string_for_type ctxt) nonmono_Ts *) val need_incremental = Int.max (max_potential, max_genuine) >= 2 val effective_sat_solver = if sat_solver <> "smart" then - if need_incremental - andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true) - sat_solver) then + if need_incremental andalso + not (member (op =) (Kodkod_SAT.configured_sat_solvers true) + sat_solver) then (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ \be used instead of " ^ quote sat_solver ^ ".")); "SAT4J") @@ -421,9 +403,9 @@ (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) = let val _ = not (exists (fn other => scope_less_eq other scope) - (!too_big_scopes)) - orelse raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\ - \problem_for_scope", "too large scope") + (!too_big_scopes)) orelse + raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\ + \problem_for_scope", "too large scope") (* val _ = priority "Offsets:" val _ = List.app (fn (T, j0) => @@ -437,9 +419,9 @@ val main_j0 = offset_of_type ofs bool_T val (nat_card, nat_j0) = spec_of_type scope nat_T val (int_card, int_j0) = spec_of_type scope int_T - val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) - orelse raise BAD ("Nitpick.pick_them_nits_in_term.\ - \problem_for_scope", "bad offsets") + val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse + raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope", + "bad offsets") val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 val (free_names, rep_table) = choose_reps_for_free_vars scope free_names NameTable.empty @@ -527,8 +509,8 @@ defs = nondef_fs @ def_fs @ declarative_axioms}) end handle TOO_LARGE (loc, msg) => - if loc = "Nitpick_KK.check_arity" - andalso not (Typtab.is_empty ofs) then + if loc = "Nitpick_Kodkod.check_arity" andalso + not (Typtab.is_empty ofs) then problem_for_scope liberal {ext_ctxt = ext_ctxt, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jan 21 09:27:57 2010 +0100 @@ -82,6 +82,7 @@ val dest_n_tuple : int -> term -> term list val instantiate_type : theory -> typ -> typ -> typ -> typ val is_real_datatype : theory -> string -> bool + val is_quot_type : theory -> typ -> bool val is_codatatype : theory -> typ -> bool val is_pure_typedef : theory -> typ -> bool val is_univ_typedef : theory -> typ -> bool @@ -91,6 +92,8 @@ val is_record_update : theory -> styp -> bool val is_abs_fun : theory -> styp -> bool val is_rep_fun : theory -> styp -> bool + val is_quot_abs_fun : Proof.context -> styp -> bool + val is_quot_rep_fun : Proof.context -> styp -> bool val is_constr : theory -> styp -> bool val is_stale_constr : theory -> styp -> bool val is_sel : string -> bool @@ -325,6 +328,8 @@ (@{const_name uminus_int_inst.uminus_int}, 0), (@{const_name ord_int_inst.less_int}, 2), (@{const_name ord_int_inst.less_eq_int}, 2), + (@{const_name unknown}, 0), + (@{const_name is_unknown}, 1), (@{const_name Tha}, 1), (@{const_name Frac}, 0), (@{const_name norm_frac}, 0)] @@ -506,8 +511,8 @@ val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs val (co_s, co_Ts) = dest_Type co_T val _ = - if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) - andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then + if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso + co_s <> "fun" andalso not (is_basic_datatype co_s) then () else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) @@ -543,14 +548,16 @@ val is_typedef = is_some oo typedef_info val is_real_datatype = is_some oo Datatype.get_info (* theory -> typ -> bool *) +fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* ### *) + | is_quot_type _ _ = false fun is_codatatype thy (T as Type (s, _)) = not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s |> Option.map snd |> these)) | is_codatatype _ _ = false fun is_pure_typedef thy (T as Type (s, _)) = is_typedef thy s andalso - not (is_real_datatype thy s orelse is_codatatype thy T - orelse is_record_type T orelse is_integer_type T) + not (is_real_datatype thy s orelse is_quot_type thy T orelse + is_codatatype thy T orelse is_record_type T orelse is_integer_type T) | is_pure_typedef _ _ = false fun is_univ_typedef thy (Type (s, _)) = (case typedef_info thy s of @@ -564,8 +571,9 @@ | NONE => false) | is_univ_typedef _ _ = false fun is_datatype thy (T as Type (s, _)) = - (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind}) - andalso not (is_basic_datatype s) + (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse + is_quot_type thy T) andalso + not (is_basic_datatype s) | is_datatype _ _ = false (* theory -> typ -> (string * typ) list * (string * typ) *) @@ -606,6 +614,11 @@ SOME {Rep_name, ...} => s = Rep_name | NONE => false) | is_rep_fun _ _ = false +(* Proof.context -> styp -> bool *) +fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* ### *) + | is_quot_abs_fun _ _ = false +fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* ### *) + | is_quot_rep_fun _ _ = false (* theory -> styp -> styp *) fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) = @@ -613,6 +626,15 @@ SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1])) | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])) | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) +(* theory -> typ -> typ *) +fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"} + | rep_type_for_quot_type _ T = + raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], []) +(* theory -> typ -> term *) +fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) = + Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"}) + | equiv_relation_for_quot_type _ T = + raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) (* theory -> styp -> bool *) fun is_coconstr thy (s, T) = @@ -628,19 +650,20 @@ fun is_constr_like thy (s, T) = s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse let val (x as (s, T)) = (s, unbit_and_unbox_type T) in - Refute.is_IDT_constructor thy x orelse is_record_constr x - orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) - orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} - orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T) - orelse is_coconstr thy x + Refute.is_IDT_constructor thy x orelse is_record_constr x orelse + (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse + s = @{const_name Quot} orelse + s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} orelse + x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse + is_coconstr thy x end fun is_stale_constr thy (x as (_, T)) = - is_codatatype thy (body_type T) andalso is_constr_like thy x - andalso not (is_coconstr thy x) + is_codatatype thy (body_type T) andalso is_constr_like thy x andalso + not (is_coconstr thy x) fun is_constr thy (x as (_, T)) = - is_constr_like thy x - andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) - andalso not (is_stale_constr thy x) + is_constr_like thy x andalso + not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso + not (is_stale_constr thy x) (* string -> bool *) val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix val is_sel_like_and_no_discr = @@ -662,13 +685,13 @@ fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = case T of Type ("fun", _) => - (boxy = InPair orelse boxy = InFunLHS) - andalso not (is_boolean_type (body_type T)) + (boxy = InPair orelse boxy = InFunLHS) andalso + not (is_boolean_type (body_type T)) | Type ("*", Ts) => - boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 - orelse ((boxy = InExpr orelse boxy = InFunLHS) - andalso exists (is_boxing_worth_it ext_ctxt InPair) - (map (box_type ext_ctxt InPair) Ts)) + boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse + ((boxy = InExpr orelse boxy = InFunLHS) andalso + exists (is_boxing_worth_it ext_ctxt InPair) + (map (box_type ext_ctxt InPair) Ts)) | _ => false (* extended_context -> boxability -> string * typ list -> string *) and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) = @@ -679,8 +702,8 @@ and box_type ext_ctxt boxy T = case T of Type (z as ("fun", [T1, T2])) => - if boxy <> InConstr andalso boxy <> InSel - andalso should_box_type ext_ctxt boxy z then + if boxy <> InConstr andalso boxy <> InSel andalso + should_box_type ext_ctxt boxy z then Type (@{type_name fun_box}, [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2]) else @@ -778,6 +801,8 @@ val T' = (Record.get_extT_fields thy T |> apsnd single |> uncurry append |> map snd) ---> T in [(s', T')] end + else if is_quot_type thy T then + [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)] else case typedef_info thy s of SOME {abs_type, rep_type, Abs_name, ...} => [(Abs_name, instantiate_type thy abs_type T rep_type --> T)] @@ -871,10 +896,10 @@ let val args = map Envir.eta_contract args in case hd args of Const (x' as (s', _)) $ t => - if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s - andalso forall (fn (n, t') => - select_nth_constr_arg thy x t n dummyT = t') - (index_seq 0 (length args) ~~ args) then + if is_sel_like_and_no_discr s' andalso + constr_name_for_sel_like s' = s andalso + forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t') + (index_seq 0 (length args) ~~ args) then t else list_comb (Const x, args) @@ -1011,8 +1036,8 @@ (* theory -> string -> bool *) fun is_funky_typedef_name thy s = member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, - @{type_name int}] s - orelse is_frac_type thy (Type (s, [])) + @{type_name int}] s orelse + is_frac_type thy (Type (s, [])) (* theory -> term -> bool *) fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s | is_funky_typedef _ _ = false @@ -1055,8 +1080,8 @@ (* term -> bool *) fun do_lhs t1 = case strip_comb t1 of - (Const _, args) => forall is_Var args - andalso not (has_duplicates (op =) args) + (Const _, args) => + forall is_Var args andalso not (has_duplicates (op =) args) | _ => false fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) = @@ -1174,8 +1199,8 @@ (* term -> bool *) fun is_good_arg (Bound _) = true | is_good_arg (Const (s, _)) = - s = @{const_name True} orelse s = @{const_name False} - orelse s = @{const_name undefined} + s = @{const_name True} orelse s = @{const_name False} orelse + s = @{const_name undefined} | is_good_arg _ = false in case t |> strip_abs_body |> strip_comb of @@ -1289,9 +1314,17 @@ fun nondef_props_for_const thy slack table (x as (s, _)) = these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) +(* theory -> styp -> term list *) +fun inverse_axioms_for_rep_fun thy (x as (_, T)) = + let val abs_T = domain_type T in + typedef_info thy (fst (dest_Type abs_T)) |> the + |> pairf #Abs_inverse #Rep_inverse + |> pairself (Refute.specialize_type thy x o prop_of o the) + ||> single |> op :: + end (* theory -> styp list -> term list *) -fun optimized_typedef_axioms thy (abs_s, abs_Ts) = - let val abs_T = Type (abs_s, abs_Ts) in +fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) = + let val abs_T = Type abs_z in if is_univ_typedef thy abs_T then [] else case typedef_info thy abs_s of @@ -1313,13 +1346,31 @@ end | NONE => [] end -(* theory -> styp -> term list *) -fun inverse_axioms_for_rep_fun thy (x as (_, T)) = - let val abs_T = domain_type T in - typedef_info thy (fst (dest_Type abs_T)) |> the - |> pairf #Abs_inverse #Rep_inverse - |> pairself (Refute.specialize_type thy x o prop_of o the) - ||> single |> op :: +fun optimized_quot_type_axioms thy abs_z = + let + val abs_T = Type abs_z + val rep_T = rep_type_for_quot_type thy abs_T + val equiv_rel = equiv_relation_for_quot_type thy abs_T + val a_var = Var (("a", 0), abs_T) + val x_var = Var (("x", 0), rep_T) + val y_var = Var (("y", 0), rep_T) + val x = (@{const_name Quot}, rep_T --> abs_T) + val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T + val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T) + val normal_x = normal_t $ x_var + val normal_y = normal_t $ y_var + val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T) + in + [Logic.mk_equals (sel_a_t, normal_t $ sel_a_t), + Logic.list_implies + ([@{const Not} $ (HOLogic.mk_eq (x_var, y_var)), + @{const Not} $ (is_unknown_t $ normal_x), + @{const Not} $ (is_unknown_t $ normal_y), + equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop, + Logic.mk_equals (normal_x, normal_y)), + @{const "==>"} + $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x))) + $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))] end (* theory -> int * styp -> term *) @@ -1402,8 +1453,8 @@ (* extended_context -> styp -> bool *) fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...} : extended_context) x = - not (null (def_props_for_const thy fast_descrs intro_table x)) - andalso fixpoint_kind_of_const thy def_table x <> NoFp + not (null (def_props_for_const thy fast_descrs intro_table x)) andalso + fixpoint_kind_of_const thy def_table x <> NoFp fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...} : extended_context) x = exists (fn table => not (null (def_props_for_const thy fast_descrs table x))) @@ -1489,10 +1540,9 @@ (t1 |> HOLogic.dest_list |> distinctness_formula T' handle TERM _ => do_const depth Ts t x [t1]) | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 => - if is_ground_term t1 - andalso exists (Pattern.matches thy o rpair t1) - (Inttab.lookup_list ground_thm_table - (hash_term t1)) then + if is_ground_term t1 andalso + exists (Pattern.matches thy o rpair t1) + (Inttab.lookup_list ground_thm_table (hash_term t1)) then do_term depth Ts t2 else do_const depth Ts t x [t1, t2, t3] @@ -1534,8 +1584,24 @@ if is_constr thy x then (Const x, ts) else if is_stale_constr thy x then - raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \ + raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \ \(\"" ^ s ^ "\")") + else if is_quot_abs_fun thy x then + let + val rep_T = domain_type T + val abs_T = range_type T + in + (Abs (Name.uu, rep_T, + Const (@{const_name Quot}, rep_T --> abs_T) + $ (Const (@{const_name quot_normal}, + rep_T --> rep_T) $ Bound 0)), ts) + end + else if is_quot_rep_fun thy x then + let + val abs_T = domain_type T + val rep_T = range_type T + val x' = (@{const_name Quot}, rep_T --> abs_T) + in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end else if is_record_get thy x then case length ts of 0 => (do_term depth Ts (eta_expand Ts t 1), []) @@ -1691,8 +1757,8 @@ else () in - if tac_timeout = (!cached_timeout) - andalso length (!cached_wf_props) < max_cached_wfs then + if tac_timeout = (!cached_timeout) andalso + length (!cached_wf_props) < max_cached_wfs then () else (cached_wf_props := []; cached_timeout := tac_timeout); @@ -1716,8 +1782,8 @@ (x as (s, _)) = case triple_lookup (const_match thy) wfs x of SOME (SOME b) => b - | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} - orelse case AList.lookup (op =) (!wf_cache) x of + | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse + case AList.lookup (op =) (!wf_cache) x of SOME (_, wf) => wf | NONE => let @@ -1859,8 +1925,8 @@ in if is_equational_fun ext_ctxt x' then unrolled_const (* already done *) - else if not gfp andalso is_linear_inductive_pred_def def - andalso star_linear_preds then + else if not gfp andalso is_linear_inductive_pred_def def andalso + star_linear_preds then starred_linear_pred_const ext_ctxt x def else let @@ -1980,10 +2046,10 @@ let val t_comb = list_comb (t, args) in case t of Const x => - if not relax andalso is_constr thy x - andalso not (is_fun_type (fastype_of1 (Ts, t_comb))) - andalso has_heavy_bounds_or_vars Ts level t_comb - andalso not (loose_bvar (t_comb, level)) then + if not relax andalso is_constr thy x andalso + not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso + has_heavy_bounds_or_vars Ts level t_comb andalso + not (loose_bvar (t_comb, level)) then let val (j, seen) = case find_index (curry (op =) t_comb) seen of ~1 => (0, t_comb :: seen) @@ -2062,18 +2128,17 @@ and aux_eq careful pass1 t0 t1 t2 = (if careful then raise SAME () - else if axiom andalso is_Var t2 - andalso num_occs_of_var (dest_Var t2) = 1 then + else if axiom andalso is_Var t2 andalso + num_occs_of_var (dest_Var t2) = 1 then @{const True} else case strip_comb t2 of (Const (x as (s, T)), args) => let val arg_Ts = binder_types T in - if length arg_Ts = length args - andalso (is_constr thy x orelse s = @{const_name Pair} - orelse x = (@{const_name Suc}, nat_T --> nat_T)) - andalso (not careful orelse not (is_Var t1) - orelse String.isPrefix val_var_prefix - (fst (fst (dest_Var t1)))) then + if length arg_Ts = length args andalso + (is_constr thy x orelse s = @{const_name Pair} orelse + x = (@{const_name Suc}, nat_T --> nat_T)) andalso + (not careful orelse not (is_Var t1) orelse + String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then discriminate_value ext_ctxt x t1 :: map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args |> foldr1 s_conj @@ -2095,8 +2160,8 @@ let (* term -> int -> term *) fun is_nth_sel_on t' n (Const (s, _) $ t) = - (t = t' andalso is_sel_like_and_no_discr s - andalso sel_no_from_name s = n) + (t = t' andalso is_sel_like_and_no_discr s andalso + sel_no_from_name s = n) | is_nth_sel_on _ _ _ = false (* term -> term list -> term *) fun do_term (Const (@{const_name Rep_Frac}, _) @@ -2109,9 +2174,9 @@ if length args = num_binder_types T then case hd args of Const (x' as (_, T')) $ t' => - if domain_type T' = body_type T - andalso forall (uncurry (is_nth_sel_on t')) - (index_seq 0 (length args) ~~ args) then + if domain_type T' = body_type T andalso + forall (uncurry (is_nth_sel_on t')) + (index_seq 0 (length args) ~~ args) then t' else raise SAME () @@ -2121,9 +2186,9 @@ else if is_sel_like_and_no_discr s then case strip_comb (hd args) of (Const (x' as (s', T')), ts') => - if is_constr_like thy x' - andalso constr_name_for_sel_like s = s' - andalso not (exists is_pair_type (binder_types T')) then + if is_constr_like thy x' andalso + constr_name_for_sel_like s = s' andalso + not (exists is_pair_type (binder_types T')) then list_comb (nth ts' (sel_no_from_name s), tl args) else raise SAME () @@ -2164,8 +2229,8 @@ (* term list -> (indexname * typ) list -> indexname * typ -> term -> term -> term -> term *) and aux_eq prems zs z t' t1 t2 = - if not (member (op =) zs z) - andalso not (exists_subterm (curry (op =) (Var z)) t') then + if not (member (op =) zs z) andalso + not (exists_subterm (curry (op =) (Var z)) t') then aux prems zs (subst_free [(Var z, t')] t2) else aux (t1 :: prems) (Term.add_vars t1 zs) t2 @@ -2323,8 +2388,8 @@ (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) => if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then aux s0 (s1 :: ss) (T1 :: Ts) t1 - else if quant_s = "" andalso (s0 = @{const_name All} - orelse s0 = @{const_name Ex}) then + else if quant_s = "" andalso + (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then aux s0 [s1] [T1] t1 else raise SAME () @@ -2402,8 +2467,8 @@ (* polarity -> string -> bool *) fun is_positive_existential polar quant_s = - (polar = Pos andalso quant_s = @{const_name Ex}) - orelse (polar = Neg andalso quant_s <> @{const_name Ex}) + (polar = Pos andalso quant_s = @{const_name Ex}) orelse + (polar = Neg andalso quant_s <> @{const_name Ex}) (* extended_context -> int -> term -> term *) fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...}) @@ -2418,8 +2483,8 @@ fun do_quantifier quant_s quant_T abs_s abs_T t = if not (loose_bvar1 (t, 0)) then aux ss Ts js depth polar (incr_boundvars ~1 t) - else if depth <= skolem_depth - andalso is_positive_existential polar quant_s then + else if depth <= skolem_depth andalso + is_positive_existential polar quant_s then let val j = length (!skolems) + 1 val sko_s = skolem_prefix_for (length js) j ^ abs_s @@ -2469,8 +2534,8 @@ | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 => t0 $ t1 $ aux ss Ts js depth polar t2 | Const (x as (s, T)) => - if is_inductive_pred ext_ctxt x - andalso not (is_well_founded_inductive_pred ext_ctxt x) then + if is_inductive_pred ext_ctxt x andalso + not (is_well_founded_inductive_pred ext_ctxt x) then let val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) val (pref, connective, set_oper) = @@ -2582,9 +2647,9 @@ (* typ list -> term -> bool *) fun is_eligible_arg Ts t = let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in - null bad_Ts - orelse (is_higher_order_type (fastype_of1 (Ts, t)) - andalso forall (not o is_higher_order_type) bad_Ts) + null bad_Ts orelse + (is_higher_order_type (fastype_of1 (Ts, t)) andalso + forall (not o is_higher_order_type) bad_Ts) end (* (int * term option) list -> (int * term) list -> int list *) @@ -2608,9 +2673,9 @@ else case term_under_def t of Const x => [x] | _ => [] (* term list -> typ list -> term -> term *) fun aux args Ts (Const (x as (s, T))) = - ((if not (member (op =) blacklist x) andalso not (null args) - andalso not (String.isPrefix special_prefix s) - andalso is_equational_fun ext_ctxt x then + ((if not (member (op =) blacklist x) andalso not (null args) andalso + not (String.isPrefix special_prefix s) andalso + is_equational_fun ext_ctxt x then let val eligible_args = filter (is_eligible_arg Ts o snd) (index_seq 0 (length args) ~~ args) @@ -2678,8 +2743,8 @@ let val table = aux t2 [] table in aux t1 (t2 :: args) table end | aux (Abs (_, _, t')) _ table = aux t' [] table | aux (t as Const (x as (s, _))) args table = - if is_built_in_const true x orelse is_constr_like thy x orelse is_sel s - orelse s = @{const_name Sigma} then + if is_built_in_const true x orelse is_constr_like thy x orelse + is_sel s orelse s = @{const_name Sigma} then table else Termtab.map_default (t, 65536) (curry Int.min (length args)) table @@ -2699,8 +2764,8 @@ let val (arg_Ts, rest_T) = strip_n_binders n T val j = - if hd arg_Ts = @{typ bisim_iterator} - orelse is_fp_iterator_type (hd arg_Ts) then + if hd arg_Ts = @{typ bisim_iterator} orelse + is_fp_iterator_type (hd arg_Ts) then 1 else case find_index (not_equal bool_T) arg_Ts of ~1 => n @@ -2766,8 +2831,8 @@ \coerce_term", [t'])) | (Type (new_s, new_Ts as [new_T1, new_T2]), Type (old_s, old_Ts as [old_T1, old_T2])) => - if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box} - orelse old_s = "*" then + if old_s = @{type_name fun_box} orelse + old_s = @{type_name pair_box} orelse old_s = "*" then case constr_expand ext_ctxt old_T t of Const (@{const_name FunBox}, _) $ t1 => if new_s = "fun" then @@ -2881,13 +2946,17 @@ $ do_term new_Ts old_Ts polar t2 | Const (s as @{const_name The}, T) => do_description_operator s T | Const (s as @{const_name Eps}, T) => do_description_operator s T + | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) => + let val T' = box_type ext_ctxt InFunRHS1 T2 in + Const (@{const_name quot_normal}, T' --> T') + end | Const (s as @{const_name Tha}, T) => do_description_operator s T | Const (x as (s, T)) => - Const (s, if s = @{const_name converse} - orelse s = @{const_name trancl} then + Const (s, if s = @{const_name converse} orelse + s = @{const_name trancl} then box_relational_operator_type T - else if is_built_in_const fast_descrs x - orelse s = @{const_name Sigma} then + else if is_built_in_const fast_descrs x orelse + s = @{const_name Sigma} then T else if is_constr_like thy x then box_type ext_ctxt InConstr T @@ -2972,7 +3041,7 @@ |> map Logic.mk_equals, Logic.mk_equals (list_comb (Const x1, bounds1 @ args1), list_comb (Const x2, bounds2 @ args2))) - |> Refute.close_form + |> Refute.close_form (* TODO: needed? *) end (* extended_context -> styp list -> term list *) @@ -3078,23 +3147,29 @@ fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x) accum else if is_abs_fun thy x then - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> is_funky_typedef thy (range_type T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true + if is_quot_type thy (range_type T) then + raise NOT_SUPPORTED "\"Abs_\" function of quotient type" + else + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> is_funky_typedef thy (range_type T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) else if is_rep_fun thy x then - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> is_funky_typedef thy (range_type T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true + if is_quot_type thy (domain_type T) then + raise NOT_SUPPORTED "\"Rep_\" function of quotient type" + else + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> is_funky_typedef thy (range_type T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) - |> add_axioms_for_term depth - (Const (mate_of_rep_fun thy x)) - |> fold (add_def_axiom depth) - (inverse_axioms_for_rep_fun thy x) + |> add_axioms_for_term depth + (Const (mate_of_rep_fun thy x)) + |> fold (add_def_axiom depth) + (inverse_axioms_for_rep_fun thy x) else accum |> user_axioms <> SOME false ? fold (add_nondef_axiom depth) @@ -3116,10 +3191,12 @@ | @{typ unit} => I | TFree (_, S) => add_axioms_for_sort depth T S | TVar (_, S) => add_axioms_for_sort depth T S - | Type (z as (_, Ts)) => + | Type (z as (s, Ts)) => fold (add_axioms_for_type depth) Ts #> (if is_pure_typedef thy T then fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z) + else if is_quot_type thy T then + fold (add_def_axiom depth) (optimized_quot_type_axioms thy z) else if max_bisim_depth >= 0 andalso is_codatatype thy T then fold (add_maybe_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T) @@ -3364,11 +3441,11 @@ member (op =) [@{const_name times_nat_inst.times_nat}, @{const_name div_nat_inst.div_nat}, @{const_name times_int_inst.times_int}, - @{const_name div_int_inst.div_int}] s - orelse (String.isPrefix numeral_prefix s andalso - let val n = the (Int.fromString (unprefix numeral_prefix s)) in - n <= ~ binary_int_threshold orelse n >= binary_int_threshold - end) + @{const_name div_int_inst.div_int}] s orelse + (String.isPrefix numeral_prefix s andalso + let val n = the (Int.fromString (unprefix numeral_prefix s)) in + n <= ~ binary_int_threshold orelse n >= binary_int_threshold + end) | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t' | should_use_binary_ints _ = false @@ -3398,8 +3475,8 @@ SOME false => false | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso - (binary_ints = SOME true - orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts)) + (binary_ints = SOME true orelse + exists should_use_binary_ints (core_t :: def_ts @ nondef_ts)) val box = exists (not_equal (SOME false) o snd) boxes val table = Termtab.empty |> uncurry diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Jan 21 09:27:57 2010 +0100 @@ -106,12 +106,12 @@ (* string -> bool *) fun is_known_raw_param s = - AList.defined (op =) default_default_params s - orelse AList.defined (op =) negated_params s - orelse s = "max" orelse s = "eval" orelse s = "expect" - orelse exists (fn p => String.isPrefix (p ^ " ") s) - ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", - "wf", "non_wf", "format"] + AList.defined (op =) default_default_params s orelse + AList.defined (op =) negated_params s orelse + s = "max" orelse s = "eval" orelse s = "expect" orelse + exists (fn p => String.isPrefix (p ^ " ") s) + ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "wf", + "non_wf", "format"] (* string * 'a -> unit *) fun check_raw_param (s, _) = diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Jan 21 09:27:57 2010 +0100 @@ -380,8 +380,8 @@ val one = is_one_rep body_R val opt_x = case r of KK.Rel x => SOME x | _ => NONE in - if opt_x <> NONE andalso length binder_schema = 1 - andalso length body_schema = 1 then + if opt_x <> NONE andalso length binder_schema = 1 andalso + length body_schema = 1 then (if one then KK.Function else KK.Functional) (the opt_x, KK.AtomSeq (hd binder_schema), KK.AtomSeq (hd body_schema)) @@ -490,8 +490,8 @@ r else let val card = card_of_rep old_R in - if is_lone_rep old_R andalso is_lone_rep new_R - andalso card = card_of_rep new_R then + if is_lone_rep old_R andalso is_lone_rep new_R andalso + card = card_of_rep new_R then if card >= lone_rep_fallback_max_card then raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback", "too high cardinality (" ^ string_of_int card ^ ")") @@ -1005,13 +1005,13 @@ | Op1 (Finite, _, _, u1) => let val opt1 = is_opt_rep (rep_of u1) in case polar of - Neut => if opt1 then - raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) - else - KK.True + Neut => + if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) + else KK.True | Pos => formula_for_bool (not opt1) | Neg => KK.True end + | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1) | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1 | Op2 (All, _, _, u1, u2) => kk_all (untuple to_decl u1) (to_f_with_polarity polar u2) @@ -1070,8 +1070,8 @@ | args _ = [] val opt_arg_us = filter (is_opt_rep o rep_of) (args u1) in - if null opt_arg_us orelse not (is_Opt min_R) - orelse is_eval_name u1 then + if null opt_arg_us orelse not (is_Opt min_R) orelse + is_eval_name u1 then fold (kk_or o (kk_no o to_r)) opt_arg_us (kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) else @@ -1100,8 +1100,8 @@ (if polar = Pos then if not both_opt then kk_rel_eq r1 r2 - else if is_lone_rep min_R - andalso arity_of_rep min_R = 1 then + else if is_lone_rep min_R andalso + arity_of_rep min_R = 1 then kk_some (kk_intersect r1 r2) else raise SAME () @@ -1132,9 +1132,9 @@ val rs1 = unpack_products r1 val rs2 = unpack_products r2 in - if length rs1 = length rs2 - andalso map KK.arity_of_rel_expr rs1 - = map KK.arity_of_rel_expr rs2 then + if length rs1 = length rs2 andalso + map KK.arity_of_rel_expr rs1 + = map KK.arity_of_rel_expr rs2 then fold1 kk_and (map2 kk_subset rs1 rs2) else kk_subset r1 r2 @@ -1582,8 +1582,8 @@ else fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel) | Op2 (Apply, _, R, u1, u2) => - if is_Cst Unrep u2 andalso is_set_type (type_of u1) - andalso is_FreeName u1 then + if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso + is_FreeName u1 then false_atom else to_apply R u1 u2 diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Jan 21 09:27:57 2010 +0100 @@ -440,7 +440,9 @@ | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\ \for_atom (Abs_Frac)", ts) end - else if not for_auto andalso is_abs_fun thy constr_x then + else if not for_auto andalso + (is_abs_fun thy constr_x orelse + constr_s = @{const_name Quot}) then Const (abs_name, constr_T) $ the_single ts else list_comb (Const constr_x, ts) @@ -560,8 +562,8 @@ pairself (strip_comb o unfold_outer_the_binders) (t1, t2) val max_depth = max_depth - (if member (op =) coTs T then 1 else 0) in - head1 = head2 - andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2) + head1 = head2 andalso + forall (bisimilar_values coTs max_depth) (args1 ~~ args2) end else t1 = t2 @@ -704,8 +706,8 @@ in (Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"] else chunks), - bisim_depth >= 0 - orelse forall (is_codatatype_wellformed codatatypes) codatatypes) + bisim_depth >= 0 orelse + forall (is_codatatype_wellformed codatatypes) codatatypes) end (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Jan 21 09:27:57 2010 +0100 @@ -121,8 +121,8 @@ (* typ -> typ -> bool *) fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = - T = alpha_T orelse (not (is_fp_iterator_type T) - andalso exists (could_exist_alpha_subtype alpha_T) Ts) + T = alpha_T orelse (not (is_fp_iterator_type T) andalso + exists (could_exist_alpha_subtype alpha_T) Ts) | could_exist_alpha_subtype alpha_T T = (T = alpha_T) (* theory -> typ -> typ -> bool *) fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T = @@ -195,8 +195,8 @@ let val C1 = do_type T1 val C2 = do_type T2 - val a = if is_boolean_type (body_type T2) - andalso exists_alpha_sub_ctype_fresh C1 then + val a = if is_boolean_type (body_type T2) andalso + exists_alpha_sub_ctype_fresh C1 then V (Unsynchronized.inc max_fresh) else S Neg diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Jan 21 09:27:57 2010 +0100 @@ -39,6 +39,7 @@ Converse | Closure | SingletonSet | + IsUnknown | Tha | First | Second | @@ -158,6 +159,7 @@ Converse | Closure | SingletonSet | + IsUnknown | Tha | First | Second | @@ -231,6 +233,7 @@ | string_for_op1 Converse = "Converse" | string_for_op1 Closure = "Closure" | string_for_op1 SingletonSet = "SingletonSet" + | string_for_op1 IsUnknown = "IsUnknown" | string_for_op1 Tha = "Tha" | string_for_op1 First = "First" | string_for_op1 Second = "Second" @@ -567,7 +570,6 @@ sub t1, sub_abs s T' t2) | (t0 as Const (@{const_name Let}, T), [t1, t2]) => sub (t0 $ t1 $ eta_expand Ts t2 1) - | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any) | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any) | (Const (@{const_name Pair}, T), [t1, t2]) => Tuple (nth_range_type 2 T, Any, map sub [t1, t2]) @@ -641,6 +643,9 @@ Op2 (Less, bool_T, Any, sub t1, sub t2) | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) => Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) + | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any) + | (Const (@{const_name is_unknown}, T), [t1]) => + Op1 (IsUnknown, bool_T, Any, sub t1) | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) => Op1 (Tha, T2, Any, sub t1) | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any) @@ -715,12 +720,12 @@ rep_for_abs_fun else if is_rep_fun thy x then Func oo best_non_opt_symmetric_reps_for_fun_type - else if all_exact orelse is_skolem_name v - orelse member (op =) [@{const_name undefined_fast_The}, - @{const_name undefined_fast_Eps}, - @{const_name bisim}, - @{const_name bisim_iterator_max}] - (original_name s) then + else if all_exact orelse is_skolem_name v orelse + member (op =) [@{const_name undefined_fast_The}, + @{const_name undefined_fast_Eps}, + @{const_name bisim}, + @{const_name bisim_iterator_max}] + (original_name s) then best_non_opt_set_rep_for_type else if member (op =) [@{const_name set}, @{const_name distinct}, @{const_name ord_class.less}, @@ -746,9 +751,9 @@ (vs, table) = let val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n - val R' = if n = ~1 orelse is_word_type (body_type T) - orelse (is_fun_type (range_type T') - andalso is_boolean_type (body_type T')) then + val R' = if n = ~1 orelse is_word_type (body_type T) orelse + (is_fun_type (range_type T') andalso + is_boolean_type (body_type T')) then best_non_opt_set_rep_for_type scope T' else best_opt_set_rep_for_type scope T' |> unopt_rep @@ -798,10 +803,8 @@ if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u (* typ -> rep -> nut *) fun unknown_boolean T R = - Cst (case R of - Formula Pos => False - | Formula Neg => True - | _ => Unknown, T, R) + Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown, + T, R) (* op1 -> typ -> rep -> nut -> nut *) fun s_op1 oper T R u1 = @@ -954,19 +957,18 @@ let val T1 = domain_type T val R1 = Atom (spec_of_type scope T1) - val total = T1 = nat_T - andalso (cst = Subtract orelse cst = Divide - orelse cst = Gcd) + val total = T1 = nat_T andalso + (cst = Subtract orelse cst = Divide orelse cst = Gcd) in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end else if cst = NatToInt orelse cst = IntToNat then let val (dom_card, dom_j0) = spec_of_type scope (domain_type T) val (ran_card, ran_j0) = spec_of_type scope (range_type T) - val total = not (is_word_type (domain_type T)) - andalso (if cst = NatToInt then - max_int_for_card ran_card >= dom_card + 1 - else - max_int_for_card dom_card < ran_card) + val total = not (is_word_type (domain_type T)) andalso + (if cst = NatToInt then + max_int_for_card ran_card >= dom_card + 1 + else + max_int_for_card dom_card < ran_card) in Cst (cst, T, Func (Atom (dom_card, dom_j0), Atom (ran_card, ran_j0) |> not total ? Opt)) @@ -979,6 +981,11 @@ triad (s_op1 Not T (Formula Pos) u12) (s_op1 Not T (Formula Neg) u11) | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1') + | Op1 (IsUnknown, T, _, u1) => + let val u1 = sub u1 in + if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1) + else Cst (False, T, Formula Neut) + end | Op1 (oper, T, _, u1) => let val u1 = sub u1 @@ -1029,8 +1036,8 @@ if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2' else opt_opt_case () in - if liberal orelse polar = Neg - orelse is_concrete_type datatypes (type_of u1) then + if liberal orelse polar = Neg orelse + is_concrete_type datatypes (type_of u1) then case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of (true, true) => opt_opt_case () | (true, false) => hybrid_case u1' @@ -1108,12 +1115,11 @@ val u1' = aux table' false Neut u1 val u2' = aux table' false Neut u2 val R = - if is_opt_rep (rep_of u2') - orelse (range_type T = bool_T andalso - not (is_Cst False - (unrepify_nut_in_nut table false Neut - u1 u2 - |> optimize_nut))) then + if is_opt_rep (rep_of u2') orelse + (range_type T = bool_T andalso + not (is_Cst False (unrepify_nut_in_nut table false Neut + u1 u2 + |> optimize_nut))) then opt_rep ofs T R else unopt_rep R @@ -1131,9 +1137,9 @@ triad_fn (fn polar => gsub def polar u) else let val quant_u = s_op2 oper T (Formula polar) u1' u2' in - if def - orelse (liberal andalso (polar = Pos) = (oper = All)) - orelse is_complete_type datatypes (type_of u1) then + if def orelse + (liberal andalso (polar = Pos) = (oper = All)) orelse + is_complete_type datatypes (type_of u1) then quant_u else let @@ -1231,8 +1237,8 @@ in Construct (map sub us', T, R |> opt ? Opt, us) end | _ => let val u = modify_name_rep u (the_name table u) in - if polar = Neut orelse not (is_boolean_type (type_of u)) - orelse not (is_opt_rep (rep_of u)) then + if polar = Neut orelse not (is_boolean_type (type_of u)) orelse + not (is_opt_rep (rep_of u)) then u else s_op1 Cast (type_of u) (Formula polar) u diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_peephole.ML --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Jan 21 09:27:57 2010 +0100 @@ -421,8 +421,8 @@ if is_one_rel_expr r1 then s_or (s_subset r1 r21) (s_subset r1 r22) else - if s_subset r1 r21 = True orelse s_subset r1 r22 = True - orelse r1 = r2 then + if s_subset r1 r21 = True orelse s_subset r1 r22 = True orelse + r1 = r2 then True else Subset (r1, r2) diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Jan 21 09:27:57 2010 +0100 @@ -274,8 +274,8 @@ | (R1, R2) => Struct [R1, R2]) | best_one_rep_for_type (scope as {card_assigns, datatypes, ofs, ...}) T = (case card_of_type card_assigns T of - 1 => if is_some (datatype_spec datatypes T) - orelse is_fp_iterator_type T then + 1 => if is_some (datatype_spec datatypes T) orelse + is_fp_iterator_type T then Atom (1, offset_of_type ofs T) else Unit diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Jan 21 09:27:57 2010 +0100 @@ -107,8 +107,8 @@ | is_complete_type dtypes (Type ("*", Ts)) = forall (is_complete_type dtypes) Ts | is_complete_type dtypes T = - not (is_integer_type T) andalso not (is_bit_type T) - andalso #complete (the (datatype_spec dtypes T)) + not (is_integer_type T) andalso not (is_bit_type T) andalso + #complete (the (datatype_spec dtypes T)) handle Option.Option => true and is_concrete_type dtypes (Type ("fun", [T1, T2])) = is_complete_type dtypes T1 andalso is_concrete_type dtypes T2 @@ -427,8 +427,8 @@ {delta = delta, epsilon = delta, exclusive = true, total = false} end else if not co andalso num_self_recs > 0 then - if not self_rec andalso num_non_self_recs = 1 - andalso domain_card 2 card_assigns T = 1 then + if not self_rec andalso num_non_self_recs = 1 andalso + domain_card 2 card_assigns T = 1 then {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}), total = true} else if s = @{const_name Cons} then diff -r 156925dd67af -r d62eddd9e253 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Jan 21 09:27:57 2010 +0100 @@ -285,8 +285,8 @@ (* string -> string *) fun maybe_quote y = let val s = plain_string_from_yxml y in - y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) - orelse OuterKeyword.is_keyword s) ? quote + y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse + OuterKeyword.is_keyword s) ? quote end end; diff -r 156925dd67af -r d62eddd9e253 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/Transitive_Closure.thy Thu Jan 21 09:27:57 2010 +0100 @@ -106,12 +106,8 @@ theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]: assumes a: "r^** a b" and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z" - shows "P b" -proof - - from a have "a = a --> P b" - by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+ - then show ?thesis by iprover -qed + shows "P b" using a + by (induct x\a b) (rule cases)+ lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set] @@ -257,7 +253,7 @@ lemma sym_rtrancl: "sym r ==> sym (r^*)" by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) -theorem converse_rtranclp_induct[consumes 1]: +theorem converse_rtranclp_induct [consumes 1, case_names base step]: assumes major: "r^** a b" and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y" shows "P a" @@ -274,7 +270,7 @@ converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names refl step] -lemma converse_rtranclpE: +lemma converse_rtranclpE [consumes 1, case_names base step]: assumes major: "r^** x z" and cases: "x=z ==> P" "!!y. [| r x y; r^** y z |] ==> P" @@ -352,15 +348,11 @@ text {* Nice induction rule for @{text trancl} *} lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]: - assumes "r^++ a b" + assumes a: "r^++ a b" and cases: "!!y. r a y ==> P y" "!!y z. r^++ a y ==> r y z ==> P y ==> P z" - shows "P b" -proof - - from `r^++ a b` have "a = a --> P b" - by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+ - then show ?thesis by iprover -qed + shows "P b" using a + by (induct x\a b) (iprover intro: cases)+ lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set] @@ -484,7 +476,7 @@ lemma sym_trancl: "sym r ==> sym (r^+)" by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) -lemma converse_tranclp_induct: +lemma converse_tranclp_induct [consumes 1, case_names base step]: assumes major: "r^++ a b" and cases: "!!y. r y b ==> P(y)" "!!y z.[| r y z; r^++ z b; P(z) |] ==> P(y)" diff -r 156925dd67af -r d62eddd9e253 src/HOL/ex/ThreeDivides.thy --- a/src/HOL/ex/ThreeDivides.thy Sat Jan 16 17:15:28 2010 +0100 +++ b/src/HOL/ex/ThreeDivides.thy Thu Jan 21 09:27:57 2010 +0100 @@ -178,21 +178,17 @@ lemma exp_exists: "m = (\x "nlen m" arbitrary: m) +proof (induct "nlen m" arbitrary: m) case 0 thus ?case by (simp add: nlen_zero) next case (Suc nd) - hence IH: - "nd = nlen (m div 10) \ - m div 10 = (\x c < 10" and cdef: "c = m mod 10" by simp show "m = (\xxx y \ ubasis_le (basis_emb x) (basis_emb y)" -proof (induct n \ "max (place x) (place y)" arbitrary: x y rule: less_induct) - case (less n) - hence IH: - "\(a::'a compact_basis) b. - \max (place a) (place b) < max (place x) (place y); a \ b\ - \ ubasis_le (basis_emb a) (basis_emb b)" - by simp +proof (induct "max (place x) (place y)" arbitrary: x y rule: less_induct) + case less show ?case proof (rule linorder_cases) assume "place x < place y" then have "rank x < rank y" @@ -709,7 +704,7 @@ apply (case_tac "y = compact_bot", simp) apply (simp add: basis_emb.simps [of y]) apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) - apply (rule IH) + apply (rule less) apply (simp add: less_max_iff_disj) apply (erule place_sub_less) apply (erule rank_less_imp_below_sub [OF `x \ y`]) @@ -724,7 +719,7 @@ apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal) apply (simp add: basis_emb.simps [of x]) apply (rule ubasis_le_upper [OF fin2], simp) - apply (rule IH) + apply (rule less) apply (simp add: less_max_iff_disj) apply (erule place_sub_less) apply (erule rev_below_trans) diff -r 156925dd67af -r d62eddd9e253 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/Pure/Isar/proof.ML Thu Jan 21 09:27:57 2010 +0100 @@ -387,7 +387,7 @@ fun no_goal_cases st = map (rpair NONE) (goals st); fun goal_cases st = - Rule_Cases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); + Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); fun apply_method current_context meth state = let diff -r 156925dd67af -r d62eddd9e253 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/Pure/Isar/rule_cases.ML Thu Jan 21 09:27:57 2010 +0100 @@ -25,8 +25,8 @@ binds: (indexname * term option) list, cases: (string * T) list} val strip_params: term -> (string * typ) list - val make_common: bool -> theory * term -> (string * string list) list -> cases - val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases + val make_common: theory * term -> (string * string list) list -> cases + val make_nested: term -> theory * term -> (string * string list) list -> cases val apply: term list -> T -> T val consume: thm list -> thm list -> ('a * int) * thm -> (('a * (int * thm list)) * thm) Seq.seq @@ -43,6 +43,7 @@ val get: thm -> (string * string list) list * int val rename_params: string list list -> thm -> thm val params: string list list -> attribute + val internalize_params: thm -> thm val mutual_rule: Proof.context -> thm list -> (int list * thm) option val strict_mutual_rule: Proof.context -> thm list -> int list * thm end; @@ -90,18 +91,15 @@ chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop) in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end; -fun extract_case is_open thy (case_outline, raw_prop) name concls = +fun extract_case thy (case_outline, raw_prop) name concls = let - val rename = if is_open then I else apfst (Name.internal o Name.clean); - val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop); val len = length props; val nested = is_some case_outline andalso len > 1; fun extract prop = let - val (fixes1, fixes2) = extract_fixes case_outline prop - |> apfst (map rename); + val (fixes1, fixes2) = extract_fixes case_outline prop; val abs_fixes = abs (fixes1 @ fixes2); fun abs_fixes1 t = if not nested then abs_fixes t @@ -135,7 +133,7 @@ else SOME (nested_case (hd cases)) end; -fun make is_open rule_struct (thy, prop) cases = +fun make rule_struct (thy, prop) cases = let val n = length cases; val nprems = Logic.count_prems prop; @@ -143,13 +141,13 @@ ((case try (fn () => (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of NONE => (name, NONE) - | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1); + | SOME p => (name, extract_case thy p name concls)) :: cs, i - 1); in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end; in -fun make_common is_open = make is_open NONE; -fun make_nested is_open rule_struct = make is_open (SOME rule_struct); +val make_common = make NONE; +fun make_nested rule_struct = make (SOME rule_struct); fun apply args = let @@ -334,6 +332,20 @@ fun params xss = Thm.rule_attribute (K (rename_params xss)); +(* internalize parameter names *) + +fun internalize_params rule = + let + fun rename prem = + let val xs = + map (Name.internal o Name.clean o fst) (Logic.strip_params prem) + in Logic.list_rename_params (xs, prem) end; + fun rename_prems prop = + let val (As, C) = Logic.strip_horn (Thm.prop_of rule) + in Logic.list_implies (map rename As, C) end; + in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; + + (** mutual_rule **) diff -r 156925dd67af -r d62eddd9e253 src/Tools/induct.ML --- a/src/Tools/induct.ML Sat Jan 16 17:15:28 2010 +0100 +++ b/src/Tools/induct.ML Thu Jan 21 09:27:57 2010 +0100 @@ -10,6 +10,8 @@ val atomize: thm list val rulify: thm list val rulify_fallback: thm list + val dest_def: term -> (term * term) option + val trivial_tac: int -> tactic end; signature INDUCT = @@ -42,6 +44,9 @@ val coinduct_type: string -> attribute val coinduct_pred: string -> attribute val coinduct_del: attribute + val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic + val add_simp_rule: attribute + val no_simpN: string val casesN: string val inductN: string val coinductN: string @@ -50,19 +55,24 @@ val setN: string (*proof methods*) val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic - val add_defs: (binding option * term) option list -> Proof.context -> + val add_defs: (binding option * (term * bool)) option list -> Proof.context -> (term option list * thm list) * Proof.context val atomize_term: theory -> term -> term + val atomize_cterm: conv val atomize_tac: int -> tactic val inner_atomize_tac: int -> tactic val rulified_term: thm -> theory * term val rulify_tac: int -> tactic + val simplified_rule: Proof.context -> thm -> thm + val simplify_tac: Proof.context -> int -> tactic + val trivial_tac: int -> tactic + val rotate_tac: int -> int -> int -> tactic val internalize: int -> thm -> thm val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq val cases_tac: Proof.context -> term option list list -> thm option -> thm list -> int -> cases_tactic val get_inductT: Proof.context -> term option list list -> thm list list - val induct_tac: Proof.context -> (binding option * term) option list list -> + val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> cases_tactic val coinduct_tac: Proof.context -> term option list -> term option list -> thm option -> @@ -107,6 +117,77 @@ +(** constraint simplification **) + +(* rearrange parameters and premises to allow application of one-point-rules *) + +fun swap_params_conv ctxt i j cv = + let + fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt + | conv1 k ctxt = + Conv.rewr_conv @{thm swap_params} then_conv + Conv.forall_conv (conv1 (k-1) o snd) ctxt + fun conv2 0 ctxt = conv1 j ctxt + | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt + in conv2 i ctxt end; + +fun swap_prems_conv 0 = Conv.all_conv + | swap_prems_conv i = + Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv + Conv.rewr_conv Drule.swap_prems_eq + +fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt); + +fun find_eq ctxt t = + let + val l = length (Logic.strip_params t); + val Hs = Logic.strip_assums_hyp t; + fun find (i, t) = + case Data.dest_def (drop_judgment ctxt t) of + SOME (Bound j, _) => SOME (i, j) + | SOME (_, Bound j) => SOME (i, j) + | _ => NONE + in + case get_first find (map_index I Hs) of + NONE => NONE + | SOME (0, 0) => NONE + | SOME (i, j) => SOME (i, l-j-1, j) + end; + +fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of + NONE => NONE + | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct); + +val rearrange_eqs_simproc = Simplifier.simproc + (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"] + (fn thy => fn ss => fn t => + mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t)) + +(* rotate k premises to the left by j, skipping over first j premises *) + +fun rotate_conv 0 j 0 = Conv.all_conv + | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1) + | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k); + +fun rotate_tac j 0 = K all_tac + | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv + j (length (Logic.strip_assums_hyp goal) - j - k) k) i); + +(* rulify operators around definition *) + +fun rulify_defs_conv ctxt ct = + if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso + not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct)))) + then + (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv + Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt)) + (Conv.try_conv (rulify_defs_conv ctxt)) else_conv + Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv + Conv.try_conv (rulify_defs_conv ctxt)) ct + else Conv.no_conv ct; + + + (** induct data **) (* rules *) @@ -132,23 +213,25 @@ structure InductData = Generic_Data ( - type T = (rules * rules) * (rules * rules) * (rules * rules); + type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset; val empty = ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), - (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2))); + (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)), + empty_ss addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]); val extend = I; - fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)), - ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) = + fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1), + ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) = ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)), - (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)), - (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2))); + (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)), + (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)), + merge_ss (simpset1, simpset2)); ); val get_local = InductData.get o Context.Proof; fun dest_rules ctxt = - let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in + let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in {type_cases = Item_Net.content casesT, pred_cases = Item_Net.content casesP, type_induct = Item_Net.content inductT, @@ -158,7 +241,7 @@ end; fun print_rules ctxt = - let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in + let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in [pretty_rules ctxt "coinduct type:" coinductT, pretty_rules ctxt "coinduct pred:" coinductP, pretty_rules ctxt "induct type:" inductT, @@ -206,9 +289,10 @@ fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs => fold Item_Net.remove (filter_rules rs th) rs)))); -fun map1 f (x, y, z) = (f x, y, z); -fun map2 f (x, y, z) = (x, f y, z); -fun map3 f (x, y, z) = (x, y, f z); +fun map1 f (x, y, z, s) = (f x, y, z, s); +fun map2 f (x, y, z, s) = (x, f y, z, s); +fun map3 f (x, y, z, s) = (x, y, f z, s); +fun map4 f (x, y, z, s) = (x, y, z, f s); fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x; fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x; @@ -234,12 +318,17 @@ val coinduct_pred = mk_att add_coinductP consumes1; val coinduct_del = del_att map3; +fun map_simpset f = InductData.map (map4 f); +fun add_simp_rule (ctxt, thm) = + (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm); + end; (** attribute syntax **) +val no_simpN = "no_simp"; val casesN = "cases"; val inductN = "induct"; val coinductN = "coinduct"; @@ -268,7 +357,9 @@ Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del) "declaration of induction rule" #> Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del) - "declaration of coinduction rule"; + "declaration of coinduction rule" #> + Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule) + "declaration of rules for simplifying induction or cases rules"; end; @@ -362,7 +453,8 @@ ruleq |> Seq.maps (Rule_Cases.consume [] facts) |> Seq.maps (fn ((cases, (_, more_facts)), rule) => - CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases) + CASES (Rule_Cases.make_common (thy, + Thm.prop_of (Rule_Cases.internalize_params rule)) cases) (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) end; @@ -409,6 +501,22 @@ (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac); +(* simplify *) + +fun simplify_conv ctxt ct = + if exists_subterm (is_some o Data.dest_def) (term_of ct) then + (Conv.try_conv (rulify_defs_conv ctxt) then_conv + Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)))) ct + else Conv.all_conv ct; + +fun simplified_rule ctxt thm = + Conv.fconv_rule (Conv.prems_conv ~1 (simplify_conv ctxt)) thm; + +fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt); + +val trivial_tac = Data.trivial_tac; + + (* prepare rule *) fun rule_instance ctxt inst rule = @@ -548,11 +656,19 @@ fun add_defs def_insts = let - fun add (SOME (SOME x, t)) ctxt = + fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt) + | add (SOME (SOME x, (t, _))) ctxt = let val ([(lhs, (_, th))], ctxt') = LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt in ((SOME lhs, [th]), ctxt') end - | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) + | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt) + | add (SOME (NONE, (t, _))) ctxt = + let + val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt); + val ([(lhs, (_, th))], ctxt') = + LocalDefs.add_defs [((Binding.name s, NoSyn), + (Thm.empty_binding, t))] ctxt + in ((SOME lhs, [th]), ctxt') end | add NONE ctxt = ((NONE, []), ctxt); in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; @@ -576,12 +692,12 @@ fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) | get_inductP _ _ = []; -fun induct_tac ctxt def_insts arbitrary taking opt_rule facts = +fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts = let val thy = ProofContext.theory_of ctxt; val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; - val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; + val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs; fun inst_rule (concls, r) = (if null insts then `Rule_Cases.get r @@ -601,8 +717,10 @@ |> tap (trace_rules ctxt inductN o map #2) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); - fun rule_cases rule = - Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule); + fun rule_cases ctxt rule = + let val rule' = (if simp then simplified_rule ctxt else I) + (Rule_Cases.internalize_params rule); + in Rule_Cases.make_nested (Thm.prop_of rule') (rulified_term rule') end; in (fn i => fn st => ruleq @@ -610,19 +728,32 @@ |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => (CONJUNCTS (ALLGOALS - (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1)) - THEN' fix_tac defs_ctxt - (nth concls (j - 1) + more_consumes) - (nth_list arbitrary (j - 1)))) + let + val adefs = nth_list atomized_defs (j - 1); + val frees = fold (Term.add_frees o prop_of) adefs []; + val xs = nth_list arbitrary (j - 1); + val k = nth concls (j - 1) + more_consumes + in + Method.insert_tac (more_facts @ adefs) THEN' + (if simp then + rotate_tac k (length adefs) THEN' + fix_tac defs_ctxt k + (List.partition (member op = frees) xs |> op @) + else + fix_tac defs_ctxt k xs) + end) THEN' inner_atomize_tac) j)) THEN' atomize_tac) i st |> Seq.maps (fn st' => guess_instance ctxt (internalize more_consumes rule) i st' |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking)) |> Seq.maps (fn rule' => - CASES (rule_cases rule' cases) + CASES (rule_cases ctxt rule' cases) (Tactic.rtac rule' i THEN PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) - THEN_ALL_NEW_CASES rulify_tac + THEN_ALL_NEW_CASES + ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) + else K all_tac) + THEN_ALL_NEW rulify_tac) end; @@ -672,7 +803,8 @@ guess_instance ctxt rule i st |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking)) |> Seq.maps (fn rule' => - CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases) + CASES (Rule_Cases.make_common (thy, + Thm.prop_of (Rule_Cases.internalize_params rule')) cases) (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) end; @@ -711,10 +843,15 @@ val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; +val inst' = Scan.lift (Args.$$$ "_") >> K NONE || + Args.term >> (SOME o rpair false) || + Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --| + Scan.lift (Args.$$$ ")"); + val def_inst = ((Scan.lift (Args.binding --| (Args.$$$ "\" || Args.$$$ "==")) >> SOME) - -- Args.term) >> SOME || - inst >> Option.map (pair NONE); + -- (Args.term >> rpair false)) >> SOME || + inst' >> Option.map (pair NONE); val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); @@ -740,11 +877,11 @@ val induct_setup = Method.setup @{binding induct} - (P.and_list' (Scan.repeat (unless_more_args def_inst)) -- - (arbitrary -- taking -- Scan.option induct_rule) >> - (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt => + (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) -- + (arbitrary -- taking -- Scan.option induct_rule)) >> + (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => RAW_METHOD_CASES (fn facts => - Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))))) + Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))) "induction on types or predicates/sets"; val coinduct_setup = diff -r 156925dd67af -r d62eddd9e253 src/Tools/jEdit/README_BUILD --- a/src/Tools/jEdit/README_BUILD Sat Jan 16 17:15:28 2010 +0100 +++ b/src/Tools/jEdit/README_BUILD Thu Jan 21 09:27:57 2010 +0100 @@ -31,6 +31,9 @@ * Isabelle/Pure Scala components Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar +* Scala Compiler + Netbeans Library "Scala-compiler" = $SCALA_HOME/lib/scala-compiler.jar + Running the application within Netbeans =======================================