--- a/NEWS Fri Dec 23 20:06:54 2016 +0100
+++ b/NEWS Fri Dec 23 20:10:38 2016 +0100
@@ -16,6 +16,13 @@
*** HOL ***
+* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
+INCOMPATIBILITY.
+
+* Dropped abbreviation transP, antisymP, single_valuedP;
+use constants transp, antisymp, single_valuedp instead.
+INCOMPATIBILITY.
+
* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
--- a/src/HOL/Divides.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Divides.thy Fri Dec 23 20:10:38 2016 +0100
@@ -781,7 +781,38 @@
lemma one_mod_numeral [simp]:
"1 mod numeral n = snd (divmod num.One n)"
by (simp add: snd_divmod)
-
+
+text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
+
+lemma cong_exp_iff_simps:
+ "numeral n mod numeral Num.One = 0
+ \<longleftrightarrow> True"
+ "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
+ \<longleftrightarrow> numeral n mod numeral q = 0"
+ "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
+ \<longleftrightarrow> False"
+ "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
+ \<longleftrightarrow> True"
+ "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> True"
+ "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> False"
+ "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> (numeral n mod numeral q) = 0"
+ "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> False"
+ "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+ "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> False"
+ "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> (numeral m mod numeral q) = 0"
+ "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> False"
+ "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+ \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+ by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
+
end
@@ -797,18 +828,18 @@
@{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
\<close>
-definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
- "divmod_nat_rel m n qr \<longleftrightarrow>
- m = fst qr * n + snd qr \<and>
- (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
-
-text \<open>@{const divmod_nat_rel} is total:\<close>
-
-qualified lemma divmod_nat_rel_ex:
- obtains q r where "divmod_nat_rel m n (q, r)"
+inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
+ where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
+ | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
+
+text \<open>@{const eucl_rel_nat} is total:\<close>
+
+qualified lemma eucl_rel_nat_ex:
+ obtains q r where "eucl_rel_nat m n (q, r)"
proof (cases "n = 0")
- case True with that show thesis
- by (auto simp add: divmod_nat_rel_def)
+ case True
+ with that eucl_rel_nat_by0 show thesis
+ by blast
next
case False
have "\<exists>q r. m = q * n + r \<and> r < n"
@@ -833,74 +864,92 @@
with \<open>n \<noteq> 0\<close> show ?thesis by blast
qed
qed
- with that show thesis
- using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
+ with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
+ by blast
qed
-text \<open>@{const divmod_nat_rel} is injective:\<close>
-
-qualified lemma divmod_nat_rel_unique:
- assumes "divmod_nat_rel m n qr"
- and "divmod_nat_rel m n qr'"
- shows "qr = qr'"
+text \<open>@{const eucl_rel_nat} is injective:\<close>
+
+qualified lemma eucl_rel_nat_unique_div:
+ assumes "eucl_rel_nat m n (q, r)"
+ and "eucl_rel_nat m n (q', r')"
+ shows "q = q'"
proof (cases "n = 0")
case True with assms show ?thesis
- by (cases qr, cases qr')
- (simp add: divmod_nat_rel_def)
+ by (auto elim: eucl_rel_nat.cases)
next
case False
- have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
- apply (rule leI)
- apply (subst less_iff_Suc_add)
- apply (auto simp add: add_mult_distrib)
- done
- from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
- by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
- with assms have "snd qr = snd qr'"
- by (simp add: divmod_nat_rel_def)
- with * show ?thesis by (cases qr, cases qr') simp
+ have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
+ proof (rule ccontr)
+ assume "\<not> q' \<le> q"
+ then have "q < q'"
+ by (simp add: not_le)
+ with that show False
+ by (auto simp add: less_iff_Suc_add algebra_simps)
+ qed
+ from \<open>n \<noteq> 0\<close> assms show ?thesis
+ by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
+qed
+
+qualified lemma eucl_rel_nat_unique_mod:
+ assumes "eucl_rel_nat m n (q, r)"
+ and "eucl_rel_nat m n (q', r')"
+ shows "r = r'"
+proof -
+ from assms have "q' = q"
+ by (auto intro: eucl_rel_nat_unique_div)
+ with assms show ?thesis
+ by (auto elim!: eucl_rel_nat.cases)
qed
text \<open>
We instantiate divisibility on the natural numbers by
- means of @{const divmod_nat_rel}:
+ means of @{const eucl_rel_nat}:
\<close>
qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
-
-qualified lemma divmod_nat_rel_divmod_nat:
- "divmod_nat_rel m n (divmod_nat m n)"
+ "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
+
+qualified lemma eucl_rel_nat_divmod_nat:
+ "eucl_rel_nat m n (divmod_nat m n)"
proof -
- from divmod_nat_rel_ex
- obtain qr where rel: "divmod_nat_rel m n qr" .
+ from eucl_rel_nat_ex
+ obtain q r where rel: "eucl_rel_nat m n (q, r)" .
then show ?thesis
- by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
+ by (auto simp add: divmod_nat_def intro: theI
+ elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
qed
qualified lemma divmod_nat_unique:
- assumes "divmod_nat_rel m n qr"
- shows "divmod_nat m n = qr"
- using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
-
-qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
- by (simp add: divmod_nat_unique divmod_nat_rel_def)
-
-qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
- by (simp add: divmod_nat_unique divmod_nat_rel_def)
-
-qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
- by (simp add: divmod_nat_unique divmod_nat_rel_def)
+ "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
+ using that
+ by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
+
+qualified lemma divmod_nat_zero:
+ "divmod_nat m 0 = (0, m)"
+ by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
+
+qualified lemma divmod_nat_zero_left:
+ "divmod_nat 0 n = (0, 0)"
+ by (rule divmod_nat_unique)
+ (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
+
+qualified lemma divmod_nat_base:
+ "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
+ by (rule divmod_nat_unique)
+ (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
qualified lemma divmod_nat_step:
assumes "0 < n" and "n \<le> m"
- shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
+ shows "divmod_nat m n =
+ (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
proof (rule divmod_nat_unique)
- have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
- by (fact divmod_nat_rel_divmod_nat)
- then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
- unfolding divmod_nat_rel_def using assms
- by (auto split: if_splits simp add: algebra_simps)
+ have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
+ by (fact eucl_rel_nat_divmod_nat)
+ then show "eucl_rel_nat m n (Suc
+ (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
+ using assms
+ by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
qed
end
@@ -938,19 +987,19 @@
by (simp add: prod_eq_iff)
lemma div_nat_unique:
- assumes "divmod_nat_rel m n (q, r)"
+ assumes "eucl_rel_nat m n (q, r)"
shows "m div n = q"
using assms
by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
lemma mod_nat_unique:
- assumes "divmod_nat_rel m n (q, r)"
+ assumes "eucl_rel_nat m n (q, r)"
shows "m mod n = r"
using assms
by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
-lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
- using Divides.divmod_nat_rel_divmod_nat
+lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
+ using Divides.eucl_rel_nat_divmod_nat
by (simp add: divmod_nat_div_mod)
text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
@@ -983,22 +1032,21 @@
fixes m n :: nat
assumes "n > 0"
shows "m mod n < n"
- using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
- by (auto split: if_splits)
+ using assms eucl_rel_nat [of m n]
+ by (auto elim: eucl_rel_nat.cases)
lemma mod_le_divisor [simp]:
fixes m n :: nat
assumes "n > 0"
shows "m mod n \<le> n"
-proof (rule less_imp_le)
- from assms show "m mod n < n"
- by simp
-qed
+ using assms eucl_rel_nat [of m n]
+ by (auto elim: eucl_rel_nat.cases)
instance proof
fix m n :: nat
show "m div n * n + m mod n = m"
- using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
+ using eucl_rel_nat [of m n]
+ by (auto elim: eucl_rel_nat.cases)
next
fix n :: nat show "n div 0 = 0"
by (simp add: div_nat_def Divides.divmod_nat_zero)
@@ -1006,7 +1054,7 @@
fix m n :: nat
assume "n \<noteq> 0"
then show "m * n div n = m"
- by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
+ by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
qed (simp_all add: unit_factor_nat_def)
end
@@ -1020,11 +1068,20 @@
next
fix m n q :: nat
assume "m \<noteq> 0"
- then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
- using div_mult_mod_eq [of n q]
- by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
- then show "(m * n) div (m * q) = n div q"
- by (rule div_nat_unique)
+ show "(m * n) div (m * q) = n div q"
+ proof (cases "q = 0")
+ case True
+ then show ?thesis
+ by simp
+ next
+ case False
+ show ?thesis
+ proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
+ show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
+ by (rule eucl_rel_natI)
+ (use \<open>m \<noteq> 0\<close> \<open>q \<noteq> 0\<close> div_mult_mod_eq [of n q] in \<open>auto simp add: algebra_simps distrib_left [symmetric]\<close>)
+ qed
+ qed
qed
lemma div_by_Suc_0 [simp]:
@@ -1156,31 +1213,33 @@
subsubsection \<open>Quotient and Remainder\<close>
-lemma divmod_nat_rel_mult1_eq:
- "divmod_nat_rel b c (q, r)
- \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
-by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
-
lemma div_mult1_eq:
"(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
-by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
-
-lemma divmod_nat_rel_add1_eq:
- "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
- \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
-by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
+ by (cases "c = 0")
+ (auto simp add: algebra_simps distrib_left [symmetric]
+ intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
+
+lemma eucl_rel_nat_add1_eq:
+ "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
+ \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
+ by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma div_add1_eq:
- "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
-by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
-
-lemma divmod_nat_rel_mult2_eq:
- assumes "divmod_nat_rel a b (q, r)"
- shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
-proof -
- { assume "r < b" and "0 < c"
- then have "b * (q mod c) + r < b * c"
+ "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
+by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
+
+lemma eucl_rel_nat_mult2_eq:
+ assumes "eucl_rel_nat a b (q, r)"
+ shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
+proof (cases "c = 0")
+ case True
+ with assms show ?thesis
+ by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
+next
+ case False
+ { assume "r < b"
+ with False have "b * (q mod c) + r < b * c"
apply (cut_tac m = q and n = c in mod_less_divisor)
apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
@@ -1188,15 +1247,15 @@
done
then have "r + b * (q mod c) < b * c"
by (simp add: ac_simps)
- } with assms show ?thesis
- by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
+ } with assms False show ?thesis
+ by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
qed
lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
-by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
+by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
-by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
+by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
instantiation nat :: semiring_numeral_div
begin
@@ -1355,8 +1414,8 @@
from A B show ?lhs ..
next
assume P: ?lhs
- then have "divmod_nat_rel m n (q, m - n * q)"
- unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
+ then have "eucl_rel_nat m n (q, m - n * q)"
+ by (auto intro: eucl_rel_natI simp add: ac_simps)
then have "m div n = q"
by (rule div_nat_unique)
then show ?rhs by simp
@@ -1636,46 +1695,25 @@
shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
by (simp_all add: snd_divmod)
-lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
- fixes m n q :: num
- shows
- "numeral n mod numeral Num.One = (0::nat)
- \<longleftrightarrow> True"
- "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
- \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
- "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
- \<longleftrightarrow> False"
- "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
- \<longleftrightarrow> True"
- "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> True"
- "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> False"
- "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
- "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> False"
- "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
- "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> False"
- "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
- "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> False"
- "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
- \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
- by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
-
subsection \<open>Division on @{typ int}\<close>
context
begin
-definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
- where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
- (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
+inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
+ where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
+ | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
+ | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
+ \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
+
+lemma eucl_rel_int_iff:
+ "eucl_rel_int k l (q, r) \<longleftrightarrow>
+ k = l * q + r \<and>
+ (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
+ by (cases "r = 0")
+ (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
+ simp add: ac_simps sgn_1_pos sgn_1_neg)
lemma unique_quotient_lemma:
"b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
@@ -1694,17 +1732,17 @@
by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
lemma unique_quotient:
- "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
-apply (simp add: divmod_int_rel_def linorder_neq_iff split: if_split_asm)
-apply (blast intro: order_antisym
- dest: order_eq_refl [THEN unique_quotient_lemma]
- order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
-done
+ "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
+ apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
+ apply (blast intro: order_antisym
+ dest: order_eq_refl [THEN unique_quotient_lemma]
+ order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
+ done
lemma unique_remainder:
- "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> r = r'"
+ "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
apply (subgoal_tac "q = q'")
- apply (simp add: divmod_int_rel_def)
+ apply (simp add: eucl_rel_int_iff)
apply (blast intro: unique_quotient)
done
@@ -1733,12 +1771,12 @@
then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
-lemma divmod_int_rel:
- "divmod_int_rel k l (k div l, k mod l)"
+lemma eucl_rel_int:
+ "eucl_rel_int k l (k div l, k mod l)"
proof (cases k rule: int_cases3)
case zero
then show ?thesis
- by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
+ by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
next
case (pos n)
then show ?thesis
@@ -1746,7 +1784,7 @@
by (cases l rule: int_cases3)
(auto simp del: of_nat_mult of_nat_add
simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
- divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+ eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
next
case (neg n)
then show ?thesis
@@ -1754,29 +1792,29 @@
by (cases l rule: int_cases3)
(auto simp del: of_nat_mult of_nat_add
simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
- divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+ eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
qed
lemma divmod_int_unique:
- assumes "divmod_int_rel k l (q, r)"
+ assumes "eucl_rel_int k l (q, r)"
shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
- using assms divmod_int_rel [of k l]
+ using assms eucl_rel_int [of k l]
using unique_quotient [of k l] unique_remainder [of k l]
by auto
instance proof
fix k l :: int
show "k div l * l + k mod l = k"
- using divmod_int_rel [of k l]
- unfolding divmod_int_rel_def by (simp add: ac_simps)
+ using eucl_rel_int [of k l]
+ unfolding eucl_rel_int_iff by (simp add: ac_simps)
next
fix k :: int show "k div 0 = 0"
- by (rule div_int_unique, simp add: divmod_int_rel_def)
+ by (rule div_int_unique, simp add: eucl_rel_int_iff)
next
fix k l :: int
assume "l \<noteq> 0"
then show "k * l div l = k"
- by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
+ by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
end
@@ -1789,23 +1827,23 @@
proof
fix k l s :: int
assume "l \<noteq> 0"
- then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
- using divmod_int_rel [of k l]
- unfolding divmod_int_rel_def by (auto simp: algebra_simps)
+ then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
+ using eucl_rel_int [of k l]
+ unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
then show "(k + s * l) div l = s + k div l"
by (rule div_int_unique)
next
fix k l s :: int
assume "s \<noteq> 0"
- have "\<And>q r. divmod_int_rel k l (q, r)
- \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
- unfolding divmod_int_rel_def
+ have "\<And>q r. eucl_rel_int k l (q, r)
+ \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
+ unfolding eucl_rel_int_iff
by (rule linorder_cases [of 0 l])
(use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
- then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
- using divmod_int_rel [of k l] .
+ then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
+ using eucl_rel_int [of k l] .
then show "(s * k) div (s * l) = k div l"
by (rule div_int_unique)
qed
@@ -1839,15 +1877,15 @@
by (simp add: modulo_int_def int_dvd_iff)
lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
- using divmod_int_rel [of a b]
- by (auto simp add: divmod_int_rel_def prod_eq_iff)
+ using eucl_rel_int [of a b]
+ by (auto simp add: eucl_rel_int_iff prod_eq_iff)
lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
- using divmod_int_rel [of a b]
- by (auto simp add: divmod_int_rel_def prod_eq_iff)
+ using eucl_rel_int [of a b]
+ by (auto simp add: eucl_rel_int_iff prod_eq_iff)
lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
@@ -1857,34 +1895,34 @@
lemma div_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a div b = 0"
apply (rule div_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
done
lemma div_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a div b = 0"
apply (rule div_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
done
lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1"
apply (rule div_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
done
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)
lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a"
apply (rule_tac q = 0 in mod_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
done
lemma mod_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a mod b = a"
apply (rule_tac q = 0 in mod_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
done
lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b"
apply (rule_tac q = "-1" in mod_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
done
text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
@@ -1893,22 +1931,22 @@
subsubsection \<open>Laws for div and mod with Unary Minus\<close>
lemma zminus1_lemma:
- "divmod_int_rel a b (q, r) ==> b \<noteq> 0
- ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
+ "eucl_rel_int a b (q, r) ==> b \<noteq> 0
+ ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
if r=0 then 0 else b-r)"
-by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
+by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff right_diff_distrib)
lemma zdiv_zminus1_eq_if:
"b \<noteq> (0::int)
==> (-a) div b =
(if a mod b = 0 then - (a div b) else - (a div b) - 1)"
-by (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN div_int_unique])
+by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
lemma zmod_zminus1_eq_if:
"(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"
apply (case_tac "b = 0", simp)
-apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
+apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
done
lemma zmod_zminus1_not_zero:
@@ -2022,27 +2060,27 @@
text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
lemma zmult1_lemma:
- "[| divmod_int_rel b c (q, r) |]
- ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
-by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
+ "[| eucl_rel_int b c (q, r) |]
+ ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
+by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
apply (case_tac "c = 0", simp)
-apply (blast intro: divmod_int_rel [THEN zmult1_lemma, THEN div_int_unique])
+apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
done
text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
lemma zadd1_lemma:
- "[| divmod_int_rel a c (aq, ar); divmod_int_rel b c (bq, br) |]
- ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
-by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
+ "[| eucl_rel_int a c (aq, ar); eucl_rel_int b c (bq, br) |]
+ ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
+by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma zdiv_zadd1_eq:
"(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF divmod_int_rel divmod_int_rel] div_int_unique)
+apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
done
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
@@ -2095,9 +2133,9 @@
apply simp
done
-lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
- ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
-by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
+lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
+ ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
+by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
zero_less_mult_iff distrib_left [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
@@ -2105,14 +2143,14 @@
fixes a b c :: int
shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
apply (case_tac "b = 0", simp)
-apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN div_int_unique])
+apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
done
lemma zmod_zmult2_eq:
fixes a b c :: int
shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
apply (case_tac "b = 0", simp)
-apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN mod_int_unique])
+apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
done
lemma div_pos_geq:
@@ -2199,27 +2237,27 @@
subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
-lemma pos_divmod_int_rel_mult_2:
+lemma pos_eucl_rel_int_mult_2:
assumes "0 \<le> b"
- assumes "divmod_int_rel a b (q, r)"
- shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
- using assms unfolding divmod_int_rel_def by auto
-
-lemma neg_divmod_int_rel_mult_2:
+ assumes "eucl_rel_int a b (q, r)"
+ shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
+ using assms unfolding eucl_rel_int_iff by auto
+
+lemma neg_eucl_rel_int_mult_2:
assumes "b \<le> 0"
- assumes "divmod_int_rel (a + 1) b (q, r)"
- shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
- using assms unfolding divmod_int_rel_def by auto
+ assumes "eucl_rel_int (a + 1) b (q, r)"
+ shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
+ using assms unfolding eucl_rel_int_iff by auto
text\<open>computing div by shifting\<close>
lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
- using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel]
+ using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
by (rule div_int_unique)
lemma neg_zdiv_mult_2:
assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
- using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel]
+ using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
by (rule div_int_unique)
(* FIXME: add rules for negative numerals *)
@@ -2240,14 +2278,14 @@
fixes a b :: int
assumes "0 \<le> a"
shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
- using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
+ using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
by (rule mod_int_unique)
lemma neg_zmod_mult_2:
fixes a b :: int
assumes "a \<le> 0"
shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
- using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
+ using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
by (rule mod_int_unique)
(* FIXME: add rules for negative numerals *)
@@ -2452,19 +2490,19 @@
text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
- by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
+ by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
by (rule div_int_unique [of a b q r],
- simp add: divmod_int_rel_def)
+ simp add: eucl_rel_int_iff)
lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
by (rule mod_int_unique [of a b q r],
- simp add: divmod_int_rel_def)
+ simp add: eucl_rel_int_iff)
lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
by (rule mod_int_unique [of a b q r],
- simp add: divmod_int_rel_def)
+ simp add: eucl_rel_int_iff)
lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
--- a/src/HOL/Library/Polynomial.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy Fri Dec 23 20:10:38 2016 +0100
@@ -1613,18 +1613,26 @@
subsection \<open>Long division of polynomials\<close>
-definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
-where
- "pdivmod_rel x y q r \<longleftrightarrow>
- x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
-
-lemma pdivmod_rel_0:
- "pdivmod_rel 0 y 0 0"
- unfolding pdivmod_rel_def by simp
-
-lemma pdivmod_rel_by_0:
- "pdivmod_rel x 0 0 x"
- unfolding pdivmod_rel_def by simp
+inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
+ where eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
+ | eucl_rel_poly_dividesI: "y \<noteq> 0 \<Longrightarrow> x = q * y \<Longrightarrow> eucl_rel_poly x y (q, 0)"
+ | eucl_rel_poly_remainderI: "y \<noteq> 0 \<Longrightarrow> degree r < degree y
+ \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
+
+lemma eucl_rel_poly_iff:
+ "eucl_rel_poly x y (q, r) \<longleftrightarrow>
+ x = q * y + r \<and>
+ (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
+ by (auto elim: eucl_rel_poly.cases
+ intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
+
+lemma eucl_rel_poly_0:
+ "eucl_rel_poly 0 y (0, 0)"
+ unfolding eucl_rel_poly_iff by simp
+
+lemma eucl_rel_poly_by_0:
+ "eucl_rel_poly x 0 (0, x)"
+ unfolding eucl_rel_poly_iff by simp
lemma eq_zero_or_degree_less:
assumes "degree p \<le> n" and "coeff p n = 0"
@@ -1650,15 +1658,15 @@
then show ?thesis ..
qed
-lemma pdivmod_rel_pCons:
- assumes rel: "pdivmod_rel x y q r"
+lemma eucl_rel_poly_pCons:
+ assumes rel: "eucl_rel_poly x y (q, r)"
assumes y: "y \<noteq> 0"
assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
- shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
- (is "pdivmod_rel ?x y ?q ?r")
+ shows "eucl_rel_poly (pCons a x) y (pCons b q, pCons a r - smult b y)"
+ (is "eucl_rel_poly ?x y (?q, ?r)")
proof -
have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
- using assms unfolding pdivmod_rel_def by simp_all
+ using assms unfolding eucl_rel_poly_iff by simp_all
have 1: "?x = ?q * y + ?r"
using b x by simp
@@ -1678,31 +1686,31 @@
qed
from 1 2 show ?thesis
- unfolding pdivmod_rel_def
+ unfolding eucl_rel_poly_iff
using \<open>y \<noteq> 0\<close> by simp
qed
-lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
+lemma eucl_rel_poly_exists: "\<exists>q r. eucl_rel_poly x y (q, r)"
apply (cases "y = 0")
-apply (fast intro!: pdivmod_rel_by_0)
+apply (fast intro!: eucl_rel_poly_by_0)
apply (induct x)
-apply (fast intro!: pdivmod_rel_0)
-apply (fast intro!: pdivmod_rel_pCons)
+apply (fast intro!: eucl_rel_poly_0)
+apply (fast intro!: eucl_rel_poly_pCons)
done
-lemma pdivmod_rel_unique:
- assumes 1: "pdivmod_rel x y q1 r1"
- assumes 2: "pdivmod_rel x y q2 r2"
+lemma eucl_rel_poly_unique:
+ assumes 1: "eucl_rel_poly x y (q1, r1)"
+ assumes 2: "eucl_rel_poly x y (q2, r2)"
shows "q1 = q2 \<and> r1 = r2"
proof (cases "y = 0")
assume "y = 0" with assms show ?thesis
- by (simp add: pdivmod_rel_def)
+ by (simp add: eucl_rel_poly_iff)
next
assume [simp]: "y \<noteq> 0"
from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
- unfolding pdivmod_rel_def by simp_all
+ unfolding eucl_rel_poly_iff by simp_all
from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
- unfolding pdivmod_rel_def by simp_all
+ unfolding eucl_rel_poly_iff by simp_all
from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
by (simp add: algebra_simps)
from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
@@ -1723,15 +1731,15 @@
qed
qed
-lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
-by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
-
-lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
-by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
-
-lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
-
-lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
+lemma eucl_rel_poly_0_iff: "eucl_rel_poly 0 y (q, r) \<longleftrightarrow> q = 0 \<and> r = 0"
+by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
+
+lemma eucl_rel_poly_by_0_iff: "eucl_rel_poly x 0 (q, r) \<longleftrightarrow> q = 0 \<and> r = x"
+by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
+
+lemmas eucl_rel_poly_unique_div = eucl_rel_poly_unique [THEN conjunct1]
+
+lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2]
@@ -2236,8 +2244,8 @@
if g = 0 then f
else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g"
-lemma pdivmod_rel: "pdivmod_rel (x::'a::field poly) y (x div y) (x mod y)"
- unfolding pdivmod_rel_def
+lemma eucl_rel_poly: "eucl_rel_poly (x::'a::field poly) y (x div y, x mod y)"
+ unfolding eucl_rel_poly_iff
proof (intro conjI)
show "x = x div y * y + x mod y"
proof(cases "y = 0")
@@ -2261,24 +2269,24 @@
qed
lemma div_poly_eq:
- "pdivmod_rel (x::'a::field poly) y q r \<Longrightarrow> x div y = q"
- by(rule pdivmod_rel_unique_div[OF pdivmod_rel])
+ "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x div y = q"
+ by(rule eucl_rel_poly_unique_div[OF eucl_rel_poly])
lemma mod_poly_eq:
- "pdivmod_rel (x::'a::field poly) y q r \<Longrightarrow> x mod y = r"
- by (rule pdivmod_rel_unique_mod[OF pdivmod_rel])
+ "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x mod y = r"
+ by (rule eucl_rel_poly_unique_mod[OF eucl_rel_poly])
instance
proof
fix x y :: "'a poly"
- from pdivmod_rel[of x y,unfolded pdivmod_rel_def]
+ from eucl_rel_poly[of x y,unfolded eucl_rel_poly_iff]
show "x div y * y + x mod y = x" by auto
next
fix x y z :: "'a poly"
assume "y \<noteq> 0"
- hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
- using pdivmod_rel [of x y]
- by (simp add: pdivmod_rel_def distrib_right)
+ hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
+ using eucl_rel_poly [of x y]
+ by (simp add: eucl_rel_poly_iff distrib_right)
thus "(x + z * y) div y = z + x div y"
by (rule div_poly_eq)
next
@@ -2286,23 +2294,23 @@
assume "x \<noteq> 0"
show "(x * y) div (x * z) = y div z"
proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
- have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
- by (rule pdivmod_rel_by_0)
+ have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
+ by (rule eucl_rel_poly_by_0)
then have [simp]: "\<And>x::'a poly. x div 0 = 0"
by (rule div_poly_eq)
- have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
- by (rule pdivmod_rel_0)
+ have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
+ by (rule eucl_rel_poly_0)
then have [simp]: "\<And>x::'a poly. 0 div x = 0"
by (rule div_poly_eq)
case False then show ?thesis by auto
next
case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
with \<open>x \<noteq> 0\<close>
- have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
- by (auto simp add: pdivmod_rel_def algebra_simps)
+ have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
+ by (auto simp add: eucl_rel_poly_iff algebra_simps)
(rule classical, simp add: degree_mult_eq)
- moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
- ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
+ moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
+ ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
then show ?thesis by (simp add: div_poly_eq)
qed
qed
@@ -2311,35 +2319,35 @@
lemma degree_mod_less:
"y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
- using pdivmod_rel [of x y]
- unfolding pdivmod_rel_def by simp
+ using eucl_rel_poly [of x y]
+ unfolding eucl_rel_poly_iff by simp
lemma div_poly_less: "degree (x::'a::field poly) < degree y \<Longrightarrow> x div y = 0"
proof -
assume "degree x < degree y"
- hence "pdivmod_rel x y 0 x"
- by (simp add: pdivmod_rel_def)
+ hence "eucl_rel_poly x y (0, x)"
+ by (simp add: eucl_rel_poly_iff)
thus "x div y = 0" by (rule div_poly_eq)
qed
lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
proof -
assume "degree x < degree y"
- hence "pdivmod_rel x y 0 x"
- by (simp add: pdivmod_rel_def)
+ hence "eucl_rel_poly x y (0, x)"
+ by (simp add: eucl_rel_poly_iff)
thus "x mod y = x" by (rule mod_poly_eq)
qed
-lemma pdivmod_rel_smult_left:
- "pdivmod_rel x y q r
- \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
- unfolding pdivmod_rel_def by (simp add: smult_add_right)
+lemma eucl_rel_poly_smult_left:
+ "eucl_rel_poly x y (q, r)
+ \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
+ unfolding eucl_rel_poly_iff by (simp add: smult_add_right)
lemma div_smult_left: "(smult (a::'a::field) x) div y = smult a (x div y)"
- by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+ by (rule div_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
- by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+ by (rule mod_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
lemma poly_div_minus_left [simp]:
fixes x y :: "'a::field poly"
@@ -2351,23 +2359,23 @@
shows "(- x) mod y = - (x mod y)"
using mod_smult_left [of "- 1::'a"] by simp
-lemma pdivmod_rel_add_left:
- assumes "pdivmod_rel x y q r"
- assumes "pdivmod_rel x' y q' r'"
- shows "pdivmod_rel (x + x') y (q + q') (r + r')"
- using assms unfolding pdivmod_rel_def
+lemma eucl_rel_poly_add_left:
+ assumes "eucl_rel_poly x y (q, r)"
+ assumes "eucl_rel_poly x' y (q', r')"
+ shows "eucl_rel_poly (x + x') y (q + q', r + r')"
+ using assms unfolding eucl_rel_poly_iff
by (auto simp add: algebra_simps degree_add_less)
lemma poly_div_add_left:
fixes x y z :: "'a::field poly"
shows "(x + y) div z = x div z + y div z"
- using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
+ using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
by (rule div_poly_eq)
lemma poly_mod_add_left:
fixes x y z :: "'a::field poly"
shows "(x + y) mod z = x mod z + y mod z"
- using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
+ using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
by (rule mod_poly_eq)
lemma poly_div_diff_left:
@@ -2380,17 +2388,17 @@
shows "(x - y) mod z = x mod z - y mod z"
by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
-lemma pdivmod_rel_smult_right:
- "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
- \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
- unfolding pdivmod_rel_def by simp
+lemma eucl_rel_poly_smult_right:
+ "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r)
+ \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
+ unfolding eucl_rel_poly_iff by simp
lemma div_smult_right:
"(a::'a::field) \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
- by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+ by (rule div_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
- by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+ by (rule mod_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
lemma poly_div_minus_right [simp]:
fixes x y :: "'a::field poly"
@@ -2402,30 +2410,30 @@
shows "x mod (- y) = x mod y"
using mod_smult_right [of "- 1::'a"] by simp
-lemma pdivmod_rel_mult:
- "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
- \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
-apply (cases "z = 0", simp add: pdivmod_rel_def)
-apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
+lemma eucl_rel_poly_mult:
+ "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r')
+ \<Longrightarrow> eucl_rel_poly x (y * z) (q', y * r' + r)"
+apply (cases "z = 0", simp add: eucl_rel_poly_iff)
+apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
apply (cases "r = 0")
apply (cases "r' = 0")
-apply (simp add: pdivmod_rel_def)
-apply (simp add: pdivmod_rel_def field_simps degree_mult_eq)
+apply (simp add: eucl_rel_poly_iff)
+apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
apply (cases "r' = 0")
-apply (simp add: pdivmod_rel_def degree_mult_eq)
-apply (simp add: pdivmod_rel_def field_simps)
+apply (simp add: eucl_rel_poly_iff degree_mult_eq)
+apply (simp add: eucl_rel_poly_iff field_simps)
apply (simp add: degree_mult_eq degree_add_less)
done
lemma poly_div_mult_right:
fixes x y z :: "'a::field poly"
shows "x div (y * z) = (x div y) div z"
- by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+ by (rule div_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
lemma poly_mod_mult_right:
fixes x y z :: "'a::field poly"
shows "x mod (y * z) = y * (x div y mod z) + x mod y"
- by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+ by (rule mod_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
lemma mod_pCons:
fixes a and x
@@ -2434,7 +2442,7 @@
shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
unfolding b
apply (rule mod_poly_eq)
-apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
+apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
done
definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
@@ -2453,9 +2461,9 @@
in (pCons b s, pCons a r - smult b q)))"
apply (simp add: pdivmod_def Let_def, safe)
apply (rule div_poly_eq)
- apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
+ apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
apply (rule mod_poly_eq)
- apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
+ apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
done
lemma pdivmod_fold_coeffs:
@@ -2700,8 +2708,8 @@
(* *************** *)
subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close>
-lemma pdivmod_pdivmodrel: "pdivmod_rel p q r s = (pdivmod p q = (r, s))"
- by (metis pdivmod_def pdivmod_rel pdivmod_rel_unique prod.sel)
+lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> pdivmod p q = (r, s)"
+ by (metis pdivmod_def eucl_rel_poly eucl_rel_poly_unique)
lemma pdivmod_via_pseudo_divmod: "pdivmod f g = (if g = 0 then (0,f)
else let
@@ -2720,7 +2728,7 @@
unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto
from pseudo_divmod[OF h0 p, unfolded h1]
have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto
- have "pdivmod_rel f h q r" unfolding pdivmod_rel_def using f r h0 by auto
+ have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto
hence "pdivmod f h = (q,r)" by (simp add: pdivmod_pdivmodrel)
hence "pdivmod f g = (smult lc q, r)"
unfolding pdivmod_def h_def div_smult_right[OF lc] mod_smult_right[OF lc]
--- a/src/HOL/Library/Transitive_Closure_Table.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Dec 23 20:10:38 2016 +0100
@@ -207,10 +207,10 @@
code_pred rtranclp
using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
-lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> RangeP R z"
+lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> Rangep R z"
by(induction rule: rtrancl_path.induct) auto
-lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> RangeP R y"
+lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> Rangep R y"
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
lemma rtrancl_path_nth:
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Fri Dec 23 20:10:38 2016 +0100
@@ -451,7 +451,7 @@
lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
by (intro prime_elem_dvd_multD) simp_all
-lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
+lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
by (auto dest: prime_dvd_multD)
lemma prime_dvd_power:
@@ -1640,7 +1640,6 @@
(insert nz False, auto simp: Gcd_factorial_eq_0_iff)
qed (simp_all add: Gcd_factorial_def)
-
lemma normalize_Lcm_factorial:
"normalize (Lcm_factorial A) = Lcm_factorial A"
proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
--- a/src/HOL/Number_Theory/Gauss.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy Fri Dec 23 20:10:38 2016 +0100
@@ -12,12 +12,12 @@
lemma cong_prime_prod_zero_nat:
fixes a::nat
shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
- by (auto simp add: cong_altdef_nat)
+ by (auto simp add: cong_altdef_nat prime_dvd_mult_iff)
lemma cong_prime_prod_zero_int:
fixes a::int
shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
- by (auto simp add: cong_altdef_int)
+ by (auto simp add: cong_altdef_int prime_dvd_mult_iff)
locale GAUSS =
--- a/src/HOL/Partial_Function.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Partial_Function.thy Fri Dec 23 20:10:38 2016 +0100
@@ -283,8 +283,8 @@
lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
by(auto simp add: flat_ord_def)
-lemma antisymP_flat_ord: "antisymP (flat_ord a)"
-by(rule antisymI)(auto dest: flat_ord_antisym)
+lemma antisymp_flat_ord: "antisymp (flat_ord a)"
+by(rule antisympI)(auto dest: flat_ord_antisym)
interpretation tailrec:
partial_function_definitions "flat_ord undefined" "flat_lub undefined"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Dec 23 20:10:38 2016 +0100
@@ -1573,34 +1573,29 @@
fixes p q :: "'a pmf"
assumes 1: "rel_pmf R p q"
assumes 2: "rel_pmf R q p"
- and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R"
+ and refl: "reflp R" and trans: "transp R" and antisym: "antisymp R"
shows "p = q"
proof -
from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
also have "inf R R\<inverse>\<inverse> = op ="
- using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD)
+ using refl antisym by (auto intro!: ext simp add: reflpD dest: antisympD)
finally show ?thesis unfolding pmf.rel_eq .
qed
lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)"
-by(blast intro: reflpI rel_pmf_reflI reflpD)
+ by (fact pmf.rel_reflp)
-lemma antisymP_rel_pmf:
- "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk>
- \<Longrightarrow> antisymP (rel_pmf R)"
-by(rule antisymI)(blast intro: rel_pmf_antisym)
+lemma antisymp_rel_pmf:
+ "\<lbrakk> reflp R; transp R; antisymp R \<rbrakk>
+ \<Longrightarrow> antisymp (rel_pmf R)"
+by(rule antisympI)(blast intro: rel_pmf_antisym)
lemma transp_rel_pmf:
assumes "transp R"
shows "transp (rel_pmf R)"
-proof (rule transpI)
- fix x y z
- assume "rel_pmf R x y" and "rel_pmf R y z"
- hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI)
- thus "rel_pmf R x z"
- using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq)
-qed
+ using assms by (fact pmf.rel_transp)
+
subsection \<open> Distributions \<close>
context
--- a/src/HOL/Probability/SPMF.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Probability/SPMF.thy Fri Dec 23 20:10:38 2016 +0100
@@ -95,8 +95,8 @@
lemma transp_ord_option: "transp ord \<Longrightarrow> transp (ord_option ord)"
unfolding transp_def by(blast intro: ord_option_trans)
-lemma antisymP_ord_option: "antisymP ord \<Longrightarrow> antisymP (ord_option ord)"
-by(auto intro!: antisymI elim!: ord_option.cases dest: antisymD)
+lemma antisymp_ord_option: "antisymp ord \<Longrightarrow> antisymp (ord_option ord)"
+by(auto intro!: antisympI elim!: ord_option.cases dest: antisympD)
lemma ord_option_chainD:
"Complete_Partial_Order.chain (ord_option ord) Y
@@ -1508,7 +1508,7 @@
fix x y
assume "?R x y" "?R y x"
thus "x = y"
- by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymP_ord_option)
+ by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymp_ord_option)
next
fix Y x
assume "Complete_Partial_Order.chain ?R Y" "x \<in> Y"
--- a/src/HOL/Relation.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Relation.thy Fri Dec 23 20:10:38 2016 +0100
@@ -321,26 +321,51 @@
definition antisym :: "'a rel \<Rightarrow> bool"
where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
-abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
- where "antisymP r \<equiv> antisym {(x, y). r x y}" (* FIXME proper logical operation *)
+definition antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+ where "antisymp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x \<longrightarrow> x = y)"
-lemma antisymI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
+lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym r"
+ by (simp add: antisym_def antisymp_def)
+
+lemma antisymI [intro?]:
+ "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
unfolding antisym_def by iprover
-lemma antisymD [dest?]: "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"
+lemma antisympI [intro?]:
+ "(\<And>x y. r x y \<Longrightarrow> r y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp r"
+ by (fact antisymI [to_pred])
+
+lemma antisymD [dest?]:
+ "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"
unfolding antisym_def by iprover
-lemma antisym_subset: "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r"
- unfolding antisym_def by blast
+lemma antisympD [dest?]:
+ "antisymp r \<Longrightarrow> r a b \<Longrightarrow> r b a \<Longrightarrow> a = b"
+ by (fact antisymD [to_pred])
-lemma antisym_empty [simp]: "antisym {}"
+lemma antisym_subset:
+ "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r"
unfolding antisym_def by blast
-lemma antisymP_equality [simp]: "antisymP op ="
- by (auto intro: antisymI)
+lemma antisymp_less_eq:
+ "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r"
+ by (fact antisym_subset [to_pred])
+
+lemma antisym_empty [simp]:
+ "antisym {}"
+ unfolding antisym_def by blast
-lemma antisym_singleton [simp]: "antisym {x}"
-by (blast intro: antisymI)
+lemma antisym_bot [simp]:
+ "antisymp \<bottom>"
+ by (fact antisym_empty [to_pred])
+
+lemma antisymp_equality [simp]:
+ "antisymp HOL.eq"
+ by (auto intro: antisympI)
+
+lemma antisym_singleton [simp]:
+ "antisym {x}"
+ by (blast intro: antisymI)
subsubsection \<open>Transitivity\<close>
@@ -437,21 +462,45 @@
definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
-abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "single_valuedP r \<equiv> single_valued {(x, y). r x y}" (* FIXME proper logical operation *)
+definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))"
+
+lemma single_valuedp_single_valued_eq [pred_set_conv]:
+ "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
+ by (simp add: single_valued_def single_valuedp_def)
-lemma single_valuedI: "\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z) \<Longrightarrow> single_valued r"
- unfolding single_valued_def .
+lemma single_valuedI:
+ "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r"
+ unfolding single_valued_def by blast
-lemma single_valuedD: "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
+lemma single_valuedpI:
+ "(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r"
+ by (fact single_valuedI [to_pred])
+
+lemma single_valuedD:
+ "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
by (simp add: single_valued_def)
-lemma single_valued_empty[simp]: "single_valued {}"
+lemma single_valuedpD:
+ "single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
+ by (fact single_valuedD [to_pred])
+
+lemma single_valued_empty [simp]:
+ "single_valued {}"
by (simp add: single_valued_def)
-lemma single_valued_subset: "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
+lemma single_valuedp_bot [simp]:
+ "single_valuedp \<bottom>"
+ by (fact single_valued_empty [to_pred])
+
+lemma single_valued_subset:
+ "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
unfolding single_valued_def by blast
+lemma single_valuedp_less_eq:
+ "r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r"
+ by (fact single_valued_subset [to_pred])
+
subsection \<open>Relation operations\<close>
@@ -1149,12 +1198,4 @@
(auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
cong: if_cong)
-text \<open>Misc\<close>
-
-abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
- where "transP r \<equiv> trans {(x, y). r x y}" (* FIXME drop *)
-
-abbreviation (input) "RangeP \<equiv> Rangep"
-abbreviation (input) "DomainP \<equiv> Domainp"
-
end
--- a/src/HOL/Statespace/state_fun.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Statespace/state_fun.ML Fri Dec 23 20:10:38 2016 +0100
@@ -77,7 +77,7 @@
fun string_eq_simp_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt
addsimps @{thms list.inject list.distinct Char_eq_Char_iff
- cut_eq_simps simp_thms}
+ cong_exp_iff_simps simp_thms}
addsimprocs [lazy_conj_simproc]
|> Simplifier.add_cong @{thm block_conj_cong});
--- a/src/HOL/String.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/String.thy Fri Dec 23 20:10:38 2016 +0100
@@ -114,7 +114,7 @@
"nat_of_char (Char k) = numeral k mod 256"
by (simp add: Char_def)
-lemma Char_eq_Char_iff [simp]:
+lemma Char_eq_Char_iff:
"Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
proof -
have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
@@ -124,14 +124,25 @@
finally show ?thesis .
qed
-lemma zero_eq_Char_iff [simp]:
+lemma zero_eq_Char_iff:
"0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
by (auto simp add: zero_char_def Char_def)
-lemma Char_eq_zero_iff [simp]:
+lemma Char_eq_zero_iff:
"Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
by (auto simp add: zero_char_def Char_def)
+simproc_setup char_eq
+ ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \<open>
+ let
+ val ss = put_simpset HOL_ss @{context}
+ |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps}
+ |> simpset_of
+ in
+ fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt)
+ end
+\<close>
+
definition integer_of_char :: "char \<Rightarrow> integer"
where
"integer_of_char = integer_of_nat \<circ> nat_of_char"
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Dec 23 20:10:38 2016 +0100
@@ -122,9 +122,9 @@
val mk_pred: typ list -> term -> term
val mk_rel: int -> typ list -> typ list -> term -> term
val mk_set: typ list -> term -> term
- val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
- val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) ->
- typ * typ -> term
+ val build_map: Proof.context -> typ list -> typ list -> (typ * typ -> term) -> typ * typ -> term
+ val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> typ list ->
+ (typ * typ -> term) -> typ * typ -> term
val build_set: Proof.context -> typ -> typ -> term
val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
@@ -744,12 +744,13 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
-fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts build_simple =
+fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts simple_Us build_simple =
let
fun build (TU as (T, U)) =
- if exists (curry (op =) T) simple_Ts then
+ if exists (curry (op =) T) simple_Ts orelse exists (curry (op =) U) simple_Us then
build_simple TU
- else if T = U andalso not (exists_subtype_in simple_Ts T) then
+ else if T = U andalso not (exists_subtype_in simple_Ts T) andalso
+ not (exists_subtype_in simple_Us U) then
const T
else
(case TU of
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Dec 23 20:10:38 2016 +0100
@@ -163,11 +163,14 @@
* (((term list list * term list list * term list list list list * term list list list list)
* term list list list) * typ list) -> (string -> binding) -> 'b list -> typ list ->
term list -> term -> local_theory -> (term * thm) * local_theory
- val mk_induct_raw_prem: Proof.context -> typ list list -> (string * term list) list -> term ->
- term -> typ list -> typ list ->
+ val mk_induct_raw_prem: (term -> term) -> Proof.context -> typ list list ->
+ (string * term list) list -> term -> term -> typ list -> typ list ->
term list * ((term * (term * term)) list * (int * term)) list * term
val finish_induct_prem: Proof.context -> int -> term list ->
term list * ((term * (term * term)) list * (int * term)) list * term -> term
+ val mk_coinduct_prem: Proof.context -> typ list list -> typ list list -> term list -> term ->
+ term -> term -> int -> term list -> term list list -> term list -> term list list ->
+ typ list list -> term
val mk_induct_attrs: term list list -> Token.src list
val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list ->
Token.src list * Token.src list
@@ -176,18 +179,18 @@
BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
term list -> thm list -> Proof.context -> lfp_sugar_thms
- val derive_coinduct_thms_for_types: bool -> (term -> term) -> BNF_Def.bnf list -> thm ->
- thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list list list -> int list ->
+ val derive_coinduct_thms_for_types: Proof.context -> bool -> (term -> term) -> BNF_Def.bnf list ->
+ thm -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list list list -> int list ->
thm list -> thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list ->
- Proof.context -> (thm list * thm) list
- val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list ->
+ (thm list * thm) list
+ val derive_coinduct_corecs_thms_for_types: Proof.context -> BNF_Def.bnf list ->
string * term list * term list list
* (((term list list * term list list * term list list list list * term list list list list)
* term list list list) * typ list) ->
thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list ->
typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
- thm list -> Proof.context -> gfp_sugar_thms
+ thm list -> gfp_sugar_thms
val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
binding list -> binding list list -> binding list -> (string * sort) list ->
@@ -530,7 +533,7 @@
Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u));
fun build_the_rel ctxt Rs Ts A B =
- build_rel [] ctxt Ts (the o choose_binary_fun Rs) (A, B);
+ build_rel [] ctxt Ts [] (the o choose_binary_fun Rs) (A, B);
fun build_rel_app ctxt Rs Ts t u =
build_the_rel ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u;
@@ -860,7 +863,7 @@
fun mk_arg (x as Free (_, T)) (Free (_, U)) =
if T = U then x
- else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x;
+ else build_map lthy [] [] (the o AList.lookup (op =) ABfs) (T, U) $ x;
val xs' = map2 mk_arg xs ys;
in
@@ -1242,7 +1245,7 @@
val lhsT = fastype_of lhs;
val map_rhsT =
map_atyps (perhaps (AList.lookup (op =) (map swap live_AsBs))) lhsT;
- val map_rhs = build_map lthy []
+ val map_rhs = build_map lthy [] []
(the o (AList.lookup (op =) (live_AsBs ~~ fs))) (map_rhsT, lhsT);
val rhs = (case map_rhs of
Const (@{const_name id}, _) => selA $ ta
@@ -1539,7 +1542,7 @@
val cpss = map2 (map o rapp) cs pss;
- fun build_sum_inj mk_inj = build_map ctxt [] (uncurry mk_inj o dest_sumT o snd);
+ fun build_sum_inj mk_inj = build_map ctxt [] [] (uncurry mk_inj o dest_sumT o snd);
fun build_dtor_corec_arg _ [] [cg] = cg
| build_dtor_corec_arg T [cq] [cg, cg'] =
@@ -1623,7 +1626,7 @@
@{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
end;
-fun mk_induct_raw_prem_prems names_lthy Xss setss_fp_nesting (x as Free (s, Type (T_name, Ts0)))
+fun mk_induct_raw_prem_prems names_ctxt Xss setss_fp_nesting (x as Free (s, Type (T_name, Ts0)))
(Type (_, Xs_Ts0)) =
(case AList.lookup (op =) setss_fp_nesting T_name of
NONE => []
@@ -1633,9 +1636,9 @@
filter (exists_subtype_in (flat Xss) o fst) (Xs_Ts0 ~~ (Ts0 ~~ raw_sets0))
|> split_list ||> split_list;
val sets = map (mk_set Ts0) raw_sets;
- val (ys, names_lthy') = names_lthy |> mk_Frees s Ts;
+ val (ys, names_ctxt') = names_ctxt |> mk_Frees s Ts;
val xysets = map (pair x) (ys ~~ sets);
- val ppremss = map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) ys Xs_Ts;
+ val ppremss = map2 (mk_induct_raw_prem_prems names_ctxt' Xss setss_fp_nesting) ys Xs_Ts;
in
flat (map2 (map o apfst o cons) xysets ppremss)
end)
@@ -1643,29 +1646,59 @@
[([], (find_index (fn Xs => member (op =) Xs X) Xss + 1, x))]
| mk_induct_raw_prem_prems _ _ _ _ _ = [];
-fun mk_induct_raw_prem names_lthy Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts =
+fun mk_induct_raw_prem alter_x names_ctxt Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts =
let
- val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
+ val (xs, names_ctxt') = names_ctxt |> mk_Frees "x" ctr_Ts;
val pprems =
- flat (map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) xs ctrXs_Ts);
- val y = Term.list_comb (ctr, xs);
- val p' = enforce_type names_lthy domain_type (fastype_of y) p;
+ flat (map2 (mk_induct_raw_prem_prems names_ctxt' Xss setss_fp_nesting) xs ctrXs_Ts);
+ val y = Term.list_comb (ctr, map alter_x xs);
+ val p' = enforce_type names_ctxt domain_type (fastype_of y) p;
in (xs, pprems, HOLogic.mk_Trueprop (p' $ y)) end;
fun close_induct_prem_prem nn ps xs t =
fold_rev Logic.all (map Free (drop (nn + length xs)
(rev (Term.add_frees t (map dest_Free xs @ map_filter (try dest_Free) ps))))) t;
-fun finish_induct_prem_prem lthy nn ps xs (xysets, (j, x)) =
- let val p' = enforce_type lthy domain_type (fastype_of x) (nth ps (j - 1)) in
+fun finish_induct_prem_prem ctxt nn ps xs (xysets, (j, x)) =
+ let val p' = enforce_type ctxt domain_type (fastype_of x) (nth ps (j - 1)) in
close_induct_prem_prem nn ps xs (Logic.list_implies (map (fn (x', (y, set)) =>
mk_Trueprop_mem (y, set $ x')) xysets,
HOLogic.mk_Trueprop (p' $ x)))
end;
-fun finish_induct_prem lthy nn ps (xs, raw_pprems, concl) =
+fun finish_induct_prem ctxt nn ps (xs, raw_pprems, concl) =
fold_rev Logic.all xs (Logic.list_implies
- (map (finish_induct_prem_prem lthy nn ps xs) raw_pprems, concl));
+ (map (finish_induct_prem_prem ctxt nn ps xs) raw_pprems, concl));
+
+fun mk_coinduct_prem_ctr_concls ctxt Xss fpTss rs' n k udisc usels vdisc vsels ctrXs_Ts =
+ let
+ fun build_the_rel T Xs_T =
+ build_rel [] ctxt [] [] (fn (T, X) =>
+ nth rs' (find_index (fn Xs => member (op =) Xs X) Xss)
+ |> enforce_type ctxt domain_type T)
+ (T, Xs_T)
+ |> Term.subst_atomic_types (flat Xss ~~ flat fpTss);
+ fun build_rel_app usel vsel Xs_T =
+ fold rapp [usel, vsel] (build_the_rel (fastype_of usel) Xs_T);
+ in
+ (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
+ (if null usels then
+ []
+ else
+ [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
+ Library.foldr1 HOLogic.mk_conj (@{map 3} build_rel_app usels vsels ctrXs_Ts))])
+ end;
+
+fun mk_coinduct_prem_concl ctxt Xss fpTss rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
+ @{map 6} (mk_coinduct_prem_ctr_concls ctxt Xss fpTss rs' n)
+ (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss
+ |> flat |> Library.foldr1 HOLogic.mk_conj
+ handle List.Empty => @{term True};
+
+fun mk_coinduct_prem ctxt Xss fpTss rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
+ fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
+ HOLogic.mk_Trueprop (mk_coinduct_prem_concl ctxt Xss fpTss rs' n udiscs uselss vdiscs vselss
+ ctrXs_Tss)));
fun postproc_co_induct ctxt nn prop prop_conj =
Drule.zero_var_indexes
@@ -1679,7 +1712,7 @@
let val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
in [Attrib.case_names induct_cases] end;
-fun derive_rel_induct_thms_for_types lthy nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
+fun derive_rel_induct_thms_for_types ctxt nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
let
val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
@@ -1689,7 +1722,7 @@
val ctrBs_Tsss = map (map (map B_ify_T)) ctrAs_Tsss;
val ctrBss = map (map B_ify) ctrAss;
- val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy
+ val ((((Rs, IRs), ctrAsss), ctrBsss), names_ctxt) = ctxt
|> mk_Frees "R" (map2 mk_pred2T As Bs)
||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts)
||>> mk_Freesss "a" ctrAs_Tsss
@@ -1699,30 +1732,30 @@
let
fun mk_prem ctrA ctrB argAs argBs =
fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies)
- (map2 (HOLogic.mk_Trueprop oo build_rel_app names_lthy (Rs @ IRs) fpA_Ts) argAs argBs)
- (HOLogic.mk_Trueprop (build_rel_app names_lthy (Rs @ IRs) fpA_Ts
+ (map2 (HOLogic.mk_Trueprop oo build_rel_app names_ctxt (Rs @ IRs) fpA_Ts) argAs argBs)
+ (HOLogic.mk_Trueprop (build_rel_app names_ctxt (Rs @ IRs) fpA_Ts
(Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs)))));
in
flat (@{map 4} (@{map 4} mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
end;
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
- (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs));
- val vars = Variable.add_free_names lthy goal [];
+ (map2 (build_the_rel ctxt (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs));
+ val vars = Variable.add_free_names ctxt goal [];
val rel_induct0_thm =
- Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} =>
+ Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} =>
mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts
ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
|> Thm.close_derivation;
in
- (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm,
+ (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm,
mk_induct_attrs ctrAss)
end;
fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
- live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses pre_type_definitions
- abs_inverses ctrss ctr_defss recs rec_defs lthy =
+ live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss pre_abs_inverses pre_type_definitions
+ abs_inverses ctrss ctr_defss recs rec_defs ctxt =
let
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
@@ -1738,7 +1771,7 @@
val fp_b_names = map base_name_of_typ fpTs;
- val (((ps, xsss), us'), names_lthy) = lthy
+ val (((ps, xsss), us'), names_ctxt) = ctxt
|> mk_Frees "P" (map mk_pred1T fpTs)
||>> mk_Freesss "x" ctr_Tsss
||>> Variable.variant_fixes fp_b_names;
@@ -1750,22 +1783,21 @@
val (induct_thms, induct_thm) =
let
val raw_premss = @{map 4} (@{map 3}
- o mk_induct_raw_prem names_lthy (map single Xs) setss_fp_nesting)
+ o mk_induct_raw_prem I names_ctxt (map single Xs) setss_fp_nesting)
ps ctrss ctr_Tsss ctrXs_Tsss;
val concl =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us));
val goal =
- Library.foldr (Logic.list_implies o apfst (map (finish_induct_prem lthy nn ps)))
+ Library.foldr (Logic.list_implies o apfst (map (finish_induct_prem ctxt nn ps)))
(raw_premss, concl);
- val vars = Variable.add_free_names lthy goal [];
-
+ val vars = Variable.add_free_names ctxt goal [];
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
val ctor_induct' = ctor_induct OF (map2 mk_absumprodE pre_type_definitions mss);
val thm =
- Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
- mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses
+ Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
+ mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' pre_abs_inverses
abs_inverses fp_nesting_set_maps pre_set_defss)
|> Thm.close_derivation;
in
@@ -1797,7 +1829,7 @@
indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
(fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk));
in
- build_map lthy [] build_simple (T, U) $ x
+ build_map ctxt [] [] build_simple (T, U) $ x
end;
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
@@ -1805,10 +1837,10 @@
val tacss = @{map 4} (map ooo
mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs)
- ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
+ ctor_rec_thms pre_abs_inverses abs_inverses ctr_defss;
fun prove goal tac =
- Goal.prove_sorry lthy [] [] goal (tac o #context)
+ Goal.prove_sorry ctxt [] [] goal (tac o #context)
|> Thm.close_derivation;
in
map2 (map2 prove) goalss tacss
@@ -1853,7 +1885,7 @@
(coinduct_attrs, common_coinduct_attrs)
end;
-fun derive_rel_coinduct_thms_for_types lthy nn fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list)
+fun derive_rel_coinduct_thms_for_types ctxt nn fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list)
abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct
live_nesting_rel_eqs =
let
@@ -1863,14 +1895,14 @@
val (Rs, IRs, fpAs, fpBs, _) =
let
val fp_names = map base_name_of_typ fpA_Ts;
- val ((((Rs, IRs), fpAs_names), fpBs_names), names_lthy) = lthy
+ val ((((Rs, IRs), fpAs_names), fpBs_names), names_ctxt) = ctxt
|> mk_Frees "R" (map2 mk_pred2T As Bs)
||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts)
||>> Variable.variant_fixes fp_names
||>> Variable.variant_fixes (map (suffix "'") fp_names);
in
(Rs, IRs, map2 (curry Free) fpAs_names fpA_Ts, map2 (curry Free) fpBs_names fpB_Ts,
- names_lthy)
+ names_ctxt)
end;
val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) =
@@ -1896,7 +1928,7 @@
[Library.foldr HOLogic.mk_imp
(if n = 1 then [] else [discA_t, discB_t],
Library.foldr1 HOLogic.mk_conj
- (map2 (build_rel_app lthy (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]);
+ (map2 (build_rel_app ctxt (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]);
fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss =
Library.foldr1 HOLogic.mk_conj (flat (@{map 5} (mk_prem_ctr_concls n)
@@ -1911,22 +1943,22 @@
end;
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
- IRs (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts)));
- val vars = Variable.add_free_names lthy goal [];
+ IRs (map2 (build_the_rel ctxt (Rs @ IRs) []) fpA_Ts fpB_Ts)));
+ val vars = Variable.add_free_names ctxt goal [];
val rel_coinduct0_thm =
- Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} =>
+ Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} =>
mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (Thm.cterm_of ctxt) IRs) prems
(map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
(map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
rel_pre_defs abs_inverses live_nesting_rel_eqs)
|> Thm.close_derivation;
in
- (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
+ (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
end;
-fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts set_pre_defs
+fun derive_set_induct_thms_for_types ctxt nn fpTs ctrss setss dtor_set_inducts exhausts set_pre_defs
ctor_defs dtor_ctors Abs_pre_inverses =
let
fun mk_prems A Ps ctr_args t ctxt =
@@ -1995,9 +2027,9 @@
|>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj))
|>> apsnd flat;
- val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
+ val vars = fold (Variable.add_free_names ctxt) (concl :: prems) [];
val thm =
- Goal.prove_sorry lthy vars prems (HOLogic.mk_Trueprop concl)
+ Goal.prove_sorry ctxt vars prems (HOLogic.mk_Trueprop concl)
(fn {context = ctxt, prems} =>
mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts
exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
@@ -2010,7 +2042,7 @@
end
val consumes_attr = Attrib.consumes 1;
in
- map (mk_thm lthy fpTs ctrss
+ map (mk_thm ctxt fpTs ctrss
#> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr))
(transpose setss)
end;
@@ -2034,9 +2066,9 @@
|> unfold_thms ctxt unfolds
end;
-fun derive_coinduct_thms_for_types strong alter_r pre_bnfs dtor_coinduct dtor_ctors
- live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss
- (ctr_sugars : ctr_sugar list) ctxt =
+fun derive_coinduct_thms_for_types ctxt strong alter_r pre_bnfs dtor_coinduct dtor_ctors
+ live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p ctr_defss
+ (ctr_sugars : ctr_sugar list) =
let
val nn = length pre_bnfs;
@@ -2070,45 +2102,23 @@
@{map 4} (fn u => fn v => fn uvr => fn uv_eq =>
fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
- fun build_the_rel rs' T Xs_T =
- build_rel [] ctxt [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
- |> Term.subst_atomic_types (Xs ~~ fpTs);
-
- fun build_rel_app rs' usel vsel Xs_T =
- fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T);
-
- fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts =
- (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
- (if null usels then
- []
- else
- [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
- Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]);
-
- fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
- flat (@{map 6} (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)
- |> Library.foldr1 HOLogic.mk_conj
- handle List.Empty => @{term True};
-
- fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
- fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
- HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss)));
-
val concl =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
- uvrs us vs));
+ uvrs us vs))
fun mk_goal rs0' =
- Logic.list_implies (@{map 9} (mk_prem (map alter_r rs0')) uvrs us vs ns udiscss uselsss
- vdiscss vselsss ctrXs_Tsss, concl);
+ Logic.list_implies (@{map 9} (mk_coinduct_prem ctxt (map single Xs) (map single fpTs)
+ (map alter_r rs0'))
+ uvrs us vs ns udiscss uselsss vdiscss vselsss ctrXs_Tsss,
+ concl);
val goals = map mk_goal ([rs] @ (if strong then [strong_rs] else []));
fun prove dtor_coinduct' goal =
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
- mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses
+ mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses
abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss))
|> Thm.close_derivation;
@@ -2123,10 +2133,10 @@
dtor_coinducts goals
end;
-fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
- dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
- kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
- corecs corec_defs ctxt =
+fun derive_coinduct_corecs_thms_for_types ctxt pre_bnfs
+ (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) dtor_coinduct dtor_injects dtor_ctors
+ dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns pre_abs_inverses abs_inverses
+ mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) corecs corec_defs =
let
fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]];
@@ -2146,9 +2156,9 @@
val discIss = map #discIs ctr_sugars;
val sel_thmsss = map #sel_thmss ctr_sugars;
- val coinduct_thms_pairs = derive_coinduct_thms_for_types true I pre_bnfs dtor_coinduct
- dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns fp_abs_inverses abs_inverses mk_vimage2p
- ctr_defss ctr_sugars ctxt;
+ val coinduct_thms_pairs = derive_coinduct_thms_for_types ctxt true I pre_bnfs dtor_coinduct
+ dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p
+ ctr_defss ctr_sugars;
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
@@ -2182,7 +2192,7 @@
indexify fst (map2 (curry mk_sumT) fpTs Cs)
(fn kk => fn _ => tack (nth cs kk, nth us kk) (nth gcorecs kk));
in
- build_map ctxt [] build_simple (T, U) $ cqg
+ build_map ctxt [] [] build_simple (T, U) $ cqg
end
else
cqg
@@ -2595,7 +2605,7 @@
fun mk_rec_arg_arg (x as Free (_, T)) =
let val U = B_ify_T T in
- if T = U then x else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x
+ if T = U then x else build_map lthy [] [] (the o AList.lookup (op =) ABfs) (T, U) $ x
end;
fun mk_rec_o_map_arg rec_arg_T h =
@@ -2748,8 +2758,10 @@
val T = range_type (fastype_of g);
val U = range_type corec_argB_T;
in
- if T = U then g
- else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABfs) (T, U), g)
+ if T = U then
+ g
+ else
+ HOLogic.mk_comp (build_map lthy2 [] [] (the o AList.lookup (op =) ABfs) (T, U), g)
end;
fun mk_map_o_corec_rhs corecx =
@@ -2785,9 +2797,9 @@
(coinduct_attrs, common_coinduct_attrs)),
corec_thmss, corec_disc_thmss,
(corec_disc_iff_thmss, corec_disc_iff_attrs), (corec_sel_thmsss, corec_sel_attrs)) =
- derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
+ derive_coinduct_corecs_thms_for_types lthy pre_bnfs (the corecs_args_types) xtor_co_induct
dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
- ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs lthy;
+ ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs;
fun distinct_prems ctxt thm =
Goal.prove (*no sorry*) ctxt [] []
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Dec 23 20:10:38 2016 +0100
@@ -12,6 +12,8 @@
val co_induct_inst_as_projs_tac: Proof.context -> int -> tactic
val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_coinduct_discharge_prem_tac: Proof.context -> thm list -> thm list -> int -> int -> int ->
+ thm -> thm -> thm -> thm -> thm -> thm list -> thm list list -> thm list list -> int -> tactic
val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
thm list list list -> tactic
@@ -28,6 +30,8 @@
val mk_disc_transfer_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
+ val mk_induct_discharge_prem_tac: Proof.context -> int -> int -> thm list -> thm list ->
+ thm list -> thm list -> int -> int -> int list -> tactic
val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
@@ -177,10 +181,10 @@
rec_o_map_simps) ctxt))
end;
-fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
+fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec pre_abs_inverse abs_inverse ctr_def ctxt =
HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE
else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN
- unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
+ unfold_thms_tac ctxt (ctor_rec :: pre_abs_inverse :: abs_inverse :: rec_defs @
pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac ctxt refl);
fun mk_rec_transfer_tac ctxt nn ns actives passives xssss rec_defs ctor_rec_transfers rel_pre_T_defs
@@ -314,15 +318,15 @@
resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
(rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' rtac ctxt @{thm singletonI});
-fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
+fun mk_induct_leverage_prem_prems_tac ctxt nn kks pre_abs_inverses abs_inverses set_maps
pre_set_defs =
HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
etac ctxt meta_mp,
- SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @
+ SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ pre_abs_inverses @ abs_inverses @ set_maps @
sumprod_thms_set)),
solve_prem_prem_tac ctxt]) (rev kks)));
-fun mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps pre_set_defs m k
+fun mk_induct_discharge_prem_tac ctxt nn n pre_abs_inverses abs_inverses set_maps pre_set_defs m k
kks =
let val r = length kks in
HEADGOAL (EVERY' [select_prem_tac ctxt n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt,
@@ -330,11 +334,11 @@
EVERY [REPEAT_DETERM_N r
(HEADGOAL (rotate_tac ~1 THEN' dtac ctxt meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL (assume_tac ctxt),
- mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
+ mk_induct_leverage_prem_prems_tac ctxt nn kks pre_abs_inverses abs_inverses set_maps
pre_set_defs]
end;
-fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' fp_abs_inverses abs_inverses set_maps
+fun mk_induct_tac ctxt nn ns mss kksss ctr_defs ctor_induct' pre_abs_inverses abs_inverses set_maps
pre_set_defss =
let val n = Integer.sum ns in
(if exists is_def_looping ctr_defs then
@@ -343,18 +347,18 @@
unfold_thms_tac ctxt ctr_defs) THEN
HEADGOAL (rtac ctxt ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN
EVERY (@{map 4} (EVERY oooo @{map 3} o
- mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps)
- pre_set_defss mss (unflat mss (1 upto n)) kkss)
+ mk_induct_discharge_prem_tac ctxt nn n pre_abs_inverses abs_inverses set_maps)
+ pre_set_defss mss (unflat mss (1 upto n)) kksss)
end;
-fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def fp_abs_inverse abs_inverse dtor_ctor ctr_def
- discs sels =
+fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def pre_abs_inverse abs_inverse dtor_ctor ctr_def
+ discs sels extra_unfolds =
hyp_subst_tac ctxt THEN'
CONVERSION (hhf_concl_conv
(Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
- SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
- sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
+ SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: pre_abs_inverse :: abs_inverse :: dtor_ctor ::
+ sels @ sumprod_thms_rel @ extra_unfolds @ @{thms o_apply vimage2p_def})) THEN'
(assume_tac ctxt ORELSE' REPEAT o etac ctxt conjE THEN'
full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
REPEAT o etac ctxt conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
@@ -369,8 +373,8 @@
full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt)
end;
-fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def fp_abs_inverse abs_inverse
- dtor_ctor exhaust ctr_defs discss selss =
+fun mk_coinduct_discharge_prem_tac ctxt extra_unfolds rel_eqs' nn kk n pre_rel_def pre_abs_inverse
+ abs_inverse dtor_ctor exhaust ctr_defs discss selss =
let val ks = 1 upto n in
EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, dtac ctxt meta_spec, dtac ctxt meta_mp,
@@ -380,18 +384,18 @@
EVERY' ([rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
map2 (fn k' => fn discs' =>
if k' = k then
- mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def fp_abs_inverse abs_inverse
- dtor_ctor ctr_def discs sels
+ mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def pre_abs_inverse abs_inverse
+ dtor_ctor ctr_def discs sels extra_unfolds
else
mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss)
end;
-fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses abs_inverses
+fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses abs_inverses
dtor_ctors exhausts ctr_defss discsss selsss =
HEADGOAL (rtac ctxt dtor_coinduct' THEN'
- EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
- (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
- selsss));
+ EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt [] rel_eqs' nn)
+ (1 upto nn) ns pre_rel_defs pre_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss
+ discsss selsss));
fun mk_map_tac ctxt abs_inverses pre_map_def map_ctor live_nesting_map_id0s ctr_defs'
extra_unfolds =
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Dec 23 20:10:38 2016 +0100
@@ -283,10 +283,10 @@
([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
||> (fn info => (SOME info, NONE))
else
- derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types)
+ derive_coinduct_corecs_thms_for_types lthy pre_bnfs (the corecs_args_types)
xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs
ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses
- (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs lthy
+ (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs
|> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
(corec_sel_thmsss, _)) =>
(map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Dec 23 20:10:38 2016 +0100
@@ -1005,8 +1005,8 @@
val simple_Ts = map fst simple_T_mapfs;
- val t_map = build_map ctxt simple_Ts build_simple (apply2 (range_type o fastype_of) (t, u));
- val u_map = build_map ctxt simple_Ts build_simple (apply2 (domain_type o fastype_of) (t, u));
+ val t_map = build_map ctxt simple_Ts [] build_simple (apply2 (range_type o fastype_of) (t, u));
+ val u_map = build_map ctxt simple_Ts [] build_simple (apply2 (domain_type o fastype_of) (t, u));
in
mk_Trueprop_eq (HOLogic.mk_comp (u, u_map), HOLogic.mk_comp (t_map, t))
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Dec 23 20:10:38 2016 +0100
@@ -587,7 +587,7 @@
||>> mk_Frees "y" xy_Ts;
fun mk_prem xy_T x y =
- build_rel [] ctxt [fpT] (fn (T, _) => if T = fpT then Rcong else HOLogic.eq_const T)
+ build_rel [] ctxt [fpT] [] (fn (T, _) => if T = fpT then Rcong else HOLogic.eq_const T)
(xy_T, xy_T) $ x $ y;
val prems = @{map 3} mk_prem xy_Ts xs ys;
@@ -685,9 +685,9 @@
fun mk_applied_cong arg =
enforce_type ctxt domain_type (fastype_of arg) cong0 $ arg;
- val thm = derive_coinduct_thms_for_types false mk_applied_cong [pre_bnf] dtor_coinduct
+ val thm = derive_coinduct_thms_for_types ctxt false mk_applied_cong [pre_bnf] dtor_coinduct
dtor_ctors live_nesting_bnfs [fpT] [substXAT X] [map (map substXAT) ctrXs_Tss] [n]
- [abs_inverse] [abs_inverse] I [ctr_defs] [morph_ctr_sugar phi ctr_sugar0] ctxt
+ [abs_inverse] [abs_inverse] I [ctr_defs] [morph_ctr_sugar phi ctr_sugar0]
|> map snd |> the_single;
val (attrs, _) = mk_coinduct_attrs [fpT] [ctrs0] [discs0] [ms];
in
@@ -713,7 +713,7 @@
|> explore {bound_Us = T :: bound_Us, bound_Ts = T :: bound_Ts, U = U, T = T}
|> (fn t => Abs (Name.uu, T, t));
in
- betapply (build_map lthy [] build_simple (T, U), t)
+ betapply (build_map lthy [] [] build_simple (T, U), t)
end;
fun add_boundvar t = betapply (incr_boundvars 1 t, Bound 0);
@@ -1047,7 +1047,7 @@
val param2_T = Type_Infer.paramify_vars param1_T;
val deadfixed_T =
- build_map lthy [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
+ build_map lthy [] [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
|> singleton (Type_Infer_Context.infer_types lthy)
|> singleton (Type_Infer.fixate lthy false)
|> type_of
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Dec 23 20:10:38 2016 +0100
@@ -209,7 +209,7 @@
if op = TU then
t
else
- (case try (build_map ctxt [] (the o AList.lookup (op =) AB_fs)) TU of
+ (case try (build_map ctxt [] [] (the o AList.lookup (op =) AB_fs)) TU of
SOME mapx => mapx $ t
| NONE => raise UNNATURAL ());
@@ -356,7 +356,7 @@
fun mk_friend_spec () =
let
fun encapsulate_nested U T free =
- betapply (build_map ctxt [] (fn (T, _) =>
+ betapply (build_map ctxt [] [] (fn (T, _) =>
if T = domain_type VLeaf0_T then Abs (Name.uu, T, VLeaf0 $ Bound 0)
else Abs (Name.uu, T, Bound 0)) (T, U),
free);
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Dec 23 20:10:38 2016 +0100
@@ -962,7 +962,7 @@
end;
fun massage_noncall U T t =
- build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t;
+ build_map ctxt [] [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t;
val bound_Ts = List.rev (map fastype_of fun_args);
in
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Dec 23 20:10:38 2016 +0100
@@ -37,8 +37,6 @@
val split_connectI = @{thms allI impI conjI};
val unfold_lets = @{thms Let_def[abs_def] split_beta}
-fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
-
fun exhaust_inst_as_projs ctxt frees thm =
let
val num_frees = length frees;
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Fri Dec 23 20:10:38 2016 +0100
@@ -106,7 +106,7 @@
NONE
else if exists_subtype_in fpTs T then
let val U = mk_U T in
- SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
+ SOME (mk_to_nat_checked U $ (build_map ctxt [] [] (snd_const o fst) (T, U) $ Bound j))
end
else
SOME (mk_to_nat_checked T $ Bound j);
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Dec 23 20:10:38 2016 +0100
@@ -86,7 +86,7 @@
fun check_no_call t = if has_call t then unexpected_rec_call ctxt [t0] t else ();
val typof = curry fastype_of1 bound_Ts;
- val massage_no_call = build_map ctxt [] massage_nonfun;
+ val massage_no_call = build_map ctxt [] [] massage_nonfun;
val yT = typof y;
val yU = typof y';
--- a/src/HOL/Tools/BNF/bnf_tactics.ML Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Fri Dec 23 20:10:38 2016 +0100
@@ -11,6 +11,7 @@
include CTR_SUGAR_GENERAL_TACTICS
val fo_rtac: Proof.context -> thm -> int -> tactic
+ val clean_blast_tac: Proof.context -> int -> tactic
val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic
@@ -43,6 +44,8 @@
end
handle Pattern.MATCH => no_tac) ctxt;
+fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
+
(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0];
--- a/src/HOL/Wellfounded.thy Fri Dec 23 20:06:54 2016 +0100
+++ b/src/HOL/Wellfounded.thy Fri Dec 23 20:10:38 2016 +0100
@@ -308,7 +308,7 @@
done
lemma wfP_SUP:
- "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow>
+ "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
wfP (SUPREMUM UNIV r)"
by (rule wf_UN[to_pred]) simp_all