merged

--- 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 *: "\<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 list_symp:
   assumes "symp R"
   shows "symp (list_all2 R)"

--- 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: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>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 \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp
 
+lemma option_left_total[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)
+
 lemma option_symp:
   "symp R \<Longrightarrow> symp (option_rel R)"
   unfolding symp_def split_option_all option_rel.simps by fast

--- 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"

--- 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 \<Longrightarrow> reflp (set_rel R)"
+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 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	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: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>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 \<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]:
+  "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)
+
 lemma sum_symp:
   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
   unfolding symp_def split_sum_all sum_rel.simps by fast

--- 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 \<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
+
+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\<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
+
+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"
 

--- 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

--- 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 *)}
 

--- 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,

--- 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 *)
 

--- 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

--- 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"}