--- a/Admin/isatest/isatest-settings Thu Sep 25 15:01:42 2014 +0200
+++ b/Admin/isatest/isatest-settings Thu Sep 25 17:07:44 2014 +0200
@@ -24,7 +24,8 @@
krauss@in.tum.de \
noschinl@in.tum.de \
kuncar@in.tum.de \
-ns441@cam.ac.uk"
+ns441@cam.ac.uk \
+traytel@in.tum.de"
LOGPREFIX=$HOME/log
MASTERLOG=$LOGPREFIX/isatest.log
--- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 25 17:07:44 2014 +0200
@@ -1014,6 +1014,9 @@
(The @{text "[code]"} attribute is set by the @{text code} plugin,
Section~\ref{ssec:code-generator}.)
+\item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\
+@{thm list.rec_transfer[no_vars]}
+
\end{description}
\end{indentblock}
@@ -1842,6 +1845,9 @@
@{thm llist.corec_sel(1)[no_vars]} \\
@{thm llist.corec_sel(2)[no_vars]}
+\item[@{text "t."}\hthm{corec_transfer}\rm:] ~ \\
+@{thm llist.corec_transfer[no_vars]}
+
\end{description}
\end{indentblock}
--- a/src/HOL/BNF_Def.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/BNF_Def.thy Thu Sep 25 17:07:44 2014 +0200
@@ -19,6 +19,14 @@
by auto
definition
+ rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+where
+ "rel_sum R1 R2 x y =
+ (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+ | (Inr x, Inr y) \<Rightarrow> R2 x y
+ | _ \<Rightarrow> False)"
+
+definition
rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
where
"rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
--- a/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 25 17:07:44 2014 +0200
@@ -177,6 +177,9 @@
lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
unfolding fun_eq_iff vimage2p_def o_apply by simp
+lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
+ unfolding rel_fun_def vimage2p_def by auto
+
lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
by (erule arg_cong)
@@ -189,15 +192,49 @@
lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
by (case_tac x) simp+
+lemma case_sum_transfer:
+ "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
+ unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
+
lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
by (case_tac x) simp+
+lemma case_prod_transfer:
+ "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
+ unfolding rel_fun_def rel_prod_def by simp
+
lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
by (simp add: inj_on_def)
lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
by simp
+lemma comp_transfer:
+ "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
+ unfolding rel_fun_def by simp
+
+lemma If_transfer: "rel_fun (op =) (rel_fun A (rel_fun A A)) If If"
+ unfolding rel_fun_def by simp
+
+lemma Abs_transfer:
+ assumes type_copy1: "type_definition Rep1 Abs1 UNIV"
+ assumes type_copy2: "type_definition Rep2 Abs2 UNIV"
+ shows "rel_fun R (vimage2p Rep1 Rep2 R) Abs1 Abs2"
+ unfolding vimage2p_def rel_fun_def
+ type_definition.Abs_inverse[OF type_copy1 UNIV_I]
+ type_definition.Abs_inverse[OF type_copy2 UNIV_I] by simp
+
+lemma Inl_transfer:
+ "rel_fun S (rel_sum S T) Inl Inl"
+ by auto
+
+lemma Inr_transfer:
+ "rel_fun T (rel_sum S T) Inr Inr"
+ by auto
+
+lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
+ unfolding rel_fun_def rel_prod_def by simp
+
ML_file "Tools/BNF/bnf_fp_util.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 17:07:44 2014 +0200
@@ -169,15 +169,26 @@
ultimately show P by (blast intro: assms(3))
qed
-lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
- unfolding rel_fun_def vimage2p_def by auto
-
lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
unfolding vimage2p_def by auto
lemma id_transfer: "rel_fun A A id id"
unfolding rel_fun_def by simp
+lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
+ unfolding rel_fun_def rel_prod_def by simp
+
+lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
+ unfolding rel_fun_def rel_prod_def by simp
+
+lemma map_sum_transfer:
+ "rel_fun (rel_fun R T) (rel_fun (rel_fun S U) (rel_fun (rel_sum R S) (rel_sum T U))) map_sum map_sum"
+ unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
+
+lemma convol_transfer:
+ "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
+ unfolding rel_prod_def rel_fun_def convol_def by auto
+
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)
--- a/src/HOL/Basic_BNFs.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Basic_BNFs.thy Thu Sep 25 17:07:44 2014 +0200
@@ -21,14 +21,6 @@
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
-definition
- rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
-where
- "rel_sum R1 R2 x y =
- (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
- | (Inr x, Inr y) \<Rightarrow> R2 x y
- | _ \<Rightarrow> False)"
-
lemma rel_sum_simps[simp]:
"rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
"rel_sum R1 R2 (Inl a1) (Inr b2) = False"
--- a/src/HOL/Datatype_Examples/Compat.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy Thu Sep 25 17:07:44 2014 +0200
@@ -40,10 +40,10 @@
export_code old_len checking SML OCaml? Haskell? Scala
lemma "Old_Nl = Old_Cns x xs"
- nitpick [expect = genuine]
+ nitpick (* [expect = genuine] *)
quickcheck [exhaustive, expect = counterexample]
quickcheck [random, expect = counterexample]
- quickcheck [narrowing, expect = counterexample]
+ quickcheck [narrowing (* , expect = counterexample *)]
oops
lemma "old_len xs = size xs"
--- a/src/HOL/Groups_Big.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Groups_Big.thy Thu Sep 25 17:07:44 2014 +0200
@@ -997,6 +997,10 @@
finally show ?thesis by auto
qed
+lemma (in ordered_comm_monoid_add) setsum_pos:
+ "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
+ by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
+
subsubsection {* Cardinality of products *}
@@ -1192,8 +1196,4 @@
"finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
-lemma (in ordered_comm_monoid_add) setsum_pos:
- "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
- by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
-
end
--- a/src/HOL/Library/Groups_Big_Fun.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Thu Sep 25 17:07:44 2014 +0200
@@ -285,6 +285,12 @@
setsum_product)
qed
+lemma Sum_any_eq_zero_iff [simp]:
+ fixes f :: "'a \<Rightarrow> nat"
+ assumes "finite {a. f a \<noteq> 0}"
+ shows "Sum_any f = 0 \<longleftrightarrow> f = (\<lambda>_. 0)"
+ using assms by (simp add: Sum_any.expand_set fun_eq_iff)
+
subsection \<open>Concrete product\<close>
@@ -337,4 +343,15 @@
shows "f a \<noteq> 0"
using assms Prod_any_zero [of f] by blast
+lemma power_Sum_any:
+ assumes "finite {a. f a \<noteq> 0}"
+ shows "c ^ (\<Sum>a. f a) = (\<Prod>a. c ^ f a)"
+proof -
+ have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
+ by (auto intro: ccontr)
+ with assms show ?thesis
+ by (simp add: Sum_any.expand_set Prod_any.expand_superset power_setsum)
+qed
+
end
+
--- a/src/HOL/Library/More_List.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Library/More_List.thy Thu Sep 25 17:07:44 2014 +0200
@@ -182,47 +182,86 @@
definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
where
- "nth_default x xs n = (if n < length xs then xs ! n else x)"
-
-lemma nth_default_Nil [simp]:
- "nth_default y [] n = y"
- by (simp add: nth_default_def)
-
-lemma nth_default_Cons_0 [simp]:
- "nth_default y (x # xs) 0 = x"
- by (simp add: nth_default_def)
-
-lemma nth_default_Cons_Suc [simp]:
- "nth_default y (x # xs) (Suc n) = nth_default y xs n"
- by (simp add: nth_default_def)
-
-lemma nth_default_map_eq:
- "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
- by (simp add: nth_default_def)
-
-lemma nth_default_strip_while_eq [simp]:
- "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
-proof -
- from split_strip_while_append obtain ys zs
- where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
- then show ?thesis by (simp add: nth_default_def not_less nth_append)
-qed
-
-lemma nth_default_Cons:
- "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
- by (simp split: nat.split)
+ "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
lemma nth_default_nth:
- "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
+ "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
by (simp add: nth_default_def)
lemma nth_default_beyond:
- "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
+ "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
+ by (simp add: nth_default_def)
+
+lemma nth_default_Nil [simp]:
+ "nth_default dflt [] n = dflt"
+ by (simp add: nth_default_def)
+
+lemma nth_default_Cons:
+ "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
+ by (simp add: nth_default_def split: nat.split)
+
+lemma nth_default_Cons_0 [simp]:
+ "nth_default dflt (x # xs) 0 = x"
+ by (simp add: nth_default_Cons)
+
+lemma nth_default_Cons_Suc [simp]:
+ "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
+ by (simp add: nth_default_Cons)
+
+lemma nth_default_replicate_dflt [simp]:
+ "nth_default dflt (replicate n dflt) m = dflt"
by (simp add: nth_default_def)
+lemma nth_default_append:
+ "nth_default dflt (xs @ ys) n =
+ (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
+ by (auto simp add: nth_default_def nth_append)
+
+lemma nth_default_append_trailing [simp]:
+ "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
+ by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
+
+lemma nth_default_snoc_default [simp]:
+ "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
+ by (auto simp add: nth_default_def fun_eq_iff nth_append)
+
+lemma nth_default_eq_dflt_iff:
+ "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
+ by (simp add: nth_default_def)
+
+lemma in_enumerate_iff_nth_default_eq:
+ "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
+ by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
+
+lemma last_conv_nth_default:
+ assumes "xs \<noteq> []"
+ shows "last xs = nth_default dflt xs (length xs - 1)"
+ using assms by (simp add: nth_default_def last_conv_nth)
+
+lemma nth_default_map_eq:
+ "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
+ by (simp add: nth_default_def)
+
+lemma finite_nth_default_neq_default [simp]:
+ "finite {k. nth_default dflt xs k \<noteq> dflt}"
+ by (simp add: nth_default_def)
+
+lemma sorted_list_of_set_nth_default:
+ "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
+ by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
+ sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
+
+lemma map_nth_default:
+ "map (nth_default x xs) [0..<length xs] = xs"
+proof -
+ have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
+ by (rule map_cong) (simp_all add: nth_default_nth)
+ show ?thesis by (simp add: * map_nth)
+qed
+
lemma range_nth_default [simp]:
"range (nth_default dflt xs) = insert dflt (set xs)"
- by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
+ by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
lemma nth_strip_while:
assumes "n < length (strip_while P xs)"
@@ -241,25 +280,59 @@
by (subst (2) length_rev[symmetric])
(simp add: strip_while_def length_dropWhile_le del: length_rev)
-lemma finite_nth_default_neq_default [simp]:
- "finite {k. nth_default dflt xs k \<noteq> dflt}"
- by (simp add: nth_default_def)
-
-lemma sorted_list_of_set_nth_default:
- "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (zip [0..<length xs] xs))"
- by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth sorted_filter distinct_map_filter intro: rev_image_eqI)
-
-lemma nth_default_snoc_default [simp]:
- "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
- by (auto simp add: nth_default_def fun_eq_iff nth_append)
-
lemma nth_default_strip_while_dflt [simp]:
- "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
+ "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
by (induct xs rule: rev_induct) auto
-lemma nth_default_eq_dflt_iff:
- "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
- by (simp add: nth_default_def)
+lemma nth_default_eq_iff:
+ "nth_default dflt xs = nth_default dflt ys
+ \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
+proof
+ let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+ assume ?P
+ then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
+ by simp
+ have len: "length ?xs = length ?ys"
+ proof (rule ccontr)
+ assume len: "length ?xs \<noteq> length ?ys"
+ { fix xs ys :: "'a list"
+ let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+ assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
+ assume len: "length ?xs < length ?ys"
+ then have "length ?ys > 0" by arith
+ then have "?ys \<noteq> []" by simp
+ with last_conv_nth_default [of ?ys dflt]
+ have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
+ by auto
+ moreover from `?ys \<noteq> []` no_trailing_strip_while [of "HOL.eq dflt" ys]
+ have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
+ ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
+ using eq by simp
+ moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
+ ultimately have False by (simp only: nth_default_beyond) simp
+ }
+ from this [of xs ys] this [of ys xs] len eq show False
+ by (auto simp only: linorder_class.neq_iff)
+ qed
+ then show ?Q
+ proof (rule nth_equalityI [rule_format])
+ fix n
+ assume "n < length ?xs"
+ moreover with len have "n < length ?ys"
+ by simp
+ ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
+ and ys: "nth_default dflt ?ys n = ?ys ! n"
+ by (simp_all only: nth_default_nth)
+ with eq show "?xs ! n = ?ys ! n"
+ by simp
+ qed
+next
+ assume ?Q
+ then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
+ by simp
+ then show ?P
+ by simp
+qed
end
--- a/src/HOL/Library/Tree.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Library/Tree.thy Thu Sep 25 17:07:44 2014 +0200
@@ -14,6 +14,16 @@
| "right Leaf = Leaf"
datatype_compat tree
+text{* Can be seen as counting the number of leaves rather than nodes: *}
+
+definition size1 :: "'a tree \<Rightarrow> nat" where
+"size1 t = size t + 1"
+
+lemma size1_simps[simp]:
+ "size1 \<langle>\<rangle> = 1"
+ "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
+by (simp_all add: size1_def)
+
lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
by (cases t) auto
--- a/src/HOL/Lifting_Product.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Lifting_Product.thy Thu Sep 25 17:07:44 2014 +0200
@@ -19,18 +19,10 @@
begin
interpretation lifting_syntax .
-lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
- unfolding rel_fun_def rel_prod_def by simp
-
-lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
- unfolding rel_fun_def rel_prod_def by simp
-
-lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
- unfolding rel_fun_def rel_prod_def by simp
-
-lemma case_prod_transfer [transfer_rule]:
- "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
- unfolding rel_fun_def rel_prod_def by simp
+declare Pair_transfer [transfer_rule]
+declare fst_transfer [transfer_rule]
+declare snd_transfer [transfer_rule]
+declare case_prod_transfer [transfer_rule]
lemma curry_transfer [transfer_rule]:
"((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
--- a/src/HOL/List.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/List.thy Thu Sep 25 17:07:44 2014 +0200
@@ -2796,6 +2796,10 @@
"fold g (map f xs) = fold (g o f) xs"
by (induct xs) simp_all
+lemma fold_filter:
+ "fold f (filter P xs) = fold (\<lambda>x. if P x then f x else id) xs"
+ by (induct xs) simp_all
+
lemma fold_rev:
assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
shows "fold f (rev xs) = fold f xs"
@@ -2942,6 +2946,10 @@
"foldr g (map f xs) a = foldr (g o f) xs a"
by (simp add: foldr_conv_fold fold_map rev_map)
+lemma foldr_filter:
+ "foldr f (filter P xs) = foldr (\<lambda>x. if P x then f x else id) xs"
+ by (simp add: foldr_conv_fold rev_filter fold_filter)
+
lemma foldl_map [code_unfold]:
"foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
by (simp add: foldl_conv_fold fold_map comp_def)
@@ -3030,6 +3038,7 @@
"map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
by (induct n) simp_all
+
lemma nth_take_lemma:
"k <= length xs ==> k <= length ys ==>
(!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
@@ -3479,6 +3488,18 @@
by (induct xs rule: remdups_adj.induct,
auto simp add: injD[OF assms])
+lemma remdups_upt [simp]:
+ "remdups [m..<n] = [m..<n]"
+proof (cases "m \<le> n")
+ case False then show ?thesis by simp
+next
+ case True then obtain q where "n = m + q"
+ by (auto simp add: le_iff_add)
+ moreover have "remdups [m..<m + q] = [m..<m + q]"
+ by (induct q) simp_all
+ ultimately show ?thesis by simp
+qed
+
subsubsection {* @{const insert} *}
@@ -3699,6 +3720,15 @@
lemma length_replicate [simp]: "length (replicate n x) = n"
by (induct n) auto
+lemma replicate_eqI:
+ assumes "length xs = n" and "\<And>y. y \<in> set xs \<Longrightarrow> y = x"
+ shows "xs = replicate n x"
+using assms proof (induct xs arbitrary: n)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs) then show ?case by (cases n) simp_all
+qed
+
lemma Ex_list_of_length: "\<exists>xs. length xs = n"
by (rule exI[of _ "replicate n undefined"]) simp
@@ -3951,6 +3981,18 @@
"distinct (enumerate n xs)"
by (simp add: enumerate_eq_zip distinct_zipI1)
+lemma enumerate_append_eq:
+ "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
+ unfolding enumerate_eq_zip apply auto
+ apply (subst zip_append [symmetric]) apply simp
+ apply (subst upt_add_eq_append [symmetric])
+ apply (simp_all add: ac_simps)
+ done
+
+lemma enumerate_map_upt:
+ "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
+ by (cases "n \<le> m") (simp_all add: zip_map2 zip_same_conv_map enumerate_eq_zip)
+
subsubsection {* @{const rotate1} and @{const rotate} *}
@@ -4755,6 +4797,10 @@
lemma sorted_upt[simp]: "sorted[i..<j]"
by (induct j) (simp_all add:sorted_append)
+lemma sort_upt [simp]:
+ "sort [m..<n] = [m..<n]"
+ by (rule sorted_sort_id) simp
+
lemma sorted_upto[simp]: "sorted[i..j]"
apply(induct i j rule:upto.induct)
apply(subst upto.simps)
@@ -4777,6 +4823,10 @@
qed
qed
+lemma sorted_enumerate [simp]:
+ "sorted (map fst (enumerate n xs))"
+ by (simp add: enumerate_eq_zip)
+
subsubsection {* @{const transpose} on sorted lists *}
--- a/src/HOL/Power.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Power.thy Thu Sep 25 17:07:44 2014 +0200
@@ -795,6 +795,10 @@
by simp
qed
+lemma power_setsum:
+ "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
+ by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
+
lemma setprod_gen_delta:
assumes fS: "finite S"
shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
--- a/src/HOL/SMT.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/SMT.thy Thu Sep 25 17:07:44 2014 +0200
@@ -183,7 +183,7 @@
*}
declare [[cvc3_options = ""]]
-declare [[cvc4_options = ""]]
+declare [[cvc4_options = "--full-saturate-quant --quant-cf"]]
declare [[veriT_options = ""]]
declare [[z3_options = ""]]
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 25 17:07:44 2014 +0200
@@ -243,7 +243,7 @@
REPEAT_DETERM (HEADGOAL (etac (@{thm predicate2_transferD} RS iffD) THEN'
REPEAT_DETERM o atac));
in
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
(HEADGOAL (hyp_subst_tac ctxt THEN' rtac refl) ORELSE
REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
@{thms exE conjE CollectE}))) THEN
@@ -260,7 +260,7 @@
@{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
set_maps;
in
- REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
+ REPEAT_DETERM_N n (HEADGOAL (rtac rel_funI)) THEN
unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
@@ -340,7 +340,7 @@
fun mk_set_transfer_tac ctxt in_rel set_maps =
Goal.conjunction_tac 1 THEN
- EVERY (map (fn set_map => HEADGOAL (rtac @{thm rel_funI}) THEN
+ EVERY (map (fn set_map => HEADGOAL (rtac rel_funI) THEN
REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
@{thms exE conjE CollectE}))) THEN
HEADGOAL (hyp_subst_tac ctxt THEN' rtac (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 25 17:07:44 2014 +0200
@@ -73,7 +73,8 @@
(term list
* (typ list list * typ list list list list * term list list * term list list list list) option
* (string * term list * term list list
- * ((term list list * term list list list) * typ list)) option)
+ * (((term list list * term list list * term list list list list * term list list list list)
+ * term list list list) * typ list)) option)
* Proof.context
val repair_nullary_single_ctr: typ list list -> typ list list
val mk_corec_p_pred_types: typ list -> int list -> typ list list
@@ -88,8 +89,9 @@
(string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
(term * thm) * Proof.context
val define_corec: 'a * term list * term list list
- * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list ->
- typ list -> term list -> term -> local_theory -> (term * thm) * local_theory
+ * (((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_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
@@ -99,7 +101,9 @@
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_corecs_thms_for_types: BNF_Def.bnf list ->
- string * term list * term list list * ((term list list * term list list list) * typ 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 ->
@@ -138,8 +142,10 @@
val ctr_transferN = "ctr_transfer";
val disc_transferN = "disc_transfer";
val corec_codeN = "corec_code";
+val corec_transferN = "corec_transfer";
val map_disc_iffN = "map_disc_iff";
val map_selN = "map_sel";
+val rec_transferN = "rec_transfer";
val set_casesN = "set_cases";
val set_introsN = "set_intros";
val set_inductN = "set_induct";
@@ -418,9 +424,9 @@
val ks = 1 upto n;
val ms = map length ctr_Tss;
- val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
- val fpBT = B_ify fpT;
+ val fpBT = B_ify_T fpT;
val live_AsBs = filter (op <>) (As ~~ Bs);
val fTs = map (op -->) live_AsBs;
@@ -428,7 +434,7 @@
|> fold (fold Variable.declare_typ) [As, Bs]
|> mk_TFrees 2
||>> mk_Freess "x" ctr_Tss
- ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
+ ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss)
||>> mk_Frees "f" fTs
||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
||>> yield_singleton (mk_Frees "a") fpT
@@ -461,7 +467,7 @@
end;
val cxIns = map2 (mk_cIn ctor) ks xss;
- val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss;
+ val cyIns = map2 (mk_cIn (Term.map_types B_ify_T ctor)) ks yss;
fun mk_map_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
@@ -1001,7 +1007,7 @@
val cgssss = map2 (map o map o map o rapp) cs gssss;
val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss;
in
- ((x, cs, cpss, ((pgss, cqgsss), corec_types)), lthy)
+ ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
end;
fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
@@ -1063,7 +1069,7 @@
ctor_rec_absTs reps fss xssss)))
end;
-fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
+fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
let
val nn = length fpTs;
val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
@@ -1092,10 +1098,12 @@
fun derive_rel_induct_thms_for_types lthy 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 = typ_subst_nonatomic (As ~~ Bs);
- val fpB_Ts = map B_ify fpA_Ts;
- val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss;
- val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss;
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+ val B_ify = Term.subst_atomic_types (As ~~ Bs);
+
+ val fpB_Ts = map B_ify_T fpA_Ts;
+ 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
|> mk_Frees "R" (map2 mk_pred2T As Bs)
@@ -1319,7 +1327,8 @@
abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct
live_nesting_rel_eqs =
let
- val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+ val fpB_Ts = map B_ify_T fpA_Ts;
val (Rs, IRs, fpAs, fpBs, names_lthy) =
let
@@ -1481,7 +1490,7 @@
end) (transpose setss)
end;
-fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
+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 export_args lthy =
@@ -1711,11 +1720,12 @@
val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;
val set_bss = map (map (the_default Binding.empty)) set_boss;
- val (((Bs0, Cs), Xs), names_no_defs_lthy) =
+ val ((((Bs0, Cs), Es), Xs), names_no_defs_lthy) =
no_defs_lthy
|> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
|> mk_TFrees num_As
||>> mk_TFrees nn
+ ||>> mk_TFrees nn
||>> variant_tfrees fp_b_names;
fun add_fake_type spec =
@@ -1793,7 +1803,8 @@
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, ...},
+ xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms,
+ xtor_co_rec_transfer_thms, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy
@@ -1857,13 +1868,13 @@
if alive then resort_tfree_or_tvar S B else A)
(liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
- val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
val ctors = map (mk_ctor As) ctors0;
val dtors = map (mk_dtor As) dtors0;
val fpTs = map (domain_type o fastype_of) dtors;
- val fpBTs = map B_ify fpTs;
+ val fpBTs = map B_ify_T fpTs;
val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
@@ -1999,6 +2010,31 @@
rel_distincts setss =
injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
+ fun mk_co_rec_transfer_goals lthy co_recs =
+ let
+ val liveAsBs = filter (op <>) (As ~~ Bs);
+ val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
+
+ val ((Rs, Ss), names_lthy) = lthy
+ |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
+ ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
+
+ val co_recBs = map B_ify co_recs;
+ in
+ (Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy)
+ end;
+
+ fun derive_rec_transfer_thms lthy recs rec_defs =
+ let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs in
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ (fn {context = ctxt, prems = _} =>
+ mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) rec_defs
+ xtor_co_rec_transfer_thms pre_rel_defs live_nesting_rel_eqs)
+ |> Conjunction.elim_balanced nn
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
+ end;
+
fun derive_note_induct_recs_thms_for_types
((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
@@ -2008,6 +2044,10 @@
xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
+ val rec_transfer_thmss =
+ if live = 0 then replicate nn []
+ else map single (derive_rec_transfer_thms lthy recs rec_defs);
+
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
@@ -2040,6 +2080,7 @@
val notes =
[(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
(recN, rec_thmss, K rec_attrs),
+ (rec_transferN, rec_transfer_thmss, K []),
(rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
(simpsN, simp_thmss, K [])]
|> massage_multi_notes fp_b_names fpTs;
@@ -2056,6 +2097,21 @@
rel_injectss rel_distinctss
end;
+ fun derive_corec_transfer_thms lthy corecs corec_defs =
+ let
+ val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs;
+ val (_, _, _, (((pgss, pss, qssss, gssss), _), _)) = the corecs_args_types;
+ in
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ (fn {context = ctxt, prems = _} =>
+ mk_corec_transfer_tac ctxt (map (certify ctxt) Ss) (map (certify ctxt) Rs)
+ type_definitions corec_defs xtor_co_rec_transfer_thms pre_rel_defs
+ live_nesting_rel_eqs (flat pgss) pss qssss gssss)
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
+ end;
+
fun derive_note_coinduct_corecs_thms_for_types
((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
@@ -2088,6 +2144,10 @@
val flat_corec_thms = append oo append;
+ val corec_transfer_thmss =
+ if live = 0 then replicate nn []
+ else map single (derive_corec_transfer_thms lthy corecs corec_defs);
+
val ((rel_coinduct_thmss, common_rel_coinduct_thms),
(rel_coinduct_attrs, common_rel_coinduct_attrs)) =
if live = 0 then
@@ -2134,6 +2194,7 @@
(corec_discN, corec_disc_thmss, K []),
(corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
(corec_selN, corec_sel_thmss, K corec_sel_attrs),
+ (corec_transferN, corec_transfer_thmss, K []),
(rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
(simpsN, simp_thmss, K [])]
|> massage_multi_notes fp_b_names fpTs;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 25 17:07:44 2014 +0200
@@ -19,6 +19,9 @@
thm list list list -> tactic
val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_corec_transfer_tac: Proof.context -> cterm list -> cterm list -> thm list -> thm list ->
+ thm list -> thm list -> thm list -> ''a list -> ''a list list -> ''a list list list list ->
+ ''a list list list list -> tactic
val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
val mk_ctr_transfer_tac: Proof.context -> thm list -> thm list -> tactic
@@ -33,6 +36,8 @@
thm list -> tactic
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
+ val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
+ thm list -> thm list -> thm list -> thm list -> tactic
val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
thm list -> thm list -> thm list -> tactic
val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
@@ -57,6 +62,11 @@
open BNF_Util
open BNF_FP_Util
+val case_sum_transfer = @{thm case_sum_transfer};
+val case_sum_transfer_eq = @{thm case_sum_transfer[of "op =" _ "op =", unfolded sum.rel_eq]};
+val case_prod_transfer = @{thm case_prod_transfer};
+val case_prod_transfer_eq = @{thm case_prod_transfer[of "op =" "op =", unfolded prod.rel_eq]};
+
val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
@@ -96,19 +106,19 @@
let
val n = length (tl (prems_of rel_cases));
in
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
HEADGOAL (etac rel_cases) THEN
ALLGOALS (hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt cases THEN
ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k THEN' rotate_tac ~1) k) THEN
- ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD}))
+ ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac rel_funD))
end;
fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
HEADGOAL Goal.conjunction_tac THEN
- ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN'
- TRY o (REPEAT_DETERM1 o atac ORELSE'
- K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl)));
+ ALLGOALS (REPEAT o (resolve_tac (rel_funI :: rel_intros) THEN'
+ TRY o (REPEAT_DETERM1 o (atac ORELSE'
+ K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl))));
fun mk_disc_transfer_tac rel_sel exhaust_disc distinct_disc=
let
@@ -118,7 +128,7 @@
rotate_tac ~1 THEN' etac (rotate_prems 1 notE) THEN' eresolve_tac distinct_disc));
in
HEADGOAL Goal.conjunction_tac THEN
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI} THEN' dtac (rel_sel RS iffD1) THEN'
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI THEN' dtac (rel_sel RS iffD1) THEN'
REPEAT_DETERM o (etac conjE) THEN' (atac ORELSE' rtac iffI))) THEN
TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)
end;
@@ -155,6 +165,39 @@
unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
+fun mk_rec_transfer_tac ctxt nn ns actives passives rec_defs ctor_rec_transfers rel_pre_T_defs
+ rel_eqs =
+ let
+ val ctor_rec_transfers' =
+ map (cterm_instantiate_pos (map SOME passives @ map SOME actives)) ctor_rec_transfers;
+ val ns' = Integer.sum ns;
+ in
+ HEADGOAL Goal.conjunction_tac THEN
+ EVERY (map (fn ctor_rec_transfer =>
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt rec_defs THEN
+ HEADGOAL (etac (mk_rel_funDN_rotated (nn + 1) ctor_rec_transfer)) THEN
+ unfold_thms_tac ctxt rel_pre_T_defs THEN
+ EVERY (fst (fold_map (fn k => fn acc => rpair (k + acc)
+ (HEADGOAL (rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer})) THEN
+ HEADGOAL (rtac @{thm vimage2p_rel_fun}) THEN
+ unfold_thms_tac ctxt rel_eqs THEN
+ EVERY (map (fn n =>
+ REPEAT_DETERM (HEADGOAL
+ (rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE'
+ rtac (mk_rel_funDN 2 case_sum_transfer))) THEN
+ HEADGOAL (select_prem_tac ns' (dtac asm_rl) (acc + n)) THEN
+ HEADGOAL (SELECT_GOAL (HEADGOAL
+ ((REPEAT_DETERM o (atac ORELSE'
+ rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE'
+ rtac (mk_rel_funDN 1 case_prod_transfer) ORELSE'
+ rtac rel_funI)) THEN_ALL_NEW
+ (REPEAT_ALL_NEW (dtac rel_funD) THEN_ALL_NEW atac)))))
+ (1 upto k))))
+ ns 0)))
+ ctor_rec_transfers')
+ end;
+
val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
fun mk_corec_tac corec_defs map_ident0s ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
@@ -174,6 +217,71 @@
(if is_refl disc then all_tac else HEADGOAL (rtac disc)))
(map rtac case_splits' @ [K all_tac]) corecs discs);
+fun mk_corec_transfer_tac ctxt actives passives type_definitions corec_defs dtor_corec_transfers
+ rel_pre_T_defs rel_eqs pgs pss qssss gssss =
+ let
+ val num_pgs = length pgs;
+ fun prem_no_of x = 1 + find_index (curry (op =) x) pgs;
+
+ val Inl_Inr_Pair_tac = REPEAT_DETERM o
+ (rtac (mk_rel_funDN 1 @{thm Inl_transfer}) ORELSE'
+ rtac (mk_rel_funDN 1 @{thm Inr_transfer}) ORELSE'
+ rtac (mk_rel_funDN 2 @{thm Pair_transfer}));
+
+ fun mk_unfold_If_tac total pos =
+ HEADGOAL (Inl_Inr_Pair_tac THEN'
+ rtac (mk_rel_funDN 3 @{thm If_transfer}) THEN'
+ select_prem_tac total (dtac asm_rl) pos THEN'
+ dtac rel_funD THEN' atac THEN' atac);
+
+ fun mk_unfold_Inl_Inr_Pair_tac total pos =
+ HEADGOAL (Inl_Inr_Pair_tac THEN'
+ select_prem_tac total (dtac asm_rl) pos THEN'
+ dtac rel_funD THEN' atac THEN' atac);
+
+ fun mk_unfold_arg_tac qs gs =
+ EVERY (map (mk_unfold_If_tac num_pgs o prem_no_of) qs) THEN
+ EVERY (map (mk_unfold_Inl_Inr_Pair_tac num_pgs o prem_no_of) gs);
+
+ fun mk_unfold_ctr_tac type_definition qss gss =
+ HEADGOAL (rtac (mk_rel_funDN 1 (@{thm Abs_transfer} OF
+ [type_definition, type_definition])) THEN' Inl_Inr_Pair_tac) THEN
+ (case (qss, gss) of
+ ([], []) => HEADGOAL (rtac refl)
+ | _ => EVERY (map2 mk_unfold_arg_tac qss gss));
+
+ fun mk_unfold_type_tac type_definition ps qsss gsss =
+ let
+ val p_tacs = map (mk_unfold_If_tac num_pgs o prem_no_of) ps;
+ val qg_tacs = map2 (mk_unfold_ctr_tac type_definition) qsss gsss;
+ fun mk_unfold_ty [] [qg_tac] = qg_tac
+ | mk_unfold_ty (p_tac :: p_tacs) (qg_tac :: qg_tacs) =
+ p_tac THEN qg_tac THEN mk_unfold_ty p_tacs qg_tacs
+ in
+ HEADGOAL (rtac rel_funI) THEN mk_unfold_ty p_tacs qg_tacs
+ end;
+
+ fun mk_unfold_corec_type_tac dtor_corec_transfer corec_def =
+ let
+ val active :: actives' = actives;
+ val dtor_corec_transfer' = cterm_instantiate_pos
+ (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
+ in
+ HEADGOAL Goal.conjunction_tac THEN
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt [corec_def] THEN
+ HEADGOAL (etac (mk_rel_funDN_rotated (1 + length actives) dtor_corec_transfer')) THEN
+ unfold_thms_tac ctxt (rel_pre_T_defs @ rel_eqs)
+ end;
+
+ fun mk_unfold_prop_tac dtor_corec_transfer corec_def =
+ mk_unfold_corec_type_tac dtor_corec_transfer corec_def THEN
+ EVERY (map4 mk_unfold_type_tac type_definitions pss qssss gssss);
+ in
+ HEADGOAL Goal.conjunction_tac THEN
+ EVERY (map2 mk_unfold_prop_tac dtor_corec_transfers corec_defs)
+ end;
+
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 25 17:07:44 2014 +0200
@@ -477,7 +477,8 @@
xtor_co_rec_thms = xtor_co_rec_thms,
xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
- dtor_set_induct_thms = []}
+ dtor_set_induct_thms = [],
+ xtor_co_rec_transfer_thms = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
(fp_res, lthy)
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 17:07:44 2014 +0200
@@ -27,7 +27,8 @@
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
- dtor_set_induct_thms: thm list}
+ dtor_set_induct_thms: thm list,
+ xtor_co_rec_transfer_thms: thm list}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -62,6 +63,7 @@
val ctor_map_uniqueN: string
val ctor_recN: string
val ctor_rec_o_mapN: string
+ val ctor_rec_transferN: string
val ctor_rec_uniqueN: string
val ctor_relN: string
val ctor_rel_inductN: string
@@ -71,6 +73,7 @@
val dtor_coinductN: string
val dtor_corecN: string
val dtor_corec_o_mapN: string
+ val dtor_corec_transferN: string
val dtor_corec_uniqueN: string
val dtor_ctorN: string
val dtor_exhaustN: string
@@ -138,6 +141,8 @@
val mk_proj: typ -> int -> int -> term
val mk_convol: term * term -> term
+ val mk_rel_prod: term -> term -> term
+ val mk_rel_sum: term -> term -> term
val Inl_const: typ -> typ -> term
val Inr_const: typ -> typ -> term
@@ -174,9 +179,9 @@
val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
term list -> term list -> term list -> term list -> term list ->
({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
- val mk_un_fold_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
- term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) ->
- Proof.context -> thm list
+ val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
+ term list -> term list -> term list -> term list ->
+ ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
thm list -> thm list -> thm list
@@ -214,11 +219,13 @@
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
- dtor_set_induct_thms: thm list};
+ dtor_set_induct_thms: thm list,
+ xtor_co_rec_transfer_thms: thm list};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
- xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} =
+ xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
+ dtor_set_induct_thms, xtor_co_rec_transfer_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -235,7 +242,8 @@
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
- dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
+ dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
+ xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
@@ -292,9 +300,11 @@
val corecN = coN ^ recN
val ctor_recN = ctorN ^ "_" ^ recN
val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN
+val ctor_rec_transferN = ctor_recN ^ transferN
val ctor_rec_uniqueN = ctor_recN ^ uniqueN
val dtor_corecN = dtorN ^ "_" ^ corecN
val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN
+val dtor_corec_transferN = dtor_corecN ^ transferN
val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
val ctor_dtorN = ctorN ^ "_" ^ dtorN
@@ -376,6 +386,20 @@
val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
in Const (@{const_name convol}, convolT) $ f $ g end;
+fun mk_rel_prod R S =
+ let
+ val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
+ val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
+ val rel_prodT = RT --> ST --> mk_pred2T (HOLogic.mk_prodT (A1, B1)) (HOLogic.mk_prodT (A2, B2));
+ in Const (@{const_name rel_prod}, rel_prodT) $ R $ S end;
+
+fun mk_rel_sum R S =
+ let
+ val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
+ val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
+ val rel_sumT = RT --> ST --> mk_pred2T (mk_sumT (A1, B1)) (mk_sumT (A2, B2));
+ in Const (@{const_name rel_sum}, rel_sumT) $ R $ S end;
+
fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
@@ -498,18 +522,18 @@
|> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
end;
-fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy =
+fun mk_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
let
- val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
+ val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels;
val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
fun flip f x y = if fp = Greatest_FP then f y x else f x y;
- val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_phis;
+ val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis;
fun mk_transfer relphi pre_phi un_fold un_fold' =
fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
- val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
+ val transfers = map4 mk_transfer relphis pre_ophis un_folds un_folds';
- val goal = fold_rev Logic.all (phis @ pre_phis)
+ val goal = fold_rev Logic.all (phis @ pre_ophis)
(HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
in
Goal.prove_sorry lthy [] [] goal tac
@@ -607,7 +631,7 @@
val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
- val Dss = map3 (append oo map o nth) livess kill_poss deadss;
+ val Dss = map3 (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
fun pre_qualify b = Binding.qualify false (Binding.name_of b)
#> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 25 17:07:44 2014 +0200
@@ -1541,6 +1541,14 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val corecs = map (Morphism.term phi) corec_frees;
val corec_names = map (fst o dest_Const) corecs;
+ fun mk_corecs Ts passives actives =
+ let val Tactives = map2 (curry mk_sumT) Ts actives;
+ in
+ map3 (fn name => fn T => fn active =>
+ Const (name, Library.foldr (op -->)
+ (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
+ corec_names Ts actives
+ end;
fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
val corec_defs = map (fn def =>
@@ -2474,16 +2482,28 @@
sym_map_comps map_cong0s;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+ val Jrels = if m = 0 then map HOLogic.eq_const Ts
+ else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
val dtor_unfold_transfer_thms =
- mk_un_fold_transfer_thms Greatest_FP rels activephis
- (if m = 0 then map HOLogic.eq_const Ts
- else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
+ mk_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis
(mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
(fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
(map map_transfer_of_bnf bnfs) dtor_unfold_thms)
lthy;
+ val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs;
+ val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs;
+ val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs;
+ val corec_activephis =
+ map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
+ val dtor_corec_transfer_thms =
+ mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
+ (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
+ (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
+ dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
+ lthy;
+
val timer = time (timer "relator coinduction");
val common_notes =
@@ -2498,6 +2518,7 @@
(ctor_exhaustN, ctor_exhaust_thms),
(ctor_injectN, ctor_inject_thms),
(dtor_corecN, dtor_corec_thms),
+ (dtor_corec_transferN, dtor_corec_transfer_thms),
(dtor_ctorN, dtor_ctor_thms),
(dtor_exhaustN, dtor_exhaust_thms),
(dtor_injectN, dtor_inject_thms),
@@ -2521,7 +2542,8 @@
xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
- dtor_set_induct_thms = dtor_Jset_induct_thms};
+ dtor_set_induct_thms = dtor_Jset_induct_thms,
+ xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Sep 25 17:07:44 2014 +0200
@@ -28,6 +28,8 @@
val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
+ val mk_dtor_corec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
+ thm list -> tactic
val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
@@ -609,7 +611,7 @@
EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI,
rtac trans, rtac @{thm Shift_def},
- rtac equalityI, rtac subsetI, etac thin_rl,
+ rtac equalityI, rtac subsetI, etac thin_rl,
REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
@@ -926,7 +928,24 @@
unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
ALLGOALS (TRY o
- FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
+ FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]);
+
+fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers
+ dtor_rels =
+ CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
+ HEADGOAL (rtac (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN'
+ EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
+ etac (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
+ rtac (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
+ rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+ REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
+ REPEAT_DETERM_N n o rtac @{thm Inl_transfer} THEN'
+ rtac rel_funI THEN'
+ etac (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
+ etac (mk_rel_funDN 1 @{thm Inr_transfer})))
+ (dtor_corec_defs ~~ dtor_unfold_transfer);
fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
@@ -991,7 +1010,7 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
-fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
+fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
dtor_unfolds dtor_maps in_rels =
let
val n = length ks;
@@ -1088,7 +1107,7 @@
EVERY' (map (fn map_transfer => EVERY'
[REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt unfolds),
- rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
+ rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
REPEAT_DETERM_N m o rtac @{thm id_transfer},
REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
etac @{thm predicate2D}, etac @{thm image2pI}])
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 17:07:44 2014 +0200
@@ -1154,6 +1154,14 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val recs = map (Morphism.term phi) rec_frees;
val rec_names = map (fst o dest_Const) recs;
+ fun mk_recs Ts passives actives =
+ let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives;
+ in
+ map3 (fn name => fn T => fn active =>
+ Const (name, Library.foldr (op -->)
+ (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
+ rec_names Ts actives
+ end;
fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
val rec_defs = map (fn def =>
@@ -1764,18 +1772,31 @@
val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
val ctor_fold_transfer_thms =
- mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
+ mk_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
(mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
(fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
(map map_transfer_of_bnf bnfs) ctor_fold_thms)
lthy;
+ val rec_allAs = passiveAs @ map2 (curry HOLogic.mk_prodT) Ts activeAs;
+ val rec_allBs = passiveBs @ map2 (curry HOLogic.mk_prodT) Ts' activeBs;
+ val rec_rels = map2 (fn Ds => mk_rel_of_bnf Ds rec_allAs rec_allBs) Dss bnfs;
+ val rec_activephis =
+ map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis;
+ val ctor_rec_transfer_thms =
+ mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
+ (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
+ (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs
+ ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)
+ lthy;
+
val timer = time (timer "relator induction");
val common_notes =
[(ctor_inductN, [ctor_induct_thm]),
(ctor_induct2N, [ctor_induct2_thm]),
(ctor_fold_transferN, ctor_fold_transfer_thms),
+ (ctor_rec_transferN, ctor_rec_transfer_thms),
(ctor_rel_inductN, [Irel_induct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
@@ -1808,7 +1829,7 @@
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
- dtor_set_induct_thms = []};
+ dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 25 17:07:44 2014 +0200
@@ -47,7 +47,8 @@
xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
xtor_co_rec_o_map_thms = [ctor_rec_o_map],
rel_xtor_co_induct_thm = xtor_rel_induct,
- dtor_set_induct_thms = []};
+ dtor_set_induct_thms = [],
+ xtor_co_rec_transfer_thms = []};
fun fp_sugar_of_sum ctxt =
let
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 17:07:44 2014 +0200
@@ -22,6 +22,8 @@
val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
thm list -> tactic
val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
+ val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
+ thm list -> tactic
val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
@@ -701,6 +703,23 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
+fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
+ ctor_rels =
+ CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
+ HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
+ etac (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN'
+ EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
+ etac (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
+ rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
+ rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+ REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
+ REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
+ rtac rel_funI THEN'
+ etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
+ (ctor_rec_defs ~~ ctor_fold_transfers);
+
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
let val n = length ks;
in
@@ -729,7 +748,7 @@
[REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
SELECT_GOAL (unfold_thms_tac ctxt folds),
etac @{thm predicate2D_vimage2p},
- rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
+ rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
REPEAT_DETERM_N m o rtac @{thm id_transfer},
REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
atac])
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 25 17:07:44 2014 +0200
@@ -35,11 +35,11 @@
'o) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
- val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
'o -> 'p) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
- val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
'o -> 'p -> 'q) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
@@ -116,13 +116,6 @@
val mk_nthN: int -> term -> int -> term
(*parameterized thms*)
- val mk_Un_upper: int -> int -> thm
- val mk_conjIN: int -> thm
- val mk_nthI: int -> int -> thm
- val mk_nth_conv: int -> int -> thm
- val mk_ordLeq_csum: int -> int -> thm -> thm
- val mk_UnIN: int -> int -> thm
-
val eqTrueI: thm
val eqFalseI: thm
val prod_injectD: thm
@@ -132,11 +125,22 @@
val meta_mp: thm
val meta_spec: thm
val o_apply: thm
+ val rel_funD: thm
+ val rel_funI: thm
val set_mp: thm
val set_rev_mp: thm
val subset_UNIV: thm
+
+ val mk_conjIN: int -> thm
+ val mk_nthI: int -> int -> thm
+ val mk_nth_conv: int -> int -> thm
+ val mk_ordLeq_csum: int -> int -> thm -> thm
+ val mk_rel_funDN: int -> thm -> thm
+ val mk_rel_funDN_rotated: int -> thm -> thm
val mk_sym: thm -> thm
val mk_trans: thm -> thm -> thm
+ val mk_UnIN: int -> int -> thm
+ val mk_Un_upper: int -> int -> thm
val is_refl_bool: term -> bool
val is_refl: thm -> bool
@@ -528,6 +532,8 @@
val meta_mp = @{thm meta_mp};
val meta_spec = @{thm meta_spec};
val o_apply = @{thm o_apply};
+val rel_funD = @{thm rel_funD};
+val rel_funI = @{thm rel_funI};
val set_mp = @{thm set_mp};
val set_rev_mp = @{thm set_rev_mp};
val subset_UNIV = @{thm subset_UNIV};
@@ -560,6 +566,10 @@
| mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
[mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
+fun mk_rel_funDN n = funpow n (fn thm => thm RS @{thm rel_funD});
+
+val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN;
+
local
fun mk_Un_upper' 0 = subset_refl
| mk_Un_upper' 1 = @{thm Un_upper1}
--- a/src/HOL/Transfer.thy Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Transfer.thy Thu Sep 25 17:07:44 2014 +0200
@@ -449,8 +449,7 @@
shows "((A ===> op =) ===> op =) Ex Ex"
using assms unfolding bi_total_def rel_fun_def by fast
-lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
- unfolding rel_fun_def by simp
+declare If_transfer [transfer_rule]
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
unfolding rel_fun_def by simp
@@ -458,9 +457,7 @@
lemma id_transfer [transfer_rule]: "(A ===> A) id id"
unfolding rel_fun_def by simp
-lemma comp_transfer [transfer_rule]:
- "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
- unfolding rel_fun_def by simp
+declare comp_transfer [transfer_rule]
lemma fun_upd_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
--- a/src/Pure/Proof/extraction.ML Thu Sep 25 15:01:42 2014 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Sep 25 17:07:44 2014 +0200
@@ -478,7 +478,7 @@
val dummyt = Const ("dummy", dummyT);
-fun extract thms thy =
+fun extract thm_vss thy =
let
val thy' = add_syntax thy;
val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
@@ -769,7 +769,7 @@
| extr d vs ts Ts hs _ defs = error "extr: bad proof";
- fun prep_thm (thm, vs) =
+ fun prep_thm vs thm =
let
val thy = Thm.theory_of_thm thm;
val prop = Thm.prop_of thm;
@@ -778,11 +778,11 @@
val _ = name <> "" orelse error "extraction: unnamed theorem";
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
quote name ^ " has no computational content")
- in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
+ in Reconstruct.reconstruct_proof thy prop prf end;
val defs =
- fold (fn (prf, vs) => snd o extr 0 vs [] [] [] prf)
- (map prep_thm thms) [];
+ fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
+ thm_vss [];
fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
(case Sign.const_type thy (extr_name s vs) of