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,1368 +1,1368 @@ (* 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 = 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 = 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.full_rules}; 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.full_rules; 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' = Term_Subst.instantiate (tvars ~~ Ts, []) base_prop; 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 (Variable.auto_fixes t ctxt) ctxt) t) [] of + (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 [(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' = Term_Subst.instantiate (tvars ~~ Ts, []) base; 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/Auto2_HOL/HOL/matcher_test.ML b/thys/Auto2_HOL/HOL/matcher_test.ML --- a/thys/Auto2_HOL/HOL/matcher_test.ML +++ b/thys/Auto2_HOL/HOL/matcher_test.ML @@ -1,269 +1,269 @@ (* File: matcher_test.ML Author: Bohua Zhan Unit test of matcher.ML. *) local val init = @{context} (* Conversion between (id, th) used in rewrite.ML and (id, t) used in test cases. *) fun to_term_info (id, th) = (id, Util.rhs_of th) (* Comparison of list of (box_id, term) pairs. *) fun eq_info_list (l1, l2) = (length l1 = length l2) andalso eq_set (eq_pair (op =) (op aconv)) (l1, l2) fun print_term_info ctxt (id, t) = "(" ^ (BoxID.string_of_box_id id) ^ ", " ^ (Syntax.string_of_term ctxt t) ^ ")" fun print_term_infos ctxt lst = commas (map (print_term_info ctxt) lst) (* info is expected, in box_id * term form, info' is returned value, in box_id * thm form (to be printed). *) fun assert_eq_info (info, info') txt ctxt = if eq_info_list (info, map to_term_info info') then ctxt else let val _ = tracing ("Expected: " ^ print_term_infos ctxt info ^ "\n" ^ "Actual: " ^ print_infos ctxt info') in raise Fail txt end fun add_prim_id (prim_id, id) ctxt = let val (prim_id', ctxt') = BoxID.add_prim_id id ctxt val _ = assert (prim_id = prim_id') "add_prim_id" in ctxt' end fun declare_term str ctxt = - Variable.auto_fixes (Syntax.read_term ctxt str) ctxt + Proof_Context.augment (Syntax.read_term ctxt str) ctxt fun declare_pat str ctxt = - Variable.auto_fixes (Proof_Context.read_term_pattern ctxt str) ctxt + Proof_Context.augment (Proof_Context.read_term_pattern ctxt str) ctxt fun add_rewrite id (str1, str2) ctxt = let val (t1, t2) = (Syntax.read_term ctxt str1, Syntax.read_term ctxt str2) val thy = Proof_Context.theory_of ctxt val th = assume_eq thy (t1, t2) in ctxt |> RewriteTable.add_rewrite (id, th) |> snd end (* Check th is actually t(env) == u. *) fun check_info (t, u) txt ctxt ((_, inst), th) = let val t' = Util.subst_term_norm inst t val (lhs, rhs) = Logic.dest_equals (Thm.prop_of th) in if lhs aconv t' andalso rhs aconv u then () else let val _ = tracing ("inst does not match th.\nt', u' = " ^ (Util.string_of_terms ctxt [t', u]) ^ "\nth = " ^ (Syntax.string_of_term ctxt (Thm.prop_of th))) in raise Fail txt end end fun assert_match_gen matcher ((str_t, str_u), info_str) ctxt = let val (t, u) = (Proof_Context.read_term_pattern ctxt str_t, Syntax.read_term ctxt str_u) val _ = trace_tlist ctxt "Matching" [t, u] val info = map (apsnd (Syntax.read_term ctxt)) info_str val info' = matcher ctxt [] (t, Thm.cterm_of ctxt u) ([], fo_init) val _ = map (check_info (t, u) "assert_match" ctxt) info' val info'' = map (fn ((id, _), th) => (id, meta_sym th)) info' in assert_eq_info (info, info'') "assert_match" ctxt end val assert_match = assert_match_gen Matcher.match fun assert_match_list (pairs_str, info_str) ctxt = let val pairs = map (fn (is_head, (str_t, str_u)) => (is_head, (Proof_Context.read_term_pattern ctxt str_t, Thm.cterm_of ctxt (Syntax.read_term ctxt str_u)))) pairs_str val info = map (apsnd (map (Syntax.read_term ctxt))) info_str val info' = Matcher.rewrite_match_list ctxt pairs ([], fo_init) fun check_info_list (instsp, ths) = let fun check_pair ((t, cu), th) = check_info (t, Thm.term_of cu) "assert_match_list" ctxt (instsp, th) in map check_pair (map snd pairs ~~ ths) end val _ = map check_info_list info' val info'' = map (fn ((id, _), ths) => (id, map meta_sym ths)) info' val eq_info_list' = eq_set (eq_pair (op =) (eq_list (op aconv))) fun to_term_info' (id, ths) = (id, map Util.rhs_of ths) in if eq_info_list' (info, map to_term_info' info'') then ctxt else let val _ = tracing ("got " ^ print_infos' ctxt info'') in raise Fail "assert_match_list" end end fun done str _ = let val _ = tracing ("Finished " ^ str) in () end in (* Basic rewriting. *) val test_rewrite = init |> add_prim_id (1, []) |> add_prim_id (2, []) |> declare_term "[a::nat, b, c]" |> declare_term "f::(nat => nat => nat)" |> declare_pat "[?m::nat, ?n]" |> declare_pat "?A::('a::{plus})" |> add_rewrite [1] ("a", "b") |> add_rewrite [2] ("a", "c") |> fold assert_match [(("a", "b"), [([1], "a")]), (("c", "a"), [([2], "c")]), (("?n + ?n", "a + b"), [([1], "a + a")]), (("?A + ?A", "c + a"), [([2], "c + c")]), (("?A + ?A + ?A", "a + b + c"), [([1, 2], "a + a + a")]), (("f ?m ?n", "f a b"), [([], "f a b")]), (("f ?m ?m", "f c a"), [([2], "f c c")])] |> done "test_rewrite" (* Rewriting from atomic to function application. *) val test_rewrite2 = init |> add_prim_id (1, []) |> add_prim_id (2, []) |> declare_term "[a::nat, b, c]" |> declare_pat "[?n::nat]" |> add_rewrite [1] ("a", "b + c") |> add_rewrite [2] ("b", "c") |> assert_match (("?n + ?n", "a"), [([1, 2], "b + b")]) |> done "test_rewrite2" (* Abstractions. *) val test_abstraction = init |> declare_term "[m::nat, n]" |> declare_term "P::(nat => nat => nat)" |> declare_pat "?A::(nat => nat => 'a::{plus})" |> fold assert_match [(("%x y. ?A x y", "%m n. P m n"), [([], "%m n. P m n")]), (("%x y. ?A x y + ?A y x", "%m n. P m n + P n m"), [([], "%m n. P m n + P n m")]), (("%x y. ?A x y", "%x y. (x::nat) + y + y"), [([], "%x y. (x::nat) + y + y")])] |> done "test_abstraction" (* Abstractions with rewriting. *) val test_abstraction_rewrite = init |> declare_term "[m::nat, n, p]" |> declare_term "P::(nat => nat => nat)" |> declare_term "f::(nat => nat => 'a::{plus})" |> declare_pat "?A::(nat => ?'a::{plus})" |> add_rewrite [] ("m", "n") |> add_rewrite [] ("p", "0::nat") |> assert_match (("%x. ?A x + ?A x", "%x. P x m + P x n"), [([], "%x. P x m + P x m")]) |> assert_match (("%x. f x 0", "%x. f x p"), [([], "%x. f x 0")]) |> done "test_abstraction_rewrite" (* Test matching of higher order patterns. *) val test_higher_order = init |> declare_term "f::(nat => nat)" |> declare_pat "?f::(nat => nat)" |> assert_match (("%n. (?f n, ?f (n + 1))", "%n. (f n, f (n + 1))"), [([], "%n. (f n, f (n + 1))")]) |> assert_match (("%n. (?f (n + 1), ?f n)", "%n. (f (n + 1), f n)"), [([], "%n. (f (n + 1), f n)")]) |> done "test_higher_order" (* Test handling of schematic type variables. *) val test_match_type = init |> assert_match (("image_mset ?f {#}", "{#i. i :# {#}#}"), [([], "{#i. i :# {#}#}")]) |> assert_match (("image_mset ?f {#}", "{#(i::nat). i :# {#}#}"), [([], "{#(i::nat). i :# {#}#}")]) (* sorted [] has concrete type, but not []. *) |> assert_match (("sorted []", "sorted []"), [([], "sorted []")]) |> done "test_match_type" (* Test special schematic variable ?NUMC. *) val test_numc = init |> declare_term "[k::int, m]" |> add_rewrite [] ("k", "1::int") |> assert_match (("?NUMC::int", "k"), [([], "1::int")]) |> assert_match (("?NUMC", "k"), [([], "1::int")]) |> assert_match (("?NUMC", "m"), []) |> done "test_numc" (* Test match list. *) val test_match_list = init |> declare_term "[k::nat, l]" |> declare_pat "?a::nat" |> add_rewrite [] ("k", "l") |> assert_match_list ([(false, ("?a", "k")), (false, ("?a", "l"))], [([], ["k", "k"])]) |> assert_match_list ([(false, ("?a", "k")), (true, ("?a", "l"))], []) |> assert_match_list ([(true, ("?a", "k")), (false, ("?a", "l"))], [([], ["k", "k"])]) |> assert_match_list ([(true, ("?a + b", "k + b")), (true, ("?a + b", "l + b"))], [([], ["k + b", "k + b"])]) |> done "test_match_list" (* Test of pre-matcher. *) fun assert_pre_match_gen res at_head (str_t, str_u) ctxt = let val (t, cu) = (Proof_Context.read_term_pattern ctxt str_t, Thm.cterm_of ctxt (Syntax.read_term ctxt str_u)) val pre_match_fn = if at_head then Matcher.pre_match_head else Matcher.pre_match in if pre_match_fn ctxt (t, cu) = res then ctxt else let val _ = trace_tlist ctxt "Pattern, term: " [t, Thm.term_of cu] in raise Fail ("assert_pre_match (expected " ^ (Util.string_of_bool res) ^ ")") end end val assert_pre_match = assert_pre_match_gen true false val assert_not_pre_match = assert_pre_match_gen false false val test_pre_match = init |> declare_term "[m::nat, n]" |> declare_term "[a::'a]" |> declare_pat "?n::nat" |> declare_pat "?a::?'a" |> assert_pre_match ("?a", "n") |> assert_pre_match ("?n", "n") |> assert_not_pre_match ("?n", "a") |> assert_not_pre_match ("m", "n") |> done "test_pre_match" val test_pre_match_quant = init |> declare_term "[P::(nat => bool), Q]" |> declare_term "[S::(nat => nat => bool), T]" |> declare_term "[x::nat, y, z]" |> assert_pre_match ("ALL x. P x", "ALL y. P y") |> assert_not_pre_match ("ALL x. P x", "ALL x. Q x") |> assert_pre_match ("ALL x y. S x y", "ALL y z. S y z") |> assert_not_pre_match ("ALL x y. S x y", "ALL x y. S y x") |> assert_not_pre_match ("ALL x y. S x y", "ALL x y. T x y") |> assert_pre_match ("ALL x y. ?S x y", "ALL x y. x < y") |> assert_pre_match ("ALL x. x + y = z & ?P x", "ALL x. x + y = z & P x") |> done "test_pre_match_quant" end diff --git a/thys/Auto2_HOL/HOL/rewrite_test.ML b/thys/Auto2_HOL/HOL/rewrite_test.ML --- a/thys/Auto2_HOL/HOL/rewrite_test.ML +++ b/thys/Auto2_HOL/HOL/rewrite_test.ML @@ -1,406 +1,406 @@ (* File: rewrite_test.ML Author: Bohua Zhan Unit test for rewrite.ML. *) local val init = @{context} fun add_prim_id (prim_id, id) ctxt = let val (prim_id', ctxt') = BoxID.add_prim_id id ctxt val _ = assert (prim_id = prim_id') "add_prim_id" in ctxt' end (* Conversion between (id, th) used in rewrite.ML and (id, t) used in test cases. *) fun to_term_info (id, th) = (id, Util.rhs_of th) (* Comparison of list of box_ids. *) val eq_id_list = eq_set (op =) (* Comparison of list of (box_id, term) pairs. *) val eq_info_list = eq_set (eq_pair (op =) (op aconv)) fun print_term_info ctxt (id, t) = "(" ^ (BoxID.string_of_box_id id) ^ ", " ^ (Syntax.string_of_term ctxt t) ^ ")" fun print_term_infos ctxt lst = commas (map (print_term_info ctxt) lst) val string_of_box_id_list = Util.string_of_list BoxID.string_of_box_id fun done str _ = let val _ = tracing ("Finished " ^ str) in () end (* info is expected, in box_id * term form, info' is returned value, in box_id * thm form (to be printed). *) fun assert_eq_info (info, info') txt ctxt = if eq_info_list (info, map to_term_info info') then ctxt else let val _ = tracing ("Expected: " ^ print_term_infos ctxt info ^ "\n" ^ "Actual: " ^ print_infos ctxt info') in raise Fail txt end fun assert_rew_info str info_str ctxt = let val t = Syntax.read_term ctxt str val ct = Thm.cterm_of ctxt t val info = map (apsnd (Syntax.read_term ctxt)) info_str in assert_eq_info (info, RewriteTable.get_rewrite_info ctxt ct) "assert_rew_info" ctxt end fun assert_srew_info str info_str ctxt = let val t = Syntax.read_term ctxt str val ct = Thm.cterm_of ctxt t val info = map (apsnd (Syntax.read_term ctxt)) info_str in assert_eq_info (info, RewriteTable.get_subterm_rewrite_info ctxt ct) "assert_srew_info" ctxt end fun assert_head_rep (id, str) info_str ctxt = let val t = Syntax.read_term ctxt str val ct = Thm.cterm_of ctxt t val info = map (apsnd (Syntax.read_term ctxt)) info_str val th = Thm.reflexive ct in assert_eq_info (info, RewriteTable.get_head_rep_with_id_th ctxt (id, th)) "assert_head_rep" ctxt end fun assert_equiv_gen exp_equiv id (str1, str2) ctxt = let val (t1, t2) = (Syntax.read_term ctxt str1, Syntax.read_term ctxt str2) in if exp_equiv = RewriteTable.is_equiv_t id ctxt (t1, t2) then ctxt else let val _ = tracing ("id: " ^ (BoxID.string_of_box_id id)) val _ = trace_tlist ctxt "Input:" [t1, t2] in raise Fail (if exp_equiv then "assert_equiv" else "assert_not_equiv") end end val assert_equiv = assert_equiv_gen true val assert_not_equiv = assert_equiv_gen false fun assert_simpl_info str info_str ctxt = let val t = Syntax.read_term ctxt str val ct = Thm.cterm_of ctxt t val info = map (apsnd (Syntax.read_term ctxt)) info_str in assert_eq_info (info, RewriteTable.simplify_info ctxt ct) "assert_simpl_info" ctxt end fun assert_simpl id (str, str') ctxt = let val (t, t') = (Syntax.read_term ctxt str, Syntax.read_term ctxt str') val ct = Thm.cterm_of ctxt t val res = Util.rhs_of (RewriteTable.simplify id ctxt ct) in if res aconv t' then ctxt else let val _ = trace_t ctxt "Input:" t val _ = trace_t ctxt "Expected:" t' val _ = trace_t ctxt "Actual:" res in raise Fail "assert_simpl" end end (* Collect all head equivs under box id. The return value of get_head_equiv is in the form [(head, [((id, th), groups), ...]), ...], and we want to collect the set of (id, th). *) fun assert_head_equivs (id, str) info_str ctxt = let val cu = Thm.cterm_of ctxt (Syntax.read_term ctxt str) val info = map (apsnd (Syntax.read_term ctxt)) info_str val res = (RewriteTable.get_head_equiv ctxt cu) |> BoxID.merge_box_with_info ctxt id in assert_eq_info (info, res) "assert_head_equivs" ctxt end fun index_reps ctxt = let fun index_reps_t t = fold RewriteTable.update_subsimp (RewriteTable.get_subterm_rewrite_info ctxt t) in fold index_reps_t (RewriteTable.get_all_terms ctxt) ctxt end fun declare_term str ctxt = - Variable.auto_fixes (Syntax.read_term ctxt str) ctxt + Proof_Context.augment (Syntax.read_term ctxt str) ctxt (* First part: test internal functions. *) (* Modification functions using terms. *) fun add_equiv id (str1, str2) ctxt = let val (t1, t2) = (Syntax.read_term ctxt str1, Syntax.read_term ctxt str2) val thy = Proof_Context.theory_of ctxt val eq_th = Util.assume_meta_eq thy (t1, t2) in ctxt |> RewriteTable.add_equiv (id, eq_th) end fun add_term str ctxt = ctxt |> RewriteTable.add_term ([], Thm.cterm_of ctxt (Syntax.read_term ctxt str)) |> snd fun assert_eq_edges (str1, str2) ids ctxt = let val (t1, t2) = (Syntax.read_term ctxt str1, Syntax.read_term ctxt str2) val ids' = (RewriteTable.equiv_neighs ctxt t1) |> map to_term_info |> filter (fn (_, t2') => t2 aconv t2') |> map fst in if eq_id_list (ids, ids') then ctxt else let val _ = trace_tlist ctxt "Input:" [t1, t2] val _ = tracing ("Expected: " ^ (string_of_box_id_list ids) ^ "\n" ^ "Actual: " ^ (string_of_box_id_list ids')) in raise Fail "assert_eq_edges" end end fun update_simp id (str1, str2) ctxt = let val (t1, t2) = (Syntax.read_term ctxt str1, Syntax.read_term ctxt str2) val thy = Proof_Context.theory_of ctxt val eq_th = Util.assume_meta_eq thy (t1, t2) in ctxt |> RewriteTable.update_simp (id, eq_th) end fun assert_rewrite id (str, str') ctxt = let val (t, t') = (Syntax.read_term ctxt str, Syntax.read_term ctxt str') val res = Util.rhs_of (RewriteTable.get_rewrite id ctxt (Thm.cterm_of ctxt t)) in if res aconv t' then ctxt else let val _ = trace_t ctxt "Input:" t val _ = trace_t ctxt "Expected:" t' val _ = trace_t ctxt "Actual:" res in raise Fail "assert_rewrite" end end fun add_rewrite id (str1, str2) ctxt = let val (t1, t2) = (Syntax.read_term ctxt str1, Syntax.read_term ctxt str2) val thy = Proof_Context.theory_of ctxt val th = assume_eq thy (t1, t2) in ctxt |> RewriteTable.add_rewrite (id, th) |> snd end in val test_equiv_basic = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1]), (4, [2])] |> declare_term "[a, b, c, d]" |> fold add_term ["a", "b", "c", "d"] |> add_equiv [2] ("a", "b") |> assert_eq_edges ("a", "b") [[2]] |> add_equiv [3] ("b", "c") |> assert_eq_edges ("b", "c") [[3]] |> add_equiv [] ("a", "b") |> assert_eq_edges ("a", "b") [[]] |> add_equiv [4] ("a", "d") |> assert_eq_edges ("a", "d") [[4]] |> add_equiv [3] ("a", "d") |> assert_eq_edges ("a", "d") [[3], [4]] |> add_equiv [2] ("a", "d") |> assert_eq_edges ("a", "d") [[2], [3]] |> add_equiv [] ("a", "d") |> assert_eq_edges ("a", "d") [[]] |> done "test_equiv_basic" val test_simp_basic = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1]), (4, [2])] |> declare_term "[a, b, c, d, e]" |> fold add_term ["a", "b", "c", "d", "e"] |> update_simp [2] ("e", "d") |> assert_rewrite [2, 3] ("e", "d") |> update_simp [3] ("e", "c") |> assert_rewrite [3] ("e", "c") |> update_simp [3] ("e", "b") |> assert_rewrite [2, 3] ("e", "b") |> update_simp [4] ("e", "a") |> assert_rewrite [2, 3] ("e", "b") |> update_simp [2] ("e", "b") |> update_simp [2, 3] ("e", "a") |> assert_rew_info "e" [([], "e"), ([4], "a"), ([3], "b"), ([2], "b"), ([2, 3], "a")] |> done "test_simp_basic" val test_head_rep = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "f a b"] |> add_term "f b d" |> update_simp [2] ("d", "c") |> update_simp [3] ("b", "a") |> assert_srew_info "f b d" [([], "f b d"), ([2], "f b c"), ([3], "f a d"), ([2, 3], "f a c")] |> index_reps |> assert_head_rep ([], "f a c") [([2, 3], "f b d")] |> assert_head_rep ([], "f b c") [([2], "f b d")] |> assert_head_rep ([], "f a d") [([3], "f b d")] |> assert_head_rep ([], "f b d") [([], "f b d")] |> assert_head_rep ([3], "f b c") [([2, 3], "f b d")] |> done "test_head_rep" val test_head_rep3 = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "f a b"] |> add_term "f b c" |> add_term "f a d" |> update_simp [2] ("d", "c") |> update_simp [3] ("b", "a") |> index_reps |> assert_head_rep ([], "f a c") [([2], "f a d"), ([3], "f b c")] |> assert_head_rep ([2], "f a c") [([2], "f a d"), ([2, 3], "f b c")] |> assert_head_rep ([3], "f a c") [([3], "f b c"), ([2, 3], "f a d")] |> done "test_head_rep3" val test_add_term = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "f a b"] |> add_rewrite [2] ("d", "c") |> add_rewrite [3] ("b", "a") |> index_reps |> add_term "f b c" |> add_term "f a d" |> assert_head_rep ([], "f a c") [([2], "f a d"), ([3], "f b c")] |> assert_eq_edges ("f a d", "f b c") [[2, 3]] |> add_term "f a c" |> add_term "f b d" |> assert_head_rep ([], "f a c") [([], "f a c"), ([2], "f a d"), ([3], "f b c"), ([2, 3], "f b d")] |> assert_equiv [2, 3] ("f a c", "f b d") |> assert_not_equiv [2] ("f a c", "f b d") |> assert_not_equiv [3] ("f a c", "f b d") |> done "test_add_term" val test_add_rewrite = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "f a b"] |> add_term "f a d" |> add_rewrite [2] ("d", "c") |> assert_head_rep ([], "f a c") [([2], "f a d")] |> add_term "f b d" |> assert_head_rep ([], "f b c") [([2], "f b d")] |> add_rewrite [3] ("a", "b") |> assert_eq_edges ("f a d", "f b d") [[3]] |> assert_rew_info "f b d" [([], "f b d"), ([2], "f b c"), ([3], "f a d"), ([2, 3], "f a c")] |> add_term "f b c" |> assert_head_rep ([], "f a c") [([2], "f a d"), ([3], "f b c"), ([2, 3], "f b d")] |> done "test_add_rewrite" val test_simplify = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "[f a b, e]"] |> add_rewrite [1] ("f b d", "e") |> add_rewrite [2] ("d", "c") |> add_rewrite [3] ("b", "a") |> assert_simpl_info "f a c" [([], "f a c"), ([2, 3], "e")] |> assert_simpl_info "f a d" [([], "f a d"), ([2], "f a c"), ([3], "e")] |> assert_simpl_info "f b c" [([], "f b c"), ([3], "f a c"), ([2], "e")] |> assert_simpl_info "f b d" [([], "f b d"), ([1], "e")] |> assert_simpl [2] ("f a c", "f a c") |> assert_simpl [2, 3] ("f a c", "e") |> assert_simpl [2] ("f a d", "f a c") |> assert_simpl [3] ("f a d", "e") |> assert_simpl [2, 3] ("f a d", "e") |> add_rewrite [] ("f b d", "e") |> assert_simpl_info "f b d" [([], "e")] |> add_term "f a c" |> assert_equiv [2, 3] ("f a c", "f b d") |> done "test_simplify" val test_simplify2 = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1]), (4, [2])] |> declare_term "[a, b, c, d]" |> add_rewrite [3] ("b", "c") |> add_rewrite [4] ("a", "b") |> add_rewrite [2] ("c", "d") |> assert_simpl_info "c" [([], "c"), ([3], "b"), ([3, 4], "a")] |> assert_simpl_info "d" [([], "d"), ([2], "c"), ([2, 3], "b"), ([3, 4], "a")] |> done "test_simplify2" val test_simplify3 = init |> fold add_prim_id [(1, []), (2, [1])] |> declare_term "[a, b, c, d, e, g]" |> add_rewrite [1] ("e", "c") |> add_rewrite [1] ("g", "d") |> add_rewrite [2] ("e", "b") |> add_rewrite [2] ("g", "a") |> add_rewrite [] ("e", "g") |> assert_simpl_info "e" [([], "e"), ([1], "c"), ([2], "a")] |> assert_simpl_info "g" [([], "e"), ([1], "c"), ([2], "a")] |> done "test_simplify3" val test_head_equivs = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "[f a b, e]"] |> add_rewrite [1] ("f b d", "e") |> add_rewrite [2] ("d", "c") |> add_rewrite [3] ("b", "a") |> assert_head_equivs ([], "c") [([], "c"), ([2], "d")] |> assert_head_equivs ([], "f b d") [([], "f b d"), ([1], "e")] |> assert_head_equivs ([2], "f b c") [([2], "f b c"), ([2], "e"), ([2], "f b d")] |> assert_head_equivs ([], "f b c") [([], "f b c"), ([2], "e"), ([2], "f b d")] |> assert_head_equivs ([], "f a c") [([], "f a c"), ([2, 3], "e"), ([2, 3], "f b d")] |> add_term "f a c" |> assert_head_equivs ([], "f b d") [([], "f b d"), ([1], "e"), ([2, 3], "f a c")] |> assert_head_equivs ([], "f a c") [([], "f a c"), ([2, 3], "e"), ([2, 3], "f b d")] |> assert_head_equivs ([], "f b c") [([], "f b c"), ([2], "e"), ([2], "f b d"), ([3], "f a c")] |> done "test_head_equivs" val test_head_equivs2 = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1]), (4, [2])] |> declare_term "[a, b, c, d]" |> add_rewrite [3] ("b", "c") |> add_rewrite [4] ("a", "b") |> assert_head_equivs ([], "b") [([], "b"), ([3], "c"), ([4], "a")] |> add_rewrite [2] ("c", "d") |> assert_head_equivs ([], "b") [([], "b"), ([3], "c"), ([4], "a"), ([2, 3], "d")] |> done "test_head_equivs2" val test_head_equivs3 = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "[f a b, e]"] |> add_rewrite [] ("b", "a") |> add_rewrite [2] ("f b d", "e") |> add_rewrite [3] ("f a d", "e") (* Both fbd and fad are ok in the result. *) |> assert_head_equivs ([], "f a d") [([], "f b d"), ([2], "e"), ([3], "e"), ([], "f a d")] |> assert_head_equivs ([], "f b d") [([], "f a d"), ([2], "e"), ([3], "e"), ([], "f b d")] |> done "test_head_equivs3" val test_head_equivs4 = init |> fold add_prim_id [(1, []), (2, [1]), (3, [1])] |> fold declare_term ["[a, b, c, d]", "[f a b, e]"] |> add_rewrite [2] ("b", "a") |> add_rewrite [] ("f b c", "e") |> add_rewrite [3] ("f a c", "e") (* Note fbc ~ fac under 3. *) |> assert_head_equivs ([], "f b c") [([], "f b c"), ([], "e"), ([3], "f a c"), ([2], "f a c")] |> assert_head_equivs ([], "f a c") [([], "f a c"), ([2], "e"), ([3], "e"), ([3], "f b c"), ([2], "f b c")] |> done "test_head_equivs4" (* Simplify with nat variables. *) val test_simplify_nat = init |> declare_term "[a::nat, b, c]" |> add_rewrite [] ("a + b", "b + a") |> add_rewrite [] ("a", "c") |> assert_simpl [] ("b + c", "a + b") |> assert_equiv [] ("b + c", "a + b") |> done "test_simplify_nat" end; (* local *) diff --git a/thys/Auto2_Imperative_HOL/Imperative/list_matcher_test.ML b/thys/Auto2_Imperative_HOL/Imperative/list_matcher_test.ML --- a/thys/Auto2_Imperative_HOL/Imperative/list_matcher_test.ML +++ b/thys/Auto2_Imperative_HOL/Imperative/list_matcher_test.ML @@ -1,106 +1,106 @@ (* File: list_matcher_test.ML Author: Bohua Zhan Unit test for matching of assertions on linked lists. *) local open SepUtil val ctxt = @{context} fun eq_info_list (l1, l2) = length l1 = length l2 andalso eq_set (eq_pair (op =) (op aconv)) (l1, l2) fun print_term_info ctxt (id, t) = "(" ^ (BoxID.string_of_box_id id) ^ ", " ^ (Syntax.string_of_term ctxt t) ^ ")" fun print_term_infos ctxt lst = commas (map (print_term_info ctxt) lst) fun add_rewrite id (str1, str2) ctxt = let val (t1, t2) = (Syntax.read_term ctxt str1, Syntax.read_term ctxt str2) val thy = Proof_Context.theory_of ctxt val th = assume_eq thy (t1, t2) in ctxt |> RewriteTable.add_rewrite (id, th) end val ts = [@{term "[p::nat node ref option, n1, s1, s2]"}, @{term "[pp::nat node ref, pp']"}, @{term "[x::nat]"}, @{term "[xs::nat list, ys, zs]"}] - val ctxt' = ctxt |> fold Variable.auto_fixes ts + val ctxt' = ctxt |> fold Proof_Context.augment ts |> RewriteTable.add_term ([], Thm.cterm_of ctxt (Free ("P", assnT))) |> snd |> add_rewrite [] ("n1", "None::nat node ref option") |> snd |> add_rewrite [] ("s1", "Some pp") |> snd |> add_rewrite [] ("s2", "Some pp'") |> snd |> add_rewrite [] ("zs", "x # xs") |> snd in fun test test_fun str (pat_str, t_str, info_str) = let val pat = Proof_Context.read_term_pattern ctxt' pat_str val t = Syntax.read_term ctxt' t_str val ct = Thm.cterm_of ctxt t val info = map (apsnd (Syntax.read_term ctxt')) info_str val info' = (test_fun ctxt' (pat, ct) ([], fo_init)) |> map (apsnd prop_of') val infol = info' |> map snd |> map dest_arg1 val infor = info' |> map (fn ((id, _), t) => (id, dest_arg t)) in if forall (fn t' => t' aconv t) infol andalso eq_info_list (info, infor) then () else let val _ = tracing ("Expected: " ^ print_term_infos ctxt' info) val _ = tracing ("Actual: " ^ print_term_infos ctxt' infor) in raise Fail str end end val test_assn_term_matcher = let val test_data = [ ("os_list ?xs n1", "emp", [([], "os_list [] n1 * emp")]), ("os_list ?xs n1", "sngr_assn a 1", [([], "os_list [] n1 * sngr_assn a 1")]), ("os_list ?xs s1", "sngr_assn pp (Node x r) * os_list xs r", [([], "os_list (x # xs) s1 * emp")]), ("os_list (?x # ?xs) s1", "sngr_assn pp (Node x r) * os_list xs r", [([], "os_list (x # xs) s1 * emp")]), ("os_list ys s1", "sngr_assn pp (Node x r) * os_list xs r", []), ("os_list zs s1", "sngr_assn pp (Node x r) * os_list xs r", [([], "os_list zs s1 * emp")]), ("os_list zs s1", "sngr_assn pp (Node x r) * os_list xs r * os_list ys p", [([], "os_list zs s1 * os_list ys p")]) ] in map (test AssnMatcher.assn_match_term "test_assn_term_matcher") test_data end val test_list_prop_matcher = let val test_data = [ ("os_list ?xs s1", "sngr_assn pp (Node x r) * os_list xs r", [([], "os_list (x # xs) s1")]), ("os_list zs s1", "sngr_assn pp (Node x r) * os_list xs r", [([], "os_list zs s1")]), ("os_list ?xs p * os_list ?ys q", "os_list ys q * os_list xs p", [([], "os_list xs p * os_list ys q")]), ("os_list ?xs p", "os_list xs p * os_list ys q", []), ("sngr_assn a 1", "sngr_assn a 1", [([], "sngr_assn a 1")]), ("sngr_assn ?a 1 * os_list ?ys q * os_list ?zs r", "os_list ys q * os_list zs r * sngr_assn a 1", [([], "sngr_assn a 1 * os_list ys q * os_list zs r")]) ] in map (test AssnMatcher.assn_match_strict "test_list_prop_matcher") test_data end end diff --git a/thys/Auto2_Imperative_HOL/Imperative/sep_steps_test.ML b/thys/Auto2_Imperative_HOL/Imperative/sep_steps_test.ML --- a/thys/Auto2_Imperative_HOL/Imperative/sep_steps_test.ML +++ b/thys/Auto2_Imperative_HOL/Imperative/sep_steps_test.ML @@ -1,87 +1,87 @@ (* File: sep_steps_test.ML Author: Bohua Zhan Unit test for sep_steps.ML. *) local open SepUtil val ctxt = @{context} - val ctxt' = ctxt |> fold Variable.auto_fixes [ + val ctxt' = ctxt |> fold Proof_Context.augment [ Free ("P", assnT), Free ("Q", assnT), Free ("R", assnT), Free ("S", natT --> assnT), Free ("T", natT --> assnT)] in val test_normalize_assn = let val test_data = [ ("P * (Q * R)", "P * Q * R"), ("P * \(b)", "P * \(b)"), ("\(b) * P", "P * \(b)"), ("P * \(b) * Q", "P * Q * \(b)"), ("\(b) * (P * \(c)) * Q", "P * Q * \(b) * \(c)"), ("EXA x. S x", "EXA x. S x"), ("(EXA x. S x) * P", "EXA x. P * S x"), ("P * (EXA x. S x)", "EXA x. P * S x"), ("(EXA x. S x) * (EXA y. T y)", "EXA x y. S x * T y"), ("EXA x. S x * \(B x) * T x", "EXA x. S x * T x * \(B x)"), ("P * true * true", "P * true"), ("true * P * true", "P * true"), ("true * P * true * \(b)", "P * true * \(b)"), ("(EXA x. S x) * P * Q", "EXA x. P * Q * S x"), ("\(b1 & b2)", "\b1 * \b2") ] in map (Util.test_conv ctxt' (SepUtil.normalize_assn_cv ctxt') "normalize_assn") test_data end val test_contract_hoare = let val test_data = [ ("

(b)> c ", "

(b)> c "), ("b -->

c ", "

(b)> c "), ("b1 --> b2 -->

c ", "

(b2) * \(b1)> c "), ("b1 -->

(b2)> c ", "

(b2) * \(b1)> c "), (" c ", "

c ") ] in map (Util.test_conv ctxt' (SepLogic.contract_hoare_cv ctxt') "contract_hoare") test_data end val test_normalize_hoare_goal = let val test_data = [ ("~

c ", "~

c "), ("~<\(b)> c ", "~ c & b"), ("~

(b)> c ", "~

c & b"), ("~<\(b1) * \(b2)> c ", "(~ c & b1) & b2"), ("~

c ", "~

c "), ("EX x. ~ c ", "EX x. ~ c "), ("EX x. ~<\(b x)> c ", "EX x. ~ c & b x") ] in map (Util.test_conv ctxt' (SepLogic.normalize_hoare_goal_cv ctxt') "normalize_hoare_goal") test_data end val test_normalize_entail_goal = let val test_data = [ ("~(entails P Q)", "~(entails P Q)"), ("~(entails (\b) Q)", "~(entails emp Q) & b"), ("~(entails (\b * P) Q)", "~(entails P Q) & b"), ("~(entails (EXA x. S x) Q)", "EX x. ~(entails (S x) Q)") ] in map (Util.test_conv ctxt' (SepLogic.normalize_entail_goal_cv ctxt') "normalize_entail_goal") test_data end end diff --git a/thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy b/thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy --- a/thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy +++ b/thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy @@ -1,984 +1,984 @@ section \Relator Fixing\ theory Autoref_Fix_Rel imports Autoref_Id_Ops begin ML_val "2 upto 5" subsubsection \Priority tags\ text \ Priority tags are used to influence the ordering of refinement theorems. A priority tag defines two numeric priorities, a major and a minor priority. The major priority is considered first, the minor priority last, i.e., after the homogenity and relator-priority criteria. The default value for both priorities is 0. \ definition PRIO_TAG :: "int \ int \ bool" where [simp]: "PRIO_TAG ma mi \ True" lemma PRIO_TAGI: "PRIO_TAG ma mi" by simp abbreviation "MAJOR_PRIO_TAG i \ PRIO_TAG i 0" abbreviation "MINOR_PRIO_TAG i \ PRIO_TAG 0 i" abbreviation "DFLT_PRIO_TAG \ PRIO_TAG 0 0" text \Some standard tags\ abbreviation "PRIO_TAG_OPTIMIZATION \ MINOR_PRIO_TAG 10" \ \Optimized version of an algorithm, with additional side-conditions\ abbreviation "PRIO_TAG_GEN_ALGO \ MINOR_PRIO_TAG (- 10)" \ \Generic algorithm, considered to be less efficient than default algorithm\ subsection \Solving Relator Constraints\ text \ In this phase, we try to instantiate the annotated relators, using the available refinement rules. \ definition CONSTRAINT :: "'a \ ('c\'a) set \ bool" where [simp]: "CONSTRAINT f R \ True" lemma CONSTRAINTI: "CONSTRAINT f R" by auto ML \ structure Autoref_Rules = Named_Thms ( val name = @{binding autoref_rules_raw} val description = "Refinement Framework: " ^ "Automatic refinement rules" ); \ setup Autoref_Rules.setup text \Generic algorithm tags have to be defined here, as we need them for relator fixing !\ definition PREFER_tag :: "bool \ bool" where [simp, autoref_tag_defs]: "PREFER_tag x \ x" definition DEFER_tag :: "bool \ bool" where [simp, autoref_tag_defs]: "DEFER_tag x \ x" lemma PREFER_tagI: "P \ PREFER_tag P" by simp lemma DEFER_tagI: "P \ DEFER_tag P" by simp lemmas SIDEI = PREFER_tagI DEFER_tagI definition [simp, autoref_tag_defs]: "GEN_OP_tag P == P" lemma GEN_OP_tagI: "P ==> GEN_OP_tag P" by simp abbreviation "SIDE_GEN_OP P == PREFER_tag (GEN_OP_tag P)" text \Shortcut for assuming an operation in a generic algorithm lemma\ abbreviation "GEN_OP c a R \ SIDE_GEN_OP ((c,OP a ::: R) \ R)" definition TYREL :: "('a\'b) set \ bool" where [simp]: "TYREL R \ True" definition TYREL_DOMAIN :: "'a itself \ bool" where [simp]: "TYREL_DOMAIN i \ True" lemma TYREL_RES: "\ TYREL_DOMAIN TYPE('a); TYREL (R::(_\'a) set) \ \ TYREL R" . lemma DOMAIN_OF_TYREL: "TYREL (R::(_\'a) set) \ TYREL_DOMAIN TYPE('a)" by simp lemma TYRELI: "TYREL (R::(_\'a) set)" by simp lemma ty_REL: "TYREL (R::(_\'a) set)" by simp ML \ signature AUTOREF_FIX_REL = sig type constraint = (term * term) list * (term * term) type thm_pairs = (constraint option * thm) list type hom_net = (int * thm) Net.net val thm_pairsD_init: Proof.context -> Proof.context val thm_pairsD_get: Proof.context -> thm_pairs val constraints_of_term: term -> (term * term) list val constraints_of_goal: int -> thm -> (term * term) list val mk_CONSTRAINT: term * term -> term val mk_CONSTRAINT_rl: Proof.context -> constraint -> thm val insert_CONSTRAINTS_tac: Proof.context -> tactic' val constraint_of_thm: Proof.context -> thm -> constraint datatype prio_relpos = PR_FIRST | PR_LAST | PR_BEFORE of string | PR_AFTER of string val declare_prio: string -> term -> prio_relpos -> local_theory -> local_theory val delete_prio: string -> local_theory -> local_theory val print_prios: Proof.context -> unit val compute_hom_net: thm_pairs -> Proof.context -> hom_net val add_hom_rule: thm -> Context.generic -> Context.generic val del_hom_rule: thm -> Context.generic -> Context.generic val get_hom_rules: Proof.context -> thm list val add_tyrel_rule: thm -> Context.generic -> Context.generic val del_tyrel_rule: thm -> Context.generic -> Context.generic val get_tyrel_rules: Proof.context -> thm list val insert_tyrel_tac : Proof.context -> int -> int -> tactic' val solve_tyrel_tac : Proof.context -> tactic' val tyrel_tac : Proof.context -> itactic val internal_hom_tac: Proof.context -> itactic val internal_spec_tac: Proof.context -> itactic val internal_solve_tac: Proof.context -> itactic val guess_relators_tac: Proof.context -> itactic val pretty_constraint: Proof.context -> constraint -> Pretty.T val pretty_constraints: Proof.context -> constraint list -> Pretty.T val pretty_thm_pair: Proof.context -> (constraint option * thm) -> Pretty.T val pretty_thm_pairs: Proof.context -> thm_pairs -> Pretty.T val analyze: Proof.context -> int -> int -> thm -> bool val pretty_failure: Proof.context -> int -> int -> thm -> Pretty.T val try_solve_tac: Proof.context -> tactic' val solve_step_tac: Proof.context -> tactic' val phase: Autoref_Phases.phase val setup: theory -> theory end structure Autoref_Fix_Rel :AUTOREF_FIX_REL = struct type constraint = (term * term) list * (term * term) type thm_pairs = (constraint option * thm) list type hom_net = (int * thm) Net.net (*********************) (* Constraints *) (*********************) local fun fix_loose_bvars env t = if Term.is_open t then let val frees = tag_list 0 env |> map (fn (i,(n,T)) => Free (":"^string_of_int i ^ "_" ^ n,T)) in subst_bounds (frees, t) end else t fun constraints env @{mpat "OP ?f ::: ?R"} = ( Term.is_open R andalso raise TERM ("Loose bvar in relator",[R]); [(fix_loose_bvars env f,R)] ) | constraints _ (Free _) = [] | constraints _ (Bound _) = [] | constraints env @{mpat "?f ::: _"} = constraints env f | constraints env @{mpat "?f$?x"} = constraints env x @ constraints env f | constraints env @{mpat "PROTECT (\x. PROTECT ?t)"} = constraints ((x,x_T)::env) t | constraints _ @{mpat "PROTECT PROTECT"} = [] | constraints _ t = raise TERM ("constraints_of_term",[t]) in val constraints_of_term = constraints [] end fun constraints_of_goal i st = case Logic.concl_of_goal (Thm.prop_of st) i of @{mpat "Trueprop ((_,?a)\_)"} => constraints_of_term a | _ => raise THM ("constraints_of_goal",i,[st]) fun mk_CONSTRAINT (f,R) = let val fT = fastype_of f val RT = fastype_of R val res = Const (@{const_name CONSTRAINT},fT --> RT --> HOLogic.boolT) $f$R in res end; (* Types of f and R must match! *) fun mk_CONSTRAINT_rl ctxt (ps,c) = let val ps = map (mk_CONSTRAINT #> HOLogic.mk_Trueprop) ps val c = mk_CONSTRAINT c |> HOLogic.mk_Trueprop val g = Logic.list_implies (ps,c) in Goal.prove ctxt [] [] g (K (resolve_tac ctxt @{thms CONSTRAINTI} 1)) end; (* Internal use for hom-patterns, f and R are unified *) fun mk_CONSTRAINT_rl_atom ctxt (f,R) = let val ts = map (SOME o Thm.cterm_of ctxt) [f,R] val idx = Term.maxidx_term f (Term.maxidx_of_term R) + 1 in infer_instantiate' ctxt ts (Thm.incr_indexes idx @{thm CONSTRAINTI}) end; fun insert_CONSTRAINTS_tac ctxt i st = let val cs = constraints_of_goal i st |> map (mk_CONSTRAINT #> HOLogic.mk_Trueprop #> Thm.cterm_of ctxt) in Refine_Util.insert_subgoals_tac cs i st end fun constraint_of_thm ctxt thm = let exception NO_REL of term open Autoref_Tagging fun extract_entry t = case Logic.strip_imp_concl (strip_all_body t) of @{mpat "Trueprop ((_,?f)\_)"} => SOME (fst (strip_app f),t) | _ => NONE fun relator_of t = let (*val _ = tracing (Syntax.string_of_term @{context} t)*) val t = strip_all_body t val prems = Logic.strip_imp_prems t val concl = Logic.strip_imp_concl t in case concl of @{mpat "Trueprop ((_,?t)\?R)"} => let val (f,args) = strip_app t in case f of @{mpat "OP ?f:::?rel"} => (f,rel) | _ => let val rels = map_filter extract_entry prems fun find_rel t = case filter (fn (t',_) => t=t') rels of [(_,t)] => snd (relator_of t) | _ => raise NO_REL t val argrels = map find_rel args val rel = fold Relators.mk_fun_rel (rev argrels) R in (f,rel) end end | _ => raise THM ("constraint_of_thm: Invalid concl",~1,[thm]) end val (f,rel) = relator_of (Thm.prop_of thm) handle exc as (NO_REL t) => ( warning ( "Could not infer unique higher-order relator for " ^ "refinement rule: \n" ^ Thm.string_of_thm ctxt thm ^ "\n for argument: " ^ Syntax.string_of_term ctxt t ); Exn.reraise exc) (* Extract GEN_OP-tags *) fun genop_cs @{mpat "Trueprop (SIDE_GEN_OP ((_,OP ?f ::: _) \ ?R))"} = if has_Var f then NONE else SOME (f,R) | genop_cs _ = NONE val gen_ops = Thm.prems_of thm |> map_filter genop_cs in (gen_ops,(f,rel)) end (*********************) (* Priorities *) (*********************) structure Rel_Prio_List = Prio_List ( type item = string * term val eq = (op =) o apply2 fst ) structure Rel_Prio = Generic_Data ( type T = Rel_Prio_List.T val empty = Rel_Prio_List.empty val merge = Rel_Prio_List.merge val extend = I ) fun pretty_rel_prio ctxt (s,t) = Pretty.block [ Pretty.str s, Pretty.str ":", Pretty.brk 1, Syntax.pretty_term ctxt t ] fun print_prios ctxt = let val rpl = Rel_Prio.get (Context.Proof ctxt) in (map (pretty_rel_prio ctxt) rpl) |> Pretty.big_list "Relator Priorities" |> Pretty.string_of |> warning end datatype prio_relpos = PR_FIRST | PR_LAST | PR_BEFORE of string | PR_AFTER of string fun declare_prio name pat0 relpos lthy = let val pat1 = Proof_Context.cert_term lthy pat0 - val pat2 = singleton (Variable.export_terms (Variable.auto_fixes pat1 lthy) lthy) pat1 + val pat2 = singleton (Variable.export_terms (Proof_Context.augment pat1 lthy) lthy) pat1 in lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => let val item = (name, Morphism.term phi pat2) in Rel_Prio.map (fn rpl => case relpos of PR_FIRST => Rel_Prio_List.add_first rpl item | PR_LAST => Rel_Prio_List.add_last rpl item | PR_BEFORE n => Rel_Prio_List.add_before rpl item (n,Term.dummy) | PR_AFTER n => Rel_Prio_List.add_after rpl item (n,Term.dummy) ) end) end fun delete_prio name = Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => Rel_Prio.map (Rel_Prio_List.delete (name, Term.dummy))) local fun relators_of R = let fun f @{mpat "?R1.0\?R2.0"} = f R1 @ f R2 | f R = [R] in f R |> map Refine_Util.anorm_term |> distinct (op =) end fun dest_prio_tag @{mpat "Trueprop (PRIO_TAG ?ma ?mi)"} = apply2 (#2 o HOLogic.dest_number) (ma,mi) | dest_prio_tag t = raise TERM ("dest_prio_tag",[t]) fun get_tagged_prios thm = let val prems = Thm.prems_of thm fun r [] = (0,0) | r (prem::prems) = ( case try dest_prio_tag prem of NONE => r prems | SOME p => p ) in r prems end fun prio_order_of ctxt (SOME (_,(_,R)),thm) = let val rels = relators_of R val hom = length rels val (major_prio,minor_prio) = get_tagged_prios thm val rpl = Rel_Prio.get (Context.Proof ctxt) val matches = Pattern.matches (Proof_Context.theory_of ctxt) fun prefer ((_,p1),(_,p2)) = matches (p2,p1) fun prio_of R = Rel_Prio_List.prio_of (fn (_,pat) => matches (pat,R)) prefer rpl + 1 val prio = fold (fn R => fn s => prio_of R + s) rels 0 in (major_prio, (hom,(prio,minor_prio))) end | prio_order_of _ _ = raise Match val prio_order = prod_ord (rev_order o int_ord) (prod_ord int_ord (prod_ord (rev_order o int_ord) (rev_order o int_ord))) fun annotate_thm_pair ctxt (SOME (ps,(f,R)),thm) = let open Autoref_Tagging Conv fun warn () = warning ("Error annotating refinement theorem: " ^ Thm.string_of_thm ctxt thm ) val R_cert = Thm.cterm_of ctxt R fun cnv ctxt ct = (case Thm.term_of ct of @{mpat "OP _ ::: _"} => all_conv | @{mpat "OP _"} => mk_rel_ANNOT_conv ctxt R_cert | @{mpat "_ $ _"} => arg1_conv (cnv ctxt) | _ => mk_OP_conv then_conv mk_rel_ANNOT_conv ctxt R_cert ) ct (*val _ = tracing ("ANNOT: " ^ @{make_string} thm)*) val thm = (fconv_rule (rhs_conv cnv ctxt)) thm val thm = case try (fconv_rule (rhs_conv cnv ctxt)) thm of NONE => (warn (); thm) | SOME thm => thm (*val _ = tracing ("RES: " ^ @{make_string} thm)*) in (SOME (ps,(f,R)),thm) end | annotate_thm_pair _ p = p in fun compute_thm_pairs ctxt = let val rules = Autoref_Rules.get ctxt fun add_o p = (prio_order_of ctxt p,p) val pairs = rules |> map (fn thm => (try (constraint_of_thm ctxt) thm,thm)) val spairs = filter (is_some o #1) pairs |> map add_o |> sort (prio_order o apply2 #1) |> map #2 val npairs = filter (is_none o #1) pairs in spairs@npairs |> map (annotate_thm_pair ctxt) end end structure thm_pairsD = Autoref_Data ( type T = thm_pairs val compute = compute_thm_pairs val prereq = [] ) val thm_pairsD_init = thm_pairsD.init val thm_pairsD_get = thm_pairsD.get structure hom_rules = Named_Sorted_Thms ( val name = @{binding autoref_hom} val description = "Autoref: Homogenity rules" val sort = K I val transform = K ( fn thm => case Thm.concl_of thm of @{mpat "Trueprop (CONSTRAINT _ _)"} => [thm] | _ => raise THM ("Invalid homogenity rule",~1,[thm]) ) ) val add_hom_rule = hom_rules.add_thm val del_hom_rule = hom_rules.del_thm val get_hom_rules = hom_rules.get local open Relators fun repl @{mpat "?R\?S"} ctab = let val (R,ctab) = repl R ctab val (S,ctab) = repl S ctab in (mk_fun_rel R S,ctab) end | repl R ctab = let val (args,R) = strip_relAPP R val (args,ctab) = fold_map repl args ctab val (ctxt,tab) = ctab val (R,(ctxt,tab)) = case Termtab.lookup tab R of SOME R => (R,(ctxt,tab)) | NONE => let val aT = fastype_of R |> strip_type |> #2 |> HOLogic.dest_setT |> HOLogic.dest_prodT |> #2 val (cT,ctxt) = yield_singleton Variable.invent_types @{sort type} ctxt val cT = TFree cT val T = map fastype_of args ---> HOLogic.mk_setT (HOLogic.mk_prodT (cT,aT)) val (R',ctxt) = yield_singleton Variable.variant_fixes "R" ctxt val R' = list_relAPP args (Free (R',T)) val tab = Termtab.update (R,R') tab in (R',(ctxt,tab)) end in (R,(ctxt,tab)) end fun hom_pat_of_rel ctxt R = let val (R,(ctxt',_)) = repl R (ctxt,Termtab.empty) val R = singleton (Variable.export_terms ctxt' ctxt) R in Refine_Util.anorm_term R end in fun compute_hom_net pairs ctxt = let val cs = map_filter #1 pairs val cs' = map (fn (_,(f,R)) => (f,hom_pat_of_rel ctxt R)) cs val thms = get_hom_rules ctxt @ map (mk_CONSTRAINT_rl_atom ctxt) cs' val thms = map (Thm.cprop_of #> Thm.trivial) thms val net = Tactic.build_net thms in net end end structure hom_netD = Autoref_Data ( type T = hom_net fun compute ctxt = compute_hom_net (thm_pairsD.get ctxt) ctxt val prereq = [ thm_pairsD.init ] ) structure tyrel_rules = Named_Sorted_Thms ( val name = @{binding autoref_tyrel} val description = "Autoref: Type-based relator fixing rules" val sort = K I val transform = K ( fn thm => case Thm.prop_of thm of @{mpat "Trueprop (TYREL _)"} => [thm] | _ => raise THM ("Invalid tyrel-rule",~1,[thm]) ) ) val add_tyrel_rule = tyrel_rules.add_thm val del_tyrel_rule = tyrel_rules.del_thm val get_tyrel_rules = tyrel_rules.get local (*fun rel_annots @{mpat "_ ::: ?R"} = [R] | rel_annots @{mpat "?f$?x"} = rel_annots f @ rel_annots x | rel_annots @{mpat "PROTECT (\_. PROTECT ?t)"} = rel_annots t | rel_annots @{mpat "PROTECT PROTECT"} = [] | rel_annots (Free _) = [] | rel_annots (Bound _) = [] | rel_annots t = raise TERM ("rel_annots",[t]) *) fun add_relators t acc = let open Relators val (args,_) = strip_relAPP t val res = fold add_relators args acc val res = insert (op =) t res in res end fun add_relators_of_subgoal st i acc = case Logic.concl_of_goal (Thm.prop_of st) i of @{mpat "Trueprop (CONSTRAINT _ ?R)"} => add_relators R acc | _ => acc in fun insert_tyrel_tac ctxt i j k st = let fun get_constraint t = let val T = fastype_of t val res = Const (@{const_name TYREL}, T --> HOLogic.boolT) $ t in res |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt end val relators = fold (add_relators_of_subgoal st) (i upto j) [] val tyrels = map get_constraint relators in Refine_Util.insert_subgoals_tac tyrels k st end end fun solve_tyrel_tac ctxt = let fun mk_tac rl = resolve_tac ctxt @{thms TYREL_RES} THEN' match_tac ctxt [rl RS @{thm DOMAIN_OF_TYREL}] THEN' resolve_tac ctxt [rl] val tac = FIRST' (map mk_tac (tyrel_rules.get ctxt)) in DETERM o tac ORELSE' (TRY o resolve_tac ctxt @{thms TYRELI}) end fun tyrel_tac ctxt i j = (insert_tyrel_tac ctxt i j THEN_ALL_NEW_FWD solve_tyrel_tac ctxt) i fun internal_hom_tac ctxt = let val hom_net = hom_netD.get ctxt in Seq.INTERVAL (TRY o DETERM o resolve_from_net_tac ctxt hom_net) end fun internal_spec_tac ctxt = let val pairs = thm_pairsD.get ctxt val net = pairs |> map_filter (fst #> map_option (snd #> mk_CONSTRAINT_rl_atom ctxt)) |> Tactic.build_net in fn i => fn j => REPEAT (CHANGED (Seq.INTERVAL (DETERM o Anti_Unification.specialize_net_tac ctxt net) i j) ) end fun apply_to_constraints tac = let fun no_CONSTRAINT_tac i st = case Logic.concl_of_goal (Thm.prop_of st) i of @{mpat "Trueprop (CONSTRAINT _ _)"} => Seq.empty | _ => Seq.single st in Seq.INTERVAL (no_CONSTRAINT_tac ORELSE' tac) end fun internal_solve_tac ctxt = let val pairs = thm_pairsD.get ctxt val net = pairs |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt)) |> Tactic.build_net val s_tac = SOLVED' (REPEAT_ALL_NEW (resolve_from_net_tac ctxt net)) in apply_to_constraints s_tac ORELSE_INTERVAL apply_to_constraints (TRY o DETERM o s_tac) end fun guess_relators_tac ctxt = let val pairs = thm_pairsD.get ctxt val net = pairs |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt)) |> Tactic.build_net val hom_net = hom_netD.get ctxt fun hom_tac i j = Seq.INTERVAL (TRY o DETERM o resolve_from_net_tac ctxt hom_net) i j fun spec_tac i j = REPEAT (CHANGED (Seq.INTERVAL (DETERM o Anti_Unification.specialize_net_tac ctxt net) i j) ) val solve_tac = let val s_tac = SOLVED' (REPEAT_ALL_NEW (resolve_from_net_tac ctxt net)) in apply_to_constraints s_tac ORELSE_INTERVAL apply_to_constraints (TRY o DETERM o s_tac) end in Seq.INTERVAL (insert_CONSTRAINTS_tac ctxt) THEN_INTERVAL hom_tac THEN_INTERVAL spec_tac THEN_INTERVAL (tyrel_tac ctxt) THEN_INTERVAL solve_tac end (*********************) (* Pretty Printing *) (*********************) fun pretty_constraint_atom ctxt (f,R) = Pretty.block [ Syntax.pretty_term ctxt f, Pretty.str " :: ", Syntax.pretty_typ ctxt (fastype_of f), Pretty.str " ::: ", Syntax.pretty_term ctxt R] fun pretty_constraint ctxt (ps,(f,R)) = case ps of [] => pretty_constraint_atom ctxt (f,R) | _ => Pretty.block [ map (pretty_constraint_atom ctxt) ps |> Pretty.separate "; " |> Pretty.enclose "\" "\", Pretty.brk 1, Pretty.str "\", Pretty.brk 1, pretty_constraint_atom ctxt (f,R) ] fun pretty_constraints ctxt l = Pretty.big_list "Constraints" (map (pretty_constraint ctxt) l) fun pretty_thm_pair ctxt (c,thm) = Pretty.block [ case c of NONE => Pretty.str "NONE" | SOME c => pretty_constraint ctxt c, Pretty.brk 2, Pretty.str "---", Pretty.brk 2, Thm.pretty_thm ctxt thm ] fun pretty_thm_pairs ctxt pairs = Pretty.big_list "Thm-Pairs" (map (pretty_thm_pair ctxt) pairs) local fun unifies ctxt (t1, t2) = Term.could_unify (t1, t2) andalso let val idx1 = Term.maxidx_of_term t1 val t2 = Logic.incr_indexes ([], [], idx1 + 1) t2 val idx2 = Term.maxidx_of_term t2 in can (Pattern.unify (Context.Proof ctxt) (t1,t2)) (Envir.empty idx2) end fun analyze_possible_problems ctxt (f,R) = let fun strange_aux sf R = ( if sf then let val T = fastype_of R in case try (HOLogic.dest_prodT o HOLogic.dest_setT) T of SOME _ => [] | NONE => [Pretty.block [ Pretty.str "Strange relator type, expected plain relation: ", Syntax.pretty_term (Config.put show_types true ctxt) R ]] end else [] ) @ ( case R of @{mpat "\?R\?S"} => strange_aux true R @ strange_aux false S | Var (_,T) => ( case try (HOLogic.dest_prodT o HOLogic.dest_setT) (#2 (strip_type T)) of SOME (TFree _,_) => [Pretty.block [ Pretty.str "Fixed concrete type on schematic relator: ", Syntax.pretty_term (Config.put show_types true ctxt) R ]] | _ => [] ) | _ => [] ) val strange = case strange_aux true R of [] => NONE | l => SOME (Pretty.block l) val folded_relator = let fun match (Type (name,args)) R = let val (Rargs,Rhd) = Relators.strip_relAPP R in if is_Var Rhd then [] else if length args <> length Rargs then [Pretty.block [ Pretty.str "Type/relator arity mismatch:", Pretty.brk 1, Pretty.block [ Pretty.str name, Pretty.str "/", Pretty.str (string_of_int (length args)) ], Pretty.brk 1,Pretty.str "vs.",Pretty.brk 1, Pretty.block [ Syntax.pretty_term ctxt Rhd, Pretty.str "/", Pretty.str (string_of_int (length Rargs)) ] ]] else args ~~ Rargs |> map (uncurry match) |> flat end | match _ _ = [] in case match (fastype_of f) R of [] => NONE | l => SOME (Pretty.block (Pretty.fbreaks l @ [Pretty.fbrk, Pretty.str ("Explanation: This may be due to using polymorphic " ^ "relators like Id on non-terminal types." ^ "A problem usually occurs when " ^ "this relator has to be matched against a fully unfolded one." ^ "This warning is also issued on partially parametric relators " ^ "like br. However, the refinement rules are usually set up to " ^ "compensate for this, so this is probably not the cause for an " ^ "unsolved constraint") ])) end val issues = [strange, folded_relator] |> map_filter I in case issues of [] => NONE | l => SOME (Pretty.big_list "Possible problems" l) end fun pretty_try_candidates ctxt i st = if i > Thm.nprems_of st then Pretty.str "Goal number out of range" else case Logic.concl_of_goal (Thm.prop_of st) i of @{mpat "Trueprop (CONSTRAINT ?f ?R)"} => let val pairs = thm_pairsD.get ctxt val st = Drule.zero_var_indexes st val pt_hd = Pretty.block [ Pretty.str "Head: ", Pretty.fbrk, pretty_constraint_atom ctxt (f,R) ] fun isc (SOME (ps,(fp,R)),_) = if unifies ctxt (f,fp) then SOME (ps,(fp,R)) else NONE | isc _ = NONE val candidates = pairs |> map_filter isc fun try_c c = let val pt1 = Pretty.block [ Pretty.str "Trying ", pretty_constraint ctxt c ] val rl = mk_CONSTRAINT_rl ctxt c |> Drule.zero_var_indexes val res = (SOLVED' (resolve_tac ctxt [rl])) i st |> Seq.pull |> is_some val pt2 = (if res then Pretty.str "OK" else Pretty.str "ERR") in Pretty.block [pt1,Pretty.fbrk,pt2] end val res = Pretty.block ( Pretty.fbreaks [pt_hd, Pretty.big_list "Solving Attempts" (map try_c candidates)] ) in res end | _ => Pretty.str "Unexpected goal format" exception ERR of Pretty.T fun analyze' ctxt i j st = let val As = Logic.strip_horn (Thm.prop_of st) |> #1 |> drop (i-1) |> take (j-i+1) |> map (strip_all_body #> Logic.strip_imp_concl) val Cs = map_filter ( fn @{mpat "Trueprop (CONSTRAINT ?f ?R)"} => SOME (f,R) | @{mpat "Trueprop ((_,_)\_)"} => NONE | t => raise ERR (Pretty.block [ Pretty.str "Internal: Unexpected goal format: ", Syntax.pretty_term ctxt t ]) ) As val Cs_problems = map (fn c => case analyze_possible_problems ctxt c of NONE => pretty_constraint_atom ctxt c | SOME p => Pretty.block [pretty_constraint_atom ctxt c,Pretty.fbrk,p] ) Cs val Cs_pretty = Pretty.big_list "Constraints" Cs_problems in case Cs of [] => () | _ => raise ERR (Pretty.block [ Pretty.str "Could not infer all relators, some constraints remaining", Pretty.fbrk, Cs_pretty, Pretty.fbrk, Pretty.block [ Pretty.str "Trying to solve first constraint", Pretty.fbrk, pretty_try_candidates ctxt i st ] ]) end in fun analyze ctxt i j st = can (analyze' ctxt i j) st fun pretty_failure ctxt i j st = (analyze' ctxt i j st; Pretty.str "No failure") handle ERR p => p fun try_solve_tac ctxt i st = if i > Thm.nprems_of st then (tracing "Goal number out of range"; Seq.empty) else case Logic.concl_of_goal (Thm.prop_of st) i of @{mpat "Trueprop (CONSTRAINT ?f ?R)"} => let val pairs = thm_pairsD.get ctxt val st = Drule.zero_var_indexes st val pt = Pretty.block [ Pretty.str "Head: ", Pretty.fbrk, pretty_constraint_atom ctxt (f,R) ] val _ = tracing (Pretty.string_of pt) val _ = case analyze_possible_problems ctxt (f,R) of NONE => () | SOME p => tracing (Pretty.string_of p) fun isc (SOME (ps,(fp,R)),_) = if unifies ctxt (f,fp) then SOME (ps,(fp,R)) else NONE | isc _ = NONE val net = pairs |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt)) |> Tactic.build_net val candidates = pairs |> map_filter isc fun try_c c = let val _ = Pretty.block [ Pretty.str "Trying ", pretty_constraint ctxt c ] |> Pretty.string_of |> tracing val rl = mk_CONSTRAINT_rl ctxt c |> Drule.zero_var_indexes val res = (SOLVED' (resolve_tac ctxt [rl] THEN_ALL_NEW (REPEAT_ALL_NEW (resolve_from_net_tac ctxt net))) ) i st |> Seq.pull |> is_some val _ = (if res then Pretty.str "OK" else Pretty.str "ERR") |> Pretty.string_of |> tracing in () end val _ = map try_c candidates in Seq.single st end | _ => Seq.empty end fun solve_step_tac ctxt = let val pairs = thm_pairsD.get ctxt val net = pairs |> map_filter (fst #> map_option (mk_CONSTRAINT_rl ctxt)) |> Tactic.build_net in resolve_from_net_tac ctxt net end val phase = { init = thm_pairsD.init #> hom_netD.init, tac = guess_relators_tac, analyze = analyze, pretty_failure = pretty_failure } val setup = hom_rules.setup #> tyrel_rules.setup end \ setup Autoref_Fix_Rel.setup end diff --git a/thys/IMP2/automation/IMP2_Var_Abs.thy b/thys/IMP2/automation/IMP2_Var_Abs.thy --- a/thys/IMP2/automation/IMP2_Var_Abs.thy +++ b/thys/IMP2/automation/IMP2_Var_Abs.thy @@ -1,105 +1,105 @@ section \Abstraction over Program Variables\ theory IMP2_Var_Abs imports "../basic/Semantics" "../parser/Parser" IMP2_Basic_Simpset begin definition VAR :: "'v \ ('v \ 'a) \ 'a" where "VAR v f \ f v" ML \ structure Program_Variables = struct datatype T = AbsInfo of ((IMP_Syntax.impvar * string) * term) list * (string * term) (* (imp_var \ sfx_name \ Free) list \ (statename \ statev) where imp_var -- IMP variable sfx_name -- HOL variable name to bind to Free -- Free variable in term that shall be abstracted statename -- HOL variable name to bind state to statev -- Free variable for state in term *) val stateN = "\" (* Base name for state variable *) val nameT = @{typ vname} (* HOL type of variable names *) val avalueT = @{typ val} (* HOL type of array variable values *) val pvalueT = @{typ pval} (* HOL type of primitive variable values *) fun mk_vref_t state_t (ivname,IMP_Syntax.VAL) = state_t $ IMP_Syntax.mk_varname ivname $ @{term "0::int"} | mk_vref_t state_t (ivname,IMP_Syntax.ARRAY) = state_t $ IMP_Syntax.mk_varname ivname val stateT = nameT --> avalueT fun abstract_var statev ((imp_var, sfx_name), v) t = let val T = fastype_of t val vT = fastype_of v val t = Term.lambda_name (sfx_name,v) t val vref_t = mk_vref_t statev imp_var in Const (@{const_name VAR}, vT --> (vT --> T) --> T) $ vref_t $ t end fun get_statev (AbsInfo (_,(_,v))) = v (* Create context and abstraction info that binds imp variables to Isabelle variable names. Moreover, the state is bound to Isabelle variable with name stateN and specified suffix. *) fun gen_declare_variables imp_x_isa_names isa_suffix ctxt = let val ctxt = ctxt |> Variable.set_body true val isa_statename = suffix isa_suffix stateN val (statev,ctxt) = yield_singleton Variable.add_fixes isa_statename ctxt val statev = Free (statev,stateT) val ctxt = Variable.declare_constraints statev ctxt fun imp_var_isa_T (_,IMP_Syntax.VAL) = pvalueT | imp_var_isa_T (_,IMP_Syntax.ARRAY) = avalueT fun declare_impv (imp_var,isa_name) ctxt = let val isa_name = suffix isa_suffix isa_name val (vname,ctxt) = yield_singleton Variable.add_fixes isa_name ctxt val v = Free (vname, imp_var_isa_T imp_var) val ctxt = Variable.declare_constraints v ctxt in - (((imp_var,isa_name),v), Variable.auto_fixes v ctxt ) + (((imp_var,isa_name),v), Proof_Context.augment v ctxt ) end val (vs, ctxt) = fold_map declare_impv imp_x_isa_names ctxt in (AbsInfo (vs, (isa_statename, statev)), ctxt) end fun declare_variables imp_vars sfx ctxt = let val imp_x_isa_names = imp_vars ~~ (map fst imp_vars) in gen_declare_variables imp_x_isa_names sfx ctxt end fun abstract_vars (AbsInfo (nsvs, (_,statev))) t = let val frees = Term.add_frees t [] |> map Free |> Termtab.make_set fun absv (nss,v) = if Termtab.defined frees v then abstract_var statev (nss,v) else I val t = fold absv nsvs t in t end fun abstract_state (AbsInfo (_, (staten,statev))) t = Term.lambda_name (staten, statev) t fun abstract vinfo = abstract_vars vinfo #> abstract_state vinfo end \ end diff --git a/thys/Nominal2/nominal_dt_quot.ML b/thys/Nominal2/nominal_dt_quot.ML --- a/thys/Nominal2/nominal_dt_quot.ML +++ b/thys/Nominal2/nominal_dt_quot.ML @@ -1,751 +1,751 @@ (* Title: nominal_dt_alpha.ML Author: Christian Urban Author: Cezary Kaliszyk Performing quotient constructions, lifting theorems and deriving support properties for the quotient types. *) signature NOMINAL_DT_QUOT = sig val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> thm list -> local_theory -> Quotient_Info.quotients list * local_theory val define_qconsts: typ list -> (string * term * mixfix * thm) list -> local_theory -> Quotient_Info.quotconsts list * local_theory val define_qperms: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory val define_qsizes: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> local_theory -> local_theory val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context val prove_supports: Proof.context -> thm list -> term list -> thm list val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> local_theory -> local_theory val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list val prove_strong_induct: Proof.context -> thm -> thm list -> thm list -> bclause list list list -> thm list end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = struct open Nominal_Permeq fun lookup xs x = the (AList.lookup (op=) xs x) (* defines the quotient types *) fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = let val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1 val qty_args3 = qty_args2 ~~ alpha_equivp_thms in fold_map (Quotient_Type.add_quotient_type {overloaded = false}) qty_args3 lthy end (* a wrapper for lifting a raw constant *) fun lift_raw_const qtys (qconst_name, rconst, mx', rsp_thm) lthy = let val rty = fastype_of rconst val qty = Quotient_Term.derive_qtyp lthy qtys rty val lhs_raw = Free (qconst_name, qty) val rhs_raw = rconst val raw_var = (Binding.name qconst_name, NONE, mx') val ((binding, _, mx), ctxt) = Proof_Context.cert_var raw_var lthy val lhs = Syntax.check_term ctxt lhs_raw val rhs = Syntax.check_term ctxt rhs_raw val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" val _ = if is_Const rhs then () else warning "The definiens is not a constant" in Quotient_Def.add_quotient_def (((binding, mx), Binding.empty_atts), (lhs, rhs)) rsp_thm ctxt end (* defines quotient constants *) fun define_qconsts qtys consts_specs lthy = let val (qconst_infos, lthy') = fold_map (lift_raw_const qtys) consts_specs lthy val phi = Proof_Context.export_morphism lthy' (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy) in (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy') end (* defines the quotient permutations and proves pt-class *) fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = let val lthy1 = lthy |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) val (_, lthy2) = define_qconsts qtys perm_specs lthy1 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 val lifted_perm_laws = map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |> Variable.exportT lthy3 lthy2 fun tac ctxt = Class.intro_classes_tac ctxt [] THEN (ALLGOALS (resolve_tac ctxt lifted_perm_laws)) in lthy2 |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end (* defines the size functions and proves size-class *) fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = let fun tac ctxt = Class.intro_classes_tac ctxt [] in lthy |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) |> snd o (define_qconsts qtys size_specs) |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end (* lifts a theorem and cleans all "_raw" parts from variable names *) local val any = Scan.one (Symbol.not_eof) val raw = Scan.this_string "_raw" val exclude = Scan.repeat (Scan.unless raw any) --| raw >> implode val parser = Scan.repeat (exclude || any) in fun unraw_str s = s |> raw_explode |> Scan.finite Symbol.stopper parser >> implode |> fst end fun unraw_vars_thm ctxt thm = let fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) val vars = Term.add_vars (Thm.prop_of thm) [] val vars' = map (Thm.cterm_of ctxt o Var o unraw_var_str) vars in Thm.instantiate ([], (vars ~~ vars')) thm end fun unraw_bounds_thm th = let val trm = Thm.prop_of th val trm' = Term.map_abs_vars unraw_str trm in Thm.rename_boundvars trm trm' th end fun lift_thms qtys simps thms ctxt = (map (Quotient_Tacs.lifted ctxt qtys simps #> unraw_bounds_thm #> unraw_vars_thm ctxt #> Drule.zero_var_indexes) thms, ctxt) fun mk_supports_goal ctxt qtrm = let val vs = fresh_args ctxt qtrm val rhs = list_comb (qtrm, vs) val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} |> mk_supp in mk_supports lhs rhs |> HOLogic.mk_Trueprop end fun supports_tac ctxt perm_simps = let val simpset1 = put_simpset HOL_basic_ss ctxt addsimps @{thms supports_def fresh_def[symmetric]} val simpset2 = put_simpset HOL_ss ctxt addsimps @{thms swap_fresh_fresh fresh_Pair} in EVERY' [ simp_tac simpset1, eqvt_tac ctxt (eqvt_strict_config addpres perm_simps), simp_tac simpset2 ] end fun prove_supports_single ctxt perm_simps qtrm = let val goal = mk_supports_goal ctxt qtrm - val ctxt' = Variable.auto_fixes goal ctxt + val ctxt' = Proof_Context.augment goal ctxt in Goal.prove ctxt' [] [] goal (K (HEADGOAL (supports_tac ctxt perm_simps))) |> singleton (Proof_Context.export ctxt' ctxt) end fun prove_supports ctxt perm_simps qtrms = map (prove_supports_single ctxt perm_simps) qtrms (* finite supp lemmas for qtypes *) fun prove_fsupp ctxt qtys qinduct qsupports_thms = let val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt val goals = vs ~~ qtys |> map Free |> map (mk_finite o mk_supp) |> foldr1 (HOLogic.mk_conj) |> HOLogic.mk_Trueprop val tac = EVERY' [ resolve_tac ctxt' @{thms supports_finite}, resolve_tac ctxt' qsupports_thms, asm_simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms finite_supp supp_Pair finite_Un}) ] in Goal.prove ctxt' [] [] goals (K (HEADGOAL (resolve_tac ctxt' [qinduct] THEN_ALL_NEW tac))) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map zero_var_indexes end (* finite supp instances *) fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = let val lthy1 = lthy |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) fun tac ctxt = Class.intro_classes_tac ctxt [] THEN (ALLGOALS (resolve_tac ctxt qfsupp_thms)) in lthy1 |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end (* proves that fv and fv_bn equals supp *) fun gen_mk_goals fv supp = let val arg_ty = fastype_of fv |> domain_type in (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x)) end fun mk_fvs_goals fv = gen_mk_goals fv mk_supp fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn) fun add_simpset ctxt thms = put_simpset HOL_basic_ss ctxt addsimps thms fun symmetric thms = map (fn thm => thm RS @{thm sym}) thms val supp_Abs_set = @{thms supp_Abs(1)[symmetric]} val supp_Abs_res = @{thms supp_Abs(2)[symmetric]} val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]} fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst fun mk_supp_abs_tac ctxt [] = [] | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs fun mk_bn_supp_abs_tac ctxt trm = trm |> fastype_of |> body_type |> (fn ty => case ty of @{typ "atom set"} => simp_tac (add_simpset ctxt supp_Abs_set) | @{typ "atom list"} => simp_tac (add_simpset ctxt supp_Abs_lst) | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_conv permute_prod_def prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps fv_bn_eqvts qinduct bclausess ctxt = let val goals1 = map mk_fvs_goals fvs val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns fun tac ctxt = SUBGOAL (fn (goal, i) => let val (fv_fun, arg) = goal |> Envir.eta_contract |> Logic.strip_assums_concl |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |> dest_comb val supp_abs_tac = case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) | NONE => mk_bn_supp_abs_tac ctxt fv_fun val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts) in EVERY' [ TRY o asm_full_simp_tac (add_simpset ctxt (@{thm supp_Pair[symmetric]}::fv_simps)), TRY o supp_abs_tac, TRY o simp_tac (add_simpset ctxt @{thms supp_def supp_rel_def}), TRY o eqvt_tac ctxt eqvt_rconfig, TRY o simp_tac (add_simpset ctxt (@{thms Abs_eq_iff} @ eq_iffs)), TRY o asm_full_simp_tac (add_simpset ctxt thms3), TRY o simp_tac (add_simpset ctxt thms2), TRY o asm_full_simp_tac (add_simpset ctxt (thms1 @ (symmetric fv_bn_eqvts)))] i end) in induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |> map (atomize ctxt) |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]})) end fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = let fun mk_goal qbn = let val arg_ty = domain_type (fastype_of qbn) val finite = @{term "finite :: atom set => bool"} in (arg_ty, fn x => finite $ (to_set (qbn $ x))) end val props = map mk_goal qbns val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @ @{thms set_simps set_append finite_insert finite.emptyI finite_Un})) in induct_prove qtys props qinduct (K ss_tac) ctxt end fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) fun mk_goal qperm_bn alpha_bn = let val arg_ty = domain_type (fastype_of alpha_bn) in (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) end val props = map2 mk_goal qperm_bns alpha_bns val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls val ss_tac = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in induct_prove qtys props qinduct (K ss_tac) ctxt' |> Proof_Context.export ctxt' ctxt |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def})) end fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt = let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) fun mk_goal qbn qperm_bn = let val arg_ty = domain_type (fastype_of qbn) in (arg_ty, fn x => (mk_id (Abs ("", arg_ty, HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x)) end val props = map2 mk_goal qbns qperm_bns val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs val ss_tac = EVERY' [asm_full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts), TRY o asm_full_simp_tac (put_simpset HOL_basic_ss ctxt')] in induct_prove qtys props qinduct (K ss_tac) ctxt' |> Proof_Context.export ctxt' ctxt |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def})) end (*** proves strong exhauts theorems ***) (* fixme: move into nominal_library *) fun abs_const bmode ty = let val (const_name, binder_ty, abs_ty) = case bmode of Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) in Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty])) end fun mk_abs bmode trm1 trm2 = abs_const bmode (fastype_of trm2) $ trm1 $ trm2 fun is_abs_eq thm = let fun is_abs trm = case (head_of trm) of Const (@{const_name "Abs_set"}, _) => true | Const (@{const_name "Abs_lst"}, _) => true | Const (@{const_name "Abs_res"}, _) => true | _ => false in thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> is_abs end (* adds a freshness condition to the assumptions *) fun mk_ecase_prems lthy c (params, prems, concl) bclauses = let val tys = map snd params val binders = get_all_binders bclauses fun prep_binder (opt, i) = let val t = Bound (length tys - i - 1) in case opt of NONE => setify_ty lthy (nth tys i) t | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) end val prems' = case binders of [] => prems (* case: no binders *) | _ => binders (* case: binders *) |> map prep_binder |> fold_union_env tys |> (fn t => mk_fresh_star t c) |> (fn t => HOLogic.mk_Trueprop t :: prems) in mk_full_horn params prems' concl end (* derives the freshness theorem that there exists a p, such that (p o as) #* (c, t1,..., tn) *) fun fresh_thm ctxt c parms binders bn_finite_thms = let fun prep_binder (opt, i) = case opt of NONE => setify ctxt (nth parms i) | SOME bn => to_set (bn $ (nth parms i)) fun prep_binder2 (opt, i) = case opt of NONE => atomify ctxt (nth parms i) | SOME bn => bn $ (nth parms i) val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders)) val lhs = binders |> map prep_binder |> fold_union |> mk_perm (Bound 0) val goal = mk_fresh_star lhs rhs |> mk_exists ("p", @{typ perm}) |> HOLogic.mk_Trueprop val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} @ @{thms finite.intros finite_Un finite_set finite_fset} in Goal.prove ctxt [] [] goal (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding1} THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss))))) end (* derives an abs_eq theorem of the form Exists q. [as].x = [p o as].(q o x) for non-recursive binders Exists q. [as].x = [q o as].(q o x) for recursive binders *) fun abs_eq_thm ctxt fprops p parms bn_eqvt permute_bns (bclause as (BC (bmode, binders, bodies))) = case binders of [] => [] | _ => let val rec_flag = is_recursive_binder bclause val binder_trm = comb_binders ctxt bmode parms binders val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) val abs_lhs = mk_abs bmode binder_trm body_trm val abs_rhs = if rec_flag then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm) else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm) val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) val goal = HOLogic.mk_conj (abs_eq, peq) |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |> HOLogic.mk_Trueprop val ss = fprops @ @{thms set_simps set_append union_eqvt} @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset fresh_star_set} val tac1 = if rec_flag then resolve_tac ctxt @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} else resolve_tac ctxt @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} val tac2 = EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss), TRY o simp_tac (put_simpset HOL_ss ctxt)] in [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |> (if rec_flag then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt) else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ] end val setify = @{lemma "xs = ys ==> set xs = set ys" by simp} fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas prems bclausess qexhaust_thm = let fun aux_tac prem bclauses = case (get_all_binders bclauses) of [] => EVERY' [resolve_tac ctxt [prem], assume_tac ctxt] | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => let val parms = map (Thm.term_of o snd) params val fthm = fresh_thm ctxt c parms binders bn_finite_thms val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} val (([(_, fperm)], fprops), ctxt') = Obtain.result (fn ctxt' => EVERY1 [eresolve_tac ctxt [exE], full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), REPEAT o (eresolve_tac ctxt @{thms conjE})]) [fthm] ctxt val abs_eq_thms = flat (map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses) val ((_, eqs), ctxt'') = Obtain.result (fn ctxt'' => EVERY1 [ REPEAT o (eresolve_tac ctxt @{thms exE}), REPEAT o (eresolve_tac ctxt @{thms conjE}), REPEAT o (dresolve_tac ctxt [setify]), full_simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt' val (abs_eqs, peqs) = split_filter is_abs_eq eqs val fprops' = map (eqvt_rule ctxt'' (eqvt_strict_config addpres permute_bns)) fprops @ map (eqvt_rule ctxt'' (eqvt_strict_config addpres bn_eqvt)) fprops (* for freshness conditions *) val tac1 = SOLVED' (EVERY' [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}), conj_tac ctxt'' (DETERM o resolve_tac ctxt'' fprops') ]) (* for equalities between constructors *) val tac2 = SOLVED' (EVERY' [ resolve_tac ctxt [@{thm ssubst} OF prems], rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms), rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs), conj_tac ctxt'' (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ]) (* proves goal "P" *) val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl) (K (EVERY1 [ resolve_tac ctxt'' [prem], RANGE [tac1, tac2] ])) |> singleton (Proof_Context.export ctxt'' ctxt) in resolve_tac ctxt [side_thm] 1 end) ctxt in EVERY1 [resolve_tac ctxt [qexhaust_thm], RANGE (map2 aux_tac prems bclausess)] end fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas = let val ((_, exhausts'), lthy') = Variable.import true exhausts lthy val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' val c = Free (c, TFree (a, @{sort fs})) val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *) |> map Thm.prop_of |> map Logic.strip_horn |> split_list val ecases' = (map o map) strip_full_horn ecases val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss fun tac bclausess exhaust {prems, context} = case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas prems bclausess exhaust fun prove prems bclausess exhaust concl = Goal.prove lthy'' [] prems concl (tac bclausess exhaust) in map4 prove premss bclausesss exhausts' main_concls |> Proof_Context.export lthy'' lthy end (** strong induction theorems **) fun add_c_prop c c_ty trm = let val (P, arg) = dest_comb trm val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty in Free (P_name, (c_ty :: ty_args) ---> bool) $ c $ arg end fun add_qnt_c_prop c_name c_ty trm = trm |> HOLogic.dest_Trueprop |> incr_boundvars 1 |> add_c_prop (Bound 0) c_ty |> HOLogic.mk_Trueprop |> mk_all (c_name, c_ty) fun prep_prem lthy c c_name c_ty bclauses (params, prems, concl) = let val tys = map snd params val binders = get_all_binders bclauses fun prep_binder (opt, i) = let val t = Bound (length tys - i - 1) in case opt of NONE => setify_ty lthy (nth tys i) t | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) end val prems' = prems |> map (incr_boundvars 1) |> map (add_qnt_c_prop c_name c_ty) val prems'' = case binders of [] => prems' (* case: no binders *) | _ => binders (* case: binders *) |> map prep_binder |> fold_union_env tys |> incr_boundvars 1 |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |> (fn t => HOLogic.mk_Trueprop t :: prems') val concl' = concl |> HOLogic.dest_Trueprop |> incr_boundvars 1 |> add_c_prop (Bound 0) c_ty |> HOLogic.mk_Trueprop in mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' end fun prove_strong_induct lthy induct exhausts size_thms bclausesss = let val ((_, [induct']), lthy') = Variable.import true [induct] lthy val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' val c_ty = TFree (a, @{sort fs}) val c = Free (c_name, c_ty) val (prems, concl) = induct' |> Thm.prop_of |> Logic.strip_horn val concls = concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map (add_c_prop c c_ty) |> map HOLogic.mk_Trueprop val prems' = prems |> map strip_full_horn |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss) fun pat_tac ctxt thm = Subgoal.FOCUS (fn {params, context = ctxt', ...} => let val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params val vs = Term.add_vars (Thm.prop_of thm) [] val vs_tys = map (Type.legacy_freeze_type o snd) vs val assigns = map (lookup ty_parms) vs_tys val thm' = infer_instantiate ctxt' (map #1 vs ~~ assigns) thm in resolve_tac ctxt' [thm'] 1 end) ctxt THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) fun size_simp_tac ctxt = simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms)) in Goal.prove_common lthy'' NONE [] prems' concls (fn {prems, context = ctxt} => Induction_Schema.induction_schema_tac ctxt prems THEN RANGE (map (pat_tac ctxt) exhausts) 1 THEN prove_termination_ind ctxt 1 THEN ALLGOALS (size_simp_tac ctxt)) |> Proof_Context.export lthy'' lthy end end (* structure *) diff --git a/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy b/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy --- a/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy @@ -1,1378 +1,1378 @@ section \Utilities for Interface Specifications and Implementations\ theory Sepref_Intf_Util imports Sepref_Rules Sepref_Translate "Lib/Term_Synth" Sepref_Combinator_Setup "Lib/Concl_Pres_Clarification" keywords "sepref_decl_op" :: thy_goal and "sepref_decl_impl" :: thy_goal begin subsection \Relation Interface Binding\ definition INTF_OF_REL :: "('a\'b) set \ 'c itself \ bool" where [simp]: "INTF_OF_REL R I \ True" lemma intf_of_relI: "INTF_OF_REL (R::(_\'a) set) TYPE('a)" by simp declare intf_of_relI[synth_rules] \ \Declare as fallback rule\ lemma [synth_rules]: "INTF_OF_REL unit_rel TYPE(unit)" "INTF_OF_REL nat_rel TYPE(nat)" "INTF_OF_REL int_rel TYPE(int)" "INTF_OF_REL bool_rel TYPE(bool)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\option_rel) TYPE('a option)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\list_rel) TYPE('a list)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\nres_rel) TYPE('a nres)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (R\\<^sub>rS) TYPE('a\'b)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (\R,S\sum_rel) TYPE('a+'b)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (R\S) TYPE('a\'b)" by simp_all lemma synth_intf_of_relI: "INTF_OF_REL R I \ SYNTH_TERM R I" by simp subsection \Operations with Precondition\ definition mop :: "('a\bool) \ ('a\'b nres) \ 'a \ 'b nres" \ \Package operation with precondition\ where [simp]: "mop P f \ \x. ASSERT (P x) \ f x" lemma param_op_mop_iff: assumes "(Q,P)\R\bool_rel" shows "(f, g) \ [P]\<^sub>f R \ \S\nres_rel \ (mop Q f, mop P g) \ R \\<^sub>f \S\nres_rel " using assms by (auto simp: mop_def fref_def pw_nres_rel_iff refine_pw_simps dest: fun_relD) lemma param_mopI: assumes "(f,g) \ [P]\<^sub>f R \ \S\nres_rel" assumes "(Q,P) \ R \ bool_rel" shows "(mop Q f, mop P g) \ R \\<^sub>f \S\nres_rel" using assms by (simp add: param_op_mop_iff) lemma mop_spec_rl: "P x \ mop P f x \ f x" by simp lemma mop_spec_rl_from_def: assumes "f \ mop P g" assumes "P x" assumes "g x \ z" shows "f x \ z" using assms mop_spec_rl by simp lemma mop_leof_rl_from_def: assumes "f \ mop P g" assumes "P x \ g x \\<^sub>n z" shows "f x \\<^sub>n z" using assms by (simp add: pw_leof_iff refine_pw_simps) lemma assert_true_bind_conv: "ASSERT True \ m = m" by simp lemmas mop_alt_unfolds = curry_def curry0_def mop_def uncurry_apply uncurry0_apply o_apply assert_true_bind_conv subsection \Constraints\ lemma add_is_pure_constraint: "\PROP P; CONSTRAINT is_pure A\ \ PROP P" . lemma sepref_relpropI: "P R = CONSTRAINT P R" by simp subsubsection \Purity\ lemmas [constraint_simps] = the_pure_pure definition [constraint_abbrevs]: "IS_PURE P R \ is_pure R \ P (the_pure R)" lemma IS_PURE_pureI: "P R \ IS_PURE P (pure R)" by (auto simp: IS_PURE_def) lemma [fcomp_norm_simps]: "CONSTRAINT (IS_PURE \) P \ pure (the_pure P) = P" by (simp add: IS_PURE_def) lemma [fcomp_norm_simps]: "CONSTRAINT (IS_PURE P) A \ P (the_pure A)" by (auto simp: IS_PURE_def) lemma handle_purity1: "CONSTRAINT (IS_PURE \) A \ CONSTRAINT \ (the_pure A)" by (auto simp: IS_PURE_def) lemma handle_purity2: "CONSTRAINT (IS_PURE \) A \ CONSTRAINT is_pure A" by (auto simp: IS_PURE_def) subsection \Composition\ (* TODO/FIXME: Overlaps with FCOMP! *) subsubsection \Preconditions\ definition [simp]: "tcomp_pre Q T P \ \a. Q a \ (\a'. (a', a) \ T \ P a')" definition "and_pre P1 P2 \ \x. P1 x \ P2 x" definition "imp_pre P1 P2 \ \x. P1 x \ P2 x" lemma and_pre_beta: "PP \ P x \ Q x \ PP \ and_pre P Q x" by (auto simp: and_pre_def) lemma imp_pre_beta: "PP \ P x \ Q x \ PP \ imp_pre P Q x" by (auto simp: imp_pre_def) definition "IMP_PRE P1 P2 \ \x. P1 x \ P2 x" lemma IMP_PRED: "IMP_PRE P1 P2 \ P1 x \ P2 x" unfolding IMP_PRE_def by auto lemma IMP_PRE_refl: "IMP_PRE P P" unfolding IMP_PRE_def by auto definition "IMP_PRE_CUSTOM \ IMP_PRE" lemma IMP_PRE_CUSTOMD: "IMP_PRE_CUSTOM P1 P2 \ IMP_PRE P1 P2" by (simp add: IMP_PRE_CUSTOM_def) lemma IMP_PRE_CUSTOMI: "\\x. P1 x \ P2 x\ \ IMP_PRE_CUSTOM P1 P2" by (simp add: IMP_PRE_CUSTOM_def IMP_PRE_def) lemma imp_and_triv_pre: "IMP_PRE P (and_pre (\_. True) P)" unfolding IMP_PRE_def and_pre_def by auto subsubsection \Premises\ definition "ALL_LIST A \ (\x\set A. x)" definition "IMP_LIST A B \ ALL_LIST A \ B" lemma to_IMP_LISTI: "P \ IMP_LIST [] P" by (auto simp: IMP_LIST_def) lemma to_IMP_LIST: "(P \ IMP_LIST Ps Q) \ Trueprop (IMP_LIST (P#Ps) Q)" by (auto simp: IMP_LIST_def ALL_LIST_def intro!: equal_intr_rule) lemma from_IMP_LIST: "Trueprop (IMP_LIST As B) \ (ALL_LIST As \ B)" "(ALL_LIST [] \ B) \ Trueprop B" "(ALL_LIST (A#As) \ B) \ (A \ ALL_LIST As \ B)" by (auto simp: IMP_LIST_def ALL_LIST_def intro!: equal_intr_rule) lemma IMP_LIST_trivial: "IMP_LIST A B \ IMP_LIST A B" . subsubsection \Composition Rules\ lemma hfcomp_tcomp_pre: assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" shows "(f,h) \ [tcomp_pre Q T P]\<^sub>a hrp_comp RR' T \ hr_comp S U" using hfcomp[OF A B] by simp lemma transform_pre_param: assumes A: "IMP_LIST Cns ((f, h) \ [tcomp_pre Q T P]\<^sub>a hrp_comp RR' T \ hr_comp S U)" assumes P: "IMP_LIST Cns ((P,P') \ T \ bool_rel)" assumes C: "IMP_PRE PP' (and_pre P' Q)" shows "IMP_LIST Cns ((f,h) \ [PP']\<^sub>a hrp_comp RR' T \ hr_comp S U)" unfolding from_IMP_LIST apply (rule hfref_cons) apply (rule A[unfolded from_IMP_LIST]) apply assumption apply (drule IMP_PRED[OF C]) using P[unfolded from_IMP_LIST] unfolding and_pre_def apply (auto dest: fun_relD) [] by simp_all lemma hfref_mop_conv: "((g,mop P f) \ [Q]\<^sub>a R \ S) \ (g,f) \ [\x. P x \ Q x]\<^sub>a R \ S" apply (simp add: hfref_to_ASSERT_conv) apply (fo_rule arg_cong fun_cong)+ by (auto intro!: ext simp: pw_eq_iff refine_pw_simps) lemma hfref_op_to_mop: assumes R: "(impl,f) \ [Q]\<^sub>a R \ S" assumes DEF: "mf \ mop P f" assumes C: "IMP_PRE PP' (imp_pre P Q)" shows "(impl,mf) \ [PP']\<^sub>a R \ S" unfolding DEF hfref_mop_conv apply (rule hfref_cons[OF R]) using C by (auto simp: IMP_PRE_def imp_pre_def) lemma hfref_mop_to_op: assumes R: "(impl,mf) \ [Q]\<^sub>a R \ S" assumes DEF: "mf \ mop P f" assumes C: "IMP_PRE PP' (and_pre Q P)" shows "(impl,f) \ [PP']\<^sub>a R \ S" using R unfolding DEF hfref_mop_conv apply (rule hfref_cons) using C apply (auto simp: and_pre_def IMP_PRE_def) done subsubsection \Precondition Simplification\ lemma IMP_PRE_eqI: assumes "\x. P x \ Q x" assumes "CNV P P'" shows "IMP_PRE P' Q" using assms by (auto simp: IMP_PRE_def) lemma simp_and1: assumes "Q \ CNV P P'" assumes "PP \ P' \ Q" shows "PP \ P \ Q" using assms by auto lemma simp_and2: assumes "P \ CNV Q Q'" assumes "PP \ P \ Q'" shows "PP \ P \ Q" using assms by auto lemma triv_and1: "Q \ True \ Q" by blast lemma simp_imp: assumes "P \ CNV Q Q'" assumes "PP \ Q'" shows "PP \ (P \ Q)" using assms by auto lemma CNV_split: assumes "CNV A A'" assumes "CNV B B'" shows "CNV (A \ B) (A' \ B')" using assms by auto lemma CNV_prove: assumes "P" shows "CNV P True" using assms by auto lemma simp_pre_final_simp: assumes "CNV P P'" shows "P' \ P" using assms by auto lemma auto_weaken_pre_uncurry_step': assumes "PROTECT f a \ f'" shows "PROTECT (uncurry f) (a,b) \ f' b" using assms by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection) subsection \Protected Constants\ lemma add_PR_CONST_to_def: "x\y \ PR_CONST x \ y" by simp subsection \Rule Collections\ named_theorems_rev sepref_mop_def_thms \Sepref: mop - definition theorems\ named_theorems_rev sepref_fref_thms \Sepref: fref-theorems\ named_theorems sepref_relprops_transform \Sepref: Simp-rules to transform relator properties\ named_theorems sepref_relprops \Sepref: Simp-rules to add CONSTRAINT-tags to relator properties\ named_theorems sepref_relprops_simps \Sepref: Simp-rules to simplify relator properties\ subsubsection \Default Setup\ subsection \ML-Level Declarations\ ML \ signature SEPREF_INTF_UTIL = sig (* Miscellaneous*) val list_filtered_subterms: (term -> 'a option) -> term -> 'a list (* Interface types for relations *) val get_intf_of_rel: Proof.context -> term -> typ (* Constraints *) (* Convert relations to pure assertions *) val to_assns_rl: bool -> Proof.context -> thm -> thm (* Recognize, summarize and simplify CONSTRAINT - premises *) val cleanup_constraints: Proof.context -> thm -> thm (* Preconditions *) (* Simplify precondition. Goal must be in IMP_PRE or IMP_PRE_CUSTOM form. *) val simp_precond_tac: Proof.context -> tactic' (* Configuration options *) val cfg_def: bool Config.T (* decl_op: Define constant *) val cfg_ismop: bool Config.T (* decl_op: Specified term is mop *) val cfg_mop: bool Config.T (* decl_op, decl_impl: Derive mop *) val cfg_rawgoals: bool Config.T (* decl_op, decl_impl: Do not pre-process/solve goals *) (* TODO: Make do_cmd usable from ML-level! *) end structure Sepref_Intf_Util: SEPREF_INTF_UTIL = struct val cfg_debug = Attrib.setup_config_bool @{binding sepref_debug_intf_util} (K false) val dbg_trace = Sepref_Debugging.dbg_trace_msg cfg_debug val dbg_msg_tac = Sepref_Debugging.dbg_msg_tac cfg_debug fun list_filtered_subterms f t = let fun r t = case f t of SOME a => [a] | NONE => ( case t of t1$t2 => r t1 @ r t2 | Abs (_,_,t) => r t | _ => [] ) in r t end fun get_intf_of_rel ctxt R = Term_Synth.synth_term @{thms synth_intf_of_relI} ctxt R |> fastype_of |> Refine_Util.dest_itselfT local fun add_is_pure_constraint ctxt v thm = let val v = Thm.cterm_of ctxt v val rl = Drule.infer_instantiate' ctxt [NONE, SOME v] @{thm add_is_pure_constraint} in thm RS rl end in fun to_assns_rl add_pure_constr ctxt thm = let val orig_ctxt = ctxt val (thm,ctxt) = yield_singleton (apfst snd oo Variable.importT) thm ctxt val (R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\fref _ ?R ?S)"} => (R,S) | _ => raise THM("to_assns_rl: expected fref-thm",~1,[thm]) fun mk_cn_subst (fname,(iname,C,A)) = let val T' = A --> C --> @{typ assn} val v' = Free (fname,T') val ct' = @{mk_term "the_pure ?v'"} |> Thm.cterm_of ctxt in (v',(iname,ct')) end fun relation_flt (name,Type (@{type_name set},[Type (@{type_name prod},[C,A])])) = SOME (name,C,A) | relation_flt _ = NONE val vars = [] |> Term.add_vars R |> Term.add_vars S |> map_filter (relation_flt) val (names,ctxt) = Variable.variant_fixes (map (#1 #> fst) vars) ctxt val cn_substs = map mk_cn_subst (names ~~ vars) val thm = Drule.infer_instantiate ctxt (map snd cn_substs) thm val thm = thm |> add_pure_constr ? fold (fn (v,_) => fn thm => add_is_pure_constraint ctxt v thm) cn_substs val thm = singleton (Variable.export ctxt orig_ctxt) thm in thm end fun cleanup_constraints ctxt thm = let val orig_ctxt = ctxt val (thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) thm ctxt val xform_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops_transform} val rprops_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops} val simp_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops_simps} fun simp thms = Conv.fconv_rule ( Simplifier.asm_full_rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)) (* Check for pure (the_pure R) - patterns *) local val (_,R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\hfref ?P ?R ?S)"} => (P,R,S) | @{mpat "Trueprop (_\fref ?P ?R ?S)"} => (P,R,S) | _ => raise THM("cleanup_constraints: Expected hfref or fref-theorem",~1,[thm]) fun flt_pat @{mpat "pure (the_pure ?A)"} = SOME A | flt_pat _ = NONE val purify_terms = (list_filtered_subterms flt_pat R @ list_filtered_subterms flt_pat S) |> distinct op aconv val thm = fold (add_is_pure_constraint ctxt) purify_terms thm in val thm = thm end val thm = thm |> Local_Defs.unfold0 ctxt xform_thms |> Local_Defs.unfold0 ctxt rprops_thms val insts = map (fn @{mpat "Trueprop (CONSTRAINT _ (the_pure _))"} => @{thm handle_purity1} | _ => asm_rl ) (Thm.prems_of thm) val thm = (thm OF insts) |> Conv.fconv_rule Thm.eta_conversion |> simp @{thms handle_purity2} |> simp simp_thms val thm = singleton (Variable.export ctxt orig_ctxt) thm in thm end end fun simp_precond_tac ctxt = let fun simp_only thms = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps thms) val rtac = resolve_tac ctxt val cnv_ss = ctxt delsimps @{thms CNV_def} (*val uncurry_tac = SELECT_GOAL (ALLGOALS (DETERM o SOLVED' ( REPEAT' (rtac @{thms auto_weaken_pre_uncurry_step'}) THEN' rtac @{thms auto_weaken_pre_uncurry_finish} )))*) val prove_cnv_tac = SOLVED' (rtac @{thms CNV_prove} THEN' SELECT_GOAL (auto_tac ctxt)) val do_cnv_tac = (cp_clarsimp_tac cnv_ss) THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms CNV_split})) THEN_ALL_NEW (prove_cnv_tac ORELSE' rtac @{thms CNV_I}) val final_simp_tac = rtac @{thms simp_pre_final_simp} THEN' cp_clarsimp_tac cnv_ss THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "final_simp_tac: Before CNV_I") ctxt THEN' rtac @{thms CNV_I} THEN' dbg_msg_tac (Sepref_Debugging.msg_text "Final-Simp done") ctxt (*val curry_tac = let open Conv in CONVERSION (Refine_Util.HOL_concl_conv (fn ctxt => arg1_conv ( top_conv ( fn _ => try_conv (rewr_conv @{thm uncurry_def})) ctxt)) ctxt) THEN' REPEAT' (EqSubst.eqsubst_tac ctxt [1] @{thms case_prod_eta}) THEN' rtac @{thms CNV_I} end*) val simp_tupled_pre_tac = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms prod_casesK uncurry0_hfref_post}) THEN' REPEAT' (EqSubst.eqsubst_tac ctxt [1] @{thms case_prod_eta}) THEN' rtac @{thms CNV_I} val unfold_and_tac = rtac @{thms and_pre_beta} THEN_ALL_NEW simp_only @{thms split} val simp_and1_tac = rtac @{thms simp_and1} THEN' do_cnv_tac val simp_and2_tac = rtac @{thms simp_and2} THEN' do_cnv_tac val and_plan_tac = simp_and1_tac THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "State after and1") ctxt THEN' ( rtac @{thms triv_and1} ORELSE' dbg_msg_tac (Sepref_Debugging.msg_subgoal "Invoking and2 on") ctxt THEN' simp_and2_tac THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "State before final_simp_tac") ctxt THEN' final_simp_tac ) val unfold_imp_tac = rtac @{thms imp_pre_beta} THEN_ALL_NEW simp_only @{thms split} val simp_imp1_tac = rtac @{thms simp_imp} THEN' do_cnv_tac val imp_plan_tac = simp_imp1_tac THEN' final_simp_tac val imp_pre_tac = APPLY_LIST [ simp_only @{thms split_tupled_all} THEN' Refine_Util.instantiate_tuples_subgoal_tac ctxt THEN' CASES' [ (unfold_and_tac, ALLGOALS and_plan_tac), (unfold_imp_tac, ALLGOALS imp_plan_tac) ] , simp_tupled_pre_tac ] val imp_pre_custom_tac = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms and_pre_def}) THEN' TRY o SOLVED' (SELECT_GOAL (auto_tac ctxt)) in CASES' [ (rtac @{thms IMP_PRE_eqI}, imp_pre_tac 1), (rtac @{thms IMP_PRE_CUSTOMI}, ALLGOALS imp_pre_custom_tac) ] end local fun inf_bn_aux name = case String.tokens (fn c => c = #".") name of [] => NONE | [a] => SOME (Binding.name a) | (_::a::_) => SOME (Binding.name a) in fun infer_basename (Const ("_type_constraint_",_)$t) = infer_basename t | infer_basename (Const (name,_)) = inf_bn_aux name | infer_basename (Free (name,_)) = inf_bn_aux name | infer_basename _ = NONE end val cfg_mop = Attrib.setup_config_bool @{binding sepref_register_mop} (K true) val cfg_ismop = Attrib.setup_config_bool @{binding sepref_register_ismop} (K false) val cfg_rawgoals = Attrib.setup_config_bool @{binding sepref_register_rawgoals} (K false) val cfg_transfer = Attrib.setup_config_bool @{binding sepref_decl_impl_transfer} (K true) val cfg_def = Attrib.setup_config_bool @{binding sepref_register_def} (K true) val cfg_register = Attrib.setup_config_bool @{binding sepref_decl_impl_register} (K true) local open Refine_Util val flags = parse_bool_config' "mop" cfg_mop || parse_bool_config' "ismop" cfg_ismop || parse_bool_config' "rawgoals" cfg_rawgoals || parse_bool_config' "def" cfg_def val parse_flags = parse_paren_list' flags val parse_name = Scan.option (Parse.binding --| @{keyword ":"}) val parse_relconds = Scan.optional (@{keyword "where"} |-- Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat) [] in val do_parser = parse_flags -- parse_name -- Parse.term --| @{keyword "::"} -- Parse.term -- parse_relconds end fun do_cmd ((((flags,name),opt_raw), relt_raw),relconds_raw) lthy = let local val ctxt = Refine_Util.apply_configs flags lthy in val flag_ismop = Config.get ctxt cfg_ismop val flag_mop = Config.get ctxt cfg_mop andalso not flag_ismop val flag_rawgoals = Config.get ctxt cfg_rawgoals val flag_def = Config.get ctxt cfg_def end open Sepref_Basic Sepref_Rules val relt = Syntax.parse_term lthy relt_raw val relconds = map (Syntax.parse_prop lthy) relconds_raw val _ = dbg_trace lthy "Parse relation and relation conditions together" val relt = Const (@{const_name "Pure.term"}, dummyT) $ relt local val l = Syntax.check_props lthy (relt::relconds) in val (relt, relconds) = (hd l, tl l) end val relt = Logic.dest_term relt val opt_pre = Syntax.parse_term lthy opt_raw val _ = dbg_trace lthy "Infer basename" val name = case name of SOME name => name | NONE => ( case infer_basename opt_pre of NONE => (error "Could not infer basename: You have to specify a basename"; Binding.empty) | SOME name => name ) fun qname s n = Binding.qualify true (Binding.name_of n) (Binding.name s) fun def name t_pre attribs lthy = let val t = Syntax.check_term lthy t_pre (*|> Thm.cterm_of lthy |> Drule.mk_term |> Local_Defs.unfold0 lthy @{thms PR_CONST_def} |> Drule.dest_term |> Thm.term_of*) val (_,lthy) = Local_Theory.open_target lthy val ((dt,(_,thm)),lthy) = Local_Theory.define ((name,Mixfix.NoSyn),((Thm.def_binding name,@{attributes [code]}@attribs),t)) lthy; val (lthy, lthy_old) = `Local_Theory.close_target lthy val phi = Proof_Context.export_morphism lthy_old lthy val thm = Morphism.thm phi thm val dt = Morphism.term phi dt in ((dt,thm),lthy) end val _ = dbg_trace lthy "Analyze Relation" val (pre,args,res) = analyze_rel relt val specified_pre = is_some pre val pre = the_default (mk_triv_precond args) pre val def_thms = @{thms PR_CONST_def} val _ = dbg_trace lthy "Define op" val op_name = Binding.prefix_name (if flag_ismop then "mop_" else "op_") name val (def_thms,opc,lthy) = if flag_def then let val ((opc,op_def_thm),lthy) = def op_name opt_pre @{attributes [simp]} lthy val opc = Refine_Util.dummify_tvars opc val def_thms = op_def_thm::def_thms in (def_thms,opc,lthy) end else let val _ = dbg_trace lthy "Refine type of opt_pre to get opc" val opc = Syntax.check_term lthy opt_pre val new_ctxt = Variable.declare_term opc lthy val opc = singleton (Variable.export_terms new_ctxt lthy) opc |> Refine_Util.dummify_tvars in (def_thms,opc,lthy) end (* PR_CONST Heuristics *) fun pr_const_heuristics basename c_pre lthy = let val _ = dbg_trace lthy ("PR_CONST heuristics " ^ @{make_string} c_pre) val c = Syntax.check_term lthy c_pre in case c of @{mpat "PR_CONST _"} => ((c_pre,false),lthy) | Const _ => ((c_pre,false),lthy) | _ => let val (f,args) = strip_comb c val lthy = case f of Const _ => let val ctxt = Variable.declare_term c lthy val lhs = Autoref_Tagging.list_APP (f,args) val rhs = @{mk_term "UNPROTECT ?c"} val goal = Logic.mk_equals (lhs,rhs) |> Thm.cterm_of ctxt val tac = Local_Defs.unfold0_tac ctxt @{thms APP_def UNPROTECT_def} THEN ALLGOALS (simp_tac (put_simpset HOL_basic_ss ctxt)) val thm = Goal.prove_internal ctxt [] goal (K tac) |> singleton (Variable.export ctxt lthy) val (_,lthy) = Local_Theory.note ((Binding.suffix_name "_def_pat" basename,@{attributes [def_pat_rules]}),[thm]) lthy val _ = Thm.pretty_thm lthy thm |> Pretty.string_of |> writeln in lthy end | _ => ( Pretty.block [ Pretty.str "Complex operation pattern. Added PR_CONST but no pattern rules:", Pretty.brk 1,Syntax.pretty_term lthy c] |> Pretty.string_of |> warning ; lthy) val c_pre = Const(@{const_name PR_CONST},dummyT)$c_pre in ((c_pre,true),lthy) end end val ((opc,_),lthy) = pr_const_heuristics op_name opc lthy (* Register *) val arg_intfs = map (get_intf_of_rel lthy) args val res_intf = get_intf_of_rel lthy res fun register basename c lthy = let val _ = dbg_trace lthy "Register" open Sepref_Basic val c = Syntax.check_term lthy c val ri = case (is_nresT (body_type (fastype_of c)), is_nresT res_intf) of (true,false) => mk_nresT res_intf | (false,true) => dest_nresT res_intf | _ => res_intf val iT = arg_intfs ---> ri val ((_,itype_thm),lthy) = Sepref_Combinator_Setup.sepref_register_single (Binding.name_of basename) c iT lthy val _ = Thy_Output.pretty_thm lthy itype_thm |> Pretty.string_of |> writeln in lthy end val lthy = register op_name opc lthy val _ = dbg_trace lthy "Define pre" val pre_name = Binding.prefix_name "pre_" name val ((prec,pre_def_thm),lthy) = def pre_name pre @{attributes [simp]} lthy val prec = Refine_Util.dummify_tvars prec val def_thms = pre_def_thm::def_thms (* Re-integrate pre-constant into type-context of relation. TODO: This is probably not clean/robust *) val pre = constrain_type_pre (fastype_of pre) prec |> Syntax.check_term lthy val _ = dbg_trace lthy "Convert both, relation and operation to uncurried form, and add nres" val _ = dbg_trace lthy "Convert relation (arguments have already been separated by analyze-rel)" val res = case res of @{mpat "\_\nres_rel"} => res | _ => @{mk_term "\?res\nres_rel"} val relt = mk_rel (SOME pre,args,res) val _ = dbg_trace lthy "Convert operation" val opcT = fastype_of (Syntax.check_term lthy opc) val op_is_nres = Sepref_Basic.is_nresT (body_type opcT) val (opcu, op_ar) = let val arity = binder_types #> length (* Arity of operation is number of arguments before result (which may be a fun-type! )*) val res_ar = arity (Relators.rel_absT res |> not op_is_nres ? dest_nresT) val op_ar = arity opcT - res_ar val _ = op_ar = length args orelse raise TERM("Operation/relation arity mismatch: " ^ string_of_int op_ar ^ " vs " ^ string_of_int (length args),[opc,relt]) (* Add RETURN o...o if necessary*) val opc = if op_is_nres then opc else mk_compN_pre op_ar (Const(@{const_name Refine_Basic.RETURN},dummyT)) opc (* Add uncurry if necessary *) val opc = mk_uncurryN_pre op_ar opc in (opc, op_ar) end (* Build mop-variant *) val declare_mop = (specified_pre orelse not op_is_nres) andalso flag_mop val (mop_data,lthy) = if declare_mop then let val _ = dbg_trace lthy "mop definition" val mop_rhs = Const(@{const_name mop},dummyT) $ prec $ opcu |> mk_curryN_pre op_ar val mop_name = Binding.prefix_name "mop_" name val ((mopc,mop_def_thm),lthy) = def mop_name mop_rhs [] lthy val mopc = Refine_Util.dummify_tvars mopc val ((mopc,added_pr_const),lthy) = pr_const_heuristics mop_name mopc lthy val mop_def_thm' = if added_pr_const then mop_def_thm RS @{thm add_PR_CONST_to_def} else mop_def_thm val (_,lthy) = Local_Theory.note ((Binding.empty, @{attributes [sepref_mop_def_thms]}),[mop_def_thm']) lthy val _ = dbg_trace lthy "mop alternative definition" val alt_unfolds = @{thms mop_alt_unfolds} |> not specified_pre ? curry op :: pre_def_thm val mop_alt_thm = Local_Defs.unfold0 lthy alt_unfolds mop_def_thm |> Refine_Util.shift_lambda_leftN op_ar val (_,lthy) = Local_Theory.note ((Binding.suffix_name "_alt" mop_name,@{attributes [simp]}),[mop_alt_thm]) lthy val _ = dbg_trace lthy "mop: register" val lthy = register mop_name mopc lthy val _ = dbg_trace lthy "mop: vcg theorem" local val Ts = map Relators.rel_absT args val ctxt = Variable.declare_thm mop_def_thm lthy val ctxt = fold Variable.declare_typ Ts ctxt val (x,ctxt) = Refine_Util.fix_left_tuple_from_Ts "x" Ts ctxt val mop_def_thm = mop_def_thm |> Local_Defs.unfold0 ctxt @{thms curry_shl} fun prep_thm thm = (thm OF [mop_def_thm]) |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt x)] |> Local_Defs.unfold0 ctxt @{thms uncurry_apply uncurry0_apply o_apply} |> Local_Defs.unfold0 ctxt (def_thms @ @{thms Product_Type.split HOL.True_implies_equals}) |> singleton (Variable.export ctxt lthy) val thms = map prep_thm @{thms mop_spec_rl_from_def mop_leof_rl_from_def} in val (_,lthy) = Local_Theory.note ((qname "vcg" mop_name,@{attributes [refine_vcg]}),thms) lthy end in (SOME (mop_name,mopc,mop_def_thm),lthy) end else (NONE,lthy) val _ = dbg_trace lthy "Build Parametricity Theorem" val param_t = mk_pair_in_pre opcu opcu relt |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds val _ = dbg_trace lthy "Build Parametricity Theorem for Precondition" val param_pre_t = let val pre_relt = Relators.mk_fun_rel (Relators.list_prodrel_left args) @{term bool_rel} val param_pre_t = mk_pair_in_pre prec prec pre_relt |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds in param_pre_t end val _ = dbg_trace lthy "Build goals" val goals = [[ (param_t, []), (param_pre_t, []) ]] fun after_qed [[p_thm, pp_thm]] _ (*ctxt*) = let val _ = dbg_trace lthy "after_qed" val p_thm' = p_thm |> not specified_pre ? Local_Defs.unfold0 lthy [pre_def_thm] val (_,lthy) = Local_Theory.note ((qname "fref" op_name,@{attributes [sepref_fref_thms]}), [p_thm']) lthy val (_,lthy) = Local_Theory.note ((qname "param" pre_name,@{attributes [param]}), [pp_thm]) lthy val p'_unfolds = pre_def_thm :: @{thms True_implies_equals} val (_,lthy) = Local_Theory.note ((qname "fref'" op_name,[]), [Local_Defs.unfold0 lthy p'_unfolds p_thm]) lthy val lthy = case mop_data of NONE => lthy | SOME (mop_name,mopc,mop_def_thm) => let val _ = dbg_trace lthy "Build and prove mop-stuff" (* mop - parametricity theorem: (uncurry\<^sup>n mopc,uncurry\<^sup>n mopc) \ args \\<^sub>f res *) val mopcu = mk_uncurryN_pre op_ar mopc val param_mop_t = mk_pair_in_pre mopcu mopcu (mk_rel (NONE,args,res)) |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds - val ctxt = Variable.auto_fixes param_mop_t lthy + val ctxt = Proof_Context.augment param_mop_t lthy val tac = let val p_thm = Local_Defs.unfold0 ctxt @{thms PR_CONST_def} p_thm in Local_Defs.unfold0_tac ctxt (mop_def_thm :: @{thms PR_CONST_def uncurry_curry_id uncurry_curry0_id}) THEN FIRSTGOAL ( dbg_msg_tac (Sepref_Debugging.msg_subgoal "Mop-param thm goal after unfolding") ctxt THEN' resolve_tac ctxt @{thms param_mopI} THEN' SOLVED' (resolve_tac ctxt [p_thm] THEN_ALL_NEW assume_tac ctxt) THEN' SOLVED' (resolve_tac ctxt [pp_thm] THEN_ALL_NEW assume_tac ctxt) ) end val pm_thm = Goal.prove_internal lthy [] (Thm.cterm_of ctxt param_mop_t) (K tac) |> singleton (Variable.export ctxt lthy) val (_,lthy) = Local_Theory.note ((qname "fref" mop_name,@{attributes [sepref_fref_thms]}), [pm_thm]) lthy val (_,lthy) = Local_Theory.note ((qname "fref'" mop_name,[]), [Local_Defs.unfold0 lthy p'_unfolds pm_thm]) lthy in lthy end in lthy end | after_qed thmss _ = raise THM ("After-qed: Wrong thmss structure",~1,flat thmss) fun std_tac ctxt = let val ptac = REPEAT_ALL_NEW_FWD (Parametricity.net_tac (Parametricity.get_dflt ctxt) ctxt) (* Massage simpset a bit *) val ctxt = ctxt |> Context_Position.set_visible false |> Context.proof_map (Thm.attribute_declaration Clasimp.iff_del @{thm pair_in_Id_conv}) in if flag_rawgoals then all_tac else Local_Defs.unfold0_tac ctxt def_thms THEN ALLGOALS ( TRY o SOLVED' ( TRY o resolve_tac ctxt @{thms frefI} THEN' TRY o REPEAT_ALL_NEW (ematch_tac ctxt @{thms prod_relE}) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split uncurry_apply uncurry0_apply}) THEN' ( SOLVED' (ptac THEN_ALL_NEW asm_full_simp_tac ctxt) ORELSE' SOLVED' (cp_clarsimp_tac ctxt THEN_ALL_NEW_FWD ptac THEN_ALL_NEW SELECT_GOAL (auto_tac ctxt)) ) ) ) end val rf_std = Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (std_tac ctxt))) #> Seq.the_result "do_cmd: Standard proof tactic returned empty result sequence" in Proof.theorem NONE after_qed goals lthy |> rf_std end val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "sepref_decl_op"} "" (do_parser >> do_cmd) local fun unfold_PR_CONST_tac ctxt = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms PR_CONST_def}) fun transfer_precond_rl ctxt t R = let (*val tfrees = Term.add_tfreesT (fastype_of t) [] val t' = map_types (map_type_tfree (fn x => if member op= tfrees x then dummyT else TFree x)) t *) (* TODO: Brute force approach, that may generalize too much! *) val t' = map_types (K dummyT) t val goal = Sepref_Basic.mk_pair_in_pre t t' R |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val thm = Drule.infer_instantiate' ctxt [NONE,SOME goal] @{thm IMP_LIST_trivial} in thm end (* Generate a hnr-thm for mop given one for op *) fun generate_mop_thm ctxt op_thm = let val orig_ctxt = ctxt val (op_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) op_thm ctxt (* Convert mop_def_thms to form uncurry^n f \ mop P g *) val mop_def_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_mop_def_thms} |> map (Local_Defs.unfold0 ctxt @{thms curry_shl}) fun fail_hnr_tac _ _ = raise THM("Invalid hnr-theorem",~1,[op_thm]) fun fail_mop_def_tac i st = let val g = nth (Thm.prems_of st) (i-1) in raise TERM("Found no matching mop-definition",[g]) end (* Tactic to solve preconditions of hfref_op_to_mop *) val tac = APPLY_LIST [ resolve_tac ctxt [op_thm] ORELSE' fail_hnr_tac, ((*unfold_PR_CONST_tac ctxt THEN'*) resolve_tac ctxt mop_def_thms) ORELSE' fail_mop_def_tac, simp_precond_tac ctxt ORELSE' Sepref_Debugging.error_tac' "precond simplification failed" ctxt ] 1 (* Do synthesis *) val st = @{thm hfref_op_to_mop} val st = Goal.protect (Thm.nprems_of st) st val mop_thm = tac st |> Seq.hd |> Goal.conclude val mop_thm = singleton (Variable.export ctxt orig_ctxt) mop_thm |> Sepref_Rules.norm_fcomp_rule orig_ctxt in mop_thm end (* Generate a hnr-thm for op given one for mop *) fun generate_op_thm ctxt mop_thm = let (* TODO: Almost-clone of generate_mop_thm *) val orig_ctxt = ctxt val (mop_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) mop_thm ctxt (* Convert mop_def_thms to form uncurry^n f \ mop P g *) val mop_def_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_mop_def_thms} |> map (Local_Defs.unfold0 ctxt @{thms curry_shl}) fun fail_hnr_tac _ _ = raise THM("Invalid hnr-theorem",~1,[mop_thm]) fun fail_mop_def_tac i st = let val g = nth (Thm.prems_of st) (i-1) in raise TERM("Found no matching mop-definition",[g]) end (* Tactic to solve preconditions of hfref_mop_to_op *) val tac = APPLY_LIST [ resolve_tac ctxt [mop_thm] ORELSE' fail_hnr_tac, ((*unfold_PR_CONST_tac ctxt THEN'*) resolve_tac ctxt mop_def_thms) ORELSE' fail_mop_def_tac, simp_precond_tac ctxt ORELSE' Sepref_Debugging.error_tac' "precond simplification failed" ctxt ] 1 (* Do synthesis *) val st = @{thm hfref_mop_to_op} val st = Goal.protect (Thm.nprems_of st) st val op_thm = tac st |> Seq.hd |> Goal.conclude val op_thm = singleton (Variable.export ctxt orig_ctxt) op_thm |> Sepref_Rules.norm_fcomp_rule orig_ctxt in op_thm end fun chk_result ctxt thm = let val (_,R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\hfref ?P ?R ?S)"} => (P,R,S) | _ => raise THM("chk_result: Expected hfref-theorem",~1,[thm]) fun err t = let val ts = Syntax.pretty_term ctxt t |> Pretty.string_of in raise THM ("chk_result: Invalid pattern left in assertions: " ^ ts,~1,[thm]) end fun check_invalid (t as @{mpat "hr_comp _ _"}) = err t | check_invalid (t as @{mpat "hrp_comp _ _"}) = err t | check_invalid (t as @{mpat "pure (the_pure _)"}) = err t | check_invalid (t as @{mpat "_ O _"}) = err t | check_invalid _ = false val _ = exists_subterm check_invalid R val _ = exists_subterm check_invalid S in () end fun to_IMP_LIST ctxt thm = (thm RS @{thm to_IMP_LISTI}) |> Local_Defs.unfold0 ctxt @{thms to_IMP_LIST} fun from_IMP_LIST ctxt thm = thm |> Local_Defs.unfold0 ctxt @{thms from_IMP_LIST} in local open Refine_Util val flags = parse_bool_config' "mop" cfg_mop || parse_bool_config' "ismop" cfg_ismop || parse_bool_config' "transfer" cfg_transfer || parse_bool_config' "rawgoals" cfg_rawgoals || parse_bool_config' "register" cfg_register val parse_flags = parse_paren_list' flags val parse_precond = Scan.option (@{keyword "["} |-- Parse.term --| @{keyword "]"}) val parse_fref_thm = Scan.option (@{keyword "uses"} |-- Parse.thm) in val di_parser = parse_flags -- Scan.optional (Parse.binding --| @{keyword ":"}) Binding.empty -- parse_precond -- Parse.thm -- parse_fref_thm end fun di_cmd ((((flags,name), precond_raw), i_thm_raw), p_thm_raw) lthy = let val i_thm = singleton (Attrib.eval_thms lthy) i_thm_raw val p_thm = map_option (singleton (Attrib.eval_thms lthy)) p_thm_raw local val ctxt = Refine_Util.apply_configs flags lthy in val flag_mop = Config.get ctxt cfg_mop val flag_ismop = Config.get ctxt cfg_ismop val flag_rawgoals = Config.get ctxt cfg_rawgoals val flag_transfer = Config.get ctxt cfg_transfer val flag_register = Config.get ctxt cfg_register end val fr_attribs = if flag_register then @{attributes [sepref_fr_rules]} else [] val ctxt = lthy (* Compose with fref-theorem *) val _ = dbg_trace lthy "Compose with fref" local val hf_tcomp_pre = @{thm hfcomp_tcomp_pre} OF [asm_rl,i_thm] fun compose p_thm = let val p_thm = p_thm |> to_assns_rl false lthy in hf_tcomp_pre OF [p_thm] end in val thm = case p_thm of SOME p_thm => compose p_thm | NONE => let val p_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_fref_thms} fun err () = let val prem_s = nth (Thm.prems_of hf_tcomp_pre) 0 |> Syntax.pretty_term ctxt |> Pretty.string_of in error ("Found no fref-theorem matching " ^ prem_s) end in case get_first (try compose) p_thms of NONE => err () | SOME thm => thm end end val (thm,ctxt) = yield_singleton (apfst snd oo Variable.import true) thm ctxt val _ = dbg_trace lthy "Transfer Precond" val thm = to_IMP_LIST ctxt thm val thm = thm RS @{thm transform_pre_param} local val (pre,R,pp_name,pp_type) = case Thm.prems_of thm of [@{mpat "Trueprop (IMP_LIST _ ((?pre,_)\?R))"}, @{mpat "Trueprop (IMP_PRE (mpaq_STRUCT (mpaq_Var ?pp_name ?pp_type)) _)"}] => (pre,R,pp_name,pp_type) | _ => raise THM("di_cmd: Cannot recognize first prems of transform_pre_param: ", ~1,[thm]) in val thm = if flag_transfer then thm OF [transfer_precond_rl ctxt pre R] else thm val thm = case precond_raw of NONE => thm | SOME precond_raw => let val precond = Syntax.parse_term ctxt precond_raw |> Sepref_Basic.constrain_type_pre pp_type |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val thm = Drule.infer_instantiate ctxt [(pp_name,precond)] thm val thm = thm OF [asm_rl,@{thm IMP_PRE_CUSTOMD}] in thm end end val _ = dbg_trace lthy "Build goals" val goals = [map (fn x => (x,[])) (Thm.prems_of thm)] fun after_qed thmss _ = let val _ = dbg_trace lthy "After QED" val prems_thms = hd thmss val thm = thm OF prems_thms val thm = from_IMP_LIST ctxt thm (* Two rounds of cleanup-constraints, norm_fcomp *) val _ = dbg_trace lthy "Cleanup" val thm = thm |> cleanup_constraints ctxt |> Sepref_Rules.norm_fcomp_rule ctxt |> cleanup_constraints ctxt |> Sepref_Rules.norm_fcomp_rule ctxt val thm = thm |> singleton (Variable.export ctxt lthy) |> zero_var_indexes val _ = dbg_trace lthy "Check Result" val _ = chk_result lthy thm fun qname suffix = if Binding.is_empty name then name else Binding.suffix_name suffix name val thm_name = if flag_ismop then qname "_hnr_mop" else qname "_hnr" val (_,lthy) = Local_Theory.note ((thm_name,fr_attribs),[thm]) lthy val _ = Thm.pretty_thm lthy thm |> Pretty.string_of |> writeln (* Create mop theorem from op-theorem *) val cr_mop_thm = flag_mop andalso not flag_ismop val lthy = if cr_mop_thm then let val _ = dbg_trace lthy "Create mop-thm" val mop_thm = thm |> generate_mop_thm lthy |> zero_var_indexes val (_,lthy) = Local_Theory.note ((qname "_hnr_mop",fr_attribs),[mop_thm]) lthy val _ = Thm.pretty_thm lthy mop_thm |> Pretty.string_of |> writeln in lthy end else lthy (* Create op theorem from mop-theorem *) val cr_op_thm = flag_ismop val lthy = if cr_op_thm then let val _ = dbg_trace lthy "Create op-thm" val op_thm = thm |> generate_op_thm lthy |> zero_var_indexes val (_,lthy) = Local_Theory.note ((qname "_hnr",fr_attribs),[op_thm]) lthy val _ = Thm.pretty_thm lthy op_thm |> Pretty.string_of |> writeln in lthy end else lthy in lthy end fun std_tac ctxt = let val ptac = REPEAT_ALL_NEW_FWD ( Parametricity.net_tac (Parametricity.get_dflt ctxt) ctxt ORELSE' assume_tac ctxt ) in if flag_rawgoals orelse not flag_transfer then all_tac else APPLY_LIST [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms from_IMP_LIST}) THEN' TRY o SOLVED' ptac, simp_precond_tac ctxt ] 1 end val rf_std = Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (std_tac ctxt))) #> Seq.the_result "di_cmd: Standard proof tactic returned empty result sequence" in Proof.theorem NONE after_qed goals ctxt |> rf_std end val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "sepref_decl_impl"} "" (di_parser >> di_cmd) end end \ subsection \Obsolete Manual Specification Helpers\ (* Generate VCG-rules for operations *) lemma vcg_of_RETURN_np: assumes "f \ RETURN r" shows "SPEC (\x. x=r) \ m \ f \ m" and "SPEC (\x. x=r) \\<^sub>n m \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff) lemma vcg_of_RETURN: assumes "f \ do { ASSERT \; RETURN r }" shows "\\; SPEC (\x. x=r) \ m\ \ f \ m" and "\\ \ SPEC (\x. x=r) \\<^sub>n m\ \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps) lemma vcg_of_SPEC: assumes "f \ do { ASSERT pre; SPEC post }" shows "\pre; SPEC post \ m\ \ f \ m" and "\pre \ SPEC post \\<^sub>n m\ \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps) lemma vcg_of_SPEC_np: assumes "f \ SPEC post" shows "SPEC post \ m \ f \ m" and "SPEC post \\<^sub>n m \ f \\<^sub>n m" using assms by auto (* Generate parametricity rules to generalize plain operations to monadic ones. Use with FCOMP. *) lemma mk_mop_rl1: assumes "\x. mf x \ ASSERT (P x) \ RETURN (f x)" shows "(RETURN o f, mf) \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl2: assumes "\x y. mf x y \ ASSERT (P x y) \ RETURN (f x y)" shows "(RETURN oo f, mf) \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl3: assumes "\x y z. mf x y z \ ASSERT (P x y z) \ RETURN (f x y z)" shows "(RETURN ooo f, mf) \ Id \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl0_np: assumes "mf \ RETURN f" shows "(RETURN f, mf) \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl1_np: assumes "\x. mf x \ RETURN (f x)" shows "(RETURN o f, mf) \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl2_np: assumes "\x y. mf x y \ RETURN (f x y)" shows "(RETURN oo f, mf) \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl3_np: assumes "\x y z. mf x y z \ RETURN (f x y z)" shows "(RETURN ooo f, mf) \ Id \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_op_rl0_np: assumes "mf \ RETURN f" shows "(uncurry0 mf, uncurry0 (RETURN f)) \ unit_rel \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl1: assumes "\x. mf x \ ASSERT (P x) \ RETURN (f x)" shows "(mf, RETURN o f) \ [P]\<^sub>f Id \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl1_np: assumes "\x. mf x \ RETURN (f x)" shows "(mf, (RETURN o f)) \ Id \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl2: assumes "\x y. mf x y \ ASSERT (P x y) \ RETURN (f x y)" shows "(uncurry mf, uncurry (RETURN oo f)) \ [uncurry P]\<^sub>f Id\\<^sub>rId \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl2_np: assumes "\x y. mf x y \ RETURN (f x y)" shows "(uncurry mf, uncurry (RETURN oo f)) \ Id\\<^sub>rId \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl3: assumes "\x y z. mf x y z \ ASSERT (P x y z) \ RETURN (f x y z)" shows "(uncurry2 mf, uncurry2 (RETURN ooo f)) \ [uncurry2 P]\<^sub>f (Id\\<^sub>rId)\\<^sub>rId \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl3_np: assumes "\x y z. mf x y z \ RETURN (f x y z)" shows "(uncurry2 mf, uncurry2 (RETURN ooo f)) \ (Id\\<^sub>rId)\\<^sub>rId \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done end