more complete fp_sugars for sum and prod;
tuned;
removed theorem duplicates;
removed obsolete Lifting_{Option,Product,Sum} theories
--- a/src/HOL/BNF_Def.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/BNF_Def.thy Fri Nov 07 11:28:37 2014 +0100
@@ -18,13 +18,13 @@
lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
by auto
-definition
- rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+inductive
+ rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool" for R1 R2
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)"
+ "R1 a c \<Longrightarrow> rel_sum R1 R2 (Inl a) (Inl c)"
+| "R2 b d \<Longrightarrow> rel_sum R1 R2 (Inr b) (Inr d)"
+
+hide_fact rel_sum_def
definition
rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
--- a/src/HOL/BNF_Fixpoint_Base.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy Fri Nov 07 11:28:37 2014 +0100
@@ -85,7 +85,7 @@
lemma prod_set_simps:
"fsts (x, y) = {x}"
"snds (x, y) = {y}"
- unfolding fsts_def snds_def by simp+
+ unfolding prod_set_defs by simp+
lemma sum_set_simps:
"setl (Inl x) = {x}"
@@ -204,7 +204,7 @@
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)
+ unfolding rel_fun_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+
@@ -214,10 +214,7 @@
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)
+ unfolding rel_fun_def by simp
lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
by simp
@@ -246,7 +243,7 @@
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
+ unfolding rel_fun_def by simp
ML_file "Tools/BNF/bnf_fp_util.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
--- a/src/HOL/BNF_Least_Fixpoint.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy Fri Nov 07 11:28:37 2014 +0100
@@ -176,18 +176,14 @@
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
+ unfolding rel_fun_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)
+ unfolding rel_fun_def by simp
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
+ unfolding 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)
@@ -243,6 +239,4 @@
ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
ML_file "Tools/BNF/bnf_lfp_size.ML"
-hide_fact (open) id_transfer
-
end
--- a/src/HOL/Basic_BNF_Least_Fixpoints.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy Fri Nov 07 11:28:37 2014 +0100
@@ -53,6 +53,43 @@
lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
+lemma eq_fst_iff: "a = fst p \<longleftrightarrow> (\<exists>b. p = (a, b))"
+ by (cases p) auto
+
+lemma eq_snd_iff: "b = snd p \<longleftrightarrow> (\<exists>a. p = (a, b))"
+ by (cases p) auto
+
+lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
+ by default blast+
+
+lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)"
+ by default blast+
+
+lemma isl_map_sum:
+ "isl (map_sum f g s) = isl s"
+ by (cases s) simp_all
+
+lemma map_sum_sel:
+ "isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)"
+ "\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)"
+ by (case_tac [!] s) simp_all
+
+lemma set_sum_sel:
+ "isl s \<Longrightarrow> projl s \<in> setl s"
+ "\<not> isl s \<Longrightarrow> projr s \<in> setr s"
+ by (case_tac [!] s) (auto intro: setl.intros setr.intros)
+
+lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and>
+ (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and>
+ (\<not> isl a \<longrightarrow> \<not> isl b \<longrightarrow> R2 (projr a) (projr b)))"
+ by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all
+
+lemma isl_transfer: "rel_fun (rel_sum A B) (op =) isl isl"
+ unfolding rel_fun_def rel_sum_sel by simp
+
+lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))"
+ by (force simp: rel_prod.simps elim: rel_prod.cases)
+
ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
--- a/src/HOL/Basic_BNFs.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy Fri Nov 07 11:28:37 2014 +0100
@@ -13,20 +13,22 @@
imports BNF_Def
begin
-definition setl :: "'a + 'b \<Rightarrow> 'a set" where
-"setl x = (case x of Inl z => {z} | _ => {})"
+inductive_set setl :: "'a + 'b \<Rightarrow> 'a set" for s :: "'a + 'b" where
+ "s = Inl x \<Longrightarrow> x \<in> setl s"
+inductive_set setr :: "'a + 'b \<Rightarrow> 'b set" for s :: "'a + 'b" where
+ "s = Inr x \<Longrightarrow> x \<in> setr s"
-definition setr :: "'a + 'b \<Rightarrow> 'b set" where
-"setr x = (case x of Inr z => {z} | _ => {})"
+lemma sum_set_defs[code]:
+ "setl = (\<lambda>x. case x of Inl z => {z} | _ => {})"
+ "setr = (\<lambda>x. case x of Inr z => {z} | _ => {})"
+ by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits)
-lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
-
-lemma rel_sum_simps[simp]:
+lemma rel_sum_simps[code, simp]:
"rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
"rel_sum R1 R2 (Inl a1) (Inr b2) = False"
"rel_sum R1 R2 (Inr a2) (Inl b1) = False"
"rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
- unfolding rel_sum_def by simp_all
+ by (auto intro: rel_sum.intros elim: rel_sum.cases)
bnf "'a + 'b"
map: map_sum
@@ -46,18 +48,18 @@
a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
thus "map_sum f1 f2 x = map_sum g1 g2 x"
proof (cases x)
- case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
+ case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1))
next
- case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
+ case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2))
qed
next
fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
show "setl o map_sum f1 f2 = image f1 o setl"
- by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
+ by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
next
fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
show "setr o map_sum f1 f2 = image f2 o setr"
- by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
+ by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
next
show "card_order natLeq" by (rule natLeq_card_order)
next
@@ -67,42 +69,48 @@
show "|setl x| \<le>o natLeq"
apply (rule ordLess_imp_ordLeq)
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
- by (simp add: setl_def split: sum.split)
+ by (simp add: sum_set_defs(1) split: sum.split)
next
fix x :: "'o + 'p"
show "|setr x| \<le>o natLeq"
apply (rule ordLess_imp_ordLeq)
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
- by (simp add: setr_def split: sum.split)
+ by (simp add: sum_set_defs(2) split: sum.split)
next
fix R1 R2 S1 S2
show "rel_sum R1 R2 OO rel_sum S1 S2 \<le> rel_sum (R1 OO S1) (R2 OO S2)"
- by (auto simp: rel_sum_def split: sum.splits)
+ by (force elim: rel_sum.cases)
next
fix R S
show "rel_sum R S =
(Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
- unfolding setl_def setr_def rel_sum_def Grp_def relcompp.simps conversep.simps fun_eq_iff
- by (fastforce split: sum.splits)
+ unfolding sum_set_defs Grp_def relcompp.simps conversep.simps fun_eq_iff
+ by (fastforce elim: rel_sum.cases split: sum.splits)
qed (auto simp: sum_set_defs)
-definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
-"fsts x = {fst x}"
+inductive_set fsts :: "'a \<times> 'b \<Rightarrow> 'a set" for p :: "'a \<times> 'b" where
+ "fst p \<in> fsts p"
+inductive_set snds :: "'a \<times> 'b \<Rightarrow> 'b set" for p :: "'a \<times> 'b" where
+ "snd p \<in> snds p"
-definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
-"snds x = {snd x}"
-
-lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
+lemma prod_set_defs[code]: "fsts = (\<lambda>p. {fst p})" "snds = (\<lambda>p. {snd p})"
+ by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases)
-definition
- rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
+inductive
+ rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" for R1 R2
where
+ "\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
+
+hide_fact rel_prod_def
+
+lemma rel_prod_apply [code, simp]:
+ "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
+ by (auto intro: rel_prod.intros elim: rel_prod.cases)
+
+lemma rel_prod_conv:
"rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-
-lemma rel_prod_apply [simp]:
- "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
- by (simp add: rel_prod_def)
+ by (rule ext, rule ext) auto
bnf "'a \<times> 'b"
map: map_prod
@@ -147,7 +155,7 @@
show "rel_prod R S =
(Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
- unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff
+ unfolding prod_set_defs rel_prod_apply Grp_def relcompp.simps conversep.simps fun_eq_iff
by auto
qed
--- a/src/HOL/Datatype_Examples/Process.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Datatype_Examples/Process.thy Fri Nov 07 11:28:37 2014 +0100
@@ -17,15 +17,8 @@
(* Read: prefix of, continuation of, choice 1 of, choice 2 of *)
-section {* Customization *}
-
subsection {* Basic properties *}
-declare
- rel_pre_process_def[simp]
- rel_sum_def[simp]
- rel_prod_def[simp]
-
(* Constructors versus discriminators *)
theorem isAction_isChoice:
"isAction p \<or> isChoice p"
--- a/src/HOL/Library/Quotient_Option.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Library/Quotient_Option.thy Fri Nov 07 11:28:37 2014 +0100
@@ -54,12 +54,12 @@
lemma option_None_rsp [quot_respect]:
assumes q: "Quotient3 R Abs Rep"
shows "rel_option R None None"
- by (rule None_transfer)
+ by (rule option.ctr_transfer(1))
lemma option_Some_rsp [quot_respect]:
assumes q: "Quotient3 R Abs Rep"
shows "(R ===> rel_option R) Some Some"
- by (rule Some_transfer)
+ by (rule option.ctr_transfer(2))
lemma option_None_prs [quot_preserve]:
assumes q: "Quotient3 R Abs Rep"
--- a/src/HOL/Library/Quotient_Product.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Fri Nov 07 11:28:37 2014 +0100
@@ -89,7 +89,7 @@
lemma [quot_respect]:
shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
rel_prod R2 R1 ===> rel_prod R2 R1 ===> op =) rel_prod rel_prod"
- by (rule rel_prod_transfer)
+ by (rule prod.rel_transfer)
lemma [quot_preserve]:
assumes q1: "Quotient3 R1 abs1 rep1"
--- a/src/HOL/Library/Quotient_Sum.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Fri Nov 07 11:28:37 2014 +0100
@@ -12,11 +12,11 @@
lemma rel_sum_map1:
"rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
- by (simp add: rel_sum_def split: sum.split)
+ by (rule sum.rel_map(1))
lemma rel_sum_map2:
"rel_sum R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> rel_sum (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
- by (simp add: rel_sum_def split: sum.split)
+ by (rule sum.rel_map(2))
lemma map_sum_id [id_simps]:
"map_sum id id = id"
@@ -24,7 +24,7 @@
lemma rel_sum_eq [id_simps]:
"rel_sum (op =) (op =) = (op =)"
- by (simp add: rel_sum_def fun_eq_iff split: sum.split)
+ by (rule sum.rel_eq)
lemma reflp_rel_sum:
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)"
@@ -50,7 +50,7 @@
apply (simp_all add: map_sum.compositionality comp_def map_sum.identity rel_sum_eq rel_sum_map1 rel_sum_map2
Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
- apply (simp add: rel_sum_def comp_def split: sum.split)
+ apply (fastforce elim!: rel_sum.cases simp add: comp_def split: sum.split)
done
declare [[mapQ3 sum = (rel_sum, sum_quotient)]]
--- a/src/HOL/Lifting_Option.thy Fri Nov 07 12:24:56 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* Title: HOL/Lifting_Option.thy
- Author: Brian Huffman and Ondrej Kuncar
- Author: Andreas Lochbihler, Karlsruhe Institute of Technology
-*)
-
-section {* Setup for Lifting/Transfer for the option type *}
-
-theory Lifting_Option
-imports Lifting Option
-begin
-
-subsection {* Relator and predicator properties *}
-
-lemma rel_option_iff:
- "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
- | (Some x, Some y) \<Rightarrow> R x y
- | _ \<Rightarrow> False)"
-by (auto split: prod.split option.split)
-
-subsection {* Transfer rules for the Transfer package *}
-
-context
-begin
-interpretation lifting_syntax .
-
-lemma None_transfer [transfer_rule]: "(rel_option A) None None"
- by (rule option.rel_inject)
-
-lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
- unfolding rel_fun_def by simp
-
-lemma case_option_transfer [transfer_rule]:
- "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
- unfolding rel_fun_def split_option_all by simp
-
-lemma map_option_transfer [transfer_rule]:
- "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
- unfolding map_option_case[abs_def] by transfer_prover
-
-lemma option_bind_transfer [transfer_rule]:
- "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
- Option.bind Option.bind"
- unfolding rel_fun_def split_option_all by simp
-
-end
-
-end
--- a/src/HOL/Lifting_Product.thy Fri Nov 07 12:24:56 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: HOL/Lifting_Product.thy
- Author: Brian Huffman and Ondrej Kuncar
-*)
-
-section {* Setup for Lifting/Transfer for the product type *}
-
-theory Lifting_Product
-imports Lifting Basic_BNFs
-begin
-
-(* The following lemma can be deleted when product is added to FP sugar *)
-lemma prod_pred_inject [simp]:
- "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
- unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
-
-subsection {* Transfer rules for the Transfer package *}
-
-context
-begin
-interpretation lifting_syntax .
-
-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"
- unfolding curry_def by transfer_prover
-
-lemma map_prod_transfer [transfer_rule]:
- "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
- map_prod map_prod"
- unfolding map_prod_def [abs_def] by transfer_prover
-
-lemma rel_prod_transfer [transfer_rule]:
- "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
- rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
- unfolding rel_fun_def by auto
-
-end
-
-end
--- a/src/HOL/Lifting_Sum.thy Fri Nov 07 12:24:56 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(* Title: HOL/Lifting_Sum.thy
- Author: Brian Huffman and Ondrej Kuncar
-*)
-
-section {* Setup for Lifting/Transfer for the sum type *}
-
-theory Lifting_Sum
-imports Lifting Basic_BNFs
-begin
-
-(* The following lemma can be deleted when sum is added to FP sugar *)
-lemma sum_pred_inject [simp]:
- "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
- unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
-
-subsection {* Transfer rules for the Transfer package *}
-
-context
-begin
-interpretation lifting_syntax .
-
-lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
- unfolding rel_fun_def by simp
-
-lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
- unfolding rel_fun_def by simp
-
-lemma case_sum_transfer [transfer_rule]:
- "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
- unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
-
-end
-
-end
--- a/src/HOL/List.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/List.thy Fri Nov 07 11:28:37 2014 +0100
@@ -5,7 +5,7 @@
section {* The datatype of finite lists *}
theory List
-imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
+imports Sledgehammer Code_Numeral Lifting_Set
begin
datatype (set: 'a) list =
--- a/src/HOL/Main.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Main.thy Fri Nov 07 11:28:37 2014 +0100
@@ -1,8 +1,7 @@
section {* Main HOL *}
theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
- BNF_Greatest_Fixpoint
+imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint
begin
text {*
--- a/src/HOL/Option.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Option.thy Fri Nov 07 11:28:37 2014 +0100
@@ -5,7 +5,7 @@
section {* Datatype option *}
theory Option
-imports BNF_Least_Fixpoint Finite_Set
+imports Lifting Finite_Set
begin
datatype 'a option =
@@ -114,6 +114,12 @@
"case_option g h (map_option f x) = case_option g (h \<circ> f) x"
by (cases x) simp_all
+lemma rel_option_iff:
+ "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
+ | (Some x, Some y) \<Rightarrow> R x y
+ | _ \<Rightarrow> False)"
+by (auto split: prod.split option.split)
+
primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
bind_lzero: "bind None f = None" |
bind_lunit: "bind (Some x) f = f x"
@@ -192,6 +198,20 @@
hide_fact (open) bind_cong
+subsection {* Transfer rules for the Transfer package *}
+
+context
+begin
+interpretation lifting_syntax .
+
+lemma option_bind_transfer [transfer_rule]:
+ "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
+ Option.bind Option.bind"
+ unfolding rel_fun_def split_option_all by simp
+
+end
+
+
subsubsection {* Interaction with finite sets *}
lemma finite_option_UNIV [simp]:
--- a/src/HOL/Product_Type.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Product_Type.thy Fri Nov 07 11:28:37 2014 +0100
@@ -867,7 +867,7 @@
"fst (map_prod f g x) = f (fst x)"
by (cases x) simp_all
-lemma snd_prod_fun [simp]:
+lemma snd_map_prod [simp]:
"snd (map_prod f g x) = g (snd x)"
by (cases x) simp_all
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Nov 07 11:28:37 2014 +0100
@@ -81,23 +81,25 @@
{ctrXs_Tss = ctr_Tss,
ctr_defs = @{thms Inl_def_alt Inr_def_alt},
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
- ctr_transfers = [],
- case_transfers = [],
- disc_transfers = [],
+ ctr_transfers = @{thms Inl_transfer Inr_transfer},
+ case_transfers = @{thms case_sum_transfer},
+ disc_transfers = @{thms isl_transfer},
sel_transfers = []},
fp_bnf_sugar =
{map_thms = @{thms map_sum.simps},
- map_disc_iffs = [],
- map_selss = [],
+ map_disc_iffs = @{thms isl_map_sum},
+ map_selss = map single @{thms map_sum_sel},
rel_injects = @{thms rel_sum_simps(1,4)},
rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
- rel_sels = [],
- rel_intros = [],
- rel_cases = [],
- set_thms = [],
- set_selssss = [],
- set_introssss = [],
- set_cases = []},
+ rel_sels = @{thms rel_sum_sel},
+ rel_intros = @{thms rel_sum.intros},
+ rel_cases = @{thms rel_sum.cases},
+ set_thms = @{thms sum_set_simps},
+ set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]],
+ set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]],
+ [[[]], [@{thms setr.intros[OF refl]}]]],
+ set_cases = @{thms setl.cases[unfolded hypsubst_in_prems]
+ setr.cases[unfolded hypsubst_in_prems]}},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
common_co_inducts = @{thms sum.induct},
@@ -108,10 +110,10 @@
co_rec_disc_iffs = [],
co_rec_selss = [],
co_rec_codes = [],
- co_rec_transfers = [],
+ co_rec_transfers = @{thms case_sum_transfer},
co_rec_o_maps = @{thms case_sum_o_map_sum},
- common_rel_co_inducts = [],
- rel_co_inducts = [],
+ common_rel_co_inducts = @{thms rel_sum.inducts},
+ rel_co_inducts = @{thms rel_sum.induct},
common_set_inducts = [],
set_inducts = []}}
end;
@@ -147,23 +149,25 @@
{ctrXs_Tss = [ctr_Ts],
ctr_defs = @{thms Pair_def_alt},
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
- ctr_transfers = [],
- case_transfers = [],
+ ctr_transfers = @{thms Pair_transfer},
+ case_transfers = @{thms case_prod_transfer},
disc_transfers = [],
- sel_transfers = []},
+ sel_transfers = @{thms fst_transfer snd_transfer}},
fp_bnf_sugar =
{map_thms = @{thms map_prod_simp},
map_disc_iffs = [],
- map_selss = [],
+ map_selss = [@{thms fst_map_prod snd_map_prod}],
rel_injects = @{thms rel_prod_apply},
rel_distincts = [],
- rel_sels = [],
- rel_intros = [],
- rel_cases = [],
- set_thms = [],
- set_selssss = [],
- set_introssss = [],
- set_cases = []},
+ rel_sels = @{thms rel_prod_sel},
+ rel_intros = @{thms rel_prod.intros},
+ rel_cases = @{thms rel_prod.cases},
+ set_thms = @{thms prod_set_simps},
+ set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]],
+ set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]],
+ [[[], @{thms snds.intros[of "(a, b)" for a b, unfolded snd_conv]}]]],
+ set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos]
+ snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},
@@ -174,10 +178,10 @@
co_rec_disc_iffs = [],
co_rec_selss = [],
co_rec_codes = [],
- co_rec_transfers = [],
+ co_rec_transfers = @{thms case_prod_transfer},
co_rec_o_maps = @{thms case_prod_o_map_prod},
- common_rel_co_inducts = [],
- rel_co_inducts = [],
+ common_rel_co_inducts = @{thms rel_prod.inducts},
+ rel_co_inducts = @{thms rel_prod.induct},
common_set_inducts = [],
set_inducts = []}}
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Nov 07 11:28:37 2014 +0100
@@ -62,7 +62,7 @@
val rec_o_map_simps =
@{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def};
-val size_gen_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
+val size_gen_o_map_simps = @{thms prod.inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
unfold_thms_tac ctxt [size_def] THEN
--- a/src/HOL/Transfer.thy Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Transfer.thy Fri Nov 07 11:28:37 2014 +0100
@@ -6,13 +6,9 @@
section {* Generic theorem transfer using relations *}
theory Transfer
-imports Hilbert_Choice Metis Option
+imports Hilbert_Choice Metis Basic_BNF_Least_Fixpoints
begin
-(* We import Option here although it's not needed here.
- By doing this, we avoid a diamond problem for BNF and
- FP sugar interpretation defined in this file. *)
-
subsection {* Relator for function space *}
locale lifting_syntax
@@ -453,11 +449,14 @@
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
unfolding rel_fun_def by simp
-lemma id_transfer [transfer_rule]: "(A ===> A) id id"
- unfolding rel_fun_def by simp
+declare id_transfer [transfer_rule]
declare comp_transfer [transfer_rule]
+lemma curry_transfer [transfer_rule]:
+ "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
+ unfolding curry_def by transfer_prover
+
lemma fun_upd_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"