src/HOL/Matrix_LP/Compute_Oracle/compute.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 52788 da1fdbfebd39
child 58669 6bade3d91c49
permissions -rw-r--r--
more qualified names;
     1 (*  Title:      HOL/Matrix_LP/Compute_Oracle/compute.ML
     2     Author:     Steven Obua
     3 *)
     4 
     5 signature COMPUTE = sig
     6 
     7     type computer
     8     type theorem
     9     type naming = int -> string
    10 
    11     datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML
    12 
    13     (* Functions designated with a ! in front of them actually update the computer parameter *)
    14 
    15     exception Make of string
    16     val make : machine -> theory -> thm list -> computer
    17     val make_with_cache : machine -> theory -> term list -> thm list -> computer
    18     val theory_of : computer -> theory
    19     val hyps_of : computer -> term list
    20     val shyps_of : computer -> sort list
    21     (* ! *) val update : computer -> thm list -> unit
    22     (* ! *) val update_with_cache : computer -> term list -> thm list -> unit
    23     
    24     (* ! *) val set_naming : computer -> naming -> unit
    25     val naming_of : computer -> naming
    26     
    27     exception Compute of string    
    28     val simplify : computer -> theorem -> thm 
    29     val rewrite : computer -> cterm -> thm 
    30 
    31     val make_theorem : computer -> thm -> string list -> theorem
    32     (* ! *) val instantiate : computer -> (string * cterm) list -> theorem -> theorem
    33     (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem
    34     (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem
    35 
    36 end
    37 
    38 structure Compute :> COMPUTE = struct
    39 
    40 open Report;
    41 
    42 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML      
    43 
    44 (* Terms are mapped to integer codes *)
    45 structure Encode :> 
    46 sig
    47     type encoding
    48     val empty : encoding
    49     val insert : term -> encoding -> int * encoding
    50     val lookup_code : term -> encoding -> int option
    51     val lookup_term : int -> encoding -> term option
    52     val remove_code : int -> encoding -> encoding
    53     val remove_term : term -> encoding -> encoding
    54 end 
    55 = 
    56 struct
    57 
    58 type encoding = int * (int Termtab.table) * (term Inttab.table)
    59 
    60 val empty = (0, Termtab.empty, Inttab.empty)
    61 
    62 fun insert t (e as (count, term2int, int2term)) = 
    63     (case Termtab.lookup term2int t of
    64          NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
    65        | SOME code => (code, e))
    66 
    67 fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t
    68 
    69 fun lookup_term c (_, _, int2term) = Inttab.lookup int2term c
    70 
    71 fun remove_code c (e as (count, term2int, int2term)) = 
    72     (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term))
    73 
    74 fun remove_term t (e as (count, term2int, int2term)) = 
    75     (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term))
    76 
    77 end
    78 
    79 exception Make of string;
    80 exception Compute of string;
    81 
    82 local
    83     fun make_constant t encoding = 
    84         let 
    85             val (code, encoding) = Encode.insert t encoding 
    86         in 
    87             (encoding, AbstractMachine.Const code)
    88         end
    89 in
    90 
    91 fun remove_types encoding t =
    92     case t of 
    93         Var _ => make_constant t encoding
    94       | Free _ => make_constant t encoding
    95       | Const _ => make_constant t encoding
    96       | Abs (_, _, t') => 
    97         let val (encoding, t'') = remove_types encoding t' in
    98             (encoding, AbstractMachine.Abs t'')
    99         end
   100       | a $ b => 
   101         let
   102             val (encoding, a) = remove_types encoding a
   103             val (encoding, b) = remove_types encoding b
   104         in
   105             (encoding, AbstractMachine.App (a,b))
   106         end
   107       | Bound b => (encoding, AbstractMachine.Var b)
   108 end
   109     
   110 local
   111     fun type_of (Free (_, ty)) = ty
   112       | type_of (Const (_, ty)) = ty
   113       | type_of (Var (_, ty)) = ty
   114       | type_of _ = raise Fail "infer_types: type_of error"
   115 in
   116 fun infer_types naming encoding =
   117     let
   118         fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, nth bounds v)
   119           | infer_types _ bounds _ (AbstractMachine.Const code) = 
   120             let
   121                 val c = the (Encode.lookup_term code encoding)
   122             in
   123                 (c, type_of c)
   124             end
   125           | infer_types level bounds _ (AbstractMachine.App (a, b)) = 
   126             let
   127                 val (a, aty) = infer_types level bounds NONE a
   128                 val (adom, arange) =
   129                     case aty of
   130                         Type ("fun", [dom, range]) => (dom, range)
   131                       | _ => raise Fail "infer_types: function type expected"
   132                 val (b, _) = infer_types level bounds (SOME adom) b
   133             in
   134                 (a $ b, arange)
   135             end
   136           | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) =
   137             let
   138                 val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m
   139             in
   140                 (Abs (naming level, dom, m), ty)
   141             end
   142           | infer_types _ _ NONE (AbstractMachine.Abs _) =
   143               raise Fail "infer_types: cannot infer type of abstraction"
   144 
   145         fun infer ty term =
   146             let
   147                 val (term', _) = infer_types 0 [] (SOME ty) term
   148             in
   149                 term'
   150             end
   151     in
   152         infer
   153     end
   154 end
   155 
   156 datatype prog = 
   157          ProgBarras of AM_Interpreter.program 
   158        | ProgBarrasC of AM_Compiler.program
   159        | ProgHaskell of AM_GHC.program
   160        | ProgSML of AM_SML.program
   161 
   162 fun machine_of_prog (ProgBarras _) = BARRAS
   163   | machine_of_prog (ProgBarrasC _) = BARRAS_COMPILED
   164   | machine_of_prog (ProgHaskell _) = HASKELL
   165   | machine_of_prog (ProgSML _) = SML
   166 
   167 type naming = int -> string
   168 
   169 fun default_naming i = "v_" ^ string_of_int i
   170 
   171 datatype computer = Computer of
   172   (theory * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming)
   173     option Unsynchronized.ref
   174 
   175 fun theory_of (Computer (Unsynchronized.ref (SOME (thy,_,_,_,_,_,_)))) = thy
   176 fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
   177 fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
   178 fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
   179 fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
   180 fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
   181 fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
   182 fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,_,p2,p3,p4,p5,p6)))) encoding' = 
   183     (r := SOME (p1,encoding',p2,p3,p4,p5,p6))
   184 fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n
   185 fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,_)))) naming'= 
   186     (r := SOME (p1,p2,p3,p4,p5,p6,naming'))
   187 
   188 fun ref_of (Computer r) = r
   189 
   190 datatype cthm = ComputeThm of term list * sort list * term
   191 
   192 fun thm2cthm th = 
   193     let
   194         val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
   195         val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
   196     in
   197         ComputeThm (hyps, shyps, prop)
   198     end
   199 
   200 fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
   201     let
   202         fun transfer (x:thm) = Thm.transfer thy x
   203         val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
   204 
   205         fun make_pattern encoding n vars (AbstractMachine.Abs _) =
   206             raise (Make "no lambda abstractions allowed in pattern")
   207           | make_pattern encoding n vars (AbstractMachine.Var _) =
   208             raise (Make "no bound variables allowed in pattern")
   209           | make_pattern encoding n vars (AbstractMachine.Const code) =
   210             (case the (Encode.lookup_term code encoding) of
   211                  Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
   212                            handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
   213                | _ => (n, vars, AbstractMachine.PConst (code, [])))
   214           | make_pattern encoding n vars (AbstractMachine.App (a, b)) =
   215             let
   216                 val (n, vars, pa) = make_pattern encoding n vars a
   217                 val (n, vars, pb) = make_pattern encoding n vars b
   218             in
   219                 case pa of
   220                     AbstractMachine.PVar =>
   221                     raise (Make "patterns may not start with a variable")
   222                   | AbstractMachine.PConst (c, args) =>
   223                     (n, vars, AbstractMachine.PConst (c, args@[pb]))
   224             end
   225 
   226         fun thm2rule (encoding, hyptable, shyptable) th =
   227             let
   228                 val (ComputeThm (hyps, shyps, prop)) = th
   229                 val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
   230                 val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
   231                 val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
   232                 val (a, b) = Logic.dest_equals prop
   233                   handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
   234                 val a = Envir.eta_contract a
   235                 val b = Envir.eta_contract b
   236                 val prems = map Envir.eta_contract prems
   237 
   238                 val (encoding, left) = remove_types encoding a     
   239                 val (encoding, right) = remove_types encoding b  
   240                 fun remove_types_of_guard encoding g = 
   241                     (let
   242                          val (t1, t2) = Logic.dest_equals g 
   243                          val (encoding, t1) = remove_types encoding t1
   244                          val (encoding, t2) = remove_types encoding t2
   245                      in
   246                          (encoding, AbstractMachine.Guard (t1, t2))
   247                      end handle TERM _ => raise (Make "guards must be meta-level equations"))
   248                 val (encoding, prems) = fold_rev (fn p => fn (encoding, ps) => let val (e, p) = remove_types_of_guard encoding p in (e, p::ps) end) prems (encoding, [])
   249 
   250                 (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule.
   251                    As it is, all variables of the rule are schematic, and there are no schematic variables in meta-hyps, therefore
   252                    this check can be left out. *)
   253 
   254                 val (vcount, vars, pattern) = make_pattern encoding 0 Inttab.empty left
   255                 val _ = (case pattern of
   256                              AbstractMachine.PVar =>
   257                              raise (Make "patterns may not start with a variable")
   258                            | _ => ())
   259 
   260                 (* finally, provide a function for renaming the
   261                    pattern bound variables on the right hand side *)
   262 
   263                 fun rename level vars (var as AbstractMachine.Var _) = var
   264                   | rename level vars (c as AbstractMachine.Const code) =
   265                     (case Inttab.lookup vars code of 
   266                          NONE => c 
   267                        | SOME n => AbstractMachine.Var (vcount-n-1+level))
   268                   | rename level vars (AbstractMachine.App (a, b)) =
   269                     AbstractMachine.App (rename level vars a, rename level vars b)
   270                   | rename level vars (AbstractMachine.Abs m) =
   271                     AbstractMachine.Abs (rename (level+1) vars m)
   272                     
   273                 fun rename_guard (AbstractMachine.Guard (a,b)) = 
   274                     AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
   275             in
   276                 ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
   277             end
   278 
   279         val ((encoding, hyptable, shyptable), rules) =
   280           fold_rev (fn th => fn (encoding_hyptable, rules) =>
   281             let
   282               val (encoding_hyptable, rule) = thm2rule encoding_hyptable th
   283             in (encoding_hyptable, rule::rules) end)
   284           ths ((encoding, Termtab.empty, Sorttab.empty), [])
   285 
   286         fun make_cache_pattern t (encoding, cache_patterns) =
   287             let
   288                 val (encoding, a) = remove_types encoding t
   289                 val (_,_,p) = make_pattern encoding 0 Inttab.empty a
   290             in
   291                 (encoding, p::cache_patterns)
   292             end
   293         
   294         val (encoding, _) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
   295 
   296         val prog = 
   297             case machine of 
   298                 BARRAS => ProgBarras (AM_Interpreter.compile rules)
   299               | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile rules)
   300               | HASKELL => ProgHaskell (AM_GHC.compile rules)
   301               | SML => ProgSML (AM_SML.compile rules)
   302 
   303         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
   304 
   305         val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
   306 
   307     in (thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
   308 
   309 fun make_with_cache machine thy cache_patterns raw_thms =
   310   Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms)))
   311 
   312 fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms
   313 
   314 fun update_with_cache computer cache_patterns raw_thms =
   315     let 
   316         val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) 
   317                               (encoding_of computer) cache_patterns raw_thms
   318         val _ = (ref_of computer) := SOME c     
   319     in
   320         ()
   321     end
   322 
   323 fun update computer raw_thms = update_with_cache computer [] raw_thms
   324 
   325 fun runprog (ProgBarras p) = AM_Interpreter.run p
   326   | runprog (ProgBarrasC p) = AM_Compiler.run p
   327   | runprog (ProgHaskell p) = AM_GHC.run p
   328   | runprog (ProgSML p) = AM_SML.run p    
   329 
   330 (* ------------------------------------------------------------------------------------- *)
   331 (* An oracle for exporting theorems; must only be accessible from inside this structure! *)
   332 (* ------------------------------------------------------------------------------------- *)
   333 
   334 fun merge_hyps hyps1 hyps2 = 
   335 let
   336     fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab
   337 in
   338     Termtab.keys (add hyps2 (add hyps1 Termtab.empty))
   339 end
   340 
   341 fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab
   342 
   343 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
   344 
   345 val (_, export_oracle) = Context.>>> (Context.map_theory_result
   346   (Thm.add_oracle (@{binding compute}, fn (thy, hyps, shyps, prop) =>
   347     let
   348         val shyptab = add_shyps shyps Sorttab.empty
   349         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
   350         fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
   351         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
   352         val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
   353         val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
   354         val _ =
   355           if not (null shyps) then
   356             raise Compute ("dangling sort hypotheses: " ^
   357               commas (map (Syntax.string_of_sort_global thy) shyps))
   358           else ()
   359     in
   360         Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
   361     end)));
   362 
   363 fun export_thm thy hyps shyps prop =
   364     let
   365         val th = export_oracle (thy, hyps, shyps, prop)
   366         val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
   367     in
   368         fold (fn h => fn p => Thm.implies_elim p h) hyps th 
   369     end
   370         
   371 (* --------- Rewrite ----------- *)
   372 
   373 fun rewrite computer ct =
   374     let
   375         val thy = Thm.theory_of_cterm ct
   376         val {t=t',T=ty,...} = rep_cterm ct
   377         val _ = Theory.assert_super (theory_of computer) thy
   378         val naming = naming_of computer
   379         val (encoding, t) = remove_types (encoding_of computer) t'
   380         val t = runprog (prog_of computer) t
   381         val t = infer_types naming encoding ty t
   382         val eq = Logic.mk_equals (t', t)
   383     in
   384         export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq
   385     end
   386 
   387 (* --------- Simplify ------------ *)
   388 
   389 datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int 
   390               | Prem of AbstractMachine.term
   391 datatype theorem = Theorem of theory * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table  
   392                * prem list * AbstractMachine.term * term list * sort list
   393 
   394 
   395 exception ParamSimplify of computer * theorem
   396 
   397 fun make_theorem computer th vars =
   398 let
   399     val _ = Theory.assert_super (theory_of computer) (theory_of_thm th)
   400 
   401     val (ComputeThm (hyps, shyps, prop)) = thm2cthm th 
   402 
   403     val encoding = encoding_of computer
   404  
   405     (* variables in the theorem are identified upfront *)
   406     fun collect_vars (Abs (_, _, t)) tab = collect_vars t tab
   407       | collect_vars (a $ b) tab = collect_vars b (collect_vars a tab)
   408       | collect_vars (Const _) tab = tab
   409       | collect_vars (Free _) tab = tab
   410       | collect_vars (Var ((s, i), ty)) tab = 
   411             if List.find (fn x => x=s) vars = NONE then 
   412                 tab
   413             else                
   414                 (case Symtab.lookup tab s of
   415                      SOME ((s',i'),ty') => 
   416                      if s' <> s orelse i' <> i orelse ty <> ty' then 
   417                          raise Compute ("make_theorem: variable name '"^s^"' is not unique")
   418                      else 
   419                          tab
   420                    | NONE => Symtab.update (s, ((s, i), ty)) tab)
   421     val vartab = collect_vars prop Symtab.empty 
   422     fun encodevar (s, t as (_, ty)) (encoding, tab) = 
   423         let
   424             val (x, encoding) = Encode.insert (Var t) encoding
   425         in
   426             (encoding, Symtab.update (s, (x, ty)) tab)
   427         end
   428     val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty)                                                     
   429     val varsubst = Inttab.make (map (fn (_, (x, _)) => (x, NONE)) (Symtab.dest vartab))
   430 
   431     (* make the premises and the conclusion *)
   432     fun mk_prem encoding t = 
   433         (let
   434              val (a, b) = Logic.dest_equals t
   435              val ty = type_of a
   436              val (encoding, a) = remove_types encoding a
   437              val (encoding, b) = remove_types encoding b
   438              val (eq, encoding) =
   439               Encode.insert (Const (@{const_name Pure.eq}, ty --> ty --> @{typ "prop"})) encoding 
   440          in
   441              (encoding, EqPrem (a, b, ty, eq))
   442          end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
   443     val (encoding, prems) = 
   444         (fold_rev (fn t => fn (encoding, l) => 
   445             case mk_prem encoding t  of 
   446                 (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, []))
   447     val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop)
   448     val _ = set_encoding computer encoding
   449 in
   450     Theorem (theory_of_thm th, stamp_of computer, vartab, varsubst, 
   451              prems, concl, hyps, shyps)
   452 end
   453     
   454 fun theory_of_theorem (Theorem (thy,_,_,_,_,_,_,_)) = thy
   455 fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = Theorem (thy,p0,p1,p2,p3,p4,p5,p6)
   456 fun stamp_of_theorem (Theorem (_,s, _, _, _, _, _, _)) = s     
   457 fun vartab_of_theorem (Theorem (_,_,vt,_,_,_,_,_)) = vt
   458 fun varsubst_of_theorem (Theorem (_,_,_,vs,_,_,_,_)) = vs 
   459 fun update_varsubst vs (Theorem (p0,p1,p2,_,p3,p4,p5,p6)) = Theorem (p0,p1,p2,vs,p3,p4,p5,p6)
   460 fun prems_of_theorem (Theorem (_,_,_,_,prems,_,_,_)) = prems
   461 fun update_prems prems (Theorem (p0,p1,p2,p3,_,p4,p5,p6)) = Theorem (p0,p1,p2,p3,prems,p4,p5,p6)
   462 fun concl_of_theorem (Theorem (_,_,_,_,_,concl,_,_)) = concl
   463 fun hyps_of_theorem (Theorem (_,_,_,_,_,_,hyps,_)) = hyps
   464 fun update_hyps hyps (Theorem (p0,p1,p2,p3,p4,p5,_,p6)) = Theorem (p0,p1,p2,p3,p4,p5,hyps,p6)
   465 fun shyps_of_theorem (Theorem (_,_,_,_,_,_,_,shyps)) = shyps
   466 fun update_shyps shyps (Theorem (p0,p1,p2,p3,p4,p5,p6,_)) = Theorem (p0,p1,p2,p3,p4,p5,p6,shyps)
   467 
   468 fun check_compatible computer th s = 
   469     if stamp_of computer <> stamp_of_theorem th then
   470         raise Compute (s^": computer and theorem are incompatible")
   471     else ()
   472 
   473 fun instantiate computer insts th =
   474 let
   475     val _ = check_compatible computer th
   476 
   477     val thy = theory_of computer
   478 
   479     val vartab = vartab_of_theorem th
   480 
   481     fun rewrite computer t =
   482     let  
   483         val (encoding, t) = remove_types (encoding_of computer) t
   484         val t = runprog (prog_of computer) t
   485         val _ = set_encoding computer encoding
   486     in
   487         t
   488     end
   489 
   490     fun assert_varfree vs t = 
   491         if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then
   492             ()
   493         else
   494             raise Compute "instantiate: assert_varfree failed"
   495 
   496     fun assert_closed t =
   497         if AbstractMachine.closed t then
   498             ()
   499         else 
   500             raise Compute "instantiate: not a closed term"
   501 
   502     fun compute_inst (s, ct) vs =
   503         let
   504             val _ = Theory.assert_super (theory_of_cterm ct) thy
   505             val ty = typ_of (ctyp_of_term ct) 
   506         in          
   507             (case Symtab.lookup vartab s of 
   508                  NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
   509                | SOME (x, ty') => 
   510                  (case Inttab.lookup vs x of 
   511                       SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated")
   512                     | SOME NONE => 
   513                       if ty <> ty' then 
   514                           raise Compute ("instantiate: wrong type for variable '"^s^"'")
   515                       else
   516                           let
   517                               val t = rewrite computer (term_of ct)
   518                               val _ = assert_varfree vs t 
   519                               val _ = assert_closed t
   520                           in
   521                               Inttab.update (x, SOME t) vs
   522                           end
   523                     | NONE => raise Compute "instantiate: internal error"))
   524         end
   525 
   526     val vs = fold compute_inst insts (varsubst_of_theorem th)
   527 in
   528     update_varsubst vs th
   529 end
   530 
   531 fun match_aterms subst =
   532     let 
   533         exception no_match
   534         open AbstractMachine
   535         fun match subst (b as (Const c)) a = 
   536             if a = b then subst
   537             else 
   538                 (case Inttab.lookup subst c of 
   539                      SOME (SOME a') => if a=a' then subst else raise no_match
   540                    | SOME NONE => if AbstractMachine.closed a then 
   541                                       Inttab.update (c, SOME a) subst 
   542                                   else raise no_match
   543                    | NONE => raise no_match)
   544           | match subst (b as (Var _)) a = if a=b then subst else raise no_match
   545           | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v'
   546           | match subst (Abs u) (Abs u') = match subst u u'
   547           | match subst _ _ = raise no_match
   548     in
   549         fn b => fn a => (SOME (match subst b a) handle no_match => NONE)
   550     end
   551 
   552 fun apply_subst vars_allowed subst =
   553     let
   554         open AbstractMachine
   555         fun app (t as (Const c)) = 
   556             (case Inttab.lookup subst c of 
   557                  NONE => t 
   558                | SOME (SOME t) => Computed t
   559                | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed")
   560           | app (t as (Var _)) = t
   561           | app (App (u, v)) = App (app u, app v)
   562           | app (Abs m) = Abs (app m)
   563     in
   564         app
   565     end
   566 
   567 fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1)
   568 
   569 fun evaluate_prem computer prem_no th =
   570 let
   571     val _ = check_compatible computer th
   572     val prems = prems_of_theorem th
   573     val varsubst = varsubst_of_theorem th
   574     fun run vars_allowed t = 
   575         runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
   576 in
   577     case nth prems prem_no of
   578         Prem _ => raise Compute "evaluate_prem: no equality premise"
   579       | EqPrem (a, b, ty, _) =>         
   580         let
   581             val a' = run false a
   582             val b' = run true b
   583         in
   584             case match_aterms varsubst b' a' of
   585                 NONE => 
   586                 let
   587                     fun mk s = Syntax.string_of_term_global Pure.thy
   588                       (infer_types (naming_of computer) (encoding_of computer) ty s)
   589                     val left = "computed left side: "^(mk a')
   590                     val right = "computed right side: "^(mk b')
   591                 in
   592                     raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n")
   593                 end
   594               | SOME varsubst => 
   595                 update_prems (splicein prem_no [] prems) (update_varsubst varsubst th)
   596         end
   597 end
   598 
   599 fun prem2term (Prem t) = t
   600   | prem2term (EqPrem (a,b,_,eq)) = 
   601     AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b)
   602 
   603 fun modus_ponens computer prem_no th' th = 
   604 let
   605     val _ = check_compatible computer th
   606     val thy = 
   607         let
   608             val thy1 = theory_of_theorem th
   609             val thy2 = theory_of_thm th'
   610         in
   611             if Theory.subthy (thy1, thy2) then thy2 
   612             else if Theory.subthy (thy2, thy1) then thy1 else
   613             raise Compute "modus_ponens: theorems are not compatible with each other"
   614         end 
   615     val th' = make_theorem computer th' []
   616     val varsubst = varsubst_of_theorem th
   617     fun run vars_allowed t =
   618         runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
   619     val prems = prems_of_theorem th
   620     val prem = run true (prem2term (nth prems prem_no))
   621     val concl = run false (concl_of_theorem th')    
   622 in
   623     case match_aterms varsubst prem concl of
   624         NONE => raise Compute "modus_ponens: conclusion does not match premise"
   625       | SOME varsubst =>
   626         let
   627             val th = update_varsubst varsubst th
   628             val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th
   629             val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th
   630             val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th
   631         in
   632             update_theory thy th
   633         end
   634 end
   635                      
   636 fun simplify computer th =
   637 let
   638     val _ = check_compatible computer th
   639     val varsubst = varsubst_of_theorem th
   640     val encoding = encoding_of computer
   641     val naming = naming_of computer
   642     fun infer t = infer_types naming encoding @{typ "prop"} t
   643     fun run t = infer (runprog (prog_of computer) (apply_subst true varsubst t))
   644     fun runprem p = run (prem2term p)
   645     val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th))
   646     val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th)
   647     val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer))
   648 in
   649     export_thm (theory_of_theorem th) hyps shyps prop
   650 end
   651 
   652 end
   653