diff --git a/thys/Applicative_Lifting/applicative.ML b/thys/Applicative_Lifting/applicative.ML --- a/thys/Applicative_Lifting/applicative.ML +++ b/thys/Applicative_Lifting/applicative.ML @@ -1,1370 +1,1369 @@ (* Author: Joshua Schneider, ETH Zurich *) signature APPLICATIVE = sig type afun val intern: Context.generic -> xstring -> string val extern: Context.generic -> string -> xstring val afun_of_generic: Context.generic -> string -> afun val afun_of: Proof.context -> string -> afun val afuns_of_term_generic: Context.generic -> term -> afun list val afuns_of_term: Proof.context -> term -> afun list val afuns_of_typ_generic: Context.generic -> typ -> afun list val afuns_of_typ: Proof.context -> typ -> afun list val name_of_afun: afun -> binding val unfolds_of_afun: afun -> thm list type afun_inst val match_afun_inst: Proof.context -> afun -> term * int -> afun_inst val import_afun_inst: afun -> Proof.context -> afun_inst * Proof.context val inner_sort_of: afun_inst -> sort val mk_type: afun_inst -> typ -> typ val mk_pure: afun_inst -> typ -> term val lift_term: afun_inst -> term -> term val mk_ap: afun_inst -> typ * typ -> term val mk_comb: afun_inst -> typ -> term * term -> term val mk_set: afun_inst -> typ -> term val dest_type: Proof.context -> afun_inst -> typ -> typ option val dest_type': Proof.context -> afun_inst -> typ -> typ val dest_pure: Proof.context -> afun_inst -> term -> term val dest_comb: Proof.context -> afun_inst -> term -> term * term val infer_comb: Proof.context -> afun_inst -> term * term -> term val subst_lift_term: afun_inst -> (term * term) list -> term -> term val generalize_lift_terms: afun_inst -> term list -> Proof.context -> term list * Proof.context val afun_unfold_tac: Proof.context -> afun -> int -> tactic val afun_fold_tac: Proof.context -> afun -> int -> tactic val unfold_all_tac: Proof.context -> int -> tactic val normalform_conv: Proof.context -> afun -> conv val normalize_rel_tac: Proof.context -> afun -> int -> tactic val general_normalform_conv: Proof.context -> afun -> cterm * cterm -> thm * thm val general_normalize_rel_tac: Proof.context -> afun -> int -> tactic val forward_lift_rule: Proof.context -> afun -> thm -> thm val unfold_wrapper_tac: Proof.context -> afun option -> int -> tactic val fold_wrapper_tac: Proof.context -> afun option -> int -> tactic val normalize_wrapper_tac: Proof.context -> afun option -> int -> tactic val lifting_wrapper_tac: Proof.context -> afun option -> int -> tactic val setup_combinators: (string * thm) list -> local_theory -> local_theory val combinator_rule_attrib: string list option -> attribute val parse_opt_afun: afun option context_parser val applicative_cmd: (((((binding * string list) * string) * string) * string option) * string option) -> local_theory -> Proof.state val print_afuns: Proof.context -> unit val add_unfold_attrib: xstring option -> attribute val forward_lift_attrib: xstring -> attribute end; structure Applicative : APPLICATIVE = struct open Ctr_Sugar_Util (** General utilities **) fun fold_options xs = fold (fn x => (case x of SOME x' => cons x' | NONE => I)) xs []; fun the_pair [x, y] = (x, y) | the_pair _ = raise General.Size; fun strip_comb2 (f $ x $ y) = (f, (x, y)) | strip_comb2 t = raise TERM ("strip_comb2", [t]); fun mk_comb_pattern (t, n) = let val Ts = take n (binder_types (fastype_of t)); val maxidx = maxidx_of_term t; val vars = map (fn (T, i) => ((Name.uu, maxidx + i), T)) (Ts ~~ (1 upto n)); in (vars, Term.betapplys (t, map Var vars)) end; fun match_comb_pattern ctxt tn u = let val thy = Proof_Context.theory_of ctxt; val (vars, pat) = mk_comb_pattern tn; val envs = Pattern.match thy (pat, u) (Vartab.empty, Vartab.empty) handle Pattern.MATCH => raise TERM ("match_comb_pattern", [u, pat]); in (vars, envs) end; fun dest_comb_pattern ctxt tn u = let val (vars, (_, env)) = match_comb_pattern ctxt tn u; in map (the o Envir.lookup1 env) vars end; fun norm_term_types tyenv t = Term_Subst.map_types_same (Envir.norm_type_same tyenv) t handle Same.SAME => t; val mk_TFrees_of = mk_TFrees' oo replicate; fun mk_Free name typ ctxt = yield_singleton Variable.variant_fixes name ctxt |>> (fn name' => Free (name', typ)); (*tuples with explicit sentinel*) fun mk_tuple' ts = fold_rev (curry HOLogic.mk_prod) ts HOLogic.unit; fun strip_tuple' (Const (@{const_name Unity}, _)) = [] | strip_tuple' (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: strip_tuple' t2 | strip_tuple' t = raise TERM ("strip_tuple'", [t]); fun mk_eq_on S = let val (SA, ST) = `HOLogic.dest_setT (fastype_of S); in Const (@{const_name eq_on}, ST --> BNF_Util.mk_pred2T SA SA) $ S end; (* Polymorphic terms and term groups *) type poly_type = typ list * typ; type poly_term = typ list * term; fun instantiate_poly_type (tvars, T) insts = typ_subst_atomic (tvars ~~ insts) T; fun instantiate_poly_term (tvars, t) insts = subst_atomic_types (tvars ~~ insts) t; fun dest_poly_type ctxt (tvars, T) U = let val thy = Proof_Context.theory_of ctxt; val tyenv = Sign.typ_match thy (T, U) Vartab.empty handle Type.TYPE_MATCH => raise TYPE ("dest_poly_type", [U, T], []); in map (Type.lookup tyenv o dest_TVar) tvars end; fun poly_type_to_term (tvars, T) = (tvars, Logic.mk_type T); fun poly_type_of_term (tvars, t) = (tvars, Logic.dest_type t); (* Schematic variables are treated uniformly in packed terms, thus forming an ad hoc context of type variables. Otherwise, morphisms are allowed to rename schematic variables non-consistently in separate terms, and occasionally will do so. *) fun pack_poly_term (tvars, t) = HOLogic.mk_prod (mk_tuple' (map Logic.mk_type tvars), t); fun unpack_poly_term t = let val (tvars, t') = HOLogic.dest_prod t; in (map Logic.dest_type (strip_tuple' tvars), t') end; val pack_poly_terms = mk_tuple' o map pack_poly_term; val unpack_poly_terms = map unpack_poly_term o strip_tuple'; (*match and instantiate schematic type variables which are not "quantified" in the packed term*) fun match_poly_terms_type ctxt (pt, i) (U, maxidx) = let val thy = Proof_Context.theory_of ctxt; val pt' = Logic.incr_indexes ([], [], maxidx + 1) pt; val (tvars, T) = poly_type_of_term (nth (unpack_poly_terms pt') i); val tyenv = Sign.typ_match thy (T, U) Vartab.empty handle Type.TYPE_MATCH => raise TYPE ("match_poly_terms", [U, T], []); val tyenv' = fold Vartab.delete_safe (map (#1 o dest_TVar) tvars) tyenv; val pt'' = Envir.subst_term_types tyenv' pt'; in unpack_poly_terms pt'' end; fun match_poly_terms ctxt (pt, i) (t, maxidx) = match_poly_terms_type ctxt (pt, i) (fastype_of t, maxidx); (*fix schematic type variables which are not "quantified", as well as schematic term variables*) fun import_poly_terms pt ctxt = let fun insert_paramTs (tvars, t) = fold_types (fold_atyps (fn TVar v => if member (op =) tvars (TVar v) then I else insert (op =) v | _ => I)) t; val paramTs = rev (fold insert_paramTs (unpack_poly_terms pt) []); val (tfrees, ctxt') = Variable.invent_types (map #2 paramTs) ctxt; - val instT = Term_Subst.TVars.table (paramTs ~~ map TFree tfrees); + val instT = TVars.make (paramTs ~~ map TFree tfrees); val params = map (apsnd (Term_Subst.instantiateT instT)) (rev (Term.add_vars pt [])); val (frees, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) params) ctxt'; - val inst = Term_Subst.Vars.table (params ~~ map Free (frees ~~ map #2 params)); + val inst = Vars.make (params ~~ map Free (frees ~~ map #2 params)); val pt' = Term_Subst.instantiate (instT, inst) pt; in (unpack_poly_terms pt', ctxt'') end; (** Internal representation **) (* Applicative functors *) type rel_thms = { pure_transfer: thm, ap_rel_fun: thm }; fun map_rel_thms f {pure_transfer, ap_rel_fun} = {pure_transfer = f pure_transfer, ap_rel_fun = f ap_rel_fun}; type afun_thms = { hom: thm, ichng: thm, reds: thm Symtab.table, rel_thms: rel_thms option, rel_intros: thm list, pure_comp_conv: thm }; fun map_afun_thms f {hom, ichng, reds, rel_thms, rel_intros, pure_comp_conv} = {hom = f hom, ichng = f ichng, reds = Symtab.map (K f) reds, rel_thms = Option.map (map_rel_thms f) rel_thms, rel_intros = map f rel_intros, pure_comp_conv = f pure_comp_conv}; datatype afun = AFun of { name: binding, terms: term, rel: term option, thms: afun_thms, unfolds: thm Item_Net.T }; fun rep_afun (AFun af) = af; val name_of_afun = #name o rep_afun; val terms_of_afun = #terms o rep_afun; val rel_of_afun = #rel o rep_afun; val thms_of_afun = #thms o rep_afun; val unfolds_of_afun = Item_Net.content o #unfolds o rep_afun; val red_of_afun = Symtab.lookup o #reds o thms_of_afun; val has_red_afun = is_some oo red_of_afun; fun mk_afun name terms rel thms = AFun {name = name, terms = terms, rel = rel, thms = thms, unfolds = Thm.item_net}; fun map_afun f1 f2 f3 f4 f5 (AFun {name, terms, rel, thms, unfolds}) = AFun {name = f1 name, terms = f2 terms, rel = f3 rel, thms = f4 thms, unfolds = f5 unfolds}; fun map_unfolds f thms = fold Item_Net.update (map f (Item_Net.content thms)) Thm.item_net; fun morph_afun phi = let val binding = Morphism.binding phi; val term = Morphism.term phi; val thm = Morphism.thm phi; in map_afun binding term (Option.map term) (map_afun_thms thm) (map_unfolds thm) end; val transfer_afun = morph_afun o Morphism.transfer_morphism; fun add_unfolds_afun thms = map_afun I I I I (fold Item_Net.update thms); fun patterns_of_afun af = let val [Tt, (_, pure), (_, ap), _] = unpack_poly_terms (terms_of_afun af); val (_, T) = poly_type_of_term Tt; in [#2 (mk_comb_pattern (pure, 1)), #2 (mk_comb_pattern (ap, 2)), Net.encode_type T] end; (* Combinator rules *) datatype combinator_rule = Combinator_Rule of { strong_premises: string Ord_List.T, weak_premises: bool, conclusion: string, eq_thm: thm }; fun rep_combinator_rule (Combinator_Rule rule) = rule; val conclusion_of_rule = #conclusion o rep_combinator_rule; val thm_of_rule = #eq_thm o rep_combinator_rule; fun eq_combinator_rule (rule1, rule2) = pointer_eq (rule1, rule2) orelse Thm.eq_thm (thm_of_rule rule1, thm_of_rule rule2); fun is_applicable_rule rule have_weak have_premises = let val {strong_premises, weak_premises, ...} = rep_combinator_rule rule; in (have_weak orelse not weak_premises) andalso have_premises strong_premises end; fun map_combinator_rule f1 f2 f3 f4 (Combinator_Rule {strong_premises, weak_premises, conclusion, eq_thm}) = Combinator_Rule {strong_premises = f1 strong_premises, weak_premises = f2 weak_premises, conclusion = f3 conclusion, eq_thm = f4 eq_thm}; fun transfer_combinator_rule thy = map_combinator_rule I I I (Thm.transfer thy); fun mk_combinator_rule comb_names weak_premises thm = let val (lhs, rhs) = Logic.dest_equals (Thm.prop_of thm); val conclusion = the (Symtab.lookup comb_names (#1 (dest_Const lhs))); val premises = Ord_List.make fast_string_ord (fold_options (map (Symtab.lookup comb_names o #1) (Term.add_consts rhs []))); val weak_premises' = Ord_List.make fast_string_ord (these weak_premises); val strong_premises = Ord_List.subtract fast_string_ord weak_premises' premises; in Combinator_Rule {strong_premises = strong_premises, weak_premises = is_some weak_premises, conclusion = conclusion, eq_thm = thm} end; (* Generic data *) (*FIXME: needs tests, especially around theory merging*) fun merge_afuns _ (af1, af2) = if pointer_eq (af1, af2) then raise Change_Table.SAME else map_afun I I I I (fn thms1 => Item_Net.merge (thms1, #unfolds (rep_afun af2))) af1; structure Data = Generic_Data ( type T = { combinators: thm Symtab.table * combinator_rule list, afuns: afun Name_Space.table, patterns: (string * term list) Item_Net.T }; val empty = { combinators = (Symtab.empty, []), afuns = Name_Space.empty_table "applicative functor", patterns = Item_Net.init (op = o apply2 #1) #2 }; val extend = I; fun merge ({combinators = (cd1, cr1), afuns = a1, patterns = p1}, {combinators = (cd2, cr2), afuns = a2, patterns = p2}) = {combinators = (Symtab.merge (K true) (cd1, cd2), Library.merge eq_combinator_rule (cr1, cr2)), afuns = Name_Space.join_tables merge_afuns (a1, a2), patterns = Item_Net.merge (p1, p2)}; ); fun get_combinators context = let val thy = Context.theory_of context; val {combinators = (defs, rules), ...} = Data.get context; in (Symtab.map (K (Thm.transfer thy)) defs, map (transfer_combinator_rule thy) rules) end; val get_afun_table = #afuns o Data.get; val get_afun_space = Name_Space.space_of_table o get_afun_table; val get_patterns = #patterns o Data.get; fun map_data f1 f2 f3 {combinators, afuns, patterns} = {combinators = f1 combinators, afuns = f2 afuns, patterns = f3 patterns}; val intern = Name_Space.intern o get_afun_space; fun extern context = Name_Space.extern (Context.proof_of context) (get_afun_space context); local fun undeclared name = error ("Undeclared applicative functor " ^ quote name); in fun afun_of_generic context name = case Name_Space.lookup (get_afun_table context) name of SOME af => transfer_afun (Context.theory_of context) af | NONE => undeclared name; val afun_of = afun_of_generic o Context.Proof; fun update_afun name f context = if Name_Space.defined (get_afun_table context) name then Data.map (map_data I (Name_Space.map_table_entry name f) I) context else undeclared name; end; fun match_term context = map #1 o Item_Net.retrieve_matching (get_patterns context); fun match_typ context = match_term context o Net.encode_type; (*works only with terms which are combinations of pure and ap*) fun afuns_of_term_generic context = map (afun_of_generic context) o match_term context; val afuns_of_term = afuns_of_term_generic o Context.Proof; fun afuns_of_typ_generic context = map (afun_of_generic context) o match_typ context; val afuns_of_typ = afuns_of_typ_generic o Context.Proof; fun all_unfolds_of_generic context = let val unfolds_of = map (Thm.transfer'' context) o unfolds_of_afun; in Name_Space.fold_table (fn (_, af) => append (unfolds_of af)) (get_afun_table context) [] end; val all_unfolds_of = all_unfolds_of_generic o Context.Proof; (** Term construction and destruction **) type afun_inst = { T: poly_type, pure: poly_term, ap: poly_term, set: poly_term }; fun mk_afun_inst [T, pure, ap, set] = {T = poly_type_of_term T, pure = pure, ap = ap, set = set}; fun pack_afun_inst {T, pure, ap, set} = pack_poly_terms [poly_type_to_term T, pure, ap, set]; fun match_afun_inst ctxt af = match_poly_terms ctxt (terms_of_afun af, 0) #> mk_afun_inst; fun import_afun_inst_raw terms = import_poly_terms terms #>> mk_afun_inst; val import_afun_inst = import_afun_inst_raw o terms_of_afun; fun inner_sort_of {T = (tvars, _), ...} = Type.sort_of_atyp (the_single tvars); fun mk_type {T, ...} = instantiate_poly_type T o single; fun mk_pure {pure, ...} = instantiate_poly_term pure o single; fun mk_ap {ap, ...} (T1, T2) = instantiate_poly_term ap [T1, T2]; fun mk_set {set, ...} = instantiate_poly_term set o single; fun lift_term af_inst t = Term.betapply (mk_pure af_inst (Term.fastype_of t), t); fun mk_comb af_inst funT (t1, t2) = Term.betapplys (mk_ap af_inst (dest_funT funT), [t1, t2]); fun dest_type ctxt {T, ...} = the_single o dest_poly_type ctxt T; val dest_type' = the_default HOLogic.unitT ooo dest_type; fun dest_pure ctxt {pure = (_, pure), ...} = the_single o dest_comb_pattern ctxt (pure, 1); fun dest_comb ctxt {ap = (_, ap), ...} = the_pair o dest_comb_pattern ctxt (ap, 2); fun infer_comb ctxt af_inst (t1, t2) = let val funT = the_default (dummyT --> dummyT) (dest_type ctxt af_inst (fastype_of t1)); in mk_comb af_inst funT (t1, t2) end; (*lift a term, except for non-combination subterms mapped by subst*) fun subst_lift_term af_inst subst tm = let fun subst_lift (s $ t) = (case (subst_lift s, subst_lift t) of (NONE, NONE) => NONE | (SOME s', NONE) => SOME (mk_comb af_inst (fastype_of s) (s', lift_term af_inst t)) | (NONE, SOME t') => SOME (mk_comb af_inst (fastype_of s) (lift_term af_inst s, t')) | (SOME s', SOME t') => SOME (mk_comb af_inst (fastype_of s) (s', t'))) | subst_lift t = AList.lookup (op aconv) subst t; in (case subst_lift tm of NONE => lift_term af_inst tm | SOME tm' => tm') end; fun add_lifted_vars (s $ t) = add_lifted_vars s #> add_lifted_vars t | add_lifted_vars (Abs (_, _, t)) = Term.add_vars t | add_lifted_vars _ = I; (*lift terms, where schematic variables are generalized to the functor and then fixed*) fun generalize_lift_terms af_inst ts ctxt = let val vars = subtract (op =) (fold add_lifted_vars ts []) (fold Term.add_vars ts []); val (var_names, Ts) = split_list vars; val (free_names, ctxt') = Variable.variant_fixes (map #1 var_names) ctxt; val Ts' = map (mk_type af_inst) Ts; val subst = map Var vars ~~ map Free (free_names ~~ Ts'); in (map (subst_lift_term af_inst subst) ts, ctxt') end; (** Reasoning with applicative functors **) (* Utilities *) val clean_name = perhaps (perhaps_apply [try Name.dest_skolem, try Name.dest_internal]); (*based on term_name from Pure/term.ML*) fun term_to_vname (Const (x, _)) = Long_Name.base_name x | term_to_vname (Free (x, _)) = clean_name x | term_to_vname (Var ((x, _), _)) = clean_name x | term_to_vname _ = "x"; fun afuns_of_rel precise ctxt t = let val (_, (lhs, rhs)) = Variable.focus NONE t ctxt |> #1 |> #2 |> Logic.strip_imp_concl |> Envir.beta_eta_contract |> HOLogic.dest_Trueprop |> strip_comb2; in if precise then (case afuns_of_term ctxt lhs of [] => afuns_of_term ctxt rhs | afs => afs) else afuns_of_typ ctxt (fastype_of lhs) end; fun AUTO_AFUNS precise tac ctxt opt_af = case opt_af of SOME af => tac [af] | NONE => SUBGOAL (fn (goal, i) => (case afuns_of_rel precise ctxt goal of [] => no_tac | afs => tac afs i) handle TERM _ => no_tac); fun AUTO_AFUN precise tac = AUTO_AFUNS precise (tac o hd); fun binop_par_conv cv ct = let val ((binop, arg1), arg2) = Thm.dest_comb ct |>> Thm.dest_comb; val (th1, th2) = cv (arg1, arg2); in Drule.binop_cong_rule binop th1 th2 end; fun binop_par_conv_tac cv = CONVERSION (HOLogic.Trueprop_conv (binop_par_conv cv)); val fold_goal_tac = SELECT_GOAL oo Raw_Simplifier.fold_goals_tac; (* Unfolding of lifted constants *) fun afun_unfold_tac ctxt af = Raw_Simplifier.rewrite_goal_tac ctxt (unfolds_of_afun af); fun afun_fold_tac ctxt af = fold_goal_tac ctxt (unfolds_of_afun af); fun unfold_all_tac ctxt = Raw_Simplifier.rewrite_goal_tac ctxt (all_unfolds_of ctxt); (* Basic conversions *) fun pure_conv ctxt {pure = (_, pure), ...} cv ct = let val ([var], (tyenv, env)) = match_comb_pattern ctxt (pure, 1) (Thm.term_of ct); val arg = the (Envir.lookup1 env var); val thm = cv (Thm.cterm_of ctxt arg); in if Thm.is_reflexive thm then Conv.all_conv ct else let val pure_inst = Envir.subst_term_types tyenv pure; in Drule.arg_cong_rule (Thm.cterm_of ctxt pure_inst) thm end end; fun ap_conv ctxt {ap = (_, ap), ...} cv1 cv2 ct = let val ([var1, var2], (tyenv, env)) = match_comb_pattern ctxt (ap, 2) (Thm.term_of ct); val (arg1, arg2) = apply2 (the o Envir.lookup1 env) (var1, var2); val thm1 = cv1 (Thm.cterm_of ctxt arg1); val thm2 = cv2 (Thm.cterm_of ctxt arg2); in if Thm.is_reflexive thm1 andalso Thm.is_reflexive thm2 then Conv.all_conv ct else let val ap_inst = Envir.subst_term_types tyenv ap; in Drule.binop_cong_rule (Thm.cterm_of ctxt ap_inst) thm1 thm2 end end; (* Normal form conversion *) (*convert a term into applicative normal form*) fun normalform_conv ctxt af ct = let val {hom, ichng, pure_comp_conv, ...} = thms_of_afun af; val the_red = the o red_of_afun af; val leaf_conv = Conv.rewr_conv (mk_meta_eq (the_red "I") |> Thm.symmetric); val merge_conv = Conv.rewr_conv (mk_meta_eq hom); val swap_conv = Conv.rewr_conv (mk_meta_eq ichng); val rotate_conv = Conv.rewr_conv (mk_meta_eq (the_red "B") |> Thm.symmetric); val pure_rotate_conv = Conv.rewr_conv (mk_meta_eq pure_comp_conv); val af_inst = match_afun_inst ctxt af (Thm.term_of ct, Thm.maxidx_of_cterm ct); fun left_conv cv = ap_conv ctxt af_inst cv Conv.all_conv; fun norm_pure_nf ct = ((pure_rotate_conv then_conv left_conv norm_pure_nf) else_conv merge_conv) ct; val norm_nf_pure = swap_conv then_conv norm_pure_nf; fun norm_nf_nf ct = ((rotate_conv then_conv left_conv (left_conv norm_pure_nf then_conv norm_nf_nf)) else_conv norm_nf_pure) ct; fun normalize ct = ((ap_conv ctxt af_inst normalize normalize then_conv norm_nf_nf) else_conv pure_conv ctxt af_inst Conv.all_conv else_conv leaf_conv) ct; in normalize ct end; val normalize_rel_tac = binop_par_conv_tac o apply2 oo normalform_conv; (* Bracket abstraction and generalized unlifting *) (*TODO: use proper conversions*) datatype apterm = Pure of term (*includes pure application*) | ApVar of int * term (*unique index, instantiated term*) | Ap of apterm * apterm; fun apterm_vars (Pure _) = I | apterm_vars (ApVar v) = cons v | apterm_vars (Ap (t1, t2)) = apterm_vars t1 #> apterm_vars t2; fun occurs_any _ (Pure _) = false | occurs_any vs (ApVar (i, _)) = exists (fn j => i = j) vs | occurs_any vs (Ap (t1, t2)) = occurs_any vs t1 orelse occurs_any vs t2; fun term_of_apterm ctxt af_inst t = let fun tm_of (Pure t) = t | tm_of (ApVar (_, t)) = t | tm_of (Ap (t1, t2)) = infer_comb ctxt af_inst (tm_of t1, tm_of t2); in tm_of t end; fun apterm_of_term ctxt af_inst t = let fun aptm_of t i = case try (dest_comb ctxt af_inst) t of SOME (t1, t2) => i |> aptm_of t1 ||>> aptm_of t2 |>> Ap | NONE => if can (dest_pure ctxt af_inst) t then (Pure t, i) else (ApVar (i, t), i + 1); in aptm_of t end; (*find a common variable sequence for two applicative terms, depending on available combinators*) fun consolidate ctxt af (t1, t2) = let fun common_inst (i, t) (j, insts) = case Termtab.lookup insts t of SOME k => (((i, t), k), (j, insts)) | NONE => (((i, t), j), (j + 1, Termtab.update (t, j) insts)); val (vars, _) = (0, Termtab.empty) |> fold_map common_inst (apterm_vars t1 []) ||>> fold_map common_inst (apterm_vars t2 []); fun merge_adjacent (([], _), _) [] = [] | merge_adjacent ((is, t), d) [] = [((is, t), d)] | merge_adjacent (([], _), _) (((i, t), d)::xs) = merge_adjacent (([i], t), d) xs | merge_adjacent ((is, t), d) (((i', t'), d')::xs) = if d = d' then merge_adjacent ((i'::is, t), d) xs else ((is, t), d) :: merge_adjacent (([i'], t'), d') xs; fun align _ [] = NONE | align ((i, t), d) (((i', t'), d')::xs) = if d = d' then SOME ([((i @ i', t), d)], xs) else Option.map (apfst (cons ((i', t'), d'))) (align ((i, t), d) xs); fun merge ([], ys) = ys | merge (xs, []) = xs | merge ((xs as ((is1, t1), d1)::xs'), ys as (((is2, t2), d2)::ys')) = if d1 = d2 then ((is1 @ is2, t1), d1) :: merge (xs', ys') else case (align ((is2, t2), d2) xs, align ((is1, t1), d1) ys) of (SOME (zs, xs''), NONE) => zs @ merge (xs'', ys') | (NONE, SOME (zs, ys'')) => zs @ merge (xs', ys'') | _ => ((is1, t1), d1) :: ((is2, t2), d2) :: merge (xs', ys'); fun unbalanced vs = error ("Unbalanced opaque terms " ^ commas_quote (map (Syntax.string_of_term ctxt o #2 o #1) vs)); fun mismatch (t1, t2) = error ("Mismatched opaque terms " ^ quote (Syntax.string_of_term ctxt t1) ^ " and " ^ quote (Syntax.string_of_term ctxt t2)); fun same ([], []) = [] | same ([], ys) = unbalanced ys | same (xs, []) = unbalanced xs | same ((((i1, t1), d1)::xs), (((i2, t2), d2)::ys)) = if d1 = d2 then ((i1 @ i2, t1), d1) :: same (xs, ys) else mismatch (t1, t2); in vars |> has_red_afun af "C" ? apply2 (sort (int_ord o apply2 #2)) |> apply2 (if has_red_afun af "W" then merge_adjacent (([], Term.dummy), 0) else map (apfst (apfst single))) |> (if has_red_afun af "K" then merge else same) |> map #1 end; fun ap_cong ctxt af_inst thm1 thm2 = let val funT = the_default (dummyT --> dummyT) (dest_type ctxt af_inst (Thm.typ_of_cterm (Thm.lhs_of thm1))); val ap_inst = Thm.cterm_of ctxt (mk_ap af_inst (dest_funT funT)); in Drule.binop_cong_rule ap_inst thm1 thm2 end; fun rewr_subst_ap ctxt af_inst rewr thm1 thm2 = let val rule1 = ap_cong ctxt af_inst thm1 thm2; val rule2 = Conv.rewr_conv rewr (Thm.rhs_of rule1); in Thm.transitive rule1 rule2 end; fun merge_pures ctxt af_inst merge_thm tt = let fun merge (Pure t) = SOME (Thm.reflexive (Thm.cterm_of ctxt t)) | merge (ApVar _) = NONE | merge (Ap (tt1, tt2)) = case merge tt1 of NONE => NONE | SOME thm1 => case merge tt2 of NONE => NONE | SOME thm2 => SOME (rewr_subst_ap ctxt af_inst merge_thm thm1 thm2); in merge tt end; exception ASSERT of string; (*abstract over a variable (opaque subterm)*) fun eliminate ctxt (af, af_inst) tt (v, v_tm) = let val {hom, ichng, ...} = thms_of_afun af; val the_red = the o red_of_afun af; val hom_conv = mk_meta_eq hom; val ichng_conv = mk_meta_eq ichng; val mk_combI = Thm.symmetric o mk_meta_eq; val id_conv = mk_combI (the_red "I"); val comp_conv = mk_combI (the_red "B"); val flip_conv = Option.map mk_combI (red_of_afun af "C"); val const_conv = Option.map mk_combI (red_of_afun af "K"); val dup_conv = Option.map mk_combI (red_of_afun af "W"); val rewr_subst_ap = rewr_subst_ap ctxt af_inst; fun extract_comb n thm = Pure (thm |> Thm.rhs_of |> funpow n Thm.dest_arg1 |> Thm.term_of); fun refl_step tt = (tt, Thm.reflexive (Thm.cterm_of ctxt (term_of_apterm ctxt af_inst tt))); fun comb2_step def (tt1, thm1) (tt2, thm2) = let val thm = rewr_subst_ap def thm1 thm2; in (Ap (Ap (extract_comb 3 thm, tt1), tt2), thm) end; val B_step = comb2_step comp_conv; fun swap_B_step (tt1, thm1) thm2 = let val thm3 = rewr_subst_ap ichng_conv thm1 thm2; val thm4 = Thm.transitive thm3 (Conv.rewr_conv comp_conv (Thm.rhs_of thm3)); in (Ap (Ap (extract_comb 3 thm4, extract_comb 1 thm3), tt1), thm4) end; fun I_step tm = let val thm = Conv.rewr_conv id_conv (Thm.cterm_of ctxt tm) in (extract_comb 1 thm, thm) end; fun W_step s1 s2 = let val (Ap (Ap (tt1, tt2), tt3), thm1) = B_step s1 s2; val thm2 = Conv.rewr_conv comp_conv (Thm.rhs_of thm1 |> funpow 2 Thm.dest_arg1); val thm3 = merge_pures ctxt af_inst hom_conv tt3 |> the; val (tt4, thm4) = swap_B_step (Ap (Ap (extract_comb 3 thm2, tt1), tt2), thm2) thm3; val var = Thm.rhs_of thm1 |> Thm.dest_arg; val thm5 = rewr_subst_ap (the dup_conv) thm4 (Thm.reflexive var); val thm6 = Thm.transitive thm1 thm5; in (Ap (extract_comb 2 thm6, tt4), thm6) end; fun S_step s1 s2 = let val (Ap (Ap (tt1, tt2), tt3), thm1) = comb2_step (the flip_conv) s1 s2; val thm2 = Conv.rewr_conv comp_conv (Thm.rhs_of thm1 |> Thm.dest_arg1); val var = Thm.rhs_of thm1 |> Thm.dest_arg; val thm3 = rewr_subst_ap (the dup_conv) thm2 (Thm.reflexive var); val thm4 = Thm.transitive thm1 thm3; val tt = Ap (extract_comb 2 thm4, Ap (Ap (extract_comb 3 thm2, Ap (tt1, tt2)), tt3)); in (tt, thm4) end; fun K_step tt tm = let val ct = Thm.cterm_of ctxt tm; val T_opt = Term.fastype_of tm |> dest_type ctxt af_inst |> Option.map (Thm.ctyp_of ctxt); val thm = Thm.instantiate' [T_opt] [SOME ct] (Conv.rewr_conv (the const_conv) (term_of_apterm ctxt af_inst tt |> Thm.cterm_of ctxt)) in (Ap (extract_comb 2 thm, tt), thm) end; fun unreachable _ = raise ASSERT "eliminate: assertion failed"; fun elim (Pure _) = unreachable () | elim (ApVar (i, t)) = if exists (fn x => x = i) v then I_step t else unreachable () | elim (Ap (t1, t2)) = (case (occurs_any v t1, occurs_any v t2) of (false, false) => unreachable () | (false, true) => B_step (refl_step t1) (elim t2) | (true, false) => (case merge_pures ctxt af_inst hom_conv t2 of SOME thm => swap_B_step (elim t1) thm | NONE => comb2_step (the flip_conv) (elim t1) (refl_step t2)) | (true, true) => if is_some flip_conv then S_step (elim t1) (elim t2) else W_step (elim t1) (elim t2)); in if occurs_any v tt then elim tt else K_step tt v_tm end; (*convert a pair of terms into equal canonical forms, modulo pure terms*) fun general_normalform_conv ctxt af cts = let val (t1, t2) = apply2 (Thm.term_of) cts; val maxidx = Int.max (apply2 Thm.maxidx_of_cterm cts); (* TODO: is there a better strategy for finding the instantiated functor? *) val af_inst = match_afun_inst ctxt af (t1, maxidx); val ((apt1, apt2), _) = 0 |> apterm_of_term ctxt af_inst t1 ||>> apterm_of_term ctxt af_inst t2; val vs = consolidate ctxt af (apt1, apt2); val merge_thm = mk_meta_eq (#hom (thms_of_afun af)); fun elim_all tt [] = the (merge_pures ctxt af_inst merge_thm tt) | elim_all tt (v::vs) = let val (tt', rule1) = eliminate ctxt (af, af_inst) tt v; val rule2 = elim_all tt' vs; val (_, vartm) = dest_comb ctxt af_inst (Thm.term_of (Thm.rhs_of rule1)); val rule3 = ap_cong ctxt af_inst rule2 (Thm.reflexive (Thm.cterm_of ctxt vartm)); in Thm.transitive rule1 rule3 end; in (elim_all apt1 vs, elim_all apt2 vs) end; val general_normalize_rel_tac = binop_par_conv_tac oo general_normalform_conv; (* Reduce canonical forms to base relation *) fun rename_params names i st = let val (_, Bs, Bi, C) = Thm.dest_state (st, i); val Bi' = Logic.list_rename_params names Bi; in Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st end; (* R' (pure f <> x1 <> ... <> xn) (pure g <> x1 <> ... <> xn) ===> !!y1 ... yn. [| yi : setF xi ... |] ==> R (f y1 ... yn) (g y1 ... yn), where either both R and R' are equality, or R' = relF R for relator relF of the functor. The premises yi : setF xi are added only in the latter case and if the set operator is available. Succeeds if partial progress can be made. The names of the new parameters yi are derived from the arguments xi. *) fun head_cong_tac ctxt af renames = let val {rel_intros, ...} = thms_of_afun af; fun term_name tm = case AList.lookup (op aconv) renames tm of SOME n => n | NONE => term_to_vname tm; fun gather_vars' af_inst tm = case try (dest_comb ctxt af_inst) tm of SOME (t1, t2) => term_name t2 :: gather_vars' af_inst t1 | NONE => []; fun gather_vars prop = case prop of Const (@{const_name Trueprop}, _) $ (_ $ rhs) => rev (gather_vars' (match_afun_inst ctxt af (rhs, maxidx_of_term prop)) rhs) | _ => []; in SUBGOAL (fn (subgoal, i) => (REPEAT_DETERM (resolve_tac ctxt rel_intros i) THEN REPEAT_DETERM (resolve_tac ctxt [ext, @{thm rel_fun_eq_onI}] i ORELSE eresolve_tac ctxt [@{thm UNIV_E}] i) THEN PRIMITIVE (rename_params (gather_vars subgoal) i))) end; (* Forward lifting *) (* TODO: add limited support for premises, where used variables are not generalized in the conclusion *) fun forward_lift_rule ctxt af thm = let val thm = Object_Logic.rulify ctxt thm; val (af_inst, ctxt_inst) = import_afun_inst af ctxt; val (prop, ctxt_Ts) = yield_singleton Variable.importT_terms (Thm.prop_of thm) ctxt_inst; val (lhs, rhs) = prop |> HOLogic.dest_Trueprop |> HOLogic.dest_eq; val ([lhs', rhs'], ctxt_lifted) = generalize_lift_terms af_inst [lhs, rhs] ctxt_Ts; val lifted = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs')); val (lifted', ctxt') = yield_singleton (Variable.import_terms true) lifted ctxt_lifted; fun tac {prems, context} = HEADGOAL (general_normalize_rel_tac context af THEN' head_cong_tac context af [] THEN' resolve_tac context [prems MRS thm]); val thm' = singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] lifted' tac); val thm'' = Raw_Simplifier.fold_rule ctxt (unfolds_of_afun af) thm'; in thm'' end; fun forward_lift_attrib name = Thm.rule_attribute [] (fn context => fn thm => let val af = afun_of_generic context (intern context name) (* FIXME !?!? *) in forward_lift_rule (Context.proof_of context) af thm end); (* High-level tactics *) fun unfold_wrapper_tac ctxt = AUTO_AFUNS false (fn afs => Simplifier.safe_asm_full_simp_tac (ctxt addsimps flat (map unfolds_of_afun afs))) ctxt; fun fold_wrapper_tac ctxt = AUTO_AFUN true (fold_goal_tac ctxt o unfolds_of_afun) ctxt; fun WRAPPER tac ctxt opt_af = REPEAT_DETERM o resolve_tac ctxt [@{thm allI}] THEN' Subgoal.FOCUS (fn {context = ctxt, params, ...} => let val renames = map (swap o apsnd Thm.term_of) params in AUTO_AFUNS false (EVERY' o map (afun_unfold_tac ctxt)) ctxt opt_af 1 THEN AUTO_AFUN true (fn af => afun_unfold_tac ctxt af THEN' CONVERSION Drule.beta_eta_conversion THEN' tac ctxt af THEN' head_cong_tac ctxt af renames) ctxt opt_af 1 end) ctxt THEN' Raw_Simplifier.rewrite_goal_tac ctxt [Drule.triv_forall_equality]; val normalize_wrapper_tac = WRAPPER normalize_rel_tac; val lifting_wrapper_tac = WRAPPER general_normalize_rel_tac; val parse_opt_afun = Scan.peek (fn context => Scan.option Parse.name >> Option.map (intern context #> afun_of_generic context)); (** Declaration **) (* Combinator setup *) fun declare_combinators combs phi = let val (names, thms) = split_list combs; val thms' = map (Morphism.thm phi) thms; fun add_combs (defs, rules) = (fold (Symtab.insert (K false)) (names ~~ thms') defs, rules); in Data.map (map_data add_combs I I) end; val setup_combinators = Local_Theory.declaration {syntax = false, pervasive = false} o declare_combinators; fun combinator_of_red thm = let val (lhs, _) = Logic.dest_equals (Thm.prop_of thm); val (head, _) = strip_comb lhs; in #1 (dest_Const head) end; fun register_combinator_rule weak_premises thm context = let val (lhs, rhs) = Logic.dest_equals (Thm.prop_of thm); val ltvars = Term.add_tvars lhs []; val rtvars = Term.add_tvars rhs []; val _ = if exists (not o member op = ltvars) rtvars then Pretty.breaks [Pretty.str "Combinator equation", Pretty.quote (Syntax.pretty_term (Context.proof_of context) (Thm.prop_of thm)), Pretty.str "has additional type variables on right-hand side."] |> Pretty.block |> Pretty.string_of |> error else (); val (defs, _) = #combinators (Data.get context); val comb_names = Symtab.make (map (fn (name, thm) => (combinator_of_red thm, name)) (Symtab.dest defs)); val rule = mk_combinator_rule comb_names weak_premises thm; fun add_rule (defs, rules) = (defs, insert eq_combinator_rule rule rules); in Data.map (map_data add_rule I I) context end; val combinator_rule_attrib = Thm.declaration_attribute o register_combinator_rule; (* Derivation of combinator reductions *) fun combinator_closure rules have_weak combs = let fun apply rule (cs, changed) = if not (Ord_List.member fast_string_ord cs (conclusion_of_rule rule)) andalso is_applicable_rule rule have_weak (fn prems => Ord_List.subset fast_string_ord (prems, cs)) then (Ord_List.insert fast_string_ord (conclusion_of_rule rule) cs, true) else (cs, changed); fun loop cs = (case fold apply rules (cs, false) of (cs', true) => loop cs' | (_, false) => cs); in loop combs end; fun derive_combinator_red ctxt af_inst red_thms (base_thm, eq_thm) = let val base_prop = Thm.prop_of base_thm; val tvars = Term.add_tvars base_prop []; val (Ts, ctxt_Ts) = mk_TFrees_of (length tvars) (inner_sort_of af_inst) ctxt; - val base_prop' = base_prop - |> Term_Subst.instantiate (Term_Subst.TVars.table (tvars ~~ Ts), Term_Subst.Vars.empty); + val base_prop' = base_prop |> Term_Subst.instantiate (TVars.make (tvars ~~ Ts), Vars.empty); val (lhs, rhs) = Logic.dest_equals base_prop'; val ([lhs', rhs'], ctxt') = generalize_lift_terms af_inst [lhs, rhs] ctxt_Ts; val lifted_prop = (lhs', rhs') |> HOLogic.mk_eq |> HOLogic.mk_Trueprop; val unfold_comb_conv = HOLogic.Trueprop_conv (HOLogic.eq_conv (Conv.top_sweep_conv (K (Conv.rewr_conv eq_thm)) ctxt') Conv.all_conv); val tac = HEADGOAL (CONVERSION unfold_comb_conv THEN' Raw_Simplifier.rewrite_goal_tac ctxt' red_thms THEN' resolve_tac ctxt' [@{thm refl}]); in singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] lifted_prop (K tac)) end; (*derive all instantiations with pure terms which can be simplified by homomorphism*) (*FIXME: more of a workaround than a sensible solution*) fun weak_red_closure ctxt (af_inst, merge_thm) strong_red = let val (lhs, _) = Thm.prop_of strong_red |> Logic.dest_equals; val vars = rev (Term.add_vars lhs []); fun closure [] prev thms = (prev::thms) | closure ((v, af_T)::vs) prev thms = (case try (dest_type ctxt af_inst) af_T of NONE => closure vs prev thms | SOME T_opt => let val (T, ctxt') = (case T_opt of NONE => yield_singleton Variable.invent_types (inner_sort_of af_inst) ctxt |>> TFree | SOME T => (T, ctxt)); val (v', ctxt'') = mk_Free (#1 v) T ctxt'; val pure_v = Thm.cterm_of ctxt'' (lift_term af_inst v'); val next = Drule.instantiate_normalize ([], [((v, af_T), pure_v)]) prev; val next' = Raw_Simplifier.rewrite_rule ctxt'' [merge_thm] next; val next'' = singleton (Variable.export ctxt'' ctxt) next'; in closure vs next'' (prev::thms) end); in closure vars strong_red [] end; fun combinator_red_closure ctxt (comb_defs, rules) (af_inst, merge_thm) weak_reds combs = let val have_weak = not (null weak_reds); val red_thms0 = Symtab.fold (fn (_, thm) => cons (mk_meta_eq thm)) combs weak_reds; val red_thms = flat (map (weak_red_closure ctxt (af_inst, merge_thm)) red_thms0); fun apply rule ((cs, rs), changed) = if not (Symtab.defined cs (conclusion_of_rule rule)) andalso is_applicable_rule rule have_weak (forall (Symtab.defined cs)) then let val conclusion = conclusion_of_rule rule; val def = the (Symtab.lookup comb_defs conclusion); val new_red_thm = derive_combinator_red ctxt af_inst rs (def, thm_of_rule rule); val new_red_thms = weak_red_closure ctxt (af_inst, merge_thm) (mk_meta_eq new_red_thm); in ((Symtab.update (conclusion, new_red_thm) cs, new_red_thms @ rs), true) end else ((cs, rs), changed); fun loop xs = (case fold apply rules (xs, false) of (xs', true) => loop xs' | (_, false) => xs); in #1 (loop (combs, red_thms)) end; (* Preparation of AFun data *) fun mk_terms ctxt (raw_pure, raw_ap, raw_rel, raw_set) = let val thy = Proof_Context.theory_of ctxt; val show_typ = quote o Syntax.string_of_typ ctxt; val show_term = quote o Syntax.string_of_term ctxt; fun closed_poly_term t = let val poly_t = singleton (Variable.polymorphic ctxt) t; in case Term.add_vars (singleton (Variable.export_terms (Proof_Context.augment t ctxt) ctxt) t) [] of [] => (case (Term.hidden_polymorphism poly_t) of [] => poly_t | _ => error ("Hidden type variables in term " ^ show_term t)) | _ => error ("Locally free variables in term " ^ show_term t) end; val pure = closed_poly_term raw_pure; val (tvar, T1) = fastype_of pure |> dest_funT |>> dest_TVar handle TYPE _ => error ("Bad type for pure: " ^ show_typ (fastype_of pure)); val maxidx_pure = maxidx_of_term pure; val ap = Logic.incr_indexes ([], [], maxidx_pure + 1) (closed_poly_term raw_ap); fun bad_ap _ = error ("Bad type for ap: " ^ show_typ (fastype_of ap)); val (T23, (T2, T3)) = fastype_of ap |> dest_funT ||> dest_funT handle TYPE _ => bad_ap (); val maxidx_common = Term.maxidx_term ap maxidx_pure; (*unify type variables, while keeping the live variables separate*) fun no_unifier (T, U) = error ("Unable to infer common functor type from " ^ commas (map show_typ [T, U])); fun unify_ap_type T (tyenv, maxidx) = let val argT = TVar ((Name.aT, maxidx + 1), []); - val T1' = Term_Subst.instantiateT (Term_Subst.TVars.table [(tvar, argT)]) T1; + val T1' = Term_Subst.instantiateT (TVars.make [(tvar, argT)]) T1; val (tyenv', maxidx') = Sign.typ_unify thy (T1', T) (tyenv, maxidx + 1) handle Type.TUNIFY => no_unifier (T1', T); in (argT, (tyenv', maxidx')) end; val (ap_args, (ap_env, maxidx_env)) = fold_map unify_ap_type [T2, T3, T23] (Vartab.empty, maxidx_common); val [T2_arg, T3_arg, T23_arg] = map (Envir.norm_type ap_env) ap_args; val (tvar2, tvar3) = (dest_TVar T2_arg, dest_TVar T3_arg) handle TYPE _ => bad_ap (); val _ = if T23_arg = T2_arg --> T3_arg then () else bad_ap (); val sort = foldl1 (Sign.inter_sort thy) (map #2 [tvar, tvar2, tvar3]); val _ = Sign.of_sort thy (Term.aT sort --> Term.aT sort, sort) orelse error ("Sort constraint " ^ quote (Syntax.string_of_sort ctxt sort) ^ " not closed under function types"); fun update_sort (v, S) (tyenv, maxidx) = (Vartab.update_new (v, (S, TVar ((Name.aT, maxidx + 1), sort))) tyenv, maxidx + 1); val (common_env, _) = fold update_sort [tvar, tvar2, tvar3] (ap_env, maxidx_env); val tvar' = Envir.norm_type common_env (TVar tvar); val pure' = norm_term_types common_env pure; val (tvar2', tvar3') = apply2 (Envir.norm_type common_env) (T2_arg, T3_arg); val ap' = norm_term_types common_env ap; fun bad_set set = error ("Bad type for set: " ^ show_typ (fastype_of set)); fun mk_set set = let val tyenv = Sign.typ_match thy (domain_type (fastype_of set), range_type (fastype_of pure')) Vartab.empty handle Type.TYPE_MATCH => bad_set set; val set' = Envir.subst_term_types tyenv set; val set_tvar = fastype_of set' |> range_type |> HOLogic.dest_setT |> dest_TVar handle TYPE _ => bad_set set; val _ = if Term.eq_tvar (dest_TVar tvar', set_tvar) then () else bad_set set; in ([tvar'], set') end val set = (case raw_set of NONE => ([tvar'], Abs ("x", tvar', HOLogic.mk_UNIV tvar')) | SOME t => mk_set (closed_poly_term t)); val terms = Term_Subst.zero_var_indexes (pack_poly_terms [poly_type_to_term ([tvar'], range_type (fastype_of pure')), ([tvar'], pure'), ([tvar2', tvar3'], ap'), set]); (*TODO: also infer the relator type?*) fun bad_rel rel = error ("Bad type for rel: " ^ show_typ (fastype_of rel)); fun mk_rel rel = let val ((T1, T2), (T1_af, T2_af)) = fastype_of rel |> dest_funT |>> BNF_Util.dest_pred2T ||> BNF_Util.dest_pred2T; val _ = (dest_TVar T1; dest_TVar T2); val _ = if T1 = T2 then bad_rel rel else (); val af_inst = mk_afun_inst (match_poly_terms_type ctxt (terms, 0) (T1_af, maxidx_of_term rel)); val (T1', T2') = apply2 (dest_type ctxt af_inst) (T1_af, T2_af); val _ = if (is_none T1' andalso is_none T2') orelse (T1' = SOME T1 andalso T2' = SOME T2) then () else bad_rel rel; in Term_Subst.zero_var_indexes (pack_poly_terms [([T1, T2], rel)]) end handle TYPE _ => bad_rel rel; val rel = Option.map (mk_rel o closed_poly_term) raw_rel; in (terms, rel) end; fun mk_rel_intros {pure_transfer, ap_rel_fun} = let val pure_rel_intro = pure_transfer RS @{thm rel_funD}; in [pure_rel_intro, ap_rel_fun] end; fun mk_afun_thms ctxt af_inst (hom_thm, ichng_thm, reds, rel_axioms) = let val pure_comp_conv = let val ([T1, T2, T3], ctxt_Ts) = mk_TFrees_of 3 (inner_sort_of af_inst) ctxt; val (((g, f), x), ctxt') = ctxt_Ts |> mk_Free "g" (T2 --> T3) ||>> mk_Free "f" (mk_type af_inst (T1 --> T2)) ||>> mk_Free "x" (mk_type af_inst T1); val comb = mk_comb af_inst; val lhs = comb (T2 --> T3) (lift_term af_inst g, comb (T1 --> T2) (f, x)); val B_g = Abs ("f", T1 --> T2, Abs ("x", T1, Term.betapply (g, Bound 1 $ Bound 0))); val rhs = comb (T1 --> T3) (comb ((T1 --> T2) --> T1 --> T3) (lift_term af_inst B_g, f), x); val prop = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop; val merge_rule = mk_meta_eq hom_thm; val B_intro = the (Symtab.lookup reds "B") |> mk_meta_eq |> Thm.symmetric; val tac = HEADGOAL (Raw_Simplifier.rewrite_goal_tac ctxt' [B_intro, merge_rule] THEN' resolve_tac ctxt' [@{thm refl}]); in singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] prop (K tac)) end; val eq_intros = let val ([T1, T2], ctxt_Ts) = mk_TFrees_of 2 (inner_sort_of af_inst) ctxt; val T12 = mk_type af_inst (T1 --> T2); val (((((x, y), x'), f), g), ctxt') = ctxt_Ts |> mk_Free "x" T1 ||>> mk_Free "y" T1 ||>> mk_Free "x" (mk_type af_inst T1) ||>> mk_Free "f" T12 ||>> mk_Free "g" T12; val pure_fun = mk_pure af_inst T1; val pure_cong = Drule.infer_instantiate' ctxt' (map (SOME o Thm.cterm_of ctxt') [x, y, pure_fun]) @{thm arg_cong}; val ap_fun = mk_ap af_inst (T1, T2); val ap_cong1 = Drule.infer_instantiate' ctxt' (map (SOME o Thm.cterm_of ctxt') [f, g, ap_fun, x']) @{thm arg1_cong}; in Variable.export ctxt' ctxt [pure_cong, ap_cong1] end; val rel_intros = case rel_axioms of NONE => [] | SOME axioms => mk_rel_intros axioms; in {hom = hom_thm, ichng = ichng_thm, reds = reds, rel_thms = rel_axioms, rel_intros = eq_intros @ rel_intros, pure_comp_conv = pure_comp_conv} end; fun reuse_TFrees n S (ctxt, Ts) = let val have_n = Int.min (n, length Ts); val (more_Ts, ctxt') = mk_TFrees_of (n - have_n) S ctxt; in (take have_n Ts @ more_Ts, (ctxt', Ts @ more_Ts)) end; fun mk_comb_prop lift_pos thm af_inst ctxt_Ts = let val base = Thm.prop_of thm; val tvars = Term.add_tvars base []; val (Ts, (ctxt', Ts')) = reuse_TFrees (length tvars) (inner_sort_of af_inst) ctxt_Ts; val base' = base - |> Term_Subst.instantiate (Term_Subst.TVars.table (tvars ~~ Ts), Term_Subst.Vars.empty); + |> Term_Subst.instantiate (TVars.make (tvars ~~ Ts), Vars.empty); val (lhs, rhs) = Logic.dest_equals base'; val (_, lhs_args) = strip_comb lhs; val lift_var = Var o apsnd (mk_type af_inst) o dest_Var; val (lhs_args', subst) = fold_index (fn (i, v) => if member (op =) lift_pos i then apfst (cons v) else map_prod (cons (lift_var v)) (cons (v, lift_var v))) lhs_args ([], []); val (lhs', rhs') = apply2 (subst_lift_term af_inst subst) (lhs, rhs); val lifted = (lhs', rhs') |> HOLogic.mk_eq |> HOLogic.mk_Trueprop; in (fold Logic.all lhs_args' lifted, (ctxt', Ts')) end; fun mk_homomorphism_prop af_inst ctxt_Ts = let val ([T1, T2], (ctxt', Ts')) = reuse_TFrees 2 (inner_sort_of af_inst) ctxt_Ts; val ((f, x), _) = ctxt' |> mk_Free "f" (T1 --> T2) ||>> mk_Free "x" T1; val lhs = mk_comb af_inst (T1 --> T2) (lift_term af_inst f, lift_term af_inst x); val rhs = lift_term af_inst (f $ x); val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); in (Logic.all f (Logic.all x prop), (ctxt', Ts')) end; fun mk_interchange_prop af_inst ctxt_Ts = let val ([T1, T2], (ctxt', Ts')) = reuse_TFrees 2 (inner_sort_of af_inst) ctxt_Ts; val ((f, x), _) = ctxt' |> mk_Free "f" (mk_type af_inst (T1 --> T2)) ||>> mk_Free "x" T1; val lhs = mk_comb af_inst (T1 --> T2) (f, lift_term af_inst x); val T_x = Abs ("f", T1 --> T2, Bound 0 $ x); val rhs = mk_comb af_inst ((T1 --> T2) --> T2) (lift_term af_inst T_x, f); val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); in (Logic.all f (Logic.all x prop), (ctxt', Ts')) end; fun mk_rel_props (af_inst, rel_inst) ctxt_Ts = let fun mk_af_rel tm = let val (T1, T2) = BNF_Util.dest_pred2T (fastype_of tm); in betapply (instantiate_poly_term rel_inst [T1, T2], tm) end; val ([T1, T2, T3], (ctxt', Ts')) = reuse_TFrees 3 (inner_sort_of af_inst) ctxt_Ts; val (pure_R, _) = mk_Free "R" (T1 --> T2 --> @{typ bool}) ctxt'; val rel_pure = BNF_Util.mk_rel_fun pure_R (mk_af_rel pure_R) $ mk_pure af_inst T1 $ mk_pure af_inst T2; val pure_prop = Logic.all pure_R (HOLogic.mk_Trueprop rel_pure); val ((((f, g), x), ap_R), _) = ctxt' |> mk_Free "f" (mk_type af_inst (T1 --> T2)) ||>> mk_Free "g" (mk_type af_inst (T1 --> T3)) ||>> mk_Free "x" (mk_type af_inst T1) ||>> mk_Free "R" (T2 --> T3 --> @{typ bool}); val fun_rel = BNF_Util.mk_rel_fun (mk_eq_on (mk_set af_inst T1 $ x)) ap_R; val rel_ap = Logic.mk_implies (HOLogic.mk_Trueprop (mk_af_rel fun_rel $ f $ g), HOLogic.mk_Trueprop (mk_af_rel ap_R $ mk_comb af_inst (T1 --> T2) (f, x) $ mk_comb af_inst (T1 --> T3) (g, x))); val ap_prop = fold_rev Logic.all [ap_R, f, g, x] rel_ap; in ([pure_prop, ap_prop], (ctxt', Ts')) end; fun mk_interchange ctxt ((comb_defs, _), comb_unfolds) (af_inst, merge_thm) reds = let val T_def = the (Symtab.lookup comb_defs "T"); val T_red = the (Symtab.lookup reds "T"); val (weak_prop, (ctxt', _)) = mk_comb_prop [0] T_def af_inst (ctxt, []); fun tac {context, ...} = HEADGOAL (Raw_Simplifier.rewrite_goal_tac context [Thm.symmetric merge_thm] THEN' resolve_tac context [T_red]); val weak_red = singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] weak_prop tac); in Raw_Simplifier.rewrite_rule ctxt (comb_unfolds) weak_red RS sym end; fun mk_weak_reds ctxt ((comb_defs, _), comb_unfolds) af_inst (hom_thm, ichng_thm, reds) = let val unfolded_reds = Symtab.map (K (Raw_Simplifier.rewrite_rule ctxt comb_unfolds)) reds; val af_thms = mk_afun_thms ctxt af_inst (hom_thm, ichng_thm, unfolded_reds, NONE); val af = mk_afun Binding.empty (pack_afun_inst af_inst) NONE af_thms; fun tac {context, ...} = HEADGOAL (normalize_wrapper_tac context (SOME af) THEN' Raw_Simplifier.rewrite_goal_tac context comb_unfolds THEN' resolve_tac context [refl]); fun mk comb lift_pos = let val def = the (Symtab.lookup comb_defs comb); val (prop, (ctxt', _)) = mk_comb_prop lift_pos def af_inst (ctxt, []); val hol_thm = singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] prop tac); in mk_meta_eq hol_thm end; val uncurry_thm = mk_meta_eq (forward_lift_rule ctxt af @{thm uncurry_pair}); in [mk "C" [1], mk "C" [2], uncurry_thm] end; fun mk_comb_reds ctxt combss af_inst user_combs (hom_thm, user_thms, ichng_thms) = let val ((comb_defs, comb_rules), comb_unfolds) = combss; val merge_thm = mk_meta_eq hom_thm; val user_reds = Symtab.make (user_combs ~~ user_thms); val reds0 = combinator_red_closure ctxt (comb_defs, comb_rules) (af_inst, merge_thm) [] user_reds; val ichng_thm = case ichng_thms of [] => singleton (Variable.export ctxt ctxt) (mk_interchange ctxt combss (af_inst, merge_thm) reds0) | [thm] => thm; val weak_reds = mk_weak_reds ctxt combss af_inst (hom_thm, ichng_thm, reds0); val reds1 = combinator_red_closure ctxt (comb_defs, comb_rules) (af_inst, merge_thm) weak_reds reds0; val unfold = Raw_Simplifier.rewrite_rule ctxt comb_unfolds; in (Symtab.map (K unfold) reds1, ichng_thm) end; fun note_afun_thms af = let val thms = thms_of_afun af; val named_thms = [("homomorphism", [#hom thms]), ("interchange", [#ichng thms]), ("afun_rel_intros", #rel_intros thms)] @ map (fn (name, thm) => ("pure_" ^ name ^ "_conv", [thm])) (Symtab.dest (#reds thms)) @ (case #rel_thms thms of NONE => [] | SOME rel_thms' => [("pure_transfer", [#pure_transfer rel_thms']), ("ap_rel_fun_cong", [#ap_rel_fun rel_thms'])]); val base_name = Binding.name_of (name_of_afun af); fun mk_note (name, thms) = ((Binding.qualify true base_name (Binding.name name), []), [(thms, [])]); in Local_Theory.notes (map mk_note named_thms) #> #2 end; fun register_afun af = let fun decl phi context = Data.map (fn {combinators, afuns, patterns} => let val af' = morph_afun phi af; val (name, afuns') = Name_Space.define context true (name_of_afun af', af') afuns; val patterns' = Item_Net.update (name, patterns_of_afun af') patterns; in {combinators = combinators, afuns = afuns', patterns = patterns'} end) context; in Local_Theory.declaration {syntax = false, pervasive = false} decl end; fun applicative_cmd (((((name, flags), raw_pure), raw_ap), raw_rel), raw_set) lthy = let val comb_unfolds = Named_Theorems.get lthy @{named_theorems combinator_unfold}; val comb_reprs = Named_Theorems.get lthy @{named_theorems combinator_repr}; val (comb_defs, comb_rules) = get_combinators (Context.Proof lthy); val _ = fold (fn name => if Symtab.defined comb_defs name then I else error ("Unknown combinator " ^ quote name)) flags (); val _ = if has_duplicates op = flags then warning "Ignoring duplicate combinators" else (); val user_combs0 = Ord_List.make fast_string_ord flags; val raw_pure' = Syntax.read_term lthy raw_pure; val raw_ap' = Syntax.read_term lthy raw_ap; val raw_rel' = Option.map (Syntax.read_term lthy) raw_rel; val raw_set' = Option.map (Syntax.read_term lthy) raw_set; val (terms, rel) = mk_terms lthy (raw_pure', raw_ap', raw_rel', raw_set'); val derived_combs0 = combinator_closure comb_rules false user_combs0; val required_combs = Ord_List.make fast_string_ord ["B", "I"]; val user_combs = Ord_List.union fast_string_ord user_combs0 (Ord_List.subtract fast_string_ord derived_combs0 required_combs); val derived_combs1 = combinator_closure comb_rules false user_combs; val derived_combs2 = combinator_closure comb_rules true derived_combs1; fun is_redundant comb = eq_list (op =) (derived_combs2, (combinator_closure comb_rules true (Ord_List.remove fast_string_ord comb user_combs))); val redundant_combs = filter is_redundant user_combs; val _ = if null redundant_combs then () else warning ("Redundant combinators: " ^ commas redundant_combs); val prove_interchange = not (Ord_List.member fast_string_ord derived_combs1 "T"); val (af_inst, ctxt_af) = import_afun_inst_raw terms lthy; (* TODO: reuse TFrees from above *) val (rel_insts, ctxt_inst) = (case rel of NONE => (NONE, ctxt_af) | SOME r => let val (rel_inst, ctxt') = import_poly_terms r ctxt_af |>> the_single; val T = fastype_of (#2 rel_inst) |> range_type |> domain_type; val af_inst = match_poly_terms_type ctxt' (terms, 0) (T, ~1) |> mk_afun_inst; in (SOME (af_inst, rel_inst), ctxt') end); val mk_propss = [apfst single o mk_homomorphism_prop af_inst, fold_map (fn comb => mk_comb_prop [] (the (Symtab.lookup comb_defs comb)) af_inst) user_combs, if prove_interchange then apfst single o mk_interchange_prop af_inst else pair [], if is_some rel then mk_rel_props (the rel_insts) else pair []]; val (propss, (ctxt_Ts, _)) = fold_map I mk_propss (ctxt_inst, []); fun repr_tac ctxt = Raw_Simplifier.rewrite_goals_tac ctxt comb_reprs; fun after_qed thmss lthy' = let val [[hom_thm], user_thms, ichng_thms, rel_thms] = map (Variable.export lthy' ctxt_inst) thmss; val (reds, ichng_thm) = mk_comb_reds ctxt_inst ((comb_defs, comb_rules), comb_unfolds) af_inst user_combs (hom_thm, user_thms, ichng_thms); val rel_axioms = case rel_thms of [] => NONE | [thm1, thm2] => SOME {pure_transfer = thm1, ap_rel_fun = thm2}; val af_thms = mk_afun_thms ctxt_inst af_inst (hom_thm, ichng_thm, reds, rel_axioms); val af_thms = map_afun_thms (singleton (Variable.export ctxt_inst lthy)) af_thms; val af = mk_afun name terms rel af_thms; in lthy |> register_afun af |> note_afun_thms af end; in Proof.theorem NONE after_qed ((map o map) (rpair []) propss) ctxt_Ts |> Proof.refine (Method.Basic (SIMPLE_METHOD o repr_tac)) |> Seq.the_result "" end; fun print_afuns ctxt = let fun pretty_afun (name, af) = let val [pT, (_, pure), (_, ap), (_, set)] = unpack_poly_terms (terms_of_afun af); val ([tvar], T) = poly_type_of_term pT; val rel = Option.map (#2 o the_single o unpack_poly_terms) (rel_of_afun af); val combinators = Symtab.keys (#reds (thms_of_afun af)); in Pretty.block (Pretty.fbreaks ([Pretty.block [Pretty.str name, Pretty.str ":", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, Pretty.str "of", Pretty.brk 1, Syntax.pretty_typ ctxt tvar], Pretty.block [Pretty.str "pure:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt pure)], Pretty.block [Pretty.str "ap:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt ap)], Pretty.block [Pretty.str "set:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt set)]] @ (case rel of NONE => [] | SOME rel' => [Pretty.block [Pretty.str "rel:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt rel')]]) @ [Pretty.block ([Pretty.str "combinators:", Pretty.brk 1] @ Pretty.commas (map Pretty.str combinators))])) end; val afuns = sort_by #1 (Name_Space.fold_table cons (get_afun_table (Context.Proof ctxt)) []); in Pretty.writeln (Pretty.big_list "Registered applicative functors:" (map pretty_afun afuns)) end; (* Unfolding *) fun add_unfold_thm name thm context = let val (lhs, _) = Thm.prop_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_eq handle TERM _ => error "Not an equation"; val names = case name of SOME n => [intern context n] | NONE => case match_typ context (Term.fastype_of lhs) of ns as (_::_) => ns | [] => error "Unable to determine applicative functor instance"; val _ = map (afun_of_generic context) names; (*TODO: check equation*) val thm' = mk_meta_eq thm; in fold (fn n => update_afun n (add_unfolds_afun [thm'])) names context end; fun add_unfold_attrib name = Thm.declaration_attribute (add_unfold_thm name); (*TODO: attribute to delete unfolds*) end; diff --git a/thys/Collections/ICF/tools/Locale_Code.thy b/thys/Collections/ICF/tools/Locale_Code.thy --- a/thys/Collections/ICF/tools/Locale_Code.thy +++ b/thys/Collections/ICF/tools/Locale_Code.thy @@ -1,387 +1,386 @@ section \Code Generation from Locales\ theory Locale_Code imports ICF_Tools Ord_Code_Preproc begin text \ Provides a simple mechanism to prepare code equations for constants stemming from locale interpretations. The usage pattern is as follows: \setup Locale_Code.checkpoint\ is called before a series of interpretations, and afterwards, \setup Locale_Code.prepare\ is called. Afterwards, the code generator will correctly recognize expressions involving terms from the locale interpretation. \ text \Tag to indicate pattern deletion\ definition LC_DEL :: "'a \ unit" where "LC_DEL a \ ()" ML \ signature LOCALE_CODE = sig type pat_eq = cterm * thm list val open_block: theory -> theory val close_block: theory -> theory val del_pat: cterm -> theory -> theory val add_pat_eq: cterm -> thm list -> theory -> theory val lc_decl_eq: thm list -> local_theory -> local_theory val lc_decl_del: term -> local_theory -> local_theory val setup: theory -> theory val get_unf_ss: theory -> simpset val tracing_enabled: bool Unsynchronized.ref end structure Locale_Code :LOCALE_CODE = struct open ICF_Tools val tracing_enabled = Unsynchronized.ref false; type pat_eq = cterm * thm list type block_data = {idx:int, del_pats: cterm list, add_pateqs: pat_eq list} val closed_block = {idx = ~1, del_pats=[], add_pateqs=[]}; fun init_block idx = {idx = idx, del_pats=[], add_pateqs=[]}; fun is_open ({idx,...}:block_data) = idx <> ~1; fun assert_open bd = if is_open bd then () else error "Locale_Code: No open block"; fun assert_closed bd = if is_open bd then error "Locale_Code: Block already open" else (); fun merge_bd (bd1,bd2) = ( if is_open bd1 orelse is_open bd2 then error "Locale_Code: Merge with open block" else (); closed_block ); fun bd_add_del_pats ps {idx,del_pats,add_pateqs} = {idx = idx, del_pats = ps@del_pats, add_pateqs = add_pateqs}; fun bd_add_add_pateqs pes {idx,del_pats,add_pateqs} = {idx = idx, del_pats = del_pats, add_pateqs = pes@add_pateqs}; structure BlockData = Theory_Data ( type T = block_data val empty = (closed_block) val extend = I val merge = merge_bd ); structure FoldSSData = Oc_Simpset ( val prio = 5; val name = "Locale_Code"; ); fun add_unf_thms thms thy = let val ctxt = Proof_Context.init_global thy val thms = map Thm.symmetric thms in FoldSSData.map (fn ss => put_simpset ss ctxt |> sss_add thms |> simpset_of ) thy end val get_unf_ss = FoldSSData.get; (* First order match with fixed head *) fun match_fixed_head (pat,obj) = let (* Match heads *) val inst = Thm.first_order_match (chead_of pat, chead_of obj); val pat = Thm.instantiate_cterm inst pat; (* Now match whole pattern *) val inst = Thm.first_order_match (pat, obj); in inst end; val matches_fixed_head = can match_fixed_head; (* First order match of heads only *) fun match_heads (pat,obj) = Thm.first_order_match (chead_of pat, chead_of obj); val matches_heads = can match_heads; val pat_nargs = Thm.term_of #> strip_comb #> #2 #> length; (* Adjust a theorem to exactly match pattern *) fun norm_thm_pat (thm,pat) = let val thm = norm_def_thm thm; val na_pat = pat_nargs pat; val lhs = Thm.lhs_of thm; val na_lhs = pat_nargs lhs; val lhs' = if na_lhs > na_pat then funpow (na_lhs - na_pat) Thm.dest_fun lhs else lhs; val inst = Thm.first_order_match (lhs',pat); in Thm.instantiate inst thm end; fun del_pat_matches cpat (epat,_) = if pat_nargs cpat = 0 then matches_heads (cpat,epat) else matches_fixed_head (cpat,epat); (* Pattern-Eqs from specification *) local datatype action = ADD of (cterm * thm list) | DEL of cterm fun filter_pat_eq thy thms pat = let val cpat = Thm.global_cterm_of thy pat; in if (pat_nargs cpat = 0) then NONE else let val thms' = fold (fn thm => fn acc => case try norm_thm_pat (thm, cpat) of NONE => acc | SOME thm => thm::acc ) thms []; in case thms' of [] => NONE | _ => SOME (ADD (cpat,thms')) end end; fun process_actions acc [] = acc | process_actions acc (ADD peq::acts) = process_actions (peq::acc) acts | process_actions acc (DEL cpat::acts) = let val acc' = filter (not o curry renames_cterm cpat o fst) acc; val _ = if length acc = length acc' then warning ("Locale_Code: LC_DEL without effect: " ^ @{make_string} cpat) else (); in process_actions acc' acts end; fun pat_eqs_of_spec thy {rough_classification = Spec_Rules.Equational _, terms = pats, rules = thms, ...} = map_filter (filter_pat_eq thy thms) pats | pat_eqs_of_spec thy {rough_classification = Spec_Rules.Unknown, terms = [Const (@{const_name LC_DEL},_)$pat], ...} = [(DEL (Thm.global_cterm_of thy pat))] | pat_eqs_of_spec _ _ = []; in fun pat_eqs_of_specs thy specs = map (pat_eqs_of_spec thy) specs |> flat |> rev |> process_actions []; end; fun is_proper_pat cpat = let val pat = Thm.term_of cpat; val (f,args) = strip_comb pat; in is_Const f andalso args <> [] andalso not (is_Var (hd (rev args))) end; (* Instantiating pattern-eq *) local (* Get constant name for instantiation pattern *) fun inst_name lthy pat = let val (fname,params) = case strip_comb pat of ((Const (fname,_)),params) => (fname,params) | _ => raise TERM ("inst_name: Expected pattern",[pat]); fun pname (Const (n,_)) = Long_Name.base_name n | pname (s$t) = pname s ^ "_" ^ pname t | pname _ = Name.uu; in space_implode "_" (Long_Name.base_name fname::map pname params) |> gen_variant (can (Proof_Context.read_const {proper = true, strict = false} lthy)) end; in fun inst_pat_eq (cpat,thms) = wrap_lthy_result_global (fn lthy => let val (((instT,inst),thms),lthy) = Variable.import true thms lthy; - val cpat = - Thm.instantiate_cterm (Term_Subst.TVars.dest instT, Term_Subst.Vars.dest inst) cpat; + val cpat = Thm.instantiate_cterm (TVars.dest instT, Vars.dest inst) cpat; val pat = Thm.term_of cpat; val name = inst_name lthy pat; val ((_,(_,def_thm)),lthy) = Local_Theory.define ((Binding.name name,NoSyn), ((Binding.name (Thm.def_name name),[]),pat)) lthy; val thms' = map (Local_Defs.fold lthy [def_thm]) thms; in ((def_thm,thms'),lthy) end) (fn m => fn (def_thm,thms') => (Morphism.thm m def_thm, map (Morphism.thm m) thms')) #> (fn ((def_thm,thms'),thy) => let val thy = thy |> add_unf_thms [def_thm] |> Code.declare_default_eqns_global (map (rpair true) thms'); in thy end) end (* Bookkeeping *) fun new_specs thy = let val bd = BlockData.get thy; val _ = assert_open bd; val ctxt = Proof_Context.init_global thy; val srules = Spec_Rules.get ctxt; val res = take (length srules - #idx bd) srules; in res end fun open_block thy = let val bd = BlockData.get thy; val _ = assert_closed bd; val ctxt = Proof_Context.init_global thy; val idx = length (Spec_Rules.get ctxt); val thy = BlockData.map (K (init_block idx)) thy; in thy end; fun process_block bd thy = let fun filter_del_pats cpat peqs = let val peqs' = filter (not o del_pat_matches cpat) peqs val _ = if length peqs = length peqs' then warning ("Locale_Code: No pattern-eqs matching filter: " ^ @{make_string} cpat) else (); in peqs' end; fun filter_add_pats (orig_pat,_) = forall (fn (add_pat,_) => not (renames_cterm (orig_pat,add_pat))) (#add_pateqs bd); val specs = new_specs thy; val peqs = pat_eqs_of_specs thy specs |> fold filter_del_pats (#del_pats bd) |> filter filter_add_pats; val peqs = peqs @ #add_pateqs bd; val peqs = rev peqs; (* Important: Process equations in the order in that they have been added! *) val _ = if !tracing_enabled then map (fn peq => (tracing (@{make_string} peq); ())) peqs else []; val thy = thy |> fold inst_pat_eq peqs; in thy end; fun close_block thy = let val bd = BlockData.get thy; val _ = assert_open bd; val thy = process_block bd thy |> BlockData.map (K closed_block); in thy end; fun del_pat cpat thy = let val bd = BlockData.get thy; val _ = assert_open bd; val bd = bd_add_del_pats [cpat] bd; val thy = BlockData.map (K bd) thy; in thy end; fun add_pat_eq cpat thms thy = let val _ = is_proper_pat cpat orelse raise CTERM ("add_pat_eq: Not a proper pattern",[cpat]); fun ntp thm = case try norm_thm_pat (thm,cpat) of NONE => raise THM ("add_pat_eq: Theorem does not match pattern",~1,[thm]) | SOME thm => thm; val thms = map ntp thms; val thy = BlockData.map (bd_add_add_pateqs [(cpat,thms)]) thy; in thy end; local fun cpat_of_thm thm = let fun strip ct = case Thm.term_of ct of (_$Var _) => strip (Thm.dest_fun ct) | _ => ct; in strip (Thm.lhs_of thm) end; fun adjust_length (cpat1,cpat2) = let val n1 = cpat1 |> Thm.term_of |> strip_comb |> #2 |> length; val n2 = cpat2 |> Thm.term_of |> strip_comb |> #2 |> length; in if n1>n2 then (funpow (n1-n2) Thm.dest_fun cpat1, cpat2) else (cpat1, funpow (n2-n1) Thm.dest_fun cpat2) end fun find_match cpat cpat' = SOME (cpat,rename_cterm (cpat',cpat)) handle Pattern.MATCH => (case Thm.term_of cpat' of _$_ => find_match (Thm.dest_fun cpat) (Thm.dest_fun cpat') | _ => NONE ); (* Common head of definitional theorems *) fun comp_head thms = case map norm_def_thm thms of [] => NONE | thm::thms => let fun ch [] r = SOME r | ch (thm::thms) (cpat,acc) = let val cpat' = cpat_of_thm thm; val (cpat,cpat') = adjust_length (cpat,cpat') in case find_match cpat cpat' of NONE => NONE | SOME (cpat,inst) => ch thms (cpat, Drule.instantiate_normalize inst thm :: acc) end; in ch thms (cpat_of_thm thm,[thm]) end; in fun lc_decl_eq thms lthy = case comp_head thms of SOME (cpat,thms) => let val _ = if !tracing_enabled then tracing ("decl_eq: " ^ @{make_string} cpat ^ ": " ^ @{make_string} thms) else (); fun decl m = let val cpat'::thms' = Morphism.fact m (Drule.mk_term cpat :: thms); val cpat' = Drule.dest_term cpat'; in Context.mapping (BlockData.map (bd_add_add_pateqs [(cpat',thms')])) I end in lthy |> Local_Theory.declaration {syntax = false, pervasive = false} decl end | NONE => raise THM ("Locale_Code.lc_decl_eq: No common pattern",~1,thms); end; fun lc_decl_del pat = let val ty = fastype_of pat; val dpat = Const (@{const_name LC_DEL},ty --> @{typ unit})$pat; in Spec_Rules.add Binding.empty Spec_Rules.Unknown [dpat] [] end (* Package setup *) val setup = FoldSSData.setup; end \ setup Locale_Code.setup attribute_setup lc_delete = \ Parse.and_list1' ICF_Tools.parse_cpat >> (fn cpats => Thm.declaration_attribute (K (Context.mapping (fold Locale_Code.del_pat cpats) I))) \ "Locale_Code: Delete patterns for current block" attribute_setup lc_add = \ Parse.and_list1' (ICF_Tools.parse_cpat -- Attrib.thms) >> (fn peqs => Thm.declaration_attribute (K (Context.mapping (fold (uncurry Locale_Code.add_pat_eq) peqs) I))) \ "Locale_Code: Add pattern-eqs for current block" end diff --git a/thys/Forcing/Synthetic_Definition.thy b/thys/Forcing/Synthetic_Definition.thy --- a/thys/Forcing/Synthetic_Definition.thy +++ b/thys/Forcing/Synthetic_Definition.thy @@ -1,128 +1,128 @@ section\Automatic synthesis of formulas\ theory Synthetic_Definition imports Utils keywords "synthesize" :: thy_decl % "ML" and "synthesize_notc" :: thy_decl % "ML" and "from_schematic" begin ML\ val $` = curry ((op $) o swap) infix $` fun pair f g x = (f x, g x) fun display kind pos (thms,thy) = let val _ = Proof_Display.print_results true pos thy ((kind,""),[thms]) in thy end fun prove_tc_form goal thms ctxt = Goal.prove ctxt [] [] goal (fn _ => rewrite_goal_tac ctxt thms 1 THEN TypeCheck.typecheck_tac ctxt) fun prove_sats goal thms thm_auto ctxt = let val ctxt' = ctxt |> Simplifier.add_simp (thm_auto |> hd) in Goal.prove ctxt [] [] goal (fn _ => rewrite_goal_tac ctxt thms 1 THEN PARALLEL_ALLGOALS (asm_simp_tac ctxt') THEN TypeCheck.typecheck_tac ctxt') end fun is_mem (@{const mem} $ _ $ _) = true | is_mem _ = false fun synth_thm_sats def_name term lhs set env hyps vars vs pos thm_auto lthy = let val (_,tm,ctxt1) = Utils.thm_concl_tm lthy term val (thm_refs,ctxt2) = Variable.import true [Proof_Context.get_thm lthy term] ctxt1 |>> #2 val vs' = map (Thm.term_of o #2) vs val vars' = map (Thm.term_of o #2) vars val r_tm = tm |> Utils.dest_lhs_def |> fold (op $`) vs' val sats = @{const apply} $ (@{const satisfies} $ set $ r_tm) $ env val rhs = @{const IFOL.eq(i)} $ sats $ (@{const succ} $ @{const zero}) val concl = @{const IFOL.iff} $ lhs $ rhs val g_iff = Logic.list_implies(hyps, Utils.tp concl) val thm = prove_sats g_iff thm_refs thm_auto ctxt2 val name = Binding.name (def_name ^ "_iff_sats") val thm = Utils.fix_vars thm (map (#1 o dest_Free) vars') lthy in Local_Theory.note ((name, []), [thm]) lthy |> display "theorem" pos end fun synth_thm_tc def_name term hyps vars pos lthy = let val (_,tm,ctxt1) = Utils.thm_concl_tm lthy term val (thm_refs,ctxt2) = Variable.import true [Proof_Context.get_thm lthy term] ctxt1 |>> #2 val vars' = map (Thm.term_of o #2) vars val tc_attrib = @{attributes [TC]} val r_tm = tm |> Utils.dest_lhs_def |> fold (op $`) vars' val concl = @{const mem} $ r_tm $ @{const formula} val g = Logic.list_implies(hyps, Utils.tp concl) val thm = prove_tc_form g thm_refs ctxt2 val name = Binding.name (def_name ^ "_type") val thm = Utils.fix_vars thm (map (#1 o dest_Free) vars') ctxt2 in Local_Theory.note ((name, tc_attrib), [thm]) lthy |> display "theorem" pos end fun synthetic_def def_name thmref pos tc auto thy = let val (thm_ref,_) = thmref |>> Facts.ref_name val thm = Proof_Context.get_thm thy thm_ref; val thm_vars = rev (Term.add_vars (Thm.full_prop_of thm) []); val (((_,inst),thm_tms),_) = Variable.import true [thm] thy - val vars = map (fn v => (v, the (Term_Subst.Vars.lookup inst v))) thm_vars; + val vars = map (fn v => (v, the (Vars.lookup inst v))) thm_vars; val (tm,hyps) = thm_tms |> hd |> pair Thm.concl_of Thm.prems_of val (lhs,rhs) = tm |> Utils.dest_iff_tms o Utils.dest_trueprop val ((set,t),env) = rhs |> Utils.dest_sats_frm fun relevant ts (@{const mem} $ t $ _) = not (Term.is_Free t) orelse member (op =) ts (t |> Term.dest_Free |> #1) | relevant _ _ = false val t_vars = sort_strings (Term.add_free_names t []) val vs = filter (member (op =) t_vars o #1 o #1 o #1) vars val at = fold_rev (lambda o Thm.term_of o #2) vs t val hyps' = filter (relevant t_vars o Utils.dest_trueprop) hyps in Local_Theory.define ((Binding.name def_name, NoSyn), ((Binding.name (def_name ^ "_def"), []), at)) thy |> #2 |> (if tc then synth_thm_tc def_name (def_name ^ "_def") hyps' vs pos else I) |> (if auto then synth_thm_sats def_name (def_name ^ "_def") lhs set env hyps vars vs pos thm_tms else I) end \ ML\ local val synth_constdecl = Parse.position (Parse.string -- ((Parse.$$$ "from_schematic" |-- Parse.thm))); val _ = Outer_Syntax.local_theory \<^command_keyword>\synthesize\ "ML setup for synthetic definitions" (synth_constdecl >> (fn ((bndg,thm),p) => synthetic_def bndg thm p true true)) val _ = Outer_Syntax.local_theory \<^command_keyword>\synthesize_notc\ "ML setup for synthetic definitions" (synth_constdecl >> (fn ((bndg,thm),p) => synthetic_def bndg thm p false false)) in end \ text\The \<^ML>\synthetic_def\ function extracts definitions from schematic goals. A new definition is added to the context. \ (* example of use *) (* schematic_goal mem_formula_ex : assumes "m\nat" "n\ nat" "env \ list(M)" shows "nth(m,env) \ nth(n,env) \ sats(M,?frm,env)" by (insert assms ; (rule sep_rules empty_iff_sats cartprod_iff_sats | simp del:sats_cartprod_fm)+) synthesize "\" from_schematic mem_formula_ex *) end diff --git a/thys/Forcing/utils.ML b/thys/Forcing/utils.ML --- a/thys/Forcing/utils.ML +++ b/thys/Forcing/utils.ML @@ -1,124 +1,124 @@ signature UTILS = sig val binop : term -> term -> term -> term val add_: term -> term -> term val app_: term -> term -> term val concat_: term -> term -> term val dest_apply: term -> term * term val dest_iff_lhs: term -> term val dest_iff_rhs: term -> term val dest_iff_tms: term -> term * term val dest_lhs_def: term -> term val dest_rhs_def: term -> term val dest_satisfies_tms: term -> term * term val dest_satisfies_frm: term -> term val dest_eq_tms: term -> term * term val dest_sats_frm: term -> (term * term) * term val dest_trueprop: term -> term val eq_: term -> term -> term val fix_vars: thm -> string list -> Proof.context -> thm val formula_: term val freeName: term -> string val isFree: term -> bool val length_: term -> term val list_: term -> term val lt_: term -> term -> term val mem_: term -> term -> term val mk_FinSet: term list -> term val mk_Pair: term -> term -> term val mk_ZFlist: ('a -> term) -> 'a list -> term val mk_ZFnat: int -> term val nat_: term val nth_: term -> term -> term val subset_: term -> term -> term val thm_concl_tm : Proof.context -> xstring -> - cterm Term_Subst.Vars.table * term * Proof.context + cterm Vars.table * term * Proof.context val to_ML_list: term -> term list val tp: term -> term end structure Utils : UTILS = struct (* Smart constructors for ZF-terms *) fun binop h t u = h $ t $ u val mk_Pair = binop @{const Pair} fun mk_FinSet nil = @{const zero} | mk_FinSet (e :: es) = @{const cons} $ e $ mk_FinSet es fun mk_ZFnat 0 = @{const zero} | mk_ZFnat n = @{const succ} $ mk_ZFnat (n-1) fun mk_ZFlist _ nil = @{const "Nil"} | mk_ZFlist f (t :: ts) = @{const "Cons"} $ f t $ mk_ZFlist f ts fun to_ML_list (@{const Nil}) = nil | to_ML_list (@{const Cons} $ t $ ts) = t :: to_ML_list ts | to_ML_list _ = nil fun isFree (Free (_,_)) = true | isFree _ = false fun freeName (Free (n,_)) = n | freeName _ = error "Not a free variable" val app_ = binop @{const apply} fun tp x = @{const Trueprop} $ x fun length_ env = @{const length} $ env val nth_ = binop @{const nth} val add_ = binop @{const add} val mem_ = binop @{const mem} val subset_ = binop @{const Subset} val lt_ = binop @{const lt} val concat_ = binop @{const app} val eq_ = binop @{const IFOL.eq(i)} (* Abbreviation for sets *) fun list_ set = @{const list} $ set val nat_ = @{const nat} val formula_ = @{const formula} (** Destructors of terms **) fun dest_eq_tms (Const (@{const_name IFOL.eq},_) $ t $ u) = (t, u) | dest_eq_tms t = raise TERM ("dest_eq_tms", [t]) fun dest_lhs_def (Const (@{const_name Pure.eq},_) $ x $ _) = x | dest_lhs_def t = raise TERM ("dest_lhs_def", [t]) fun dest_rhs_def (Const (@{const_name Pure.eq},_) $ _ $ y) = y | dest_rhs_def t = raise TERM ("dest_rhs_def", [t]) fun dest_apply (@{const apply} $ t $ u) = (t,u) | dest_apply t = raise TERM ("dest_applies_op", [t]) fun dest_satisfies_tms (@{const Formula.satisfies} $ A $ f) = (A,f) | dest_satisfies_tms t = raise TERM ("dest_satisfies_tms", [t]); val dest_satisfies_frm = #2 o dest_satisfies_tms fun dest_sats_frm t = t |> dest_eq_tms |> #1 |> dest_apply |>> dest_satisfies_tms ; fun dest_trueprop (@{const IFOL.Trueprop} $ t) = t | dest_trueprop t = t fun dest_iff_tms (@{const IFOL.iff} $ t $ u) = (t, u) | dest_iff_tms t = raise TERM ("dest_iff_tms", [t]) val dest_iff_lhs = #1 o dest_iff_tms val dest_iff_rhs = #2 o dest_iff_tms fun thm_concl_tm ctxt thm_ref = let val (((_,vars),thm_tms),ctxt1) = Variable.import true [Proof_Context.get_thm ctxt thm_ref] ctxt in (vars, thm_tms |> hd |> Thm.concl_of, ctxt1) end fun fix_vars thm vars ctxt = let val (_, ctxt1) = Variable.add_fixes vars ctxt in singleton (Proof_Context.export ctxt1 ctxt) thm end end ; diff --git a/thys/IMP2/lib/subgoal_focus_some.ML b/thys/IMP2/lib/subgoal_focus_some.ML --- a/thys/IMP2/lib/subgoal_focus_some.ML +++ b/thys/IMP2/lib/subgoal_focus_some.ML @@ -1,181 +1,181 @@ (* Generalized version of Subgoal.FOCUS, where the premises to be be focused on can be selected by a filter function. This generalizes the do_prems from bool to Proof.context -> cterm -> bool Author: Peter Lammich. Derived from subgoal_focus.ML. *) signature SUBGOAL_FOCUS_SOME = sig type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: (bool * cterm) list, concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} type prem_filter = Proof.context -> cterm -> bool val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm val focus: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_some_prems: prem_filter -> Proof.context -> int -> binding list option -> thm -> focus * thm val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> (bool * cterm) list -> int -> thm -> thm -> thm Seq.seq val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_SOME_PREMS: prem_filter -> (focus -> tactic) -> Proof.context -> int -> tactic end structure Subgoal_Focus_Some : SUBGOAL_FOCUS_SOME = struct type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: (bool * cterm) list, concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} type prem_filter = Proof.context -> cterm -> bool fun partition P l = (filter P l, filter_out P l) fun invert_perm l = tag_list 0 l |> map swap |> order_list fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st = let val st = raw_st |> Thm.transfer (Proof_Context.theory_of ctxt) |> Raw_Simplifier.norm_hhf_protect ctxt; val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1; val (asms, concl) = (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) val asms = map (`(do_prems ctxt2)) asms val fasms = filter fst asms |> map snd val nasms = filter_out fst asms |> map snd val concl = Drule.list_implies (nasms, concl) val text = fasms @ (if do_concl then [concl] else []); val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2; - val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst []; + val schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst []; - val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms); + val schematics = (TVars.dest schematic_types, schematic_terms); val asms' = map (apsnd (Thm.instantiate_cterm schematics)) asms; val fasms' = filter fst asms' |> map snd val concl' = Thm.instantiate_cterm schematics concl; val (prems, context) = Assumption.add_assumes fasms' ctxt3; in ({context = context, params = params, prems = prems, asms = asms', concl = concl', schematics = schematics}, Goal.init concl') end; val focus_params = gen_focus (K (K false), false); val focus_params_fixed = gen_focus (K (K false), true); val focus_prems = gen_focus (K (K true), false); val focus = gen_focus (K (K true), true); fun focus_some_prems flt = gen_focus (flt,false) (* B [?'b, ?y] ---------------- B ['b, y params] *) fun lift_import idx params th ctxt = let val ((_, [th']), ctxt') = Variable.importT [th] ctxt; val Ts = map Thm.typ_of_cterm params; val ts = map Thm.term_of params; val prop = Thm.full_prop_of th'; val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []; val vars = rev (Term.add_vars prop []); val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt'; fun var_inst v y = let val ((x, i), T) = v; val (U, args) = if member (op =) concl_vars v then (T, []) else (Ts ---> T, ts); val u = Free (y, U); in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; val (inst1, inst2) = split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys)); val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th'; in ((inst2, th''), ctxt'') end; (* [x, A x] : B x ==> C ------------------ [!!x. A x ==> B x] : C *) fun lift_subgoals ctxt params asms th = let fun lift ct = fold_rev (Thm.all_name ctxt) params (Drule.list_implies (asms, ct)); val unlift = fold (Thm.elim_implies o Thm.assume) asms o Drule.forall_elim_list (map #2 params) o Thm.assume; val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th)); val th' = fold (Thm.elim_implies o unlift) subgoals th; in (subgoals, th') end; fun retrofit ctxt1 ctxt0 params all_asms i st1 st0 = let val asms = filter fst all_asms |> map snd val perm = tag_list 0 all_asms |> partition (fst o snd) |> op @ |> map fst val perm = invert_perm perm val idx = Thm.maxidx_of st0 + 1; val ps = map #2 params; val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1; val (subgoals, st3) = lift_subgoals ctxt2 params asms st2; val result = st3 |> Goal.conclude |> Drule.implies_intr_list asms |> Drule.rearrange_prems perm |> Drule.forall_intr_list ps |> Drule.implies_intr_list subgoals |> fold_rev (Thm.forall_intr o #1) subgoal_inst |> fold (Thm.forall_elim o #2) subgoal_inst |> Thm.adjust_maxidx_thm idx |> singleton (Variable.export ctxt2 ctxt0); in Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false} (false, result, Thm.nprems_of st1) i st0 end; fun GEN_FOCUS flags tac ctxt i st = if Thm.nprems_of st < i then Seq.empty else let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags (ctxt |> Variable.set_bound_focus true) i NONE st; in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end; val FOCUS_PARAMS = GEN_FOCUS (K (K false), false); val FOCUS_PARAMS_FIXED = GEN_FOCUS (K (K false), true); val FOCUS_PREMS = GEN_FOCUS (K (K true), false); val FOCUS = GEN_FOCUS (K (K true), true); fun FOCUS_SOME_PREMS flt = GEN_FOCUS (flt, true); end diff --git a/thys/Nominal2/nominal_inductive.ML b/thys/Nominal2/nominal_inductive.ML --- a/thys/Nominal2/nominal_inductive.ML +++ b/thys/Nominal2/nominal_inductive.ML @@ -1,445 +1,445 @@ (* Title: nominal_inductive.ML Author: Christian Urban Author: Tjark Weber Infrastructure for proving strong induction theorems for inductive predicates involving nominal datatypes. Code based on an earlier version by Stefan Berghofer. *) signature NOMINAL_INDUCTIVE = sig val prove_strong_inductive: string list -> string list -> term list list -> thm -> thm list -> Proof.context -> Proof.state val prove_strong_inductive_cmd: xstring * (string * string list) list -> Proof.context -> Proof.state end structure Nominal_Inductive : NOMINAL_INDUCTIVE = struct fun mk_cplus p q = Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q fun mk_cminus p = Thm.apply @{cterm "uminus :: perm => perm"} p fun minus_permute_intro_tac ctxt p = resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}] fun minus_permute_elim p thm = thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) (* fixme: move to nominal_library *) fun real_head_of (@{term Trueprop} $ t) = real_head_of t | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of (Const (@{const_name HOL.induct_forall}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of t = head_of t fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = if null avoid then [] else let val vc_goal = concl_args |> HOLogic.mk_tuple |> mk_fresh_star avoid_trm |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params val finite_goal = avoid_trm |> mk_finite |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params in [vc_goal, finite_goal] end (* fixme: move to nominal_library *) fun map_term prop f trm = if prop trm then f trm else case trm of (t1 $ t2) => map_term prop f t1 $ map_term prop f t2 | Abs (x, T, t) => Abs (x, T, map_term prop f t) | _ => trm fun add_p_c p (c, c_ty) trm = let val (P, args) = strip_comb trm val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = map (mk_perm p) args in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> (fn t => HOLogic.all_const c_ty $ lambda c t ) |> (fn t => HOLogic.all_const @{typ perm} $ lambda p t) end fun induct_forall_const T = Const (@{const_name HOL.induct_forall}, (T --> @{typ bool}) --> @{typ bool}) fun mk_induct_forall (a, T) t = induct_forall_const T $ Abs (a, T, t) fun add_c_prop qnt Ps (c, c_name, c_ty) trm = let fun add t = let val (P, args) = strip_comb t val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = args |> qnt ? map (incr_boundvars 1) in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> qnt ? mk_induct_forall (c_name, c_ty) end in map_term (member (op =) Ps o head_of) add trm end fun prep_prem Ps c_name c_ty (avoid, avoid_trm) (params, prems, concl) = let val prems' = prems |> map (incr_boundvars 1) |> map (add_c_prop true Ps (Bound 0, c_name, c_ty)) val avoid_trm' = avoid_trm |> fold_rev absfree (params @ [(c_name, c_ty)]) |> strip_abs_body |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |> HOLogic.mk_Trueprop val prems'' = if null avoid then prems' else avoid_trm' :: prems' val concl' = concl |> incr_boundvars 1 |> add_c_prop false Ps (Bound 0, c_name, c_ty) in mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' end (* fixme: move to nominal_library *) fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2) | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2) | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2) | same_name _ = false (* fixme: move to nominal_library *) fun map7 _ [] [] [] [] [] [] [] = [] | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = f x y z u v r s :: map7 f xs ys zs us vs rs ss (* local abbreviations *) local open Nominal_Permeq in (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel} fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig end val all_elims = let fun spec' ct = Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec} in fold (fn ct => fn th => th RS spec' ct) end fun helper_tac flag prm p ctxt = Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} => let val prems' = prems |> map (minus_permute_elim p) |> map (eqvt_srule ctxt') val prm' = (prems' MRS prm) |> flag ? (all_elims [p]) |> flag ? (eqvt_srule ctxt') in asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1 end) ctxt fun non_binder_tac prem intr_cvars Ps ctxt = Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} => let val (prms, p, _) = split_last2 (map snd params) val prm_tys = map (fastype_of o Thm.term_of) prms val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms) |> eqvt_srule ctxt' (* for inductive-premises*) fun tac1 prm = helper_tac true prm p ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac ctxt' p, eqvt_stac ctxt', helper_tac false prm p ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i in EVERY1 [ eqvt_stac ctxt', resolve_tac ctxt' [prem'], RANGE (map (SUBGOAL o select) prems) ] end) ctxt fun fresh_thm ctxt user_thm p c concl_args avoid_trm = let val conj1 = mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c val conj2 = mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) concl_args))) (Bound 0) val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2)) |> HOLogic.mk_Trueprop val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ @{thms fresh_star_Pair fresh_star_permute_iff} val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in Goal.prove ctxt [] [] fresh_goal (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2} THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o eresolve_tac ctxt @{thms conjE}, simp]))) end val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x" by (simp add: supp_perm_eq)} val fresh_star_plus = @{lemma "fresh_star (permute q (permute p x)) c ==> fresh_star (permute (q + p) x) c" by (simp add: permute_plus)} fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => let val (prms, p, c) = split_last2 (map snd params) val prm_trms = map Thm.term_of prms val prm_tys = map fastype_of prm_trms val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems))) val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm' val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result (K (EVERY1 [eresolve_tac ctxt @{thms exE}, full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms supp_Pair fresh_star_Un}), REPEAT o eresolve_tac ctxt @{thms conjE}, dresolve_tac ctxt [fresh_star_plus], REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms) |> eqvt_srule ctxt' val fprop' = eqvt_srule ctxt' fprop val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop']) (* for inductive-premises*) fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p), eqvt_stac ctxt', helper_tac false prm (mk_cplus q p) ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl) (fn {context = ctxt'', ...} => EVERY1 [ CONVERSION (expand_conv_bot ctxt''), eqvt_stac ctxt'', resolve_tac ctxt'' [prem'], RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) |> singleton (Proof_Context.export ctxt' ctxt) in resolve_tac ctxt [side_thm] 1 end) ctxt fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = let val tac1 = non_binder_tac prem intr_cvars Ps ctxt val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI}, if null avoid then tac1 else tac2 ] end fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args {prems, context = ctxt} = let val cases_tac = map7 (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args in EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ] end val normalise = @{lemma "(Q \ (\p c. P p c)) \ (\c. Q \ P (0::perm) c)" by simp} fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = let val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt val (ind_prems, ind_concl) = raw_induct' |> Thm.prop_of |> Logic.strip_horn |>> map strip_full_horn val params = map (fn (x, _, _) => x) ind_prems val param_trms = (map o map) Free params val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs val intr_vars = (map o map) fst intr_vars_tys val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys val (intr_prems, intr_concls) = intrs |> map Thm.prop_of |> map2 subst_Vars intr_vars_substs |> map Logic.strip_horn |> split_list val intr_concls_args = map (snd o fixed_nonfixed_args ctxt' o HOLogic.dest_Trueprop) intr_concls val avoid_trms = avoids |> (map o map) (setify ctxt') |> map fold_union val vc_compat_goals = map4 mk_vc_compat (avoids ~~ avoid_trms) intr_prems intr_concls_args params val ([c_name, a, p], ctxt'') = Variable.variant_fixes ["c", "'a", "p"] ctxt' val c_ty = TFree (a, @{sort fs}) val c = Free (c_name, c_ty) val p = Free (p, @{typ perm}) val (preconds, ind_concls) = ind_concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map HOLogic.dest_imp |> split_list val Ps = map (fst o strip_comb) ind_concls val ind_concl' = ind_concls |> map (add_p_c p (c, c_ty)) |> (curry (op ~~)) preconds |> map HOLogic.mk_imp |> fold_conj |> HOLogic.mk_Trueprop val ind_prems' = ind_prems |> map2 (prep_prem Ps c_name c_ty) (avoids ~~ avoid_trms) fun after_qed ctxt_outside user_thms ctxt = let val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |> singleton (Proof_Context.export ctxt ctxt_outside) |> Old_Datatype_Aux.split_conj_thm |> map (fn thm => thm RS normalise) |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms permute_zero induct_rulify})) |> map (Drule.rotate_prems (length ind_prems')) |> map zero_var_indexes val qualified_thm_name = pred_names |> map Long_Name.base_name |> space_implode "_" |> (fn s => Binding.qualify false s (Binding.name "strong_induct")) val attrs = [ Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Rule_Cases.case_names rule_names)) ] in ctxt |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms) |> snd end in Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt'' end fun prove_strong_inductive_cmd (pred_name, avoids) ctxt = let val ({names, ...}, {raw_induct, intrs, ...}) = Inductive.the_inductive_global ctxt (long_name ctxt pred_name) val rule_names = hd names |> the o Induct.lookup_inductP ctxt |> fst o Rule_Cases.get |> map (fst o fst) val case_names = map fst avoids val _ = case duplicates (op =) case_names of [] => () | xs => error ("Duplicate case names: " ^ commas_quote xs) val _ = case subtract (op =) rule_names case_names of [] => () | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs) val avoids_ordered = order_default (op =) [] rule_names avoids fun read_avoids avoid_trms intr = let (* fixme hack *) val (((_, inst), _), ctxt') = Variable.import true [intr] ctxt - val trms = build (inst |> Term_Subst.Vars.fold (cons o Thm.term_of o snd)) + val trms = build (inst |> Vars.fold (cons o Thm.term_of o snd)) val ctxt'' = fold Variable.declare_term trms ctxt' in map (Syntax.read_term ctxt'') avoid_trms end val avoid_trms = map2 read_avoids avoids_ordered intrs in prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt end (* outer syntax *) local val single_avoid_parser = Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term) val avoids_parser = Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] val main_parser = Parse.name -- avoids_parser in val _ = Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} "prove strong induction theorem for inductive predicate involving nominal datatypes" (main_parser >> prove_strong_inductive_cmd) end end diff --git a/thys/Refine_Imperative_HOL/Sepref_Rules.thy b/thys/Refine_Imperative_HOL/Sepref_Rules.thy --- a/thys/Refine_Imperative_HOL/Sepref_Rules.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Rules.thy @@ -1,1745 +1,1745 @@ section \Refinement Rule Management\ theory Sepref_Rules imports Sepref_Basic Sepref_Constraints begin text \This theory contains tools for managing the refinement rules used by Sepref\ text \The theories are based on uncurried functions, i.e., every function has type @{typ "'a\'b"}, where @{typ 'a} is the tuple of parameters, or unit if there are none. \ subsection \Assertion Interface Binding\ text \Binding of interface types to refinement assertions\ definition intf_of_assn :: "('a \ _ \ assn) \ 'b itself \ bool" where [simp]: "intf_of_assn a b = True" lemma intf_of_assnI: "intf_of_assn R TYPE('a)" by simp named_theorems_rev intf_of_assn \Links between refinement assertions and interface types\ lemma intf_of_assn_fallback: "intf_of_assn (R :: 'a \ _ \ assn) TYPE('a)" by simp subsection \Function Refinement with Precondition\ definition fref :: "('c \ bool) \ ('a \ 'c) set \ ('b \ 'd) set \ (('a \ 'b) \ ('c \ 'd)) set" ("[_]\<^sub>f _ \ _" [0,60,60] 60) where "[P]\<^sub>f R \ S \ {(f,g). \x y. P y \ (x,y)\R \ (f x, g y)\S}" abbreviation freft ("_ \\<^sub>f _" [60,60] 60) where "R \\<^sub>f S \ ([\_. True]\<^sub>f R \ S)" lemma rel2p_fref[rel2p]: "rel2p (fref P R S) = (\f g. (\x y. P y \ rel2p R x y \ rel2p S (f x) (g y)))" by (auto simp: fref_def rel2p_def[abs_def]) lemma fref_cons: assumes "(f,g) \ [P]\<^sub>f R \ S" assumes "\c a. (c,a)\R' \ Q a \ P a" assumes "R' \ R" assumes "S \ S'" shows "(f,g) \ [Q]\<^sub>f R' \ S'" using assms unfolding fref_def by fastforce lemmas fref_cons' = fref_cons[OF _ _ order_refl order_refl] lemma frefI[intro?]: assumes "\x y. \P y; (x,y)\R\ \ (f x, g y)\S" shows "(f,g)\fref P R S" using assms unfolding fref_def by auto lemma fref_ncI: "(f,g)\R\S \ (f,g)\R\\<^sub>fS" apply (rule frefI) apply parametricity done lemma frefD: assumes "(f,g)\fref P R S" shows "\P y; (x,y)\R\ \ (f x, g y)\S" using assms unfolding fref_def by auto lemma fref_ncD: "(f,g)\R\\<^sub>fS \ (f,g)\R\S" apply (rule fun_relI) apply (drule frefD) apply simp apply assumption+ done lemma fref_compI: "fref P R1 R2 O fref Q S1 S2 \ fref (\x. Q x \ (\y. (y,x)\S1 \ P y)) (R1 O S1) (R2 O S2)" unfolding fref_def apply (auto) apply blast done lemma fref_compI': "\ (f,g)\fref P R1 R2; (g,h)\fref Q S1 S2 \ \ (f,h) \ fref (\x. Q x \ (\y. (y,x)\S1 \ P y)) (R1 O S1) (R2 O S2)" using fref_compI[of P R1 R2 Q S1 S2] by auto lemma fref_unit_conv: "(\_. c, \_. a) \ fref P unit_rel S \ (P () \ (c,a)\S)" by (auto simp: fref_def) lemma fref_uncurry_conv: "(uncurry c, uncurry a) \ fref P (R1\\<^sub>rR2) S \ (\x1 y1 x2 y2. P (y1,y2) \ (x1,y1)\R1 \ (x2,y2)\R2 \ (c x1 x2, a y1 y2) \ S)" by (auto simp: fref_def) lemma fref_mono: "\ \x. P' x \ P x; R' \ R; S \ S' \ \ fref P R S \ fref P' R' S'" unfolding fref_def by auto blast lemma fref_composeI: assumes FR1: "(f,g)\fref P R1 R2" assumes FR2: "(g,h)\fref Q S1 S2" assumes C1: "\x. P' x \ Q x" assumes C2: "\x y. \P' x; (y,x)\S1\ \ P y" assumes R1: "R' \ R1 O S1" assumes R2: "R2 O S2 \ S'" assumes FH: "f'=f" "h'=h" shows "(f',h') \ fref P' R' S'" unfolding FH apply (rule subsetD[OF fref_mono fref_compI'[OF FR1 FR2]]) using C1 C2 apply blast using R1 apply blast using R2 apply blast done lemma fref_triv: "A\Id \ (f,f)\[P]\<^sub>f A \ Id" by (auto simp: fref_def) subsection \Heap-Function Refinement\ text \ The following relates a heap-function with a pure function. It contains a precondition, a refinement assertion for the arguments before and after execution, and a refinement relation for the result. \ (* TODO: We only use this with keep/destroy information, so we could model the parameter relations as such (('a\'ai \ assn) \ bool) *) definition hfref :: " ('a \ bool) \ (('a \ 'ai \ assn) \ ('a \ 'ai \ assn)) \ ('b \ 'bi \ assn) \ (('ai \ 'bi Heap) \ ('a\'b nres)) set" ("[_]\<^sub>a _ \ _" [0,60,60] 60) where "[P]\<^sub>a RS \ T \ { (f,g) . \c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)}" abbreviation hfreft ("_ \\<^sub>a _" [60,60] 60) where "RS \\<^sub>a T \ ([\_. True]\<^sub>a RS \ T)" lemma hfrefI[intro?]: assumes "\c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)" shows "(f,g)\hfref P RS T" using assms unfolding hfref_def by blast lemma hfrefD: assumes "(f,g)\hfref P RS T" shows "\c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)" using assms unfolding hfref_def by blast lemma hfref_to_ASSERT_conv: "NO_MATCH (\_. True) P \ (a,b)\[P]\<^sub>a R \ S \ (a,\x. ASSERT (P x) \ b x) \ R \\<^sub>a S" unfolding hfref_def apply (clarsimp; safe; clarsimp?) apply (rule hn_refine_nofailI) apply (simp add: refine_pw_simps) subgoal for xc xa apply (drule spec[of _ xc]) apply (drule spec[of _ xa]) by simp done text \ A pair of argument refinement assertions can be created by the input assertion and the information whether the parameter is kept or destroyed by the function. \ primrec hf_pres :: "('a \ 'b \ assn) \ bool \ ('a \ 'b \ assn)\('a \ 'b \ assn)" where "hf_pres R True = (R,R)" | "hf_pres R False = (R,invalid_assn R)" abbreviation hfkeep :: "('a \ 'b \ assn) \ ('a \ 'b \ assn)\('a \ 'b \ assn)" ("(_\<^sup>k)" [1000] 999) where "R\<^sup>k \ hf_pres R True" abbreviation hfdrop :: "('a \ 'b \ assn) \ ('a \ 'b \ assn)\('a \ 'b \ assn)" ("(_\<^sup>d)" [1000] 999) where "R\<^sup>d \ hf_pres R False" abbreviation "hn_kede R kd \ hn_ctxt (snd (hf_pres R kd))" abbreviation "hn_keep R \ hn_kede R True" abbreviation "hn_dest R \ hn_kede R False" lemma keep_drop_sels[simp]: "fst (R\<^sup>k) = R" "snd (R\<^sup>k) = R" "fst (R\<^sup>d) = R" "snd (R\<^sup>d) = invalid_assn R" by auto lemma hf_pres_fst[simp]: "fst (hf_pres R k) = R" by (cases k) auto text \ The following operator combines multiple argument assertion-pairs to argument assertion-pairs for the product. It is required to state argument assertion-pairs for uncurried functions. \ definition hfprod :: " (('a \ 'b \ assn)\('a \ 'b \ assn)) \ (('c \ 'd \ assn)\('c \ 'd \ assn)) \ ((('a\'c) \ ('b \ 'd) \ assn) \ (('a\'c) \ ('b \ 'd) \ assn))" (infixl "*\<^sub>a" 65) where "RR *\<^sub>a SS \ (prod_assn (fst RR) (fst SS), prod_assn (snd RR) (snd SS))" lemma hfprod_fst_snd[simp]: "fst (A *\<^sub>a B) = prod_assn (fst A) (fst B)" "snd (A *\<^sub>a B) = prod_assn (snd A) (snd B)" unfolding hfprod_def by auto subsubsection \Conversion from fref to hfref\ (* TODO: Variant of import-param! Automate this! *) lemma fref_to_pure_hfref': assumes "(f,g) \ [P]\<^sub>f R\\S\nres_rel" assumes "\x. x\Domain R \ R\``Collect P \ f x = RETURN (f' x)" shows "(return o f', g) \ [P]\<^sub>a (pure R)\<^sup>k\pure S" apply (rule hfrefI) apply (rule hn_refineI) using assms apply ((sep_auto simp: fref_def pure_def pw_le_iff pw_nres_rel_iff refine_pw_simps eintros del: exI)) apply force done subsubsection \Conversion from hfref to hnr\ text \This section contains the lemmas. The ML code is further down. \ lemma hf2hnr: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "\x xi. P x \ hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" using assms unfolding hfref_def by (auto simp: hn_ctxt_def) (*lemma hf2hnr_new: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "\x xi. (\h. h\fst R x xi \ P x) \ hn_refine (emp * hn_ctxt (fst R) x xi) (f xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" using assms unfolding hfref_def by (auto simp: hn_ctxt_def intro: hn_refine_preI) *) (* Products that stem from currying are tagged by a special refinement relation *) definition [simp]: "to_hnr_prod \ prod_assn" lemma to_hnr_prod_fst_snd: "fst (A *\<^sub>a B) = to_hnr_prod (fst A) (fst B)" "snd (A *\<^sub>a B) = to_hnr_prod (snd A) (snd B)" unfolding hfprod_def by auto (* Warning: This lemma is carefully set up to be applicable as an unfold rule, for more than one level of uncurrying*) lemma hnr_uncurry_unfold: " (\x xi. P x \ hn_refine (\ * hn_ctxt (to_hnr_prod A B) x xi) (fi xi) (\' * hn_ctxt (to_hnr_prod A' B') x xi) R (f x)) \ (\b bi a ai. P (a,b) \ hn_refine (\ * hn_ctxt B b bi * hn_ctxt A a ai) (fi (ai,bi)) (\' * hn_ctxt B' b bi * hn_ctxt A' a ai) R (f (a,b)) )" by (auto simp: hn_ctxt_def prod_assn_def star_aci) lemma hnr_intro_dummy: "\x xi. P x \ hn_refine (\ x xi) (c xi) (\' x xi) R (a x) \ \x xi. P x \ hn_refine (emp*\ x xi) (c xi) (emp*\' x xi) R (a x)" by simp lemma hn_ctxt_ctxt_fix_conv: "hn_ctxt (hn_ctxt R) = hn_ctxt R" by (simp add: hn_ctxt_def[abs_def]) lemma uncurry_APP: "uncurry f$(a,b) = f$a$b" by auto (* TODO: Replace by more general rule. *) lemma norm_RETURN_o: "\f. (RETURN o f)$x = (RETURN$(f$x))" "\f. (RETURN oo f)$x$y = (RETURN$(f$x$y))" "\f. (RETURN ooo f)$x$y$z = (RETURN$(f$x$y$z))" "\f. (\x. RETURN ooo f x)$x$y$z$a = (RETURN$(f$x$y$z$a))" "\f. (\x y. RETURN ooo f x y)$x$y$z$a$b = (RETURN$(f$x$y$z$a$b))" by auto lemma norm_return_o: "\f. (return o f)$x = (return$(f$x))" "\f. (return oo f)$x$y = (return$(f$x$y))" "\f. (return ooo f)$x$y$z = (return$(f$x$y$z))" "\f. (\x. return ooo f x)$x$y$z$a = (return$(f$x$y$z$a))" "\f. (\x y. return ooo f x y)$x$y$z$a$b = (return$(f$x$y$z$a$b))" by auto lemma hn_val_unit_conv_emp[simp]: "hn_val unit_rel x y = emp" by (auto simp: hn_ctxt_def pure_def) subsubsection \Conversion from hnr to hfref\ text \This section contains the lemmas. The ML code is further down. \ abbreviation "id_assn \ pure Id" abbreviation "unit_assn \ id_assn :: unit \ _" lemma pure_unit_rel_eq_empty: "unit_assn x y = emp" by (auto simp: pure_def) lemma uc_hfprod_sel: "fst (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \ fst A a1 c1 * fst B a2 c2)" "snd (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \ snd A a1 c1 * snd B a2 c2)" unfolding hfprod_def prod_assn_def[abs_def] by auto subsubsection \Conversion from relation to fref\ text \This section contains the lemmas. The ML code is further down. \ definition "CURRY R \ { (f,g). (uncurry f, uncurry g) \ R }" lemma fref_param1: "R\S = fref (\_. True) R S" by (auto simp: fref_def fun_relD) lemma fref_nest: "fref P1 R1 (fref P2 R2 S) \ CURRY (fref (\(a,b). P1 a \ P2 b) (R1\\<^sub>rR2) S)" apply (rule eq_reflection) by (auto simp: fref_def CURRY_def) lemma in_CURRY_conv: "(f,g) \ CURRY R \ (uncurry f, uncurry g) \ R" unfolding CURRY_def by auto lemma uncurry0_APP[simp]: "uncurry0 c $ x = c" by auto lemma fref_param0I: "(c,a)\R \ (uncurry0 c, uncurry0 a) \ fref (\_. True) unit_rel R" by (auto simp: fref_def) subsubsection \Composition\ definition hr_comp :: "('b \ 'c \ assn) \ ('b \ 'a) set \ 'a \ 'c \ assn" \ \Compose refinement assertion with refinement relation\ where "hr_comp R1 R2 a c \ \\<^sub>Ab. R1 b c * \((b,a)\R2)" definition hrp_comp :: "('d \ 'b \ assn) \ ('d \ 'c \ assn) \ ('d \ 'a) set \ ('a \ 'b \ assn) \ ('a \ 'c \ assn)" \ \Compose argument assertion-pair with refinement relation\ where "hrp_comp RR' S \ (hr_comp (fst RR') S, hr_comp (snd RR') S) " lemma hr_compI: "(b,a)\R2 \ R1 b c \\<^sub>A hr_comp R1 R2 a c" unfolding hr_comp_def by sep_auto lemma hr_comp_Id1[simp]: "hr_comp (pure Id) R = pure R" unfolding hr_comp_def[abs_def] pure_def apply (intro ext ent_iffI) by sep_auto+ lemma hr_comp_Id2[simp]: "hr_comp R Id = R" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) by sep_auto+ (*lemma hr_comp_invalid[simp]: "hr_comp (\a c. true) R a c = true * \(\b. (b,a)\R)" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) apply sep_auto+ done*) lemma hr_comp_emp[simp]: "hr_comp (\a c. emp) R a c = \(\b. (b,a)\R)" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) apply sep_auto+ done lemma hr_comp_prod_conv[simp]: "hr_comp (prod_assn Ra Rb) (Ra' \\<^sub>r Rb') = prod_assn (hr_comp Ra Ra') (hr_comp Rb Rb')" unfolding hr_comp_def[abs_def] prod_assn_def[abs_def] apply (intro ext ent_iffI) apply solve_entails apply clarsimp apply sep_auto apply clarsimp apply (intro ent_ex_preI) apply (rule ent_ex_postI) apply (sep_auto split: prod.splits) done lemma hr_comp_pure: "hr_comp (pure R) S = pure (R O S)" apply (intro ext) apply (rule ent_iffI) unfolding hr_comp_def[abs_def] apply (sep_auto simp: pure_def)+ done lemma hr_comp_is_pure[safe_constraint_rules]: "is_pure A \ is_pure (hr_comp A B)" by (auto simp: hr_comp_pure is_pure_conv) lemma hr_comp_the_pure: "is_pure A \ the_pure (hr_comp A B) = the_pure A O B" unfolding is_pure_conv by (clarsimp simp: hr_comp_pure) lemma rdomp_hrcomp_conv: "rdomp (hr_comp A R) x \ (\y. rdomp A y \ (y,x)\R)" by (auto simp: rdomp_def hr_comp_def) lemma hn_rel_compI: "\nofail a; (b,a)\\R2\nres_rel\ \ hn_rel R1 b c \\<^sub>A hn_rel (hr_comp R1 R2) a c" unfolding hr_comp_def hn_rel_def nres_rel_def apply (clarsimp intro!: ent_ex_preI) apply (drule (1) order_trans) apply (simp add: ret_le_down_conv) by sep_auto lemma hr_comp_precise[constraint_rules]: assumes [safe_constraint_rules]: "precise R" assumes SV: "single_valued S" shows "precise (hr_comp R S)" apply (rule preciseI) unfolding hr_comp_def apply clarsimp by (metis SV assms(1) preciseD single_valuedD) lemma hr_comp_assoc: "hr_comp (hr_comp R S) T = hr_comp R (S O T)" apply (intro ext) unfolding hr_comp_def apply (rule ent_iffI; clarsimp) apply sep_auto apply (rule ent_ex_preI; clarsimp) (* TODO: sep_auto/solve_entails is too eager splitting the subgoal here! *) apply sep_auto done lemma hnr_comp: assumes R: "\b1 c1. P b1 \ hn_refine (R1 b1 c1 * \) (c c1) (R1p b1 c1 * \') R (b b1)" assumes S: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ (b b1,a a1)\\R'\nres_rel" assumes PQ: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ P b1" assumes Q: "Q a1" shows "hn_refine (hr_comp R1 R1' a1 c1 * \) (c c1) (hr_comp R1p R1' a1 c1 * \') (hr_comp R R') (a a1)" unfolding hn_refine_alt proof clarsimp assume NF: "nofail (a a1)" show " > c c1 <\r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \')>\<^sub>t" apply (subst hr_comp_def) apply (clarsimp intro!: norm_pre_ex_rule) proof - fix b1 assume R1: "(b1, a1) \ R1'" from S R1 Q have R': "(b b1, a a1) \ \R'\nres_rel" by blast with NF have NFB: "nofail (b b1)" by (simp add: nres_rel_def pw_le_iff refine_pw_simps) from PQ R1 Q have P: "P b1" by blast with NFB R have "> c c1 <\r. hn_rel R (b b1) r * (R1p b1 c1 * \')>\<^sub>t" unfolding hn_refine_alt by auto thus "> c c1 <\r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \')>\<^sub>t" apply (rule cons_post_rule) apply (solve_entails) by (intro ent_star_mono hn_rel_compI[OF NF R'] hr_compI[OF R1] ent_refl) qed qed lemma hnr_comp1_aux: assumes R: "\b1 c1. P b1 \ hn_refine (hn_ctxt R1 b1 c1) (c c1) (hn_ctxt R1p b1 c1) R (b$b1)" assumes S: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ (b$b1,a$a1)\\R'\nres_rel" assumes PQ: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ P b1" assumes Q: "Q a1" shows "hn_refine (hr_comp R1 R1' a1 c1) (c c1) (hr_comp R1p R1' a1 c1) (hr_comp R R') (a a1)" using assms hnr_comp[where \=emp and \'=emp and a=a and b=b and c=c and P=P and Q=Q] unfolding hn_ctxt_def by auto lemma hfcomp: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [\a. Q a \ (\a'. (a',a)\T \ P a')]\<^sub>a hrp_comp RR' T \ hr_comp S U" using assms unfolding fref_def hfref_def hrp_comp_def apply clarsimp apply (rule hnr_comp1_aux[of P "fst RR'" f "snd RR'" S g "\a. Q a \ (\a'. (a',a)\T \ P a')" T h U]) apply (auto simp: hn_ctxt_def) done lemma hfref_weaken_pre_nofail: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "(f,g) \ [\x. nofail (g x) \ P x]\<^sub>a R \ S" using assms unfolding hfref_def hn_refine_def by auto lemma hfref_cons: assumes "(f,g) \ [P]\<^sub>a R \ S" assumes "\x. P' x \ P x" assumes "\x y. fst R' x y \\<^sub>t fst R x y" assumes "\x y. snd R x y \\<^sub>t snd R' x y" assumes "\x y. S x y \\<^sub>t S' x y" shows "(f,g) \ [P']\<^sub>a R' \ S'" unfolding hfref_def apply clarsimp apply (rule hn_refine_cons) apply (rule assms(3)) defer apply (rule entt_trans[OF assms(4)]; sep_auto) apply (rule assms(5)) apply (frule assms(2)) using assms(1) unfolding hfref_def apply auto done subsubsection \Composition Automation\ text \This section contains the lemmas. The ML code is further down. \ lemma prod_hrp_comp: "hrp_comp (A *\<^sub>a B) (C \\<^sub>r D) = hrp_comp A C *\<^sub>a hrp_comp B D" unfolding hrp_comp_def hfprod_def by simp lemma hrp_comp_keep: "hrp_comp (A\<^sup>k) B = (hr_comp A B)\<^sup>k" by (auto simp: hrp_comp_def) lemma hr_comp_invalid: "hr_comp (invalid_assn R1) R2 = invalid_assn (hr_comp R1 R2)" apply (intro ent_iffI entailsI ext) unfolding invalid_assn_def hr_comp_def by auto lemma hrp_comp_dest: "hrp_comp (A\<^sup>d) B = (hr_comp A B)\<^sup>d" by (auto simp: hrp_comp_def hr_comp_invalid) definition "hrp_imp RR RR' \ \a b. (fst RR' a b \\<^sub>t fst RR a b) \ (snd RR a b \\<^sub>t snd RR' a b)" lemma hfref_imp: "hrp_imp RR RR' \ [P]\<^sub>a RR \ S \ [P]\<^sub>a RR' \ S" apply clarsimp apply (erule hfref_cons) apply (simp_all add: hrp_imp_def) done lemma hrp_imp_refl: "hrp_imp RR RR" unfolding hrp_imp_def by auto lemma hrp_imp_reflI: "RR = RR' \ hrp_imp RR RR'" unfolding hrp_imp_def by auto lemma hrp_comp_cong: "hrp_imp A A' \ B=B' \ hrp_imp (hrp_comp A B) (hrp_comp A' B')" by (sep_auto simp: hrp_imp_def hrp_comp_def hr_comp_def entailst_def) lemma hrp_prod_cong: "hrp_imp A A' \ hrp_imp B B' \ hrp_imp (A*\<^sub>aB) (A'*\<^sub>aB')" by (sep_auto simp: hrp_imp_def prod_assn_def intro: entt_star_mono) lemma hrp_imp_trans: "hrp_imp A B \ hrp_imp B C \ hrp_imp A C" unfolding hrp_imp_def by (fastforce intro: entt_trans) lemma fcomp_norm_dflt_init: "x\[P]\<^sub>a R \ T \ hrp_imp R S \ x\[P]\<^sub>a S \ T" apply (erule rev_subsetD) by (rule hfref_imp) definition "comp_PRE R P Q S \ \x. S x \ (P x \ (\y. (y,x)\R \ Q x y))" lemma comp_PRE_cong[cong]: assumes "R\R'" assumes "\x. P x \ P' x" assumes "\x. S x \ S' x" assumes "\x y. \P x; (y,x)\R; y\Domain R; S' x \ \ Q x y \ Q' x y" shows "comp_PRE R P Q S \ comp_PRE R' P' Q' S'" using assms by (fastforce simp: comp_PRE_def intro!: eq_reflection ext) lemma fref_compI_PRE: "\ (f,g)\fref P R1 R2; (g,h)\fref Q S1 S2 \ \ (f,h) \ fref (comp_PRE S1 Q (\_. P) (\_. True)) (R1 O S1) (R2 O S2)" using fref_compI[of P R1 R2 Q S1 S2] unfolding comp_PRE_def by auto lemma PRE_D1: "(Q x \ P x) \ comp_PRE S1 Q (\x _. P x) S x" by (auto simp: comp_PRE_def) lemma PRE_D2: "(Q x \ (\y. (y,x)\S1 \ S x \ P x y)) \ comp_PRE S1 Q P S x" by (auto simp: comp_PRE_def) lemma fref_weaken_pre: assumes "\x. P x \ P' x" assumes "(f,h) \ fref P' R S" shows "(f,h) \ fref P R S" apply (rule rev_subsetD[OF assms(2) fref_mono]) using assms(1) by auto lemma fref_PRE_D1: assumes "(f,h) \ fref (comp_PRE S1 Q (\x _. P x) X) R S" shows "(f,h) \ fref (\x. Q x \ P x) R S" by (rule fref_weaken_pre[OF PRE_D1 assms]) lemma fref_PRE_D2: assumes "(f,h) \ fref (comp_PRE S1 Q P X) R S" shows "(f,h) \ fref (\x. Q x \ (\y. (y,x)\S1 \ X x \ P x y)) R S" by (rule fref_weaken_pre[OF PRE_D2 assms]) lemmas fref_PRE_D = fref_PRE_D1 fref_PRE_D2 lemma hfref_weaken_pre: assumes "\x. P x \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" using assms by (auto simp: hfref_def) lemma hfref_weaken_pre': assumes "\x. \P x; rdomp (fst R) x\ \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" apply (rule hfrefI) apply (rule hn_refine_preI) using assms by (auto simp: hfref_def rdomp_def) lemma hfref_weaken_pre_nofail': assumes "(f,g) \ [P]\<^sub>a R \ S" assumes "\x. \nofail (g x); Q x\ \ P x" shows "(f,g) \ [Q]\<^sub>a R \ S" apply (rule hfref_weaken_pre[OF _ assms(1)[THEN hfref_weaken_pre_nofail]]) using assms(2) by blast lemma hfref_compI_PRE_aux: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [comp_PRE T Q (\_. P) (\_. True)]\<^sub>a hrp_comp RR' T \ hr_comp S U" apply (rule hfref_weaken_pre[OF _ hfcomp[OF A B]]) by (auto simp: comp_PRE_def) lemma hfref_compI_PRE: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [comp_PRE T Q (\x y. P y) (\x. nofail (h x))]\<^sub>a hrp_comp RR' T \ hr_comp S U" using hfref_compI_PRE_aux[OF A B, THEN hfref_weaken_pre_nofail] apply (rule hfref_weaken_pre[rotated]) apply (auto simp: comp_PRE_def) done lemma hfref_PRE_D1: assumes "(f,h) \ hfref (comp_PRE S1 Q (\x _. P x) X) R S" shows "(f,h) \ hfref (\x. Q x \ P x) R S" by (rule hfref_weaken_pre[OF PRE_D1 assms]) lemma hfref_PRE_D2: assumes "(f,h) \ hfref (comp_PRE S1 Q P X) R S" shows "(f,h) \ hfref (\x. Q x \ (\y. (y,x)\S1 \ X x \ P x y)) R S" by (rule hfref_weaken_pre[OF PRE_D2 assms]) lemma hfref_PRE_D3: assumes "(f,h) \ hfref (comp_PRE S1 Q P X) R S" shows "(f,h) \ hfref (comp_PRE S1 Q P X) R S" using assms . lemmas hfref_PRE_D = hfref_PRE_D1 hfref_PRE_D3 subsection \Automation\ text \Purity configuration for constraint solver\ lemmas [safe_constraint_rules] = pure_pure text \Configuration for hfref to hnr conversion\ named_theorems to_hnr_post \to_hnr converter: Postprocessing unfold rules\ lemma uncurry0_add_app_tag: "uncurry0 (RETURN c) = uncurry0 (RETURN$c)" by simp lemmas [to_hnr_post] = norm_RETURN_o norm_return_o uncurry0_add_app_tag uncurry0_apply uncurry0_APP hn_val_unit_conv_emp mult_1[of "x::assn" for x] mult_1_right[of "x::assn" for x] named_theorems to_hfref_post \to_hfref converter: Postprocessing unfold rules\ lemma prod_casesK[to_hfref_post]: "case_prod (\_ _. k) = (\_. k)" by auto lemma uncurry0_hfref_post[to_hfref_post]: "hfref (uncurry0 True) R S = hfref (\_. True) R S" apply (fo_rule arg_cong fun_cong)+ by auto (* Currently not used, we keep it in here anyway. *) text \Configuration for relation normalization after composition\ named_theorems fcomp_norm_unfold \fcomp-normalizer: Unfold theorems\ named_theorems fcomp_norm_simps \fcomp-normalizer: Simplification theorems\ named_theorems fcomp_norm_init "fcomp-normalizer: Initialization rules" named_theorems fcomp_norm_trans "fcomp-normalizer: Transitivity rules" named_theorems fcomp_norm_cong "fcomp-normalizer: Congruence rules" named_theorems fcomp_norm_norm "fcomp-normalizer: Normalization rules" named_theorems fcomp_norm_refl "fcomp-normalizer: Reflexivity rules" text \Default Setup\ lemmas [fcomp_norm_unfold] = prod_rel_comp nres_rel_comp Id_O_R R_O_Id lemmas [fcomp_norm_unfold] = hr_comp_Id1 hr_comp_Id2 lemmas [fcomp_norm_unfold] = hr_comp_prod_conv lemmas [fcomp_norm_unfold] = prod_hrp_comp hrp_comp_keep hrp_comp_dest hr_comp_pure (*lemmas [fcomp_norm_unfold] = prod_casesK uncurry0_hfref_post*) lemma [fcomp_norm_simps]: "CONSTRAINT is_pure P \ pure (the_pure P) = P" by simp lemmas [fcomp_norm_simps] = True_implies_equals lemmas [fcomp_norm_init] = fcomp_norm_dflt_init lemmas [fcomp_norm_trans] = hrp_imp_trans lemmas [fcomp_norm_cong] = hrp_comp_cong hrp_prod_cong (*lemmas [fcomp_norm_norm] = hrp_comp_dest*) lemmas [fcomp_norm_refl] = refl hrp_imp_refl lemma ensure_fref_nresI: "(f,g)\[P]\<^sub>f R\S \ (RETURN o f, RETURN o g)\[P]\<^sub>f R\\S\nres_rel" by (auto intro: nres_relI simp: fref_def) lemma ensure_fref_nres_unfold: "\f. RETURN o (uncurry0 f) = uncurry0 (RETURN f)" "\f. RETURN o (uncurry f) = uncurry (RETURN oo f)" "\f. (RETURN ooo uncurry) f = uncurry (RETURN ooo f)" by auto text \Composed precondition normalizer\ named_theorems fcomp_prenorm_simps \fcomp precondition-normalizer: Simplification theorems\ text \Support for preconditions of the form \_\Domain R\, where \R\ is the relation of the next more abstract level.\ declare DomainI[fcomp_prenorm_simps] lemma auto_weaken_pre_init_hf: assumes "\x. PROTECT P x \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" using assms by (auto simp: hfref_def) lemma auto_weaken_pre_init_f: assumes "\x. PROTECT P x \ P' x" assumes "(f,h) \ fref P' R S" shows "(f,h) \ fref P R S" using assms by (auto simp: fref_def) lemmas auto_weaken_pre_init = auto_weaken_pre_init_hf auto_weaken_pre_init_f lemma auto_weaken_pre_uncurry_step: assumes "PROTECT f a \ f'" shows "PROTECT (\(x,y). f x y) (a,b) \ f' b" using assms by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection) lemma auto_weaken_pre_uncurry_finish: "PROTECT f x \ f x" by (auto) lemma auto_weaken_pre_uncurry_start: assumes "P \ P'" assumes "P'\Q" shows "P\Q" using assms by (auto) lemma auto_weaken_pre_comp_PRE_I: assumes "S x \ P x" assumes "\y. \(y,x)\R; P x; S x\ \ Q x y" shows "comp_PRE R P Q S x" using assms by (auto simp: comp_PRE_def) lemma auto_weaken_pre_to_imp_nf: "(A\B\C) = (A\B \ C)" "((A\B)\C) = (A\B\C)" by auto lemma auto_weaken_pre_add_dummy_imp: "P \ True \ P" by simp text \Synthesis for hfref statements\ definition hfsynth_ID_R :: "('a \ _ \ assn) \ 'a \ bool" where [simp]: "hfsynth_ID_R _ _ \ True" lemma hfsynth_ID_R_D: fixes I :: "'a itself" assumes "hfsynth_ID_R R a" assumes "intf_of_assn R I" shows "a ::\<^sub>i I" by simp lemma hfsynth_hnr_from_hfI: assumes "\x xi. P x \ hfsynth_ID_R (fst R) x \ hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" shows "(f,g) \ [P]\<^sub>a R \ S" using assms unfolding hfref_def by (auto simp: hn_ctxt_def) lemma hfsynth_ID_R_uncurry_unfold: "hfsynth_ID_R (to_hnr_prod R S) (a,b) \ hfsynth_ID_R R a \ hfsynth_ID_R S b" "hfsynth_ID_R (fst (hf_pres R k)) \ hfsynth_ID_R R" by (auto intro!: eq_reflection) ML \ signature SEPREF_RULES = sig (* Analysis of relations, both fref and fun_rel *) (* "R1\...\Rn\_" / "[_]\<^sub>f ((R1\\<^sub>rR2)...\\<^sub>rRn)" \ "[R1,...,Rn]" *) val binder_rels: term -> term list (* "_\...\_\S" / "[_]\<^sub>f _ \ S" \ "S" *) val body_rel: term -> term (* Map \/fref to (precond,args,res). NONE if no/trivial precond. *) val analyze_rel: term -> term option * term list * term (* Make trivial ("\_. True") precond *) val mk_triv_precond: term list -> term (* Make "[P]\<^sub>f ((R1\\<^sub>rR2)...\\<^sub>rRn) \ S". Insert trivial precond if NONE. *) val mk_rel: term option * term list * term -> term (* Map relation to (args,res) *) val strip_rel: term -> term list * term (* Make hfprod (op *\<^sub>a) *) val mk_hfprod : term * term -> term val mk_hfprods : term list -> term (* Determine interface type of refinement assertion, using default fallback if necessary. Use named_thms intf_of_assn for configuration. *) val intf_of_assn : Proof.context -> term -> typ (* Convert a parametricity theorem in higher-order form to uncurried fref-form. For functions without arguments, a unit-argument is added. TODO/FIXME: Currently this only works for higher-order theorems, i.e., theorems of the form (f,g)\R1\\\Rn. First-order theorems are silently treated as refinement theorems for functions with zero arguments, i.e., a unit-argument is added. *) val to_fref : Proof.context -> thm -> thm (* Convert a parametricity or fref theorem to first order form *) val to_foparam : Proof.context -> thm -> thm (* Convert schematic hfref goal to hnr-goal *) val prepare_hfref_synth_tac : Proof.context -> tactic' (* Convert theorem in hfref-form to hnr-form *) val to_hnr : Proof.context -> thm -> thm (* Convert theorem in hnr-form to hfref-form *) val to_hfref: Proof.context -> thm -> thm (* Convert theorem to given form, if not yet in this form *) val ensure_fref : Proof.context -> thm -> thm val ensure_fref_nres : Proof.context -> thm -> thm val ensure_hfref : Proof.context -> thm -> thm val ensure_hnr : Proof.context -> thm -> thm type hnr_analysis = { thm: thm, (* Original theorem, may be normalized *) precond: term, (* Precondition, abstracted over abs-arguments *) prems : term list, (* Premises not depending on arguments *) ahead: term * bool, (* Abstract function, has leading RETURN *) chead: term * bool, (* Concrete function, has leading return *) argrels: (term * bool) list, (* Argument relations, preserved (keep-flag) *) result_rel: term (* Result relation *) } val analyze_hnr: Proof.context -> thm -> hnr_analysis val pretty_hnr_analysis: Proof.context -> hnr_analysis -> Pretty.T val mk_hfref_thm: Proof.context -> hnr_analysis -> thm (* Simplify precondition of fref/hfref-theorem *) val simplify_precond: Proof.context -> thm -> thm (* Normalize hfref-theorem after composition *) val norm_fcomp_rule: Proof.context -> thm -> thm (* Replace "pure ?A" by "?A'" and is_pure constraint, then normalize *) val add_pure_constraints_rule: Proof.context -> thm -> thm (* Compose fref/hfref and fref theorem, to produce hfref theorem. The input theorems may also be in ho-param or hnr form, and are converted accordingly. *) val gen_compose : Proof.context -> thm -> thm -> thm (* FCOMP-attribute *) val fcomp_attrib: attribute context_parser end structure Sepref_Rules: SEPREF_RULES = struct local open Refine_Util Relators in fun binder_rels @{mpat "?F \ ?G"} = F::binder_rels G | binder_rels @{mpat "fref _ ?F _"} = strip_prodrel_left F | binder_rels _ = [] local fun br_aux @{mpat "_ \ ?G"} = br_aux G | br_aux R = R in fun body_rel @{mpat "fref _ _ ?G"} = G | body_rel R = br_aux R end fun strip_rel R = (binder_rels R, body_rel R) fun analyze_rel @{mpat "fref (\_. True) ?R ?S"} = (NONE,strip_prodrel_left R,S) | analyze_rel @{mpat "fref ?P ?R ?S"} = (SOME P,strip_prodrel_left R,S) | analyze_rel R = let val (args,res) = strip_rel R in (NONE,args,res) end fun mk_triv_precond Rs = absdummy (map rel_absT Rs |> list_prodT_left) @{term True} fun mk_rel (P,Rs,S) = let val R = list_prodrel_left Rs val P = case P of SOME P => P | NONE => mk_triv_precond Rs in @{mk_term "fref ?P ?R ?S"} end end fun mk_hfprod (a, b) = @{mk_term "?a*\<^sub>a?b"} local fun mk_hfprods_rev [] = @{mk_term "unit_assn\<^sup>k"} | mk_hfprods_rev [Rk] = Rk | mk_hfprods_rev (Rkn::Rks) = mk_hfprod (mk_hfprods_rev Rks, Rkn) in val mk_hfprods = mk_hfprods_rev o rev end fun intf_of_assn ctxt t = let val orig_ctxt = ctxt val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt val v = TVar (("T",0),Proof_Context.default_sort ctxt ("T",0)) |> Logic.mk_type val goal = @{mk_term "Trueprop (intf_of_assn ?t ?v)"} val i_of_assn_rls = Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn} @ @{thms intf_of_assn_fallback} fun tac ctxt = REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls) val thm = Goal.prove ctxt [] [] goal (fn {context,...} => ALLGOALS (tac context)) val intf = case Thm.concl_of thm of @{mpat "Trueprop (intf_of_assn _ (?v AS\<^sub>p TYPE (_)))"} => v | _ => raise THM("Intf_of_assn: Proved a different theorem?",~1,[thm]) val intf = singleton (Variable.export_terms ctxt orig_ctxt) intf |> Logic.dest_type in intf end datatype rthm_type = RT_HOPARAM (* (_,_) \ _ \ \ \ _ *) | RT_FREF (* (_,_) \ [_]\<^sub>f _ \ _ *) | RT_HNR (* hn_refine _ _ _ _ _ *) | RT_HFREF (* (_,_) \ [_]\<^sub>a _ \ _ *) | RT_OTHER fun rthm_type thm = case Thm.concl_of thm |> HOLogic.dest_Trueprop of @{mpat "(_,_) \ fref _ _ _"} => RT_FREF | @{mpat "(_,_) \ hfref _ _ _"} => RT_HFREF | @{mpat "hn_refine _ _ _ _ _"} => RT_HNR | @{mpat "(_,_) \ _"} => RT_HOPARAM (* TODO: Distinction between ho-param and fo-param *) | _ => RT_OTHER fun to_fref ctxt thm = let open Conv in case Thm.concl_of thm |> HOLogic.dest_Trueprop of @{mpat "(_,_)\_\_"} => Local_Defs.unfold0 ctxt @{thms fref_param1} thm |> fconv_rule (repeat_conv (Refine_Util.ftop_conv (K (rewr_conv @{thm fref_nest})) ctxt)) |> Local_Defs.unfold0 ctxt @{thms in_CURRY_conv} | @{mpat "(_,_)\_"} => thm RS @{thm fref_param0I} | _ => raise THM ("to_fref: Expected theorem of form (_,_)\_",~1,[thm]) end fun to_foparam ctxt thm = let val unf_thms = @{thms split_tupled_all prod_rel_simp uncurry_apply cnv_conj_to_meta Product_Type.split} in case Thm.concl_of thm of @{mpat "Trueprop ((_,_) \ fref _ _ _)"} => (@{thm frefD} OF [thm]) |> Thm.forall_intr_vars |> Local_Defs.unfold0 ctxt unf_thms |> Variable.gen_all ctxt | @{mpat "Trueprop ((_,_) \ _)"} => Parametricity.fo_rule thm | _ => raise THM("Expected parametricity or fref theorem",~1,[thm]) end fun to_hnr ctxt thm = (thm RS @{thm hf2hnr}) |> Local_Defs.unfold0 ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels} (* Resolve fst and snd over *\<^sub>a and R\<^sup>k, R\<^sup>d *) |> Local_Defs.unfold0 ctxt @{thms hnr_uncurry_unfold} (* Resolve products for uncurried parameters *) |> Local_Defs.unfold0 ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Remove the uncurry modifiers, the emp-dummy, and unfold product cases *) |> Local_Defs.unfold0 ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt tagging *) |> Local_Defs.unfold0 ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert to meta-level, remove vacuous condition *) |> Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hnr_post}) (* Post-Processing *) |> Goal.norm_result ctxt |> Conv.fconv_rule Thm.eta_conversion (* Convert schematic hfref-goal to hn_refine goal *) fun prepare_hfref_synth_tac ctxt = let val i_of_assn_rls = Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn} @ @{thms intf_of_assn_fallback} val to_hnr_post_rls = Named_Theorems.get ctxt @{named_theorems to_hnr_post} val i_of_assn_tac = ( REPEAT' ( DETERM o dresolve_tac ctxt @{thms hfsynth_ID_R_D} THEN' DETERM o SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls)) ) ) in (* Note: To re-use the to_hnr infrastructure, we first work with $-tags on the abstract function, which are finally removed. *) resolve_tac ctxt @{thms hfsynth_hnr_from_hfI} THEN_ELSE' ( SELECT_GOAL ( unfold_tac ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst} (* Distribute fst,snd over product and hf_pres *) THEN unfold_tac ctxt @{thms hnr_uncurry_unfold hfsynth_ID_R_uncurry_unfold} (* Curry parameters *) THEN unfold_tac ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Curry parameters (II) and remove emp assertion *) (*THEN unfold_tac ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt (Should not be necessary) *)*) THEN unfold_tac ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert precondition to meta-level *) THEN ALLGOALS i_of_assn_tac (* Generate _::\<^sub>i_ premises*) THEN unfold_tac ctxt to_hnr_post_rls (* Postprocessing *) THEN unfold_tac ctxt @{thms APP_def} (* Get rid of $ - tags *) ) , K all_tac ) end (************************************) (* Analyze hnr *) structure Termtab2 = Table( type key = term * term val ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord); type hnr_analysis = { thm: thm, precond: term, prems : term list, ahead: term * bool, chead: term * bool, argrels: (term * bool) list, result_rel: term } fun analyze_hnr (ctxt:Proof.context) thm = let (* Debug information: Stores string*term pairs, which are pretty-printed on error *) val dbg = Unsynchronized.ref [] fun add_dbg msg ts = ( dbg := (msg,ts) :: !dbg; () ) fun pretty_dbg (msg,ts) = Pretty.block [ Pretty.str msg, Pretty.str ":", Pretty.brk 1, Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) ts) ] fun pretty_dbgs l = map pretty_dbg l |> Pretty.fbreaks |> Pretty.block fun trace_dbg msg = Pretty.block [Pretty.str msg, Pretty.fbrk, pretty_dbgs (rev (!dbg))] |> Pretty.string_of |> tracing fun fail msg = (trace_dbg msg; raise THM(msg,~1,[thm])) fun assert cond msg = cond orelse fail msg; (* Heads may have a leading return/RETURN. The following code strips off the leading return, unless it has the form "return x" for an argument x *) fun check_strip_leading args t f = (* Handle the case RETURN x, where x is an argument *) if Termtab.defined args f then (t,false) else (f,true) fun strip_leading_RETURN args (t as @{mpat "RETURN$(?f)"}) = check_strip_leading args t f | strip_leading_RETURN args (t as @{mpat "RETURN ?f"}) = check_strip_leading args t f | strip_leading_RETURN _ t = (t,false) fun strip_leading_return args (t as @{mpat "return$(?f)"}) = check_strip_leading args t f | strip_leading_return args (t as @{mpat "return ?f"}) = check_strip_leading args t f | strip_leading_return _ t = (t,false) (* The following code strips the arguments of the concrete or abstract function. It knows how to handle APP-tags ($), and stops at PR_CONST-tags. Moreover, it only strips actual arguments that occur in the precondition-section of the hn_refine-statement. This ensures that non-arguments, like maxsize, are treated correctly. *) fun strip_fun _ (t as @{mpat "PR_CONST _"}) = (t,[]) | strip_fun s (t as @{mpat "?f$?x"}) = check_arg s t f x | strip_fun s (t as @{mpat "?f ?x"}) = check_arg s t f x | strip_fun _ f = (f,[]) and check_arg s t f x = if Termtab.defined s x then strip_fun s f |> apsnd (curry op :: x) else (t,[]) (* Arguments in the pre/postcondition are wrapped into hn_ctxt tags. This function strips them off. *) fun dest_hn_ctxt @{mpat "hn_ctxt ?R ?a ?c"} = ((a,c),R) | dest_hn_ctxt _ = fail "Invalid hn_ctxt parameter in pre or postcondition" fun dest_hn_refine @{mpat "(hn_refine ?G ?c ?G' ?R ?a)"} = (G,c,G',R,a) | dest_hn_refine _ = fail "Conclusion is not a hn_refine statement" (* Strip separation conjunctions. Special case for "emp", which is ignored. *) fun is_emp @{mpat emp} = true | is_emp _ = false val strip_star' = Sepref_Basic.strip_star #> filter (not o is_emp) (* Compare Termtab2s for equality of keys *) fun pairs_eq pairs1 pairs2 = Termtab2.forall (Termtab2.defined pairs1 o fst) pairs2 andalso Termtab2.forall (Termtab2.defined pairs2 o fst) pairs1 fun atomize_prem @{mpat "Trueprop ?p"} = p | atomize_prem _ = fail "Non-atomic premises" (* Make HOL conjunction list *) fun mk_conjs [] = @{const True} | mk_conjs [p] = p | mk_conjs (p::ps) = HOLogic.mk_binop @{const_name "HOL.conj"} (p,mk_conjs ps) (***********************) (* Start actual analysis *) val _ = add_dbg "thm" [Thm.prop_of thm] val prems = Thm.prems_of thm val concl = Thm.concl_of thm |> HOLogic.dest_Trueprop val (G,c,G',R,a) = dest_hn_refine concl val pre_pairs = G |> strip_star' |> tap (add_dbg "precondition") |> map dest_hn_ctxt |> Termtab2.make val post_pairs = G' |> strip_star' |> tap (add_dbg "postcondition") |> map dest_hn_ctxt |> Termtab2.make val _ = assert (pairs_eq pre_pairs post_pairs) "Parameters in precondition do not match postcondition" val aa_set = pre_pairs |> Termtab2.keys |> map fst |> Termtab.make_set val ca_set = pre_pairs |> Termtab2.keys |> map snd |> Termtab.make_set val (a,leading_RETURN) = strip_leading_RETURN aa_set a val (c,leading_return) = strip_leading_return ca_set c val _ = add_dbg "stripped abstract term" [a] val _ = add_dbg "stripped concrete term" [c] val (ahead,aargs) = strip_fun aa_set a; val (chead,cargs) = strip_fun ca_set c; val _ = add_dbg "abstract head" [ahead] val _ = add_dbg "abstract args" aargs val _ = add_dbg "concrete head" [chead] val _ = add_dbg "concrete args" cargs val _ = assert (length cargs = length aargs) "Different number of abstract and concrete arguments"; val _ = assert (not (has_duplicates op aconv aargs)) "Duplicate abstract arguments" val _ = assert (not (has_duplicates op aconv cargs)) "Duplicate concrete arguments" val argpairs = aargs ~~ cargs val ap_set = Termtab2.make_set argpairs val _ = assert (pairs_eq pre_pairs ap_set) "Arguments from pre/postcondition do not match operation's arguments" val pre_rels = map (the o (Termtab2.lookup pre_pairs)) argpairs val post_rels = map (the o (Termtab2.lookup post_pairs)) argpairs val _ = add_dbg "pre-rels" pre_rels val _ = add_dbg "post-rels" post_rels fun adjust_hf_pres @{mpat "snd (?R\<^sup>k)"} = R | adjust_hf_pres t = t val post_rels = map adjust_hf_pres post_rels fun is_invalid R @{mpat "invalid_assn ?R'"} = R aconv R' | is_invalid _ @{mpat "snd (_\<^sup>d)"} = true | is_invalid _ _ = false fun is_keep (R,R') = if R aconv R' then true else if is_invalid R R' then false else fail "Mismatch between pre and post relation for argument" val keep = map is_keep (pre_rels ~~ post_rels) val argrels = pre_rels ~~ keep val aa_set = Termtab.make_set aargs val ca_set = Termtab.make_set cargs fun is_precond t = (exists_subterm (Termtab.defined ca_set) t andalso fail "Premise contains concrete argument") orelse exists_subterm (Termtab.defined aa_set) t val (preconds, prems) = split is_precond prems val precond = map atomize_prem preconds |> mk_conjs |> fold lambda aargs val _ = add_dbg "precond" [precond] val _ = add_dbg "prems" prems in { thm = thm, precond = precond, prems = prems, ahead = (ahead,leading_RETURN), chead = (chead,leading_return), argrels = argrels, result_rel = R } end fun pretty_hnr_analysis ctxt ({thm,precond,ahead,chead,argrels,result_rel,...}) : Pretty.T = let val _ = thm (* Suppress unused warning for thm *) fun pretty_argrel (R,k) = Pretty.block [ Syntax.pretty_term ctxt R, if k then Pretty.str "\<^sup>k" else Pretty.str "\<^sup>d" ] val pretty_chead = case chead of (t,false) => Syntax.pretty_term ctxt t | (t,true) => Pretty.block [Pretty.str "return ", Syntax.pretty_term ctxt t] val pretty_ahead = case ahead of (t,false) => Syntax.pretty_term ctxt t | (t,true) => Pretty.block [Pretty.str "RETURN ", Syntax.pretty_term ctxt t] in Pretty.fbreaks [ (*Display.pretty_thm ctxt thm,*) Pretty.block [ Pretty.enclose "[" "]" [pretty_chead, pretty_ahead], Pretty.enclose "[" "]" [Syntax.pretty_term ctxt precond], Pretty.brk 1, Pretty.block (Pretty.separate " \" (map pretty_argrel argrels @ [Syntax.pretty_term ctxt result_rel])) ] ] |> Pretty.block end fun mk_hfref_thm ctxt ({thm,precond,prems,ahead,chead,argrels,result_rel}) = let fun mk_keep (R,true) = @{mk_term "?R\<^sup>k"} | mk_keep (R,false) = @{mk_term "?R\<^sup>d"} (* TODO: Move, this is of general use! *) fun mk_uncurry f = @{mk_term "uncurry ?f"} (* Uncurry function for the given number of arguments. For zero arguments, add a unit-parameter. *) fun rpt_uncurry n t = if n=0 then @{mk_term "uncurry0 ?t"} else if n=1 then t else funpow (n-1) mk_uncurry t (* Rewrite uncurried lambda's to \(_,_). _ form. Use top-down rewriting to correctly handle nesting to the left. TODO: Combine with abstraction and uncurry-procedure, and mark the deviation about uncurry as redundant intermediate step to be eliminated. *) fun rew_uncurry_lambda t = let val rr = map (Logic.dest_equals o Thm.prop_of) @{thms uncurry_def uncurry0_def} val thy = Proof_Context.theory_of ctxt in Pattern.rewrite_term_top thy rr [] t end (* Shortcuts for simplification tactics *) fun gsimp_only ctxt sec = let val ss = put_simpset HOL_basic_ss ctxt |> sec in asm_full_simp_tac ss end fun simp_only ctxt thms = gsimp_only ctxt (fn ctxt => ctxt addsimps thms) (********************************) (* Build theorem statement *) (* \prems\ \ (chead,ahead) \ [precond] rels \ R *) (* Uncurry precondition *) val num_args = length argrels val precond = precond |> rpt_uncurry num_args |> rew_uncurry_lambda (* Convert to nicer \((...,_),_) - form*) (* Re-attach leading RETURN/return *) fun mk_RETURN (t,r) = if r then let val T = funpow num_args range_type (fastype_of (fst ahead)) val tRETURN = Const (@{const_name RETURN}, T --> Type(@{type_name nres},[T])) in Refine_Util.mk_compN num_args tRETURN t end else t fun mk_return (t,r) = if r then let val T = funpow num_args range_type (fastype_of (fst chead)) val tRETURN = Const (@{const_name return}, T --> Type(@{type_name Heap},[T])) in Refine_Util.mk_compN num_args tRETURN t end else t (* Hrmpf!: Gone for good from 2015\2016. Inserting ctxt-based substitute here. *) fun certify_inst ctxt (instT, inst) = - (map (apsnd (Thm.ctyp_of ctxt)) (Term_Subst.TVars.dest instT), - map (apsnd (Thm.cterm_of ctxt)) (Term_Subst.Vars.dest inst)); + (map (apsnd (Thm.ctyp_of ctxt)) (TVars.dest instT), + map (apsnd (Thm.cterm_of ctxt)) (Vars.dest inst)); (* fun mk_RETURN (t,r) = if r then @{mk_term "RETURN o ?t"} else t fun mk_return (t,r) = if r then @{mk_term "return o ?t"} else t *) (* Uncurry abstract and concrete function, append leading return *) val ahead = ahead |> mk_RETURN |> rpt_uncurry num_args val chead = chead |> mk_return |> rpt_uncurry num_args (* Add keep-flags and summarize argument relations to product *) val argrel = map mk_keep argrels |> rev (* TODO: Why this rev? *) |> mk_hfprods (* Produce final result statement *) val result = @{mk_term "Trueprop ((?chead,?ahead) \ [?precond]\<^sub>a ?argrel \ ?result_rel)"} val result = Logic.list_implies (prems,result) (********************************) (* Prove theorem *) (* Create context and import result statement and original theorem *) val orig_ctxt = ctxt (*val thy = Proof_Context.theory_of ctxt*) val (insts, ctxt) = Variable.import_inst true [result] ctxt val insts' = certify_inst ctxt insts val result = Term_Subst.instantiate insts result val thm = Thm.instantiate insts' thm (* Unfold APP tags. This is required as some APP-tags have also been unfolded by analysis *) val thm = Local_Defs.unfold0 ctxt @{thms APP_def} thm (* Tactic to prove the theorem. A first step uses hfrefI to get a hnr-goal. This is then normalized in several consecutive steps, which get rid of uncurrying. Finally, the original theorem is used for resolution, where the pre- and postcondition, and result relation are connected with a consequence rule, to handle unfolded hn_ctxt-tags, re-ordered relations, and introduced unit-parameters (TODO: Mark artificially introduced unit-parameter specially, it may get confused with intentional unit-parameter, e.g., functional empty_set ()!) *) fun tac ctxt = resolve_tac ctxt @{thms hfrefI} THEN' gsimp_only ctxt (fn c => c addsimps @{thms uncurry_def hn_ctxt_def uncurry0_def keep_drop_sels uc_hfprod_sel o_apply APP_def} |> Splitter.add_split @{thm prod.split} ) THEN' TRY o ( REPEAT_ALL_NEW (match_tac ctxt @{thms allI impI}) THEN' simp_only ctxt @{thms Product_Type.split prod.inject}) THEN' TRY o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE}) THEN' TRY o hyp_subst_tac ctxt THEN' simp_only ctxt @{thms triv_forall_equality} THEN' ( resolve_tac ctxt @{thms hn_refine_cons[rotated]} THEN' (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt)) THEN_ALL_NEW simp_only ctxt @{thms hn_ctxt_def entt_refl pure_unit_rel_eq_empty mult_ac mult_1 mult_1_right keep_drop_sels} (* Prove theorem *) val result = Thm.cterm_of ctxt result val rthm = Goal.prove_internal ctxt [] result (fn _ => ALLGOALS (tac ctxt)) (* Export statement to original context *) val rthm = singleton (Variable.export ctxt orig_ctxt) rthm (* Post-processing *) val rthm = Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hfref_post}) rthm in rthm end fun to_hfref ctxt = analyze_hnr ctxt #> mk_hfref_thm ctxt (***********************************) (* Composition *) local fun norm_set_of ctxt = { trans_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_trans}, cong_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_cong}, norm_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_norm}, refl_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_refl} } fun init_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_init} fun unfold_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_unfold} fun simp_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_simps} in fun norm_fcomp_rule ctxt = let open PO_Normalizer Refine_Util val norm1 = gen_norm_rule (init_rules_of ctxt) (norm_set_of ctxt) ctxt val norm2 = Local_Defs.unfold0 ctxt (unfold_rules_of ctxt) val norm3 = Conv.fconv_rule ( Simplifier.asm_full_rewrite (put_simpset HOL_basic_ss ctxt addsimps simp_rules_of ctxt)) val norm = changed_rule (try_rule norm1 o try_rule norm2 o try_rule norm3) in repeat_rule norm end end fun add_pure_constraints_rule ctxt thm = let val orig_ctxt = ctxt val t = Thm.prop_of thm fun cnv (@{mpat (typs) "pure (mpaq_STRUCT (mpaq_Var ?x _) :: (?'v_c\?'v_a) set)"}) = let val T = a --> c --> @{typ assn} val t = Var (x,T) val t = @{mk_term "(the_pure ?t)"} in [(x,T,t)] end | cnv (t$u) = union op= (cnv t) (cnv u) | cnv (Abs (_,_,t)) = cnv t | cnv _ = [] val pvars = cnv t val _ = (pvars |> map #1 |> has_duplicates op=) andalso raise TERM ("Duplicate indexname with different type",[t]) (* This should not happen *) val substs = map (fn (x,_,t) => (x,t)) pvars val t' = subst_Vars substs t fun mk_asm (x,T,_) = let val t = Var (x,T) val t = @{mk_term "Trueprop (CONSTRAINT is_pure ?t)"} in t end val assms = map mk_asm pvars fun add_prems prems t = let val prems' = Logic.strip_imp_prems t val concl = Logic.strip_imp_concl t in Logic.list_implies (prems@prems', concl) end val t' = add_prems assms t' val (t',ctxt) = yield_singleton (Variable.import_terms true) t' ctxt val thm' = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt t') (fn _ => ALLGOALS (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt)) val thm' = norm_fcomp_rule ctxt thm' val thm' = singleton (Variable.export ctxt orig_ctxt) thm' in thm' end val cfg_simp_precond = Attrib.setup_config_bool @{binding fcomp_simp_precond} (K true) local fun mk_simp_thm ctxt t = let val st = t |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Goal.init val ctxt = Context_Position.set_visible false ctxt val ctxt = ctxt addsimps ( refine_pw_simps.get ctxt @ Named_Theorems.get ctxt @{named_theorems fcomp_prenorm_simps} @ @{thms split_tupled_all cnv_conj_to_meta} ) val trace_incomplete_transfer_tac = COND (Thm.prems_of #> exists (strip_all_body #> Logic.strip_imp_concl #> Term.is_open)) (print_tac ctxt "Failed transfer from intermediate level:") all_tac val tac = ALLGOALS (resolve_tac ctxt @{thms auto_weaken_pre_comp_PRE_I} ) THEN ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN trace_incomplete_transfer_tac THEN ALLGOALS (TRY o filter_prems_tac ctxt (K false)) THEN Local_Defs.unfold0_tac ctxt [Drule.triv_forall_equality] val st' = tac st |> Seq.take 1 |> Seq.list_of val thm = case st' of [st'] => Goal.conclude st' | _ => raise THM("Simp_Precond: Simp-Tactic failed",~1,[st]) (* Check generated premises for leftover intermediate stuff *) val _ = exists (Logic.is_all) (Thm.prems_of thm) andalso raise THM("Simp_Precond: Transfer from intermediate level failed",~1,[thm]) val thm = thm (*|> map (Simplifier.asm_full_simplify ctxt)*) |> Conv.fconv_rule (Object_Logic.atomize ctxt) |> Local_Defs.unfold0 ctxt @{thms auto_weaken_pre_to_imp_nf} val thm = case Thm.concl_of thm of @{mpat "Trueprop (_ \ _)"} => thm | @{mpat "Trueprop _"} => thm RS @{thm auto_weaken_pre_add_dummy_imp} | _ => raise THM("Simp_Precond: Generated odd theorem, expected form 'P\Q'",~1,[thm]) in thm end in fun simplify_precond ctxt thm = let val orig_ctxt = ctxt val thm = Refine_Util.OF_fst @{thms auto_weaken_pre_init} [asm_rl,thm] val thm = Local_Defs.unfold0 ctxt @{thms split_tupled_all} thm OF @{thms auto_weaken_pre_uncurry_start} fun rec_uncurry thm = case try (fn () => thm OF @{thms auto_weaken_pre_uncurry_step}) () of NONE => thm OF @{thms auto_weaken_pre_uncurry_finish} | SOME thm => rec_uncurry thm val thm = rec_uncurry thm |> Conv.fconv_rule Thm.eta_conversion val t = case Thm.prems_of thm of t::_ => t | _ => raise THM("Simp-Precond: Expected at least one premise",~1,[thm]) val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt val ((_,t),ctxt) = Variable.focus NONE t ctxt val t = case t of @{mpat "Trueprop (_ \ ?t)"} => t | _ => raise TERM("Simp_Precond: Expected implication",[t]) val simpthm = mk_simp_thm ctxt t |> singleton (Variable.export ctxt orig_ctxt) val thm = thm OF [simpthm] val thm = Local_Defs.unfold0 ctxt @{thms prod_casesK} thm in thm end fun simplify_precond_if_cfg ctxt = if Config.get ctxt cfg_simp_precond then simplify_precond ctxt else I end (* fref O fref *) fun compose_ff ctxt A B = (@{thm fref_compI_PRE} OF [A,B]) |> norm_fcomp_rule ctxt |> simplify_precond_if_cfg ctxt |> Conv.fconv_rule Thm.eta_conversion (* hfref O fref *) fun compose_hf ctxt A B = (@{thm hfref_compI_PRE} OF [A,B]) |> norm_fcomp_rule ctxt |> simplify_precond_if_cfg ctxt |> Conv.fconv_rule Thm.eta_conversion |> add_pure_constraints_rule ctxt |> Conv.fconv_rule Thm.eta_conversion fun ensure_fref ctxt thm = case rthm_type thm of RT_HOPARAM => to_fref ctxt thm | RT_FREF => thm | _ => raise THM("Expected parametricity or fref theorem",~1,[thm]) fun ensure_fref_nres ctxt thm = let val thm = ensure_fref ctxt thm in case Thm.concl_of thm of @{mpat (typs) "Trueprop (_\fref _ _ (_::(_ nres\_)set))"} => thm | @{mpat "Trueprop ((_,_)\fref _ _ _)"} => (thm RS @{thm ensure_fref_nresI}) |> Local_Defs.unfold0 ctxt @{thms ensure_fref_nres_unfold} | _ => raise THM("Expected fref-theorem",~1,[thm]) end fun ensure_hfref ctxt thm = case rthm_type thm of RT_HNR => to_hfref ctxt thm | RT_HFREF => thm | _ => raise THM("Expected hnr or hfref theorem",~1,[thm]) fun ensure_hnr ctxt thm = case rthm_type thm of RT_HNR => thm | RT_HFREF => to_hnr ctxt thm | _ => raise THM("Expected hnr or hfref theorem",~1,[thm]) fun gen_compose ctxt A B = let val rtA = rthm_type A in if rtA = RT_HOPARAM orelse rtA = RT_FREF then compose_ff ctxt (ensure_fref ctxt A) (ensure_fref ctxt B) else compose_hf ctxt (ensure_hfref ctxt A) ((ensure_fref_nres ctxt B)) end val parse_fcomp_flags = Refine_Util.parse_paren_lists (Refine_Util.parse_bool_config "prenorm" cfg_simp_precond) val fcomp_attrib = parse_fcomp_flags |-- Attrib.thm >> (fn B => Thm.rule_attribute [] (fn context => fn A => let val ctxt = Context.proof_of context in gen_compose ctxt A B end)) end \ attribute_setup to_fref = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_fref o Context.proof_of)) \ "Convert parametricity theorem to uncurried fref-form" attribute_setup to_foparam = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of)) \ \Convert param or fref rule to first order rule\ (* Overloading existing param_fo - attribute from Parametricity.thy *) attribute_setup param_fo = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of)) \ \Convert param or fref rule to first order rule\ attribute_setup to_hnr = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_hnr o Context.proof_of)) \ "Convert hfref-rule to hnr-rule" attribute_setup to_hfref = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.to_hfref) )\ \Convert hnr to hfref theorem\ attribute_setup ensure_fref_nres = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.ensure_fref_nres) )\ attribute_setup sepref_dbg_norm_fcomp_rule = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.norm_fcomp_rule) )\ attribute_setup sepref_simplify_precond = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.simplify_precond) )\ \Simplify precondition of fref/hfref-theorem\ attribute_setup FCOMP = Sepref_Rules.fcomp_attrib "Composition of refinement rules" end diff --git a/thys/Refine_Monadic/Refine_Automation.thy b/thys/Refine_Monadic/Refine_Automation.thy --- a/thys/Refine_Monadic/Refine_Automation.thy +++ b/thys/Refine_Monadic/Refine_Automation.thy @@ -1,555 +1,555 @@ section "More Automation" theory Refine_Automation imports Refine_Basic Refine_Transfer keywords "concrete_definition" :: thy_decl and "prepare_code_thms" :: thy_decl and "uses" begin text \ This theory provides a tool for extracting definitions from terms, and for generating code equations for recursion combinators. \ ML \ signature REFINE_AUTOMATION = sig type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } val extract_as_def: (string * typ) list -> string -> term -> local_theory -> ((term * thm) * local_theory) val extract_recursion_eqs: extraction list -> string -> thm -> local_theory -> local_theory val add_extraction: string -> extraction -> theory -> theory val prepare_code_thms_cmd: string list -> thm -> local_theory -> local_theory val define_concrete_fun: extraction list option -> binding -> Token.src list -> indexname list -> thm -> cterm list -> local_theory -> (thm * thm) * local_theory val mk_qualified: string -> bstring -> binding val prepare_cd_pattern: Proof.context -> cterm -> cterm val add_cd_pattern: cterm -> Context.generic -> Context.generic val del_cd_pattern: cterm -> Context.generic -> Context.generic val get_cd_patterns: Proof.context -> cterm list val add_vc_rec_thm: thm -> Context.generic -> Context.generic val del_vc_rec_thm: thm -> Context.generic -> Context.generic val get_vc_rec_thms: Proof.context -> thm list val add_vc_solve_thm: thm -> Context.generic -> Context.generic val del_vc_solve_thm: thm -> Context.generic -> Context.generic val get_vc_solve_thms: Proof.context -> thm list val vc_solve_tac: Proof.context -> bool -> tactic' val vc_solve_modifiers: Method.modifier parser list val setup: theory -> theory end structure Refine_Automation :REFINE_AUTOMATION = struct type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } structure extractions = Generic_Data ( type T = extraction list Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge_list ((op =) o apply2 #pattern) ) fun add_extraction name ex = Context.theory_map (extractions.map ( Symtab.update_list ((op =) o apply2 #pattern) (name,ex))) (* Define new constant name for subterm t in context bnd. Returns replacement for t using the new constant and definition theorem. *) fun extract_as_def bnd name t lthy = let val loose = rev (loose_bnos t); val rnames = #1 (Variable.names_of lthy |> fold_map (Name.variant o #1) bnd); val rfrees = map (fn (name,(_,typ)) => Free (name,typ)) (rnames ~~ bnd); val t' = subst_bounds (rfrees,t); val params = map Bound (rev loose); val param_vars = (Library.foldl (fn (l,i) => nth rfrees i :: l) ([],loose)); val param_types = map fastype_of param_vars; val def_t = Logic.mk_equals (list_comb (Free (name,param_types ---> fastype_of t'),param_vars),t'); val ((lhs_t,(_,def_thm)),lthy) = Specification.definition NONE [] [] (Binding.empty_atts,def_t) lthy; (*val _ = tracing "xxxx";*) val app_t = list_comb (lhs_t, params); in ((app_t,def_thm),lthy) end; fun mk_qualified basename q = Binding.qualify true basename (Binding.name q); fun extract_recursion_eqs exs basename orig_def_thm lthy = let val thy = Proof_Context.theory_of lthy val pat_net : extraction Item_Net.T = Item_Net.init ((op =) o apply2 #pattern) (fn {pattern, ...} => [pattern]) |> fold Item_Net.update exs local fun tr env t ctx = let (* Recurse for subterms *) val (t,ctx) = case t of t1$t2 => let val (t1,ctx) = tr env t1 ctx val (t2,ctx) = tr env t2 ctx in (t1$t2,ctx) end | Abs (x,T,t) => let val (t',ctx) = tr ((x,T)::env) t ctx in (Abs (x,T,t'),ctx) end | _ => (t,ctx) (* Check if we match a pattern *) val ex = Item_Net.retrieve_matching pat_net t |> get_first (fn ex => case try (Pattern.first_order_match thy (#pattern ex,t)) (Vartab.empty,Vartab.empty) of NONE => NONE | SOME _ => SOME ex ) in case ex of NONE => (t,ctx) | SOME ex => let (* Extract as new constant *) val (idx,defs,lthy) = ctx val name = (basename ^ "_" ^ string_of_int idx) val ((t,def_thm),lthy) = extract_as_def env name t lthy val ctx = (idx+1,(def_thm,ex)::defs,lthy) in (t,ctx) end end in fun transform t lthy = let val (t,(_,defs,lthy)) = tr [] t (0,[],lthy) in ((t,defs),lthy) end end (* Import theorem and extract RHS *) val ((_,orig_def_thm'),lthy) = yield_singleton2 (Variable.import true) orig_def_thm lthy; val (lhs,rhs) = orig_def_thm' |> Thm.prop_of |> Logic.dest_equals; (* Transform RHS, generating new constants *) val ((rhs',defs),lthy) = transform rhs lthy; val def_thms = map #1 defs (* Register definitions of generated constants *) val (_,lthy) = Local_Theory.note ((mk_qualified basename "defs",[]),def_thms) lthy; (* Obtain new def_thm *) val def_unfold_ss = put_simpset HOL_basic_ss lthy addsimps (orig_def_thm::def_thms) val new_def_thm = Goal.prove_internal lthy [] (Logic.mk_equals (lhs,rhs') |> Thm.cterm_of lthy) (K (simp_tac def_unfold_ss 1)) (* Obtain new theorem by folding with defs of generated constants *) (* TODO: Maybe cleaner to generate eq-thm and prove by "unfold, refl" *) (*val new_def_thm = Library.foldr (fn (dt,t) => Local_Defs.fold lthy [dt] t) (def_thms,orig_def_thm');*) (* Prepare code equations *) fun mk_code_thm lthy (def_thm,{gen_thm, gen_tac, ...}) = let val ((_,def_thm),lthy') = yield_singleton2 (Variable.import true) def_thm lthy; val thm = def_thm RS gen_thm; val tac = SOLVED' (gen_tac lthy') ORELSE' (simp_tac def_unfold_ss THEN' gen_tac lthy') val thm = the (SINGLE (ALLGOALS tac) thm); val thm = singleton (Variable.export lthy' lthy) thm; in thm end; val code_thms = map (mk_code_thm lthy) defs; val _ = if forall Thm.no_prems code_thms then () else warning "Unresolved premises in code theorems" val (_,lthy) = Local_Theory.note ((mk_qualified basename "code",@{attributes [code]}),new_def_thm::code_thms) lthy; in lthy end; fun prepare_code_thms_cmd names thm lthy = let fun name_of (Const (n,_)) = n | name_of (Free (n,_)) = n | name_of _ = raise (THM ("No definitional theorem",0,[thm])); val (lhs,_) = thm |> Thm.prop_of |> Logic.dest_equals; val basename = lhs |> strip_comb |> #1 |> name_of |> Long_Name.base_name; val exs_tab = extractions.get (Context.Proof lthy) fun get_exs name = case Symtab.lookup exs_tab name of NONE => error ("No such extraction mode: " ^ name) | SOME exs => exs val exs = case names of [] => Symtab.dest_list exs_tab |> map #2 | _ => map get_exs names |> flat val _ = case exs of [] => error "No extraction patterns selected" | _ => () val lthy = extract_recursion_eqs exs basename thm lthy in lthy end; fun extract_concrete_fun _ [] concl = raise TERM ("Conclusion does not match any extraction pattern",[concl]) | extract_concrete_fun thy (pat::pats) concl = ( case Refine_Util.fo_matchp thy pat concl of NONE => extract_concrete_fun thy pats concl | SOME [t] => t | SOME (t::_) => ( warning ("concrete_definition: Pattern has multiple holes, taking " ^ "first one: " ^ @{make_string} pat ); t) | _ => (warning ("concrete_definition: Ignoring invalid pattern " ^ @{make_string} pat); extract_concrete_fun thy pats concl) ) (* Define concrete function from refinement lemma *) fun define_concrete_fun gen_code fun_name attribs_raw param_names thm pats (orig_lthy:local_theory) = let val lthy = orig_lthy; val (((_,inst),thm'),lthy) = yield_singleton2 (Variable.import true) thm lthy; val concl = thm' |> Thm.concl_of (*val ((typ_subst,term_subst),lthy) = Variable.import_inst true [concl] lthy; val concl = Term_Subst.instantiate (typ_subst,term_subst) concl; *) - val term_subst = build (inst |> Term_Subst.Vars.fold (cons o apsnd Thm.term_of)) + val term_subst = build (inst |> Vars.fold (cons o apsnd Thm.term_of)) val param_terms = map (fn name => case AList.lookup (fn (n,v) => n = #1 v) term_subst name of NONE => raise TERM ("No such variable: " ^Term.string_of_vname name,[concl]) | SOME t => t ) param_names; val f_term = extract_concrete_fun (Proof_Context.theory_of lthy) pats concl; val lhs_type = map Term.fastype_of param_terms ---> Term.fastype_of f_term; val lhs_term = list_comb ((Free (Binding.name_of fun_name,lhs_type)),param_terms); val def_term = Logic.mk_equals (lhs_term,f_term) |> fold Logic.all param_terms; val attribs = map (Attrib.check_src lthy) attribs_raw; val ((_,(_,def_thm)),lthy) = Specification.definition (SOME (fun_name,NONE,Mixfix.NoSyn)) [] [] ((Binding.empty,attribs),def_term) lthy; val folded_thm = Local_Defs.fold lthy [def_thm] thm'; val (_,lthy) = Local_Theory.note ((mk_qualified (Binding.name_of fun_name) "refine",[]),[folded_thm]) lthy; val lthy = case gen_code of NONE => lthy | SOME modes => extract_recursion_eqs modes (Binding.name_of fun_name) def_thm lthy in ((def_thm,folded_thm),lthy) end; val cd_pat_eq = apply2 (Thm.term_of #> Refine_Util.anorm_term) #> (op aconv) structure cd_patterns = Generic_Data ( type T = cterm list val empty = [] val extend = I val merge = merge cd_pat_eq ) fun prepare_cd_pattern ctxt pat = case Thm.term_of pat |> fastype_of of @{typ bool} => Thm.term_of pat |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt | _ => pat fun add_cd_pattern pat context = cd_patterns.map (insert cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context fun del_cd_pattern pat context = cd_patterns.map (remove cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context val get_cd_patterns = cd_patterns.get o Context.Proof structure rec_thms = Named_Thms ( val name = @{binding vcs_rec} val description = "VC-Solver: Recursive intro rules" ) structure solve_thms = Named_Thms ( val name = @{binding vcs_solve} val description = "VC-Solver: Solve rules" ) val add_vc_rec_thm = rec_thms.add_thm val del_vc_rec_thm = rec_thms.del_thm val get_vc_rec_thms = rec_thms.get val add_vc_solve_thm = solve_thms.add_thm val del_vc_solve_thm = solve_thms.del_thm val get_vc_solve_thms = solve_thms.get val rec_modifiers = [ Args.$$$ "rec" -- Scan.option Args.add -- Args.colon >> K (Method.modifier rec_thms.add \<^here>), Args.$$$ "rec" -- Scan.option Args.del -- Args.colon >> K (Method.modifier rec_thms.del \<^here>) ]; val solve_modifiers = [ Args.$$$ "solve" -- Scan.option Args.add -- Args.colon >> K (Method.modifier solve_thms.add \<^here>), Args.$$$ "solve" -- Scan.option Args.del -- Args.colon >> K (Method.modifier solve_thms.del \<^here>) ]; val vc_solve_modifiers = clasimp_modifiers @ rec_modifiers @ solve_modifiers; fun vc_solve_tac ctxt no_pre = let val rthms = rec_thms.get ctxt val sthms = solve_thms.get ctxt val pre_tac = if no_pre then K all_tac else clarsimp_tac ctxt val tac = SELECT_GOAL (auto_tac ctxt) in TRY o pre_tac THEN_ALL_NEW_FWD (TRY o REPEAT_ALL_NEW_FWD (resolve_tac ctxt rthms)) THEN_ALL_NEW_FWD (TRY o SOLVED' (resolve_tac ctxt sthms THEN_ALL_NEW_FWD tac)) end val setup = I #> rec_thms.setup #> solve_thms.setup end; \ setup Refine_Automation.setup setup \ let fun parse_cpat cxt = let val (t, (context, tks)) = Scan.lift Args.embedded_inner_syntax cxt val ctxt = Context.proof_of context val t = Proof_Context.read_term_pattern ctxt t in (Thm.cterm_of ctxt t, (context, tks)) end fun do_p f = Scan.repeat1 parse_cpat >> (fn pats => Thm.declaration_attribute (K (fold f pats))) in Attrib.setup @{binding "cd_patterns"} ( Scan.lift Args.add |-- do_p Refine_Automation.add_cd_pattern || Scan.lift Args.del |-- do_p Refine_Automation.del_cd_pattern || do_p Refine_Automation.add_cd_pattern ) "Add/delete concrete_definition pattern" end \ (* Command setup *) (* TODO: Folding of .refine-lemma seems not to work, if the function has parameters on which it does not depend *) ML \Outer_Syntax.local_theory @{command_keyword concrete_definition} "Define function from refinement theorem" (Parse.binding -- Parse.opt_attribs -- Scan.optional (@{keyword "for"} |-- Scan.repeat1 Args.var) [] --| @{keyword "uses"} -- Parse.thm -- Scan.optional (@{keyword "is"} |-- Scan.repeat1 Args.embedded_inner_syntax) [] >> (fn ((((name,attribs),params),raw_thm),pats) => fn lthy => let val thm = case Attrib.eval_thms lthy [raw_thm] of [thm] => thm | _ => error "Expecting exactly one theorem"; val pats = case pats of [] => Refine_Automation.get_cd_patterns lthy | l => map (Proof_Context.read_term_pattern lthy #> Thm.cterm_of lthy #> Refine_Automation.prepare_cd_pattern lthy) l in Refine_Automation.define_concrete_fun NONE name attribs params thm pats lthy |> snd end)) \ text \ Command: \concrete_definition name [attribs] for params uses thm is patterns\ where \attribs\, \for\, and \is\-parts are optional. Declares a new constant \name\ by matching the theorem \thm\ against a pattern. If the \for\ clause is given, it lists variables in the theorem, and thus determines the order of parameters of the defined constant. Otherwise, parameters will be in order of occurrence. If the \is\ clause is given, it lists patterns. The conclusion of the theorem will be matched against each of these patterns. For the first matching pattern, the constant will be declared to be the term that matches the first non-dummy variable of the pattern. If no \is\-clause is specified, the default patterns will be tried. Attribute: \cd_patterns pats\. Declaration attribute. Declares default patterns for the \concrete_definition\ command. \ declare [[ cd_patterns "(?f,_)\_"]] declare [[ cd_patterns "RETURN ?f \ _" "nres_of ?f \ _"]] declare [[ cd_patterns "(RETURN ?f,_)\_" "(nres_of ?f,_)\_"]] declare [[ cd_patterns "_ = ?f" "_ == ?f" ]] ML \ let val modes = (Scan.optional (@{keyword "("} |-- Parse.list1 Parse.name --| @{keyword ")"}) []) in Outer_Syntax.local_theory @{command_keyword prepare_code_thms} "Refinement framework: Prepare theorems for code generation" (modes -- Parse.thms1 >> (fn (modes,raw_thms) => fn lthy => let val thms = Attrib.eval_thms lthy raw_thms in fold (Refine_Automation.prepare_code_thms_cmd modes) thms lthy end) ) end \ text \ Command: \prepare_code_thms (modes) thm\ where the \(mode)\-part is optional. Set up code-equations for recursions in constant defined by \thm\. The optional \modes\ is a comma-separated list of extraction modes. \ lemma gen_code_thm_RECT: fixes x assumes D: "f \ RECT B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst RECT_unfold) by (rule M) lemma gen_code_thm_REC: fixes x assumes D: "f \ REC B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst REC_unfold) by (rule M) setup \ Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "REC x"}, gen_thm = @{thm gen_code_thm_REC}, gen_tac = Refine_Mono_Prover.mono_tac } #> Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "RECT x"}, gen_thm = @{thm gen_code_thm_RECT}, gen_tac = Refine_Mono_Prover.mono_tac } \ text \ Method \vc_solve (no_pre) clasimp_modifiers rec (add/del): ... solve (add/del): ...\ Named theorems \vcs_rec\ and \vcs_solve\. This method is specialized to solve verification conditions. It first clarsimps all goals, then it tries to apply a set of safe introduction rules (\vcs_rec\, \rec add\). Finally, it applies introduction rules (\vcs_solve\, \solve add\) and tries to discharge all emerging subgoals by auto. If this does not succeed, it backtracks over the application of the solve-rule. \ method_setup vc_solve = \Scan.lift (Args.mode "nopre") --| Method.sections Refine_Automation.vc_solve_modifiers >> (fn (nopre) => fn ctxt => SIMPLE_METHOD ( CHANGED (ALLGOALS (Refine_Automation.vc_solve_tac ctxt nopre)) ))\ "Try to solve verification conditions" end