Merge pull request #191 from larsrh/topic/isabelle-2016

update to Isabelle2016

src/main/isabelle/stateful_ops.ML

@@ -486,10 +486,10 @@ fun lookup_datatype (name, raw_constructors) =
         (Codec.Left ("unknown datatype " ^ name), lthy)
     | SOME {ctrs, discs, selss, split, split_asm, case_thms, ...} =>
         let
-          val raw_constructors = sort_wrt snd (raw_constructors)
+          val raw_constructors = sort_by snd (raw_constructors)
           val (names, terms) =
             map (fst o dest_Const) ctrs ~~ (discs ~~ selss)
-            |> sort_wrt fst
+            |> sort_by fst
             |> split_list
           fun process (internal_name, name) (disc, sels) =
             (internal_name, (Const (name, dummyT), dummify_types disc, map dummify_types sels))

src/main/isabelle/tactics.ML

@@ -31,8 +31,8 @@ fun equiv_tac rule ctxt =
           |> Syntax.check_term ctxt
           |> Thm.cterm_of ctxt
 
-        val insts = [(Thm.cterm_of ctxt p, p_inst)]
-        val rule = Drule.cterm_instantiate insts rule
+        val insts = [(fst (dest_Var p), p_inst)]
+        val rule = Drule.infer_instantiate ctxt insts rule
       in ext_tac (length args) n THEN resolve_tac ctxt [rule] n end)
 
     val maybe_induct =
@@ -53,8 +53,7 @@ fun method_tac pos src = Subgoal.FOCUS (fn {context = ctxt, concl, ...} =>
       |> Scan.catch scan
     val state =
       Proof.theorem NONE (K I) [[(Thm.term_of concl, [])]] ctxt
-      |> Proof.refine m
-      |> Seq.hd
+      |> Proof.refine_singleton m
     val {goal, ...} = Proof.simple_goal state
   in
     HEADGOAL (resolve_tac ctxt [Goal.conclude goal])
@@ -64,4 +63,4 @@ fun pat_completeness_auto_tac ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
 
 fun termination_tac ctxt =
-  Function_Common.termination_prover_tac ctxt
\ No newline at end of file
+  Function_Common.termination_prover_tac true ctxt
\ No newline at end of file

src/main/isabelle/term_codec.ML

-datatype ('a, 'b) either = Left of 'a | Right of 'b
-
-structure Codec = struct
-
-open Codec
-
-fun triple a b c =
-  tuple a (tuple b c)
-  |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
-
-fun either a b =
-  let
-    fun enc (Left l)  = (0, encode a l)
-      | enc (Right r) = (1, encode b r)
-    fun dec 0 = SOME (decode a #> map_result Left)
-      | dec 1 = SOME (decode b #> map_result Right)
-      | dec _ = NONE
-  in Codec.variant enc dec "either" end
-
-end
-
-signature TERM_CODEC = sig
-  val typ : typ codec
-  val term : term codec
-end
-
-structure Term_Codec : TERM_CODEC = struct
-
-val sort : sort codec = Codec.list Codec.string
-val indexname : indexname codec = Codec.tuple Codec.string Codec.int
-
-fun typ () =
-  let
-    fun typ_type () = Codec.tuple Codec.string (Codec.list (typ ()))
-    val typ_tfree = Codec.tuple Codec.string sort
-    val typ_tvar = Codec.tuple indexname sort
-
-    fun enc (Type arg) =  (0, Codec.encode (typ_type ()) arg)
-      | enc (TFree arg) = (1, Codec.encode typ_tfree arg)
-      | enc (TVar arg) =  (2, Codec.encode typ_tvar arg)
-    fun dec 0 = SOME (Codec.decode (typ_type ()) #> Codec.map_result Type)
-      | dec 1 = SOME (Codec.decode typ_tfree #> Codec.map_result TFree)
-      | dec 2 = SOME (Codec.decode typ_tvar #> Codec.map_result TVar)
-      | dec _ = NONE
-  in Codec.variant enc dec "Pure.typ" end
-
-val typ = typ ()
-
-fun term () =
-  let
-    val term_const = Codec.tuple Codec.string typ
-    val term_free = Codec.tuple Codec.string typ
-    val term_var = Codec.tuple indexname typ
-    val term_bound = Codec.int
-    fun term_abs () = Codec.triple Codec.string typ (term ())
-    fun term_app () = Codec.tuple (term ()) (term ())
-
-    fun enc (Const arg) = (0, Codec.encode term_const arg)
-      | enc (Free arg) =  (1, Codec.encode term_free arg)
-      | enc (Var arg) =   (2, Codec.encode term_var arg)
-      | enc (Bound arg) = (3, Codec.encode term_bound arg)
-      | enc (Abs arg) =   (4, Codec.encode (term_abs ()) arg)
-      | enc (op $ arg) =  (5, Codec.encode (term_app ()) arg)
-    fun dec 0 = SOME (Codec.decode term_const #> Codec.map_result Const)
-      | dec 1 = SOME (Codec.decode term_free #> Codec.map_result Free)
-      | dec 2 = SOME (Codec.decode term_var #> Codec.map_result Var)
-      | dec 3 = SOME (Codec.decode term_bound #> Codec.map_result Bound)
-      | dec 4 = SOME (Codec.decode (term_abs ()) #> Codec.map_result Abs)
-      | dec 5 = SOME (Codec.decode (term_app ()) #> Codec.map_result op $)
-      | dec _ = NONE
-  in Codec.variant enc dec "Pure.term" end
-
-val term = term ()
-
-end
\ No newline at end of file

src/main/isabelle/util.ML

@@ -117,7 +117,7 @@ fun fold_opt _ [] y = SOME y
   | fold_opt f (x :: xs) y = Option.mapPartial (fold_opt f xs) (f x y)
 
 fun fold_res _ [] y = Exn.Res y
-  | fold_res f (x :: xs) y = Exn.maps_result (fold_res f xs) (f x y)
+  | fold_res f (x :: xs) y = Exn.maps_res (fold_res f xs) (f x y)
 
 fun map_generalized f t =
   case t of
@@ -229,7 +229,7 @@ fun homogenize_spec_types ctxt thms =
     val typ = Sign.the_const_type (Proof_Context.theory_of ctxt) head
 
     fun mk_subst (iname, (sort, inst)) =
-      (Thm.ctyp_of ctxt (TVar (iname, sort)), Thm.ctyp_of ctxt inst)
+      ((iname, sort), Thm.ctyp_of ctxt inst)
 
     fun instantiate ((_, ttyp), thm) =
       let

src/main/scala/leon/solvers/isabelle/package.scala

@@ -22,7 +22,7 @@ import shapeless.tag
 object `package` {
 
   val theory = "Leon_Runtime"
-  val isabelleVersion = "2015"
+  val isabelleVersion = "2016"
 
 
   implicit class FutureResultOps[A](val future: Future[ProverResult[A]]) extends AnyVal {