# HG changeset patch # User wenzelm # Date 1337867678 -7200 # Node ID ca7104aebb74db57f603adfedc629315413d7c24 # Parent 22846a7cf66ee655d278449b04044b88b18a0d80# Parent c81801f881b346077482d12f69771ae796b86ed1 merged diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Library/Quotient_List.thy Thu May 24 15:54:38 2012 +0200 @@ -37,7 +37,7 @@ by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast) qed -lemma list_reflp[reflp_preserve]: +lemma list_reflp[reflexivity_rule]: assumes "reflp R" shows "reflp (list_all2 R)" proof (rule reflpI) @@ -47,6 +47,17 @@ 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 list_symp: assumes "symp R" shows "symp (list_all2 R)" diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Thu May 24 15:54:38 2012 +0200 @@ -46,10 +46,16 @@ lemma split_option_ex: "(\x. P x) \ P None \ (\x. P (Some x))" by (metis option.exhaust) (* TODO: move to Option.thy *) -lemma option_reflp[reflp_preserve]: +lemma option_reflp[reflexivity_rule]: "reflp R \ reflp (option_rel R)" unfolding reflp_def split_option_all by simp +lemma option_left_total[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) + lemma option_symp: "symp R \ symp (option_rel R)" unfolding symp_def split_option_all option_rel.simps by fast diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Thu May 24 15:54:38 2012 +0200 @@ -27,12 +27,18 @@ shows "prod_rel (op =) (op =) = (op =)" by (simp add: fun_eq_iff) -lemma prod_reflp [reflp_preserve]: +lemma prod_reflp [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]: + 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) + lemma prod_equivp [quot_equiv]: assumes "equivp R1" assumes "equivp R2" diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Thu May 24 15:54:38 2012 +0200 @@ -34,9 +34,22 @@ lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)" unfolding set_rel_def fun_eq_iff by auto -lemma reflp_set_rel[reflp_preserve]: "reflp R \ reflp (set_rel R)" +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 symp_set_rel: "symp R \ symp (set_rel R)" unfolding symp_def set_rel_def by fast diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Thu May 24 15:54:38 2012 +0200 @@ -46,10 +46,16 @@ lemma split_sum_ex: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) -lemma sum_reflp[reflp_preserve]: +lemma sum_reflp[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]: + "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) + lemma sum_symp: "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" unfolding symp_def split_sum_all sum_rel.simps by fast diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Lifting.thy Thu May 24 15:54:38 2012 +0200 @@ -121,9 +121,6 @@ lemma identity_quotient: "Quotient (op =) id id (op =)" unfolding Quotient_def by simp -lemma reflp_equality: "reflp (op =)" -by (auto intro: reflpI) - text {* TODO: Use one of these alternatives as the real definition. *} lemma Quotient_alt_def: @@ -380,6 +377,45 @@ shows "T c c'" using assms by (auto dest: Quotient_cr_rel) +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 + +lemma Quotient_to_left_total: + assumes q: "Quotient R Abs Rep T" + and r_R: "reflp R" + shows "left_total T" +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 + +lemma reflp_equality: "reflp (op =)" +by (auto intro: reflpI) + subsection {* ML setup *} use "Tools/Lifting/lifting_util.ML" @@ -388,7 +424,7 @@ setup Lifting_Info.setup declare fun_quotient[quot_map] -declare reflp_equality[reflp_preserve] +lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition use "Tools/Lifting/lifting_term.ML" diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 24 15:54:38 2012 +0200 @@ -819,19 +819,18 @@ in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end | intentionalize_def t = t -type translated_formula = +type ifact = {name : string, stature : stature, role : formula_role, iformula : (name, typ, iterm) formula, atomic_types : typ list} -fun update_iformula f ({name, stature, role, iformula, atomic_types} - : translated_formula) = +fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) = {name = name, stature = stature, role = role, iformula = f iformula, - atomic_types = atomic_types} : translated_formula + atomic_types = atomic_types} : ifact -fun fact_lift f ({iformula, ...} : translated_formula) = f iformula +fun ifact_lift f ({iformula, ...} : ifact) = f iformula fun insert_type thy get_T x xs = let val T = get_T x in @@ -1327,8 +1326,17 @@ fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (role, t)) => - t |> role = Conjecture ? s_not - |> make_formula ctxt format type_enc true name stature role) + let + val role = + if is_type_enc_higher_order type_enc andalso + role <> Conjecture andalso is_legitimate_thf_def t then + Definition + else + role + in + t |> role = Conjecture ? s_not + |> make_formula ctxt format type_enc true name stature role + end) (** Finite and infinite type inference **) @@ -1575,7 +1583,7 @@ fun add_iterm_syms conj_fact = add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true fun add_fact_syms conj_fact = - K (add_iterm_syms conj_fact) |> formula_fold NONE |> fact_lift + K (add_iterm_syms conj_fact) |> formula_fold NONE |> ifact_lift in ((false, []), Symtab.empty) |> fold (add_fact_syms true) conjs @@ -1893,29 +1901,30 @@ else error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".") -fun order_definitions facts = +val pull_and_reorder_definitions = let fun add_consts (IApp (t, u)) = fold add_consts [t, u] | add_consts (IAbs (_, t)) = add_consts t | add_consts (IConst (name, _, _)) = insert (op =) name | add_consts (IVar _) = I - fun consts_of_hs l_or_r (_, {iformula, ...} : translated_formula) = + fun consts_of_hs l_or_r ({iformula, ...} : ifact) = case iformula of AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) [] | _ => [] (* Quadratic, but usually OK. *) - fun order [] [] = [] - | order (fact :: skipped) [] = fact :: order [] skipped (* break cycle *) - | order skipped (fact :: facts) = + fun reorder [] [] = [] + | reorder (fact :: skipped) [] = + fact :: reorder [] skipped (* break cycle *) + | reorder skipped (fact :: facts) = let val rhs_consts = consts_of_hs snd fact in if exists (exists (member (op =) rhs_consts o the_single o consts_of_hs fst)) [skipped, facts] then - order (fact :: skipped) facts + reorder (fact :: skipped) facts else - fact :: order [] (facts @ skipped) + fact :: reorder [] (facts @ skipped) end - in order [] facts end + in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts = @@ -1943,15 +1952,15 @@ op @ #> preprocess_abstractions_in_terms trans_lams #>> chop (length conjs)) - val conjs = conjs |> make_conjecture ctxt format type_enc - val (fact_names, facts) = - facts - |> map_filter (fn (name, (_, t)) => - make_fact ctxt format type_enc true (name, t) - |> Option.map (pair name)) - |> List.partition (fn (_, {role, ...}) => role = Definition) - |>> order_definitions - |> op @ |> ListPair.unzip + val conjs = + conjs |> make_conjecture ctxt format type_enc + |> pull_and_reorder_definitions + val facts = + facts |> map_filter (fn (name, (_, t)) => + make_fact ctxt format type_enc true (name, t)) + |> pull_and_reorder_definitions + val fact_names = + facts |> map (fn {name, stature, ...} : ifact => (name, stature)) val lifted = lam_facts |> map (extract_lambda_def o snd o snd) val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) @@ -2157,7 +2166,7 @@ NONE, isabelle_info inductiveN helper_rank) fun formula_line_for_conjecture ctxt polym_constrs mono type_enc - ({name, role, iformula, atomic_types, ...} : translated_formula) = + ({name, role, iformula, atomic_types, ...} : ifact) = Formula (conjecture_prefix ^ name, role, iformula |> formula_from_iformula ctxt polym_constrs mono type_enc @@ -2171,7 +2180,7 @@ fun formula_line_for_free_type j phi = Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, []) -fun formula_lines_for_free_types type_enc (facts : translated_formula list) = +fun formula_lines_for_free_types type_enc (facts : ifact list) = if type_enc_needs_free_types type_enc then let val phis = @@ -2230,7 +2239,7 @@ | _ => I) #> fold add_iterm_syms args end - val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift + val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift fun add_formula_var_types (AQuant (_, xs, phi)) = fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs #> add_formula_var_types phi @@ -2239,7 +2248,7 @@ | add_formula_var_types _ = I fun var_types () = if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a] - else fold (fact_lift add_formula_var_types) (conjs @ facts) [] + else fold (ifact_lift add_formula_var_types) (conjs @ facts) [] fun add_undefined_const T = let val (s, s') = @@ -2329,8 +2338,7 @@ mono end | add_iterm_mononotonicity_info _ _ _ _ mono = mono -fun add_fact_mononotonicity_info ctxt level - ({role, iformula, ...} : translated_formula) = +fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) = formula_fold (SOME (role <> Conjecture)) (add_iterm_mononotonicity_info ctxt level) iformula fun mononotonicity_info_for_facts ctxt type_enc facts = @@ -2351,7 +2359,7 @@ and add_term tm = add_type (ityp_of tm) #> add_args tm in formula_fold NONE (K add_term) end fun add_fact_monotonic_types ctxt mono type_enc = - add_iformula_monotonic_types ctxt mono type_enc |> fact_lift + add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift fun monotonic_types_for_facts ctxt mono type_enc facts = let val level = level_of_type_enc type_enc in [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu May 24 15:54:38 2012 +0200 @@ -363,10 +363,10 @@ proof_delims = [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], known_failures = known_szs_status_failures, - prem_role = Definition (* motivated by "isabelle tptp_sledgehammer" tool *), + prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))], + K [(1.0, (true, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)} diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu May 24 15:54:38 2012 +0200 @@ -182,7 +182,7 @@ 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_reflp_preserve_rules ctxt + val rules = Lifting_Info.get_reflexivity_rules ctxt in EVERY' [CSUBGOAL intro_reflp_tac, CONVERSION conv, diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu May 24 15:54:38 2012 +0200 @@ -21,9 +21,9 @@ val get_invariant_commute_rules: Proof.context -> thm list - val get_reflp_preserve_rules: Proof.context -> thm list - val add_reflp_preserve_rule_attribute: attribute - val add_reflp_preserve_rule_attrib: Attrib.src + val get_reflexivity_rules: Proof.context -> thm list + val add_reflexivity_rule_attribute: attribute + val add_reflexivity_rule_attrib: Attrib.src val setup: theory -> theory end; @@ -183,13 +183,13 @@ structure Reflp_Preserve = Named_Thms ( - val name = @{binding reflp_preserve} + val name = @{binding reflexivity_rule} val description = "theorems that a relator preserves a reflexivity property" ) -val get_reflp_preserve_rules = Reflp_Preserve.get -val add_reflp_preserve_rule_attribute = Reflp_Preserve.add -val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute) +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) (* theory setup *) diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu May 24 15:54:38 2012 +0200 @@ -103,8 +103,10 @@ fun quot_info phi = Lifting_Info.transform_quotients phi quotients val lthy' = case maybe_reflp_thm of SOME reflp_thm => lthy - |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]), + |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]), [reflp_thm]) + |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]), + [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}]) |> define_code_constr gen_code quot_thm | NONE => lthy |> define_abs_type gen_code quot_thm diff -r c81801f881b3 -r ca7104aebb74 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Thu May 24 15:33:45 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Thu May 24 15:54:38 2012 +0200 @@ -9,11 +9,11 @@ val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory - val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * - ((binding * binding) option * bool)) list -> Proof.context -> Proof.state + val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * + ((binding * binding) option * bool) -> Proof.context -> Proof.state - val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) * - (binding * binding) option) list -> Proof.context -> Proof.state + val quotient_type_cmd: (((((bool * string list) * binding) * mixfix) * string) * (bool * string)) * + (binding * binding) option -> Proof.context -> Proof.state end; structure Quotient_Type: QUOTIENT_TYPE = @@ -290,11 +290,11 @@ relations are equivalence relations *) -fun quotient_type quot_list lthy = +fun quotient_type quot lthy = let (* sanity check *) - val _ = List.app sanity_check quot_list - val _ = List.app (map_check lthy) quot_list + val _ = sanity_check quot + val _ = map_check lthy quot fun mk_goal (rty, rel, partial) = let @@ -305,14 +305,14 @@ HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) end - val goals = map (mk_goal o #2) quot_list + val goal = (mk_goal o #2) quot - fun after_qed [thms] = fold (snd oo add_quotient_type) (quot_list ~~ thms) + fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm) in - Proof.theorem NONE after_qed [map (rpair []) goals] lthy + Proof.theorem NONE after_qed [[(goal, [])]] lthy end -fun quotient_type_cmd specs lthy = +fun quotient_type_cmd spec lthy = let fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy = let @@ -327,7 +327,7 @@ (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2) end - val (spec', _) = fold_map parse_spec specs lthy + val (spec', _) = parse_spec spec lthy in quotient_type spec' lthy end @@ -338,12 +338,11 @@ val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false val quotspec_parser = - Parse.and_list1 - ((opt_gen_code -- Parse.type_args -- Parse.binding) -- + (opt_gen_code -- Parse.type_args -- Parse.binding) -- (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |-- (partial -- Parse.term)) -- - Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))) + Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) val _ = Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"} diff -r c81801f881b3 -r ca7104aebb74 src/Pure/ML/install_pp_polyml.ML