--- a/src/HOL/IMP/Abs_Int2_ivl.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed May 15 12:10:39 2013 +0200
@@ -63,8 +63,7 @@
definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
-lift_definition empty_ivl :: ivl is empty_rep
-by simp
+lift_definition empty_ivl :: ivl is empty_rep .
lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
by(auto simp add: is_empty_rep_def empty_rep_def)
@@ -105,8 +104,7 @@
lift_definition sup_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is sup_rep
by(auto simp: eq_ivl_iff sup_rep_def)
-lift_definition top_ivl :: ivl is "(Minf,Pinf)"
-by(auto simp: eq_ivl_def)
+lift_definition top_ivl :: ivl is "(Minf,Pinf)" .
lemma is_empty_min_max:
"\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
--- a/src/HOL/IMP/Abs_State.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy Wed May 15 12:10:39 2013 +0200
@@ -102,8 +102,7 @@
lift_definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<squnion>)"
by (simp add: eq_st_def)
-lift_definition top_st :: "'a st" is "[]"
-by(simp add: eq_st_def)
+lift_definition top_st :: "'a st" is "[]" .
instance
proof
--- a/src/HOL/Int.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Int.thy Wed May 15 12:10:39 2013 +0200
@@ -37,11 +37,9 @@
instantiation int :: comm_ring_1
begin
-lift_definition zero_int :: "int" is "(0, 0)"
- by simp
+lift_definition zero_int :: "int" is "(0, 0)" .
-lift_definition one_int :: "int" is "(1, 0)"
- by simp
+lift_definition one_int :: "int" is "(1, 0)" .
lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
is "\<lambda>(x, y) (u, v). (x + u, y + v)"
--- a/src/HOL/Library/Quotient_List.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Library/Quotient_List.thy Wed May 15 12:10:39 2013 +0200
@@ -57,7 +57,7 @@
by (auto iff: fun_eq_iff)
qed
-lemma list_reflp[reflexivity_rule]:
+lemma reflp_list_all2[reflexivity_rule]:
assumes "reflp R"
shows "reflp (list_all2 R)"
proof (rule reflpI)
@@ -67,16 +67,20 @@
by (induct xs) (simp_all add: *)
qed
-lemma list_left_total[reflexivity_rule]:
- assumes "left_total R"
- shows "left_total (list_all2 R)"
-proof (rule left_totalI)
- from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
- fix xs
- show "\<exists> ys. list_all2 R xs ys"
- by (induct xs) (simp_all add: * list_all2_Cons1)
-qed
+lemma left_total_list_all2[reflexivity_rule]:
+ "left_total R \<Longrightarrow> left_total (list_all2 R)"
+ unfolding left_total_def
+ apply safe
+ apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
+done
+lemma left_unique_list_all2 [reflexivity_rule]:
+ "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
+ unfolding left_unique_def
+ apply (subst (2) all_comm, subst (1) all_comm)
+ apply (rule allI, rename_tac zs, induct_tac zs)
+ apply (auto simp add: list_all2_Cons2)
+ done
lemma list_symp:
assumes "symp R"
@@ -102,7 +106,7 @@
lemma list_equivp [quot_equiv]:
"equivp R \<Longrightarrow> equivp (list_all2 R)"
- by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
+ by (blast intro: equivpI reflp_list_all2 list_symp list_transp elim: equivpE)
lemma right_total_list_all2 [transfer_rule]:
"right_total R \<Longrightarrow> right_total (list_all2 R)"
--- a/src/HOL/Library/Quotient_Option.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Wed May 15 12:10:39 2013 +0200
@@ -71,15 +71,17 @@
using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
by (auto iff: fun_eq_iff split: option.split)
-lemma option_reflp[reflexivity_rule]:
+lemma reflp_option_rel[reflexivity_rule]:
"reflp R \<Longrightarrow> reflp (option_rel R)"
unfolding reflp_def split_option_all by simp
-lemma option_left_total[reflexivity_rule]:
+lemma left_total_option_rel[reflexivity_rule]:
"left_total R \<Longrightarrow> left_total (option_rel R)"
- apply (intro left_totalI)
- unfolding split_option_ex
- by (case_tac x) (auto elim: left_totalE)
+ unfolding left_total_def split_option_all split_option_ex by simp
+
+lemma left_unique_option_rel [reflexivity_rule]:
+ "left_unique R \<Longrightarrow> left_unique (option_rel R)"
+ unfolding left_unique_def split_option_all by simp
lemma option_symp:
"symp R \<Longrightarrow> symp (option_rel R)"
@@ -91,7 +93,7 @@
lemma option_equivp [quot_equiv]:
"equivp R \<Longrightarrow> equivp (option_rel R)"
- by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
+ by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE)
lemma right_total_option_rel [transfer_rule]:
"right_total R \<Longrightarrow> right_total (option_rel R)"
--- a/src/HOL/Library/Quotient_Product.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Wed May 15 12:10:39 2013 +0200
@@ -50,17 +50,22 @@
shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
using assms unfolding prod_rel_def prod_pred_def by blast
-lemma prod_reflp [reflexivity_rule]:
+lemma reflp_prod_rel [reflexivity_rule]:
assumes "reflp R1"
assumes "reflp R2"
shows "reflp (prod_rel R1 R2)"
using assms by (auto intro!: reflpI elim: reflpE)
-lemma prod_left_total [reflexivity_rule]:
+lemma left_total_prod_rel [reflexivity_rule]:
assumes "left_total R1"
assumes "left_total R2"
shows "left_total (prod_rel R1 R2)"
-using assms by (auto intro!: left_totalI elim!: left_totalE)
+ using assms unfolding left_total_def prod_rel_def by auto
+
+lemma left_unique_prod_rel [reflexivity_rule]:
+ assumes "left_unique R1" and "left_unique R2"
+ shows "left_unique (prod_rel R1 R2)"
+ using assms unfolding left_unique_def prod_rel_def by auto
lemma prod_equivp [quot_equiv]:
assumes "equivp R1"
--- a/src/HOL/Library/Quotient_Set.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Wed May 15 12:10:39 2013 +0200
@@ -53,18 +53,17 @@
lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
unfolding reflp_def set_rel_def by fast
-lemma left_total_set_rel[reflexivity_rule]:
- assumes lt_R: "left_total R"
- shows "left_total (set_rel R)"
-proof -
- {
- fix A
- let ?B = "{y. \<exists>x \<in> A. R x y}"
- have "(\<forall>x\<in>A. \<exists>y\<in>?B. R x y) \<and> (\<forall>y\<in>?B. \<exists>x\<in>A. R x y)" using lt_R by(elim left_totalE) blast
- }
- then have "\<And>A. \<exists>B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y)" by blast
- then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
-qed
+lemma left_total_set_rel[reflexivity_rule]:
+ "left_total A \<Longrightarrow> left_total (set_rel A)"
+ unfolding left_total_def set_rel_def
+ apply safe
+ apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
+done
+
+lemma left_unique_set_rel[reflexivity_rule]:
+ "left_unique A \<Longrightarrow> left_unique (set_rel A)"
+ unfolding left_unique_def set_rel_def
+ by fast
lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
unfolding symp_def set_rel_def by fast
--- a/src/HOL/Library/Quotient_Sum.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Wed May 15 12:10:39 2013 +0200
@@ -73,15 +73,17 @@
using assms
by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
-lemma sum_reflp[reflexivity_rule]:
+lemma reflp_sum_rel[reflexivity_rule]:
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
unfolding reflp_def split_sum_all sum_rel.simps by fast
-lemma sum_left_total[reflexivity_rule]:
+lemma left_total_sum_rel[reflexivity_rule]:
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
- apply (intro left_totalI)
- unfolding split_sum_ex
- by (case_tac x) (auto elim: left_totalE)
+ using assms unfolding left_total_def split_sum_all split_sum_ex by simp
+
+lemma left_unique_sum_rel [reflexivity_rule]:
+ "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
+ using assms unfolding left_unique_def split_sum_all by simp
lemma sum_symp:
"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
@@ -93,7 +95,7 @@
lemma sum_equivp [quot_equiv]:
"equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
- by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
+ by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
lemma right_total_sum_rel [transfer_rule]:
"right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
--- a/src/HOL/Lifting.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Lifting.thy Wed May 15 12:10:39 2013 +0200
@@ -22,6 +22,23 @@
"(id ---> id) = id"
by (simp add: fun_eq_iff)
+subsection {* Other predicates on relations *}
+
+definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
+
+lemma left_totalI:
+ "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
+unfolding left_total_def by blast
+
+lemma left_totalE:
+ assumes "left_total R"
+ obtains "(\<And>x. \<exists>y. R x y)"
+using assms unfolding left_total_def by blast
+
+definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+
subsection {* Quotient Predicate *}
definition
@@ -190,7 +207,7 @@
assumes 1: "Quotient R1 Abs1 Rep1 T1"
assumes 2: "Quotient R2 Abs2 Rep2 T2"
shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
- using assms unfolding Quotient_alt_def4 by (auto intro!: ext)
+ using assms unfolding Quotient_alt_def4 by fastforce
lemma equivp_reflp2:
"equivp R \<Longrightarrow> reflp R"
@@ -323,6 +340,10 @@
assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
begin
+lemma typedef_left_unique: "left_unique T"
+ unfolding left_unique_def T_def
+ by (simp add: type_definition.Rep_inject [OF type])
+
lemma typedef_bi_unique: "bi_unique T"
unfolding bi_unique_def T_def
by (simp add: type_definition.Rep_inject [OF type])
@@ -352,17 +373,7 @@
text {* Proving reflexivity *}
-definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
-
-lemma left_totalI:
- "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
-unfolding left_total_def by blast
-
-lemma left_totalE:
- assumes "left_total R"
- obtains "(\<And>x. \<exists>y. R x y)"
-using assms unfolding left_total_def by blast
+definition reflp' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where "reflp' R \<equiv> reflp R"
lemma Quotient_to_left_total:
assumes q: "Quotient R Abs Rep T"
@@ -371,20 +382,30 @@
using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
lemma reflp_Quotient_composition:
- assumes lt_R1: "left_total R1"
- and r_R2: "reflp R2"
- shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)"
-using assms
-proof -
- {
- fix x
- from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast
- moreover then have "R1\<inverse>\<inverse> y x" by simp
- moreover have "R2 y y" using r_R2 by (auto elim: reflpE)
- ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto
- }
- then show ?thesis by (auto intro: reflpI)
-qed
+ assumes "left_total R"
+ assumes "reflp T"
+ shows "reflp (R OO T OO R\<inverse>\<inverse>)"
+using assms unfolding reflp_def left_total_def by fast
+
+lemma reflp_fun1:
+ assumes "is_equality R"
+ assumes "reflp' S"
+ shows "reflp (R ===> S)"
+using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
+
+lemma reflp_fun2:
+ assumes "is_equality R"
+ assumes "is_equality S"
+ shows "reflp (R ===> S)"
+using assms unfolding is_equality_def reflp_def fun_rel_def by blast
+
+lemma is_equality_Quotient_composition:
+ assumes "is_equality T"
+ assumes "left_total R"
+ assumes "left_unique R"
+ shows "is_equality (R OO T OO R\<inverse>\<inverse>)"
+using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
+by fastforce
lemma reflp_equality: "reflp (op =)"
by (auto intro: reflpI)
@@ -400,9 +421,6 @@
definition NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
"NEG A B \<equiv> B \<le> A"
-definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
-
(*
The following two rules are here because we don't have any proper
left-unique ant left-total relations. Left-unique and left-total
@@ -559,7 +577,18 @@
ML_file "Tools/Lifting/lifting_info.ML"
setup Lifting_Info.setup
-lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
+lemmas [reflexivity_rule] =
+ reflp_equality reflp_Quotient_composition is_equality_Quotient_composition
+
+text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
+ because we don't want to get reflp' variant of these theorems *}
+
+setup{*
+Context.theory_map
+ (fold
+ (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute))
+ [@{thm reflp_fun1}, @{thm reflp_fun2}])
+*}
(* setup for the function type *)
declare fun_quotient[quot_map]
@@ -572,6 +601,6 @@
ML_file "Tools/Lifting/lifting_setup.ML"
-hide_const (open) invariant POS NEG
+hide_const (open) invariant POS NEG reflp'
end
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Wed May 15 12:10:39 2013 +0200
@@ -35,8 +35,7 @@
subsection {* Lifted constant definitions *}
-lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer
- by simp
+lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer .
lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric Cons_transfer
by simp
--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed May 15 12:10:39 2013 +0200
@@ -25,6 +25,31 @@
infix 0 MRSL
+(* Reflexivity prover *)
+
+fun refl_tac ctxt =
+ let
+ fun intro_reflp_tac (ct, i) =
+ let
+ val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm reflpD}
+ val concl_pat = Drule.strip_imp_concl (cprop_of rule)
+ val insts = Thm.first_order_match (concl_pat, ct)
+ in
+ rtac (Drule.instantiate_normalize insts rule) i
+ end
+ handle Pattern.MATCH => no_tac
+
+ val rules = @{thm is_equality_eq} ::
+ ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+ in
+ EVERY' [CSUBGOAL intro_reflp_tac,
+ REPEAT_ALL_NEW (resolve_tac rules)]
+ end
+
+fun try_prove_reflexivity ctxt prop =
+ SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
+ handle ERROR _ => NONE
+
(* Generation of a transfer rule *)
fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
@@ -70,8 +95,7 @@
Drule.cterm_instantiate subst relcomppI
end
- fun zip_transfer_rules ctxt thm =
- let
+ fun zip_transfer_rules ctxt thm = let
val thy = Proof_Context.theory_of ctxt
fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
@@ -268,30 +292,6 @@
fun generate_abs_eq ctxt def_thm rsp_thm quot_thm =
let
- fun refl_tac ctxt =
- let
- fun intro_reflp_tac (t, i) =
- let
- val concl_pat = Drule.strip_imp_concl (cprop_of @{thm reflpD})
- val insts = Thm.first_order_match (concl_pat, t)
- in
- rtac (Drule.instantiate_normalize insts @{thm reflpD}) i
- end
- handle Pattern.MATCH => no_tac
-
- val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq}
- val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt
- val rules = Lifting_Info.get_reflexivity_rules ctxt
- in
- EVERY' [CSUBGOAL intro_reflp_tac,
- CONVERSION conv,
- REPEAT_ALL_NEW (resolve_tac rules)]
- end
-
- fun try_prove_prem ctxt prop =
- SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
- handle ERROR _ => NONE
-
val abs_eq_with_assms =
let
val (rty, qty) = quot_thm_rty_qty quot_thm
@@ -319,7 +319,7 @@
val prems = prems_of abs_eq_with_assms
val indexed_prems = map_index (apfst (fn x => x + 1)) prems
- val indexed_assms = map (apsnd (try_prove_prem ctxt)) indexed_prems
+ val indexed_assms = map (apsnd (try_prove_reflexivity ctxt)) indexed_prems
val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms)
val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms
in
@@ -414,7 +414,6 @@
val ((_, (_ , def_thm)), lthy') =
Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
- fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
@@ -498,49 +497,37 @@
fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy =
let
- val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy
- val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw
-
- fun try_to_prove_refl thm =
- let
- val lhs_eq =
- thm
- |> prop_of
- |> Logic.dest_implies
- |> fst
- |> strip_all_body
- |> try HOLogic.dest_Trueprop
- in
- case lhs_eq of
- SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
- | _ => NONE
- end
-
- val rsp_rel = Lifting_Term.equiv_relation lthy' (fastype_of rhs, qty)
+ val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy
+ val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
+ val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
val rty_forced = (domain_type o fastype_of) rsp_rel;
- val forced_rhs = force_rty_type lthy' rty_forced rhs;
+ val forced_rhs = force_rty_type lthy rty_forced rhs;
val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
- val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy'
- val opt_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
- val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
- val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm
- val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy')) opt_par_xthm
-
- fun after_qed thm_list lthy =
- let
- val internal_rsp_thm =
- case thm_list of
- [] => the opt_proven_rsp_thm
- | [[thm]] => Goal.prove lthy [] [] internal_rsp_tm
- (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
- in
- add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
- end
+ val opt_proven_rsp_thm = try_prove_reflexivity lthy internal_rsp_tm
+ val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
+
+ fun after_qed internal_rsp_thm lthy =
+ add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
in
case opt_proven_rsp_thm of
- SOME _ => Proof.theorem NONE after_qed [] lthy'
- | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy'
+ SOME thm => Proof.theorem NONE (K (after_qed thm)) [] lthy
+ | NONE =>
+ let
+ val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
+ val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
+ val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
+
+ fun after_qed' thm_list lthy =
+ let
+ val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm
+ (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1)
+ in
+ after_qed internal_rsp_thm lthy
+ end
+ in
+ Proof.theorem NONE after_qed' [[(readable_rsp_tm_tnames,[])]] lthy
+ end
end
fun quot_thm_err ctxt (rty, qty) pretty_msg =
--- a/src/HOL/Tools/Lifting/lifting_info.ML Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Wed May 15 12:10:39 2013 +0200
@@ -23,8 +23,8 @@
val get_invariant_commute_rules: Proof.context -> thm list
val get_reflexivity_rules: Proof.context -> thm list
+ val add_reflexivity_rule_raw_attribute: attribute
val add_reflexivity_rule_attribute: attribute
- val add_reflexivity_rule_attrib: Attrib.src
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
pos_distr_rules: thm list, neg_distr_rules: thm list}
@@ -195,15 +195,51 @@
fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
-structure Reflp_Preserve = Named_Thms
+(* info about reflexivity rules *)
+
+structure Reflexivity_Rule = Generic_Data
(
- val name = @{binding reflexivity_rule}
- val description = "theorems that a relator preserves a reflexivity property"
+ type T = thm Item_Net.T
+ val empty = Thm.full_rules
+ val extend = I
+ val merge = Item_Net.merge
)
-val get_reflexivity_rules = Reflp_Preserve.get
-val add_reflexivity_rule_attribute = Reflp_Preserve.add
-val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
+fun get_reflexivity_rules ctxt = ctxt
+ |> (Item_Net.content o Reflexivity_Rule.get o Context.Proof)
+
+(* Conversion to create a reflp' variant of a reflexivity rule *)
+fun safe_reflp_conv ct =
+ Conv.try_conv (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm reflp'_def}))) ct
+
+fun prep_reflp_conv ct = (
+ Conv.implies_conv safe_reflp_conv prep_reflp_conv
+ else_conv
+ safe_reflp_conv
+ else_conv
+ Conv.all_conv) ct
+
+fun add_reflexivity_rule_raw thm = Reflexivity_Rule.map (Item_Net.update thm)
+val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw
+
+fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>
+ add_reflexivity_rule_raw (Conv.fconv_rule prep_reflp_conv thm)
+val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
+
+
+val relfexivity_rule_setup =
+ let
+ val name = @{binding reflexivity_rule}
+ fun del_thm_raw thm = Reflexivity_Rule.map (Item_Net.remove thm)
+ fun del_thm thm = del_thm_raw thm #>
+ del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)
+ val del = Thm.declaration_attribute del_thm
+ val text = "rules that are used to prove that a relation is reflexive"
+ val content = Item_Net.content o Reflexivity_Rule.get
+ in
+ Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text
+ #> Global_Theory.add_thms_dynamic (name, content)
+ end
(* info about relator distributivity theorems *)
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
@@ -414,7 +450,7 @@
quot_map_attribute_setup
#> quot_del_attribute_setup
#> Invariant_Commute.setup
- #> Reflp_Preserve.setup
+ #> relfexivity_rule_setup
#> relator_distr_attribute_setup
(* outer syntax commands *)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed May 15 12:10:39 2013 +0200
@@ -206,11 +206,12 @@
val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
val qty_full_name = (fst o dest_Type) qtyp
fun quot_info phi = Lifting_Info.transform_quotients phi quotients
+ val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
val lthy = case opt_reflp_thm of
SOME reflp_thm => lthy
- |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
+ |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
[reflp_thm])
- |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
+ |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
|> define_code_constr gen_code quot_thm
| NONE => lthy
@@ -591,13 +592,13 @@
val qty_full_name = (fst o dest_Type) qty
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
fun qualify suffix = Binding.qualified true suffix qty_name
- val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
val opt_reflp_thm =
case typedef_set of
Const ("Orderings.top_class.top", _) =>
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
| _ => NONE
val dom_thm = get_Domainp_thm quot_thm
+ val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
fun setup_transfer_rules_nonpar lthy =
let
@@ -679,6 +680,8 @@
lthy
|> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []),
[quot_thm])
+ |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
+ [[typedef_thm, T_def] MRSL @{thm typedef_left_unique}])
|> setup_lifting_infr gen_code quot_thm opt_reflp_thm
|> setup_transfer_rules
end