diff -r c7ce7685e087 -r d83659570337 src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Wed Jul 21 15:31:38 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,683 +0,0 @@ -(* Title: Tools/Compute_Oracle/compute.ML - Author: Steven Obua -*) - -signature COMPUTE = sig - - type computer - type theorem - type naming = int -> string - - datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML - - (* Functions designated with a ! in front of them actually update the computer parameter *) - - exception Make of string - val make : machine -> theory -> thm list -> computer - val make_with_cache : machine -> theory -> term list -> thm list -> computer - val theory_of : computer -> theory - val hyps_of : computer -> term list - val shyps_of : computer -> sort list - (* ! *) val update : computer -> thm list -> unit - (* ! *) val update_with_cache : computer -> term list -> thm list -> unit - (* ! *) val discard : computer -> unit - - (* ! *) val set_naming : computer -> naming -> unit - val naming_of : computer -> naming - - exception Compute of string - val simplify : computer -> theorem -> thm - val rewrite : computer -> cterm -> thm - - val make_theorem : computer -> thm -> string list -> theorem - (* ! *) val instantiate : computer -> (string * cterm) list -> theorem -> theorem - (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem - (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem - -end - -structure Compute :> COMPUTE = struct - -open Report; - -datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML - -(* Terms are mapped to integer codes *) -structure Encode :> -sig - type encoding - val empty : encoding - val insert : term -> encoding -> int * encoding - val lookup_code : term -> encoding -> int option - val lookup_term : int -> encoding -> term option - val remove_code : int -> encoding -> encoding - val remove_term : term -> encoding -> encoding - val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a -end -= -struct - -type encoding = int * (int Termtab.table) * (term Inttab.table) - -val empty = (0, Termtab.empty, Inttab.empty) - -fun insert t (e as (count, term2int, int2term)) = - (case Termtab.lookup term2int t of - NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term)) - | SOME code => (code, e)) - -fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t - -fun lookup_term c (_, _, int2term) = Inttab.lookup int2term c - -fun remove_code c (e as (count, term2int, int2term)) = - (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term)) - -fun remove_term t (e as (count, term2int, int2term)) = - (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term)) - -fun fold f (_, term2int, _) = Termtab.fold f term2int - -end - -exception Make of string; -exception Compute of string; - -local - fun make_constant t ty encoding = - let - val (code, encoding) = Encode.insert t encoding - in - (encoding, AbstractMachine.Const code) - end -in - -fun remove_types encoding t = - case t of - Var (_, ty) => make_constant t ty encoding - | Free (_, ty) => make_constant t ty encoding - | Const (_, ty) => make_constant t ty encoding - | Abs (_, ty, t') => - let val (encoding, t'') = remove_types encoding t' in - (encoding, AbstractMachine.Abs t'') - end - | a $ b => - let - val (encoding, a) = remove_types encoding a - val (encoding, b) = remove_types encoding b - in - (encoding, AbstractMachine.App (a,b)) - end - | Bound b => (encoding, AbstractMachine.Var b) -end - -local - fun type_of (Free (_, ty)) = ty - | type_of (Const (_, ty)) = ty - | type_of (Var (_, ty)) = ty - | type_of _ = sys_error "infer_types: type_of error" -in -fun infer_types naming encoding = - let - fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v)) - | infer_types _ bounds _ (AbstractMachine.Const code) = - let - val c = the (Encode.lookup_term code encoding) - in - (c, type_of c) - end - | infer_types level bounds _ (AbstractMachine.App (a, b)) = - let - val (a, aty) = infer_types level bounds NONE a - val (adom, arange) = - case aty of - Type ("fun", [dom, range]) => (dom, range) - | _ => sys_error "infer_types: function type expected" - val (b, bty) = infer_types level bounds (SOME adom) b - in - (a $ b, arange) - end - | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) = - let - val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m - in - (Abs (naming level, dom, m), ty) - end - | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction" - - fun infer ty term = - let - val (term', _) = infer_types 0 [] (SOME ty) term - in - term' - end - in - infer - end -end - -datatype prog = - ProgBarras of AM_Interpreter.program - | ProgBarrasC of AM_Compiler.program - | ProgHaskell of AM_GHC.program - | ProgSML of AM_SML.program - -fun machine_of_prog (ProgBarras _) = BARRAS - | machine_of_prog (ProgBarrasC _) = BARRAS_COMPILED - | machine_of_prog (ProgHaskell _) = HASKELL - | machine_of_prog (ProgSML _) = SML - -type naming = int -> string - -fun default_naming i = "v_" ^ Int.toString i - -datatype computer = Computer of - (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) - option Unsynchronized.ref - -fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy -fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps -fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) -fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable -fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp -fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog -fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding -fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = - (r := SOME (p1,encoding',p2,p3,p4,p5,p6)) -fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n -fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= - (r := SOME (p1,p2,p3,p4,p5,p6,naming')) - -fun ref_of (Computer r) = r - -datatype cthm = ComputeThm of term list * sort list * term - -fun thm2cthm th = - let - val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th - val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else () - in - ComputeThm (hyps, shyps, prop) - end - -fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths = - let - fun transfer (x:thm) = Thm.transfer thy x - val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths - - fun make_pattern encoding n vars (var as AbstractMachine.Abs _) = - raise (Make "no lambda abstractions allowed in pattern") - | make_pattern encoding n vars (var as AbstractMachine.Var _) = - raise (Make "no bound variables allowed in pattern") - | make_pattern encoding n vars (AbstractMachine.Const code) = - (case the (Encode.lookup_term code encoding) of - Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar) - handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed")) - | _ => (n, vars, AbstractMachine.PConst (code, []))) - | make_pattern encoding n vars (AbstractMachine.App (a, b)) = - let - val (n, vars, pa) = make_pattern encoding n vars a - val (n, vars, pb) = make_pattern encoding n vars b - in - case pa of - AbstractMachine.PVar => - raise (Make "patterns may not start with a variable") - | AbstractMachine.PConst (c, args) => - (n, vars, AbstractMachine.PConst (c, args@[pb])) - end - - fun thm2rule (encoding, hyptable, shyptable) th = - let - val (ComputeThm (hyps, shyps, prop)) = th - val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable - val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable - val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop) - val (a, b) = Logic.dest_equals prop - handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)") - val a = Envir.eta_contract a - val b = Envir.eta_contract b - val prems = map Envir.eta_contract prems - - val (encoding, left) = remove_types encoding a - val (encoding, right) = remove_types encoding b - fun remove_types_of_guard encoding g = - (let - val (t1, t2) = Logic.dest_equals g - val (encoding, t1) = remove_types encoding t1 - val (encoding, t2) = remove_types encoding t2 - in - (encoding, AbstractMachine.Guard (t1, t2)) - end handle TERM _ => raise (Make "guards must be meta-level equations")) - 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, []) - - (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule. - As it is, all variables of the rule are schematic, and there are no schematic variables in meta-hyps, therefore - this check can be left out. *) - - val (vcount, vars, pattern) = make_pattern encoding 0 Inttab.empty left - val _ = (case pattern of - AbstractMachine.PVar => - raise (Make "patterns may not start with a variable") - (* | AbstractMachine.PConst (_, []) => - (print th; raise (Make "no parameter rewrite found"))*) - | _ => ()) - - (* finally, provide a function for renaming the - pattern bound variables on the right hand side *) - - fun rename level vars (var as AbstractMachine.Var _) = var - | rename level vars (c as AbstractMachine.Const code) = - (case Inttab.lookup vars code of - NONE => c - | SOME n => AbstractMachine.Var (vcount-n-1+level)) - | rename level vars (AbstractMachine.App (a, b)) = - AbstractMachine.App (rename level vars a, rename level vars b) - | rename level vars (AbstractMachine.Abs m) = - AbstractMachine.Abs (rename (level+1) vars m) - - fun rename_guard (AbstractMachine.Guard (a,b)) = - AbstractMachine.Guard (rename 0 vars a, rename 0 vars b) - in - ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right)) - end - - val ((encoding, hyptable, shyptable), rules) = - fold_rev (fn th => fn (encoding_hyptable, rules) => - let - val (encoding_hyptable, rule) = thm2rule encoding_hyptable th - in (encoding_hyptable, rule::rules) end) - ths ((encoding, Termtab.empty, Sorttab.empty), []) - - fun make_cache_pattern t (encoding, cache_patterns) = - let - val (encoding, a) = remove_types encoding t - val (_,_,p) = make_pattern encoding 0 Inttab.empty a - in - (encoding, p::cache_patterns) - end - - val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, []) - - fun arity (Type ("fun", [a,b])) = 1 + arity b - | arity _ = 0 - - fun make_arity (Const (s, _), i) tab = - (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab) - | make_arity _ tab = tab - - val const_arity_tab = Encode.fold make_arity encoding Inttab.empty - fun const_arity x = Inttab.lookup const_arity_tab x - - val prog = - case machine of - BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules) - | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules) - | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules) - | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules) - - fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) - - val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable - - in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end - -fun make_with_cache machine thy cache_patterns raw_thms = - Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) - -fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms - -fun update_with_cache computer cache_patterns raw_thms = - let - val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) - (encoding_of computer) cache_patterns raw_thms - val _ = (ref_of computer) := SOME c - in - () - end - -fun update computer raw_thms = update_with_cache computer [] raw_thms - -fun discard computer = - let - val _ = - case prog_of computer of - ProgBarras p => AM_Interpreter.discard p - | ProgBarrasC p => AM_Compiler.discard p - | ProgHaskell p => AM_GHC.discard p - | ProgSML p => AM_SML.discard p - val _ = (ref_of computer) := NONE - in - () - end - -fun runprog (ProgBarras p) = AM_Interpreter.run p - | runprog (ProgBarrasC p) = AM_Compiler.run p - | runprog (ProgHaskell p) = AM_GHC.run p - | runprog (ProgSML p) = AM_SML.run p - -(* ------------------------------------------------------------------------------------- *) -(* An oracle for exporting theorems; must only be accessible from inside this structure! *) -(* ------------------------------------------------------------------------------------- *) - -fun merge_hyps hyps1 hyps2 = -let - fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab -in - Termtab.keys (add hyps2 (add hyps1 Termtab.empty)) -end - -fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab - -fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty)) - -val (_, export_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) => - let - val shyptab = add_shyps shyps Sorttab.empty - fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab - fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab - fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) - val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab - val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) - val _ = - if not (null shyps) then - raise Compute ("dangling sort hypotheses: " ^ - commas (map (Syntax.string_of_sort_global thy) shyps)) - else () - in - Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop) - end))); - -fun export_thm thy hyps shyps prop = - let - val th = export_oracle (thy, hyps, shyps, prop) - val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps - in - fold (fn h => fn p => Thm.implies_elim p h) hyps th - end - -(* --------- Rewrite ----------- *) - -fun rewrite computer ct = - let - val thy = Thm.theory_of_cterm ct - val {t=t',T=ty,...} = rep_cterm ct - val _ = Theory.assert_super (theory_of computer) thy - val naming = naming_of computer - val (encoding, t) = remove_types (encoding_of computer) t' - (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*) - val t = runprog (prog_of computer) t - val t = infer_types naming encoding ty t - val eq = Logic.mk_equals (t', t) - in - export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq - end - -(* --------- Simplify ------------ *) - -datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int - | Prem of AbstractMachine.term -datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table - * prem list * AbstractMachine.term * term list * sort list - - -exception ParamSimplify of computer * theorem - -fun make_theorem computer th vars = -let - val _ = Theory.assert_super (theory_of computer) (theory_of_thm th) - - val (ComputeThm (hyps, shyps, prop)) = thm2cthm th - - val encoding = encoding_of computer - - (* variables in the theorem are identified upfront *) - fun collect_vars (Abs (_, _, t)) tab = collect_vars t tab - | collect_vars (a $ b) tab = collect_vars b (collect_vars a tab) - | collect_vars (Const _) tab = tab - | collect_vars (Free _) tab = tab - | collect_vars (Var ((s, i), ty)) tab = - if List.find (fn x => x=s) vars = NONE then - tab - else - (case Symtab.lookup tab s of - SOME ((s',i'),ty') => - if s' <> s orelse i' <> i orelse ty <> ty' then - raise Compute ("make_theorem: variable name '"^s^"' is not unique") - else - tab - | NONE => Symtab.update (s, ((s, i), ty)) tab) - val vartab = collect_vars prop Symtab.empty - fun encodevar (s, t as (_, ty)) (encoding, tab) = - let - val (x, encoding) = Encode.insert (Var t) encoding - in - (encoding, Symtab.update (s, (x, ty)) tab) - end - val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty) - val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab)) - - (* make the premises and the conclusion *) - fun mk_prem encoding t = - (let - val (a, b) = Logic.dest_equals t - val ty = type_of a - val (encoding, a) = remove_types encoding a - val (encoding, b) = remove_types encoding b - val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding - in - (encoding, EqPrem (a, b, ty, eq)) - end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end) - val (encoding, prems) = - (fold_rev (fn t => fn (encoding, l) => - case mk_prem encoding t of - (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, [])) - val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop) - val _ = set_encoding computer encoding -in - Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, - prems, concl, hyps, shyps) -end - -fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy -fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = - Theorem (Theory.check_thy thy,p0,p1,p2,p3,p4,p5,p6) -fun stamp_of_theorem (Theorem (_,s, _, _, _, _, _, _)) = s -fun vartab_of_theorem (Theorem (_,_,vt,_,_,_,_,_)) = vt -fun varsubst_of_theorem (Theorem (_,_,_,vs,_,_,_,_)) = vs -fun update_varsubst vs (Theorem (p0,p1,p2,_,p3,p4,p5,p6)) = Theorem (p0,p1,p2,vs,p3,p4,p5,p6) -fun prems_of_theorem (Theorem (_,_,_,_,prems,_,_,_)) = prems -fun update_prems prems (Theorem (p0,p1,p2,p3,_,p4,p5,p6)) = Theorem (p0,p1,p2,p3,prems,p4,p5,p6) -fun concl_of_theorem (Theorem (_,_,_,_,_,concl,_,_)) = concl -fun hyps_of_theorem (Theorem (_,_,_,_,_,_,hyps,_)) = hyps -fun update_hyps hyps (Theorem (p0,p1,p2,p3,p4,p5,_,p6)) = Theorem (p0,p1,p2,p3,p4,p5,hyps,p6) -fun shyps_of_theorem (Theorem (_,_,_,_,_,_,_,shyps)) = shyps -fun update_shyps shyps (Theorem (p0,p1,p2,p3,p4,p5,p6,_)) = Theorem (p0,p1,p2,p3,p4,p5,p6,shyps) - -fun check_compatible computer th s = - if stamp_of computer <> stamp_of_theorem th then - raise Compute (s^": computer and theorem are incompatible") - else () - -fun instantiate computer insts th = -let - val _ = check_compatible computer th - - val thy = theory_of computer - - val vartab = vartab_of_theorem th - - fun rewrite computer t = - let - val naming = naming_of computer - val (encoding, t) = remove_types (encoding_of computer) t - val t = runprog (prog_of computer) t - val _ = set_encoding computer encoding - in - t - end - - fun assert_varfree vs t = - if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then - () - else - raise Compute "instantiate: assert_varfree failed" - - fun assert_closed t = - if AbstractMachine.closed t then - () - else - raise Compute "instantiate: not a closed term" - - fun compute_inst (s, ct) vs = - let - val _ = Theory.assert_super (theory_of_cterm ct) thy - val ty = typ_of (ctyp_of_term ct) - in - (case Symtab.lookup vartab s of - NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem") - | SOME (x, ty') => - (case Inttab.lookup vs x of - SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated") - | SOME NONE => - if ty <> ty' then - raise Compute ("instantiate: wrong type for variable '"^s^"'") - else - let - val t = rewrite computer (term_of ct) - val _ = assert_varfree vs t - val _ = assert_closed t - in - Inttab.update (x, SOME t) vs - end - | NONE => raise Compute "instantiate: internal error")) - end - - val vs = fold compute_inst insts (varsubst_of_theorem th) -in - update_varsubst vs th -end - -fun match_aterms subst = - let - exception no_match - open AbstractMachine - fun match subst (b as (Const c)) a = - if a = b then subst - else - (case Inttab.lookup subst c of - SOME (SOME a') => if a=a' then subst else raise no_match - | SOME NONE => if AbstractMachine.closed a then - Inttab.update (c, SOME a) subst - else raise no_match - | NONE => raise no_match) - | match subst (b as (Var _)) a = if a=b then subst else raise no_match - | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v' - | match subst (Abs u) (Abs u') = match subst u u' - | match subst _ _ = raise no_match - in - fn b => fn a => (SOME (match subst b a) handle no_match => NONE) - end - -fun apply_subst vars_allowed subst = - let - open AbstractMachine - fun app (t as (Const c)) = - (case Inttab.lookup subst c of - NONE => t - | SOME (SOME t) => Computed t - | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed") - | app (t as (Var _)) = t - | app (App (u, v)) = App (app u, app v) - | app (Abs m) = Abs (app m) - in - app - end - -fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1) - -fun evaluate_prem computer prem_no th = -let - val _ = check_compatible computer th - val prems = prems_of_theorem th - val varsubst = varsubst_of_theorem th - fun run vars_allowed t = - runprog (prog_of computer) (apply_subst vars_allowed varsubst t) -in - case List.nth (prems, prem_no) of - Prem _ => raise Compute "evaluate_prem: no equality premise" - | EqPrem (a, b, ty, _) => - let - val a' = run false a - val b' = run true b - in - case match_aterms varsubst b' a' of - NONE => - let - fun mk s = Syntax.string_of_term_global Pure.thy - (infer_types (naming_of computer) (encoding_of computer) ty s) - val left = "computed left side: "^(mk a') - val right = "computed right side: "^(mk b') - in - raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n") - end - | SOME varsubst => - update_prems (splicein prem_no [] prems) (update_varsubst varsubst th) - end -end - -fun prem2term (Prem t) = t - | prem2term (EqPrem (a,b,_,eq)) = - AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b) - -fun modus_ponens computer prem_no th' th = -let - val _ = check_compatible computer th - val thy = - let - val thy1 = theory_of_theorem th - val thy2 = theory_of_thm th' - in - if Theory.subthy (thy1, thy2) then thy2 - else if Theory.subthy (thy2, thy1) then thy1 else - raise Compute "modus_ponens: theorems are not compatible with each other" - end - val th' = make_theorem computer th' [] - val varsubst = varsubst_of_theorem th - fun run vars_allowed t = - runprog (prog_of computer) (apply_subst vars_allowed varsubst t) - val prems = prems_of_theorem th - val prem = run true (prem2term (List.nth (prems, prem_no))) - val concl = run false (concl_of_theorem th') -in - case match_aterms varsubst prem concl of - NONE => raise Compute "modus_ponens: conclusion does not match premise" - | SOME varsubst => - let - val th = update_varsubst varsubst th - val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th - val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th - val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th - in - update_theory thy th - end -end - -fun simplify computer th = -let - val _ = check_compatible computer th - val varsubst = varsubst_of_theorem th - val encoding = encoding_of computer - val naming = naming_of computer - fun infer t = infer_types naming encoding @{typ "prop"} t - fun run t = infer (runprog (prog_of computer) (apply_subst true varsubst t)) - fun runprem p = run (prem2term p) - val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th)) - val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th) - val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer)) -in - export_thm (theory_of_theorem th) hyps shyps prop -end - -end -