--- 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 ***
--- 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
);
*}
--- 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 \<equiv> "deg R f" arbitrary: "f" rule: nat_less_induct)
- fix n f
- assume hypo: "\<forall>m<n. \<forall>x. x \<in> carrier P \<longrightarrow>
- deg R g \<le> deg R x \<longrightarrow>
- m = deg R x \<longrightarrow>
- (\<exists>q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> x = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
- and prem: "n = deg R f" and f_in_P [simp]: "f \<in> carrier P"
- and deg_g_le_deg_f: "deg R g \<le> deg R f"
+ proof (induct "deg R f" arbitrary: "f" rule: less_induct)
+ case less
+ note f_in_P [simp] = `f \<in> carrier P`
+ and deg_g_le_deg_f = `deg R g \<le> deg R f`
let ?k = "1::nat" and ?r = "(g \<otimes>\<^bsub>P\<^esub> (monom P (lcoeff f) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)"
and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
show "\<exists> q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^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 (\<ominus>\<^bsub>P\<^esub> ?r) < n"
+ have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
proof -
have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
also have "\<dots> < deg R f"
proof (rule deg_lcoeff_cancel)
show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> 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 \<otimes>\<^bsub>P\<^esub> ?q) \<le> 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}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
unfolding Pi_def using deg_g_le_deg_f by force
qed (simp_all add: deg_f_nzero)
- finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n" unfolding prem .
+ finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
qed
moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
@@ -1660,7 +1656,7 @@
ultimately obtain q' r' k'
where rem_desc: "lcoeff g (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?r) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> 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
--- 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 @@
"\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk>
\<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
proof -
- note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
- note converse_rtranclE = converse_rtranclE [consumes 1]
assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
assume "(a,x)\<in>r\<^sup>*"
then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>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:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
by auto
--- 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:
-"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
- \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc;
- x\<in>superclasses G D
-\<rbrakk> \<Longrightarrow> x\<in>superclasses G C"
-proof -
-
- assume ws: "ws_prog G" and
- cls_C: "class G C = Some c" and
- wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
- \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
- assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
- thus "\<And> c. \<lbrakk>class G C = Some c; x\<in>superclasses G D\<rbrakk>\<Longrightarrow>
- x\<in>superclasses G C" (is "PROP ?P C"
- is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP D \<Longrightarrow> ?SUP C")
- proof (induct ?P C rule: converse_trancl_induct)
- fix C c
- assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1D" "class G C = Some c" "x \<in> 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\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S \<prec>\<^sub>C D"
- and hyp : "\<And> s. \<lbrakk>class G S = Some s; x \<in> superclasses G D\<rbrakk>
- \<Longrightarrow> x \<in> superclasses G S"
- and cls_C': "class G C = Some c"
- and x: "x \<in> 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\<turnstile>C\<prec>\<^sub>C D"
+ and ws: "ws_prog G"
+ and cls_C: "class G C = Some c"
+ and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
+ \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
+ and x: "x\<in>superclasses G D"
+ shows "x\<in>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\<in>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:
-"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
- \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc
- \<rbrakk> \<Longrightarrow> D\<in>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: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
- \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
- assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
- thus "\<And> c. class G C = Some c\<Longrightarrow> D\<in>superclasses G C"
- (is "PROP ?P C" is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP C")
- proof (induct ?P C rule: converse_trancl_induct)
- fix C c
- assume "G\<turnstile>C \<prec>\<^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\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S\<prec>\<^sub>C D"
- "\<And>s. class G S = Some s \<Longrightarrow> D \<in> 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\<turnstile>C\<prec>\<^sub>C D"
+ and ws: "ws_prog G"
+ and cls_C: "class G C = Some c"
+ and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
+ \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
+ shows "D\<in>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
--- 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
\<Longrightarrow> G\<turnstile>(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': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
lemma subint_widen_imethds:
- "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>
- \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and>
+ assumes irel: "G\<turnstile>I\<preceq>I J"
+ and wf: "wf_prog G"
+ and is_iface: "is_iface G J"
+ and jm: "jm \<in> imethds G J sig"
+ shows "\<exists>im \<in> imethds G I sig. is_static im = is_static jm \<and>
accmodi im = accmodi jm \<and>
G\<turnstile>resTy im\<preceq>resTy jm"
-proof -
- assume irel: "G\<turnstile>I\<preceq>I J" and
- wf: "wf_prog G" and
- is_iface: "is_iface G J"
- from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis"
- (is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I")
- proof (induct ?P I rule: converse_rtrancl_induct)
- case Id
- assume "jm \<in> 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\<turnstile>I \<prec>I1 SI" and
- subint_SI_J: "G\<turnstile>SI \<preceq>I J" and
- hyp: "PROP ?P SI" and
- jm: "jm \<in> imethds G J sig"
- from subint1_I_SI
+ case (step I SI)
+ from `G\<turnstile>I \<prec>I1 SI`
obtain i where
ifI: "iface G I = Some i" and
SI: "SI \<in> set (isuperIfs i)"
@@ -1784,10 +1774,10 @@
let ?newMethods
= "(Option.set \<circ> table_of (map (\<lambda>(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 \<times> mhead" where
sim: "sim \<in> 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 "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
\<Longrightarrow> 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 \<noteq> Object"
+ case (Subcls C c)
let ?newMethods = "table_of (map (\<lambda>(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)
--- 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}
--- 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 "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
then have step: "\<And>n. P (of_nat n) \<Longrightarrow> 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
--- 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 :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^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\<equiv>"maxindex p" arbitrary: p n0 rule: nat_less_induct)
- fix n p n0
- assume H: "\<forall>m<n. \<forall>p n0. isnpolyh p n0 \<longrightarrow>
- (\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)) \<longrightarrow> m = maxindex p \<longrightarrow> p = 0\<^sub>p"
- and np: "isnpolyh p n0" and zp: "\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^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 = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^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 \<noteq> 0"
+ {assume nz: "maxindex p \<noteq> 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 \<le> n" unfolding n by auto
- with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < n" by auto
+ have mihn: "maxindex ?h \<le> 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: " \<forall>x. wf_bs (x#?ts) ?h" by simp
- from ihd_lt_n have "ALL x. length (x#?ts) \<le> n" by simp
- with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast
- hence "\<forall> 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) \<le> maxindex p" by simp
+ with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
+ hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
hence "\<forall> 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 "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp
hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext)
hence "\<forall> c \<in> 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 "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^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) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p)
\<and> (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
using ns
-proof(induct d\<equiv>"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 = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
@@ -1366,20 +1363,13 @@
\<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
let ?ths = "?dths \<and> ?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: "\<forall>m<d. \<forall>x xa xb xc xd.
- isnpolyh x xd \<longrightarrow>
- m = degree x \<longrightarrow> ?D (a, n, p, xa, x) \<and>
- (polydivide_aux (a, n, p, xa, x) = (xb, xc) \<longrightarrow>
- xa \<le> xb \<and> (degree xc = 0 \<or> degree xc < degree p) \<and>
- (\<exists> nr. isnpolyh xc nr) \<and>
- (\<exists>q n1. isnpolyh q n1 \<and> 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 \<noteq> 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': "\<not> d < n" hence dn: "d \<ge> n" by arith
+ {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> 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 \<or> 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 \<or> 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 \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
and q1:"\<exists>q nq. isnpolyh q nq \<and> (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 " \<forall>(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 "\<forall>(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 "\<forall>(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 \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?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 " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
hence "\<forall>(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 "\<dots> = (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 \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
and dr: "degree r = 0 \<or> 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:"\<forall>(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: "\<forall> (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
}
--- 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
--- 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: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
shows "P a b"
-proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
- fix n a b
- assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
+proof(induct "a + b" arbitrary: a b rule: less_induct)
+ case less
have "a = b \<or> a < b \<or> 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 \<or> a = 0" using H(2) by arith
+ hence "a + b - a < a + b \<or> 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 \<or> b = 0" using H(2) by arith
+ hence "b + a - b < a + b \<or> 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
--- 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 \<longrightarrow> B"
induct_equal where "induct_equal x y == x = y"
induct_conj where "induct_conj A B == A \<and> B"
+ induct_true where "induct_true == True"
+ induct_false where "induct_false == False"
lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>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 (\<lambda>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 \<Longrightarrow> 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
--- 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 = `\<And>x. A (a x) \<Longrightarrow> n = a x \<Longrightarrow> P (a x)`
+ note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)`
and prem = `A (a x)`
and defn = `Suc n = a x`
show "P (a x)" sorry
--- 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 \<le> f n"
- proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)
- case (less k n)
- then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
+ proof (induct "f n" arbitrary: n rule: less_induct)
+ case less
show "n \<le> 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 \<le> f (f m)" .
+ with less have "f m \<le> f (f m)" .
also from f_ax have "\<dots> < f n" by (simp only: Suc)
finally have "f m < f n" .
- with hyp have "m \<le> f m" .
+ with less have "m \<le> f m" .
also note `\<dots> < f n`
finally have "m < f n" .
then have "n \<le> f n" by (simp only: Suc)
--- 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 "\<exists>z::complex. poly p z = 0"
using nc
-proof(induct n\<equiv> "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: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p"
let ?ths = "\<exists>z. ?p z = 0"
- from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
+ from nonconstant_length[OF less(2)] have n2: "psize p \<ge> 2" .
from poly_minimum_modulus obtain c where
c: "\<forall>w. cmod (?p c) \<le> 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 "\<dots> = ?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: "\<not> constant (poly q)" by blast
from q(2) have pqc0: "?p c = poly q 0" by simp
from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
@@ -682,8 +681,8 @@
from poly_decompose[OF rnc] obtain k a s where
kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
"\<forall>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 "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
moreover
- {assume kn: "k+1 \<noteq> n"
- from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
+ {assume kn: "psize p \<noteq> k+1"
+ from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p" by simp
have th01: "\<not> 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)
--- 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 \<noteq> 0` have "finite {x. poly k x = 0}" by (rule Suc.hyps)
+ then have "finite {x. poly k x = 0}" using `k \<noteq> 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
--- 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 "\<exists>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 `\<exists>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"
--- 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
--- 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 \<and> 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"\<Sum>"}*}
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) \<leftarrow> xss]) # transpose (xs # [t. (h#t) \<leftarrow> xss])"
+by pat_completeness auto
+
+lemma transpose_aux_filter_head:
+ "concat (map (list_case [] (\<lambda>h t. [h])) xss) =
+ map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
+ by (induct xss) (auto split: list.split)
+
+lemma transpose_aux_filter_tail:
+ "concat (map (list_case [] (\<lambda>h t. [t])) xss) =
+ map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
+ by (induct xss) (auto split: list.split)
+
+lemma transpose_aux_max:
+ "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
+ Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
+ (is "max _ ?foldB = Suc (max _ ?foldA)")
+proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
+ case True
+ hence "foldr (\<lambda>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 (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
+ by (induct xss) auto
+ have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
+ by (induct xss) auto
+
+ have "0 < ?foldB"
+ proof -
+ from False
+ obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
+ hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
+ hence "z \<noteq> []" 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 (\<lambda>xs. foldr (\<lambda>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 = []) \<longleftrightarrow> (\<forall>x \<in> set xs. x = [])"
+ by (induct rule: transpose.induct) simp_all
+
+lemma length_transpose:
+ fixes xs :: "'a list list"
+ shows "length (transpose xs) = foldr (\<lambda>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 (\<lambda>xs. xs ! i) [ys \<leftarrow> 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 \<noteq> []" 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 *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
+ have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
+ { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
+ by (cases x) simp_all
+ } note *** = this
+
+ have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>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 \<Longrightarrow> sorted (takeWhile P xs)"
apply (subst takeWhile_eq_take) by (rule sorted_take)
+lemma sorted_filter:
+ "sorted (map f xs) \<Longrightarrow> 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 \<leftarrow> xs. t < f x] = takeWhile (\<lambda> 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 \<in> 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) \<le>
+ (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 \<le> f (?dW ! 0)"
+ unfolding nth_append_length_plus nth_i
+ using i preorder_class.le_less_trans[OF le0 i] by simp
+ also have "... \<le> 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 "\<not> t < f x" by simp
+qed
+
end
lemma sorted_upt[simp]: "sorted[i..<j]"
@@ -3416,6 +3565,153 @@
apply(simp add:sorted_Cons)
done
+subsubsection {*@{const transpose} on sorted lists*}
+
+lemma sorted_transpose[simp]:
+ shows "sorted (rev (map length (transpose xs)))"
+ by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose
+ length_filter_conv_card intro: card_mono)
+
+lemma transpose_max_length:
+ "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
+ (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 \<leftarrow> xs. x \<noteq> []] = []"
+ 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 \<leftarrow> 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 (\<lambda>ys. i < length ys) (transpose xs)) = length (xs ! i)"
+proof -
+ have "xs \<noteq> []" using `i < length xs` by auto
+ note filter_equals_takeWhile_sorted_rev[OF sorted, simp]
+ { fix j assume "j \<le> 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) \<and> 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 (\<lambda>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 \<noteq> []` sortedE[OF le0]
+ by (auto simp: length_transpose comp_def foldr_map)
+
+ have "Suc i \<le> length (takeWhile (\<lambda>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 (\<lambda>ys. ys ! i) (filter (\<lambda>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 \<le> length (takeWhile (\<lambda>ys. Suc j \<le> length ys) xs)"
+ proof (rule length_takeWhile_less_P_nth)
+ show "Suc i \<le> length xs" using `i < length xs` by simp
+ fix k assume "k < Suc i"
+ hence "k \<le> i" by auto
+ with sorted_rev_nth_mono[OF sorted this] `i < length xs`
+ have "length (xs ! i) \<le> length (xs ! k)" by simp
+ thus "Suc j \<le> length (xs ! k)" using j_less by simp
+ qed
+ have i_less_filter: "i < length [ys\<leftarrow>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 (\<lambda>x. x \<noteq> []) 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 = [] \<Longrightarrow> n = 0"
+ assumes rect: "\<And> i. i < length xs \<Longrightarrow> length (xs ! i) = n"
+ shows "transpose xs = map (\<lambda> i. map (\<lambda> j. xs ! j ! i) [0..<length xs]) [0..<n]"
+ (is "?trans = ?map")
+proof (rule nth_equalityI)
+ have "sorted (rev (map length xs))"
+ by (auto simp: rev_nth rect intro!: sorted_nth_monoI)
+ from foldr_max_sorted[OF this] assms
+ show len: "length ?trans = length ?map"
+ by (simp_all add: length_transpose foldr_map comp_def)
+ moreover
+ { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"
+ using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
+ ultimately show "\<forall>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
--- 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]:
"\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow>
- (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
-proof (induct ?P b)
- show "?P []" by simp
+ (\<exists>t. b!n = OK t \<and> (G \<turnstile> (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]:
-"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
-proof (induct ?P x)
- show "?P []" by simp
+"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> 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 \<le> length (l # ls)"
--- 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 \<Rightarrow> real"
assume IA:"\<And>u s. \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;
- s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n \<equiv> card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
- as:"Suc n \<equiv> card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
+ s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
+ as:"Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
"finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1"
have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr)
assume " \<not> (\<exists>x\<in>s. u x \<noteq> 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\<in>s" by auto
show ?thesis unfolding caratheodory[of s]
- proof(induct "CARD('n) + 1")
+ proof(induct ("CARD('n) + 1"))
have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
using compact_empty by (auto simp add: convex_hull_empty)
case 0 thus ?case unfolding * by simp
--- 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 \<subseteq> span t"
shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
using f i sp
-proof(induct c\<equiv>"card(t - s)" arbitrary: s t rule: nat_less_induct)
- fix n:: nat and s t :: "('a ^'n) set"
- assume H: " \<forall>m<n. \<forall>(x:: ('a ^'n) set) xa.
- finite xa \<longrightarrow>
- independent x \<longrightarrow>
- x \<subseteq> span xa \<longrightarrow>
- m = card (xa - x) \<longrightarrow>
- (\<exists>t'. (card t' = card xa) \<and> finite t' \<and>
- x \<subseteq> t' \<and> t' \<subseteq> x \<union> xa \<and> x \<subseteq> span t')"
- and ft: "finite t" and s: "independent s" and sp: "s \<subseteq> 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 \<subseteq> span t`
let ?P = "\<lambda>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
let ?ths = "\<exists>t'. ?P t'"
{assume st: "s \<subseteq> t"
@@ -3568,12 +3560,12 @@
{assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast
from b have "t - {b} - s \<subset> 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 \<noteq> 0" by auto
{assume stb: "s \<subseteq> 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 \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u" and fu: "finite u" by blast
let ?w = "insert b u"
have th0: "s \<subseteq> insert b u" using u by blast
@@ -3594,8 +3586,8 @@
from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})" by blast
have ab: "a \<noteq> b" using a b by blast
have at: "a \<notin> 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 \<in> s"
have t: "t \<subseteq> (insert b (insert a (t -{b})))" using b by auto
@@ -3608,7 +3600,7 @@
from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))" .}
then have sp': "s \<subseteq> 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 \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
"s \<subseteq> 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) \<subseteq> V" and iS: "independent S"
shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
using sv iS
-proof(induct d\<equiv> "CARD('n) - card S" arbitrary: S rule: nat_less_induct)
- fix n and S:: "(real^'n) set"
- assume H: "\<forall>m<n. \<forall>S \<subseteq> V. independent S \<longrightarrow> m = CARD('n) - card S \<longrightarrow>
- (\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B)"
- and sv: "S \<subseteq> 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 \<subseteq> V` and i = `independent S`
let ?P = "\<lambda>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
let ?ths = "\<exists>x. ?P x"
let ?d = "CARD('n)"
@@ -3674,11 +3664,11 @@
have th0: "insert a S \<subseteq> 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 \<subseteq> B" "B \<subseteq> V" "independent B" " V \<subseteq> span B"
by blast
from B have "?P B" by auto
--- 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 \<Rightarrow> bool"
and undefined_fast_The :: 'a
and undefined_fast_Eps :: 'a
and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
and bisim_iterator_max :: bisim_iterator
+ and Quot :: "'a \<Rightarrow> 'b"
+ and quot_normal :: "'a \<Rightarrow> 'a"
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> '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
--- 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\<turnstile>c>b]) \<longrightarrow>\<^isub>a M'" "a\<noteq>b"
shows "\<exists>M0. M0[a\<turnstile>c>b]=M' \<and> M \<longrightarrow>\<^isub>a M0"
using a
-apply(nominal_induct M\<equiv>"M[a\<turnstile>c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
-apply(simp)
+apply(nominal_induct "M[a\<turnstile>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\<turnstile>n>y]) \<longrightarrow>\<^isub>a M'" "x\<noteq>y"
shows "\<exists>M0. M0[x\<turnstile>n>y]=M' \<and> M \<longrightarrow>\<^isub>a M0"
using a
-apply(nominal_induct M\<equiv>"M[x\<turnstile>n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
-apply(simp)
+apply(nominal_induct "M[x\<turnstile>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 *)
--- 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 `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N`
and `\<Gamma> \<turnstile> P<:Q`
show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N"
- proof (induct \<Gamma>\<equiv>"\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct)
- case (SA_Top _ S \<Gamma> X \<Delta>)
- then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok"
- and lh_drv_prm\<^isub>2: "S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
- have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
- hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
- with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
+ proof (induct "\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct)
+ case (SA_Top S \<Gamma> X \<Delta>)
+ from `\<Gamma> \<turnstile> P <: Q`
+ have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
+ with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
+ by (simp add: replace_type)
moreover
- from lh_drv_prm\<^isub>2 have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)"
+ from `S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)"
by (simp add: closed_in_def doms_append)
ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
next
- case (SA_trans_TVar Y S _ N \<Gamma> X \<Delta>)
+ case (SA_trans_TVar Y S N \<Gamma> X \<Delta>)
then have IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
and lh_drv_prm: "(TVarB Y S) \<in> set (\<Delta>@[(TVarB X Q)]@\<Gamma>)"
and rh_drv: "\<Gamma> \<turnstile> P<:Q"
@@ -1020,23 +1019,23 @@
then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
qed
next
- case (SA_refl_TVar _ Y \<Gamma> X \<Delta>)
- then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok"
- and lh_drv_prm\<^isub>2: "Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
- have "\<Gamma> \<turnstile> P <: Q" by fact
- hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
- with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
+ case (SA_refl_TVar Y \<Gamma> X \<Delta>)
+ from `\<Gamma> \<turnstile> P <: Q`
+ have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
+ with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
+ by (simp add: replace_type)
moreover
- from lh_drv_prm\<^isub>2 have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)" by (simp add: doms_append)
+ from `Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)"
+ by (simp add: doms_append)
ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> 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 \<Gamma> X \<Delta>)
+ case (SA_arrow S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Gamma> X \<Delta>)
then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast
next
- case (SA_all _ T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
- from SA_all(2,4,5,6)
+ case (SA_all T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
have IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"
- and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" by force+
+ and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"
+ by (fastsimp intro: SA_all)+
then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)" by auto
qed
}
@@ -1263,7 +1262,7 @@
assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
shows "\<turnstile> (\<Gamma> @ \<Delta>) ok"
using assms
-proof (induct \<Gamma>' \<equiv> "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>)
+proof (induct "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>)
case valid_nil
have "[] = \<Gamma> @ VarB x Q # \<Delta>" by fact
then have "False" by auto
@@ -1314,14 +1313,14 @@
and "\<turnstile> (\<Delta> @ B # \<Gamma>) ok"
shows "(\<Delta> @ B # \<Gamma>) \<turnstile> t : T"
using assms
-proof(nominal_induct \<Gamma>'\<equiv> "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct)
- case (T_Var x' T \<Gamma>' \<Gamma>'' \<Delta>')
+proof(nominal_induct "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct)
+ case (T_Var x T)
then show ?case by auto
next
- case (T_App \<Gamma> t\<^isub>1 T\<^isub>1 T\<^isub>2 t\<^isub>2 \<Gamma> \<Delta>)
+ 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 \<Gamma>' t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
+ case (T_Abs y T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
then have "VarB y T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
by (auto dest: typing_ok)
@@ -1336,22 +1335,22 @@
apply (rule closed)
done
then have "\<turnstile> ((VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
- then have "(VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
- by (rule T_Abs) (simp add: T_Abs)
+ with _ have "(VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
+ by (rule T_Abs) simp
then have "VarB y T\<^isub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
then show ?case by (rule typing.T_Abs)
next
- case (T_Sub \<Gamma>' t S T \<Delta> \<Gamma>)
- from `\<turnstile> (\<Delta> @ B # \<Gamma>) ok` and `\<Gamma>' = \<Delta> @ \<Gamma>`
+ case (T_Sub t S T \<Delta> \<Gamma>)
+ from refl and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
have "\<Delta> @ B # \<Gamma> \<turnstile> t : S" by (rule T_Sub)
- moreover from `\<Gamma>'\<turnstile>S<:T` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
+ moreover from `(\<Delta> @ \<Gamma>)\<turnstile>S<:T` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
have "(\<Delta> @ B # \<Gamma>)\<turnstile>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 \<Gamma>' t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
- then have "TVarB X T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
- then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
+ case (T_TAbs X T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
+ from `TVarB X T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2`
+ have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
by (auto dest: typing_ok)
have "\<turnstile> (TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma>) ok"
apply (rule valid_consT)
@@ -1364,15 +1363,15 @@
apply (rule closed)
done
then have "\<turnstile> ((TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
- then have "(TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
- by (rule T_TAbs) (simp add: T_TAbs)
+ with _ have "(TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
+ by (rule T_TAbs) simp
then have "TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
then show ?case by (rule typing.T_TAbs)
next
- case (T_TApp X \<Gamma>' t\<^isub>1 T2 T11 T12 \<Delta> \<Gamma>)
+ case (T_TApp X t\<^isub>1 T2 T11 T12 \<Delta> \<Gamma>)
have "\<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T11. T12)"
- by (rule T_TApp)+
- moreover from `\<Gamma>'\<turnstile>T2<:T11` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
+ by (rule T_TApp refl)+
+ moreover from `(\<Delta> @ \<Gamma>)\<turnstile>T2<:T11` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
have "(\<Delta> @ B # \<Gamma>)\<turnstile>T2<:T11"
by (rule weakening) (simp add: extends_def T_TApp)
ultimately show ?case by (rule better_T_TApp)
@@ -1393,24 +1392,22 @@
assumes "(\<Gamma> @ VarB x Q # \<Delta>) \<turnstile> S <: T"
shows "(\<Gamma>@\<Delta>) \<turnstile> S <: T"
using assms
-proof (induct \<Gamma>' \<equiv> "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>)
- case (SA_Top G' S G)
- then have "\<turnstile> (G @ \<Delta>) ok" by (auto dest: valid_cons')
- moreover have "S closed_in (G @ \<Delta>)" using SA_Top by (auto dest: closed_in_cons)
+proof (induct "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>)
+ case (SA_Top S)
+ then have "\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
+ moreover have "S closed_in (\<Gamma> @ \<Delta>)" 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 "\<turnstile> (G' @ VarB x Q # \<Delta>) ok" by simp
- then have h1:"\<turnstile> (G' @ \<Delta>) ok" by (auto dest: valid_cons')
- have "X' \<in> ty_dom (G' @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
- then have h2:"X' \<in> ty_dom (G' @ \<Delta>)" using ty_dom_vrs by auto
+ case (SA_refl_TVar X)
+ from `\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok`
+ have h1:"\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
+ have "X \<in> ty_dom (\<Gamma> @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
+ then have h2:"X \<in> ty_dom (\<Gamma> @ \<Delta>)" 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 # \<Delta> \<Longrightarrow> ((TVarB X T1 # G') @ \<Delta>)\<turnstile>S2<:T2" by fact
- then have h1:"(TVarB X T1 # (G' @ \<Delta>))\<turnstile>S2<:T2" using SA_all by auto
- have ih2:"G = G' @ VarB x Q # \<Delta> \<Longrightarrow> (G' @ \<Delta>)\<turnstile>T1<:S1" by fact
- then have h2:"(G' @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
+ case (SA_all T1 S1 X S2 T2)
+ have h1:"((TVarB X T1 # \<Gamma>) @ \<Delta>)\<turnstile>S2<:T2" by (fastsimp intro: SA_all)
+ have h2:"(\<Gamma> @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
then show ?case using h1 h2 by auto
qed (auto)
@@ -1418,26 +1415,26 @@
assumes H: "\<Delta> @ (TVarB X Q) # \<Gamma> \<turnstile> t : T"
shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Delta> @ (TVarB X P) # \<Gamma> \<turnstile> t : T"
using H
- proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct)
- case (T_Var x T G P D)
+ proof (nominal_induct "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct)
+ case (T_Var x T P D)
then have "VarB x T \<in> set (D @ TVarB X P # \<Gamma>)"
and "\<turnstile> (D @ TVarB X P # \<Gamma>) 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 # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastsimp
moreover have "(D @ [TVarB X Q] @ \<Gamma>) \<turnstile> T2<:T11" using T_TApp by auto
then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using `\<Gamma>\<turnstile>P<:Q`
@@ -1454,8 +1451,8 @@
theorem subst_type: -- {* A.8 *}
assumes H: "(\<Delta> @ (VarB x U) # \<Gamma>) \<turnstile> t : T"
shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<mapsto> u] : T" using H
- proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
- case (T_Var y T G x u D)
+ proof (nominal_induct "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> 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 @ \<Gamma> \<turnstile> t[x \<mapsto> u] : S" by auto
moreover have "(D @ \<Gamma>) \<turnstile> 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 \<turnstile> t2 : T2` have "X \<sharp> T1"
+ case (T_TAbs X T1 t2 T2 x u D)
+ from `TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2` have "X \<sharp> T1"
by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
with `X \<sharp> 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@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" 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: "(\<Delta> @ ((TVarB X Q) # \<Gamma>)) \<turnstile> S <: T"
shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>"
using H
-proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
- case (SA_Top G S X P D)
+proof (nominal_induct "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
+ case (SA_Top S X P D)
then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
moreover have closed: "P closed_in \<Gamma>" using SA_Top subtype_implies_closed by auto
ultimately have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule valid_subst)
@@ -1505,17 +1502,18 @@
then have "S[X \<mapsto> P]\<^sub>\<tau> closed_in (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" 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\<turnstile>S<:T" by fact
+ case (SA_trans_TVar Y S T X P D)
+ have h:"(D @ TVarB X Q # \<Gamma>)\<turnstile>S<:T" by fact
then have ST: "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" using SA_trans_TVar by auto
- from `G\<turnstile>S<:T` have G_ok: "\<turnstile> G ok" by (rule subtype_implies_ok)
+ from h have G_ok: "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by (rule subtype_implies_ok)
from G_ok and SA_trans_TVar have X\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok"
by (auto intro: validE_append)
show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>"
proof (cases "X = Y")
assume eq: "X = Y"
- from eq and SA_trans_TVar have "TVarB Y Q \<in> set G" by simp
- with G_ok have QS: "Q = S" using `TVarB Y S \<in> set G` by (rule uniqueness_of_ctxt)
+ from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp
+ with G_ok have QS: "Q = S" using `TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)`
+ by (rule uniqueness_of_ctxt)
from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
note `\<Gamma>\<turnstile>P<:Q`
@@ -1552,8 +1550,8 @@
qed
qed
next
- case (SA_refl_TVar G Y X P D)
- then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
+ case (SA_refl_TVar Y X P D)
+ note `\<turnstile> (D @ TVarB X Q # \<Gamma>) ok`
moreover from SA_refl_TVar have closed: "P closed_in \<Gamma>"
by (auto dest: subtype_implies_closed)
ultimately have ok: "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) 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 \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>T1[X \<mapsto> P]\<^sub>\<tau><:S1[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
from SA_arrow have h2:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S2[X \<mapsto> P]\<^sub>\<tau><:T2[X \<mapsto> P]\<^sub>\<tau>" 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 \<sharp> ty_dom (D @ TVarB X Q # \<Gamma>)"
by (auto dest: subtype_implies_ok intro: fresh_dom)
moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \<Gamma>)"
@@ -1594,13 +1592,13 @@
assumes H: "(D @ TVarB X Q # G) \<turnstile> t : T"
shows "G \<turnstile> P <: Q \<Longrightarrow>
(D[X \<mapsto> P]\<^sub>e @ G) \<turnstile> t[X \<mapsto>\<^sub>\<tau> P] : T[X \<mapsto> P]\<^sub>\<tau>" using H
-proof (nominal_induct \<Gamma>'\<equiv>"(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\<turnstile>P<:Q" by fact
then have "P closed_in G" using subtype_implies_closed by auto
- moreover have "\<turnstile> (D' @ TVarB X Q # G) ok" using T_Var by auto
+ moreover note `\<turnstile> (D' @ TVarB X Q # G) ok`
ultimately have "\<turnstile> (D'[X \<mapsto> P]\<^sub>e @ G) ok" using valid_subst by auto
- moreover have "VarB x T \<in> set (D' @ TVarB X Q # G)" using T_Var by auto
+ moreover note `VarB x T \<in> set (D' @ TVarB X Q # G)`
then have "VarB x T \<in> set D' \<or> VarB x T \<in> set G" by simp
then have "(VarB x (T[X \<mapsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<mapsto> 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 \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (T1 \<rightarrow> T2)[X \<mapsto> P]\<^sub>\<tau>" by auto
moreover from T_App have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t2[X \<mapsto>\<^sub>\<tau> P] : T1[X \<mapsto> P]\<^sub>\<tau>" 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' \<sharp> 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' \<sharp> G'" by (rule closed_in_fresh)
+ then have "X' \<sharp> 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' \<sharp> 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: "[] \<turnstile> v : T\<^isub>1 \<rightarrow> T\<^isub>2"
shows "val v \<Longrightarrow> \<exists>x t S. v = (\<lambda>x:S. t)" using ty
-proof (induct \<Gamma>\<equiv>"[]::env" v T\<equiv>"T\<^isub>1 \<rightarrow> T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2)
- case (T_Sub \<Gamma> t S T)
- hence "\<Gamma> \<turnstile> S <: T\<^isub>1 \<rightarrow> T\<^isub>2" by simp
- then obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \<rightarrow> S\<^isub>2"
+proof (induct "[]::env" v "T\<^isub>1 \<rightarrow> T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2)
+ case (T_Sub t S)
+ from `[] \<turnstile> S <: T\<^isub>1 \<rightarrow> T\<^isub>2`
+ obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \<rightarrow> S\<^isub>2"
by cases (auto simp add: T_Sub)
- with `val t` and `\<Gamma> = []` 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: "[] \<turnstile> v : (\<forall>X<:T\<^isub>1. T\<^isub>2)"
shows "val v \<Longrightarrow> \<exists>X t S. v = (\<lambda>X<:S. t)" using ty
-proof (induct \<Gamma>\<equiv>"[]::env" v T\<equiv>"\<forall>X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2)
- case (T_Sub \<Gamma> t S T)
- hence "\<Gamma> \<turnstile> S <: (\<forall>X<:T\<^isub>1. T\<^isub>2)" by simp
- then obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\<forall>X<:S\<^isub>1. S\<^isub>2)"
+proof (induct "[]::env" v "\<forall>X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2)
+ case (T_Sub t S)
+ from `[] \<turnstile> S <: (\<forall>X<:T\<^isub>1. T\<^isub>2)`
+ obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\<forall>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 "[] \<turnstile> t : T"
shows "val t \<or> (\<exists>t'. t \<longmapsto> t')"
using assms
-proof (induct \<Gamma> \<equiv> "[]::env" t T)
- case (T_App \<Gamma> 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 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
thus ?case
proof
@@ -1875,7 +1873,7 @@
thus ?case by auto
qed
next
- case (T_TApp X \<Gamma> 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 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
thus ?case
proof
--- 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: "\<Gamma> \<turnstile> u : U"
shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b
proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
- case (Var \<Gamma>' y T x u \<Delta>)
- then have a1: "valid (\<Delta> @ [(x, U)] @ \<Gamma>)"
- and a2: "(y, T) \<in> set (\<Delta> @ [(x, U)] @ \<Gamma>)"
- and a3: "\<Gamma> \<turnstile> u : U" by simp_all
- from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
+ case (Var y T x u \<Delta>)
+ from `valid (\<Delta> @ [(x, U)] @ \<Gamma>)`
+ have valid: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T"
proof cases
assume eq: "x = y"
- from a1 a2 have "T = U" using eq by (auto intro: context_unique)
- with a3 show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>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 "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" by (auto intro: weakening)
next
assume ineq: "x \<noteq> y"
- from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
- then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq a4 by auto
+ from Var ineq have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" by simp
+ then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq valid by auto
qed
next
- case (Tuple \<Gamma>' t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2)
- from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+ case (Tuple t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2)
+ from refl `\<Gamma> \<turnstile> u : U`
have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T\<^isub>1" by (rule Tuple)
- moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+ moreover from refl `\<Gamma> \<turnstile> u : U`
have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T\<^isub>2" by (rule Tuple)
ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^isub>1[x\<mapsto>u], t\<^isub>2[x\<mapsto>u]\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2" ..
then show ?case by simp
next
- case (Let p t \<Gamma>' T \<Delta>' s S)
- from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+ case (Let p t T \<Delta>' s S)
+ from refl `\<Gamma> \<turnstile> u : U`
have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let)
moreover note `\<turnstile> p : T \<Rightarrow> \<Delta>'`
- moreover from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
- have "\<Delta>' @ \<Gamma>' = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
- with `\<Gamma> \<turnstile> u : U` have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by (rule Let)
+ moreover have "\<Delta>' @ (\<Delta> @ [(x, U)] @ \<Gamma>) = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
+ then have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Let)
then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp
ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>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 \<Gamma>' t S)
- from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` have "(y, T) # \<Gamma>' = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
+ case (Abs y T t S)
+ have "(y, T) # \<Delta> @ [(x, U)] @ \<Gamma> = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
by simp
- with `\<Gamma> \<turnstile> u : U` have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by (rule Abs)
+ then have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Abs)
then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp
then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> 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 \<Gamma>' t\<^isub>1 T S t\<^isub>2)
- from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+ case (App t\<^isub>1 T S t\<^isub>2)
+ from refl `\<Gamma> \<turnstile> u : U`
have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App)
- moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+ moreover from refl `\<Gamma> \<turnstile> u : U`
have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T" by (rule App)
ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^isub>1[x\<mapsto>u]) \<cdot> (t\<^isub>2[x\<mapsto>u]) : S"
by (rule typing.App)
--- 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 "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T"
using a b
proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: e' \<Delta> rule: typing.strong_induct)
- case (t_Var \<Gamma>' y T e' \<Delta>)
+ case (t_Var y T e' \<Delta>)
then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)"
and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)"
- and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
+ and a3: "\<Gamma> \<turnstile> e' : T'" .
from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
{ assume eq: "x=y"
from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
--- 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.$$$ "\<equiv>" || 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;
--- 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
--- 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: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
- and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
+lemma ind_euclid:
+ assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
+ and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
shows "P a b"
-proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
- fix n a b
- assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
+proof(induct "a + b" arbitrary: a b rule: less_induct)
+ case less
have "a = b \<or> a < b \<or> 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 \<or> a = 0" using H(2) by arith
+ hence "a + b - a < a + b \<or> 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 \<or> b = 0" using H(2) by arith
+ hence "b + a - b < a + b \<or> 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
--- 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
--- 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
--- 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,
--- 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
--- 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, _) =
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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;
--- 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\<equiv>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\<equiv>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)"
--- 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 = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"
-proof (induct nd \<equiv> "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) \<Longrightarrow>
- m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
- by blast
obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10"
and cdef: "c = m mod 10" by simp
show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"
proof -
from `Suc nd = nlen m`
have "nd = nlen (m div 10)" by (rule nlen_suc)
- with IH have
+ with Suc have
"m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp
with mexp have
"m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
--- a/src/HOLCF/Universal.thy Sat Jan 16 17:15:28 2010 +0100
+++ b/src/HOLCF/Universal.thy Thu Jan 21 09:27:57 2010 +0100
@@ -694,13 +694,8 @@
lemma basis_emb_mono:
"x \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
-proof (induct n \<equiv> "max (place x) (place y)" arbitrary: x y rule: less_induct)
- case (less n)
- hence IH:
- "\<And>(a::'a compact_basis) b.
- \<lbrakk>max (place a) (place b) < max (place x) (place y); a \<sqsubseteq> b\<rbrakk>
- \<Longrightarrow> 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 \<sqsubseteq> 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)
--- 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
--- 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 **)
--- 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.$$$ "\<equiv>" || 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 =
--- 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
=======================================