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