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