--- a/src/HOL/Library/Quotient_List.thy Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy Fri Apr 20 23:34:03 2012 +0200
@@ -207,6 +207,8 @@
shows "list_all2 R x x"
by (induct x) (auto simp add: a)
+subsection {* Setup for lifting package *}
+
lemma list_quotient:
assumes "Quotient R Abs Rep T"
shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)"
@@ -251,4 +253,13 @@
declare [[map list = (list_all2, list_quotient)]]
+lemma list_invariant_commute [invariant_commute]:
+ "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
+ apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def)
+ apply (intro allI)
+ apply (induct_tac rule: list_induct2')
+ apply simp_all
+ apply metis
+done
+
end
--- a/src/HOL/Library/Quotient_Option.thy Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Fri Apr 20 23:34:03 2012 +0200
@@ -78,7 +78,7 @@
"bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
unfolding bi_unique_def split_option_all by simp
-subsection {* Correspondence rules for transfer package *}
+subsection {* Transfer rules for transfer package *}
lemma None_transfer [transfer_rule]: "(option_rel A) None None"
by simp
@@ -92,7 +92,7 @@
lemma option_map_transfer [transfer_rule]:
"((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map"
- unfolding Option.map_def by correspondence
+ unfolding Option.map_def by transfer_prover
lemma option_bind_transfer [transfer_rule]:
"(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
@@ -110,6 +110,22 @@
declare [[map option = (option_rel, Quotient_option)]]
+fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
+where
+ "option_pred R None = True"
+| "option_pred R (Some x) = R x"
+
+lemma option_invariant_commute [invariant_commute]:
+ "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
+ apply (simp add: fun_eq_iff Lifting.invariant_def)
+ apply (intro allI)
+ apply (case_tac x rule: option.exhaust)
+ apply (case_tac xa rule: option.exhaust)
+ apply auto[2]
+ apply (case_tac xa rule: option.exhaust)
+ apply auto
+done
+
subsection {* Rules for quotient package *}
lemma option_quotient [quot_thm]:
--- a/src/HOL/Library/Quotient_Product.thy Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Fri Apr 20 23:34:03 2012 +0200
@@ -53,7 +53,7 @@
shows "bi_unique (prod_rel R1 R2)"
using assms unfolding bi_unique_def prod_rel_def by auto
-subsection {* Correspondence rules for transfer package *}
+subsection {* Transfer rules for transfer package *}
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
unfolding fun_rel_def prod_rel_def by simp
@@ -70,12 +70,12 @@
lemma curry_transfer [transfer_rule]:
"((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
- unfolding curry_def by correspondence
+ unfolding curry_def by transfer_prover
lemma map_pair_transfer [transfer_rule]:
"((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
map_pair map_pair"
- unfolding map_pair_def [abs_def] by correspondence
+ unfolding map_pair_def [abs_def] by transfer_prover
lemma prod_rel_transfer [transfer_rule]:
"((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
@@ -93,6 +93,15 @@
declare [[map prod = (prod_rel, Quotient_prod)]]
+definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
+
+lemma prod_invariant_commute [invariant_commute]:
+ "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
+ apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def)
+ apply blast
+done
+
subsection {* Rules for quotient package *}
lemma prod_quotient [quot_thm]:
--- a/src/HOL/Library/Quotient_Sum.thy Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Fri Apr 20 23:34:03 2012 +0200
@@ -78,7 +78,7 @@
"bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
using assms unfolding bi_unique_def split_sum_all by simp
-subsection {* Correspondence rules for transfer package *}
+subsection {* Transfer rules for transfer package *}
lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
unfolding fun_rel_def by simp
@@ -102,6 +102,22 @@
declare [[map sum = (sum_rel, Quotient_sum)]]
+fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+where
+ "sum_pred R1 R2 (Inl a) = R1 a"
+| "sum_pred R1 R2 (Inr a) = R2 a"
+
+lemma sum_invariant_commute [invariant_commute]:
+ "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
+ apply (simp add: fun_eq_iff Lifting.invariant_def)
+ apply (intro allI)
+ apply (case_tac x rule: sum.exhaust)
+ apply (case_tac xa rule: sum.exhaust)
+ apply auto[2]
+ apply (case_tac xa rule: sum.exhaust)
+ apply auto
+done
+
subsection {* Rules for quotient package *}
lemma sum_quotient [quot_thm]:
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Apr 20 23:34:03 2012 +0200
@@ -231,11 +231,13 @@
@{thm fun_rel_def[THEN eq_reflection]}]
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+ val invariant_commute_conv = Conv.bottom_conv
+ (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
in
case (Thm.term_of ctm) of
Const (@{const_name "fun_rel"}, _) $ _ $ _ =>
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
- | _ => Conv.all_conv ctm
+ | _ => invariant_commute_conv ctm
end
val unfold_ret_val_invs = Conv.bottom_conv
--- a/src/HOL/Tools/Lifting/lifting_info.ML Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Fri Apr 20 23:34:03 2012 +0200
@@ -19,6 +19,8 @@
val dest_quotients: Proof.context -> quotients list
val print_quotients: Proof.context -> unit
+ val get_invariant_commute_rules: Proof.context -> thm list
+
val setup: theory -> theory
end;
@@ -27,8 +29,6 @@
(** data containers **)
-(* FIXME just one data slot (record) per program unit *)
-
(* info about map- and rel-functions for a type *)
type quotmaps = {relmap: string, quot_thm: thm}
@@ -107,10 +107,19 @@
|> Pretty.writeln
end
+structure Invariant_Commute = Named_Thms
+(
+ val name = @{binding invariant_commute}
+ val description = "theorems that a relator of an invariant is an invariant of the corresponding predicate"
+)
+
+fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
+
(* theory setup *)
val setup =
quotmaps_attribute_setup
+ #> Invariant_Commute.setup
(* outer syntax commands *)
--- a/src/HOL/Tools/transfer.ML Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Tools/transfer.ML Fri Apr 20 23:34:03 2012 +0200
@@ -12,7 +12,7 @@
val transfer_add: attribute
val transfer_del: attribute
val transfer_tac: Proof.context -> int -> tactic
- val correspondence_tac: Proof.context -> int -> tactic
+ val transfer_prover_tac: Proof.context -> int -> tactic
val setup: theory -> theory
val abs_tac: int -> tactic
end
@@ -23,7 +23,7 @@
structure Data = Named_Thms
(
val name = @{binding transfer_raw}
- val description = "raw correspondence rule for transfer method"
+ val description = "raw transfer rule for transfer method"
)
structure Relator_Eq = Named_Thms
@@ -71,7 +71,7 @@
else_conv
Conv.all_conv) ct
-(* Conversion to preprocess a correspondence rule *)
+(* Conversion to preprocess a transfer rule *)
fun prep_conv ct = (
Conv.implies_conv Conv.all_conv prep_conv
else_conv
@@ -79,11 +79,11 @@
else_conv
Conv.all_conv) ct
-(* Conversion to prep a proof goal containing a correspondence rule *)
-fun correspond_conv ctxt ct = (
- Conv.forall_conv (correspond_conv o snd) ctxt
+(* Conversion to prep a proof goal containing a transfer rule *)
+fun transfer_goal_conv ctxt ct = (
+ Conv.forall_conv (transfer_goal_conv o snd) ctxt
else_conv
- Conv.implies_conv Conv.all_conv (correspond_conv ctxt)
+ Conv.implies_conv Conv.all_conv (transfer_goal_conv ctxt)
else_conv
Trueprop_conv
(Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt))
@@ -149,13 +149,13 @@
rtac @{thm _} i]
end)
-fun correspondence_tac ctxt i =
+fun transfer_prover_tac ctxt i =
let
val rules = @{thms Rel_App Rel_Abs} @ Data.get ctxt
in
EVERY
- [CONVERSION (correspond_conv ctxt) i,
- rtac @{thm correspondence_start} i,
+ [CONVERSION (transfer_goal_conv ctxt) i,
+ rtac @{thm transfer_prover_start} i,
REPEAT_ALL_NEW
(resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1),
rewrite_goal_tac @{thms App_def Abs_def} i,
@@ -172,10 +172,10 @@
fixing >> (fn vs => fn ctxt =>
SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac ctxt))
-val correspondence_method : (Proof.context -> Method.method) context_parser =
- Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))
+val transfer_prover_method : (Proof.context -> Method.method) context_parser =
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
-(* Attribute for correspondence rules *)
+(* Attribute for transfer rules *)
val prep_rule = Conv.fconv_rule prep_conv
@@ -194,10 +194,10 @@
Data.setup
#> Relator_Eq.setup
#> Attrib.setup @{binding transfer_rule} transfer_attribute
- "correspondence rule for transfer method"
+ "transfer rule for transfer method"
#> Method.setup @{binding transfer} transfer_method
"generic theorem transfer method"
- #> Method.setup @{binding correspondence} correspondence_method
- "for proving correspondence rules"
+ #> Method.setup @{binding transfer_prover} transfer_prover_method
+ "for proving transfer rules"
end
--- a/src/HOL/Transfer.thy Fri Apr 20 23:16:46 2012 +0200
+++ b/src/HOL/Transfer.thy Fri Apr 20 23:34:03 2012 +0200
@@ -81,7 +81,7 @@
lemma transfer_start': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
unfolding Rel_def by simp
-lemma correspondence_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
+lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
by simp
lemma Rel_eq_refl: "Rel (op =) x x"
@@ -217,48 +217,52 @@
by (safe, metis, fast)
-subsection {* Correspondence rules *}
+subsection {* Transfer rules *}
-lemma eq_parametric [transfer_rule]:
+lemma eq_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(A ===> A ===> op =) (op =) (op =)"
using assms unfolding bi_unique_def fun_rel_def by auto
-lemma All_parametric [transfer_rule]:
+lemma All_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> op =) All All"
using assms unfolding bi_total_def fun_rel_def by fast
-lemma Ex_parametric [transfer_rule]:
+lemma Ex_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> op =) Ex Ex"
using assms unfolding bi_total_def fun_rel_def by fast
-lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
+lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
unfolding fun_rel_def by simp
-lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
+lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
unfolding fun_rel_def by simp
-lemma id_parametric [transfer_rule]: "(A ===> A) id id"
+lemma id_transfer [transfer_rule]: "(A ===> A) id id"
unfolding fun_rel_def by simp
-lemma comp_parametric [transfer_rule]:
+lemma comp_transfer [transfer_rule]:
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
unfolding fun_rel_def by simp
-lemma fun_upd_parametric [transfer_rule]:
+lemma fun_upd_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
- unfolding fun_upd_def [abs_def] by correspondence
+ unfolding fun_upd_def [abs_def] by transfer_prover
-lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
- by auto
+lemma nat_case_transfer [transfer_rule]:
+ "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
+ unfolding fun_rel_def by (simp split: nat.split)
text {* Fallback rule for transferring universal quantifiers over
correspondence relations that are not bi-total, and do not have
custom transfer rules (e.g. relations between function types). *}
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+ by auto
+
lemma Domainp_forall_transfer [transfer_rule]:
assumes "right_total A"
shows "((A ===> op =) ===> op =)
@@ -270,8 +274,8 @@
text {* Preferred rule for transferring universal quantifiers over
bi-total correspondence relations (later rules are tried first). *}
-lemma transfer_forall_parametric [transfer_rule]:
+lemma forall_transfer [transfer_rule]:
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
- unfolding transfer_forall_def by (rule All_parametric)
+ unfolding transfer_forall_def by (rule All_transfer)
end