(* additional stuff, such as ML bindings, for Bali theory *) val Eval_thy = theory "Eval" ; fun mkraw th = rewrite_rule [symmetric raweval_def] (transfer BaliPlus.thy th) ; val arbitrary3_def = thm "arbitrary3_def" ; val lvar_def = thm "lvar_def" ; val abupd_def = thm "abupd_def" ; val abupd_def2 = thm "abupd_def2" ; val throw_def = thm "throw_def" ; val abrupt_if_def = thm "abrupt_if_def" ; val prod_fun_def = thm "prod_fun_def" ; val unique_eval = thm "unique_eval" ; val eval_elim_cases = thms "eval_elim_cases" ; val abrupt_if_True_not_None = thm "abrupt_if_True_not_None" ; val [ Abrupt_rev, Skip_rev, Jmp_rev, Lab_rev, Nil_rev, Cons_rev, Lit_rev, UnOp_rev, BinOp_rev, LVar_rev, Cast_rev, Inst_rev, Super_rev, Acc_rev, Expr_rev, Comp_rev, Methd_rev, Body_rev, Cond_rev, If_rev, Loop_rev, Fin_rev, Throw_rev, NewC_rev, NewA_rev, Ass_rev, Try_rev, FVar_rev, AVar_rev, Call_rev, Init_rev ] = eval_elim_cases ; val Norm = thm "Norm" ; (* to get names of intro rules for eval! open TextIO ; val instr = openIn "/home2/dawson/Isabelle2003/src/HOL/Bali/Eval.thy" ; val fstr = inputAll instr ; val fds = String.fields Char.isSpace fstr ; fun tf str = let val chs = rev (String.explode str) ; in case chs of #":" :: wd => SOME (String.implode (rev wd)) | _ => NONE end ; val names = BasisLibrary.List.mapPartial tf fds ; *) structure eval = struct local val Some (_, ind_rec) = InductivePackage.get_inductive Eval_thy "Eval.eval" ; in val {defs: thm list, mono: thm, elims: thm list as [elim], intrs: thm list, induct: thm, unfold: thm, mk_cases: string -> thm, raw_induct: thm} = ind_rec ; end ; val [ Abrupt, Skip, Expr, Lab, Comp, If, Loop, Jmp, Throw, Try, Fin, Init, NewC, NewA, Cast, Inst, Lit, UnOp, BinOp, Super, Acc, Ass, Cond, Call, Methd, Body, LVar, FVar, AVar, Nil, Cons ] = intrs ; end ; (* structure eval *) val ass_reverse = eval.mk_cases "G |- ba -var:=a->va-> s1" ; val if_reverse = eval.mk_cases "(Norm s0, In1r (If(e) c1 Else c2), dummy_res, s2): eval G" ; val () = qed_goal_spec_mp "Throw'" Eval_thy "abupd (throw a) s = ns --> ?Q --> G|-Norm s0 - Throw e-> ns" (fn _ => [ Safe_tac, (etac eval.Throw 1)]) ; val () = qed_goal_spec_mp "Ass'" Eval_thy "assign f v s2 = ns --> ?P --> ?Q --> G|-Norm s0 -va:=e->v-> ns" (fn _ => [ Safe_tac, (eatac eval.Ass 1 1)]) ; val LVar' = rewrite_rule [lvar_def] (transfer BaliPlus.thy eval.LVar) ;