# HG changeset patch
# User paulson
# Date 1306754404 -3600
# Node ID 2a1b01680505ae028b3d0e5e00e59b203ee1afd5
# Parent  c46107e6714bf7a88e44d2a87b08f870767143ad# Parent  5945375700aa6d7dbb75970f0769a2e6b78314fa
merged multiple heads

diff -r c46107e6714b -r 2a1b01680505 doc-src/Functions/Thy/Functions.thy
--- a/doc-src/Functions/Thy/Functions.thy	Mon May 30 12:15:17 2011 +0100
+++ b/doc-src/Functions/Thy/Functions.thy	Mon May 30 12:20:04 2011 +0100
@@ -558,6 +558,7 @@
 *}
 
 by auto
+termination by (relation "{}") simp
 
 
 subsection {* Non-constructor patterns *}
@@ -685,6 +686,7 @@
   "check (''good'') = True"
 | "s \<noteq> ''good'' \<Longrightarrow> check s = False"
 by auto
+termination by (relation "{}") simp
 
 
 section {* Partiality *}
diff -r c46107e6714b -r 2a1b01680505 doc-src/Functions/Thy/document/Functions.tex
--- a/doc-src/Functions/Thy/document/Functions.tex	Mon May 30 12:15:17 2011 +0100
+++ b/doc-src/Functions/Thy/document/Functions.tex	Mon May 30 12:20:04 2011 +0100
@@ -803,6 +803,22 @@
 \isadelimproof
 %
 \endisadelimproof
+\isanewline
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}relation\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
 %
 \isamarkupsubsection{Non-constructor patterns%
 }
@@ -1039,6 +1055,22 @@
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}relation\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
 %
 \endisadelimproof
 %
diff -r c46107e6714b -r 2a1b01680505 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon May 30 12:15:17 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon May 30 12:20:04 2011 +0100
@@ -189,7 +189,7 @@
   let
     val ctxt = Proof.context_of state
     val reserved = reserved_isar_keyword_table ()
-    val chained_ths = #facts (Proof.goal state)
+    val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
     val facts =
       refs
       |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths)
diff -r c46107e6714b -r 2a1b01680505 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 30 12:15:17 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 30 12:20:04 2011 +0100
@@ -399,19 +399,22 @@
 
 fun filter_used_facts used = filter (member (op =) used o fst)
 
-fun preplay_one_line_proof debug timeout ths state i reconstructor =
+fun preplay_one_line_proof debug timeout ths state i reconstructors =
   let
-    fun preplay reconstructor =
-      let val timer = Timer.startRealTimer () in
-        case timed_reconstructor reconstructor debug timeout ths state i of
-          SOME (SOME _) => Preplayed (reconstructor, Timer.checkRealTimer timer)
-        | _ =>
-          if reconstructor = Metis then preplay MetisFT else Failed_to_Preplay
-      end
-      handle TimeLimit.TimeOut => Trust_Playable (reconstructor, SOME timeout)
+    fun preplay [] [] = Failed_to_Preplay
+      | preplay (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
+      | preplay timed_out (reconstructor :: reconstructors) =
+        let val timer = Timer.startRealTimer () in
+          case timed_reconstructor reconstructor debug timeout ths state i of
+            SOME (SOME _) =>
+            Preplayed (reconstructor, Timer.checkRealTimer timer)
+          | _ => preplay timed_out reconstructors
+        end
+        handle TimeLimit.TimeOut =>
+               preplay (reconstructor :: timed_out) reconstructors
   in
-    if timeout = Time.zeroTime then Trust_Playable (reconstructor, NONE)
-    else preplay reconstructor
+    if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE)
+    else preplay [] reconstructors
   end
 
 
@@ -590,7 +593,8 @@
                   length facts |> is_none max_relevant
                                   ? Integer.min best_max_relevant
                 val (format, type_sys) =
-                  determine_format_and_type_sys best_type_systems formats type_sys
+                  determine_format_and_type_sys best_type_systems formats
+                                                type_sys
                 val fairly_sound = is_type_sys_fairly_sound type_sys
                 val facts =
                   facts |> not fairly_sound
@@ -751,16 +755,16 @@
           val used_facts =
             used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
                                     atp_proof
-          val reconstructor =
-            if uses_typed_helpers typed_helpers atp_proof then MetisFT
-            else Metis
+          val reconstructors =
+            if uses_typed_helpers typed_helpers atp_proof then [MetisFT, Metis]
+            else [Metis, MetisFT]
           val used_ths =
             facts |> map untranslated_fact
                   |> filter_used_facts used_facts
                   |> map snd
           val preplay =
             preplay_one_line_proof debug preplay_timeout used_ths state subgoal
-                                   reconstructor
+                                   reconstructors
           val full_types = uses_typed_helpers typed_helpers atp_proof
           val isar_params =
             (debug, full_types, isar_shrink_factor, type_sys, pool,
@@ -950,7 +954,7 @@
             else "smt_solver = " ^ maybe_quote name
           val preplay =
             case preplay_one_line_proof debug preplay_timeout used_ths state
-                                        subgoal Metis of
+                                        subgoal [Metis, MetisFT] of
               p as Preplayed _ => p
             | _ => Trust_Playable (SMT (smt_settings ()), NONE)
           val one_line_params =
diff -r c46107e6714b -r 2a1b01680505 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 30 12:15:17 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 30 12:20:04 2011 +0100
@@ -146,7 +146,7 @@
                       reraise exn
                     else
                       (unknownN, "Internal error:\n" ^
-                                ML_Compiler.exn_message exn ^ "\n"))
+                                 ML_Compiler.exn_message exn ^ "\n"))
         val _ =
           (* The "expect" argument is deliberately ignored if the prover is
              missing so that the "Metis_Examples" can be processed on any
@@ -183,7 +183,7 @@
       end
     else
       (Async_Manager.launch das_tool birth_time death_time (desc ())
-                            (apfst (curry (op <>) timeoutN) o go);
+                            (apfst (curry (op =) someN) o go);
        (unknownN, state))
   end
 
@@ -191,7 +191,8 @@
   ctxt |> select_smt_solver name
        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
 
-(* Makes backtraces more transparent and might be more efficient as well. *)
+(* Makes backtraces more transparent and might well be more efficient as
+   well. *)
 fun smart_par_list_map _ [] = []
   | smart_par_list_map f [x] = [f x]
   | smart_par_list_map f xs = Par_List.map f xs
@@ -217,6 +218,7 @@
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val {facts = chained_ths, goal, ...} = Proof.goal state
+      val chained_ths = chained_ths |> normalize_chained_theorems
       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
@@ -318,7 +320,7 @@
       val launch_ueq_atps =
         launch_atps "Unit equational provers" is_unit_equality ueq_atps
       fun launch_atps_and_smt_solvers () =
-        [launch_full_atps, launch_ueq_atps, launch_smts]
+        [launch_full_atps, launch_smts, launch_ueq_atps]
         |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
         handle ERROR msg => (print ("Error: " ^ msg); error msg)
       fun maybe f (accum as (outcome_code, _)) =
diff -r c46107e6714b -r 2a1b01680505 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon May 30 12:15:17 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon May 30 12:20:04 2011 +0100
@@ -31,6 +31,7 @@
   val subgoal_count : Proof.state -> int
   val strip_subgoal :
     Proof.context -> thm -> int -> (string * typ) list * term list * term
+  val normalize_chained_theorems : thm list -> thm list
   val reserved_isar_keyword_table : unit -> unit Symtab.table
 end;
 
@@ -253,6 +254,8 @@
     val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
   in (rev params, hyp_ts, concl_t) end
 
+val normalize_chained_theorems =
+  maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
 fun reserved_isar_keyword_table () =
   union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
   |> map (rpair ()) |> Symtab.make
diff -r c46107e6714b -r 2a1b01680505 src/HOL/Tools/monomorph.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/monomorph.ML	Mon May 30 12:20:04 2011 +0100
@@ -0,0 +1,334 @@
+(*  Title:      HOL/Tools/SMT/monomorph.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Monomorphization of theorems, i.e., computation of all (necessary)
+instances.  This procedure is incomplete in general, but works well for
+most practical problems.
+
+For a list of universally closed theorems (without schematic term
+variables), monomorphization computes a list of theorems with schematic
+term variables: all polymorphic constants (i.e., constants occurring both
+with ground types and schematic type variables) are instantiated with all
+(necessary) ground types; thereby theorems containing these constants are
+copied.  To prevent nontermination, there is an upper limit for the number
+of iterations involved in the fixpoint construction.
+
+The search for instances is performed on the constants with schematic
+types, which are extracted from the initial set of theorems.  The search
+constructs, for each theorem with those constants, a set of substitutions,
+which, in the end, is applied to all corresponding theorems.  Remaining
+schematic type variables are substituted with fresh types.
+
+Searching for necessary substitutions is an iterative fixpoint
+construction: each iteration computes all required instances required by
+the ground instances computed in the previous step and which haven't been
+found before.  Computed substitutions are always nontrivial: schematic type
+variables are never mapped to schematic type variables.
+*)
+
+signature MONOMORPH =
+sig
+  (* utility function *)
+  val typ_has_tvars: typ -> bool
+  val all_schematic_consts_of: term -> typ list Symtab.table
+  val add_schematic_consts_of: term -> typ list Symtab.table ->
+    typ list Symtab.table
+
+  (* configuration options *)
+  val max_rounds: int Config.T
+  val max_new_instances: int Config.T
+  val complete_instances: bool Config.T
+  val verbose: bool Config.T
+
+  (* monomorphization *)
+  val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
+    Proof.context -> (int * thm) list list * Proof.context
+end
+
+structure Monomorph: MONOMORPH =
+struct
+
+(* utility functions *)
+
+fun fold_env _ [] y = y
+  | fold_env f (x :: xs) y = fold_env f xs (f xs x y)
+
+val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
+
+fun add_schematic_const (c as (_, T)) =
+  if typ_has_tvars T then Symtab.insert_list (op =) c else I
+
+fun add_schematic_consts_of t =
+  Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
+
+fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
+
+
+
+(* configuration options *)
+
+val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
+val max_new_instances =
+  Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
+val complete_instances =
+  Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true)
+val verbose = Attrib.setup_config_bool @{binding monomorph_verbose} (K true)
+
+fun show_info ctxt msg = if Config.get ctxt verbose then tracing msg else ()
+
+
+
+(* monomorphization *)
+
+(** preparing the problem **)
+
+datatype thm_info =
+  Ground of thm |
+  Schematic of {
+    index: int,
+    theorem: thm,
+    tvars: (indexname * sort) list,
+    schematics: typ list Symtab.table,
+    initial_round: int }
+
+fun make_thm_info index initial_round schematics thm =
+  if Symtab.is_empty schematics then Ground thm
+  else Schematic {
+    index = index,
+    theorem = thm,
+    tvars = Term.add_tvars (Thm.prop_of thm) [],
+    schematics = schematics,
+    initial_round = initial_round }
+
+fun prepare schematic_consts_of rthms =
+  let
+    val empty_subst = ((0, false, false), Vartab.empty)
+
+    fun prep (r, thm) ((i, idx), (consts, substs)) =
+      let
+        (* increase indices to avoid clashes of type variables *)
+        val thm' = Thm.incr_indexes idx thm
+        val idx' = Thm.maxidx_of thm' + 1
+        val schematics = schematic_consts_of (Thm.prop_of thm')
+        val consts' =
+          Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
+        val substs' = Inttab.update (i, [empty_subst]) substs
+      in
+        (make_thm_info i r schematics thm', ((i+1, idx'), (consts', substs')))
+      end
+  in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
+
+
+
+(** collecting substitutions **)
+
+fun add_relevant_instances known_grounds (Const (c as (n, T))) =
+      if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
+      else if member (op =) (Symtab.lookup_list known_grounds n) T then I
+      else Symtab.insert_list (op =) c
+  | add_relevant_instances _ _ = I
+
+fun collect_instances known_grounds thm =
+  Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
+
+
+fun exceeded_limit (limit, _, _) = (limit <= 0)
+
+fun with_substs index f (limit, substitutions, next_grounds) =
+  let
+    val substs = Inttab.lookup_list substitutions index
+    val (limit', substs', next_grounds') = f (limit, substs, next_grounds)
+  in (limit', Inttab.update (index, substs') substitutions, next_grounds') end
+
+fun with_grounds grounds f cx =
+  if exceeded_limit cx then cx else Symtab.fold f grounds cx
+
+fun with_all_combinations schematics f (n, Ts) cx =
+  if exceeded_limit cx then cx
+  else fold_product f (Symtab.lookup_list schematics n) Ts cx
+
+fun with_partial_substs f T U (cx as (limit, substs, next_grounds)) =
+  if exceeded_limit cx then cx
+  else fold_env (f (T, U)) substs (limit, [], next_grounds)
+
+
+fun same_subst subst =
+  Vartab.forall (fn (n, (_, T)) => 
+    Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
+
+(* FIXME: necessary? would it have an impact?
+   comparing substitutions can be tricky ... *)
+fun known substs1 substs2 subst = false
+
+fun refine ctxt known_grounds new_grounds info =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val count_partial = Config.get ctxt complete_instances
+    val (round, index, _, tvars, schematics) = info
+
+    fun refine_subst TU = try (Sign.typ_match thy TU)
+
+    fun add_new_ground subst n T =
+      let val T' = Envir.subst_type subst T
+      in
+        (* FIXME: maybe keep types in a table or net for known_grounds,
+           that might improve efficiency here
+        *)
+        if member (op =) (Symtab.lookup_list known_grounds n) T' then I
+        else Symtab.cons_list (n, T')
+      end
+
+    fun refine_step subst limit next_grounds substs =
+      let
+        val full = forall (Vartab.defined subst o fst) tvars
+        val limit' =
+          if full orelse count_partial then limit - 1 else limit
+        val sub = ((round, full, false), subst)
+        val next_grounds' =
+          (schematics, next_grounds)
+          |-> Symtab.fold (uncurry (fold o add_new_ground subst))
+      in (limit', sub :: substs, next_grounds') end
+
+    fun refine_substs TU substs sub (cx as (limit, substs', next_grounds)) =
+      let val ((generation, full, _), subst) = sub
+      in
+        if exceeded_limit cx orelse full then
+          (limit, sub :: substs', next_grounds)
+        else
+          (case refine_subst TU subst of
+            NONE => (limit, sub :: substs', next_grounds)
+          | SOME subst' =>
+              if (same_subst subst orf known substs substs') subst' then
+                (limit, sub :: substs', next_grounds)
+              else
+                substs'
+                |> cons ((generation, full, true), subst)
+                |> refine_step subst' limit next_grounds)
+      end
+  in
+    with_substs index (
+      with_grounds new_grounds (with_all_combinations schematics (
+        with_partial_substs refine_substs)))
+  end
+
+
+fun make_subst_ctxt ctxt thm_infos (known_grounds, substitutions) =
+  let
+    val limit = Config.get ctxt max_new_instances
+
+    fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
+      | add_ground_consts (Schematic _) = I
+    val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
+  in (thm_infos, (known_grounds, (limit, substitutions, initial_grounds))) end
+
+fun with_new round f thm_info =
+  (case thm_info of
+    Schematic {index, theorem, tvars, schematics, initial_round} =>
+      if initial_round <> round then I
+      else f (round, index, theorem, tvars, schematics)
+  | Ground _ => I)
+
+fun with_active round f thm_info =
+  (case thm_info of
+    Schematic {index, theorem, tvars, schematics, initial_round} =>
+      if initial_round < round then I
+      else f (round, index, theorem, tvars, schematics)
+  | Ground _ => I)
+
+fun collect_substitutions ctxt round thm_infos (known_grounds, subst_ctxt) =
+  let val (limit, substitutions, next_grounds) = subst_ctxt
+  in
+    (*
+      'known_grounds' are all constant names known to occur schematically
+      associated with all ground instances considered so far
+    *)
+    if exceeded_limit subst_ctxt then (true, (known_grounds, subst_ctxt))
+    else
+      let
+        fun collect (_, _, thm, _, _) = collect_instances known_grounds thm
+        val new = fold (with_new round collect) thm_infos next_grounds
+        val known' = Symtab.merge_list (op =) (known_grounds, new)
+      in
+        if Symtab.is_empty new then (true, (known_grounds, subst_ctxt))
+        else
+          (limit, substitutions, Symtab.empty)
+          |> fold (with_active round (refine ctxt known_grounds new)) thm_infos
+          |> fold (with_new round (refine ctxt Symtab.empty known')) thm_infos
+          |> pair false o pair known'
+      end
+  end
+
+
+
+(** instantiating schematic theorems **)
+
+fun super_sort (Ground _) S = S
+  | super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
+
+fun new_super_type ctxt thm_infos =
+  let val S = fold super_sort thm_infos @{sort type}
+  in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
+
+fun add_missing_tvar T (ix, S) subst =
+  if Vartab.defined subst ix then subst
+  else Vartab.update (ix, (S, T)) subst
+
+fun complete tvars subst T =
+  subst
+  |> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
+  |> fold (add_missing_tvar T) tvars
+
+fun instantiate_all' (mT, ctxt) substitutions thm_infos =
+  let
+    val thy = Proof_Context.theory_of ctxt
+
+    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
+    fun cert' subst = Vartab.fold (cons o cert) subst []
+    fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
+
+    fun with_subst tvars f ((generation, full, _), subst) =
+      if full then SOME (generation, f subst)
+      else Option.map (pair generation o f o complete tvars subst) mT
+
+    fun inst (Ground thm) = [(0, thm)]
+      | inst (Schematic {theorem, tvars, index, ...}) =
+          Inttab.lookup_list substitutions index
+          |> map_filter (with_subst tvars (instantiate theorem))
+  in (map inst thm_infos, ctxt) end
+
+fun instantiate_all ctxt thm_infos (_, (_, substitutions, _)) =
+  if Config.get ctxt complete_instances then
+    let
+      fun refined ((_, _, true), _) = true
+        | refined _ = false
+    in
+      (Inttab.map (K (filter_out refined)) substitutions, thm_infos)
+      |-> instantiate_all' (new_super_type ctxt thm_infos)
+    end
+  else instantiate_all' (NONE, ctxt) substitutions thm_infos
+
+
+
+(** overall procedure **)
+
+fun limit_rounds ctxt f thm_infos =
+  let
+    val max = Config.get ctxt max_rounds
+
+    fun round _ (true, x) = (thm_infos, x)
+      | round i (_, x) =
+          if i <= max then round (i + 1) (f ctxt i thm_infos x)
+          else (
+            show_info ctxt "Warning: Monomorphization limit reached";
+            (thm_infos, x))
+  in round 1 o pair false end
+
+fun monomorph schematic_consts_of rthms ctxt =
+  rthms
+  |> prepare schematic_consts_of
+  |-> make_subst_ctxt ctxt
+  |-> limit_rounds ctxt collect_substitutions
+  |-> instantiate_all ctxt
+
+end
+