diff --git a/src/Provers/hypsubst.ML b/src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML +++ b/src/Provers/hypsubst.ML @@ -1,306 +1,306 @@ (* Title: Provers/hypsubst.ML Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson Copyright 1995 University of Cambridge Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst". Tactic to substitute using (at least) the assumption x=t in the rest of the subgoal, and to delete (at least) that assumption. Original version due to Martin Coen. This version uses the simplifier, and requires it to be already present. Test data: Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; Goal "!!y. [| ?x=y; P(?x) |] ==> y = a"; Goal "!!z. [| ?x=y; P(?x) |] ==> y = a"; Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)"; by (bound_hyp_subst_tac 1); by (hyp_subst_tac 1); Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) Goal "P(a) --> (EX y. a=y --> P(f(a)))"; Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \ \ P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)"; by (blast_hyp_subst_tac true 1); *) signature HYPSUBST_DATA = sig val dest_Trueprop : term -> term val dest_eq : term -> term * term val dest_imp : term -> term * term val eq_reflection : thm (* a=b ==> a==b *) val rev_eq_reflection: thm (* a==b ==> a=b *) val imp_intr : thm (* (P ==> Q) ==> P-->Q *) val rev_mp : thm (* [| P; P-->Q |] ==> Q *) val subst : thm (* [| a=b; P(a) |] ==> P(b) *) val sym : thm (* a=b ==> b=a *) val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *) end; signature HYPSUBST = sig val bound_hyp_subst_tac : Proof.context -> int -> tactic val hyp_subst_tac_thin : bool -> Proof.context -> int -> tactic val hyp_subst_thin : bool Config.T val hyp_subst_tac : Proof.context -> int -> tactic val blast_hyp_subst_tac : Proof.context -> bool -> int -> tactic val stac : Proof.context -> thm -> int -> tactic end; functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST = struct exception EQ_VAR; (*Simplifier turns Bound variables to special Free variables: change it back (any Bound variable will do)*) fun inspect_contract t = (case Envir.eta_contract t of Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T) | t' => t'); val has_vars = Term.exists_subterm Term.is_Var; val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar); (*If novars then we forbid Vars in the equality. If bnd then we only look for Bound variables to eliminate. When can we safely delete the equality? Not if it equates two constants; consider 0=1. Not if it resembles x=t[x], since substitution does not eliminate x. Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P Not if it involves a variable free in the premises, but we can't check for this -- hence bnd and bound_hyp_subst_tac Prefer to eliminate Bound variables if possible. Result: true = use as is, false = reorient first also returns var to substitute, relevant if it is Free *) fun inspect_pair bnd novars (t, u) = if novars andalso (has_tvars t orelse has_tvars u) then raise Match (*variables in the type!*) else (case apply2 inspect_contract (t, u) of (Bound i, _) => if loose_bvar1 (u, i) orelse novars andalso has_vars u then raise Match else (true, Bound i) (*eliminates t*) | (_, Bound i) => if loose_bvar1 (t, i) orelse novars andalso has_vars t then raise Match else (false, Bound i) (*eliminates u*) | (t' as Free _, _) => if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u then raise Match else (true, t') (*eliminates t*) | (_, u' as Free _) => if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t then raise Match else (false, u') (*eliminates u*) | _ => raise Match); (*Locates a substitutable variable on the left (resp. right) of an equality assumption. Returns the number of intervening assumptions. *) fun eq_var bnd novars check_frees t = let fun check_free ts (orient, Free f) = if not check_frees orelse not orient orelse exists (curry Logic.occs (Free f)) ts then (orient, true) else raise Match | check_free ts (orient, _) = (orient, false) - fun eq_var_aux k (Const(\<^const_name>\Pure.all\,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs - | eq_var_aux k (Const(\<^const_name>\Pure.imp\,_) $ A $ B) hs = + fun eq_var_aux k \<^Const_>\Pure.all _ for \Abs(_,_,t)\\ hs = eq_var_aux k t hs + | eq_var_aux k \<^Const_>\Pure.imp for A B\ hs = ((k, check_free (B :: hs) (inspect_pair bnd novars (Data.dest_eq (Data.dest_Trueprop A)))) handle TERM _ => eq_var_aux (k+1) B (A :: hs) | Match => eq_var_aux (k+1) B (A :: hs)) | eq_var_aux k _ _ = raise EQ_VAR in eq_var_aux 0 t [] end; fun thin_free_eq_tac ctxt = SUBGOAL (fn (t, i) => let val (k, _) = eq_var false false false t val ok = (eq_var false false true t |> fst) > k handle EQ_VAR => true in if ok then EVERY [rotate_tac k i, eresolve_tac ctxt [thin_rl] i, rotate_tac (~k) i] else no_tac end handle EQ_VAR => no_tac) (*For the simpset. Adds ALL suitable equalities, even if not first! No vars are allowed here, as simpsets are built from meta-assumptions*) fun mk_eqs bnd th = [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst then th RS Data.eq_reflection else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ] handle TERM _ => [] | Match => []; (*Select a suitable equality assumption; substitute throughout the subgoal If bnd is true, then it replaces Bound variables only. *) fun gen_hyp_subst_tac ctxt bnd = SUBGOAL (fn (Bi, i) => let val (k, (orient, is_free)) = eq_var bnd true true Bi val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd)) in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i, if not is_free then eresolve_tac ctxt [thin_rl] i else if orient then eresolve_tac ctxt [Data.rev_mp] i else eresolve_tac ctxt [Data.sym RS Data.rev_mp] i, rotate_tac (~k) i, if is_free then resolve_tac ctxt [Data.imp_intr] i else all_tac] end handle THM _ => no_tac | EQ_VAR => no_tac) val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst); fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) => case try (Logic.strip_assums_hyp #> hd #> Data.dest_Trueprop #> Data.dest_eq #> apply2 Envir.eta_contract) (Thm.term_of cBi) of SOME (t, t') => let val Bi = Thm.term_of cBi; val ps = Logic.strip_params Bi; val U = Term.fastype_of1 (rev (map snd ps), t); val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi); val rl' = Thm.lift_rule cBi rl; val (ixn, T) = dest_Var (Term.head_of (Data.dest_Trueprop (Logic.strip_assums_concl (Thm.prop_of rl')))); val (v1, v2) = Data.dest_eq (Data.dest_Trueprop (Logic.strip_assums_concl (hd (Thm.prems_of rl')))); val (Ts, V) = split_last (Term.binder_types T); val u = fold_rev Term.abs (ps @ [("x", U)]) (case (if b then t else t') of Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q) | t => Term.abstract_over (t, Term.incr_boundvars 1 Q)); val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U)); in compose_tac ctxt (true, Drule.instantiate_normalize (instT, Vars.make (map (apsnd (Thm.cterm_of ctxt)) [((ixn, Ts ---> U --> body_type T), u), ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')])) rl', Thm.nprems_of rl) i end | NONE => no_tac); fun imp_intr_tac ctxt = resolve_tac ctxt [Data.imp_intr]; fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd; fun dup_subst ctxt = rev_dup_elim ctxt ssubst (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *) (* premises containing meta-implications or quantifiers *) (*Old version of the tactic above -- slower but the only way to handle equalities containing Vars.*) fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) => let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k, (orient, is_free)) = eq_var bnd false true Bi val rl = if is_free then dup_subst ctxt else ssubst val rl = if orient then rl else Data.sym RS rl in DETERM (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), rotate_tac 1 i, REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i), inst_subst_tac ctxt orient rl i, REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i)]) end handle THM _ => no_tac | EQ_VAR => no_tac); (*Substitutes for Free or Bound variables, discarding equalities on Bound variables and on Free variables if thin=true*) fun hyp_subst_tac_thin thin ctxt = REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl], gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false, if thin then thin_free_eq_tac ctxt else K no_tac]; val hyp_subst_thin = Attrib.setup_config_bool \<^binding>\hypsubst_thin\ (K false); fun hyp_subst_tac ctxt = hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt; (*Substitutes for Bound variables only -- this is always safe*) fun bound_hyp_subst_tac ctxt = REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac ctxt true); (** Version for Blast_tac. Hyps that are affected by the substitution are moved to the front. Defect: even trivial changes are noticed, such as substitutions in the arguments of a function Var. **) (*final re-reversal of the changed assumptions*) fun reverse_n_tac _ 0 i = all_tac | reverse_n_tac _ 1 i = rotate_tac ~1 i | reverse_n_tac ctxt n i = REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac ctxt [Data.rev_mp] i) THEN REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i); (*Use imp_intr, comparing the old hyps with the new ones as they come out.*) fun all_imp_intr_tac ctxt hyps i = let fun imptac (r, []) st = reverse_n_tac ctxt r i st | imptac (r, hyp::hyps) st = let val (hyp', _) = Thm.term_of (Thm.cprem_of st i) |> Logic.strip_assums_concl |> Data.dest_Trueprop |> Data.dest_imp; val (r', tac) = if Envir.aeconv (hyp, hyp') then (r, imp_intr_tac ctxt i THEN rotate_tac ~1 i) else (*leave affected hyps at end*) (r + 1, imp_intr_tac ctxt i); in (case Seq.pull (tac st) of NONE => Seq.single st | SOME (st', _) => imptac (r', hyps) st') end in imptac (0, rev hyps) end; fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi, i) => let val (k, (symopt, _)) = eq_var false false false Bi val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) (*omit selected equality, returning other hyps*) val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) val n = length hyps in if trace then tracing "Substituting an equality" else (); DETERM (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), rotate_tac 1 i, REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i), inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i, all_imp_intr_tac ctxt hyps i]) end handle THM _ => no_tac | EQ_VAR => no_tac); (*apply an equality or definition ONCE; fails unless the substitution has an effect*) fun stac ctxt th = let val th' = th RS Data.rev_eq_reflection handle THM _ => th in CHANGED_GOAL (resolve_tac ctxt [th' RS ssubst]) end; (* method setup *) val _ = Theory.setup (Method.setup \<^binding>\hypsubst\ (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt))) "substitution using an assumption (improper)" #> Method.setup \<^binding>\hypsubst_thin\ (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac_thin true ctxt))) "substitution using an assumption, eliminating assumptions" #> Method.setup \<^binding>\simplesubst\ (Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (stac ctxt th))) "simple substitution"); end; diff --git a/src/Provers/splitter.ML b/src/Provers/splitter.ML --- a/src/Provers/splitter.ML +++ b/src/Provers/splitter.ML @@ -1,489 +1,489 @@ (* Title: Provers/splitter.ML Author: Tobias Nipkow Copyright 1995 TU Munich Generic case-splitter, suitable for most logics. Deals with equalities of the form ?P(f args) = ... where "f args" must be a first-order term without duplicate variables. *) signature SPLITTER_DATA = sig val context : Proof.context val mk_eq : thm -> thm val meta_eq_to_iff: thm (* "x == y ==> x = y" *) val iffD : thm (* "[| P = Q; Q |] ==> P" *) val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *) val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *) val exE : thm (* "[| EX x. P x; !!x. P x ==> Q |] ==> Q" *) val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *) val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *) val notnotD : thm (* "~ ~ P ==> P" *) val safe_tac : Proof.context -> tactic end signature SPLITTER = sig (* somewhat more internal functions *) val cmap_of_split_thms: thm list -> (string * (typ * term * thm * typ * int) list) list val split_posns: (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term -> (thm * (typ * typ * int list) list * int list * typ * term) list (* first argument is a "cmap", returns a list of "split packs" *) (* the "real" interface, providing a number of tactics *) val split_tac : Proof.context -> thm list -> int -> tactic val split_inside_tac: Proof.context -> thm list -> int -> tactic val split_asm_tac : Proof.context -> thm list -> int -> tactic val add_split: thm -> Proof.context -> Proof.context val add_split_bang: thm -> Proof.context -> Proof.context val del_split: thm -> Proof.context -> Proof.context val split_modifiers : Method.modifier parser list end; functor Splitter(Data: SPLITTER_DATA): SPLITTER = struct val Const (const_not, _) $ _ = Object_Logic.drop_judgment Data.context (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD))); val Const (const_or , _) $ _ $ _ = Object_Logic.drop_judgment Data.context (#1 (Logic.dest_implies (Thm.prop_of Data.disjE))); val const_Trueprop = Object_Logic.judgment_name Data.context; fun split_format_err () = error "Wrong format for split rule"; fun split_thm_info thm = (case Thm.concl_of (Data.mk_eq thm) of - Const(\<^const_name>\Pure.eq\, _) $ (Var _ $ t) $ c => + \<^Const_>\Pure.eq _ for \Var _ $ t\ c\ => (case strip_comb t of (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false) | _ => split_format_err ()) | _ => split_format_err ()); fun cmap_of_split_thms thms = let val splits = map Data.mk_eq thms fun add_thm thm cmap = (case Thm.concl_of thm of _ $ (t as _ $ lhs) $ _ => (case strip_comb lhs of (Const(a,aT),args) => let val info = (aT,lhs,thm,fastype_of t,length args) in case AList.lookup (op =) cmap a of SOME infos => AList.update (op =) (a, info::infos) cmap | NONE => (a,[info])::cmap end | _ => split_format_err()) | _ => split_format_err()) in fold add_thm splits [] end; val abss = fold (Term.abs o pair ""); (* ------------------------------------------------------------------------- *) (* mk_case_split_tac *) (* ------------------------------------------------------------------------- *) fun mk_case_split_tac order = let (************************************************************ Create lift-theorem "trlift" : [| !!x. Q x == R x; P(%x. R x) == C |] ==> P (%x. Q x) == C *************************************************************) val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *) val lift = Goal.prove_global \<^theory> ["P", "Q", "R"] [Syntax.read_prop_global \<^theory>\Pure\ "!!x :: 'b. Q(x) == R(x) :: 'c"] (Syntax.read_prop_global \<^theory>\Pure\ "P(%x. Q(x)) == P(%x. R(x))") (fn {context = ctxt, prems} => rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1) val _ $ _ $ (_ $ (_ $ abs_lift) $ _) = Thm.prop_of lift; val trlift = lift RS transitive_thm; (************************************************************************ Set up term for instantiation of P in the lift-theorem t : lefthand side of meta-equality in subgoal the lift theorem is applied to (see select) pos : "path" leading to abstraction, coded as a list T : type of body of P(...) *************************************************************************) fun mk_cntxt t pos T = let fun down [] t = (Bound 0, t) | down (p :: ps) t = let val (h, ts) = strip_comb t val (ts1, u :: ts2) = chop p ts val (u1, u2) = down ps u in (list_comb (incr_boundvars 1 h, map (incr_boundvars 1) ts1 @ u1 :: map (incr_boundvars 1) ts2), u2) end; val (u1, u2) = down (rev pos) t in (Abs ("", T, u1), u2) end; (************************************************************************ Set up term for instantiation of P in the split-theorem P(...) == rhs t : lefthand side of meta-equality in subgoal the split theorem is applied to (see select) T : type of body of P(...) tt : the term Const(key,..) $ ... *************************************************************************) fun mk_cntxt_splitthm t tt T = let fun repl lev t = if Envir.aeconv(incr_boundvars lev tt, t) then Bound lev else case t of (Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t) | (Bound i) => Bound (if i>=lev then i+1 else i) | (t1 $ t2) => (repl lev t1) $ (repl lev t2) | t => t in Abs("", T, repl 0 t) end; (* add all loose bound variables in t to list is *) fun add_lbnos t is = add_loose_bnos (t, 0, is); (* check if the innermost abstraction that needs to be removed has a body of type T; otherwise the expansion thm will fail later on *) fun type_test (T, lbnos, apsns) = let val (_, U: typ, _) = nth apsns (foldl1 Int.min lbnos) in T = U end; (************************************************************************* Create a "split_pack". thm : the relevant split-theorem, i.e. P(...) == rhs , where P(...) is of the form P( Const(key,...) $ t_1 $ ... $ t_n ) (e.g. key = "if") T : type of P(...) T' : type of term to be scanned n : number of arguments expected by Const(key,...) ts : list of arguments actually found apsns : list of tuples of the form (T,U,pos), one tuple for each abstraction that is encountered on the way to the position where Const(key, ...) $ ... occurs, where T : type of the variable bound by the abstraction U : type of the abstraction's body pos : "path" leading to the body of the abstraction pos : "path" leading to the position where Const(key, ...) $ ... occurs. TB : type of Const(key,...) $ t_1 $ ... $ t_n t : the term Const(key,...) $ t_1 $ ... $ t_n A split pack is a tuple of the form (thm, apsns, pos, TB, tt) Note : apsns is reversed, so that the outermost quantifier's position comes first ! If the terms in ts don't contain variables bound by other than meta-quantifiers, apsns is empty, because no further lifting is required before applying the split-theorem. ******************************************************************************) fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) = if n > length ts then [] else let val lev = length apsns val lbnos = fold add_lbnos (take n ts) [] val flbnos = filter (fn i => i < lev) lbnos val tt = incr_boundvars (~lev) t in if null flbnos then if T = T' then [(thm,[],pos,TB,tt)] else [] else if type_test(T,flbnos,apsns) then [(thm, rev apsns,pos,TB,tt)] else [] end; (**************************************************************************** Recursively scans term for occurrences of Const(key,...) $ ... Returns a list of "split-packs" (one for each occurrence of Const(key,...) ) cmap : association list of split-theorems that should be tried. The elements have the format (key,(thm,T,n)) , where key : the theorem's key constant ( Const(key,...) $ ... ) thm : the theorem itself T : type of P( Const(key,...) $ ... ) n : number of arguments expected by Const(key,...) Ts : types of parameters t : the term to be scanned ******************************************************************************) (* Simplified first-order matching; assumes that all Vars in the pattern are distinct; see Pure/pattern.ML for the full version; *) local exception MATCH in fun typ_match thy (tyenv, TU) = Sign.typ_match thy TU tyenv handle Type.TYPE_MATCH => raise MATCH; fun fomatch thy args = let fun mtch tyinsts = fn (Ts, Var(_,T), t) => typ_match thy (tyinsts, (T, fastype_of1(Ts,t))) | (_, Free (a,T), Free (b,U)) => if a=b then typ_match thy (tyinsts,(T,U)) else raise MATCH | (_, Const (a,T), Const (b,U)) => if a=b then typ_match thy (tyinsts,(T,U)) else raise MATCH | (_, Bound i, Bound j) => if i=j then tyinsts else raise MATCH | (Ts, Abs(_,T,t), Abs(_,U,u)) => mtch (typ_match thy (tyinsts,(T,U))) (U::Ts,t,u) | (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u) | _ => raise MATCH in (mtch Vartab.empty args; true) handle MATCH => false end; end; fun split_posns (cmap : (string * (typ * term * thm * typ * int) list) list) thy Ts t = let val T' = fastype_of1 (Ts, t); fun posns Ts pos apsns (Abs (_, T, t)) = let val U = fastype_of1 (T::Ts,t) in posns (T::Ts) (0::pos) ((T, U, pos)::apsns) t end | posns Ts pos apsns t = let val (h, ts) = strip_comb t fun iter t (i, a) = (i+1, (posns Ts (i::pos) apsns t) @ a); val a = case h of Const(c, cT) => let fun find [] = [] | find ((gcT, pat, thm, T, n)::tups) = let val t2 = list_comb (h, take n ts) in if Sign.typ_instance thy (cT, gcT) andalso fomatch thy (Ts, pat, t2) then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2) else find tups end in find (these (AList.lookup (op =) cmap c)) end | _ => [] in snd (fold iter ts (0, a)) end in posns Ts [] [] t end; fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) = prod_ord (int_ord o apply2 length) (order o apply2 length) ((ps, pos), (qs, qos)); (************************************************************ call split_posns with appropriate parameters *************************************************************) fun select thy cmap state i = let val goal = Thm.term_of (Thm.cprem_of state i); val Ts = rev (map #2 (Logic.strip_params goal)); val _ $ t $ _ = Logic.strip_assums_concl goal; in (Ts, t, sort shorter (split_posns cmap thy Ts t)) end; fun exported_split_posns cmap thy Ts t = sort shorter (split_posns cmap thy Ts t); (************************************************************* instantiate lift theorem if t is of the form ... ( Const(...,...) $ Abs( .... ) ) ... then P = %a. ... ( Const(...,...) $ a ) ... where a has type T --> U Ts : types of parameters t : lefthand side of meta-equality in subgoal the split theorem is applied to (see cmap) T,U,pos : see mk_split_pack state : current proof state i : no. of subgoal **************************************************************) fun inst_lift ctxt Ts t (T, U, pos) state i = let val (cntxt, u) = mk_cntxt t pos (T --> U); val trlift' = Thm.lift_rule (Thm.cprem_of state i) (Thm.rename_boundvars abs_lift u trlift); val (Var (P, _), _) = strip_comb (fst (Logic.dest_equals (Logic.strip_assums_concl (Thm.prop_of trlift')))); in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] trlift' end; (************************************************************* instantiate split theorem Ts : types of parameters t : lefthand side of meta-equality in subgoal the split theorem is applied to (see cmap) tt : the term Const(key,..) $ ... thm : the split theorem TB : type of body of P(...) state : current proof state i : number of subgoal **************************************************************) fun inst_split ctxt Ts t tt thm TB state i = let val thm' = Thm.lift_rule (Thm.cprem_of state i) thm; val (Var (P, _), _) = strip_comb (fst (Logic.dest_equals (Logic.strip_assums_concl (Thm.prop_of thm')))); val cntxt = mk_cntxt_splitthm t tt TB; in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] thm' end; (***************************************************************************** The split-tactic splits : list of split-theorems to be tried i : number of subgoal the tactic should be applied to *****************************************************************************) fun split_tac _ [] i = no_tac | split_tac ctxt splits i = let val cmap = cmap_of_split_thms splits fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift ctxt Ts t p st i, 2) i st fun lift_split_tac state = let val (Ts, t, splits) = select (Proof_Context.theory_of ctxt) cmap state i in case splits of [] => no_tac state | (thm, apsns, pos, TB, tt)::_ => (case apsns of [] => compose_tac ctxt (false, inst_split ctxt Ts t tt thm TB state i, 0) i state | p::_ => EVERY [lift_tac Ts t p, resolve_tac ctxt [reflexive_thm] (i+1), lift_split_tac] state) end in COND (has_fewer_prems i) no_tac (resolve_tac ctxt [meta_iffD] i THEN lift_split_tac) end; in (split_tac, exported_split_posns) end; (* mk_case_split_tac *) val (split_tac, split_posns) = mk_case_split_tac int_ord; val (split_inside_tac, _) = mk_case_split_tac (rev_order o int_ord); (***************************************************************************** The split-tactic for premises splits : list of split-theorems to be tried ****************************************************************************) fun split_asm_tac _ [] = K no_tac | split_asm_tac ctxt splits = let val cname_list = map (fst o fst o split_thm_info) splits; fun tac (t,i) = let val n = find_index (exists_Const (member (op =) cname_list o #1)) (Logic.strip_assums_hyp t); fun first_prem_is_disj (Const (\<^const_name>\Pure.imp\, _) $ (Const (c, _) $ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or | first_prem_is_disj (Const(\<^const_name>\Pure.all\,_)$Abs(_,_,t)) = first_prem_is_disj t | first_prem_is_disj _ = false; (* does not work properly if the split variable is bound by a quantifier *) fun flat_prems_tac i = SUBGOAL (fn (t,i) => (if first_prem_is_disj t then EVERY[eresolve_tac ctxt [Data.disjE] i, rotate_tac ~1 i, rotate_tac ~1 (i+1), flat_prems_tac (i+1)] else all_tac) THEN REPEAT (eresolve_tac ctxt [Data.conjE,Data.exE] i) THEN REPEAT (dresolve_tac ctxt [Data.notnotD] i)) i; in if n<0 then no_tac else (DETERM (EVERY' [rotate_tac n, eresolve_tac ctxt [Data.contrapos2], split_tac ctxt splits, rotate_tac ~1, eresolve_tac ctxt [Data.contrapos], rotate_tac ~1, flat_prems_tac] i)) end; in SUBGOAL tac end; fun gen_split_tac _ [] = K no_tac | gen_split_tac ctxt (split::splits) = let val (_,asm) = split_thm_info split in (if asm then split_asm_tac else split_tac) ctxt [split] ORELSE' gen_split_tac ctxt splits end; (** declare split rules **) (* add_split / del_split *) fun string_of_typ (Type (s, Ts)) = (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s | string_of_typ _ = "_"; fun split_name (name, T) asm = "split " ^ (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T; fun gen_add_split bang split ctxt = let val (name, asm) = split_thm_info split val split0 = Thm.trim_context split fun tac ctxt' = let val split' = Thm.transfer' ctxt' split0 in (if asm then split_asm_tac ctxt' [split'] else if bang then split_tac ctxt' [split'] THEN_ALL_NEW TRY o (SELECT_GOAL (Data.safe_tac ctxt')) else split_tac ctxt' [split']) end in Simplifier.addloop (ctxt, (split_name name asm, tac)) end; val add_split = gen_add_split false; val add_split_bang = gen_add_split true; fun del_split split ctxt = let val (name, asm) = split_thm_info split in Simplifier.delloop (ctxt, split_name name asm) end; (* attributes *) val splitN = "split"; fun split_add bang = Simplifier.attrib (gen_add_split bang); val split_del = Simplifier.attrib del_split; val add_del = Scan.lift (Args.bang >> K (split_add true) || Args.del >> K split_del || Scan.succeed (split_add false)); val _ = Theory.setup (Attrib.setup \<^binding>\split\ add_del "declare case split rule"); (* methods *) val split_modifiers = [Args.$$$ splitN -- Args.colon >> K (Method.modifier (split_add false) \<^here>), Args.$$$ splitN -- Args.bang_colon >> K (Method.modifier (split_add true) \<^here>), Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del \<^here>)]; val _ = Theory.setup (Method.setup \<^binding>\split\ (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ctxt ths))) "apply case split rule"); end; diff --git a/src/Tools/induct.ML b/src/Tools/induct.ML --- a/src/Tools/induct.ML +++ b/src/Tools/induct.ML @@ -1,975 +1,971 @@ (* Title: Tools/induct.ML Author: Markus Wenzel, TU Muenchen Proof by cases, induction, and coinduction. *) signature INDUCT_ARGS = sig val cases_default: thm val atomize: thm list val rulify: thm list val rulify_fallback: thm list val equal_def: thm val dest_def: term -> (term * term) option val trivial_tac: Proof.context -> int -> tactic end; signature INDUCT = sig (*rule declarations*) val vars_of: term -> term list val dest_rules: Proof.context -> {type_cases: (string * thm) list, pred_cases: (string * thm) list, type_induct: (string * thm) list, pred_induct: (string * thm) list, type_coinduct: (string * thm) list, pred_coinduct: (string * thm) list} val print_rules: Proof.context -> unit val lookup_casesT: Proof.context -> string -> thm option val lookup_casesP: Proof.context -> string -> thm option val lookup_inductT: Proof.context -> string -> thm option val lookup_inductP: Proof.context -> string -> thm option val lookup_coinductT: Proof.context -> string -> thm option val lookup_coinductP: Proof.context -> string -> thm option val find_casesT: Proof.context -> typ -> thm list val find_casesP: Proof.context -> term -> thm list val find_inductT: Proof.context -> typ -> thm list val find_inductP: Proof.context -> term -> thm list val find_coinductT: Proof.context -> typ -> thm list val find_coinductP: Proof.context -> term -> thm list val cases_type: string -> attribute val cases_pred: string -> attribute val cases_del: attribute val induct_type: string -> attribute val induct_pred: string -> attribute val induct_del: attribute val coinduct_type: string -> attribute val coinduct_pred: string -> attribute val coinduct_del: attribute val map_simpset: (Proof.context -> Proof.context) -> Context.generic -> Context.generic val induct_simp_add: attribute val induct_simp_del: attribute val no_simpN: string val casesN: string val inductN: string val coinductN: string val typeN: string val predN: string val setN: string (*proof methods*) val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic val add_defs: (binding option * (term * bool)) option list -> Proof.context -> (term option list * thm list) * Proof.context val atomize_term: Proof.context -> term -> term val atomize_cterm: Proof.context -> conv val atomize_tac: Proof.context -> int -> tactic val inner_atomize_tac: Proof.context -> int -> tactic val rulified_term: Proof.context -> thm -> term val rulify_tac: Proof.context -> int -> tactic val simplified_rule: Proof.context -> thm -> thm val simplify_tac: Proof.context -> int -> tactic val trivial_tac: Proof.context -> int -> tactic val rotate_tac: int -> int -> int -> tactic val internalize: Proof.context -> int -> thm -> thm val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq val cases_context_tactic: bool -> term option list list -> thm option -> thm list -> int -> context_tactic val cases_tac: Proof.context -> bool -> term option list list -> thm option -> thm list -> int -> tactic val get_inductT: Proof.context -> term option list list -> thm list list val gen_induct_context_tactic: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) -> bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> context_tactic val gen_induct_tac: Proof.context -> ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) -> bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> tactic val induct_context_tactic: bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> context_tactic val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> tactic val coinduct_context_tactic: term option list -> term option list -> thm option -> thm list -> int -> context_tactic val coinduct_tac: Proof.context -> term option list -> term option list -> thm option -> thm list -> int -> tactic val gen_induct_setup: binding -> (bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> context_tactic) -> local_theory -> local_theory end; functor Induct(Induct_Args: INDUCT_ARGS): INDUCT = struct (** variables -- ordered left-to-right, preferring right **) fun vars_of tm = rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) tm [])); local val mk_var = Net.encode_type o #2 o Term.dest_Var; fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty => raise THM ("No variables in conclusion of rule", 0, [thm]); in fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty => raise THM ("No variables in major premise of rule", 0, [thm]); val left_var_concl = concl_var hd; val right_var_concl = concl_var List.last; end; (** constraint simplification **) (* rearrange parameters and premises to allow application of one-point-rules *) fun swap_params_conv ctxt i j cv = let fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt | conv1 k ctxt = Conv.rewr_conv @{thm swap_params} then_conv Conv.forall_conv (conv1 (k - 1) o snd) ctxt; fun conv2 0 ctxt = conv1 j ctxt | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt; in conv2 i ctxt end; fun swap_prems_conv 0 = Conv.all_conv | swap_prems_conv i = Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv Conv.rewr_conv Drule.swap_prems_eq; fun find_eq ctxt t = let val l = length (Logic.strip_params t); val Hs = Logic.strip_assums_hyp t; fun find (i, t) = (case Induct_Args.dest_def (Object_Logic.drop_judgment ctxt t) of SOME (Bound j, _) => SOME (i, j) | SOME (_, Bound j) => SOME (i, j) | _ => NONE); in (case get_first find (map_index I Hs) of NONE => NONE | SOME (0, 0) => NONE | SOME (i, j) => SOME (i, l - j - 1, j)) end; fun mk_swap_rrule ctxt ct = (case find_eq ctxt (Thm.term_of ct) of NONE => NONE | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); val rearrange_eqs_simproc = Simplifier.make_simproc \<^context> "rearrange_eqs" {lhss = [\<^term>\Pure.all (t :: 'a::{} \ prop)\], proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct}; (* rotate k premises to the left by j, skipping over first j premises *) fun rotate_conv 0 _ 0 = Conv.all_conv | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1) | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k); fun rotate_tac _ 0 = K all_tac | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv j (length (Logic.strip_assums_hyp goal) - j - k) k) i); (* rulify operators around definition *) fun rulify_defs_conv ctxt ct = if exists_subterm (is_some o Induct_Args.dest_def) (Thm.term_of ct) andalso not (is_some (Induct_Args.dest_def (Object_Logic.drop_judgment ctxt (Thm.term_of ct)))) then (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt)) (Conv.try_conv (rulify_defs_conv ctxt)) else_conv Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv Conv.try_conv (rulify_defs_conv ctxt)) ct else Conv.no_conv ct; (** induct data **) (* rules *) type rules = (string * thm) Item_Net.T; fun init_rules index : rules = Item_Net.init (fn ((s1, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2)) (single o index); fun filter_rules (rs: rules) th = filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs); fun pretty_rules ctxt kind rs = let val thms = map snd (Item_Net.content rs) in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end; (* context data *) structure Data = Generic_Data ( type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset; val empty = ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)), simpset_of (empty_simpset \<^context> addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq])); val extend = I; fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1), ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) = ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)), (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)), (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)), merge_ss (simpset1, simpset2)); ); val get_local = Data.get o Context.Proof; fun dest_rules ctxt = let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in {type_cases = Item_Net.content casesT, pred_cases = Item_Net.content casesP, type_induct = Item_Net.content inductT, pred_induct = Item_Net.content inductP, type_coinduct = Item_Net.content coinductT, pred_coinduct = Item_Net.content coinductP} end; fun print_rules ctxt = let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in [pretty_rules ctxt "coinduct type:" coinductT, pretty_rules ctxt "coinduct pred:" coinductP, pretty_rules ctxt "induct type:" inductT, pretty_rules ctxt "induct pred:" inductP, pretty_rules ctxt "cases type:" casesT, pretty_rules ctxt "cases pred:" casesP] |> Pretty.writeln_chunks end; val _ = Outer_Syntax.command \<^command_keyword>\print_induct_rules\ "print induction and cases rules" (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of))); (* access rules *) local fun lookup_rule which ctxt = AList.lookup (op =) (Item_Net.content (which (get_local ctxt))) #> Option.map (Thm.transfer' ctxt); fun find_rules which how ctxt x = Item_Net.retrieve (which (get_local ctxt)) (how x) |> map (Thm.transfer' ctxt o snd); in val lookup_casesT = lookup_rule (#1 o #1); val lookup_casesP = lookup_rule (#2 o #1); val lookup_inductT = lookup_rule (#1 o #2); val lookup_inductP = lookup_rule (#2 o #2); val lookup_coinductT = lookup_rule (#1 o #3); val lookup_coinductP = lookup_rule (#2 o #3); val find_casesT = find_rules (#1 o #1) Net.encode_type; val find_casesP = find_rules (#2 o #1) I; val find_inductT = find_rules (#1 o #2) Net.encode_type; val find_inductP = find_rules (#2 o #2) I; val find_coinductT = find_rules (#1 o #3) Net.encode_type; val find_coinductP = find_rules (#2 o #3) I; end; (** attributes **) local fun mk_att f g name = Thm.mixed_attribute (fn (context, thm) => let val thm' = g thm; val context' = if Thm.is_free_dummy thm then context else Data.map (f (name, Thm.trim_context thm')) context; in (context', thm') end); fun del_att which = Thm.declaration_attribute (fn th => Data.map (which (apply2 (fn rs => fold Item_Net.remove (filter_rules rs th) rs)))); fun add_casesT rule x = @{apply 4(1)} (apfst (Item_Net.update rule)) x; fun add_casesP rule x = @{apply 4(1)} (apsnd (Item_Net.update rule)) x; fun add_inductT rule x = @{apply 4(2)} (apfst (Item_Net.update rule)) x; fun add_inductP rule x = @{apply 4(2)} (apsnd (Item_Net.update rule)) x; fun add_coinductT rule x = @{apply 4(3)} (apfst (Item_Net.update rule)) x; fun add_coinductP rule x = @{apply 4(3)} (apsnd (Item_Net.update rule)) x; val consumes0 = Rule_Cases.default_consumes 0; val consumes1 = Rule_Cases.default_consumes 1; in val cases_type = mk_att add_casesT consumes0; val cases_pred = mk_att add_casesP consumes1; val cases_del = del_att @{apply 4(1)}; val induct_type = mk_att add_inductT consumes0; val induct_pred = mk_att add_inductP consumes1; val induct_del = del_att @{apply 4(2)}; val coinduct_type = mk_att add_coinductT consumes0; val coinduct_pred = mk_att add_coinductP consumes1; val coinduct_del = del_att @{apply 4(3)}; fun map_simpset f context = context |> (Data.map o @{apply 4(4)} o Simplifier.simpset_map (Context.proof_of context)) f; fun induct_simp f = Thm.declaration_attribute (fn thm => map_simpset (fn ctxt => f (ctxt, [thm]))); val induct_simp_add = induct_simp (op addsimps); val induct_simp_del = induct_simp (op delsimps); end; (** attribute syntax **) val no_simpN = "no_simp"; val casesN = "cases"; val inductN = "induct"; val coinductN = "coinduct"; val typeN = "type"; val predN = "pred"; val setN = "set"; local fun spec k arg = Scan.lift (Args.$$$ k -- Args.colon) |-- arg || Scan.lift (Args.$$$ k) >> K ""; fun attrib add_type add_pred del = spec typeN (Args.type_name {proper = false, strict = false}) >> add_type || spec predN (Args.const {proper = false, strict = false}) >> add_pred || spec setN (Args.const {proper = false, strict = false}) >> add_pred || Scan.lift Args.del >> K del; in val _ = Theory.local_setup (Attrib.local_setup \<^binding>\cases\ (attrib cases_type cases_pred cases_del) "declaration of cases rule" #> Attrib.local_setup \<^binding>\induct\ (attrib induct_type induct_pred induct_del) "declaration of induction rule" #> Attrib.local_setup \<^binding>\coinduct\ (attrib coinduct_type coinduct_pred coinduct_del) "declaration of coinduction rule" #> Attrib.local_setup \<^binding>\induct_simp\ (Attrib.add_del induct_simp_add induct_simp_del) "declaration of rules for simplifying induction or cases rules"); end; (** method utils **) (* alignment *) fun align_left msg xs ys = let val m = length xs and n = length ys in if m < n then error msg else (take n xs ~~ ys) end; fun align_right msg xs ys = let val m = length xs and n = length ys in if m < n then error msg else (drop (m - n) xs ~~ ys) end; (* prep_inst *) fun prep_inst ctxt align tune (tm, ts) = let fun prep_var (Var (x, xT), SOME t) = let val ct = Thm.cterm_of ctxt (tune t); val tT = Thm.typ_of_cterm ct; in if Type.could_unify (tT, xT) then SOME (x, ct) else error (Pretty.string_of (Pretty.block [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt tT])) end | prep_var (_, NONE) = NONE; val xs = vars_of tm; in align "Rule has fewer variables than instantiations given" xs ts |> map_filter prep_var end; (* trace_rules *) fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") | trace_rules ctxt _ rules = Method.trace ctxt rules; (* mark equality constraints in cases rule *) val equal_def' = Thm.symmetric Induct_Args.equal_def; fun mark_constraints n ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt false [equal_def']))) ctxt)); fun unmark_constraints ctxt = Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]); (* simplify *) fun simplify_conv' ctxt = Simplifier.full_rewrite (put_simpset (#4 (get_local ctxt)) ctxt); fun simplify_conv ctxt ct = if exists_subterm (is_some o Induct_Args.dest_def) (Thm.term_of ct) then (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct else Conv.all_conv ct; fun gen_simplified_rule cv ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (cv ctxt)); val simplified_rule' = gen_simplified_rule simplify_conv'; val simplified_rule = gen_simplified_rule simplify_conv; fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt); val trivial_tac = Induct_Args.trivial_tac; (** cases method **) (* rule selection scheme: cases - default case split `A t` cases ... - predicate/set cases cases t - type cases ... cases ... r - explicit rule *) local fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t) | get_casesT _ _ = []; fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact) | get_casesP _ _ = []; in fun cases_context_tactic simp insts opt_rule facts i : context_tactic = fn (ctxt, st) => let fun inst_rule r = (if null insts then r else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts |> maps (prep_inst ctxt align_left I) |> infer_instantiate ctxt) r) |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt |> pair (Rule_Cases.get r); val (opt_rule', facts') = (case (opt_rule, facts) of (NONE, th :: ths) => if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths) else (opt_rule, facts) | _ => (opt_rule, facts)); val ruleq = (case opt_rule' of SOME r => Seq.single (inst_rule r) | NONE => (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default]) |> tap (trace_rules ctxt casesN) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); in ruleq |> Seq.maps (Rule_Cases.consume ctxt [] facts') |> Seq.maps (fn ((cases, (_, facts'')), rule) => let val rule' = rule |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt); in CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params rule')) cases) ((Method.insert_tac ctxt facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW (if simp then TRY o trivial_tac ctxt else K all_tac)) i) (ctxt, st) end) end; fun cases_tac ctxt x1 x2 x3 x4 x5 = NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5); end; (** induct method **) val conjunction_congs = @{thms Pure.all_conjunction imp_conjunction}; (* atomize *) fun atomize_term ctxt = Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize [] #> Object_Logic.drop_judgment ctxt; fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize; fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize; fun inner_atomize_tac ctxt = rewrite_goal_tac ctxt (map Thm.symmetric conjunction_congs) THEN' atomize_tac ctxt; (* rulify *) fun rulify_term thy = Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #> Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback []; fun rulified_term ctxt thm = let val rulify = rulify_term (Proof_Context.theory_of ctxt); val (As, B) = Logic.strip_horn (Thm.prop_of thm); in Logic.list_implies (map rulify As, rulify B) end; fun rulify_tac ctxt = rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN' rewrite_goal_tac ctxt Induct_Args.rulify_fallback THEN' Goal.conjunction_tac THEN_ALL_NEW (rewrite_goal_tac ctxt @{thms Pure.conjunction_imp} THEN' Goal.norm_hhf_tac ctxt); (* prepare rule *) fun rule_instance ctxt inst rule = infer_instantiate ctxt (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule; fun internalize ctxt k th = th |> Thm.permute_prems 0 k |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) (atomize_cterm ctxt)); (* guess rule instantiation -- cannot handle pending goal parameters *) local fun insts_env ctxt env = let val pairs = Vartab.dest (Envir.term_env env); val types = Vartab.dest (Envir.type_env env); val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs; val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts; val instT = TVars.build (types |> fold (fn (ai, (S, T)) => TVars.add ((ai, S), Thm.ctyp_of ctxt T))); val inst = Vars.build (fold2 (fn x => fn t => Vars.add (x, t)) xs ts); in (instT, inst) end; in fun guess_instance ctxt rule i st = let val maxidx = Thm.maxidx_of st; val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal)); in if not (null params) then (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ commas_quote (map (Syntax.string_of_term ctxt o Syntax_Trans.mark_bound_abs) params)); Seq.single rule) else let val rule' = Thm.incr_indexes (maxidx + 1) rule; val concl = Logic.strip_assums_concl goal; in Unify.smash_unifiers (Context.Proof ctxt) [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule')) |> Seq.map (fn env => Drule.instantiate_normalize (insts_env ctxt env) rule') end end handle General.Subscript => Seq.empty; end; (* special renaming of rule parameters *) fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = let val x = Name.clean (Variable.revert_fixed ctxt z); fun index _ [] = [] | index i (y :: ys) = if x = y then x ^ string_of_int i :: index (i + 1) ys else y :: index i ys; fun rename_params [] = [] | rename_params ((y, Type (U, _)) :: ys) = (if U = T then x else y) :: rename_params ys | rename_params ((y, _) :: ys) = y :: rename_params ys; fun rename_asm A = let val xs = rename_params (Logic.strip_params A); val xs' = (case filter (fn x' => x' = x) xs of [] => xs | [_] => xs | _ => index 1 xs); in Logic.list_rename_params xs' A end; fun rename_prop prop = let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename_asm As, C) end; val thm' = Thm.renamed_prop (rename_prop (Thm.prop_of thm)) thm; in [Rule_Cases.save thm thm'] end | special_rename_params _ _ ths = ths; (* arbitrary_tac *) local -fun goal_prefix k ((c as Const (\<^const_name>\Pure.all\, _)) $ Abs (a, T, B)) = - c $ Abs (a, T, goal_prefix k B) +fun goal_prefix k ((c as \<^Const_>\Pure.all _\) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B) | goal_prefix 0 _ = Term.dummy_prop - | goal_prefix k ((c as Const (\<^const_name>\Pure.imp\, _)) $ A $ B) = - c $ A $ goal_prefix (k - 1) B + | goal_prefix k ((c as \<^Const_>\Pure.imp\) $ A $ B) = c $ A $ goal_prefix (k - 1) B | goal_prefix _ _ = Term.dummy_prop; -fun goal_params k (Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, B)) = goal_params k B + 1 +fun goal_params k \<^Const_>\Pure.all _ for \Abs (_, _, B)\\ = goal_params k B + 1 | goal_params 0 _ = 0 - | goal_params k (Const (\<^const_name>\Pure.imp\, _) $ _ $ B) = goal_params (k - 1) B + | goal_params k \<^Const_>\Pure.imp for _ B\ = goal_params (k - 1) B | goal_params _ _ = 0; fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => let val v = Free (x, T); fun spec_rule prfx (xs, body) = @{thm Pure.meta_spec} |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1) |> Thm.lift_rule (Thm.cterm_of ctxt prfx) |> `(Thm.prop_of #> Logic.strip_assums_concl) |-> (fn pred $ arg => infer_instantiate ctxt [(#1 (dest_Var (head_of pred)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, body))), (#1 (dest_Var (head_of arg)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, v)))]); - fun goal_concl k xs (Const (\<^const_name>\Pure.all\, _) $ Abs (a, T, B)) = - goal_concl k ((a, T) :: xs) B + fun goal_concl k xs \<^Const_>\Pure.all _ for \Abs (a, T, B)\\ = goal_concl k ((a, T) :: xs) B | goal_concl 0 xs B = if not (Term.exists_subterm (fn t => t aconv v) B) then NONE else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B)) - | goal_concl k xs (Const (\<^const_name>\Pure.imp\, _) $ _ $ B) = - goal_concl (k - 1) xs B + | goal_concl k xs \<^Const_>\Pure.imp for _ B\ = goal_concl (k - 1) xs B | goal_concl _ _ _ = NONE; in (case goal_concl n [] goal of SOME concl => (compose_tac ctxt (false, spec_rule (goal_prefix n goal) concl, 1) THEN' resolve_tac ctxt [asm_rl]) i | NONE => all_tac) end); fun miniscope_tac p = CONVERSION o Conv.params_conv p (fn ctxt => Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]); in fun arbitrary_tac _ _ [] = K all_tac | arbitrary_tac ctxt n xs = SUBGOAL (fn (goal, i) => (EVERY' (map (meta_spec_tac ctxt n) xs) THEN' (miniscope_tac (goal_params n goal) ctxt)) i); end; (* add_defs *) fun add_defs def_insts = let fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt) | add (SOME (SOME x, (t, _))) ctxt = let val ([(lhs, (_, th))], ctxt') = Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt in ((SOME lhs, [th]), ctxt') end | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt) | add (SOME (NONE, (t, _))) ctxt = let val (s, _) = Name.variant "x" (Variable.names_of ctxt); val x = Binding.name s; val ([(lhs, (_, th))], ctxt') = ctxt |> Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))]; in ((SOME lhs, [th]), ctxt') end | add NONE ctxt = ((NONE, []), ctxt); in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; (* induct_tac *) (* rule selection scheme: `A x` induct ... - predicate/set induction induct x - type induction ... induct ... r - explicit rule *) fun get_inductT ctxt insts = fold_rev (map_product cons) (insts |> map ((fn [] => NONE | ts => List.last ts) #> (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #> find_inductT ctxt)) [[]] |> filter_out (forall Rule_Cases.is_inner_rule); fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) | get_inductP _ _ = []; fun gen_induct_context_tactic mod_cases simp def_insts arbitrary taking opt_rule facts = CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) => let val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs; fun inst_rule (concls, r) = (if null insts then `Rule_Cases.get r else (align_left "Rule has fewer conclusions than arguments given" (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts |> maps (prep_inst ctxt align_right (atomize_term ctxt)) |> infer_instantiate ctxt) r |> pair (Rule_Cases.get r)) |> mod_cases |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); val ruleq = (case opt_rule of SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs)) | NONE => (get_inductP ctxt facts @ map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts)) |> map_filter (Rule_Cases.mutual_rule ctxt) |> tap (trace_rules ctxt inductN o map #2) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); fun rule_cases ctxt rule cases = let val rule' = Rule_Cases.internalize_params rule; val rule'' = rule' |> simp ? simplified_rule ctxt; val nonames = map (fn ((cn, _), cls) => ((cn, []), cls)); val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases; in Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end; fun context_tac _ _ = ruleq |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts) |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => (CONJUNCTS (ALLGOALS let val adefs = nth_list atomized_defs (j - 1); val frees = fold (Term.add_frees o Thm.prop_of) adefs []; val xs = nth_list arbitrary (j - 1); val k = nth concls (j - 1) + more_consumes; in Method.insert_tac defs_ctxt (more_facts @ adefs) THEN' (if simp then rotate_tac k (length adefs) THEN' arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @) else arbitrary_tac defs_ctxt k xs) end) THEN' inner_atomize_tac defs_ctxt) j)) THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' => guess_instance ctxt (internalize ctxt more_consumes rule) i st' |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking)) |> Seq.maps (fn rule' => CONTEXT_CASES (rule_cases ctxt rule' cases) (resolve_tac ctxt [rule'] i THEN PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st')))); in (context_tac CONTEXT_THEN_ALL_NEW ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac) THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st) end) val induct_context_tactic = gen_induct_context_tactic I; fun gen_induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 x8 = NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8); fun induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 = NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7); (** coinduct method **) (* rule selection scheme: goal "A x" coinduct ... - predicate/set coinduction coinduct x - type coinduction coinduct ... r - explicit rule *) local fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t) | get_coinductT _ _ = []; fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal); fun main_prop_of th = if Rule_Cases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th; in fun coinduct_context_tactic inst taking opt_rule facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => let fun inst_rule r = if null inst then `Rule_Cases.get r else infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r |> pair (Rule_Cases.get r); in (case opt_rule of SOME r => Seq.single (inst_rule r) | NONE => (get_coinductP ctxt goal @ get_coinductT ctxt inst) |> tap (trace_rules ctxt coinductN) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)) |> Seq.maps (Rule_Cases.consume ctxt [] facts) |> Seq.maps (fn ((cases, (_, more_facts)), rule) => guess_instance ctxt rule i st |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking)) |> Seq.maps (fn rule' => CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params rule')) cases) (Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st))) end); fun coinduct_tac ctxt x1 x2 x3 x4 x5 = NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5); end; (** concrete syntax **) val arbitraryN = "arbitrary"; val takingN = "taking"; val ruleN = "rule"; local fun single_rule [rule] = rule | single_rule _ = error "Single rule expected"; fun named_rule k arg get = Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|-- (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name => (case get (Context.proof_of context) name of SOME x => x | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); fun rule get_type get_pred = named_rule typeN (Args.type_name {proper = false, strict = false}) get_type || named_rule predN (Args.const {proper = false, strict = false}) get_pred || named_rule setN (Args.const {proper = false, strict = false}) get_pred || Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms; val cases_rule = rule lookup_casesT lookup_casesP >> single_rule; val induct_rule = rule lookup_inductT lookup_inductP; val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule; val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; val inst' = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> (SOME o rpair false) || Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --| Scan.lift (Args.$$$ ")"); val def_inst = ((Scan.lift (Args.binding --| (Args.$$$ "\" || Args.$$$ "==")) >> SOME) -- (Args.term >> rpair false)) >> SOME || inst' >> Option.map (pair NONE); val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN || Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan; val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |-- Parse.and_list1' (Scan.repeat (unless_more_args free))) []; val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |-- Scan.repeat1 (unless_more_args inst)) []; in fun gen_induct_setup binding tac = Method.local_setup binding (Scan.lift (Args.mode no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- (arbitrary -- taking -- Scan.option induct_rule)) >> (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn _ => fn facts => Seq.DETERM (tac (not no_simp) insts arbitrary taking opt_rule facts 1))) "induction on types or predicates/sets"; val _ = Theory.local_setup (Method.local_setup \<^binding>\cases\ (Scan.lift (Args.mode no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >> (fn (no_simp, (insts, opt_rule)) => fn _ => CONTEXT_METHOD (fn facts => Seq.DETERM (cases_context_tactic (not no_simp) insts opt_rule facts 1)))) "case analysis on types or predicates/sets" #> gen_induct_setup \<^binding>\induct\ induct_context_tactic #> Method.local_setup \<^binding>\coinduct\ (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >> (fn ((insts, taking), opt_rule) => fn _ => fn facts => Seq.DETERM (coinduct_context_tactic insts taking opt_rule facts 1))) "coinduction on types or predicates/sets"); end; end; diff --git a/src/Tools/misc_legacy.ML b/src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML +++ b/src/Tools/misc_legacy.ML @@ -1,256 +1,256 @@ (* Title: Tools/misc_legacy.ML Misc legacy stuff -- to be phased out eventually. *) signature MISC_LEGACY = sig val add_term_names: term * string list -> string list val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list val add_term_tfrees: term * (string * sort) list -> (string * sort) list val typ_tvars: typ -> (indexname * sort) list val term_tfrees: term -> (string * sort) list val term_tvars: term -> (indexname * sort) list val add_term_vars: term * term list -> term list val term_vars: term -> term list val add_term_frees: term * term list -> term list val term_frees: term -> term list val mk_defpair: term * term -> string * term val get_def: theory -> xstring -> thm val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm) end; structure Misc_Legacy: MISC_LEGACY = struct (*iterate a function over all types in a term*) fun it_term_types f = let fun iter(Const(_,T), a) = f(T,a) | iter(Free(_,T), a) = f(T,a) | iter(Var(_,T), a) = f(T,a) | iter(Abs(_,T,t), a) = iter(t,f(T,a)) | iter(f$u, a) = iter(f, iter(u, a)) | iter(Bound _, a) = a in iter end (*Accumulates the names in the term, suppressing duplicates. Includes Frees and Consts. For choosing unambiguous bound var names.*) fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs | add_term_names (Free(a,_), bs) = insert (op =) a bs | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) | add_term_names (_, bs) = bs; (*Accumulates the TVars in a type, suppressing duplicates.*) fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts | add_typ_tvars(TFree(_),vs) = vs | add_typ_tvars(TVar(v),vs) = insert (op =) v vs; (*Accumulates the TFrees in a type, suppressing duplicates.*) fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs | add_typ_tfree_names(TVar(_),fs) = fs; fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs | add_typ_tfrees(TVar(_),fs) = fs; (*Accumulates the TVars in a term, suppressing duplicates.*) val add_term_tvars = it_term_types add_typ_tvars; (*Accumulates the TFrees in a term, suppressing duplicates.*) val add_term_tfrees = it_term_types add_typ_tfrees; val add_term_tfree_names = it_term_types add_typ_tfree_names; (*Non-list versions*) fun typ_tfrees T = add_typ_tfrees(T,[]); fun typ_tvars T = add_typ_tvars(T,[]); fun term_tfrees t = add_term_tfrees(t,[]); fun term_tvars t = add_term_tvars(t,[]); (*Accumulates the Vars in the term, suppressing duplicates.*) fun add_term_vars (t, vars: term list) = case t of Var _ => Ord_List.insert Term_Ord.term_ord t vars | Abs (_,_,body) => add_term_vars(body,vars) | f$t => add_term_vars (f, add_term_vars(t, vars)) | _ => vars; fun term_vars t = add_term_vars(t,[]); (*Accumulates the Frees in the term, suppressing duplicates.*) fun add_term_frees (t, frees: term list) = case t of Free _ => Ord_List.insert Term_Ord.term_ord t frees | Abs (_,_,body) => add_term_frees(body,frees) | f$t => add_term_frees (f, add_term_frees(t, frees)) | _ => frees; fun term_frees t = add_term_frees(t,[]); fun mk_defpair (lhs, rhs) = (case Term.head_of lhs of Const (name, _) => (Thm.def_name (Long_Name.base_name name), Logic.mk_equals (lhs, rhs)) | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions METAHYPS (fn prems => tac prems) i converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new proof state A==>A, supplying A1,...,An as meta-level assumptions (in "prems"). The parameters x1,...,xm become free variables. If the resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) then it is lifted back into the original context, yielding k subgoals. Replaces unknowns in the context by Frees having the prefix METAHYP_ New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. DOES NOT HANDLE TYPE UNKNOWNS. NOTE: This version does not observe the proof context, and thus cannot work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for properly localized variants of the same idea. ****) local (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. Main difference from strip_assums concerns parameters: it replaces the bound variables by free variables. *) -fun strip_context_aux (params, Hs, Const (\<^const_name>\Pure.imp\, _) $ H $ B) = +fun strip_context_aux (params, Hs, \<^Const_>\Pure.imp for H B\) = strip_context_aux (params, H :: Hs, B) - | strip_context_aux (params, Hs, Const (\<^const_name>\Pure.all\,_) $ Abs (a, T, t)) = + | strip_context_aux (params, Hs, \<^Const_>\Pure.all _ for \Abs (a, T, t)\\) = let val (b, u) = Syntax_Trans.variant_abs (a, T, t) in strip_context_aux ((b, T) :: params, Hs, u) end | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); fun strip_context A = strip_context_aux ([], [], A); (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. Instantiates distinct free variables by terms of same type.*) fun free_instantiate ctpairs = forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); fun free_of s ((a, i), T) = Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T) fun mk_inst v = (Var v, free_of "METAHYP1_" v) fun metahyps_split_prem prem = let (*find all vars in the hyps -- should find tvars also!*) val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) [] val insts = map mk_inst hyps_vars (*replace the hyps_vars by Frees*) val prem' = subst_atomic insts prem val (params,hyps,concl) = strip_context prem' in (insts,params,hyps,concl) end; fun metahyps_aux_tac ctxt tacf (prem,gno) state = let val (insts,params,hyps,concl) = metahyps_split_prem prem val maxidx = Thm.maxidx_of state val chyps = map (Thm.cterm_of ctxt) hyps val hypths = map Thm.assume chyps val subprems = map (Thm.forall_elim_vars 0) hypths val fparams = map Free params val cparams = map (Thm.cterm_of ctxt) fparams fun swap_ctpair (t, u) = apply2 (Thm.cterm_of ctxt) (u, t) (*Subgoal variables: make Free; lift type over params*) fun mk_subgoal_inst concl_vars (v, T) = if member (op =) concl_vars (v, T) then ((v, T), true, free_of "METAHYP2_" (v, T)) else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) (*Instantiate subgoal vars by Free applied to params*) fun mk_inst (v, in_concl, u) = if in_concl then (v, Thm.cterm_of ctxt u) else (v, Thm.cterm_of ctxt (list_comb (u, fparams))) (*Restore Vars with higher type and index*) fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T)) else apply2 (Thm.cterm_of ctxt) (u, Var ((a, i + maxidx), U)) (*Embed B in the original context of params and hyps*) fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B)) (*Strip the context using elimination rules*) fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths (*A form of lifting that discharges assumptions.*) fun relift st = let val prop = Thm.prop_of st val subgoal_vars = (*Vars introduced in the subgoals*) fold Term.add_vars (Logic.strip_imp_prems prop) [] and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars val st' = Thm.instantiate (TVars.empty, Vars.build (fold (Vars.add o mk_inst) subgoal_insts)) st val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st') val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) in (*restore the unknowns to the hypotheses*) free_instantiate (map swap_ctpair insts @ map mk_subgoal_swap_ctpair subgoal_insts) (*discharge assumptions from state in same order*) (implies_intr_list emBs (forall_intr_list cparams (implies_intr_list chyps Cth))) end (*function to replace the current subgoal*) fun next st = Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} (false, relift st, Thm.nprems_of st) gno state in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end; in fun METAHYPS ctxt tacf n thm = SUBGOAL (metahyps_aux_tac ctxt tacf) n thm handle THM ("assume: variables", _, _) => Seq.empty end; (* generating identifiers -- often fresh *) local (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*) fun gensym_char i = if i<26 then chr (ord "A" + i) else if i<52 then chr (ord "a" + i - 26) else chr (ord "0" + i - 52); val char_vec = Vector.tabulate (62, gensym_char); fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n))); val gensym_seed = Synchronized.var "gensym_seed" (0: int); in fun gensym pre = Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1)); end; (*Convert all Vars in a theorem to Frees. Also return a function for reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) fun freeze_thaw_robust ctxt th = let val fth = Thm.legacy_freezeT th in case Thm.fold_terms {hyps = false} Term.add_vars fth [] of [] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*) | vars => let fun newName (ix,_) = (ix, gensym (string_of_indexname ix)) val alist = map newName vars fun mk_inst (v,T) = apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T)) val insts = map mk_inst vars fun thaw i th' = (*i is non-negative increment for Var indexes*) th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) in (Thm.instantiate (TVars.empty, Vars.build (fold (Vars.add o apfst (dest_Var o Thm.term_of)) insts)) fth, thaw) end end; end; diff --git a/src/Tools/nbe.ML b/src/Tools/nbe.ML --- a/src/Tools/nbe.ML +++ b/src/Tools/nbe.ML @@ -1,624 +1,624 @@ (* Title: Tools/nbe.ML Authors: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen Normalization by evaluation, based on generic code generator. *) signature NBE = sig val dynamic_conv: Proof.context -> conv val dynamic_value: Proof.context -> term -> term val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term datatype Univ = Const of int * Univ list (*named (uninterpreted) constants*) | DFree of string * int (*free (uninterpreted) dictionary parameters*) | BVar of int * Univ list | Abs of (int * (Univ list -> Univ)) * Univ list val apps: Univ -> Univ list -> Univ (*explicit applications*) val abss: int -> (Univ list -> Univ) -> Univ (*abstractions as closures*) val same: Univ * Univ -> bool val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context val trace: bool Config.T val add_const_alias: thm -> theory -> theory end; structure Nbe: NBE = struct (* generic non-sense *) val trace = Attrib.setup_config_bool \<^binding>\nbe_trace\ (K false); fun traced ctxt f x = if Config.get ctxt trace then (tracing (f x); x) else x; (** certificates and oracle for "trivial type classes" **) structure Triv_Class_Data = Theory_Data ( type T = (class * thm) list; val empty = []; val extend = I; fun merge data : T = AList.merge (op =) (K true) data; ); fun add_const_alias thm thy = let val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm) of SOME ofclass_eq => ofclass_eq | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val (T, class) = case try Logic.dest_of_class ofclass of SOME T_class => T_class | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm); val tvar = case try Term.dest_TVar T of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort) then tvar else error ("Bad sort: " ^ Thm.string_of_thm_global thy thm) | _ => error ("Bad type: " ^ Thm.string_of_thm_global thy thm); val _ = if Term.add_tvars eqn [] = [tvar] then () else error ("Inconsistent type: " ^ Thm.string_of_thm_global thy thm); val lhs_rhs = case try Logic.dest_equals eqn of SOME lhs_rhs => lhs_rhs | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); val c_c' = case try (apply2 (Axclass.unoverload_const thy o dest_Const)) lhs_rhs of SOME c_c' => c_c' | _ => error ("Not an equation with two constants: " ^ Syntax.string_of_term_global thy eqn); val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then () else error ("Inconsistent class: " ^ Thm.string_of_thm_global thy thm); in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end; local val get_triv_classes = map fst o Triv_Class_Data.get; val (_, triv_of_class) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\triv_of_class\, fn (thy, T, class) => Thm.global_cterm_of thy (Logic.mk_of_class (T, class))))); in fun lift_triv_classes_conv orig_ctxt conv ct = let val thy = Proof_Context.theory_of orig_ctxt; val ctxt = Proof_Context.init_global thy; (*FIXME quasi-global context*) val algebra = Sign.classes_of thy; val triv_classes = get_triv_classes thy; fun additional_classes sort = filter_out (fn class => Sorts.sort_le algebra (sort, [class])) triv_classes; fun mk_entry (v, sort) = let val T = TFree (v, sort); val cT = Thm.ctyp_of ctxt T; val triv_sort = additional_classes sort; in (v, (Sorts.inter_sort algebra (sort, triv_sort), (cT, AList.make (fn class => Thm.of_class (cT, class)) sort @ AList.make (fn class => triv_of_class (thy, T, class)) triv_sort))) end; val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []); fun instantiate thm = let val tvars = Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) []; val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab; in Thm.instantiate (TVars.make instT, Vars.empty) thm end; fun of_class (TFree (v, _), class) = the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class) | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T); fun strip_of_class thm = let val prems_of_class = Thm.prop_of thm |> Logic.strip_imp_prems |> map (Logic.dest_of_class #> of_class); in fold Thm.elim_implies prems_of_class thm end; in ct |> Thm.term_of |> (map_types o map_type_tfree) (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v)) |> Thm.cterm_of ctxt |> conv ctxt |> Thm.strip_shyps |> Thm.varifyT_global |> Thm.unconstrainT |> instantiate |> strip_of_class end; fun lift_triv_classes_rew ctxt rew t = let val thy = Proof_Context.theory_of ctxt; val algebra = Sign.classes_of thy; val triv_classes = get_triv_classes thy; val vs = Term.add_tfrees t []; in t |> (map_types o map_type_tfree) (fn (v, sort) => TFree (v, Sorts.inter_sort algebra (sort, triv_classes))) |> rew |> (map_types o map_type_tfree) (fn (v, sort) => TFree (v, the_default sort (AList.lookup (op =) vs v))) end; end; (** the semantic universe **) (* Functions are given by their semantical function value. To avoid trouble with the ML-type system, these functions have the most generic type, that is "Univ list -> Univ". The calling convention is that the arguments come as a list, the last argument first. In other words, a function call that usually would look like f x_1 x_2 ... x_n or f(x_1,x_2, ..., x_n) would be in our convention called as f [x_n,..,x_2,x_1] Moreover, to handle functions that are still waiting for some arguments we have additionally a list of arguments collected to far and the number of arguments we're still waiting for. *) datatype Univ = Const of int * Univ list (*named (uninterpreted) constants*) | DFree of string * int (*free (uninterpreted) dictionary parameters*) | BVar of int * Univ list (*bound variables, named*) | Abs of (int * (Univ list -> Univ)) * Univ list (*abstractions as closures*); (* constructor functions *) fun abss n f = Abs ((n, f), []); fun apps (Abs ((n, f), xs)) ys = let val k = n - length ys in case int_ord (k, 0) of EQUAL => f (ys @ xs) | LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*) end | apps (Const (name, xs)) ys = Const (name, ys @ xs) | apps (BVar (n, xs)) ys = BVar (n, ys @ xs); fun same (Const (k, xs), Const (l, ys)) = k = l andalso eq_list same (xs, ys) | same (DFree (s, k), DFree (t, l)) = s = t andalso k = l | same (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list same (xs, ys) | same _ = false; (** assembling and compiling ML code from terms **) (* abstract ML syntax *) infix 9 `$` `$$`; fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")"; fun e `$$` [] = e | e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")"; fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")"; fun ml_cases t cs = "(case " ^ t ^ " of " ^ space_implode " | " (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")"; fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end"; fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")"; fun ml_and [] = "true" | ml_and [x] = x | ml_and xs = "(" ^ space_implode " andalso " xs ^ ")"; fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")"; fun ml_list es = "[" ^ commas es ^ "]"; fun ml_fundefs ([(name, [([], e)])]) = "val " ^ name ^ " = " ^ e ^ "\n" | ml_fundefs (eqs :: eqss) = let fun fundef (name, eqs) = let fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e in space_implode "\n | " (map eqn eqs) end; in (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss |> cat_lines |> suffix "\n" end; (* nbe specific syntax and sandbox communication *) structure Univs = Proof_Data ( type T = unit -> Univ list -> Univ list; val empty: T = fn () => raise Fail "Univs"; fun init _ = empty; ); val get_result = Univs.get; val put_result = Univs.put; local val prefix = "Nbe."; val name_put = prefix ^ "put_result"; val name_const = prefix ^ "Const"; val name_abss = prefix ^ "abss"; val name_apps = prefix ^ "apps"; val name_same = prefix ^ "same"; in val univs_cookie = (get_result, put_result, name_put); fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value" | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym) ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i; fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n; fun nbe_bound v = "v_" ^ v; fun nbe_bound_optional NONE = "_" | nbe_bound_optional (SOME v) = nbe_bound v; fun nbe_default v = "w_" ^ v; (*note: these three are the "turning spots" where proper argument order is established!*) fun nbe_apps t [] = t | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts); fun nbe_apps_constr ctxt idx_of c ts = let val c' = if Config.get ctxt trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)" else string_of_int (idx_of c); in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end; fun nbe_abss 0 f = f `$` ml_list [] | nbe_abss n f = name_abss `$$` [string_of_int n, f]; fun nbe_same (v1, v2) = "(" ^ name_same ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))"; end; open Basic_Code_Symbol; open Basic_Code_Thingol; (* code generation *) fun assemble_eqnss ctxt idx_of deps eqnss = let fun prep_eqns (c, (vs, eqns)) = let val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; val num_args = length dicts + ((length o fst o hd) eqns); in (c, (num_args, (dicts, eqns))) end; val eqnss' = map prep_eqns eqnss; fun assemble_constapp sym dss ts = let val ts' = (maps o map) assemble_dict dss @ ts; in case AList.lookup (op =) eqnss' sym of SOME (num_args, _) => if num_args <= length ts' then let val (ts1, ts2) = chop num_args ts' in nbe_apps (nbe_apps_local idx_of 0 sym ts1) ts2 end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts' | NONE => if member (op =) deps sym then nbe_apps (nbe_fun idx_of 0 sym) ts' else nbe_apps_constr ctxt idx_of sym ts' end and assemble_classrels classrels = fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels and assemble_dict (Dict (classrels, x)) = assemble_classrels classrels (assemble_plain_dict x) and assemble_plain_dict (Dict_Const (inst, dss)) = assemble_constapp (Class_Instance inst) dss [] | assemble_plain_dict (Dict_Var { var, index, ... }) = nbe_dict var index fun assemble_iterm constapp = let fun of_iterm match_cont t = let val (t', ts) = Code_Thingol.unfold_app t in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts | of_iapp match_cont ((v, _) `|=> t) ts = nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts = nbe_apps (ml_cases (of_iterm NONE t) (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts in of_iterm end; fun subst_nonlin_vars args = let val vs = (fold o Code_Thingol.fold_varnames) (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args []; val names = Name.make_context (map fst vs); fun declare v k ctxt = let val vs = Name.invent ctxt v k in (vs, fold Name.declare vs ctxt) end; val (vs_renames, _) = fold_map (fn (v, k) => if k > 1 then declare v (k - 1) #>> (fn vs => (v, vs)) else pair (v, [])) vs names; val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames; fun subst_vars (t as IConst _) samepairs = (t, samepairs) | subst_vars (t as IVar NONE) samepairs = (t, samepairs) | subst_vars (t as IVar (SOME v)) samepairs = (case AList.lookup (op =) samepairs v of SOME v' => (IVar (SOME v'), AList.delete (op =) v samepairs) | NONE => (t, samepairs)) | subst_vars (t1 `$ t2) samepairs = samepairs |> subst_vars t1 ||>> subst_vars t2 |>> (op `$) | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs; val (args', _) = fold_map subst_vars args samepairs; in (samepairs, args') end; fun assemble_eqn sym dicts default_args (i, (args, rhs)) = let val match_cont = if Code_Symbol.is_value sym then NONE else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args)); val assemble_arg = assemble_iterm (fn sym' => fn dss => fn ts => nbe_apps_constr ctxt idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE; val assemble_rhs = assemble_iterm assemble_constapp match_cont; val (samepairs, args') = subst_nonlin_vars args; val s_args = map assemble_arg args'; val s_rhs = if null samepairs then assemble_rhs rhs else ml_if (ml_and (map nbe_same samepairs)) (assemble_rhs rhs) (the match_cont); val eqns = case match_cont of NONE => [([ml_list (rev (dicts @ s_args))], s_rhs)] | SOME default_rhs => [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs), ([ml_list (rev (dicts @ default_args))], default_rhs)] in (nbe_fun idx_of i sym, eqns) end; fun assemble_eqns (sym, (num_args, (dicts, eqns))) = let val default_args = map nbe_default (Name.invent Name.context "a" (num_args - length dicts)); val eqns' = map_index (assemble_eqn sym dicts default_args) eqns @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym, [([ml_list (rev (dicts @ default_args))], nbe_apps_constr ctxt idx_of sym (dicts @ default_args))])]); in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end; val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; val deps_vars = ml_list (map (nbe_fun idx_of 0) deps); in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end; (* compilation of equations *) fun compile_eqnss ctxt nbe_program raw_deps [] = [] | compile_eqnss ctxt nbe_program raw_deps eqnss = let val (deps, deps_vals) = split_list (map_filter (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps); val idx_of = raw_deps |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep))) |> AList.lookup (op =) |> (fn f => the o f); val s = assemble_eqnss ctxt idx_of deps eqnss; val cs = map fst eqnss; in s |> traced ctxt (fn s => "\n--- code to be evaluated:\n" ^ s) |> pair "" |> Code_Runtime.value ctxt univs_cookie |> (fn f => f deps_vals) |> (fn univs => cs ~~ univs) end; (* extraction of equations from statements *) fun dummy_const sym dss = IConst { sym = sym, typargs = [], dicts = dss, dom = [], annotation = NONE }; fun eqns_of_stmt (_, Code_Thingol.NoStmt) = [] | eqns_of_stmt (_, Code_Thingol.Fun ((_, []), _)) = [] | eqns_of_stmt (sym_const, Code_Thingol.Fun (((vs, _), eqns), _)) = [(sym_const, (vs, map fst eqns))] | eqns_of_stmt (_, Code_Thingol.Datatypecons _) = [] | eqns_of_stmt (_, Code_Thingol.Datatype _) = [] | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) = let val syms = map Class_Relation classrels @ map (Constant o fst) classparams; val params = Name.invent Name.context "d" (length syms); fun mk (k, sym) = (sym, ([(v, [])], [([dummy_const sym_class [] `$$ map (IVar o SOME) params], IVar (SOME (nth params k)))])); in map_index mk syms end | eqns_of_stmt (_, Code_Thingol.Classrel _) = [] | eqns_of_stmt (_, Code_Thingol.Classparam _) = [] | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) = [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] `$$ map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) dss) superinsts @ map (IConst o fst o snd o fst) inst_params)]))]; (* compilation of whole programs *) fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) = if can (Code_Symbol.Graph.get_node nbe_program) name then (nbe_program, (maxidx, idx_tab)) else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program, (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab)); fun compile_stmts ctxt stmts_deps = let val names = map (fst o fst) stmts_deps; val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps; val eqnss = maps (eqns_of_stmt o fst) stmts_deps; val refl_deps = names_deps |> maps snd |> distinct (op =) |> fold (insert (op =)) names; fun compile nbe_program = eqnss |> compile_eqnss ctxt nbe_program refl_deps |> rpair nbe_program; in fold ensure_const_idx refl_deps #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps #> compile #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ)))) end; fun compile_program { ctxt, program } = let fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names then (nbe_program, (maxidx, idx_tab)) else (nbe_program, (maxidx, idx_tab)) |> compile_stmts ctxt (map (fn name => ((name, Code_Symbol.Graph.get_node program name), Code_Symbol.Graph.immediate_succs program name)) names); in fold_rev add_stmts (Code_Symbol.Graph.strong_conn program) end; (** normalization **) (* compilation and reconstruction of terms *) fun compile_term { ctxt, nbe_program, deps, term = (vs, t) } = let val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs; in (Code_Symbol.value, (vs, [([], t)])) |> singleton (compile_eqnss ctxt nbe_program deps) |> snd |> (fn t => apps t (rev dict_frees)) end; fun reconstruct_term ctxt (idx_tab : Code_Symbol.T Inttab.table) t = let fun take_until f [] = [] | take_until f (x :: xs) = if f x then [] else x :: take_until f xs; fun is_dict (Const (idx, _)) = (case Inttab.lookup idx_tab idx of SOME (Constant _) => false | _ => true) | is_dict (DFree _) = true | is_dict _ = false; fun const_of_idx idx = case Inttab.lookup idx_tab idx of SOME (Constant const) => const; fun of_apps bounds (t, ts) = fold_map (of_univ bounds) ts #>> (fn ts' => list_comb (t, rev ts')) and of_univ bounds (Const (idx, ts)) typidx = let val ts' = take_until is_dict ts; val const = const_of_idx idx; val T = map_type_tvar (fn ((v, i), _) => Type_Infer.param typidx (v ^ string_of_int i, [])) (Sign.the_const_type (Proof_Context.theory_of ctxt) const); val typidx' = typidx + 1; in of_apps bounds (Term.Const (const, T), ts') typidx' end | of_univ bounds (BVar (n, ts)) typidx = of_apps bounds (Bound (bounds - n - 1), ts) typidx | of_univ bounds (t as Abs _) typidx = typidx |> of_univ (bounds + 1) (apps t [BVar (bounds, [])]) |-> (fn t' => pair (Term.Abs ("u", dummyT, t'))) in of_univ 0 t 0 |> fst end; fun compile_and_reconstruct_term { ctxt, nbe_program, idx_tab, deps, term } = compile_term { ctxt = ctxt, nbe_program = nbe_program, deps = deps, term = term } |> reconstruct_term ctxt idx_tab; fun normalize_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps = let val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt); val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); fun type_infer t' = Syntax.check_term (ctxt |> Config.put Type_Infer.object_logic false |> Config.put Type_Infer_Context.const_sorts false) (Type.constraint (fastype_of t_original) t'); fun check_tvars t' = if null (Term.add_tvars t' []) then t' else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t'); in Code_Preproc.timed "computing NBE expression" #ctxt compile_and_reconstruct_term { ctxt = ctxt, nbe_program = nbe_program, idx_tab = idx_tab, deps = deps, term = (vs, t) } |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t) |> type_infer |> traced ctxt (fn t => "Types inferred:\n" ^ string_of_term t) |> check_tvars |> traced ctxt (fn _ => "---\n") end; (* function store *) structure Nbe_Functions = Code_Data ( type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.T Inttab.table); val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty)); ); fun compile ignore_cache ctxt program = let val (nbe_program, (_, idx_tab)) = Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) (Code_Preproc.timed "compiling NBE program" #ctxt compile_program { ctxt = ctxt, program = program }); in (nbe_program, idx_tab) end; (* evaluation oracle *) fun mk_equals ctxt lhs raw_rhs = let val ty = Thm.typ_of_cterm lhs; - val eq = Thm.cterm_of ctxt (Term.Const (\<^const_name>\Pure.eq\, ty --> ty --> propT)); + val eq = Thm.cterm_of ctxt \<^Const>\Pure.eq ty\; val rhs = Thm.cterm_of ctxt raw_rhs; in Thm.mk_binop eq lhs rhs end; val (_, raw_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\normalization_by_evaluation\, fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) => mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps)))); fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct = raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct); fun dynamic_conv ctxt = lift_triv_classes_conv ctxt (fn ctxt' => Code_Thingol.dynamic_conv ctxt' (fn program => oracle (compile false ctxt program) ctxt')); fun dynamic_value ctxt = lift_triv_classes_rew ctxt (Code_Thingol.dynamic_value ctxt I (fn program => normalize_term (compile false ctxt program) ctxt)); fun static_conv (ctxt_consts as { ctxt, ... }) = let val conv = Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps = _ } => oracle (compile true ctxt program)); in fn ctxt' => lift_triv_classes_conv ctxt' conv end; fun static_value { ctxt, consts } = let val comp = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts } (fn { program, deps = _ } => normalize_term (compile false ctxt program)); in fn ctxt' => lift_triv_classes_rew ctxt' (comp ctxt') end; end;