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,1377 +1,1376 @@ (* 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 = TVars.make (paramTs ~~ map TFree tfrees); val params = map (apsnd (Term_Subst.instantiateT instT)) (rev (Term.add_vars pt [])); val (frees, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) params) ctxt'; val inst = Vars.make (params ~~ map Free (frees ~~ map #2 params)); val pt' = Term_Subst.instantiate (instT, inst) pt; in (unpack_poly_terms pt', ctxt'') end; (** Internal representation **) (* Applicative functors *) type rel_thms = { pure_transfer: thm, ap_rel_fun: thm }; fun map_rel_thms f {pure_transfer, ap_rel_fun} = {pure_transfer = f pure_transfer, ap_rel_fun = f ap_rel_fun}; type afun_thms = { hom: thm, ichng: thm, reds: thm Symtab.table, rel_thms: rel_thms option, rel_intros: thm list, pure_comp_conv: thm }; fun map_afun_thms f {hom, ichng, reds, rel_thms, rel_intros, pure_comp_conv} = {hom = f hom, ichng = f ichng, reds = Symtab.map (K f) reds, rel_thms = Option.map (map_rel_thms f) rel_thms, rel_intros = map f rel_intros, pure_comp_conv = f pure_comp_conv}; datatype afun = AFun of { name: binding, terms: term, rel: term option, thms: afun_thms, unfolds: thm Item_Net.T }; fun rep_afun (AFun af) = af; val name_of_afun = #name o rep_afun; val terms_of_afun = #terms o rep_afun; val rel_of_afun = #rel o rep_afun; val thms_of_afun = #thms o rep_afun; val unfolds_of_afun = Item_Net.content o #unfolds o rep_afun; val red_of_afun = Symtab.lookup o #reds o thms_of_afun; val has_red_afun = is_some oo red_of_afun; fun mk_afun name terms rel thms = AFun {name = name, terms = terms, rel = rel, thms = thms, unfolds = Thm.item_net}; fun map_afun f1 f2 f3 f4 f5 (AFun {name, terms, rel, thms, unfolds}) = AFun {name = f1 name, terms = f2 terms, rel = f3 rel, thms = f4 thms, unfolds = f5 unfolds}; fun map_unfolds f thms = fold Item_Net.update (map f (Item_Net.content thms)) Thm.item_net; fun morph_afun phi = let val binding = Morphism.binding phi; val term = Morphism.term phi; val thm = Morphism.thm phi; in map_afun binding term (Option.map term) (map_afun_thms thm) (map_unfolds thm) end; val transfer_afun = morph_afun o Morphism.transfer_morphism; fun add_unfolds_afun thms = map_afun I I I I (fold Item_Net.update thms); fun patterns_of_afun af = let val [Tt, (_, pure), (_, ap), _] = unpack_poly_terms (terms_of_afun af); val (_, T) = poly_type_of_term Tt; in [#2 (mk_comb_pattern (pure, 1)), #2 (mk_comb_pattern (ap, 2)), Net.encode_type T] end; (* Combinator rules *) datatype combinator_rule = Combinator_Rule of { strong_premises: string Ord_List.T, weak_premises: bool, conclusion: string, eq_thm: thm }; fun rep_combinator_rule (Combinator_Rule rule) = rule; val conclusion_of_rule = #conclusion o rep_combinator_rule; val thm_of_rule = #eq_thm o rep_combinator_rule; fun eq_combinator_rule (rule1, rule2) = pointer_eq (rule1, rule2) orelse Thm.eq_thm (thm_of_rule rule1, thm_of_rule rule2); fun is_applicable_rule rule have_weak have_premises = let val {strong_premises, weak_premises, ...} = rep_combinator_rule rule; in (have_weak orelse not weak_premises) andalso have_premises strong_premises end; fun map_combinator_rule f1 f2 f3 f4 (Combinator_Rule {strong_premises, weak_premises, conclusion, eq_thm}) = Combinator_Rule {strong_premises = f1 strong_premises, weak_premises = f2 weak_premises, conclusion = f3 conclusion, eq_thm = f4 eq_thm}; fun transfer_combinator_rule thy = map_combinator_rule I I I (Thm.transfer thy); fun mk_combinator_rule comb_names weak_premises thm = let val (lhs, rhs) = Logic.dest_equals (Thm.prop_of thm); val conclusion = the (Symtab.lookup comb_names (#1 (dest_Const lhs))); val premises = Ord_List.make fast_string_ord (fold_options (map (Symtab.lookup comb_names o #1) (Term.add_consts rhs []))); val weak_premises' = Ord_List.make fast_string_ord (these weak_premises); val strong_premises = Ord_List.subtract fast_string_ord weak_premises' premises; in Combinator_Rule {strong_premises = strong_premises, weak_premises = is_some weak_premises, conclusion = conclusion, eq_thm = thm} end; (* Generic data *) (*FIXME: needs tests, especially around theory merging*) fun merge_afuns _ (af1, af2) = if pointer_eq (af1, af2) then raise Change_Table.SAME else map_afun I I I I (fn thms1 => Item_Net.merge (thms1, #unfolds (rep_afun af2))) af1; structure Data = Generic_Data ( type T = { combinators: thm Symtab.table * combinator_rule list, afuns: afun Name_Space.table, patterns: (string * term list) Item_Net.T }; val empty = { combinators = (Symtab.empty, []), afuns = Name_Space.empty_table "applicative functor", patterns = Item_Net.init (op = o apply2 #1) #2 }; - val extend = I; fun merge ({combinators = (cd1, cr1), afuns = a1, patterns = p1}, {combinators = (cd2, cr2), afuns = a2, patterns = p2}) = {combinators = (Symtab.merge (K true) (cd1, cd2), Library.merge eq_combinator_rule (cr1, cr2)), afuns = Name_Space.join_tables merge_afuns (a1, a2), patterns = Item_Net.merge (p1, p2)}; ); fun get_combinators context = let val thy = Context.theory_of context; val {combinators = (defs, rules), ...} = Data.get context; in (Symtab.map (K (Thm.transfer thy)) defs, map (transfer_combinator_rule thy) rules) end; val get_afun_table = #afuns o Data.get; val get_afun_space = Name_Space.space_of_table o get_afun_table; val get_patterns = #patterns o Data.get; fun map_data f1 f2 f3 {combinators, afuns, patterns} = {combinators = f1 combinators, afuns = f2 afuns, patterns = f3 patterns}; val intern = Name_Space.intern o get_afun_space; fun extern context = Name_Space.extern (Context.proof_of context) (get_afun_space context); local fun undeclared name = error ("Undeclared applicative functor " ^ quote name); in fun afun_of_generic context name = case Name_Space.lookup (get_afun_table context) name of SOME af => transfer_afun (Context.theory_of context) af | NONE => undeclared name; val afun_of = afun_of_generic o Context.Proof; fun update_afun name f context = if Name_Space.defined (get_afun_table context) name then Data.map (map_data I (Name_Space.map_table_entry name f) I) context else undeclared name; end; fun match_term context = map #1 o Item_Net.retrieve_matching (get_patterns context); fun match_typ context = match_term context o Net.encode_type; (*works only with terms which are combinations of pure and ap*) fun afuns_of_term_generic context = map (afun_of_generic context) o match_term context; val afuns_of_term = afuns_of_term_generic o Context.Proof; fun afuns_of_typ_generic context = map (afun_of_generic context) o match_typ context; val afuns_of_typ = afuns_of_typ_generic o Context.Proof; fun all_unfolds_of_generic context = let val unfolds_of = map (Thm.transfer'' context) o unfolds_of_afun; in Name_Space.fold_table (fn (_, af) => append (unfolds_of af)) (get_afun_table context) [] end; val all_unfolds_of = all_unfolds_of_generic o Context.Proof; (** Term construction and destruction **) type afun_inst = { T: poly_type, pure: poly_term, ap: poly_term, set: poly_term }; fun mk_afun_inst [T, pure, ap, set] = {T = poly_type_of_term T, pure = pure, ap = ap, set = set}; fun pack_afun_inst {T, pure, ap, set} = pack_poly_terms [poly_type_to_term T, pure, ap, set]; fun match_afun_inst ctxt af = match_poly_terms ctxt (terms_of_afun af, 0) #> mk_afun_inst; fun import_afun_inst_raw terms = import_poly_terms terms #>> mk_afun_inst; val import_afun_inst = import_afun_inst_raw o terms_of_afun; fun inner_sort_of {T = (tvars, _), ...} = Type.sort_of_atyp (the_single tvars); fun mk_type {T, ...} = instantiate_poly_type T o single; fun mk_pure {pure, ...} = instantiate_poly_term pure o single; fun mk_ap {ap, ...} (T1, T2) = instantiate_poly_term ap [T1, T2]; fun mk_set {set, ...} = instantiate_poly_term set o single; fun lift_term af_inst t = Term.betapply (mk_pure af_inst (Term.fastype_of t), t); fun mk_comb af_inst funT (t1, t2) = Term.betapplys (mk_ap af_inst (dest_funT funT), [t1, t2]); fun dest_type ctxt {T, ...} = the_single o dest_poly_type ctxt T; val dest_type' = the_default HOLogic.unitT ooo dest_type; fun dest_pure ctxt {pure = (_, pure), ...} = the_single o dest_comb_pattern ctxt (pure, 1); fun dest_comb ctxt {ap = (_, ap), ...} = the_pair o dest_comb_pattern ctxt (ap, 2); fun infer_comb ctxt af_inst (t1, t2) = let val funT = the_default (dummyT --> dummyT) (dest_type ctxt af_inst (fastype_of t1)); in mk_comb af_inst funT (t1, t2) end; (*lift a term, except for non-combination subterms mapped by subst*) fun subst_lift_term af_inst subst tm = let fun subst_lift (s $ t) = (case (subst_lift s, subst_lift t) of (NONE, NONE) => NONE | (SOME s', NONE) => SOME (mk_comb af_inst (fastype_of s) (s', lift_term af_inst t)) | (NONE, SOME t') => SOME (mk_comb af_inst (fastype_of s) (lift_term af_inst s, t')) | (SOME s', SOME t') => SOME (mk_comb af_inst (fastype_of s) (s', t'))) | subst_lift t = AList.lookup (op aconv) subst t; in (case subst_lift tm of NONE => lift_term af_inst tm | SOME tm' => tm') end; fun add_lifted_vars (s $ t) = add_lifted_vars s #> add_lifted_vars t | add_lifted_vars (Abs (_, _, t)) = Term.add_vars t | add_lifted_vars _ = I; (*lift terms, where schematic variables are generalized to the functor and then fixed*) fun generalize_lift_terms af_inst ts ctxt = let val vars = subtract (op =) (fold add_lifted_vars ts []) (fold Term.add_vars ts []); val (var_names, Ts) = split_list vars; val (free_names, ctxt') = Variable.variant_fixes (map #1 var_names) ctxt; val Ts' = map (mk_type af_inst) Ts; val subst = map Var vars ~~ map Free (free_names ~~ Ts'); in (map (subst_lift_term af_inst subst) ts, ctxt') end; (** Reasoning with applicative functors **) (* Utilities *) val clean_name = perhaps (perhaps_apply [try Name.dest_skolem, try Name.dest_internal]); (*based on term_name from Pure/term.ML*) fun term_to_vname (Const (x, _)) = Long_Name.base_name x | term_to_vname (Free (x, _)) = clean_name x | term_to_vname (Var ((x, _), _)) = clean_name x | term_to_vname _ = "x"; fun afuns_of_rel precise ctxt t = let val (_, (lhs, rhs)) = Variable.focus NONE t ctxt |> #1 |> #2 |> Logic.strip_imp_concl |> Envir.beta_eta_contract |> HOLogic.dest_Trueprop |> strip_comb2; in if precise then (case afuns_of_term ctxt lhs of [] => afuns_of_term ctxt rhs | afs => afs) else afuns_of_typ ctxt (fastype_of lhs) end; fun AUTO_AFUNS precise tac ctxt opt_af = case opt_af of SOME af => tac [af] | NONE => SUBGOAL (fn (goal, i) => (case afuns_of_rel precise ctxt goal of [] => no_tac | afs => tac afs i) handle TERM _ => no_tac); fun AUTO_AFUN precise tac = AUTO_AFUNS precise (tac o hd); fun binop_par_conv cv ct = let val ((binop, arg1), arg2) = Thm.dest_comb ct |>> Thm.dest_comb; val (th1, th2) = cv (arg1, arg2); in Drule.binop_cong_rule binop th1 th2 end; fun binop_par_conv_tac cv = CONVERSION (HOLogic.Trueprop_conv (binop_par_conv cv)); val fold_goal_tac = SELECT_GOAL oo Raw_Simplifier.fold_goals_tac; (* Unfolding of lifted constants *) fun afun_unfold_tac ctxt af = Raw_Simplifier.rewrite_goal_tac ctxt (unfolds_of_afun af); fun afun_fold_tac ctxt af = fold_goal_tac ctxt (unfolds_of_afun af); fun unfold_all_tac ctxt = Raw_Simplifier.rewrite_goal_tac ctxt (all_unfolds_of ctxt); (* Basic conversions *) fun pure_conv ctxt {pure = (_, pure), ...} cv ct = let val ([var], (tyenv, env)) = match_comb_pattern ctxt (pure, 1) (Thm.term_of ct); val arg = the (Envir.lookup1 env var); val thm = cv (Thm.cterm_of ctxt arg); in if Thm.is_reflexive thm then Conv.all_conv ct else let val pure_inst = Envir.subst_term_types tyenv pure; in Drule.arg_cong_rule (Thm.cterm_of ctxt pure_inst) thm end end; fun ap_conv ctxt {ap = (_, ap), ...} cv1 cv2 ct = let val ([var1, var2], (tyenv, env)) = match_comb_pattern ctxt (ap, 2) (Thm.term_of ct); val (arg1, arg2) = apply2 (the o Envir.lookup1 env) (var1, var2); val thm1 = cv1 (Thm.cterm_of ctxt arg1); val thm2 = cv2 (Thm.cterm_of ctxt arg2); in if Thm.is_reflexive thm1 andalso Thm.is_reflexive thm2 then Conv.all_conv ct else let val ap_inst = Envir.subst_term_types tyenv ap; in Drule.binop_cong_rule (Thm.cterm_of ctxt ap_inst) thm1 thm2 end end; (* Normal form conversion *) (*convert a term into applicative normal form*) fun normalform_conv ctxt af ct = let val {hom, ichng, pure_comp_conv, ...} = thms_of_afun af; val the_red = the o red_of_afun af; val leaf_conv = Conv.rewr_conv (mk_meta_eq (the_red "I") |> Thm.symmetric); val merge_conv = Conv.rewr_conv (mk_meta_eq hom); val swap_conv = Conv.rewr_conv (mk_meta_eq ichng); val rotate_conv = Conv.rewr_conv (mk_meta_eq (the_red "B") |> Thm.symmetric); val pure_rotate_conv = Conv.rewr_conv (mk_meta_eq pure_comp_conv); val af_inst = match_afun_inst ctxt af (Thm.term_of ct, Thm.maxidx_of_cterm ct); fun left_conv cv = ap_conv ctxt af_inst cv Conv.all_conv; fun norm_pure_nf ct = ((pure_rotate_conv then_conv left_conv norm_pure_nf) else_conv merge_conv) ct; val norm_nf_pure = swap_conv then_conv norm_pure_nf; fun norm_nf_nf ct = ((rotate_conv then_conv left_conv (left_conv norm_pure_nf then_conv norm_nf_nf)) else_conv norm_nf_pure) ct; fun normalize ct = ((ap_conv ctxt af_inst normalize normalize then_conv norm_nf_nf) else_conv pure_conv ctxt af_inst Conv.all_conv else_conv leaf_conv) ct; in normalize ct end; val normalize_rel_tac = binop_par_conv_tac o apply2 oo normalform_conv; (* Bracket abstraction and generalized unlifting *) (*TODO: use proper conversions*) datatype apterm = Pure of term (*includes pure application*) | ApVar of int * term (*unique index, instantiated term*) | Ap of apterm * apterm; fun apterm_vars (Pure _) = I | apterm_vars (ApVar v) = cons v | apterm_vars (Ap (t1, t2)) = apterm_vars t1 #> apterm_vars t2; fun occurs_any _ (Pure _) = false | occurs_any vs (ApVar (i, _)) = exists (fn j => i = j) vs | occurs_any vs (Ap (t1, t2)) = occurs_any vs t1 orelse occurs_any vs t2; fun term_of_apterm ctxt af_inst t = let fun tm_of (Pure t) = t | tm_of (ApVar (_, t)) = t | tm_of (Ap (t1, t2)) = infer_comb ctxt af_inst (tm_of t1, tm_of t2); in tm_of t end; fun apterm_of_term ctxt af_inst t = let fun aptm_of t i = case try (dest_comb ctxt af_inst) t of SOME (t1, t2) => i |> aptm_of t1 ||>> aptm_of t2 |>> Ap | NONE => if can (dest_pure ctxt af_inst) t then (Pure t, i) else (ApVar (i, t), i + 1); in aptm_of t end; (*find a common variable sequence for two applicative terms, depending on available combinators*) fun consolidate ctxt af (t1, t2) = let fun common_inst (i, t) (j, insts) = case Termtab.lookup insts t of SOME k => (((i, t), k), (j, insts)) | NONE => (((i, t), j), (j + 1, Termtab.update (t, j) insts)); val (vars, _) = (0, Termtab.empty) |> fold_map common_inst (apterm_vars t1 []) ||>> fold_map common_inst (apterm_vars t2 []); fun merge_adjacent (([], _), _) [] = [] | merge_adjacent ((is, t), d) [] = [((is, t), d)] | merge_adjacent (([], _), _) (((i, t), d)::xs) = merge_adjacent (([i], t), d) xs | merge_adjacent ((is, t), d) (((i', t'), d')::xs) = if d = d' then merge_adjacent ((i'::is, t), d) xs else ((is, t), d) :: merge_adjacent (([i'], t'), d') xs; fun align _ [] = NONE | align ((i, t), d) (((i', t'), d')::xs) = if d = d' then SOME ([((i @ i', t), d)], xs) else Option.map (apfst (cons ((i', t'), d'))) (align ((i, t), d) xs); fun merge ([], ys) = ys | merge (xs, []) = xs | merge ((xs as ((is1, t1), d1)::xs'), ys as (((is2, t2), d2)::ys')) = if d1 = d2 then ((is1 @ is2, t1), d1) :: merge (xs', ys') else case (align ((is2, t2), d2) xs, align ((is1, t1), d1) ys) of (SOME (zs, xs''), NONE) => zs @ merge (xs'', ys') | (NONE, SOME (zs, ys'')) => zs @ merge (xs', ys'') | _ => ((is1, t1), d1) :: ((is2, t2), d2) :: merge (xs', ys'); fun unbalanced vs = error ("Unbalanced opaque terms " ^ commas_quote (map (Syntax.string_of_term ctxt o #2 o #1) vs)); fun mismatch (t1, t2) = error ("Mismatched opaque terms " ^ quote (Syntax.string_of_term ctxt t1) ^ " and " ^ quote (Syntax.string_of_term ctxt t2)); fun same ([], []) = [] | same ([], ys) = unbalanced ys | same (xs, []) = unbalanced xs | same ((((i1, t1), d1)::xs), (((i2, t2), d2)::ys)) = if d1 = d2 then ((i1 @ i2, t1), d1) :: same (xs, ys) else mismatch (t1, t2); in vars |> has_red_afun af "C" ? apply2 (sort (int_ord o apply2 #2)) |> apply2 (if has_red_afun af "W" then merge_adjacent (([], Term.dummy), 0) else map (apfst (apfst single))) |> (if has_red_afun af "K" then merge else same) |> map #1 end; fun ap_cong ctxt af_inst thm1 thm2 = let val funT = the_default (dummyT --> dummyT) (dest_type ctxt af_inst (Thm.typ_of_cterm (Thm.lhs_of thm1))); val ap_inst = Thm.cterm_of ctxt (mk_ap af_inst (dest_funT funT)); in Drule.binop_cong_rule ap_inst thm1 thm2 end; fun rewr_subst_ap ctxt af_inst rewr thm1 thm2 = let val rule1 = ap_cong ctxt af_inst thm1 thm2; val rule2 = Conv.rewr_conv rewr (Thm.rhs_of rule1); in Thm.transitive rule1 rule2 end; fun merge_pures ctxt af_inst merge_thm tt = let fun merge (Pure t) = SOME (Thm.reflexive (Thm.cterm_of ctxt t)) | merge (ApVar _) = NONE | merge (Ap (tt1, tt2)) = case merge tt1 of NONE => NONE | SOME thm1 => case merge tt2 of NONE => NONE | SOME thm2 => SOME (rewr_subst_ap ctxt af_inst merge_thm thm1 thm2); in merge tt end; exception ASSERT of string; (*abstract over a variable (opaque subterm)*) fun eliminate ctxt (af, af_inst) tt (v, v_tm) = let val {hom, ichng, ...} = thms_of_afun af; val the_red = the o red_of_afun af; val hom_conv = mk_meta_eq hom; val ichng_conv = mk_meta_eq ichng; val mk_combI = Thm.symmetric o mk_meta_eq; val id_conv = mk_combI (the_red "I"); val comp_conv = mk_combI (the_red "B"); val flip_conv = Option.map mk_combI (red_of_afun af "C"); val const_conv = Option.map mk_combI (red_of_afun af "K"); val dup_conv = Option.map mk_combI (red_of_afun af "W"); val rewr_subst_ap = rewr_subst_ap ctxt af_inst; fun extract_comb n thm = Pure (thm |> Thm.rhs_of |> funpow n Thm.dest_arg1 |> Thm.term_of); fun refl_step tt = (tt, Thm.reflexive (Thm.cterm_of ctxt (term_of_apterm ctxt af_inst tt))); fun comb2_step def (tt1, thm1) (tt2, thm2) = let val thm = rewr_subst_ap def thm1 thm2; in (Ap (Ap (extract_comb 3 thm, tt1), tt2), thm) end; val B_step = comb2_step comp_conv; fun swap_B_step (tt1, thm1) thm2 = let val thm3 = rewr_subst_ap ichng_conv thm1 thm2; val thm4 = Thm.transitive thm3 (Conv.rewr_conv comp_conv (Thm.rhs_of thm3)); in (Ap (Ap (extract_comb 3 thm4, extract_comb 1 thm3), tt1), thm4) end; fun I_step tm = let val thm = Conv.rewr_conv id_conv (Thm.cterm_of ctxt tm) in (extract_comb 1 thm, thm) end; fun W_step s1 s2 = let val (Ap (Ap (tt1, tt2), tt3), thm1) = B_step s1 s2; val thm2 = Conv.rewr_conv comp_conv (Thm.rhs_of thm1 |> funpow 2 Thm.dest_arg1); val thm3 = merge_pures ctxt af_inst hom_conv tt3 |> the; val (tt4, thm4) = swap_B_step (Ap (Ap (extract_comb 3 thm2, tt1), tt2), thm2) thm3; val var = Thm.rhs_of thm1 |> Thm.dest_arg; val thm5 = rewr_subst_ap (the dup_conv) thm4 (Thm.reflexive var); val thm6 = Thm.transitive thm1 thm5; in (Ap (extract_comb 2 thm6, tt4), thm6) end; fun S_step s1 s2 = let val (Ap (Ap (tt1, tt2), tt3), thm1) = comb2_step (the flip_conv) s1 s2; val thm2 = Conv.rewr_conv comp_conv (Thm.rhs_of thm1 |> Thm.dest_arg1); val var = Thm.rhs_of thm1 |> Thm.dest_arg; val thm3 = rewr_subst_ap (the dup_conv) thm2 (Thm.reflexive var); val thm4 = Thm.transitive thm1 thm3; val tt = Ap (extract_comb 2 thm4, Ap (Ap (extract_comb 3 thm2, Ap (tt1, tt2)), tt3)); in (tt, thm4) end; fun K_step tt tm = let val ct = Thm.cterm_of ctxt tm; val T_opt = Term.fastype_of tm |> dest_type ctxt af_inst |> Option.map (Thm.ctyp_of ctxt); val thm = Thm.instantiate' [T_opt] [SOME ct] (Conv.rewr_conv (the const_conv) (term_of_apterm ctxt af_inst tt |> Thm.cterm_of ctxt)) in (Ap (extract_comb 2 thm, tt), thm) end; fun unreachable _ = raise ASSERT "eliminate: assertion failed"; fun elim (Pure _) = unreachable () | elim (ApVar (i, t)) = if exists (fn x => x = i) v then I_step t else unreachable () | elim (Ap (t1, t2)) = (case (occurs_any v t1, occurs_any v t2) of (false, false) => unreachable () | (false, true) => B_step (refl_step t1) (elim t2) | (true, false) => (case merge_pures ctxt af_inst hom_conv t2 of SOME thm => swap_B_step (elim t1) thm | NONE => comb2_step (the flip_conv) (elim t1) (refl_step t2)) | (true, true) => if is_some flip_conv then S_step (elim t1) (elim t2) else W_step (elim t1) (elim t2)); in if occurs_any v tt then elim tt else K_step tt v_tm end; (*convert a pair of terms into equal canonical forms, modulo pure terms*) fun general_normalform_conv ctxt af cts = let val (t1, t2) = apply2 (Thm.term_of) cts; val maxidx = Int.max (apply2 Thm.maxidx_of_cterm cts); (* TODO: is there a better strategy for finding the instantiated functor? *) val af_inst = match_afun_inst ctxt af (t1, maxidx); val ((apt1, apt2), _) = 0 |> apterm_of_term ctxt af_inst t1 ||>> apterm_of_term ctxt af_inst t2; val vs = consolidate ctxt af (apt1, apt2); val merge_thm = mk_meta_eq (#hom (thms_of_afun af)); fun elim_all tt [] = the (merge_pures ctxt af_inst merge_thm tt) | elim_all tt (v::vs) = let val (tt', rule1) = eliminate ctxt (af, af_inst) tt v; val rule2 = elim_all tt' vs; val (_, vartm) = dest_comb ctxt af_inst (Thm.term_of (Thm.rhs_of rule1)); val rule3 = ap_cong ctxt af_inst rule2 (Thm.reflexive (Thm.cterm_of ctxt vartm)); in Thm.transitive rule1 rule3 end; in (elim_all apt1 vs, elim_all apt2 vs) end; val general_normalize_rel_tac = binop_par_conv_tac oo general_normalform_conv; (* Reduce canonical forms to base relation *) fun rename_params names i st = let val (_, Bs, Bi, C) = Thm.dest_state (st, i); val Bi' = Logic.list_rename_params names Bi; in Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st end; (* R' (pure f <> x1 <> ... <> xn) (pure g <> x1 <> ... <> xn) ===> !!y1 ... yn. [| yi : setF xi ... |] ==> R (f y1 ... yn) (g y1 ... yn), where either both R and R' are equality, or R' = relF R for relator relF of the functor. The premises yi : setF xi are added only in the latter case and if the set operator is available. Succeeds if partial progress can be made. The names of the new parameters yi are derived from the arguments xi. *) fun head_cong_tac ctxt af renames = let val {rel_intros, ...} = thms_of_afun af; fun term_name tm = case AList.lookup (op aconv) renames tm of SOME n => n | NONE => term_to_vname tm; fun gather_vars' af_inst tm = case try (dest_comb ctxt af_inst) tm of SOME (t1, t2) => term_name t2 :: gather_vars' af_inst t1 | NONE => []; fun gather_vars prop = case prop of Const (@{const_name Trueprop}, _) $ (_ $ rhs) => rev (gather_vars' (match_afun_inst ctxt af (rhs, maxidx_of_term prop)) rhs) | _ => []; in SUBGOAL (fn (subgoal, i) => (REPEAT_DETERM (resolve_tac ctxt rel_intros i) THEN REPEAT_DETERM (resolve_tac ctxt [ext, @{thm rel_fun_eq_onI}] i ORELSE eresolve_tac ctxt [@{thm UNIV_E}] i) THEN PRIMITIVE (rename_params (gather_vars subgoal) i))) end; (* Forward lifting *) (* TODO: add limited support for premises, where used variables are not generalized in the conclusion *) fun forward_lift_rule ctxt af thm = let val thm = Object_Logic.rulify ctxt thm; val (af_inst, ctxt_inst) = import_afun_inst af ctxt; val (prop, ctxt_Ts) = yield_singleton Variable.importT_terms (Thm.prop_of thm) ctxt_inst; val (lhs, rhs) = prop |> HOLogic.dest_Trueprop |> HOLogic.dest_eq; val ([lhs', rhs'], ctxt_lifted) = generalize_lift_terms af_inst [lhs, rhs] ctxt_Ts; val lifted = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs')); val (lifted', ctxt') = yield_singleton (Variable.import_terms true) lifted ctxt_lifted; fun tac {prems, context} = HEADGOAL (general_normalize_rel_tac context af THEN' head_cong_tac context af [] THEN' resolve_tac context [prems MRS thm]); val thm' = singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] lifted' tac); val thm'' = Raw_Simplifier.fold_rule ctxt (unfolds_of_afun af) thm'; in thm'' end; fun forward_lift_attrib name = Thm.rule_attribute [] (fn context => fn thm => let val af = afun_of_generic context (intern context name) (* FIXME !?!? *) in forward_lift_rule (Context.proof_of context) af thm end); (* High-level tactics *) fun unfold_wrapper_tac ctxt = AUTO_AFUNS false (fn afs => Simplifier.safe_asm_full_simp_tac (ctxt addsimps flat (map unfolds_of_afun afs))) ctxt; fun fold_wrapper_tac ctxt = AUTO_AFUN true (fold_goal_tac ctxt o unfolds_of_afun) ctxt; fun WRAPPER tac ctxt opt_af = REPEAT_DETERM o resolve_tac ctxt [@{thm allI}] THEN' Subgoal.FOCUS (fn {context = ctxt, params, ...} => let val renames = map (swap o apsnd Thm.term_of) params in AUTO_AFUNS false (EVERY' o map (afun_unfold_tac ctxt)) ctxt opt_af 1 THEN AUTO_AFUN true (fn af => afun_unfold_tac ctxt af THEN' CONVERSION Drule.beta_eta_conversion THEN' tac ctxt af THEN' head_cong_tac ctxt af renames) ctxt opt_af 1 end) ctxt THEN' Raw_Simplifier.rewrite_goal_tac ctxt [Drule.triv_forall_equality]; val normalize_wrapper_tac = WRAPPER normalize_rel_tac; val lifting_wrapper_tac = WRAPPER general_normalize_rel_tac; val parse_opt_afun = Scan.peek (fn context => Scan.option Parse.name >> Option.map (intern context #> afun_of_generic context)); (** Declaration **) (* Combinator setup *) fun declare_combinators combs phi = let val (names, thms) = split_list combs; val thms' = map (Morphism.thm phi) thms; fun add_combs (defs, rules) = (fold (Symtab.insert (K false)) (names ~~ thms') defs, rules); in Data.map (map_data add_combs I I) end; val setup_combinators = Local_Theory.declaration {syntax = false, pervasive = false} o declare_combinators; fun combinator_of_red thm = let val (lhs, _) = Logic.dest_equals (Thm.prop_of thm); val (head, _) = strip_comb lhs; in #1 (dest_Const head) end; fun register_combinator_rule weak_premises thm context = let val (lhs, rhs) = Logic.dest_equals (Thm.prop_of thm); val ltvars = Term.add_tvars lhs []; val rtvars = Term.add_tvars rhs []; val _ = if exists (not o member op = ltvars) rtvars then Pretty.breaks [Pretty.str "Combinator equation", Pretty.quote (Syntax.pretty_term (Context.proof_of context) (Thm.prop_of thm)), Pretty.str "has additional type variables on right-hand side."] |> Pretty.block |> Pretty.string_of |> error else (); val (defs, _) = #combinators (Data.get context); val comb_names = Symtab.make (map (fn (name, thm) => (combinator_of_red thm, name)) (Symtab.dest defs)); val rule = mk_combinator_rule comb_names weak_premises thm; fun add_rule (defs, rules) = (defs, insert eq_combinator_rule rule rules); in Data.map (map_data add_rule I I) context end; val combinator_rule_attrib = Thm.declaration_attribute o register_combinator_rule; (* Derivation of combinator reductions *) fun combinator_closure rules have_weak combs = let fun apply rule (cs, changed) = if not (Ord_List.member fast_string_ord cs (conclusion_of_rule rule)) andalso is_applicable_rule rule have_weak (fn prems => Ord_List.subset fast_string_ord (prems, cs)) then (Ord_List.insert fast_string_ord (conclusion_of_rule rule) cs, true) else (cs, changed); fun loop cs = (case fold apply rules (cs, false) of (cs', true) => loop cs' | (_, false) => cs); in loop combs end; fun derive_combinator_red ctxt af_inst red_thms (base_thm, eq_thm) = let val base_prop = Thm.prop_of base_thm; val tvars = Term.add_tvars base_prop []; val (Ts, ctxt_Ts) = mk_TFrees_of (length tvars) (inner_sort_of af_inst) ctxt; val base_prop' = base_prop |> Term_Subst.instantiate (TVars.make (tvars ~~ Ts), Vars.empty); val (lhs, rhs) = Logic.dest_equals base_prop'; val ([lhs', rhs'], ctxt') = generalize_lift_terms af_inst [lhs, rhs] ctxt_Ts; val lifted_prop = (lhs', rhs') |> HOLogic.mk_eq |> HOLogic.mk_Trueprop; val unfold_comb_conv = HOLogic.Trueprop_conv (HOLogic.eq_conv (Conv.top_sweep_rewrs_conv [eq_thm] ctxt') Conv.all_conv); fun tac goal_ctxt = HEADGOAL (CONVERSION unfold_comb_conv THEN' Raw_Simplifier.rewrite_goal_tac goal_ctxt red_thms THEN' resolve_tac goal_ctxt [@{thm refl}]); in singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] lifted_prop (tac o #context)) 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 (TVars.empty, Vars.make [((v, af_T), pure_v)]) prev; val next' = Raw_Simplifier.rewrite_rule ctxt'' [merge_thm] next; val next'' = singleton (Variable.export ctxt'' ctxt) next'; in closure vs next'' (prev::thms) end); in closure vars strong_red [] end; fun combinator_red_closure ctxt (comb_defs, rules) (af_inst, merge_thm) weak_reds combs = let val have_weak = not (null weak_reds); val red_thms0 = Symtab.fold (fn (_, thm) => cons (mk_meta_eq thm)) combs weak_reds; val red_thms = flat (map (weak_red_closure ctxt (af_inst, merge_thm)) red_thms0); fun apply rule ((cs, rs), changed) = if not (Symtab.defined cs (conclusion_of_rule rule)) andalso is_applicable_rule rule have_weak (forall (Symtab.defined cs)) then let val conclusion = conclusion_of_rule rule; val def = the (Symtab.lookup comb_defs conclusion); val new_red_thm = derive_combinator_red ctxt af_inst rs (def, thm_of_rule rule); val new_red_thms = weak_red_closure ctxt (af_inst, merge_thm) (mk_meta_eq new_red_thm); in ((Symtab.update (conclusion, new_red_thm) cs, new_red_thms @ rs), true) end else ((cs, rs), changed); fun loop xs = (case fold apply rules (xs, false) of (xs', true) => loop xs' | (_, false) => xs); in #1 (loop (combs, red_thms)) end; (* Preparation of AFun data *) fun mk_terms ctxt (raw_pure, raw_ap, raw_rel, raw_set) = let val thy = Proof_Context.theory_of ctxt; val show_typ = quote o Syntax.string_of_typ ctxt; val show_term = quote o Syntax.string_of_term ctxt; fun closed_poly_term t = let val poly_t = singleton (Variable.polymorphic ctxt) t; in case Term.add_vars (singleton (Variable.export_terms (Proof_Context.augment t ctxt) ctxt) t) [] of [] => (case (Term.hidden_polymorphism poly_t) of [] => poly_t | _ => error ("Hidden type variables in term " ^ show_term t)) | _ => error ("Locally free variables in term " ^ show_term t) end; val pure = closed_poly_term raw_pure; val (tvar, T1) = fastype_of pure |> dest_funT |>> dest_TVar handle TYPE _ => error ("Bad type for pure: " ^ show_typ (fastype_of pure)); val maxidx_pure = maxidx_of_term pure; val ap = Logic.incr_indexes ([], [], maxidx_pure + 1) (closed_poly_term raw_ap); fun bad_ap _ = error ("Bad type for ap: " ^ show_typ (fastype_of ap)); val (T23, (T2, T3)) = fastype_of ap |> dest_funT ||> dest_funT handle TYPE _ => bad_ap (); val maxidx_common = Term.maxidx_term ap maxidx_pure; (*unify type variables, while keeping the live variables separate*) fun no_unifier (T, U) = error ("Unable to infer common functor type from " ^ commas (map show_typ [T, U])); fun unify_ap_type T (tyenv, maxidx) = let val argT = TVar ((Name.aT, maxidx + 1), []); val T1' = Term_Subst.instantiateT (TVars.make [(tvar, argT)]) T1; val (tyenv', maxidx') = Sign.typ_unify thy (T1', T) (tyenv, maxidx + 1) handle Type.TUNIFY => no_unifier (T1', T); in (argT, (tyenv', maxidx')) end; val (ap_args, (ap_env, maxidx_env)) = fold_map unify_ap_type [T2, T3, T23] (Vartab.empty, maxidx_common); val [T2_arg, T3_arg, T23_arg] = map (Envir.norm_type ap_env) ap_args; val (tvar2, tvar3) = (dest_TVar T2_arg, dest_TVar T3_arg) handle TYPE _ => bad_ap (); val _ = if T23_arg = T2_arg --> T3_arg then () else bad_ap (); val sort = foldl1 (Sign.inter_sort thy) (map #2 [tvar, tvar2, tvar3]); val _ = Sign.of_sort thy (Term.aT sort --> Term.aT sort, sort) orelse error ("Sort constraint " ^ quote (Syntax.string_of_sort ctxt sort) ^ " not closed under function types"); fun update_sort (v, S) (tyenv, maxidx) = (Vartab.update_new (v, (S, TVar ((Name.aT, maxidx + 1), sort))) tyenv, maxidx + 1); val (common_env, _) = fold update_sort [tvar, tvar2, tvar3] (ap_env, maxidx_env); val tvar' = Envir.norm_type common_env (TVar tvar); val pure' = norm_term_types common_env pure; val (tvar2', tvar3') = apply2 (Envir.norm_type common_env) (T2_arg, T3_arg); val ap' = norm_term_types common_env ap; fun bad_set set = error ("Bad type for set: " ^ show_typ (fastype_of set)); fun mk_set set = let val tyenv = Sign.typ_match thy (domain_type (fastype_of set), range_type (fastype_of pure')) Vartab.empty handle Type.TYPE_MATCH => bad_set set; val set' = Envir.subst_term_types tyenv set; val set_tvar = fastype_of set' |> range_type |> HOLogic.dest_setT |> dest_TVar handle TYPE _ => bad_set set; val _ = if Term.eq_tvar (dest_TVar tvar', set_tvar) then () else bad_set set; in ([tvar'], set') end val set = (case raw_set of NONE => ([tvar'], Abs ("x", tvar', HOLogic.mk_UNIV tvar')) | SOME t => mk_set (closed_poly_term t)); val terms = Term_Subst.zero_var_indexes (pack_poly_terms [poly_type_to_term ([tvar'], range_type (fastype_of pure')), ([tvar'], pure'), ([tvar2', tvar3'], ap'), set]); (*TODO: also infer the relator type?*) fun bad_rel rel = error ("Bad type for rel: " ^ show_typ (fastype_of rel)); fun mk_rel rel = let val ((T1, T2), (T1_af, T2_af)) = fastype_of rel |> dest_funT |>> BNF_Util.dest_pred2T ||> BNF_Util.dest_pred2T; val _ = (dest_TVar T1; dest_TVar T2); val _ = if T1 = T2 then bad_rel rel else (); val af_inst = mk_afun_inst (match_poly_terms_type ctxt (terms, 0) (T1_af, maxidx_of_term rel)); val (T1', T2') = apply2 (dest_type ctxt af_inst) (T1_af, T2_af); val _ = if (is_none T1' andalso is_none T2') orelse (T1' = SOME T1 andalso T2' = SOME T2) then () else bad_rel rel; in Term_Subst.zero_var_indexes (pack_poly_terms [([T1, T2], rel)]) end handle TYPE _ => bad_rel rel; val rel = Option.map (mk_rel o closed_poly_term) raw_rel; in (terms, rel) end; fun mk_rel_intros {pure_transfer, ap_rel_fun} = let val pure_rel_intro = pure_transfer RS @{thm rel_funD}; in [pure_rel_intro, ap_rel_fun] end; fun mk_afun_thms ctxt af_inst (hom_thm, ichng_thm, reds, rel_axioms) = let val pure_comp_conv = let val ([T1, T2, T3], ctxt_Ts) = mk_TFrees_of 3 (inner_sort_of af_inst) ctxt; val (((g, f), x), ctxt') = ctxt_Ts |> mk_Free "g" (T2 --> T3) ||>> mk_Free "f" (mk_type af_inst (T1 --> T2)) ||>> mk_Free "x" (mk_type af_inst T1); val comb = mk_comb af_inst; val lhs = comb (T2 --> T3) (lift_term af_inst g, comb (T1 --> T2) (f, x)); val B_g = Abs ("f", T1 --> T2, Abs ("x", T1, Term.betapply (g, Bound 1 $ Bound 0))); val rhs = comb (T1 --> T3) (comb ((T1 --> T2) --> T1 --> T3) (lift_term af_inst B_g, f), x); val prop = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop; val merge_rule = mk_meta_eq hom_thm; val B_intro = the (Symtab.lookup reds "B") |> mk_meta_eq |> Thm.symmetric; fun tac goal_ctxt = HEADGOAL (Raw_Simplifier.rewrite_goal_tac goal_ctxt [B_intro, merge_rule] THEN' resolve_tac goal_ctxt [@{thm refl}]); in singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] prop (tac o #context)) end; val eq_intros = let val ([T1, T2], ctxt_Ts) = mk_TFrees_of 2 (inner_sort_of af_inst) ctxt; val T12 = mk_type af_inst (T1 --> T2); val (((((x, y), x'), f), g), ctxt') = ctxt_Ts |> mk_Free "x" T1 ||>> mk_Free "y" T1 ||>> mk_Free "x" (mk_type af_inst T1) ||>> mk_Free "f" T12 ||>> mk_Free "g" T12; val pure_fun = mk_pure af_inst T1; val pure_cong = Drule.infer_instantiate' ctxt' (map (SOME o Thm.cterm_of ctxt') [x, y, pure_fun]) @{thm arg_cong}; val ap_fun = mk_ap af_inst (T1, T2); val ap_cong1 = Drule.infer_instantiate' ctxt' (map (SOME o Thm.cterm_of ctxt') [f, g, ap_fun, x']) @{thm arg1_cong}; in Variable.export ctxt' ctxt [pure_cong, ap_cong1] end; val rel_intros = case rel_axioms of NONE => [] | SOME axioms => mk_rel_intros axioms; in {hom = hom_thm, ichng = ichng_thm, reds = reds, rel_thms = rel_axioms, rel_intros = eq_intros @ rel_intros, pure_comp_conv = pure_comp_conv} end; fun reuse_TFrees n S (ctxt, Ts) = let val have_n = Int.min (n, length Ts); val (more_Ts, ctxt') = mk_TFrees_of (n - have_n) S ctxt; in (take have_n Ts @ more_Ts, (ctxt', Ts @ more_Ts)) end; fun mk_comb_prop lift_pos thm af_inst ctxt_Ts = let val base = Thm.prop_of thm; val tvars = Term.add_tvars base []; val (Ts, (ctxt', Ts')) = reuse_TFrees (length tvars) (inner_sort_of af_inst) ctxt_Ts; val base' = base |> Term_Subst.instantiate (TVars.make (tvars ~~ Ts), Vars.empty); val (lhs, rhs) = Logic.dest_equals base'; val (_, lhs_args) = strip_comb lhs; val lift_var = Var o apsnd (mk_type af_inst) o dest_Var; val (lhs_args', subst) = fold_index (fn (i, v) => if member (op =) lift_pos i then apfst (cons v) else map_prod (cons (lift_var v)) (cons (v, lift_var v))) lhs_args ([], []); val (lhs', rhs') = apply2 (subst_lift_term af_inst subst) (lhs, rhs); val lifted = (lhs', rhs') |> HOLogic.mk_eq |> HOLogic.mk_Trueprop; in (fold Logic.all lhs_args' lifted, (ctxt', Ts')) end; fun mk_homomorphism_prop af_inst ctxt_Ts = let val ([T1, T2], (ctxt', Ts')) = reuse_TFrees 2 (inner_sort_of af_inst) ctxt_Ts; val ((f, x), _) = ctxt' |> mk_Free "f" (T1 --> T2) ||>> mk_Free "x" T1; val lhs = mk_comb af_inst (T1 --> T2) (lift_term af_inst f, lift_term af_inst x); val rhs = lift_term af_inst (f $ x); val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); in (Logic.all f (Logic.all x prop), (ctxt', Ts')) end; fun mk_interchange_prop af_inst ctxt_Ts = let val ([T1, T2], (ctxt', Ts')) = reuse_TFrees 2 (inner_sort_of af_inst) ctxt_Ts; val ((f, x), _) = ctxt' |> mk_Free "f" (mk_type af_inst (T1 --> T2)) ||>> mk_Free "x" T1; val lhs = mk_comb af_inst (T1 --> T2) (f, lift_term af_inst x); val T_x = Abs ("f", T1 --> T2, Bound 0 $ x); val rhs = mk_comb af_inst ((T1 --> T2) --> T2) (lift_term af_inst T_x, f); val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); in (Logic.all f (Logic.all x prop), (ctxt', Ts')) end; fun mk_rel_props (af_inst, rel_inst) ctxt_Ts = let fun mk_af_rel tm = let val (T1, T2) = BNF_Util.dest_pred2T (fastype_of tm); in betapply (instantiate_poly_term rel_inst [T1, T2], tm) end; val ([T1, T2, T3], (ctxt', Ts')) = reuse_TFrees 3 (inner_sort_of af_inst) ctxt_Ts; val (pure_R, _) = mk_Free "R" (T1 --> T2 --> @{typ bool}) ctxt'; val rel_pure = BNF_Util.mk_rel_fun pure_R (mk_af_rel pure_R) $ mk_pure af_inst T1 $ mk_pure af_inst T2; val pure_prop = Logic.all pure_R (HOLogic.mk_Trueprop rel_pure); val ((((f, g), x), ap_R), _) = ctxt' |> mk_Free "f" (mk_type af_inst (T1 --> T2)) ||>> mk_Free "g" (mk_type af_inst (T1 --> T3)) ||>> mk_Free "x" (mk_type af_inst T1) ||>> mk_Free "R" (T2 --> T3 --> @{typ bool}); val fun_rel = BNF_Util.mk_rel_fun (mk_eq_on (mk_set af_inst T1 $ x)) ap_R; val rel_ap = Logic.mk_implies (HOLogic.mk_Trueprop (mk_af_rel fun_rel $ f $ g), HOLogic.mk_Trueprop (mk_af_rel ap_R $ mk_comb af_inst (T1 --> T2) (f, x) $ mk_comb af_inst (T1 --> T3) (g, x))); val ap_prop = fold_rev Logic.all [ap_R, f, g, x] rel_ap; in ([pure_prop, ap_prop], (ctxt', Ts')) end; fun mk_interchange ctxt ((comb_defs, _), comb_unfolds) (af_inst, merge_thm) reds = let val T_def = the (Symtab.lookup comb_defs "T"); val T_red = the (Symtab.lookup reds "T"); val (weak_prop, (ctxt', _)) = mk_comb_prop [0] T_def af_inst (ctxt, []); fun tac goal_ctxt = HEADGOAL (Raw_Simplifier.rewrite_goal_tac goal_ctxt [Thm.symmetric merge_thm] THEN' resolve_tac goal_ctxt [T_red]); val weak_red = singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] weak_prop (tac o #context)); 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 goal_ctxt = HEADGOAL (normalize_wrapper_tac goal_ctxt (SOME af) THEN' Raw_Simplifier.rewrite_goal_tac goal_ctxt comb_unfolds THEN' resolve_tac goal_ctxt [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 o #context)); 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/acdata.ML b/thys/Auto2_HOL/HOL/acdata.ML --- a/thys/Auto2_HOL/HOL/acdata.ML +++ b/thys/Auto2_HOL/HOL/acdata.ML @@ -1,334 +1,333 @@ (* File: acdata.ML Author: Bohua Zhan Dealing with associative-commutative operations. *) (* Data for an AC function. *) type ac_info = { cfhead: cterm, unit: cterm option, assoc_th: thm, (* (a . b) . c = a . (b . c) *) comm_th: thm, (* a . b = b . a *) unitl_th: thm, (* e . a = a *) unitr_th: thm (* a . e = a *) } signature ACUTIL = sig val inst_ac_info: theory -> typ -> ac_info -> ac_info option val head_agrees: ac_info -> term -> bool val eq_unit: ac_info -> term -> bool val add_ac_data: ac_info -> theory -> theory val get_head_ac_info: theory -> term -> ac_info option val has_assoc_th: ac_info -> bool val has_comm_th: ac_info -> bool val has_unit_th: ac_info -> bool val comm_cv: ac_info -> conv val assoc_cv: ac_info -> conv val assoc_sym_cv: ac_info -> conv val swap_cv: ac_info -> conv val swap_r_cv: ac_info -> conv val dest_ac: ac_info -> term -> term list val cdest_ac: ac_info -> cterm -> cterm list val comb_ac_equiv: ac_info -> thm list -> thm val normalize_assoc: ac_info -> conv val move_outmost: ac_info -> term -> conv val normalize_unit: ac_info -> conv val normalize_comm_gen: ac_info -> (term * term -> bool) -> conv val normalize_comm: ac_info -> conv val normalize_au: ac_info -> conv val normalize_all_ac: ac_info -> conv val ac_last_conv: ac_info -> conv -> conv val norm_combine: ac_info -> (term -> bool) -> conv -> conv end; structure ACUtil : ACUTIL = struct (* Register of generators of ac_inst_info. *) structure Data = Theory_Data ( type T = ac_info Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge (fn (info1, info2) => #cfhead info1 aconvc #cfhead info2) ) (* Instantiate an ac_info for a specific type T. *) fun inst_ac_info thy T {assoc_th, comm_th, unitl_th, unitr_th, ...} = let (* Instantiate th to having argument of type T. If not possible, change th to true_th. *) fun inst_th th = if is_true_th th then true_th else let (* Extract the first argument of th, then the body type of that argument. *) val arg_type = th |> prop_of' |> Util.dest_args |> hd |> Term.type_of |> Term.body_type in if arg_type = T then th else let val tenv = Sign.typ_match thy (arg_type, T) Vartab.empty in Util.subst_thm_thy thy (tenv, Vartab.empty) th end handle Type.TYPE_MATCH => true_th end val assoc_th' = inst_th assoc_th val unitl_th' = inst_th unitl_th in if is_true_th assoc_th' then NONE else SOME {cfhead = assoc_th' |> cprop_of' |> Thm.dest_arg1 |> Thm.dest_fun2, unit = if is_true_th unitl_th' then NONE else SOME (unitl_th' |> cprop_of' |> Thm.dest_arg1 |> Thm.dest_arg1), assoc_th = assoc_th', comm_th = inst_th comm_th, unitl_th = unitl_th', unitr_th = inst_th unitr_th} end fun head_agrees {cfhead, ...} t = Util.is_head (Thm.term_of cfhead) t fun eq_unit {unit, ...} t = case unit of NONE => false | SOME ct' => t aconv (Thm.term_of ct') (* Add the given ac_info under the given name. *) fun add_ac_data info thy = let val {assoc_th, ...} = info val f = assoc_th |> prop_of' |> dest_eq |> snd |> Term.head_of in case f of Const (c, _) => let val _ = tracing ("Add ac data for function " ^ c) in Data.map (Symtab.update_new (c, info)) thy end | _ => error "Add AC data: invalid assoc_th" end handle Symtab.DUP _ => error "Add AC data: info already exists." fun get_head_ac_info thy t = case t of Const (c, _) $ _ $ _ => (case Symtab.lookup (Data.get thy) c of NONE => NONE | SOME ac_info => inst_ac_info thy (fastype_of t) ac_info) | _ => NONE fun has_assoc_th {assoc_th, ...} = not (is_true_th assoc_th) fun has_comm_th {comm_th, ...} = not (is_true_th comm_th) fun has_unit_th {unitl_th, ...} = not (is_true_th unitl_th) fun comm_cv {comm_th, ...} = rewr_obj_eq comm_th fun assoc_cv {assoc_th, ...} = rewr_obj_eq assoc_th fun assoc_sym_cv {assoc_th, ...} = rewr_obj_eq (obj_sym assoc_th) (* (a . b) . c = (a . c) . b *) fun swap_cv (ac_info as {assoc_th, comm_th, ...}) ct = if head_agrees ac_info (dest_arg1 (Thm.term_of ct)) then Conv.every_conv [rewr_obj_eq assoc_th, Conv.arg_conv (rewr_obj_eq comm_th), rewr_obj_eq (obj_sym assoc_th)] ct else rewr_obj_eq comm_th ct (* a . (b . c) = b . (a . c) *) fun swap_r_cv (ac_info as {assoc_th, comm_th, ...}) ct = if head_agrees ac_info (dest_arg (Thm.term_of ct)) then Conv.every_conv [rewr_obj_eq (obj_sym assoc_th), Conv.arg1_conv (rewr_obj_eq comm_th), rewr_obj_eq assoc_th] ct else rewr_obj_eq comm_th ct (* Destruct t, assuming it is associated to the left. *) fun dest_ac ac_info t = let fun dest t = if head_agrees ac_info t then let val (a1, a2) = Util.dest_binop_args t in a2 :: dest a1 end else [t] in rev (dest t) end fun cdest_ac ac_info ct = let fun dest ct = if head_agrees ac_info (Thm.term_of ct) then let val (a1, a2) = Util.dest_binop_cargs ct in a2 :: dest a1 end else [ct] in rev (dest ct) end (* Given ths: [A1 == B1, ..., An == Bn], get theorem A1...An == B1...Bn. Associate to the left only. *) fun comb_ac_equiv {cfhead, ...} ths = let fun binop_comb th1 th2 = Thm.combination (Thm.combination (Thm.reflexive cfhead) th1) th2 (* Combine in the reverse order. *) fun comb ths = case ths of [] => raise Fail "comb_ac_equiv: empty list" | [th] => th | [th1, th2] => binop_comb th2 th1 | th :: ths' => binop_comb (comb ths') th in comb (rev ths) end (* Normalize association with the given direction. *) fun normalize_assoc ac_info ct = if not (has_assoc_th ac_info) then Conv.all_conv ct else let val {assoc_th, ...} = ac_info (* First rewrite into form (...) * a, then rewrite the remaining parts. *) fun normalize ct = if head_agrees ac_info (Thm.term_of ct) then Conv.every_conv [Conv.repeat_conv (rewr_obj_eq (obj_sym assoc_th)), Conv.arg1_conv normalize] ct else Conv.all_conv ct in normalize ct end (* Move the given u within ct to the rightmost position. Assume associate to the left. *) fun move_outmost (ac_info as {comm_th, ...}) u ct = if not (has_assoc_th ac_info andalso has_comm_th ac_info) then raise Fail "move_outmost: commutativity is not available." else if u aconv (Thm.term_of ct) then Conv.all_conv ct else if not (head_agrees ac_info (Thm.term_of ct)) then raise Fail "move_outmost: u not found in ct." else let val (a, b) = Util.dest_binop_args (Thm.term_of ct) in if u aconv b then Conv.all_conv ct else if head_agrees ac_info a then ((Conv.arg1_conv (move_outmost ac_info u)) then_conv (swap_cv ac_info)) ct else if u aconv a then rewr_obj_eq comm_th ct else raise Fail "move_outmost: u not found in ct." end (* In a product of a_1, a_2, ..., remove any a_i that is a unit. *) fun normalize_unit (ac_info as {unitl_th, unitr_th, ...}) ct = if not (has_unit_th ac_info) then Conv.all_conv ct else let fun normalize ct = if head_agrees ac_info (Thm.term_of ct) then Conv.every_conv [Conv.binop_conv normalize, Conv.try_conv (rewr_obj_eq unitl_th), Conv.try_conv (rewr_obj_eq unitr_th)] ct else Conv.all_conv ct in normalize ct end (* Rearrange subterms of ct according to the given term ordering. Returns theorem ct == ct'. *) fun normalize_comm_gen (ac_info as {comm_th, ...}) termless ct = if not (has_comm_th ac_info) then Conv.all_conv ct else let (* If there are two terms a.b, swap if a > b. If there are at least three terms, in the left associate case this is (a.b).c, swap b and c if b > c. If there is a swap, recursively call swap_last until the original outside term is swapped into position. *) fun swap_last ct = if head_agrees ac_info (Thm.term_of ct) then let val (a1, a2) = Util.dest_binop_args (Thm.term_of ct) in if head_agrees ac_info a1 then (* Structure of t is a1 . a2 = (_ . b2) . a2. *) if termless (a2, dest_arg a1) then ((swap_cv ac_info) then_conv (Conv.arg1_conv swap_last)) ct else Conv.all_conv ct else (* Structure of t is a1 . a2. *) if termless (a2, a1) then rewr_obj_eq comm_th ct else Conv.all_conv ct end else Conv.all_conv ct (* Full ordering. Recursively perform full ordering on all but the outermost, then swap outermost into position. *) fun normalize ct = if head_agrees ac_info (Thm.term_of ct) then ((Conv.arg1_conv normalize) then_conv swap_last) ct else Conv.all_conv ct in normalize ct end fun normalize_comm ac_info = normalize_comm_gen ac_info (fn (s, t) => Term_Ord.term_ord (s, t) = LESS) (* Normalize all except comm. *) fun normalize_au ac_info = Conv.every_conv [normalize_unit ac_info, normalize_assoc ac_info] (* Normalize everything. *) fun normalize_all_ac ac_info = Conv.every_conv [normalize_au ac_info, normalize_comm ac_info] (* Rewrite the last term in ct using cv. Assume associative to left. *) fun ac_last_conv ac_info cv ct = if head_agrees ac_info (Thm.term_of ct) then Conv.arg_conv cv ct else cv ct (* Given ct in the form x_1 * ... * x_n, where some sequence of x_i satisfies predicate pred. Combine these x_i into a single term using the binary combinator cv. *) fun norm_combine ac_info pred cv ct = let val t = Thm.term_of ct in if head_agrees ac_info t then let val (a, b) = Util.dest_binop_args t in if pred b then if pred a then cv ct else if head_agrees ac_info a andalso pred (dest_arg a) then Conv.every_conv [assoc_cv ac_info, Conv.arg_conv cv, norm_combine ac_info pred cv] ct else Conv.all_conv ct else Conv.arg1_conv (norm_combine ac_info pred cv) ct end else Conv.all_conv ct end end (* structure ACUtil. *) diff --git a/thys/Auto2_HOL/HOL/induct_outer.ML b/thys/Auto2_HOL/HOL/induct_outer.ML --- a/thys/Auto2_HOL/HOL/induct_outer.ML +++ b/thys/Auto2_HOL/HOL/induct_outer.ML @@ -1,539 +1,538 @@ (* File: induct_outer.ML Author: Bohua Zhan Proof language for induction. *) signature INDUCT_PROOFSTEPS = sig val add_induct_data: string -> term * thm -> theory -> theory val add_typed_induct_data: string -> typ * thm -> theory -> theory val get_typed_ind_th: theory -> string -> typ -> thm val get_term_ind_th: theory -> string -> term -> thm val check_strong_ind_prop: term -> term list * term val add_strong_induct_rule: thm -> theory -> theory val add_case_induct_rule: thm -> theory -> theory val add_prop_induct_rule: thm -> theory -> theory val add_var_induct_rule: thm -> theory -> theory val add_cases_rule: thm -> theory -> theory val add_fun_induct_rule: term * thm -> theory -> theory val strong_induct_cmd: string * string list -> Proof.state -> Proof.state val apply_induct_hyp_cmd: string list -> Proof.state -> Proof.state val case_induct_cmd: string -> Proof.state -> Proof.state val prop_induct_cmd: string * string option -> Proof.state -> Proof.state val induct_cmd: string -> string * string option * string list * string option -> Proof.state -> Proof.state val is_simple_fun_induct: thm -> bool val fun_induct_cmd: string * string list * string option -> Proof.state -> Proof.state end; structure Induct_ProofSteps : INDUCT_PROOFSTEPS = struct structure Data = Theory_Data ( type T = ((term * thm) list) Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge_list (eq_fst (op =)) ) fun add_induct_data str (t, ind_th) = Data.map (Symtab.map_default (str, []) (cons (t, ind_th))) fun add_typed_induct_data str (ty, ind_th) = add_induct_data str (Term.dummy_pattern ty, ind_th) fun get_typed_ind_th thy ind_type ty = let val typ_can_match = can (fn t' => Sign.typ_match thy (type_of t', ty) Vartab.empty) in case Symtab.lookup (Data.get thy) ind_type of NONE => raise Fail (ind_type ^ ": cannot find theorem.") | SOME lst => case find_first (fn (t', _) => typ_can_match t') lst of NONE => raise Fail (ind_type ^ ": cannot find theorem.") | SOME (_, ind_th) => ind_th end fun get_term_ind_th thy ind_type t = let val data = Symtab.lookup_list (Data.get thy) ind_type fun match_data (pat, th) = let val inst = Pattern.first_order_match thy (pat, t) fo_init in SOME (Util.subst_thm_thy thy inst th) end handle Pattern.MATCH => NONE in case get_first match_data data of NONE => raise Fail (ind_type ^ ": cannot find theorem.") | SOME ind_th => ind_th end (* Check a strong induction theorem ind_th is of the right form, and extract the induction variables and substitution. *) fun check_strong_ind_prop ind_prop = let fun err str = "Strong induction: " ^ str val (cond_ind, concl) = ind_prop |> Logic.dest_implies |> apply2 dest_Trueprop (* concl must be of form ?P [?vars]. *) val err_concl = err "concl of ind_th must be ?P [?vars]." val (P, pat_vars) = Term.strip_comb concl handle TERM _ => error err_concl val _ = assert (is_Var P andalso forall is_Var pat_vars andalso (dest_Var P |> fst |> fst) = "P") err_concl (* cond_ind must be of form !n. P' n --> ?P n. Return the substitution pattern P'. *) val err_ind_hyp = err "cond_ind of ind_th must be !n. P' --> ?P vars." fun dest_one_all var body = case body of Const (c, _) $ Abs (_, _, t) => if c = UtilBase.All_name then subst_bound (var, t) else error err_ind_hyp | _ => error err_ind_hyp val (pat_subst, P_vars) = cond_ind |> fold dest_one_all pat_vars |> dest_imp val _ = assert (P_vars aconv concl) err_ind_hyp in (pat_vars, pat_subst) end fun add_strong_induct_rule ind_th thy = let val name = Util.name_of_thm ind_th val ctxt = Proof_Context.init_global thy val ind_th' = apply_to_thm (UtilLogic.to_obj_conv_on_horn ctxt) ind_th val (pat_var, pat_subst) = check_strong_ind_prop (Thm.prop_of ind_th') |> apfst the_single handle List.Empty => error "Strong induction: more than one var." val ty_var = type_of pat_var val _ = writeln (name ^ "\nSubstitution: " ^ (Util.string_of_terms_global thy [pat_var, pat_subst])) in thy |> add_typed_induct_data "strong_induct" (ty_var, ind_th') end fun add_case_induct_rule ind_th thy = let val init_assum = ind_th |> Thm.prems_of |> hd |> dest_Trueprop in thy |> add_induct_data "case_induct" (init_assum, ind_th) end fun add_prop_induct_rule ind_th thy = let val init_assum = ind_th |> Thm.prems_of |> hd |> dest_Trueprop in thy |> add_induct_data "prop_induct" (init_assum, ind_th) end fun add_var_induct_rule ind_th thy = let val (P, n) = ind_th |> concl_of' |> Term.dest_comb val _ = assert (Term.is_Var P andalso Term.is_Var n) "add_var_induct_rule: concl of ind_th must be ?P ?var" in thy |> add_typed_induct_data "var_induct" (type_of n, ind_th) end fun add_cases_rule ind_th thy = let val (P, n) = ind_th |> concl_of' |> Term.dest_comb val _ = assert (Term.is_Var P andalso Term.is_Var n) "add_cases_rule: concl of ind_th must be ?P ?var" in thy |> add_typed_induct_data "cases" (type_of n, ind_th) end fun add_fun_induct_rule (t, ind_th) thy = thy |> add_induct_data "fun_induct" (t, ind_th) (* Obtain the induction statement. *) fun get_induct_stmt ctxt (filt_A, ind_vars, stmt, arbitrary) = case stmt of NONE => let val (_, (As, C)) = ctxt |> Auto2_State.get_subgoal |> Util.strip_meta_horn val obj_As = As |> map dest_Trueprop |> filter filt_A val obj_C = dest_Trueprop C in (UtilLogic.list_obj_horn (arbitrary, (obj_As, obj_C))) |> fold Util.lambda_abstract (rev ind_vars) end | SOME s => (UtilLogic.list_obj_horn (arbitrary, ([], Syntax.read_term ctxt s))) |> fold Util.lambda_abstract (rev ind_vars) fun apply_simple_induct_th ind_th vars arbitraries prem_only state = let val {context = ctxt, ...} = Proof.goal state val prop = Auto2_State.get_selected ctxt val (vars', _) = prop |> Thm.prems_of |> the_single |> Util.strip_meta_horn val ind_th = ind_th |> apply_to_thm (Conv.binop_conv (UtilLogic.to_meta_conv ctxt)) val assum = hd (Drule.cprems_of ind_th) val ind_th = ind_th |> Util.send_first_to_hyps |> fold Thm.forall_elim (map (Thm.cterm_of ctxt) arbitraries) |> fold Thm.forall_intr (map (Thm.cterm_of ctxt) vars') |> Thm.implies_intr assum val t' = case Thm.prop_of ind_th of imp $ A $ B => imp $ Util.rename_abs_term vars A $ B | _ => raise Fail "strong_induct_cmd" val ind_th = ind_th |> Thm.renamed_prop t' val prop = prop |> Auto2_Outer.refine_subgoal_th ind_th in if prem_only then let val (_, (As, _)) = prop |> Thm.prems_of |> the_single |> Util.strip_meta_horn val stmt = dest_Trueprop (hd As) in state |> Proof.map_contexts (Auto2_State.map_head_th (K prop)) |> Proof.map_contexts (Auto2_State.set_induct_stmt stmt) |> Proof.map_contexts (Auto2_State.add_prem_only stmt) end else state |> Proof.map_contexts (Auto2_State.map_head_th (K prop)) end fun strong_induct_cmd (s, t) state = let val {context = ctxt, ...} = Proof.goal state val thy = Proof_Context.theory_of ctxt val var = Syntax.read_term ctxt s val arbitraries = map (Syntax.read_term ctxt) t val P = get_induct_stmt ctxt (K true, [var], NONE, arbitraries) val ind_th = get_typed_ind_th thy "strong_induct" (type_of var) val (var_P, var_n) = ind_th |> concl_of' |> Term.dest_comb val inst = fold (Pattern.match thy) [(var_P, P), (var_n, var)] fo_init val ind_th = Util.subst_thm ctxt inst ind_th in state |> apply_simple_induct_th ind_th [var] arbitraries true end val arbitrary = Scan.option (@{keyword "arbitrary"} |-- Scan.repeat Parse.term) val _ = Outer_Syntax.command @{command_keyword "@strong_induct"} "apply strong induction" ((Parse.term -- arbitrary) >> (fn (s, t) => Toplevel.proof (fn state => strong_induct_cmd (s, these t) state))) fun apply_induct_hyp_cmd s state = let val {context = ctxt, ...} = Proof.goal state val ts = Syntax.read_terms ctxt s val induct_stmt = Auto2_State.get_last_induct_stmt ctxt val stmt = induct_stmt |> the |> mk_Trueprop |> Thm.cterm_of ctxt handle Option.Option => raise Fail "apply_induct_hyp: no induct_stmt" val prop = Auto2_State.get_selected ctxt val (_, (As, _)) = prop |> Thm.prems_of |> the_single |> Util.strip_meta_horn val _ = assert (member (op aconv) As (Thm.term_of stmt)) "apply_induct_hyp: induct_stmt not found among As." val cAs = map (Thm.cterm_of ctxt) As val th = stmt |> Thm.assume |> apply_to_thm (UtilLogic.to_meta_conv ctxt) |> fold Thm.forall_elim (map (Thm.cterm_of ctxt) ts) |> apply_to_thm (Util.normalize_meta_all_imp ctxt) val prems = th |> Thm.prems_of |> map (fn t => Logic.list_implies (As, t)) |> map (Thm.cterm_of ctxt) val prems_th = (map (Auto2_Outer.auto2_solve ctxt) prems) |> map Util.send_all_to_hyps val concl = th |> fold Thm.elim_implies prems_th |> fold Thm.implies_intr (rev cAs) val _ = writeln ("Obtained " ^ Syntax.string_of_term ctxt (Thm.concl_of concl)) in state |> Proof.map_contexts ( Auto2_State.map_head_th (Auto2_Outer.have_after_qed ctxt concl)) end val _ = Outer_Syntax.command @{command_keyword "@apply_induct_hyp"} "apply induction hypothesis" ((Scan.repeat Parse.term) >> (fn s => Toplevel.proof (fn state => apply_induct_hyp_cmd s state))) fun solve_goals ind_th pats_opt filt_As state = let val {context = ctxt, ...} = Proof.goal state val (_, (As, _)) = ctxt |> Auto2_State.get_subgoal |> Util.strip_meta_horn val use_As = filter filt_As As val cAs = map (Thm.cterm_of ctxt) As val ind_goals = ind_th |> Thm.prems_of |> map (fn t => Logic.list_implies (use_As, t)) |> map (Thm.cterm_of ctxt) |> map (UtilLogic.to_meta_conv ctxt) in case pats_opt of NONE => let (* Solve the right side, obtain the left side. *) fun solve_eq eq = Thm.equal_elim (meta_sym eq) (Auto2_Outer.auto2_solve ctxt (Thm.rhs_of eq)) val ths = ind_goals |> map solve_eq |> map Util.send_all_to_hyps val ind_concl = ind_th |> fold Thm.elim_implies ths |> fold Thm.implies_intr (rev cAs) val after_qed = Auto2_Outer.have_after_qed ctxt ind_concl in state |> Proof.map_contexts (Auto2_State.map_head_th after_qed) end | SOME pats => let (* Create new block with the subgoals *) fun after_qed ths prop = let val ths' = (ind_goals ~~ ths) |> map (fn (eq, th) => Thm.equal_elim (meta_sym eq) th) |> map Util.send_all_to_hyps val ind_concl = ind_th |> fold Thm.elim_implies ths' |> fold Thm.implies_intr (rev cAs) in Auto2_Outer.have_after_qed ctxt ind_concl prop end val _ = writeln ("Patterns: " ^ Util.string_of_terms ctxt pats) val new_frame = Auto2_State.multiple_frame ( pats ~~ map Thm.rhs_of ind_goals, SOME ([], after_qed)) in state |> Proof.map_contexts (Auto2_State.push_head new_frame) end end fun case_induct_cmd s state = let val {context = ctxt, ...} = Proof.goal state val thy = Proof_Context.theory_of ctxt val start = Syntax.read_term ctxt s val ind_th = get_term_ind_th thy "case_induct" start (* Obtain list of assumptions *) val (_, (_, C)) = ctxt |> Auto2_State.get_subgoal |> Util.strip_meta_horn (* Instantiate the induction theorem *) val var_P = concl_of' ind_th val inst = Pattern.match thy (var_P, dest_Trueprop C) fo_init val ind_th = Util.subst_thm_thy thy inst ind_th in state |> solve_goals ind_th NONE (K true) end val _ = Outer_Syntax.command @{command_keyword "@case_induct"} "apply induction" (Parse.term >> (fn s => Toplevel.proof (fn state => case_induct_cmd s state))) val for_stmt = Scan.option (@{keyword "for"} |-- Parse.term) fun prop_induct_cmd (s, t) state = let val {context = ctxt, ...} = Proof.goal state val thy = Proof_Context.theory_of ctxt val start = Syntax.read_term ctxt s val ind_th = get_term_ind_th thy "prop_induct" start val (var_P, args) = ind_th |> concl_of' |> Term.strip_comb val start_As = strip_conj start val filt_A = (fn t => not (member (op aconv) start_As t)) val P = get_induct_stmt ctxt (filt_A, args, t, []) val _ = writeln ("Induct statement: " ^ Syntax.string_of_term ctxt P) val inst = Pattern.match thy (var_P, P) fo_init (* Instantiate the induction theorem *) val ind_th = Util.subst_thm_thy thy inst ind_th in state |> solve_goals ind_th NONE (K true) end val _ = Outer_Syntax.command @{command_keyword "@prop_induct"} "apply induction" ((Parse.term -- for_stmt) >> (fn (s, t) => Toplevel.proof (fn state => prop_induct_cmd (s, t) state))) (* Given an induction subgoal of the form !!x_i. A_i ==> C, retrieve the list of induction patterns. *) fun retrieve_pat ind_vars t = let val (vars, (_, C)) = Util.strip_meta_horn t fun free_to_var t = let val (x, T) = Term.dest_Free t in Var ((x,0), T) end val pat_vars = map free_to_var vars val args = C |> dest_Trueprop |> Util.dest_args |> map (Term.subst_atomic (vars ~~ pat_vars)) in HOLogic.mk_tuple (map mk_eq (ind_vars ~~ args)) end fun induct_cmd ind_ty_str (s, t, u, v) state = let val {context = ctxt, ...} = Proof.goal state val thy = Proof_Context.theory_of ctxt val var = Syntax.read_term ctxt s val arbitraries = map (Syntax.read_term ctxt) u val filt_A = Util.occurs_frees (var :: arbitraries) val P = get_induct_stmt ctxt (filt_A, [var], t, arbitraries) val ind_th = get_typed_ind_th thy ind_ty_str (type_of var) (* Instantiate the induction theorem *) val concl = concl_of' ind_th val (var_P, var_n) = Term.dest_comb concl val inst = fold (Pattern.match thy) [(var_P, P), (var_n, var)] fo_init val ind_th' = Util.subst_thm_thy thy inst ind_th val pats = case v of NONE => NONE | _ => SOME (map (retrieve_pat [var]) (Thm.prems_of ind_th)) in state |> solve_goals ind_th' pats (not o filt_A) end val _ = Outer_Syntax.command @{command_keyword "@induct"} "apply induction" (Parse.term -- for_stmt -- arbitrary -- Scan.option @{keyword "@with"} >> (fn (((s, t), u), v) => Toplevel.proof ( fn state => induct_cmd "var_induct" (s, t, these u, v) state))) val _ = Outer_Syntax.command @{command_keyword "@cases"} "apply induction" (Parse.term -- Scan.option @{keyword "@with"} >> (fn (s, v) => Toplevel.proof ( fn state => induct_cmd "cases" (s, NONE, [], v) state))) fun get_fun_induct_th thy t = let val ind_th = get_term_ind_th thy "fun_induct" (Term.head_of t) handle Fail _ => Global_Theory.get_thm thy (Util.get_head_name t ^ ".induct") handle ERROR _ => raise Fail "fun_induct: cannot find theorem." val (_, args) = Term.strip_comb t val (_, pat_args) = ind_th |> concl_of' |> Term.strip_comb val inst = Util.first_order_match_list thy (pat_args ~~ args) fo_init in Util.subst_thm_thy thy inst ind_th end fun is_simple_fun_induct ind_th = let val prems = Thm.prems_of ind_th in if length prems > 1 then false else let val (var, (_, C)) = Util.strip_meta_horn (the_single prems) val (_, args) = Term.strip_comb (dest_Trueprop C) in eq_list (op aconv) (var, args) end end fun fun_induct_cmd (s, t, u) state = let val {context = ctxt, ...} = Proof.goal state val thy = Proof_Context.theory_of ctxt val expr = Syntax.read_term ctxt s val arbitraries = map (Syntax.read_term ctxt) t val ind_th = get_fun_induct_th thy expr val (var_P, vars) = ind_th |> concl_of' |> Term.strip_comb in if is_simple_fun_induct ind_th then let val _ = assert (is_none u) "fun_induct: simple induction." (* Instantiate the induction theorem *) val P = get_induct_stmt ctxt (K true, vars, NONE, arbitraries) val inst = Pattern.match thy (var_P, P) fo_init val ind_th = Util.subst_thm_thy thy inst ind_th in state |> apply_simple_induct_th ind_th vars arbitraries false end else let (* Instantiate the induction theorem *) val filt_A = Util.occurs_frees (vars @ arbitraries) val P = get_induct_stmt ctxt (filt_A, vars, NONE, arbitraries) val inst = Pattern.match thy (var_P, P) fo_init val ind_th' = ind_th |> Util.subst_thm_thy thy inst val prems = Thm.prems_of ind_th val pats = case u of NONE => NONE | SOME _ => SOME (map (retrieve_pat vars) prems) in state |> solve_goals ind_th' pats (not o filt_A) end end val _ = Outer_Syntax.command @{command_keyword "@fun_induct"} "apply induction" (Parse.term -- arbitrary -- Scan.option @{keyword "@with"} >> (fn ((s, t), u) => Toplevel.proof (fn state => fun_induct_cmd (s, these t, u) state))) end (* structure Induct_ProofSteps. *) val add_strong_induct_rule = Induct_ProofSteps.add_strong_induct_rule val add_case_induct_rule = Induct_ProofSteps.add_case_induct_rule val add_prop_induct_rule = Induct_ProofSteps.add_prop_induct_rule val add_var_induct_rule = Induct_ProofSteps.add_var_induct_rule val add_fun_induct_rule = Induct_ProofSteps.add_fun_induct_rule val add_cases_rule = Induct_ProofSteps.add_cases_rule diff --git a/thys/Auto2_HOL/consts.ML b/thys/Auto2_HOL/consts.ML --- a/thys/Auto2_HOL/consts.ML +++ b/thys/Auto2_HOL/consts.ML @@ -1,66 +1,65 @@ (* File: consts.ML Author: Bohua Zhan Dealing with constants. *) signature CONSTS = sig val add_const_data: string * (term -> bool) -> theory -> theory val detect_const: theory -> term -> string option val detect_const_ctxt: Proof.context -> term -> string option val is_const: theory -> term -> bool val is_const_ctxt: Proof.context -> term -> bool val neq_const: theory -> term * term -> bool val neq_const_ctxt: Proof.context -> term * term -> bool end; structure Consts : CONSTS = struct (* Table of detectors for constants, each registered under a descriptive name. *) structure Data = Theory_Data ( type T = (term -> bool) Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge pointer_eq ) fun add_const_data (str, f) = Data.map (Symtab.update_new (str, f)) fun detect_const thy t = let val data = Symtab.dest (Data.get thy) in get_first (fn (str, f) => if f t then SOME str else NONE) data end fun detect_const_ctxt ctxt t = detect_const (Proof_Context.theory_of ctxt) t fun is_const thy t = is_some (detect_const thy t) fun is_const_ctxt ctxt t = is_const (Proof_Context.theory_of ctxt) t (* Whether two constants are of the same type and not equal. If either input is not a constant, return false. *) fun neq_const thy (t1, t2) = let val ty1 = the (detect_const thy t1) val ty2 = the (detect_const thy t2) in ty1 = ty2 andalso not (t1 aconv t2) end handle Option.Option => false fun neq_const_ctxt ctxt (t1, t2) = neq_const (Proof_Context.theory_of ctxt) (t1, t2) end (* structure Consts. *) diff --git a/thys/Auto2_HOL/items.ML b/thys/Auto2_HOL/items.ML --- a/thys/Auto2_HOL/items.ML +++ b/thys/Auto2_HOL/items.ML @@ -1,698 +1,697 @@ (* File: items.ML Author: Bohua Zhan Items and matching on items. *) val TY_NULL = "NULL" val TY_EQ = "EQ" val TY_VAR = "VAR" val TY_PROP = "PROP" val TY_TERM = "TERM" val TY_PROPERTY = "PROPERTY" datatype raw_item = Handler of term list * term * thm | Fact of string * term list * thm type box_item = {uid: int, id: box_id, sc: int, ty_str: string, tname: cterm list, prop: thm} signature BOXITEM = sig (* Facts. *) val var_to_fact: term -> raw_item val term_to_fact: term -> raw_item val is_fact_raw: raw_item -> bool val match_ty_str_raw: string -> raw_item -> bool val match_ty_strs_raw: string list -> raw_item -> bool val get_tname_raw: raw_item -> term list val get_thm_raw: raw_item -> thm (* Handlers. *) val is_handler_raw: raw_item -> bool val dest_handler_raw: raw_item -> term list * term * thm (* Misc. functions. *) val eq_ritem: raw_item * raw_item -> bool val instantiate: (cterm * cterm) list -> raw_item -> raw_item val obtain_variant_frees: Proof.context * raw_item list -> Proof.context * (cterm * cterm) list val null_item: box_item val item_with_id: box_id -> box_item -> box_item val item_with_incr: box_item -> box_item val item_replace_incr: box_item -> box_item val eq_item: box_item * box_item -> bool val match_ty_str: string -> box_item -> bool val match_ty_strs: string list -> box_item -> bool (* Misc. functions. *) val merged_id: Proof.context -> box_item list -> box_id val mk_box_item: Proof.context -> int * box_id * int * raw_item -> box_item end; structure BoxItem : BOXITEM = struct fun var_to_fact t = Fact (TY_VAR, [t], true_th) fun term_to_fact t = Fact (TY_TERM, [t], true_th) fun is_fact_raw ritem = case ritem of Fact _ => true | _ => false fun match_ty_str_raw s ritem = case ritem of Fact (ty_str, _, _) => s = "" orelse ty_str = s | _ => false fun match_ty_strs_raw slist ritem = case ritem of Fact (ty_str, _, _) => member (op =) slist ty_str | _ => false fun get_tname_raw ritem = case ritem of Fact (_, ts, _) => ts | _ => raise Fail "get_tname_raw" fun get_thm_raw ritem = case ritem of Fact (_, _, th) => th | _ => raise Fail "get_thm_raw" fun is_handler_raw ritem = case ritem of Handler _ => true | _ => false fun dest_handler_raw ritem = case ritem of Handler (vars, t, ex_th) => (vars, t, ex_th) | _ => raise Fail "dest_handler_raw: wrong type" fun eq_ritem (ritem1, ritem2) = case ritem1 of Fact (ty1, ts1, th1) => (case ritem2 of Fact (ty2, ts2, th2) => ty1 = ty2 andalso eq_list (op aconv) (ts1, ts2) andalso Thm.eq_thm_prop (th1, th2) | _ => false) | Handler (vars1, t1, ex_th1) => (case ritem2 of Fact _ => false | Handler (vars2, t2, ex_th2) => eq_list (op aconv) (vars1, vars2) andalso t1 aconv t2 andalso Thm.eq_thm_prop (ex_th1, ex_th2)) (* Given a context and list of raw items, obtain fresh names of free variables for each internal (schematic) variable declared in the raw items, and declare the new variables in context. Return the substitution from internal schematic variables to the new free variables. *) fun obtain_variant_frees (ctxt, ritems) = let (* Original internal variables. *) val all_vars = ritems |> filter (match_ty_str_raw TY_VAR) |> maps get_tname_raw |> filter is_Free |> map dest_Free |> filter (Util.is_just_internal o fst) (* New names for these variables. *) val all_vars' = all_vars |> map (fn (x, T) => (Name.dest_internal x, T)) |> Variable.variant_frees ctxt [] val subst = map (apply2 (Thm.cterm_of ctxt o Free)) (all_vars ~~ all_vars') in (fold Util.declare_free_term (map Free all_vars') ctxt, subst) end (* Here inst is the return value of obtain_variant_frees. Perform the replacement on the ritems. *) fun instantiate subst ritem = let val subst_fun = Term.subst_atomic (map (apply2 Thm.term_of) subst) in case ritem of Handler (vars, t, ex_th) => Handler (map subst_fun vars, subst_fun t, Util.subst_thm_atomic subst ex_th) | Fact (ty_str, tname, th) => Fact (ty_str, map subst_fun tname, Util.subst_thm_atomic subst th) end val null_item = {uid = 0, id = [], sc = 0, ty_str = TY_NULL, tname = [], prop = true_th} fun item_with_id id {uid, sc, ty_str, tname, prop, ...} = {uid = uid, id = id, sc = sc, ty_str = ty_str, tname = tname, prop = prop} fun item_with_incr item = item_with_id (BoxID.add_incr_id (#id item)) item fun item_replace_incr item = item_with_id (BoxID.replace_incr_id (#id item)) item fun eq_item (item1, item2) = (#uid item1 = #uid item2) fun match_ty_str s {ty_str, ...} = (s = "" orelse s = ty_str) fun match_ty_strs slist {ty_str, ...} = member (op =) slist ty_str fun merged_id ctxt items = case items of [] => [] | {id, ...} :: items' => BoxID.merge_boxes ctxt (id, merged_id ctxt items') fun mk_box_item ctxt (uid, id, sc, ritem) = case ritem of Handler _ => raise Fail "mk_box_item: ritem must be Fact" | Fact (ty_str, ts, prop) => {uid = uid, id = id, sc = sc, ty_str = ty_str, tname = map (Thm.cterm_of ctxt) ts, prop = prop} end (* structure BoxItem. *) (* Specifies a method for matching patterns against items. - pre_match is a filter function checking whether it is possible for the pattern to match the item, after possibly instantiating some schematic variables in the pattern (for example, this function should always return true if input pattern is ?A). - match is the actual matching function, returning instantiation, as well as theorem justifying the instantiated pattern. If the matcher is for justifying a proposition, the input term to pre_match and match is of type bool. Othewise, the restrictions depend on type of item to match. *) type item_matcher = { pre_match: term -> box_item -> Proof.context -> bool, match: term -> box_item -> Proof.context -> id_inst -> id_inst_th list } (* Output function for items of a given type. *) type item_output = Proof.context -> term list * thm -> string (* Data structure containing methods involved in the input / output of items of a given type. - prop_matchers: methods for matching the item against a desired proposition. - typed_matchers: methods for matching the item against a pattern for items of the same type. - output_fn: printing function of theorems. Input is tname and the proposition. *) type item_io_info = { prop_matchers: item_matcher list, typed_matchers: item_matcher list, term_fn: (term list -> term list) option, output_fn: item_output option, shadow_fn: (Proof.context -> box_id -> term list * cterm list -> bool) option } datatype match_arg = PropMatch of term | TypedMatch of string * term | TypedUniv of string | PropertyMatch of term | WellFormMatch of term * term type prfstep_filter = Proof.context -> id_inst -> bool signature ITEM_IO = sig val pat_of_match_arg: match_arg -> term val subst_arg: Type.tyenv * Envir.tenv -> match_arg -> match_arg val assert_valid_arg: match_arg -> unit val check_ty_str: string -> match_arg -> bool val is_ordinary_match: match_arg -> bool val is_side_match: match_arg -> bool val add_item_type: string * (term list -> term list) option * item_output option * (Proof.context -> box_id -> term list * cterm list -> bool) option -> theory -> theory val add_prop_matcher: string * item_matcher -> theory -> theory val add_typed_matcher: string * item_matcher -> theory -> theory val get_io_info: theory -> string -> item_io_info val get_prop_matchers: theory -> string -> item_matcher list val get_typed_matchers: theory -> string -> item_matcher list val prop_matcher: item_matcher val term_prop_matcher: item_matcher val null_eq_matcher: item_matcher val term_typed_matcher: item_matcher val eq_tname_typed_matcher: item_matcher val null_property_matcher: item_matcher val term_property_matcher: item_matcher val pre_match_arg: Proof.context -> match_arg -> box_item -> bool val match_arg: Proof.context -> match_arg -> box_item -> id_inst -> id_inst_th list val no_rewr_terms: term list -> term list val rewr_terms_of_item: Proof.context -> string * term list -> term list val output_prop_fn: item_output val string_of_item_info: Proof.context -> string * term list * thm -> string val add_basic_item_io: theory -> theory val string_of_raw_item: Proof.context -> raw_item -> string val string_of_item: Proof.context -> box_item -> string val trace_ritem: Proof.context -> string -> raw_item -> unit val trace_item: Proof.context -> string -> box_item -> unit val trace_ritems: Proof.context -> string -> raw_item list -> unit val trace_items: Proof.context -> string -> box_item list -> unit end; structure ItemIO : ITEM_IO = struct fun add_prop_matcher_to_info mtch {prop_matchers, typed_matchers, term_fn, output_fn, shadow_fn} = {prop_matchers = mtch :: prop_matchers, typed_matchers = typed_matchers, term_fn = term_fn, output_fn = output_fn, shadow_fn = shadow_fn} fun add_typed_matcher_to_info mtch {prop_matchers, typed_matchers, term_fn, output_fn, shadow_fn} = {prop_matchers = prop_matchers, typed_matchers = mtch :: typed_matchers, term_fn = term_fn, output_fn = output_fn, shadow_fn = shadow_fn} fun join_infos ( {prop_matchers = pm1, typed_matchers = tm1, term_fn = tf1, output_fn = of1, shadow_fn = sf1}, {prop_matchers = pm2, typed_matchers = tm2, term_fn = tf2, output_fn = of2, shadow_fn = sf2}) = {prop_matchers = merge pointer_eq (pm1, pm2), typed_matchers = merge pointer_eq (tm1, tm2), term_fn = (if pointer_eq (tf1, tf2) then tf1 else raise Fail "join_infos: term_fn non-equal"), output_fn = (if pointer_eq (of1, of2) then of1 else raise Fail "join_infos: output_fn non-equal"), shadow_fn = (if pointer_eq (sf1, sf2) then sf1 else raise Fail "join_infos: shadow_fn non-equal")} structure Data = Theory_Data ( type T = item_io_info Symtab.table val empty = Symtab.empty - val extend = I; val merge = Symtab.join (fn _ => join_infos) ) fun pat_of_match_arg arg = case arg of PropMatch pat => pat | TypedMatch (_, pat) => pat | TypedUniv _ => Term.dummy | PropertyMatch pat => pat | WellFormMatch (_, req) => req fun subst_arg inst arg = case arg of PropMatch pat => PropMatch (Util.subst_term_norm inst pat) | TypedMatch (ty_str, pat) => TypedMatch (ty_str, Util.subst_term_norm inst pat) | TypedUniv ty_str => TypedUniv ty_str | PropertyMatch pat => PropertyMatch (Util.subst_term_norm inst pat) | WellFormMatch (t, req) => WellFormMatch (Util.subst_term_norm inst t, Util.subst_term_norm inst req) fun assert_valid_arg arg = case arg of PropMatch pat => assert (fastype_of pat = boolT) "assert_valid_arg: arg for PropMatch should be bool." | TypedMatch _ => () | TypedUniv _ => () | PropertyMatch pat => assert (fastype_of pat = boolT) "assert_valid_arg: arg for PropertyMatch should be bool." | WellFormMatch (_, req) => assert (fastype_of req = boolT) "assert_valid_arg: arg for WellFormMatch should be bool." fun check_ty_str ty_str arg = case arg of TypedMatch (ty_str', _) => ty_str = ty_str' | TypedUniv ty_str' => ty_str = ty_str' | _ => true fun is_ordinary_match arg = case arg of PropMatch _ => true | TypedMatch _ => true | _ => false fun is_side_match arg = case arg of PropertyMatch _ => true | WellFormMatch _ => true | _ => false fun add_item_type (ty_str, term_fn, output_fn, shadow_fn) = let val item_info = {prop_matchers = [], typed_matchers = [], term_fn = term_fn, output_fn = output_fn, shadow_fn = shadow_fn} in Data.map (Symtab.update_new (ty_str, item_info)) end fun add_prop_matcher (ty_str, it_match) = Data.map ( Symtab.map_entry ty_str (add_prop_matcher_to_info it_match)) fun add_typed_matcher (ty_str, it_match) = Data.map ( Symtab.map_entry ty_str (add_typed_matcher_to_info it_match)) fun get_io_info thy ty_str = the (Symtab.lookup (Data.get thy) ty_str) handle Option.Option => raise Fail ("get_io_info: not found " ^ ty_str) fun get_prop_matchers thy ty_str = #prop_matchers (get_io_info thy ty_str) fun get_typed_matchers thy ty_str = #typed_matchers (get_io_info thy ty_str) (* Prop-matching with a PROP item. *) val prop_matcher = let fun pre_match pat {tname, ...} ctxt = let val ct = the_single tname val t = Thm.term_of ct in if is_neg pat then is_neg t andalso Matcher.pre_match_head ctxt (get_neg pat, UtilLogic.get_cneg ct) else Term.is_Var pat orelse (not (is_neg t) andalso Matcher.pre_match_head ctxt (pat, ct)) end fun match pat {tname, prop, ...} ctxt (id, inst) = let val ct = the_single tname val t = Thm.term_of ct in if is_neg pat andalso is_neg t then let val insts' = Matcher.rewrite_match_head ctxt (get_neg pat, UtilLogic.get_cneg ct) (id, inst) fun process_inst (inst, eq_th) = let (* This version certainly will not cancel ~~ on two sides. *) val make_neg_eq' = Thm.combination (Thm.reflexive UtilBase.cNot) in (inst, Thm.equal_elim ( make_trueprop_eq (make_neg_eq' (meta_sym eq_th))) prop) end in map process_inst insts' end else if not (is_neg pat) andalso (Term.is_Var pat orelse not (is_neg t)) then let val insts' = Matcher.rewrite_match_head ctxt (pat, ct) (id, inst) fun process_inst (inst, eq_th) = (inst, Thm.equal_elim ( make_trueprop_eq (meta_sym eq_th)) prop) in map process_inst insts' end else [] end in {pre_match = pre_match, match = match} end (* Prop-matching with a TERM item (used to justify equalities). *) val term_prop_matcher = let fun pre_match pat {tname, ...} ctxt = if not (Util.has_vars pat) then false else if is_eq_term pat then Matcher.pre_match ctxt (fst (dest_eq pat), the_single tname) else false fun match pat {tname, ...} ctxt (id, inst) = if not (is_eq_term pat) then [] else if not (Util.has_vars pat) then [] else let val (lhs, rhs) = dest_eq pat val cu = the_single tname val pairs = if Term.is_Var lhs then [(false, (lhs, cu)), (true, (rhs, cu))] else [(true, (lhs, cu)), (false, (rhs, cu))] val insts' = Matcher.rewrite_match_list ctxt pairs (id, inst) fun process_inst (inst, ths) = let (* th1: lhs(env) == u, th2: rhs(env) == u. *) val (th1, th2) = the_pair ths in (inst, to_obj_eq (Util.transitive_list [th1, meta_sym th2])) end in map process_inst insts' end in {pre_match = pre_match, match = match} end val null_eq_matcher = let fun pre_match pat _ _ = is_eq_term pat fun match pat _ ctxt (id, inst) = if not (is_eq_term pat) then [] else if Util.has_vars pat then [] else let val (lhs, rhs) = dest_eq pat val infos = RewriteTable.equiv_info_t ctxt id (lhs, rhs) fun process_info (id', th) = ((id', inst), to_obj_eq th) in map process_info infos end in {pre_match = pre_match, match = match} end (* Typed matching with a TERM item. *) val term_typed_matcher = let fun pre_match pat {tname, ...} ctxt = Matcher.pre_match_head ctxt (pat, the_single tname) (* Return value is (inst, eq), where eq is pat(inst) == tname. *) fun match pat {tname, ...} ctxt (id, inst) = Matcher.rewrite_match_head ctxt (pat, the_single tname) (id, inst) in {pre_match = pre_match, match = match} end (* Typed matching for items representing an equality ?A = ?B, where the tname is the pair (?A, ?B). Pattern is expected to be of the form ?A = ?B. *) val eq_tname_typed_matcher = let fun pre_match pat {tname, ...} ctxt = let val thy = Proof_Context.theory_of ctxt val (lhs, rhs) = the_pair (map Thm.term_of tname) val _ = Pattern.first_order_match thy (pat, mk_eq (lhs, rhs)) fo_init in true end handle Pattern.MATCH => false fun match pat {tname, ...} ctxt (id, inst) = let val thy = Proof_Context.theory_of ctxt val (lhs, rhs) = the_pair (map Thm.term_of tname) val inst' = Pattern.first_order_match thy (pat, mk_eq (lhs, rhs)) inst in [((id, inst'), true_th)] end handle Pattern.MATCH => [] in {pre_match = pre_match, match = match} end (* Obtain a proposition from the property table. *) val null_property_matcher = let fun pre_match pat _ _ = Property.is_property pat fun match pat _ ctxt (id, inst) = if Util.has_vars pat then [] else if not (Property.is_property pat) then [] else map (fn (id', th) => ((id', inst), th)) (PropertyData.get_property_t ctxt (id, pat)) in {pre_match = pre_match, match = match} end (* Obtain a proposition from the property table, matching the argument of the property with the given term. *) val term_property_matcher = let fun pre_match pat {tname, ...} ctxt = Property.is_property pat andalso Matcher.pre_match_head ctxt ( Property.get_property_arg pat, the_single tname) fun match pat {tname, ...} ctxt (id, inst) = if not (Util.has_vars pat) then [] else if not (Property.is_property pat) then [] else let val arg = Property.get_property_arg pat in let val insts' = Matcher.rewrite_match_head ctxt (arg, the_single tname) (id, inst) fun process_inst ((id', inst'), _) = let val t = Util.subst_term_norm inst' pat in map (fn (id'', th) => ((id'', inst'), th)) (PropertyData.get_property_t ctxt (id', t)) end in maps process_inst insts' end end in {pre_match = pre_match, match = match} end (* Generic pre-matching function. Returns whether there is a possible match among any of the registered matchers. *) fun pre_match_arg ctxt arg (item as {ty_str, ...}) = if not (check_ty_str ty_str arg) then false else let val _ = assert_valid_arg arg val thy = Proof_Context.theory_of ctxt val {prop_matchers, typed_matchers, ...} = get_io_info thy ty_str in case arg of PropMatch pat => Term.is_Var pat orelse (is_neg pat andalso Term.is_Var (get_neg pat)) orelse not (Util.is_pattern pat) orelse exists (fn f => f pat item ctxt) (map #pre_match prop_matchers) | TypedMatch (_, pat) => not (Util.is_pattern pat) orelse exists (fn f => f pat item ctxt) (map #pre_match typed_matchers) | TypedUniv _ => true | PropertyMatch _ => raise Fail "pre_match_arg: should not be called on PropertyMatch." | WellFormMatch _ => raise Fail "pre_match_arg: should not be called on WellFormMatch." end (* Generic matching function. Returns list of all matches (iterating over all registered matchers for the given item type. Note box_id for item is taken into account here. *) fun match_arg ctxt arg (item as {id, ty_str, ...}) (id', inst) = if not (check_ty_str ty_str arg) then [] else let val _ = assert_valid_arg arg val thy = Proof_Context.theory_of ctxt val {prop_matchers, typed_matchers, ...} = get_io_info thy ty_str val pat = pat_of_match_arg arg val id'' = BoxID.merge_boxes ctxt (id, id') in case arg of PropMatch _ => maps (fn f => f pat item ctxt (id'', inst)) (map #match prop_matchers) | TypedUniv _ => [((id'', inst), true_th)] | TypedMatch _ => maps (fn f => f pat item ctxt (id'', inst)) (map #match typed_matchers) | PropertyMatch _ => raise Fail "match_arg: should not be called on PropertyMatch." | WellFormMatch _ => raise Fail "match_arg: should not be called on WellFormMatch." end val no_rewr_terms = K [] fun arg_rewr_terms ts = maps Util.dest_args ts fun prop_rewr_terms ts = let val t = the_single ts in if is_neg t then t |> dest_arg |> Util.dest_args else t |> Util.dest_args end fun rewr_terms_of_item ctxt (ty_str, tname) = let val thy = Proof_Context.theory_of ctxt val {term_fn, ...} = get_io_info thy ty_str in case term_fn of NONE => tname | SOME f => f tname end fun output_prop_fn ctxt (_, th) = Thm.prop_of th |> Syntax.string_of_term ctxt fun string_of_item_info ctxt (ty_str, ts, th) = let val thy = Proof_Context.theory_of ctxt val {output_fn, ...} = get_io_info thy ty_str in case output_fn of NONE => ty_str ^ " " ^ (Util.string_of_terms ctxt ts) | SOME f => f ctxt (ts, th) end fun string_of_raw_item ctxt ritem = case ritem of Handler (_, t, _) => "Handler " ^ (Syntax.string_of_term ctxt t) | Fact info => string_of_item_info ctxt info fun string_of_item ctxt {ty_str, tname, prop, ...} = string_of_item_info ctxt (ty_str, map Thm.term_of tname, prop) fun trace_ritem ctxt s ritem = tracing (s ^ " " ^ (string_of_raw_item ctxt ritem)) fun trace_ritems ctxt s ritems = tracing (s ^ "\n" ^ (cat_lines (map (string_of_raw_item ctxt) ritems))) fun trace_item ctxt s item = tracing (s ^ " " ^ (string_of_item ctxt item)) fun trace_items ctxt s items = tracing (s ^ "\n" ^ (cat_lines (map (string_of_item ctxt) items))) (* We assume ts1 is the new item at the given id, while cts2 is for an existing item, at some previous id. *) fun shadow_prop_fn ctxt id (ts1, cts2) = let val (t1, ct2) = (the_single ts1, the_single cts2) val (lhs, crhs) = if is_neg t1 andalso is_neg (Thm.term_of ct2) then (get_neg t1, UtilLogic.get_cneg ct2) else (t1, ct2) in (Matcher.rewrite_match_head ctxt (lhs, crhs) (id, fo_init)) |> filter (fn ((id', _), _) => id' = id) |> not o null end fun shadow_term_fn ctxt id (ts1, cts2) = let val (lhs, crhs) = (the_single ts1, the_single cts2) in (Matcher.rewrite_match_head ctxt (lhs, crhs) (id, fo_init)) |> filter (fn ((id', _), _) => id' = id) |> not o null end val add_basic_item_io = fold add_item_type [ (TY_NULL, NONE, NONE, NONE), (TY_PROP, SOME prop_rewr_terms, SOME output_prop_fn, SOME shadow_prop_fn), (TY_TERM, SOME no_rewr_terms, NONE, SOME shadow_term_fn), (TY_EQ, NONE, SOME output_prop_fn, NONE), (TY_VAR, NONE, NONE, NONE), (TY_PROPERTY, SOME arg_rewr_terms, NONE, NONE) ] #> fold add_prop_matcher [ (TY_PROP, prop_matcher), (TY_TERM, term_prop_matcher), (TY_NULL, null_eq_matcher), (TY_NULL, null_property_matcher), (TY_TERM, term_property_matcher) ] #> fold add_typed_matcher [ (TY_PROP, prop_matcher), (TY_TERM, term_typed_matcher), (TY_VAR, term_typed_matcher), (TY_EQ, eq_tname_typed_matcher) ] end (* structure ItemIO. *) diff --git a/thys/Auto2_HOL/normalize.ML b/thys/Auto2_HOL/normalize.ML --- a/thys/Auto2_HOL/normalize.ML +++ b/thys/Auto2_HOL/normalize.ML @@ -1,291 +1,289 @@ (* File: normalize.ML Author: Bohua Zhan Normalization procedure for facts obtained during a proof. *) type normalizer = Proof.context -> raw_item -> raw_item list signature NORMALIZER = sig val add_normalizer: string * normalizer -> theory -> theory val add_th_normalizer: string * (Proof.context -> thm -> thm list) -> theory -> theory val add_rewr_normalizer: string * thm -> theory -> theory val get_normalizers: theory -> (string * normalizer) list val normalize: Proof.context -> raw_item -> raw_item list val normalize_keep: Proof.context -> raw_item -> raw_item list (* Normalization of definition of variable *) val add_inj_struct_data: thm -> theory -> theory val is_def_eq: theory -> term -> bool val swap_eq_to_front: conv val meta_use_vardef: thm -> (term * term) list * thm val meta_use_vardefs: thm -> (term * term) list * thm val def_subst: (term * term) list -> term -> term end; structure Normalizer : NORMALIZER = struct (* Keeps list of normalizers. *) structure Data = Theory_Data ( type T = normalizer Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge pointer_eq ) fun add_normalizer (norm_name, norm_fun) = Data.map (Symtab.update_new (norm_name, norm_fun)) (* Apply norm_fun: thm -> thm list to any PROP item. *) fun th_normalizer norm_fun ctxt ritem = case ritem of Handler _ => [ritem] | Fact (ty_str, _, th) => if ty_str = TY_PROP then map Update.thm_to_ritem (norm_fun ctxt th) else [ritem] fun add_th_normalizer (norm_name, norm_fun) = add_normalizer (norm_name, th_normalizer norm_fun) (* eq_th is a meta equality. *) fun rewr_normalizer eq_th ctxt ritem = let val cv = (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv eq_th))) ctxt) then_conv (Thm.beta_conversion true) in case ritem of Handler _ => [ritem] | Fact (ty_str, _, th) => if ty_str = TY_PROP then [Update.thm_to_ritem (apply_to_thm cv th)] else if ty_str = TY_EQ then if Util.is_meta_eq (Thm.prop_of th) then (* Equality between lambda terms *) [ritem] else let (* Apply to right side *) val th' = apply_to_thm' (Conv.arg_conv cv) th val (lhs, rhs) = dest_eq (prop_of' th') in [Fact (TY_EQ, [lhs, rhs], th')] end else [ritem] end fun add_rewr_normalizer (norm_name, eq_th) = add_normalizer (norm_name, rewr_normalizer eq_th) fun get_normalizers thy = Symtab.dest (Data.get thy) fun normalize ctxt ritem = let val norms = get_normalizers (Proof_Context.theory_of ctxt) fun apply_norm (_, norm_fun) ritems = maps (norm_fun ctxt) ritems val norm_once = fold apply_norm norms [ritem] in case norm_once of [ritem'] => if BoxItem.eq_ritem (ritem, ritem') then [ritem'] else normalize ctxt ritem' | _ => maps (normalize ctxt) norm_once end (* Perform normalization, but keep the original ritem. *) fun normalize_keep ctxt ritem = let val norm_ritems = normalize ctxt ritem in if length norm_ritems = 1 then norm_ritems else ritem :: norm_ritems end (* Normalization of variable definition *) structure InjStructData = Theory_Data ( type T = thm Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge pointer_eq ) fun add_inj_struct_data th thy = let val (lhs, _) = th |> prop_of' |> dest_eq |> fst |> dest_eq val (f, _) = Term.strip_comb lhs in case f of Const (nm, _) => InjStructData.map (Symtab.update_new (nm, th)) thy | _ => raise Fail "add_inj_struct_data" end (* Check whether t is of the form ?A = t, where t does not contain ?A. *) fun inj_args thy t = if Term.is_Var t then [t] else let val (f, args) = Term.strip_comb t in if Term.is_Const f andalso Symtab.defined (InjStructData.get thy) (Util.get_head_name f) then maps (inj_args thy) args else [t] end fun is_def_eq thy t = if not (is_eq_term t) then false else let val (lhs, rhs) = dest_eq t val (l_args, r_args) = apply2 (inj_args thy) (lhs, rhs) in forall Term.is_Var l_args andalso not (forall Term.is_Var r_args) andalso forall (fn t => not (Util.is_subterm t rhs)) l_args end fun is_def_eq' thy t = is_Trueprop t andalso is_def_eq thy (dest_Trueprop t) fun is_neg_def_eq thy t = is_neg t andalso is_def_eq thy (dest_not t) (* Given t of the form A_1 ==> ... ==> A_n ==> C, swap all A_i of the form ?A = t to the front. *) fun swap_eq_to_front ct = let val t = Thm.term_of ct val thy = Thm.theory_of_cterm ct in if Util.is_implies t then if is_def_eq' thy (dest_arg1 t) then Conv.all_conv ct else Conv.every_conv [Conv.arg_conv swap_eq_to_front, Conv.rewr_conv Drule.swap_prems_eq] ct else Conv.no_conv ct end (* Given th where the first premise is in the form ?A = t, or f ?A_1 ... ?A_n = t, where f is injective, replace ?A or each ?A_i in the rest of th, and remove the first premise. *) fun meta_use_vardef th = if not (Util.is_implies (Thm.prop_of th)) then ([], th) else let val cprem = th |> Thm.cprop_of |> Thm.dest_arg1 |> Thm.dest_arg val prem = Thm.term_of cprem val thy = Thm.theory_of_thm th in if is_conj prem then th |> apply_to_thm (Conv.rewr_conv (meta_sym @{thm atomize_conjL})) |> meta_use_vardef else if is_def_eq thy prem then let val (c_lhs, c_rhs) = cdest_eq cprem val (lhs, rhs) = dest_eq prem in if Term.is_Var lhs then let val (pairs, th') = th |> Util.subst_thm_atomic [(c_lhs, c_rhs)] |> apply_to_thm (Conv.arg1_conv UtilBase.to_meta_eq_cv) |> Thm.elim_implies (Thm.reflexive c_rhs) |> meta_use_vardef in ((lhs, rhs) :: pairs, th') end else let val nm = Util.get_head_name lhs val data = InjStructData.get thy val inj_th = the (Symtab.lookup data nm) handle Option.Option => raise Fail "meta_use_vardef" in th |> apply_to_thm ( Conv.arg1_conv (Conv.arg_conv (rewr_obj_eq inj_th))) |> meta_use_vardef end end else ([], th) end fun disj_ts t = if is_disj t then dest_arg1 t :: disj_ts (dest_arg t) else [t] fun swap_disj ct = Conv.every_conv [rewr_obj_eq (obj_sym UtilBase.disj_assoc_th), Conv.arg1_conv (rewr_obj_eq UtilBase.disj_commute_th), rewr_obj_eq UtilBase.disj_assoc_th] ct fun disj_swap_eq_to_front' ct = let val t = Thm.term_of ct val thy = Thm.theory_of_cterm ct in if is_disj t then if is_neg_def_eq thy (dest_arg1 t) then Conv.all_conv ct else if is_disj (dest_arg t) then Conv.every_conv [Conv.arg_conv disj_swap_eq_to_front', swap_disj] ct else if is_neg_def_eq thy (dest_arg t) then rewr_obj_eq UtilBase.disj_commute_th ct else Conv.no_conv ct else Conv.no_conv ct end fun disj_swap_eq_to_front ct = Conv.every_conv [ Trueprop_conv disj_swap_eq_to_front', Trueprop_conv (rewr_obj_eq (obj_sym UtilBase.imp_conv_disj_th)), Conv.rewr_conv (meta_sym UtilBase.atomize_imp_th) ] ct fun meta_use_vardefs th = let val thy = Thm.theory_of_thm th in if exists (is_def_eq' thy) (Thm.prems_of th) then let val (pairs, th') = th |> apply_to_thm swap_eq_to_front |> meta_use_vardef val (pairs', th'') = meta_use_vardefs th' in (pairs @ pairs', th'') end else if is_Trueprop (Thm.prop_of th) then let val ts = disj_ts (prop_of' th) in if length ts > 1 andalso exists (is_neg_def_eq thy) ts then let val (pairs, th') = th |> apply_to_thm disj_swap_eq_to_front |> meta_use_vardef val (pairs', th'') = meta_use_vardefs th' in (pairs @ pairs', th'') end else ([], th) end else ([], th) end fun def_subst pairs t = fold (fn p => Term.subst_atomic [p]) pairs t end (* structure Normalizer. *) diff --git a/thys/Auto2_HOL/proofsteps.ML b/thys/Auto2_HOL/proofsteps.ML --- a/thys/Auto2_HOL/proofsteps.ML +++ b/thys/Auto2_HOL/proofsteps.ML @@ -1,968 +1,967 @@ (* File: proofsteps.ML Author: Bohua Zhan Definition of type proofstep, and facility for adding basic proof steps. *) datatype proofstep_fn = OneStep of Proof.context -> box_item -> raw_update list | TwoStep of Proof.context -> box_item -> box_item -> raw_update list type proofstep = { name: string, args: match_arg list, func: proofstep_fn } datatype prfstep_descriptor = WithFact of term | WithItem of string * term | WithProperty of term | WithWellForm of term * term | WithScore of int | GetFact of term * thm | ShadowFirst | ShadowSecond | CreateCase of term | CreateConcl of term | Filter of prfstep_filter signature PROOFSTEP = sig val eq_prfstep: proofstep * proofstep -> bool val apply_prfstep: Proof.context -> box_item list -> proofstep -> raw_update list val WithGoal: term -> prfstep_descriptor val WithTerm: term -> prfstep_descriptor val WithProp: term -> prfstep_descriptor val string_of_desc: theory -> prfstep_descriptor -> string val string_of_descs: theory -> prfstep_descriptor list -> string (* prfstep_filter *) val all_insts: prfstep_filter val neq_filter: term -> prfstep_filter val order_filter: string -> string -> prfstep_filter val size1_filter: string -> prfstep_filter val not_type_filter: string -> typ -> prfstep_filter (* First level proofstep writing functions. *) val apply_pat_r: Proof.context -> id_inst_ths -> term * thm -> thm val retrieve_args: prfstep_descriptor list -> match_arg list val retrieve_pats_r: prfstep_descriptor list -> (term * thm) list val retrieve_filts: prfstep_descriptor list -> prfstep_filter val retrieve_cases: prfstep_descriptor list -> term list val retrieve_shadows: prfstep_descriptor list -> int list val get_side_ths: Proof.context -> id_inst -> match_arg list -> (box_id * thm list) list val prfstep_custom: string -> prfstep_descriptor list -> (id_inst_ths -> box_item list -> Proof.context -> raw_update list) -> proofstep val gen_prfstep: string -> prfstep_descriptor list -> proofstep val prfstep_pre_conv: string -> prfstep_descriptor list -> (Proof.context -> conv) -> proofstep val prfstep_conv: string -> prfstep_descriptor list -> conv -> proofstep end; structure ProofStep : PROOFSTEP = struct fun eq_prfstep (prfstep1, prfstep2) = (#name prfstep1 = #name prfstep2) fun apply_prfstep ctxt items {func, ...} = case func of OneStep f => f ctxt (the_single items) | TwoStep f => f ctxt (hd items) (nth items 1) fun WithGoal t = let val _ = assert (type_of t = boolT) "WithGoal: pat should have type bool." in WithFact (get_neg t) end fun WithTerm t = WithItem (TY_TERM, t) fun WithProp t = let val _ = assert (type_of t = boolT) "WithProp: pat should have type bool." in WithItem (TY_PROP, t) end fun string_of_desc thy desc = let val print = Syntax.string_of_term_global thy in case desc of WithFact t => if is_neg t then "WithGoal " ^ (print (get_neg t)) else "WithFact " ^ (print t) | WithItem (ty_str, t) => if ty_str = TY_TERM then "WithTerm " ^ (print t) else "WithItem " ^ ty_str ^ " " ^ (print t) | WithProperty t => "WithProperty " ^ (print t) | WithWellForm (_, req) => "WithWellForm " ^ (print req) | WithScore n => "WithScore " ^ (string_of_int n) | GetFact (t, th) => if t aconv @{term False} then "GetResolve " ^ (Util.name_of_thm th) else if is_neg t then "GetGoal (" ^ (print (get_neg t)) ^ ", " ^ (Util.name_of_thm th) ^ ")" else "GetFact (" ^ (print t) ^ ", " ^ (Util.name_of_thm th) ^ ")" | ShadowFirst => "Shadow first" | ShadowSecond => "Shadow second" | CreateCase assum => "CreateCase " ^ (print assum) | CreateConcl concl => "CreateConcl " ^ (print concl) | Filter _ => "Filter (...)" end fun string_of_descs thy descs = let fun is_filter desc = case desc of Filter _ => true | _ => false val (filts, non_filts) = filter_split is_filter descs in (cat_lines (map (string_of_desc thy) non_filts)) ^ (if length filts > 0 then (" + " ^ (string_of_int (length filts)) ^ " filters") else "") end (* prfstep_filter *) val all_insts = fn _ => fn _ => true fun neq_filter cond ctxt (id, inst) = let val (lhs, rhs) = cond |> dest_not |> dest_eq handle Fail "dest_not" => raise Fail "neq_filter: not an inequality." | Fail "dest_eq" => raise Fail "neq_filter: not an inequality." val _ = assert (null (Term.add_frees cond [])) "neq_filter: should not contain free variable." val t1 = Util.subst_term_norm inst lhs val t2 = Util.subst_term_norm inst rhs in if Util.has_vars t1 andalso Util.has_vars t2 then true else if Util.has_vars t1 then (Matcher.rewrite_match ctxt (t1, Thm.cterm_of ctxt t2) (id, fo_init)) |> filter (fn ((id', _), _) => id = id') |> null else if Util.has_vars t2 then (Matcher.rewrite_match ctxt (t2, Thm.cterm_of ctxt t1) (id, fo_init)) |> filter (fn ((id', _), _) => id = id') |> null else not (RewriteTable.is_equiv_t id ctxt (t1, t2)) end fun order_filter s1 s2 _ (_, inst) = not (Term_Ord.term_ord (lookup_inst inst s2, lookup_inst inst s1) = LESS) fun size1_filter s1 ctxt (id, inst) = size_of_term (RewriteTable.simp_val_t id ctxt (lookup_inst inst s1)) = 1 fun not_type_filter s ty _ (_, inst) = not (Term.fastype_of (lookup_inst inst s) = ty) (* First level proofstep writing functions. *) fun apply_pat_r ctxt ((_, inst), ths) (pat_r, th) = let val _ = assert (fastype_of pat_r = boolT) "apply_pat_r: pat_r should be of type bool" (* Split into meta equalities (usually produced by term matching, not applied to th, and others (assumptions for th). *) val (eqs, ths') = ths |> filter_split (Util.is_meta_eq o Thm.prop_of) val _ = assert (length ths' = Thm.nprems_of th) "apply_pat_r: wrong number of assumptions." val inst_new = Util.subst_term_norm inst (mk_Trueprop pat_r) val th' = th |> Util.subst_thm ctxt inst |> fold Thm.elim_implies ths' val _ = if inst_new aconv (Thm.prop_of th') then () else raise Fail "apply_pat_r: conclusion mismatch" (* Rewrite on subterms, top sweep order. *) fun rewr_top eq_th = Conv.top_sweep_rewrs_conv [eq_th] ctxt in th' |> apply_to_thm (Conv.every_conv (map rewr_top eqs)) end fun retrieve_args descs = maps (fn desc => case desc of WithFact t => [PropMatch t] | WithItem (ty_str, t) => [TypedMatch (ty_str, t)] | WithProperty t => [PropertyMatch t] | WithWellForm t => [WellFormMatch t] | _ => []) descs fun retrieve_pats_r descs = maps (fn desc => case desc of GetFact (pat_r, th) => [(pat_r, th)] | _ => []) descs fun retrieve_filts descs = let val filts = maps (fn Filter filt => [filt] | _ => []) descs in fn ctxt => fn inst => forall (fn f => f ctxt inst) filts end fun retrieve_cases descs = let fun retrieve_case desc = case desc of CreateCase assum => [mk_Trueprop assum] | CreateConcl concl => [mk_Trueprop (get_neg concl)] | _ => [] in maps retrieve_case descs end fun retrieve_shadows descs = let fun retrieve_shadow desc = case desc of ShadowFirst => [0] | ShadowSecond => [1] | _ => [] in maps retrieve_shadow descs end fun retrieve_score descs = let fun retrieve_score desc = case desc of WithScore n => SOME n | _ => NONE in get_first retrieve_score descs end (* Given list of PropertyMatch and WellFormMatch arguments, attempt to find the corresponding theorems in the rewrite table. Return the list of theorems for each possible (mutually non-comparable) box IDs. *) fun get_side_ths ctxt (id, inst) side_args = if null side_args then [(id, [])] else let val side_args' = map (ItemIO.subst_arg inst) side_args fun process_side_arg side_arg = case side_arg of PropertyMatch prop => PropertyData.get_property_t ctxt (id, prop) | WellFormMatch (t, req) => (WellformData.get_wellform_t ctxt (id, t)) |> filter (fn (_, th) => prop_of' th aconv req) | _ => raise Fail "get_side_ths: wrong kind of arg." val side_ths = map process_side_arg side_args' in if exists null side_ths then [] else side_ths |> BoxID.get_all_merges_info ctxt |> Util.max_partial (BoxID.id_is_eq_ancestor ctxt) end (* Creates a proofstep with specified patterns and filters (in descs), and a custom function converting any instantiations into updates. *) fun prfstep_custom name descs updt_fn = let val args = retrieve_args descs val (item_args, side_args) = filter_split ItemIO.is_ordinary_match args val filt = retrieve_filts descs val shadows = retrieve_shadows descs (* Processing an instantiation after matching the one or two main matchers: apply filters, remove trivial True from matchings, find properties, and replace incremental ids. *) fun process_inst ctxt ((id, inst), ths) = (get_side_ths ctxt (id, inst) side_args) |> filter (BoxID.has_incr_id o fst) |> map (fn (id', p_ths) => ((id', inst), p_ths @ ths)) |> filter (filt ctxt o fst) fun shadow_to_update items ((id, _), _) n = ShadowItem {id = id, item = nth items n} in if length item_args = 1 then let val arg = the_single item_args fun prfstep ctxt item = let val inst_ths = (ItemIO.match_arg ctxt arg item ([], fo_init)) |> map (fn (inst, th) => (inst, [th])) |> maps (process_inst ctxt) fun process_inst inst_th = updt_fn inst_th [item] ctxt @ map (shadow_to_update [item] inst_th) shadows in maps process_inst inst_ths end in {name = name, args = args, func = OneStep prfstep} end else if length item_args = 2 then let val (arg1, arg2) = the_pair item_args fun prfstep1 ctxt item1 = let val inst_ths = ItemIO.match_arg ctxt arg1 item1 ([], fo_init) fun process_inst1 item2 ((id, inst), th) = let val arg2' = ItemIO.subst_arg inst arg2 val inst_ths' = (ItemIO.match_arg ctxt arg2' item2 (id, inst)) |> map (fn (inst', th') => (inst', [th, th'])) |> maps (process_inst ctxt) fun process_inst inst_th' = updt_fn inst_th' [item1, item2] ctxt @ map (shadow_to_update [item1, item2] inst_th') shadows in maps process_inst inst_ths' end in fn item2 => maps (process_inst1 item2) inst_ths end in {name = name, args = args, func = TwoStep prfstep1} end else raise Fail "prfstep_custom: must have 1 or 2 patterns." end (* Create a proofstep from a list of proofstep descriptors. See datatype prfstep_descriptor for allowed types of descriptors. *) fun gen_prfstep name descs = let val args = retrieve_args descs val pats_r = retrieve_pats_r descs val cases = retrieve_cases descs val sc = retrieve_score descs val input_descs = filter (fn desc => case desc of GetFact _ => false | CreateCase _ => false | CreateConcl _ => false | _ => true) descs (* Verify that all schematic variables appearing in pats_r / cases appear in pats. *) val pats = map ItemIO.pat_of_match_arg args val vars = map Var (fold Term.add_vars pats []) fun check_pat_r (pat_r, _) = subset (op aconv) (map Var (Term.add_vars pat_r []), vars) fun check_case assum = subset (op aconv) (map Var (Term.add_vars assum []), vars) val _ = assert (forall check_pat_r pats_r andalso forall check_case cases) "gen_prfstep: new schematic variable in pats_r / cases." fun pats_r_to_update ctxt (inst_ths as ((id, _), _)) = if null pats_r then [] else let val ths = map (apply_pat_r ctxt inst_ths) pats_r in if length ths = 1 andalso Thm.prop_of (the_single ths) aconv pFalse then [ResolveBox {id = id, th = the_single ths}] else [AddItems {id = id, sc = sc, raw_items = map Update.thm_to_ritem ths}] end fun case_to_update ((id, inst), _) assum = AddBoxes {id = id, sc = sc, init_assum = Util.subst_term_norm inst assum} fun cases_to_update inst_ths = map (case_to_update inst_ths) cases fun updt_fn inst_th _ ctxt = pats_r_to_update ctxt inst_th @ cases_to_update inst_th in prfstep_custom name input_descs updt_fn end fun prfstep_pre_conv name descs pre_cv = let val args = retrieve_args descs val _ = case args of [TypedMatch ("TERM", _)] => () | _ => raise Fail ("prfstep_conv: should have exactly one " ^ "term pattern.") val filt = retrieve_filts descs fun prfstep ctxt item = let val inst_ths = (ItemIO.match_arg ctxt (the_single args) item ([], fo_init)) |> filter (BoxID.has_incr_id o fst o fst) |> filter (filt ctxt o fst) fun inst_to_updt ((id, _), eq1) = (* Here eq1 is meta_eq from pat(inst) to item. *) let val ct = Thm.lhs_of eq1 val err = name ^ ": cv failed." val eq_th = pre_cv ctxt ct handle CTERM _ => raise Fail err in if Thm.is_reflexive eq_th then [] else if RewriteTable.is_equiv id ctxt (Thm.rhs_of eq1, Thm.rhs_of eq_th) then [] else let val th = to_obj_eq (Util.transitive_list [meta_sym eq1, eq_th]) in [Update.thm_update (id, th)] end end in maps inst_to_updt inst_ths end in {name = name, args = args, func = OneStep prfstep} end fun prfstep_conv name descs cv = prfstep_pre_conv name descs (K cv) end (* structure ProofStep *) val WithTerm = ProofStep.WithTerm val WithGoal = ProofStep.WithGoal val WithProp = ProofStep.WithProp val neq_filter = ProofStep.neq_filter val order_filter = ProofStep.order_filter val size1_filter = ProofStep.size1_filter val not_type_filter = ProofStep.not_type_filter signature PROOFSTEP_DATA = sig val add_prfstep: proofstep -> theory -> theory val del_prfstep_pred: (string -> bool) -> theory -> theory val del_prfstep: string -> theory -> theory val del_prfstep_thm: thm -> theory -> theory val del_prfstep_thm_str: string -> thm -> theory -> theory val del_prfstep_thm_eqforward: thm -> theory -> theory val get_prfsteps: theory -> proofstep list val add_prfstep_custom: (string * prfstep_descriptor list * (id_inst_ths -> box_item list -> Proof.context -> raw_update list)) -> theory -> theory val add_gen_prfstep: string * prfstep_descriptor list -> theory -> theory val add_prfstep_pre_conv: string * prfstep_descriptor list * (Proof.context -> conv) -> theory -> theory val add_prfstep_conv: string * prfstep_descriptor list * conv -> theory -> theory (* Constructing conditional prfstep_descriptors. *) type pre_prfstep_descriptor = Proof.context -> prfstep_descriptor val with_term: string -> pre_prfstep_descriptor val with_cond: string -> pre_prfstep_descriptor val with_conds: string list -> pre_prfstep_descriptor list val with_filt: prfstep_filter -> pre_prfstep_descriptor val with_filts: prfstep_filter list -> pre_prfstep_descriptor list val with_score: int -> pre_prfstep_descriptor (* Second level proofstep writing functions. *) datatype prfstep_mode = MODE_FORWARD | MODE_FORWARD' | MODE_BACKWARD | MODE_BACKWARD1 | MODE_BACKWARD2 | MODE_RESOLVE val add_prfstep_check_req: string * string -> theory -> theory val add_forward_prfstep_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_forward'_prfstep_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_backward_prfstep_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_backward1_prfstep_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_backward2_prfstep_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_resolve_prfstep_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_forward_prfstep: thm -> theory -> theory val add_forward'_prfstep: thm -> theory -> theory val add_backward_prfstep: thm -> theory -> theory val add_backward1_prfstep: thm -> theory -> theory val add_backward2_prfstep: thm -> theory -> theory val add_resolve_prfstep: thm -> theory -> theory val add_rewrite_rule_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_rewrite_rule_back_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_rewrite_rule_bidir_cond: thm -> pre_prfstep_descriptor list -> theory -> theory val add_rewrite_rule: thm -> theory -> theory val add_rewrite_rule_back: thm -> theory -> theory val add_rewrite_rule_bidir: thm -> theory -> theory val setup_attrib: (thm -> theory -> theory) -> attribute context_parser end; structure ProofStepData : PROOFSTEP_DATA = struct structure Data = Theory_Data ( type T = proofstep list; val empty = []; - val extend = I; fun merge (ps1, ps2) = Library.merge ProofStep.eq_prfstep (ps1, ps2) ) (* Add the given proof step. *) fun add_prfstep (prfstep as {args, ...}) = Data.map (fn prfsteps => if Util.is_prefix_str "$" (#name prfstep) then error "Add prfstep: names beginning with $ is reserved." else let val num_args = length (filter_out ItemIO.is_side_match args) in if num_args >= 1 andalso num_args <= 2 then prfsteps @ [prfstep] else error "add_proofstep: need 1 or 2 patterns." end) (* Deleting a proofstep. For string inputs, try adding theory name. For theorem inputs, try all @-suffixes. *) fun del_prfstep_pred pred = Data.map (fn prfsteps => let val names = map #name prfsteps val to_delete = filter pred names fun eq_name (key, {name, ...}) = (key = name) in if null to_delete then error "Delete prfstep: not found" else let val _ = writeln (cat_lines (map (fn name => "Delete " ^ name) to_delete)) in subtract eq_name to_delete prfsteps end end) fun del_prfstep prfstep_name thy = del_prfstep_pred (equal prfstep_name) thy (* Delete all proofsteps for a given theorem. *) fun del_prfstep_thm th = let val th_name = Util.name_of_thm th in del_prfstep_pred (equal th_name orf Util.is_prefix_str (th_name ^ "@")) end (* Delete proofsteps for a given theorem, with the given postfix. *) fun del_prfstep_thm_str str th = del_prfstep_pred (equal (Util.name_of_thm th ^ str)) val del_prfstep_thm_eqforward = del_prfstep_thm_str "@eqforward" fun get_prfsteps thy = Data.get thy fun add_prfstep_custom (name, descs, updt_fn) = add_prfstep (ProofStep.prfstep_custom name descs updt_fn) fun add_gen_prfstep (name, descs) = add_prfstep (ProofStep.gen_prfstep name descs) fun add_prfstep_pre_conv (name, descs, pre_cv) = add_prfstep (ProofStep.prfstep_pre_conv name descs pre_cv) fun add_prfstep_conv (name, descs, cv) = add_prfstep (ProofStep.prfstep_conv name descs cv) (* Constructing conditional prfstep_descriptors. *) type pre_prfstep_descriptor = Proof.context -> prfstep_descriptor fun with_term str ctxt = let val t = Proof_Context.read_term_pattern ctxt str val _ = assert (null (Term.add_frees t [])) "with_term: should not contain free variable." in WithTerm t end fun with_cond str ctxt = Filter (neq_filter (Proof_Context.read_term_pattern ctxt str)) fun with_conds strs = map with_cond strs fun with_filt filt = K (Filter filt) fun with_filts filts = map with_filt filts fun with_score n = K (WithScore n) (* Second level proofstep writing functions. *) fun add_and_print_prfstep prfstep_name descs thy = let val _ = writeln (prfstep_name ^ "\n" ^ (ProofStep.string_of_descs thy descs)) in add_gen_prfstep (prfstep_name, descs) thy end (* Add a proofstep checking a requirement. *) fun add_prfstep_check_req (t_str, req_str) thy = let val ctxt = Proof_Context.init_global thy val t = Proof_Context.read_term_pattern ctxt t_str val vars = map Free (Term.add_frees t []) val c = Util.get_head_name t val ctxt' = fold Util.declare_free_term vars ctxt val req = Proof_Context.read_term_pattern ctxt' req_str fun get_subst var = case var of Free (x, T) => (var, Var ((x, 0), T)) | _ => raise Fail "add_prfstep_check_req" val subst = map get_subst vars val t' = Term.subst_atomic subst t val req' = Term.subst_atomic subst req in add_and_print_prfstep (c ^ "_case") [WithTerm t', CreateConcl req'] thy end datatype prfstep_mode = MODE_FORWARD | MODE_FORWARD' | MODE_BACKWARD | MODE_BACKWARD1 | MODE_BACKWARD2 | MODE_RESOLVE (* Maximum number of term matches for the given mode. *) fun max_term_matches mode = case mode of MODE_FORWARD => 2 | MODE_FORWARD' => 1 | MODE_BACKWARD => 1 | MODE_RESOLVE => 1 | _ => 0 (* Obtain the first several premises of th that are either properties or wellformed-ness data. ts is the list of term matches. *) fun get_side_prems thy mode ts th = let val (prems, concl) = UtilLogic.strip_horn' th val _ = assert (length ts <= max_term_matches mode) "get_side_prems: too many term matches." (* Helper function. Consider the case where the first n premises are side conditions. Find the additional terms to match against for each mode. *) fun additional_matches n = let val prems' = drop n prems in case mode of MODE_FORWARD => take (2 - length ts) prems' | MODE_FORWARD' => if null ts andalso length prems' >= 2 then [hd prems', List.last prems'] else [List.last prems'] | MODE_BACKWARD => [get_neg concl] | MODE_BACKWARD1 => [get_neg concl, List.last prems'] | MODE_BACKWARD2 => [get_neg concl, hd prems'] | MODE_RESOLVE => if null ts andalso length prems' > 0 then [get_neg concl, List.last prems'] else [get_neg concl] end (* Determine whether t is a valid side premises, relative to the matches ts'. If yes, return the corresponding side matching. Otherwise return NONE. *) fun to_side_prems ts' t = case WellForm.is_subterm_wellform_data thy t ts' of SOME (t, req) => SOME (WithWellForm (t, req)) | NONE => if Property.is_property_prem thy t then SOME (WithProperty t) else NONE (* Attempt to convert the first n premises to side matchings. *) fun to_side_prems_n n = let val ts' = additional_matches n @ ts val side_prems' = prems |> take n |> map (to_side_prems ts') in if forall is_some side_prems' then SOME (map the side_prems') else NONE end (* Minimum number of premises for the given mode. *) val min_prems = case mode of MODE_FORWARD => 1 - length ts | MODE_FORWARD' => 1 | MODE_BACKWARD => 1 | MODE_BACKWARD1 => 2 | MODE_BACKWARD2 => 2 | MODE_RESOLVE => 0 val _ = assert (length prems >= min_prems) "get_side_prems: too few premises." val to_test = rev (0 upto (length prems - min_prems)) in (* Always succeeds at 0. *) the (get_first to_side_prems_n to_test) end (* Convert theorems of the form A1 ==> ... ==> An ==> C to A1 & ... & An ==> C. If keep_last = true, the last assumption is kept in implication form. *) fun atomize_conj_cv keep_last ct = if length (Logic.strip_imp_prems (Thm.term_of ct)) <= (if keep_last then 2 else 1) then Conv.all_conv ct else Conv.every_conv [Conv.arg_conv (atomize_conj_cv keep_last), Conv.rewr_conv UtilBase.atomize_conjL_th] ct (* Swap the last premise to become the first. *) fun swap_prem_to_front ct = let val n = length (Logic.strip_imp_prems (Thm.term_of ct)) in if n < 2 then Conv.all_conv ct else if n = 2 then Conv.rewr_conv Drule.swap_prems_eq ct else ((Conv.arg_conv swap_prem_to_front) then_conv (Conv.rewr_conv Drule.swap_prems_eq)) ct end (* Using cv, rewrite all assumptions and conclusion in ct. *) fun horn_conv cv ct = (case Thm.term_of ct of @{const Pure.imp} $ _ $ _ => (Conv.arg1_conv (Trueprop_conv cv)) then_conv (Conv.arg_conv (horn_conv cv)) | _ => Trueprop_conv cv) ct (* Try to cancel terms of the form ~~A. *) val try_nn_cancel_cv = Conv.try_conv (rewr_obj_eq UtilBase.nn_cancel_th) (* Post-processing of the given theorem according to mode. *) fun post_process_th ctxt mode side_count ts th = case mode of MODE_FORWARD => let val to_skip = side_count + (2 - length ts) in th |> apply_to_thm (Util.skip_n_conv to_skip (UtilLogic.to_obj_conv ctxt)) |> Util.update_name_of_thm th "" end | MODE_FORWARD' => let val cv = swap_prem_to_front then_conv (Util.skip_n_conv (2 - length ts) (UtilLogic.to_obj_conv ctxt)) in th |> apply_to_thm (Util.skip_n_conv side_count cv) |> Util.update_name_of_thm th "" end | MODE_BACKWARD => let val cv = (atomize_conj_cv false) then_conv (Conv.rewr_conv UtilBase.backward_conv_th) then_conv (horn_conv try_nn_cancel_cv) in th |> apply_to_thm (Util.skip_n_conv side_count cv) |> Util.update_name_of_thm th "@back" end | MODE_BACKWARD1 => let val cv = (atomize_conj_cv true) then_conv (Conv.rewr_conv UtilBase.backward1_conv_th) then_conv (horn_conv try_nn_cancel_cv) in th |> apply_to_thm (Util.skip_n_conv side_count cv) |> Util.update_name_of_thm th "@back1" end | MODE_BACKWARD2 => let val cv = (Conv.arg_conv (atomize_conj_cv false)) then_conv (Conv.rewr_conv UtilBase.backward2_conv_th) then_conv (horn_conv try_nn_cancel_cv) in th |> apply_to_thm (Util.skip_n_conv side_count cv) |> Util.update_name_of_thm th "@back2" end | MODE_RESOLVE => let val rewr_th = case Thm.nprems_of th - side_count of 0 => if is_neg (concl_of' th) then UtilBase.to_contra_form_th' else UtilBase.to_contra_form_th | 1 => UtilBase.resolve_conv_th | _ => raise Fail "resolve: too many hypothesis in th." val cv = (Conv.rewr_conv rewr_th) then_conv (horn_conv try_nn_cancel_cv) in th |> apply_to_thm (Util.skip_n_conv side_count cv) |> Util.update_name_of_thm th "@res" end (* Add basic proofstep for the given theorem and mode. *) fun add_basic_prfstep_cond th mode conds thy = let val ctxt = Proof_Context.init_global thy val ctxt' = ctxt |> Variable.declare_term (Thm.prop_of th) (* Replace variable definitions, obtaining list of replacements and the new theorem. *) val (pairs, th) = th |> apply_to_thm (UtilLogic.to_obj_conv_on_horn ctxt') |> Normalizer.meta_use_vardefs |> apsnd (Util.update_name_of_thm th "") (* List of definitions used. *) fun print_def_subst (lhs, rhs) = writeln ("Apply def " ^ (Syntax.string_of_term ctxt' lhs) ^ " = " ^ (Syntax.string_of_term ctxt' rhs)) val _ = map print_def_subst pairs fun def_subst_fun cond = case cond of WithItem ("TERM", t) => WithItem ("TERM", Normalizer.def_subst pairs t) | _ => cond in if null conds andalso (mode = MODE_FORWARD orelse mode = MODE_FORWARD') andalso Property.can_add_property_update th thy then Property.add_property_update th thy else let fun is_term_cond cond = case cond of WithItem ("TERM", _) => true | _ => false fun extract_term_cond cond = case cond of WithItem ("TERM", t) => t | _ => raise Fail "extract_term_cond" (* Instantiate each element of conds with ctxt', then separate into term and other (filter and shadow) conds. *) val (term_conds, filt_conds) = conds |> map (fn cond => cond ctxt') |> filter_split is_term_cond |> apfst (map def_subst_fun) (* Get list of assumptions to be obtained from either the property table or the wellform table. *) val ts = map extract_term_cond term_conds val side_prems = get_side_prems thy mode ts th val side_count = length side_prems val th' = th |> post_process_th ctxt' mode side_count ts val (assums, concl) = th' |> UtilLogic.strip_horn' |> apfst (drop side_count) val pats = map extract_term_cond term_conds @ assums val match_descs = term_conds @ map WithFact assums val _ = assert (Util.is_pattern_list pats) "add_basic_prfstep: invalid patterns." val _ = assert (length pats > 0 andalso length pats <= 2) "add_basic_prfstep: invalid number of patterns." in (* Switch two assumptions if necessary. *) if length pats = 2 andalso not (Util.is_pattern (hd pats)) then let val _ = writeln "Switching two patterns." val swap_prems_cv = Conv.rewr_conv Drule.swap_prems_eq val th'' = if length assums = 1 then th' else th' |> apply_to_thm (Util.skip_n_conv side_count swap_prems_cv) |> Util.update_name_of_thm th' "" val swap_match_descs = [nth match_descs 1, hd match_descs] val descs = side_prems @ swap_match_descs @ filt_conds @ [GetFact (concl, th'')] in add_and_print_prfstep (Util.name_of_thm th') descs thy end else let val descs = side_prems @ match_descs @ filt_conds @ [GetFact (concl, th')] in add_and_print_prfstep (Util.name_of_thm th') descs thy end end end fun add_forward_prfstep_cond th = add_basic_prfstep_cond th MODE_FORWARD fun add_forward'_prfstep_cond th = add_basic_prfstep_cond th MODE_FORWARD' fun add_backward_prfstep_cond th = add_basic_prfstep_cond th MODE_BACKWARD fun add_backward1_prfstep_cond th = add_basic_prfstep_cond th MODE_BACKWARD1 fun add_backward2_prfstep_cond th = add_basic_prfstep_cond th MODE_BACKWARD2 fun add_resolve_prfstep_cond th = add_basic_prfstep_cond th MODE_RESOLVE fun add_forward_prfstep th = add_forward_prfstep_cond th [] fun add_forward'_prfstep th = add_forward'_prfstep_cond th [] fun add_backward_prfstep th = add_backward_prfstep_cond th [] fun add_backward1_prfstep th = add_backward1_prfstep_cond th [] fun add_backward2_prfstep th = add_backward2_prfstep_cond th [] fun add_resolve_prfstep th = add_resolve_prfstep_cond th [] fun add_rewrite_eq_rule_cond th conds thy = let val th = if Util.is_meta_eq (Thm.concl_of th) then UtilLogic.to_obj_eq_th th else th val (lhs, _) = th |> concl_of' |> strip_conj |> hd |> dest_eq in thy |> add_forward_prfstep_cond th (K (WithTerm lhs) :: conds) end fun add_rewrite_iff_rule_cond th conds thy = let val th = if Util.is_meta_eq (Thm.concl_of th) then UtilLogic.to_obj_eq_iff_th th else th val (lhs, _) = th |> concl_of' |> dest_eq val _ = assert (fastype_of lhs = boolT) "add_rewrite_iff: argument not of type bool." val forward_th = th |> equiv_forward_th val nforward_th = th |> inv_backward_th |> apply_to_thm (horn_conv try_nn_cancel_cv) |> Util.update_name_of_thm th "@invbackward" in thy |> add_basic_prfstep_cond forward_th MODE_FORWARD' conds |> add_basic_prfstep_cond nforward_th MODE_FORWARD' conds end fun add_rewrite_rule_cond th conds thy = let val th = if Util.is_meta_eq (Thm.concl_of th) then to_obj_eq_th th else th val (lhs, _) = th |> concl_of' |> strip_conj |> hd |> dest_eq in if fastype_of lhs = boolT then add_rewrite_iff_rule_cond th conds thy else add_rewrite_eq_rule_cond th conds thy end fun add_rewrite_rule_back_cond th conds = add_rewrite_rule_cond (obj_sym_th th) conds fun add_rewrite_rule_bidir_cond th conds = (add_rewrite_rule_cond th conds) #> add_rewrite_rule_back_cond th conds fun add_rewrite_rule th = add_rewrite_rule_cond th [] fun add_rewrite_rule_back th = add_rewrite_rule_back_cond th [] fun add_rewrite_rule_bidir th = add_rewrite_rule th #> add_rewrite_rule_back th fun setup_attrib f = Attrib.add_del (Thm.declaration_attribute ( fn th => Context.mapping (f th) I)) (Thm.declaration_attribute ( fn _ => fn _ => raise Fail "del_step: not implemented.")) end (* structure ProofStepData. *) open ProofStepData diff --git a/thys/Auto2_HOL/property.ML b/thys/Auto2_HOL/property.ML --- a/thys/Auto2_HOL/property.ML +++ b/thys/Auto2_HOL/property.ML @@ -1,258 +1,255 @@ (* File: property.ML Author: Bohua Zhan Theory data for properties. This data consists of the following parts: - Two tables containing property update rules. - A table containing list of fields that can have properties. *) signature PROPERTY = sig val is_property: term -> bool val add_property_field_const: term -> theory -> theory val is_property_field: theory -> term -> bool val strip_property_field: theory -> term -> term list val is_property_prem: theory -> term -> bool val get_property_name: term -> string val get_property_names: term list -> string list val get_property_arg: term -> term val get_property_arg_th: thm -> cterm (* About the PropertyUpdateData table.*) val can_add_property_update: thm -> theory -> bool val add_property_update: thm -> theory -> theory val lookup_property_update: theory -> string -> thm list val lookup_property_update_fun: theory -> string -> thm list val instantiate_property_update: Proof.context -> term -> thm -> thm option end; structure Property : PROPERTY = struct (* Rules deriving new properties of t from other properties of t. They are indexed under the names of the properties in the premises. *) structure UpdateData = Theory_Data ( type T = (thm list) Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge_list Thm.eq_thm_prop ) (* Rules for deriving properties of f x_1 ... x_n from properties of x_1, ... x_n. They are indexed under the name of the head function f. *) structure UpdateFunData = Theory_Data ( type T = (thm list) Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge_list Thm.eq_thm_prop ) (* Set of fields of a structure whose property can be considered as properties of the structure itself. Relevant when checking is_property_prem. *) structure FieldData = Theory_Data ( type T = unit Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge (K true) ) (* Whether the term is a property predicate applied to a term. *) fun is_property t = let val _ = assert (fastype_of t = boolT) "is_property: wrong type" val (f, ts) = Term.strip_comb t in if length ts <> 1 orelse not (Term.is_Const f) then false else let val T = fastype_of (the_single ts) val (dT, _) = Term.strip_type T in length dT = 0 andalso T <> boolT end end (* Insert the following constant as a property field. *) fun add_property_field_const t thy = case Term.head_of t of Const (c, T) => let val (pTs, _) = Term.strip_type T val _ = if length pTs = 1 then () else error "Add property field: input should be a field." val _ = writeln ("Add field " ^ c ^ " as property field.") in thy |> FieldData.map (Symtab.update_new (c, ())) end | _ => error "Add property field: input should be a constant." (* Whether the term is zero or more property field constants applied to a Var term. *) fun is_property_field thy t = case t of Var _ => true | Const (c, _) $ t' => Symtab.defined (FieldData.get thy) c andalso is_property_field thy t' | _ => false (* Given a term t, return all possible ways to strip property field constants from t. For example, if t is of the form f1(f2(x)), where f1 and f2 are property constants, then the result is [f1(f2(x)), f2(x), x]. *) fun strip_property_field thy t = case t of Const (c, _) $ t' => if Symtab.defined (FieldData.get thy) c then t :: strip_property_field thy t' else [t] | _ => [t] (* Stricter condition than is_property: the argument must be a schematic variable (up to property fields). *) fun is_property_prem thy t = is_property t andalso is_property_field thy (dest_arg t) val get_property_name = Util.get_head_name fun get_property_names ts = ts |> map get_property_name |> distinct (op =) (* Return the argument of the property. *) fun get_property_arg t = dest_arg t handle Fail "dest_arg" => raise Fail "get_property_arg: t in wrong form." (* Return the argument of the property theorem as a cterm. *) fun get_property_arg_th th = Thm.dest_arg (cprop_of' th) handle CTERM _ => raise Fail "get_property_carg" | Fail "dest_Trueprop" => raise Fail "get_property_carg" (* Add the given rule as a property update. The requirements on th is as follows: - The conclusion must be a property constant, with argument in the form of either ?x or f ?x1 ... ?xn. - Each premise must be a property constant on ?x (in the first case) or one of ?x1 ... ?xn (in the second case). The argument of the property in the conclusion must contain all schematic variables of the theorem. *) fun can_add_property_update th thy = let val (prems, concl) = UtilLogic.strip_horn' th in if is_property concl andalso forall (is_property_prem thy) prems then let val concl_arg = get_property_arg concl val all_vars = map Var (Term.add_vars (Thm.prop_of th) []) in if is_Var concl_arg then (* First case: check that concl_arg is the only schematic Var. *) length all_vars = 1 else (* Second case: concl_arg is of the form f ?x1 ... ?xn. *) let val args = Util.dest_args concl_arg in forall is_Var args andalso subset (op aconv) (all_vars, args) end end else false end (* Add the given theorem as a property update rule. Choose which table to add the rule to. *) fun add_property_update th thy = let val (prems, concl) = UtilLogic.strip_horn' th val _ = assert (is_property concl) "add_property_update: concl must be a property constant." val _ = assert (forall (is_property_prem thy) prems) "add_property_update: prem must be a property premise." val concl_arg = get_property_arg concl val all_vars = map Var (Term.add_vars (Thm.prop_of th) []) in if is_Var concl_arg then (* First case. Each premise must also be about ?x. Add to UpdateData table under the names of the predicates. *) let val _ = assert (length all_vars = 1) "add_property_update: extraneous Vars in th." val names = get_property_names prems val _ = writeln ("Add property rule for " ^ (Util.string_of_list I names)) in thy |> UpdateData.map ( fold (Symtab.update_list Thm.eq_thm_prop) (map (rpair th) names)) end else (* Second case. concl_arg in the form f ?x1 ... ?xn. Add to UpdateFunData table under f. *) let val (f, args) = Term.strip_comb concl_arg val c = case f of Const (c, _) => c | _ => raise Fail "add_property_update: f is not constant." val _ = assert (forall is_Var args) "add_property_update: all args of concl must be Vars." val _ = assert (subset (op aconv) (all_vars, args)) "add_property_update: extraneous Vars in th." val _ = writeln ("Add property rule for function " ^ c) in thy |> UpdateFunData.map (Symtab.update_list Thm.eq_thm_prop (c, th)) end end (* Find update rules of the form P1 x ==> ... ==> Pn x ==> P x, where c is one of P1, ... Pn. *) fun lookup_property_update thy c = Symtab.lookup_list (UpdateData.get thy) c (* Find update rules of the form A1 ==> ... ==> An ==> P(f(x1,...,xn)), where each A_i is a property on one of x_j. Here c is the name of f. *) fun lookup_property_update_fun thy c = Symtab.lookup_list (UpdateFunData.get thy) c (* Instantiate th by matching t with the argument of the conclusion of th. Return NONE if instantiation is unsuccessful (because type does not match). *) fun instantiate_property_update ctxt t th = let val (_, concl) = UtilLogic.strip_horn' th val concl_arg = get_property_arg concl val thy = Proof_Context.theory_of ctxt in if Sign.typ_instance thy (fastype_of t, fastype_of concl_arg) then let val err_str = "instantiate_property_update: cannot match with t." val inst = Pattern.first_order_match thy (concl_arg, t) fo_init handle Pattern.MATCH => raise Fail err_str in SOME (Util.subst_thm ctxt inst th) end else NONE end end (* structure Property. *) val add_property_field_const = Property.add_property_field_const diff --git a/thys/Auto2_HOL/wellform.ML b/thys/Auto2_HOL/wellform.ML --- a/thys/Auto2_HOL/wellform.ML +++ b/thys/Auto2_HOL/wellform.ML @@ -1,138 +1,137 @@ (* File: wellform.ML Author: Bohua Zhan Wellformed-ness of terms. *) signature WELLFORM = sig val register_wellform_data: string * string list -> theory -> theory val lookup_wellform_data: theory -> term -> term list val is_subterm_wellform_data': theory -> term -> term -> (term * term) option val is_subterm_wellform_data: theory -> term -> term list -> (term * term) option val lookup_wellform_pattern: theory -> term * term -> (term * term) option end; structure WellForm : WELLFORM = struct (* Each entry in the table consists of a term of the form f ?a_1 ... ?a_n, where f is a constant, and each ?a_i is a pure schematic variable, paired with a list of requirements for the term to be valid. It is indexed under the string of the constant f. *) structure Data = Theory_Data ( type T = (term * term list) Symtab.table val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge (op =) ) (* Add a term with its requirements to the table. *) fun register_wellform_data (t_str, req_strs) thy = let val ctxt = Proof_Context.init_global thy val t = Proof_Context.read_term_pattern ctxt t_str val ctxt' = Variable.declare_term t ctxt val reqs = map (Proof_Context.read_term_pattern ctxt') req_strs val (f, args) = Term.strip_comb t val _ = assert (Term.is_Const f) "add_wellform_data: head must be Const." val _ = assert (forall Term.is_Free args) "add_wellform_data: arguments must be Free." val (c, _) = Term.dest_Const f in thy |> Data.map (Symtab.update_new (c, (t, reqs))) end (* Lookup table for the given term t. If nothing is found, return the empty list by default. *) fun lookup_wellform_data thy t = let val (f, args) = Term.strip_comb t val data = Data.get thy in case f of Const (c, _) => (case Symtab.lookup data c of NONE => [] | SOME (t', reqs) => let val (_, vars) = Term.strip_comb t' in if length vars <> length args then [] else let val tys = map fastype_of vars ~~ map fastype_of args val tyinst = fold (Sign.typ_match thy) tys Vartab.empty val vars' = map (Envir.subst_term_types tyinst) vars fun subst_fun req = req |> Envir.subst_term_types tyinst |> Term.subst_atomic (vars' ~~ args) in distinct (op aconv) (map subst_fun reqs) end handle Type.TYPE_MATCH => [] end) | _ => [] end (* Check whether req is part of the wellformed-ness data of a subterm of t. If so, return the pair SOME (t', req), where t' is a subterm of t and req is a wellformed-ness data of t'. Otherwise return NONE. *) fun is_subterm_wellform_data' thy req t = if member (op aconv) (lookup_wellform_data thy t) req then SOME (t, req) else let val (_, args) = Term.strip_comb t in get_first (is_subterm_wellform_data' thy req) args end fun is_subterm_wellform_data thy req ts = get_first (is_subterm_wellform_data' thy req) ts (* Given a term t and wellform data for t, return the relevant wellform pattern. *) fun lookup_wellform_pattern thy (t, wf_t) = let val (f, args) = Term.strip_comb t val data = Data.get thy in case f of Const (c, _) => (case Symtab.lookup data c of NONE => NONE | SOME (t', reqs) => let val (_, vars) = Term.strip_comb t' in if length vars <> length args then NONE else let val tys = map fastype_of vars ~~ map fastype_of args val tyinst = fold (Sign.typ_match thy) tys Vartab.empty val vars' = map (Envir.subst_term_types tyinst) vars fun subst_fun t = t |> Envir.subst_term_types tyinst |> Term.subst_atomic (vars' ~~ args) val reqs' = filter (fn req => wf_t aconv subst_fun req) reqs in case reqs' of [] => NONE | req' :: _ => SOME (apply2 (Envir.subst_term_types tyinst) (t', req')) end end) | _ => NONE end end (* structure WellForm. *) val register_wellform_data = WellForm.register_wellform_data diff --git a/thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML b/thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML --- a/thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML +++ b/thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML @@ -1,324 +1,323 @@ (* File: assn_matcher.ML Author: Bohua Zhan Matching of assertions. *) (* Given arguments ctxt (pat, t) (id, inst), match pat with t. Assume pat is not a product. Produce t ==> pat(s) or t ==> pat(s) * t' for those in AssnMatchData. Produce pat(s) or pat(s) * t' ==> t for those in AssnInvMatchData. *) type assn_matcher = Proof.context -> term * cterm -> id_inst -> id_inst_th list signature ASSN_MATCHER = sig val add_assn_matcher: assn_matcher -> theory -> theory val assn_match_term: Proof.context -> term * cterm -> id_inst -> id_inst_th list val assn_match_all: Proof.context -> term * cterm -> id_inst -> id_inst_th list val assn_match_strict: Proof.context -> term * cterm -> id_inst -> id_inst_th list val triv_assn_matcher: assn_matcher val emp_assn_matcher: assn_matcher val true_assn_matcher: assn_matcher val add_entail_matcher: thm -> theory -> theory val assn_match_single: Proof.context -> term * cterm -> id_inst -> id_inst_th list val add_assn_matcher_proofsteps: theory -> theory end (* Due to strange interaction between functors and Theory_Data, this must be put outside. *) structure MatchData = Theory_Data ( type T = assn_matcher list val empty = [] - val extend = I; - val merge = merge (op pointer_eq) + val merge = merge (op pointer_eq) (* FIXME !? *) ) functor AssnMatcher(SepUtil: SEP_UTIL): ASSN_MATCHER = struct open SepUtil (* Matching in the forward direction *) fun add_assn_matcher matcher = MatchData.map (cons matcher) (* Assume pat is not in the form A * B. Match pat with one or more terms of t. Return theorem of form t ==> pat(s) * t'. *) fun assn_match_term ctxt (pat, ct) (id, inst) = let val _ = assert (not (Term.is_Var pat)) "assn_match_term: pat should not be Var." val thy = Proof_Context.theory_of ctxt fun apply_matcher matcher = matcher ctxt (pat, ct) (id, inst) (* th must be an entailment, and the right side must be pat(s), pat(s) * t', or t' * pat(s). *) fun process_res ((id, inst'), th) = let val _ = assert (is_entail (prop_of' th)) "assn_match_term" val (_, rhs) = th |> prop_of' |> dest_entail val exp_rhs = Util.subst_term_norm inst' pat in if rhs aconv exp_rhs then ((id, inst'), th |> apply_to_entail_r mult_emp_right) else if UtilArith.is_times rhs andalso dest_arg1 rhs aconv exp_rhs then ((id, inst'), th) else if UtilArith.is_times rhs andalso dest_arg rhs aconv exp_rhs then ((id, inst'), th |> apply_to_entail_r (ACUtil.comm_cv assn_ac_info)) else raise Fail "assn_match_term" end in (maps apply_matcher (MatchData.get thy)) |> map process_res end (* Match each term of pat with some term in t. Returns t ==> pat(s) * t'. *) fun assn_match_all ctxt (pat, ct) (id, inst) = if UtilArith.is_times pat then let val (A, B) = Util.dest_binop_args pat val insts = assn_match_all ctxt (A, ct) (id, inst) (* th is t ==> A(s) * t'. Match B(s) with t', with result t' ==> B(s) * t''. Produce t ==> (A(s) * B(s)) * t'' *) fun process_inst ((id', inst'), th) = let val ct' = th |> cprop_of' |> cdest_entail |> snd |> Thm.dest_arg val B' = Util.subst_term_norm inst' B val insts' = assn_match_all ctxt (B', ct') (id', inst') (* th' is t' ==> B(s) * t''. *) fun process_inst' ((id'', inst''), th') = let val res = ([th, th'] MRS entails_trans2_th) |> apply_to_entail_r ( ACUtil.assoc_sym_cv assn_ac_info) in ((id'', inst''), res) end in map process_inst' insts' end in maps process_inst insts end else assn_match_term ctxt (pat, ct) (id, inst) (* Guarantees that every term in t is matched. Returns t ==> pat(s). *) fun assn_match_strict ctxt (pat, ct) (id, inst) = let val inst = assn_match_all ctxt (pat, ct) (id, inst) fun process_inst ((id', inst'), th) = let val rhs = th |> prop_of' |> dest_entail |> snd val _ = assert (UtilArith.is_times rhs andalso dest_arg1 rhs aconv Util.subst_term_norm inst' pat) "assn_match_strict" in if dest_arg rhs aconv emp then [((id', inst'), th |> apply_to_entail_r reduce_emp_right)] else [] end in maps process_inst inst end (* Specific assertion matchers *) (* Matcher using the theorem A ==> A. *) fun triv_assn_matcher ctxt (pat, ct) (id, inst) = if pat aconv emp then [] (* leave to emp_assn_matcher *) else let val cts = ACUtil.cdest_ac assn_ac_info ct fun match_i i = let val ct' = nth cts i val insts = Matcher.rewrite_match ctxt (pat, ct') (id, inst) (* eq_th is of form pat(inst') == t'. *) fun process_inst ((id', inst'), eq_th) = let val th = entail_triv_th ctxt (Thm.term_of ct) val cv = Conv.every_conv [ ACUtil.move_outmost assn_ac_info (Thm.term_of ct'), ACUtil.ac_last_conv assn_ac_info (Conv.rewr_conv (meta_sym eq_th))] in ((id', inst'), th |> apply_to_entail_r cv) end in map process_inst insts end in maps match_i (0 upto (length cts - 1)) end (* Consider the case where pat = emp. Return t ==> emp * t. *) fun emp_assn_matcher ctxt (pat, ct) (id, inst) = if not (pat aconv emp) then [] else [((id, inst), ct |> Thm.term_of |> entail_triv_th ctxt |> apply_to_entail_r mult_emp_left)] (* If pat = true, match all of t. Return t ==> emp * true. *) fun true_assn_matcher ctxt (pat, ct) (id, inst) = if not (pat aconv assn_true) then [] else [((id, inst), ct |> Thm.term_of |> entail_true_th ctxt |> apply_to_entail_r mult_emp_left)] (* We now consider the case of generating a matcher from an entailment theorem of a particular form. Given an entailment A ==> B, where B is of the form f ?xs pat_r, where f is a constant, and pat_r may contain additional schematic variables. Attempt to find a term of form f xs r within t, for the input term r, by matching the pattern A. For each match, return the implication t ==> f xs r or t ==> t' * f xs r. This function serves as the first step of entail_matcher. *) fun entail_matcher' entail_th ctxt r ct id = let (* Match pat_r with r. *) val pat_r = entail_th |> prop_of' |> dest_entail |> snd |> dest_arg val inst_r = Matcher.rewrite_match ctxt (pat_r, Thm.cterm_of ctxt r) (id, fo_init) (* For each match, recursively match the instantiated version of A (named pat here) with t. *) fun process_inst_r ((id', inst'), eq_th) = let val entail_th' = Util.subst_thm ctxt inst' entail_th val pat = entail_th' |> prop_of' |> dest_arg1 val matches = assn_match_all ctxt (pat, ct) (id', fo_init) (* th is of form t ==> pat(s) * t'. Convert to t ==> t' * pat(s). Then use entailment theorem to convert to t ==> t' * B. Finally, convert the argument in B to the given r. *) fun process_match ((id'', _), th) = let val cv = eq_th |> Conv.rewr_conv |> Util.argn_conv 1 |> ACUtil.ac_last_conv assn_ac_info val th' = th |> apply_to_entail_r (ACUtil.comm_cv assn_ac_info) in (id'', ([th', entail_th'] MRS entails_trans2_th) |> apply_to_entail_r cv) end in map process_match matches end in maps process_inst_r inst_r end (* Given entailment theorem A ==> B, with same condition as in entail_matcher', attempt to match pat with t, and return t ==> t' * pat(s). For any matching to be performed, pat must be in the form f pat_xs r, where pat_xs may contain schematic variables, but r cannot. First, find f xs r using entail_matcher', then match pat_xs with xs. *) fun entail_matcher entail_th ctxt (pat, ct) (id, inst) = let val (f, args) = Term.strip_comb pat val pat_f = entail_th |> prop_of' |> dest_entail |> snd |> Term.head_of in if not (Term.aconv_untyped (f, pat_f)) orelse Util.has_vars (nth args 1) then [] else let val (pat_xs, r) = the_pair args val matches = entail_matcher' entail_th ctxt r ct id fun process_res (id', th) = let val xs = th |> cprop_of' |> Thm.dest_arg |> ACUtil.cdest_ac assn_ac_info |> List.last |> Drule.strip_comb |> snd |> hd val insts = Matcher.rewrite_match ctxt (pat_xs, xs) (id', inst) fun process_inst ((id'', inst'), eq_th) = let val cv = eq_th |> meta_sym |> Conv.rewr_conv |> Conv.arg1_conv |> ACUtil.ac_last_conv assn_ac_info in ((id'', inst'), th |> apply_to_entail_r cv) end in map process_inst insts end in maps process_res matches end end fun add_entail_matcher th = let val (pat_f, pat_args) = th |> prop_of' |> dest_entail |> snd |> Term.strip_comb val _ = assert (length pat_args = 2 andalso Term.is_Const pat_f) "add_entail_matcher: th must be in form A ==> f ?xs pat_r." in add_assn_matcher (entail_matcher th) end (* Matching in the backward direction *) (* Given a pattern pat, write t in the form pat(inst) * t'. *) fun assn_match_single ctxt (pat, ct) (id, inst) = let val cts = ACUtil.cdest_ac assn_ac_info ct fun match_i i = let val ct' = nth cts i val t' = Thm.term_of ct' val insts = Matcher.rewrite_match ctxt (pat, ct') (id, inst) (* eq_th is of form pat(inst) == t'. *) fun process_inst ((id', inst'), eq_th) = let val eq_th' = if length cts = 1 then eq_th |> meta_sym |> apply_to_rhs mult_emp_right else Conv.every_conv [ ACUtil.move_outmost assn_ac_info t', Conv.arg_conv (Conv.rewr_conv (meta_sym eq_th)), ACUtil.comm_cv assn_ac_info] ct in ((id', inst'), eq_th') end in map process_inst insts end in maps match_i (0 upto (length cts - 1)) end val add_assn_matcher_proofsteps = fold add_assn_matcher [ triv_assn_matcher, emp_assn_matcher, true_assn_matcher ] end (* structure AssnMatcher. *) diff --git a/thys/Auto2_Imperative_HOL/Imperative/sep_steps.ML b/thys/Auto2_Imperative_HOL/Imperative/sep_steps.ML --- a/thys/Auto2_Imperative_HOL/Imperative/sep_steps.ML +++ b/thys/Auto2_Imperative_HOL/Imperative/sep_steps.ML @@ -1,825 +1,824 @@ (* File: sep_steps.ML Author: Bohua Zhan Proof steps for separation logic. *) signature SEP_LOGIC = sig val normalize_hoare_goal_cv: Proof.context -> conv val normalize_entail_goal_cv: Proof.context -> conv val get_proc_def: theory -> term -> thm list val update_hoare_triple: thm -> theory -> theory val get_hoare_triples: theory -> string -> thm list val is_bind_cmd: term -> bool val get_first_cmd: term -> term val TY_CODE_POS: string val TY_ENTAIL: string val is_neg_hoare_triple: term -> bool val is_neg_entail: term -> bool val norm_precond: Proof.context -> conv val norm_entail_conds: Proof.context -> conv val is_implies_item: box_item -> bool val hoare_goal_update: Proof.context -> box_id * thm -> raw_update val entail_goal_update: Proof.context -> box_id * thm -> raw_update val init_entail: proofstep val entails_resolve: proofstep val init_pos: proofstep val add_forward_ent_prfstep: thm -> theory -> theory val add_backward_ent_prfstep: thm -> theory -> theory val add_rewrite_ent_rule: thm -> theory -> theory val rewrite_pos: proofstep val extract_pure_hoare_cv: conv val match_hoare_th: box_id -> Proof.context -> thm -> thm -> box_item -> raw_update list val match_hoare_prop: proofstep val match_hoare_disj: proofstep val match_assn_pure: proofstep val hoare_create_case: proofstep val entail_pure: proofstep val entail_create_case: proofstep val hoare_triple: proofstep val contract_hoare_cv: Proof.context -> conv val add_hoare_triple_prfstep: thm -> theory -> theory val add_sep_logic_proofsteps: theory -> theory end; functor SepLogic(SepUtil: SEP_UTIL) : SEP_LOGIC = struct open SepUtil structure AssnMatcher = AssnMatcher(SepUtil) (* Normalize a Hoare triple goal. *) fun normalize_hoare_goal_cv' ctxt ct = let val t = Thm.term_of ct val (P, _, _) = t |> dest_not |> dest_hoare_triple in if is_pure_assn P then rewr_obj_eq pre_pure_rule_th' ct else if UtilArith.is_times P andalso is_pure_assn (dest_arg P) then Conv.every_conv [rewr_obj_eq pre_pure_rule_th, Conv.arg1_conv (normalize_hoare_goal_cv' ctxt)] ct else if is_ex_assn P then Conv.every_conv [ rewr_obj_eq pre_ex_rule_th, Conv.binder_conv (normalize_hoare_goal_cv' o snd) ctxt] ct else Conv.all_conv ct end fun normalize_hoare_goal_cv ctxt ct = if is_ex (Thm.term_of ct) then Conv.binder_conv (normalize_hoare_goal_cv o snd) ctxt ct else Conv.every_conv [ Conv.arg_conv (Util.argn_conv 0 (SepUtil.normalize_assn_cv ctxt)), normalize_hoare_goal_cv' ctxt] ct fun normalize_entail_goal_cv' ctxt ct = let val t = Thm.term_of ct val (P, _) = t |> dest_not |> dest_entail in if is_pure_assn P then rewr_obj_eq entails_pure_th' ct else if UtilArith.is_times P andalso is_pure_assn (dest_arg P) then Conv.every_conv [rewr_obj_eq entails_pure_th, Conv.arg1_conv (normalize_entail_goal_cv' ctxt)] ct else if is_ex_assn P then Conv.every_conv [ rewr_obj_eq entails_ex_th, Conv.binder_conv (normalize_entail_goal_cv' o snd) ctxt] ct else Conv.all_conv ct end fun normalize_entail_goal_cv ctxt ct = if is_ex (Thm.term_of ct) then Conv.binder_conv (normalize_entail_goal_cv o snd) ctxt ct else Conv.every_conv [ Conv.arg_conv (Conv.binop_conv (SepUtil.normalize_assn_cv ctxt)), normalize_entail_goal_cv' ctxt] ct (* Data maintained for each imperative command. *) structure Data = Theory_Data ( type T = thm Symtab.table; val empty = Symtab.empty; - val extend = I; val merge = Symtab.merge (op Thm.eq_thm_prop) ) (* Add the given theorem as a Hoare triple. Replace previous Hoare triples for this theorem if any exist. *) fun update_hoare_triple hoare_th thy = let val (_, c, _) = dest_hoare_triple (prop_of' hoare_th) val nm = Util.get_head_name c in thy |> Data.map (Symtab.update (nm, hoare_th)) end (* Obtain list of Hoare triples for the given command *) fun get_hoare_triples thy nm = the_list (Symtab.lookup (Data.get thy) nm) fun get_proc_def thy t = if is_bind_cmd t then [] else let val nm = Util.get_head_name t in if null (get_hoare_triples thy nm) then Unfolding.get_unfold_thms_by_name thy nm else [] end fun get_first_cmd c = if is_bind_cmd c then dest_arg1 c else c fun extract_return_var t = if is_bind_cmd t then case dest_arg t of Abs (x, T, _) => if x = "uu_" then Free ("u",T) (* no assigned name *) else Free (x,T) (* regular assigned name *) | c => Free ("r", Term.domain_type (fastype_of c)) else raise Fail "extract_return_var" (* CODE_POS item stores a Hoare triple goal, indicating the current position in the program. *) val TY_CODE_POS = "CODE_POS" (* ENTAIL item stores an entailment goal, usually indicating the end of the program. *) val TY_ENTAIL = "ENTAIL" fun is_neg_hoare_triple t = is_neg t andalso is_hoare_triple (dest_not t) fun is_neg_entail t = is_neg t andalso is_entail (dest_not t) fun norm_precond ctxt ct = Util.argn_conv 0 (SepUtil.normalize_assn_cv ctxt) ct fun norm_entail_conds ctxt ct = Conv.binop_conv (SepUtil.normalize_assn_cv ctxt) ct fun is_implies_item item = Util.is_implies (Thm.prop_of (#prop item)) fun normalize_let ctxt th = let val rewr_one = Conv.first_conv [Conv.rewr_conv @{thm Let_def}, rewr_obj_eq @{thm case_prod_beta'}] val cv = Conv.every_conv [ Conv.top_conv (K (Conv.try_conv rewr_one)) ctxt, Thm.beta_conversion true] in apply_to_thm' cv th end fun hoare_goal_update ctxt (id, th) = if Util.is_implies (Thm.prop_of th) then AddItems {id = id, sc = SOME 1, raw_items = [Fact (TY_CODE_POS, [Thm.prop_of th], th)]} else let val (ex_ritems, res_th) = th |> apply_to_thm' (normalize_hoare_goal_cv ctxt) |> Update.apply_exists_ritems ctxt val (res_th', rest) = res_th |> UtilLogic.split_conj_gen_th |> filter_split (is_neg_hoare_triple o prop_of') val _ = assert (length res_th' = 1) "hoare_goal_update" val res_th' = res_th' |> the_single |> apply_to_thm' (Conv.arg_conv (norm_precond ctxt)) |> normalize_let ctxt val ritems = ex_ritems @ map Update.thm_to_ritem rest @ [Fact (TY_CODE_POS, [prop_of' res_th'], res_th')] in AddItems {id = id, sc = SOME 1, raw_items = ritems} end fun entail_goal_update ctxt (id, th) = if Util.is_implies (Thm.prop_of th) then AddItems {id = id, sc = SOME 1, raw_items = [Fact (TY_ENTAIL, [Thm.prop_of th], th)]} else let val (ex_ritems, res_th) = th |> apply_to_thm' (normalize_entail_goal_cv ctxt) |> Update.apply_exists_ritems ctxt val (res_th', rest) = res_th |> UtilLogic.split_conj_gen_th |> filter_split (is_neg_entail o prop_of') val _ = assert (length res_th' = 1) "entail_goal_update" val res_th' = res_th' |> the_single |> apply_to_thm' (Conv.arg_conv (norm_entail_conds ctxt)) |> normalize_let ctxt val ritems = ex_ritems @ map Update.thm_to_ritem rest @ [Fact (TY_ENTAIL, [prop_of' res_th'], res_th')] in AddItems {id = id, sc = SOME 1, raw_items = ritems} end fun init_entail_fn ctxt item = if not (BoxID.has_incr_id (#id item)) then [] else let val {id, prop, ...} = item in [entail_goal_update ctxt (id, prop)] end val init_entail = {name = "sep.init_entail", args = [TypedMatch (TY_PROP, get_neg (entail_t $ Var (("A",0), assnT) $ Var (("B",0), assnT)))], func = OneStep init_entail_fn} (* Apply entailment to the pre-condition P of P ==>_A Q. *) fun forward_ent_prfstep_fn ent_th ctxt item = if is_implies_item item then [] else let val (A, _) = dest_entail (prop_of' ent_th) val {id, prop, ...} = item val (P, _) = prop |> prop_of' |> dest_not |> dest_entail val cP = Thm.cterm_of ctxt P val insts = (AssnMatcher.assn_match_single ctxt (A, cP) (id, fo_init)) |> filter (BoxID.has_incr_id o fst o fst) fun process_inst ((id', _), eq_th) = (* eq_th is P == pat(inst) * P' *) let val prop' = prop |> apply_to_thm' ( Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv eq_th))) val prop'' = [prop', ent_th] MRS entails_frame_th' in [entail_goal_update ctxt (id', prop''), ShadowItem {id = id', item = item}] end in if null insts then [] else process_inst (hd insts) end fun forward_ent_prfstep ent_th = {name = Util.name_of_thm ent_th ^ "@ent", args = [TypedUniv TY_ENTAIL], func = OneStep (forward_ent_prfstep_fn ent_th)} fun backward_ent_prfstep_fn ent_th ctxt item = if is_implies_item item then [] else let val (_, B) = dest_entail (prop_of' ent_th) val {id, prop, ...} = item val (_, Q) = prop |> prop_of' |> dest_not |> dest_entail val cQ = Thm.cterm_of ctxt Q val insts = (AssnMatcher.assn_match_single ctxt (B, cQ) (id, fo_init)) |> filter (BoxID.has_incr_id o fst o fst) fun process_inst ((id', _), eq_th) = (* eq_th is P == pat(inst) * P' *) let val prop' = prop |> apply_to_thm' ( Conv.arg_conv (Conv.arg_conv (Conv.rewr_conv eq_th))) val prop'' = [prop', ent_th] MRS entails_frame_th'' in [entail_goal_update ctxt (id', prop''), ShadowItem {id = id', item = item}] end in if null insts then [] else process_inst (hd insts) end fun backward_ent_prfstep ent_th = {name = Util.name_of_thm ent_th ^ "@entback", args = [TypedUniv TY_ENTAIL], func = OneStep (backward_ent_prfstep_fn ent_th)} fun group_pure_assn ct = let val t = Thm.term_of ct in if is_pure_assn t then mult_emp_left ct else if UtilArith.is_times t then if has_pure_assn (dest_arg1 t) then Conv.every_conv [ Conv.arg1_conv group_pure_assn, ACUtil.assoc_cv assn_ac_info, Conv.arg_conv (rewr_obj_eq (obj_sym pure_conj_th))] ct else Conv.all_conv ct else Conv.all_conv ct end fun make_sch_th ctxt th = case Thm.prop_of th of Const (@{const_name Pure.all}, _) $ Abs (nm, T, _) => let val var = Var ((nm,0),T) in Thm.forall_elim (Thm.cterm_of ctxt var) th end | _ => raise Fail "make_sch_th" fun entails_norm_ex ctxt th = let val t = prop_of' th val (_, Q) = t |> dest_not |> dest_entail in if is_ex_assn Q then (th RS entails_ex_post_th) |> apply_to_thm (UtilLogic.to_meta_conv ctxt) |> make_sch_th ctxt |> entails_norm_ex ctxt else th end (* Solve an entailment. *) fun entails_resolve_fn ctxt item = if is_implies_item item then [] else let val {id, prop, ...} = item val prop = entails_norm_ex ctxt prop val (P, Q) = dest_entail (get_neg (prop_of' prop)) val cP = Thm.cterm_of ctxt P val Q' = strip_pure_assn Q val insts = (AssnMatcher.assn_match_strict ctxt (Q', cP) (id, fo_init)) |> filter (BoxID.has_incr_id o fst o fst) fun process_inst ((id', _), mod_th) = if has_pure_assn Q then let val prop' = prop |> apply_to_thm' ( Conv.arg_conv (Conv.arg_conv group_pure_assn)) val res = [prop', mod_th] MRS entails_pure_post_th in Update.thm_update (id', res) end else Update.thm_update (id', [prop, mod_th] MRS @{thm contra_triv}) in map process_inst insts end val entails_resolve = {name = "sep.entails_resolve", args = [TypedUniv TY_ENTAIL], func = OneStep entails_resolve_fn} (* Initialize CODE_POS item from a Hoare triple goal. *) fun init_pos_fn ctxt item = let val {id, prop, ...} = item val thy = Proof_Context.theory_of ctxt val (_, c, _) = dest_hoare_triple (get_neg (prop_of' prop)) val proc_defs = get_proc_def thy c fun process_proc_def proc_def = let val (lhs, _) = proc_def |> prop_of' |> dest_eq val cc = Thm.cterm_of ctxt c val insts = (Matcher.rewrite_match ctxt (lhs, cc) (id, fo_init)) |> filter (BoxID.has_incr_id o fst o fst) fun process_inst ((id', _), eq_th) = let val cv = Conv.every_conv [ Conv.rewr_conv (meta_sym eq_th), rewr_obj_eq proc_def] val th = apply_to_thm' (Conv.arg_conv (Conv.arg1_conv cv)) prop in hoare_goal_update ctxt (id', th) end in map process_inst insts end in if null proc_defs then if BoxID.has_incr_id id then [hoare_goal_update ctxt (id, prop)] else [] else maps process_proc_def proc_defs end val init_pos = {name = "sep.init_pos", args = [TypedMatch (TY_PROP, get_neg hoare_triple_pat)], func = OneStep init_pos_fn} fun forward_hoare_prfstep_fn ent_th ctxt item = if is_implies_item item then [] else let val (A, _) = dest_entail (prop_of' ent_th) val {id, prop, ...} = item val (P, _, _) = prop |> prop_of' |> dest_not |> dest_hoare_triple val cP = Thm.cterm_of ctxt P val insts = (AssnMatcher.assn_match_single ctxt (A, cP) (id, fo_init)) |> filter (BoxID.has_incr_id o fst o fst) fun process_inst ((id', _), eq_th) = let val prop' = prop |> apply_to_thm' ( Conv.arg_conv (Util.argn_conv 0 (Conv.rewr_conv eq_th))) val prop'' = [prop', ent_th] MRS pre_rule_th' in [hoare_goal_update ctxt (id', prop''), ShadowItem {id = id', item = item}] end in if null insts then [] else process_inst (hd insts) end fun forward_hoare_prfstep ent_th = {name = Util.name_of_thm ent_th ^ "@hoare_ent", args = [TypedUniv TY_CODE_POS], func = OneStep (forward_hoare_prfstep_fn ent_th)} fun add_forward_ent_prfstep ent_th thy = let val name = Util.name_of_thm ent_th val ctxt = Proof_Context.init_global thy val _ = writeln ("Add forward entailment " ^ name ^ "\n" ^ Syntax.string_of_term ctxt (prop_of' ent_th)) in thy |> add_prfstep (forward_ent_prfstep ent_th) |> add_prfstep (forward_hoare_prfstep ent_th) end fun add_backward_ent_prfstep ent_th thy = let val name = Util.name_of_thm ent_th val ctxt = Proof_Context.init_global thy val _ = writeln ("Add backward entailment " ^ name ^ "\n" ^ Syntax.string_of_term ctxt (prop_of' ent_th)) in add_prfstep (backward_ent_prfstep ent_th) thy end fun add_rewrite_ent_rule th thy = let val forward_th = (th RS entails_equiv_forward_th) |> Drule.zero_var_indexes |> Util.update_name_of_thm th "@forward" val backward_th = (th RS entails_equiv_backward_th) |> Drule.zero_var_indexes |> Util.update_name_of_thm th "@backward" in thy |> add_forward_ent_prfstep forward_th |> add_backward_ent_prfstep backward_th end (* Rewrite the first command of a Hoare triple. *) fun rewr_first_cmd eq_th ct = let val (_, c, _) = ct |> Thm.term_of |> dest_hoare_triple in if is_bind_cmd c then Conv.arg1_conv (Conv.arg1_conv (rewr_obj_eq eq_th)) ct else Conv.arg1_conv (rewr_obj_eq eq_th) ct end (* Apply rewrite to the first command in CODE_POS. *) fun rewrite_pos_fn ctxt item1 item2 = if is_implies_item item1 then [] else let val {id = id1, prop = th, ...} = item1 val {id = id2, prop = eq_th, ...} = item2 val (_, c, _) = th |> prop_of' |> dest_not |> dest_hoare_triple val c' = get_first_cmd c val (c1, _) = eq_th |> prop_of' |> dest_eq val id = BoxID.merge_boxes ctxt (id1, id2) in if not (BoxID.has_incr_id id) then [] else if c1 aconv c' then let val th' = th |> apply_to_thm' (Conv.arg_conv (rewr_first_cmd eq_th)) in [hoare_goal_update ctxt (id, th'), ShadowItem {id = id, item = item1}] end else [] end val rewrite_pos = {name = "sep.rewrite_pos", args = [TypedUniv TY_CODE_POS, TypedMatch (TY_EQ, heap_eq_pat)], func = TwoStep rewrite_pos_fn} (* Extract the pure pre-conditions from a Hoare triple fact. *) fun extract_pure_hoare_cv ct = let val (P, _, _) = ct |> Thm.term_of |> dest_hoare_triple in if is_pure_assn P then rewr_obj_eq norm_pre_pure_iff2_th ct else if UtilArith.is_times P andalso is_pure_assn (dest_arg P) then Conv.every_conv [rewr_obj_eq norm_pre_pure_iff_th, Conv.arg_conv extract_pure_hoare_cv] ct else Conv.all_conv ct end (* Use a Hoare triple to advance a step in CODE_POS. *) fun match_hoare_th id ctxt hoare_th goal item = let val (P, c, _) = goal |> prop_of' |> dest_not |> dest_hoare_triple val c' = get_first_cmd c val (P', pat, _) = dest_hoare_triple (prop_of' hoare_th) val cc = Thm.cterm_of ctxt c' val insts = Matcher.rewrite_match ctxt (pat, cc) (id, fo_init) fun process_inst ((id', inst), eq_th) = let val P'' = P' |> strip_pure_assn |> Util.subst_term_norm inst val cP = Thm.cterm_of ctxt P val insts' = (AssnMatcher.assn_match_all ctxt (P'', cP) (id', inst)) |> filter (BoxID.has_incr_id o fst o fst) fun process_inst' ((id'', inst'), ent_th) = let val hoare_th = (Util.subst_thm ctxt inst' hoare_th) |> apply_to_thm' (Conv.arg1_conv (Conv.rewr_conv eq_th)) |> apply_to_thm' extract_pure_hoare_cv |> apply_to_thm (UtilLogic.to_meta_conv ctxt) val hoare_th' = [hoare_th, ent_th] MRS pre_rule_th'' in if is_bind_cmd c then let val return_var = extract_return_var c val th' = [hoare_th', goal] MRS bind_rule_th' val (_, (assms, concl)) = th' |> Thm.prop_of |> Util.strip_meta_horn val concl' = concl |> dest_Trueprop |> Util.rename_abs_term [return_var] |> mk_Trueprop val t' = Util.list_meta_horn ([], (assms, concl')) val th' = Thm.renamed_prop t' th' in [hoare_goal_update ctxt (id'', th'), ShadowItem {id = id'', item = item}] end else [entail_goal_update ctxt (id'', [hoare_th', goal] MRS post_rule_th'), ShadowItem {id = id'', item = item}] end in if null insts' then [] else process_inst' (hd insts') end in if null insts then [] else process_inst (hd insts) end (* Match with PROP or DISJ items that are Hoare triples. In this function, we assume item1 is a Hoare triple (and item2 is the CODE_POS item). *) fun match_hoare_prop_fn ctxt item1 item2 = if is_implies_item item2 then [] else let val {id = id1, prop = hoare_th, ...} = item1 val {id = id2, prop = goal, ...} = item2 val id = BoxID.merge_boxes ctxt (id1, id2) in match_hoare_th id ctxt hoare_th goal item2 end val match_hoare_prop = {name = "sep.match_hoare_prop", args = [TypedMatch (TY_PROP, hoare_triple_pat), TypedUniv TY_CODE_POS], func = TwoStep match_hoare_prop_fn} (* For DISJ items, check that it is a Hoare triple. *) fun match_hoare_disj_fn ctxt item1 item2 = if is_implies_item item2 then [] else let val {tname, ...} = item1 val (_, csubs) = Logic_ProofSteps.dest_tname_of_disj tname val subs = map Thm.term_of csubs in if length subs > 1 then [] else if not (is_hoare_triple (the_single subs)) then [] else match_hoare_prop_fn ctxt item1 item2 end val match_hoare_disj = {name = "sep.match_hoare_disj", args = [TypedUniv TY_DISJ, TypedUniv TY_CODE_POS], func = TwoStep match_hoare_disj_fn} (* Match a MATCH_POS item with hoare triple
(b)> c c c with
proposition b, resulting in a new MATCH_POS item (shadowing the
original one) with hoare triple
. Only work in the case
where there are no schematic variables in b.
*)
fun match_assn_pure_fn ctxt item1 item2 =
let
val {id, prop, ...} = item1
in
if Util.is_implies (Thm.prop_of prop) then
let
val (A, _) = Logic.dest_implies (Thm.prop_of prop)
val pat = PropMatch (dest_Trueprop A)
val insts = (ItemIO.match_arg ctxt pat item2 (id, fo_init))
|> filter (BoxID.has_incr_id o fst o fst)
fun process_inst ((id', _), th) =
[hoare_goal_update ctxt (id', th RS prop),
ShadowItem {id = id', item = item1}]
in
maps process_inst insts
end
else []
end
val match_assn_pure =
{name = "sep.match_assn_pure",
args = [TypedUniv TY_CODE_POS,
PropMatch (@{term_pat "?b::bool"})],
func = TwoStep match_assn_pure_fn}
fun hoare_create_case_fn _ item =
let
val {id, prop, ...} = item
in
if not (BoxID.has_incr_id id) then [] else
if Util.is_implies (Thm.prop_of prop) then
let
val (A, _) = Logic.dest_implies (Thm.prop_of prop)
in
[AddBoxes {id = id, sc = SOME 1, init_assum = get_neg' A}]
end
else []
end
val hoare_create_case =
{name = "sep.hoare_create_case",
args = [TypedUniv TY_CODE_POS],
func = OneStep hoare_create_case_fn}
fun entail_pure_fn ctxt item1 item2 =
let
val {id, prop, ...} = item1
in
if Util.is_implies (Thm.prop_of prop) then
let
val (A, _) = Logic.dest_implies (Thm.prop_of prop)
val pat = PropMatch (dest_Trueprop A)
val insts = (ItemIO.match_arg ctxt pat item2 (id, fo_init))
|> filter (BoxID.has_incr_id o fst o fst)
fun process_inst ((id', _), th) =
[entail_goal_update ctxt (id', th RS prop),
ShadowItem {id = id', item = item1}]
in
maps process_inst insts
end
else []
end
val entail_pure =
{name = "sep.entail_pure",
args = [TypedUniv TY_ENTAIL,
PropMatch (@{term_pat "?b::bool"})],
func = TwoStep entail_pure_fn}
fun entail_create_case_fn _ item =
let
val {id, prop, ...} = item
in
if not (BoxID.has_incr_id id) then [] else
if Util.is_implies (Thm.prop_of prop) then
let
val (A, _) = Logic.dest_implies (Thm.prop_of prop)
in
[AddBoxes {id = id, sc = SOME 1, init_assum = get_neg' A}]
end
else []
end
val entail_create_case =
{name = "sep.entail_create_case",
args = [TypedUniv TY_ENTAIL],
func = OneStep entail_create_case_fn}
(* Matching CODE_POS with an existing Hoare triple. *)
fun hoare_triple_fn ctxt item =
if is_implies_item item then [] else
let
val thy = Proof_Context.theory_of ctxt
val {id, prop = goal, ...} = item
val (_, c, _) = goal |> prop_of' |> dest_not |> dest_hoare_triple
val hoare_ths = c |> get_first_cmd |> Util.get_head_name
|> get_hoare_triples thy
in
maps (fn hoare_th => match_hoare_th id ctxt hoare_th goal item) hoare_ths
end
val hoare_triple =
{name = "sep.hoare_triple",
args = [TypedUniv TY_CODE_POS],
func = OneStep hoare_triple_fn}
(* Contract a Hoare triple to
form. *)
fun contract_hoare_cv' ct =
if is_imp (Thm.term_of ct) then
Conv.every_conv [Conv.arg_conv contract_hoare_cv',
rewr_obj_eq (obj_sym norm_pre_pure_iff_th)] ct
else
Conv.all_conv ct
fun contract_hoare_cv ctxt ct =
Conv.every_conv [contract_hoare_cv', norm_precond ctxt] ct
(* Given hoare_th of the form ?c , produce proofstep matching
item1 with CODE_POS (?h, ?c) and item2 with proposition ?h |= ?P *
?Ru.
*)
fun add_hoare_triple_prfstep hoare_th thy =
let
val name = Util.name_of_thm hoare_th
val ctxt = Proof_Context.init_global thy
val hoare_th' =
hoare_th |> apply_to_thm (UtilLogic.to_obj_conv ctxt)
|> apply_to_thm' (contract_hoare_cv ctxt)
|> Util.update_name_of_thm hoare_th ""
val _ = writeln ("Add Hoare triple " ^ name ^ "\n" ^
Syntax.string_of_term ctxt (prop_of' hoare_th'))
in
thy |> update_hoare_triple hoare_th'
end
fun code_pos_terms ts =
let
val t = the_single ts
in
if fastype_of t = propT then []
else let
val (P, c, _) = t |> dest_not |> dest_hoare_triple
in
SepUtil.assn_rewr_terms P @ [get_first_cmd c]
end
end
fun entail_terms ts =
let
val t = the_single ts
in
if fastype_of t = propT then []
else let
val (P, Q) = t |> dest_not |> dest_entail
in
maps SepUtil.assn_rewr_terms [P, Q]
end
end
val add_sep_logic_proofsteps =
fold ItemIO.add_item_type [
(TY_CODE_POS, SOME code_pos_terms, NONE, NONE),
(TY_ENTAIL, SOME entail_terms, NONE, NONE)
] #> fold add_prfstep [
init_entail, entails_resolve,
init_pos, rewrite_pos, match_assn_pure, hoare_triple,
match_hoare_disj, match_hoare_prop, hoare_create_case,
entail_pure, entail_create_case
]
end (* structure SepLogic *)
diff --git a/thys/Automated_Stateful_Protocol_Verification/trac/trac.thy b/thys/Automated_Stateful_Protocol_Verification/trac/trac.thy
--- a/thys/Automated_Stateful_Protocol_Verification/trac/trac.thy
+++ b/thys/Automated_Stateful_Protocol_Verification/trac/trac.thy
@@ -1,1947 +1,1946 @@
(*
(C) Copyright Andreas Viktor Hess, DTU, 2020
(C) Copyright Sebastian A. Mödersheim, DTU, 2020
(C) Copyright Achim D. Brucker, University of Exeter, 2020
(C) Copyright Anders Schlichtkrull, DTU, 2020
All Rights Reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
- Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
- Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
- Neither the name of the copyright holder nor the names of its
contributors may be used to endorse or promote products
derived from this software without specific prior written
permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)
(* Title: trac.thy
Author: Andreas Viktor Hess, DTU
Author: Sebastian A. Mödersheim, DTU
Author: Achim D. Brucker, University of Exeter
Author: Anders Schlichtkrull, DTU
*)
section\