(* Title: HOL/Tools/inductive_realizer.ML ID: $Id: inductive_realizer.ML,v 1.15 2005/09/19 14:38:35 haftmann Exp $ Author: Stefan Berghofer, TU Muenchen Porgram extraction from proofs involving inductive predicates: Realizers for induction and elimination rules *) signature INDUCTIVE_REALIZER = sig val add_ind_realizers: string -> string list -> theory -> theory val setup: (theory -> theory) list end; structure InductiveRealizer : INDUCTIVE_REALIZER = struct val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); fun prf_of thm = let val {sign, prop, der = (_, prf), ...} = rep_thm thm in Reconstruct.reconstruct_proof sign prop prf end; fun forall_intr_prf (t, prf) = let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; fun subsets [] = [[]] | subsets (x::xs) = let val ys = subsets xs in ys @ map (cons x) ys end; val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem; fun strip_all t = let fun strip used (Const ("all", _) $ Abs (s, T, t)) = let val s' = variant used s in strip (s'::used) (subst_bound (Free (s', T), t)) end | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q | strip _ t = t; in strip (add_term_free_names (t, [])) t end; fun relevant_vars prop = foldr (fn (Var ((a, i), T), vs) => (case strip_type T of (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs | _ => vs) | (_, vs) => vs) [] (term_vars prop); fun params_of intr = map (fst o fst o dest_Var) (term_vars (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))))); fun dt_of_intrs thy vs intrs = let val iTs = term_tvars (prop_of (hd intrs)); val Tvs = map TVar iTs; val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs)); val (Const (s, _), ts) = strip_comb S; val params = map dest_Var ts; val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr), map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ filter_out (equal Extraction.nullT) (map (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), NoSyn); in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn, map constr_of_intr intrs) end; fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT); (** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **) fun gen_rvar vs (t as Var ((a, 0), T)) = let val U = TVar (("'" ^ a, 0), HOLogic.typeS) in case try HOLogic.dest_setT T of NONE => if body_type T <> HOLogic.boolT then t else let val Ts = binder_types T; val i = length Ts; val xs = map (pair "x") Ts; val u = list_comb (t, map Bound (i - 1 downto 0)) in if a mem vs then list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u) else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u) end | SOME T' => if a mem vs then Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $ (HOLogic.mk_mem (Bound 0, t)))) else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $ (HOLogic.mk_mem (Bound 0, t))) end | gen_rvar _ t = t; fun mk_realizes_eqn n vs intrs = let val iTs = term_tvars (prop_of (hd intrs)); val Tvs = map TVar iTs; val _ $ (_ $ _ $ S) = concl_of (hd intrs); val (Const (s, T), ts') = strip_comb S; val setT = body_type T; val elT = HOLogic.dest_setT setT; val x = Var (("x", 0), elT); val rT = if n then Extraction.nullT else Type (space_implode "_" (s ^ "T" :: vs), map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT); val rvs = relevant_vars S; val vs' = map fst rvs \\ vs; val rname = space_implode "_" (s ^ "R" :: vs); fun mk_Tprem n v = let val T = (the o AList.lookup (op =) rvs) v in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T), Extraction.mk_typ (if n then Extraction.nullT else TVar (("'" ^ v, 0), HOLogic.typeS))) end; val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs; val ts = map (gen_rvar vs) ts'; val argTs = map fastype_of ts; in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S, Extraction.mk_typ rT)), (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S), if n then HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts)) else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname, argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts))))) end; fun fun_of_prem thy rsets vs params rule intr = let (* add_term_vars and Term.add_vars may return variables in different order *) val args = map (Free o apfst fst o dest_Var) (add_term_vars (prop_of intr, []) \\ map Var params); val args' = map (Free o apfst fst) (Term.add_vars (prop_of intr) [] \\ params); val rule' = strip_all rule; val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule'); val used = map (fst o dest_Free) args; fun is_rec t = not (null (term_consts t inter rsets)); fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true | is_meta _ = false; fun fun_of ts rts args used (prem :: prems) = let val T = Extraction.etype_of thy vs [] prem; val [x, r] = variantlist (["x", "r"], used) in if T = Extraction.nullT then fun_of ts rts args used prems else if is_rec prem then if is_meta prem then let val prem' :: prems' = prems; val U = Extraction.etype_of thy vs [] prem'; in if U = Extraction.nullT then fun_of (Free (x, T) :: ts) (Free (r, binder_types T ---> HOLogic.unitT) :: rts) (Free (x, T) :: args) (x :: r :: used) prems' else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts) (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems' end else (case strip_type T of (Ts, Type ("*", [T1, T2])) => let val fx = Free (x, Ts ---> T1); val fr = Free (r, Ts ---> T2); val bs = map Bound (length Ts - 1 downto 0); val t = list_abs (map (pair "z") Ts, HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs))) in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end | (Ts, U) => fun_of (Free (x, T) :: ts) (Free (r, binder_types T ---> HOLogic.unitT) :: rts) (Free (x, T) :: args) (x :: r :: used) prems) else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args) (x :: used) prems end | fun_of ts rts args used [] = let val xs = rev (rts @ ts) in if conclT = Extraction.nullT then list_abs_free (map dest_Free xs, HOLogic.unit) else list_abs_free (map dest_Free xs, list_comb (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr), map fastype_of (rev args) ---> conclT), rev args)) end in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = let val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); val premss = List.mapPartial (fn (s, rs) => if s mem rsets then SOME (map (fn r => List.nth (prems_of raw_induct, find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss; val concls' = List.mapPartial (fn (s, _) => if s mem rsets then find_first (fn concl => s mem term_consts concl) concls else NONE) rss; val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) => let val (intrs1, intrs2) = splitAt (length prems, intrs); val fs = map (fn (rule, intr) => fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1) in (intrs2, if dummy then Const ("arbitrary", HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs else fs) end) (intrs, (premss ~~ dummies)))); val frees = fold Term.add_frees fs []; val Ts = map fastype_of fs; val rlzs = List.mapPartial (fn (a, concl) => let val T = Extraction.etype_of thy vs [] concl in if T = Extraction.nullT then NONE else SOME (list_comb (Const (a, Ts ---> T), fs)) end) (rec_names ~~ concls') in if null rlzs then Extraction.nullt else let val r = foldr1 HOLogic.mk_prod rlzs; val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct))); fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr); val r' = list_abs_free (List.mapPartial (fn intr => Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs, if length concls = 1 then r $ x else r) in if length concls = 1 then lambda x r' else r' end end; fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) = if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs)) else x; fun add_dummies f dts used thy = apsnd (pair (map fst dts)) (f (map snd dts) thy) handle DatatypeAux.Datatype_Empty name' => let val name = Sign.base_name name'; val dname = variant used "Dummy" in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy end; fun mk_realizer thy vs params ((rule, rrule), rt) = let val prems = prems_of rule ~~ prems_of rrule; val rvs = map fst (relevant_vars (prop_of rule)); val xs = rev (Term.add_vars (prop_of rule) []); val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs); val rlzvs = rev (Term.add_vars (prop_of rrule) []); val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; val rs = gen_rems (op = o pairself fst) (rlzvs, xs); fun mk_prf _ [] prf = prf | mk_prf rs ((prem, rprem) :: prems) prf = if Extraction.etype_of thy vs [] prem = Extraction.nullT then AbsP ("H", SOME rprem, mk_prf rs prems prf) else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem, mk_prf (tl rs) prems prf)); in (Thm.name_of_thm rule, (vs, if rt = Extraction.nullt then rt else foldr (uncurry lambda) rt vs1, foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2)) end; fun add_rule r rss = let val _ $ (_ $ _ $ S) = concl_of r; val (Const (s, _), _) = strip_comb S; in rss |> AList.default (op =) (s, []) |> AList.map_entry (op =) s (fn rs => rs @ [r]) end; fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) = let val iTs = term_tvars (prop_of (hd intrs)); val ar = length vs + length iTs; val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs)); val (_, params) = strip_comb S; val params' = map dest_Var params; val rss = [] |> Library.fold add_rule intrs; val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss))); val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets; val thy1 = thy |> Theory.root_path |> Theory.add_path (NameSpace.pack prfx); val (ty_eqs, rlz_eqs) = split_list (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss); val thy1' = thy1 |> Theory.copy |> Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |> Theory.add_arities_i (map (fn s => (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |> Extraction.add_typeof_eqns_i ty_eqs; val dts = List.mapPartial (fn (s, rs) => if s mem rsets then SOME (dt_of_intrs thy1' vs rs) else NONE) rss; (** datatype representing computational content of inductive set **) val (thy2, (dummies, dt_info)) = thy1 |> (if null dts then rpair ([], NONE) else apsnd (apsnd SOME) o add_dummies (DatatypePackage.add_datatype_i false false (map #2 dts)) (map (pair false) dts) []) |>> Extraction.add_typeof_eqns_i ty_eqs |>> Extraction.add_realizes_eqns_i rlz_eqs; fun get f x = getOpt (Option.map f x, []); val rec_names = distinct (map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info)); val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) => if s mem rsets then let val (d :: dummies') = dummies; val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs) in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1) end else ((recs, dummies), replicate (length rs) Extraction.nullt)) ((get #rec_thms dt_info, dummies), rss); val rintrs = map (fn (intr, c) => Pattern.eta_contract (Extraction.realizes_of thy2 vs c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var) (rev (Term.add_vars (prop_of intr) []) \\ params')) intr)))) (intrs ~~ List.concat constrss); val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs); (** realizability predicate **) val (thy3', ind_info) = thy2 |> InductivePackage.add_inductive_i false true "" false false false (map Logic.unvarify rlzsets) (map (fn (rintr, intr) => ((Sign.base_name (Thm.name_of_thm intr), strip_all (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>> Theory.absolute_path; val thy3 = PureThy.hide_thms false (map Thm.name_of_thm (#intrs ind_info)) thy3'; (** realizer for induction rule **) val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then SOME (fst (fst (dest_Var (head_of P)))) else NONE) (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct))); fun add_ind_realizer (thy, Ps) = let val r = indrule_realizer thy induct raw_induct rsets params' (vs @ Ps) rec_names rss intrs dummies; val rlz = strip_all (Logic.unvarify (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct))); val rews = map mk_meta_eq (fst_conv :: snd_conv :: get #rec_thms dt_info); val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => [if length rss = 1 then cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1 else EVERY [rewrite_goals_tac (rews @ all_simps), REPEAT (rtac allI 1), rtac (#induct ind_info) 1], rewrite_goals_tac rews, REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac, DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); val (thy', thm') = PureThy.store_thm ((space_implode "_" (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy in Extraction.add_realizers_i [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy' end; (** realizer for elimination rules **) val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info); fun add_elim_realizer Ps (((((elim, elimR), intrs), case_thms), case_name), dummy) thy = let val (prem :: prems) = prems_of elim; fun reorder1 (p, intr) = Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t) (strip_all p, Term.add_vars (prop_of intr) [] \\ params'); fun reorder2 (intr, i) = let val fs1 = term_vars (prop_of intr) \\ params; val fs2 = Term.add_vars (prop_of intr) [] \\ params' in Library.foldl (fn (t, x) => lambda (Var x) t) (list_comb (Bound (i + length fs1), fs1), fs2) end; val p = Logic.list_implies (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim); val T' = Extraction.etype_of thy (vs @ Ps) [] p; val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T'; val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim); val r = if null Ps then Extraction.nullt else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T), (if dummy then [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))] else []) @ map reorder2 (intrs ~~ (length prems - 1 downto 0)) @ [Bound (length prems)])); val rlz = strip_all (Logic.unvarify (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim))); val rews = map mk_meta_eq case_thms; val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => [cut_facts_tac [hd prems] 1, etac elimR 1, ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]), rewrite_goals_tac rews, REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN' DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); val (thy', thm') = PureThy.store_thm ((space_implode "_" (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy in Extraction.add_realizers_i [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy' end; (** add realizers to theory **) val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth (#intrs ind_info, find_index_eq r intrs)) rs) rss); val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps); val thy5 = Extraction.add_realizers_i (map (mk_realizer thy4 vs params') (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) (List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4; val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then Option.map (rpair intrs) (find_first (fn (thm, _) => s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info)) else NONE) rss; val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |> add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5, elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies) in Theory.restore_naming thy thy6 end; fun add_ind_realizers name rsets thy = let val (_, {intrs, induct, raw_induct, elims, ...}) = (case InductivePackage.get_inductive thy name of NONE => error ("Unknown inductive set " ^ quote name) | SOME info => info); val _ $ (_ $ _ $ S) = concl_of (hd intrs); val vss = sort (int_ord o pairself length) (subsets (map fst (relevant_vars S))) in Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss) end fun rlz_attrib arg (thy, thm) = let fun err () = error "ind_realizer: bad rule"; val sets = (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))] | xs => map (set_of o fst o HOLogic.dest_imp) xs) handle TERM _ => err () | Empty => err (); in (add_ind_realizers (hd sets) (case arg of NONE => sets | SOME NONE => [] | SOME (SOME sets') => sets \\ sets') thy, thm) end; val rlz_attrib_global = Attrib.syntax ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |-- Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.global_const))) >> rlz_attrib); val setup = [Attrib.add_attributes [("ind_realizer", (rlz_attrib_global, K Attrib.undef_local_attribute), "add realizers for inductive set")]]; end;