# HG changeset patch # User kuncar # Date 1368612639 -7200 # Node ID 82cc2aeb7d1392d53ab4515ef282af794b8f728f # Parent ea123790121b9daca4d24e2da6a453b7737d351a stronger reflexivity prover diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/IMP/Abs_Int2_ivl.thy --- 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 \ ivl \ 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: "\ is_empty_rep (l1,h1) \ \ is_empty_rep (l2, h2) \ \ is_empty_rep (min l1 l2, max h1 h2)" diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/IMP/Abs_State.thy --- 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 \ 'a st \ 'a st" is "map2_st_rep (op \)" 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 diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Int.thy --- 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 \ int \ int" is "\(x, y) (u, v). (x + u, y + v)" diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Library/Quotient_List.thy --- 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 *: "\xs. \ys. R xs ys" by (rule left_totalE) - fix xs - show "\ 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 \ 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 \ 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 \ 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 \ right_total (list_all2 R)" diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Library/Quotient_Option.thy --- 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 \ 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 \ 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 \ left_unique (option_rel R)" + unfolding left_unique_def split_option_all by simp lemma option_symp: "symp R \ symp (option_rel R)" @@ -91,7 +93,7 @@ lemma option_equivp [quot_equiv]: "equivp R \ 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 \ right_total (option_rel R)" diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Library/Quotient_Product.thy --- 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" diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Library/Quotient_Set.thy --- 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 \ 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. \x \ A. R x y}" - have "(\x\A. \y\?B. R x y) \ (\y\?B. \x\A. R x y)" using lt_R by(elim left_totalE) blast - } - then have "\A. \B. (\x\A. \y\B. R x y) \ (\y\B. \x\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 \ left_total (set_rel A)" + unfolding left_total_def set_rel_def + apply safe + apply (rename_tac X, rule_tac x="{y. \x\X. A x y}" in exI, fast) +done + +lemma left_unique_set_rel[reflexivity_rule]: + "left_unique A \ left_unique (set_rel A)" + unfolding left_unique_def set_rel_def + by fast lemma symp_set_rel: "symp R \ symp (set_rel R)" unfolding symp_def set_rel_def by fast diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Library/Quotient_Sum.thy --- 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 \ reflp R2 \ 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 \ left_total R2 \ 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 \ left_unique R2 \ left_unique (sum_rel R1 R2)" + using assms unfolding left_unique_def split_sum_all by simp lemma sum_symp: "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" @@ -93,7 +95,7 @@ lemma sum_equivp [quot_equiv]: "equivp R1 \ equivp R2 \ 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 \ right_total R2 \ right_total (sum_rel R1 R2)" diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Lifting.thy --- 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 \ 'b \ bool) \ bool" + where "left_total R \ (\x. \y. R x y)" + +lemma left_totalI: + "(\x. \y. R x y) \ left_total R" +unfolding left_total_def by blast + +lemma left_totalE: + assumes "left_total R" + obtains "(\x. \y. R x y)" +using assms unfolding left_total_def by blast + +definition left_unique :: "('a \ 'b \ bool) \ bool" + where "left_unique R \ (\x y z. R x z \ R y z \ 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 \ Abs1) (Rep1 \ 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 \ reflp R" @@ -323,6 +340,10 @@ assumes T_def: "T \ (\(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 \ 'b \ bool) \ bool" - where "left_total R \ (\x. \y. R x y)" - -lemma left_totalI: - "(\x. \y. R x y) \ left_total R" -unfolding left_total_def by blast - -lemma left_totalE: - assumes "left_total R" - obtains "(\x. \y. R x y)" -using assms unfolding left_total_def by blast +definition reflp' :: "('a \ 'a \ bool) \ bool" where "reflp' R \ 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\\)" -using assms -proof - - { - fix x - from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast - moreover then have "R1\\ y x" by simp - moreover have "R2 y y" using r_R2 by (auto elim: reflpE) - ultimately have "(R1 OO R2 OO R1\\) 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\\)" +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\\)" +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 \ 'b \ bool) \ ('a \ 'b \ bool) \ bool" where "NEG A B \ B \ A" -definition left_unique :: "('a \ 'b \ bool) \ bool" - where "left_unique R \ (\x y z. R x z \ R y z \ 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 diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Quotient_Examples/Lift_FSet.thy --- 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 \ 'a fset \ 'a fset" is Cons parametric Cons_transfer by simp diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Tools/Lifting/lifting_def.ML --- 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 = diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Tools/Lifting/lifting_info.ML --- 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 *) diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Tools/Lifting/lifting_setup.ML --- 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