diff --git a/thys/Auto2_HOL/logic_steps.ML b/thys/Auto2_HOL/logic_steps.ML --- a/thys/Auto2_HOL/logic_steps.ML +++ b/thys/Auto2_HOL/logic_steps.ML @@ -1,1081 +1,1081 @@ (* File: logic_steps.ML Author: Bohua Zhan Core (logic) proofsteps. *) signature LOGIC_PROOFSTEPS = sig (* General logic *) val shadow_prop_item: proofstep val shadow_term_item: proofstep val exists_elim_prfstep: proofstep val add_logic_proofsteps: theory -> theory val mk_all_disj: term list * term list -> term val strip_all_disj: term -> term list * term list val norm_all_disj: Proof.context -> conv val replace_disj_vars: Proof.context -> term list * term list -> term list * term list val disj_prop_match: Proof.context -> id_inst -> term * (term list * term list) * ((indexname * typ) list * cterm list) -> id_inst_th list val norm_conj: conv (* DISJ items. *) val TY_DISJ: string val disj_to_ritems: bool -> term -> thm -> raw_item list val disj_to_update: bool -> term -> box_id * int option * thm -> raw_update val dest_tname_of_disj: cterm list -> term * cterm list val is_match_prem_only: box_item -> bool val analyze_disj_th: Proof.context -> thm -> term * thm val disj_rewr_terms: term list -> term list val output_disj_fn: item_output val disj_prop_matcher: item_matcher val reduce_disj_True: conv val match_update_prfstep: proofstep val match_one_sch_prfstep: proofstep val disj_match_iff_prfstep: proofstep val disj_create_case_prfstep: proofstep val disj_shadow_prfstep: proofstep val add_disj_proofsteps: theory -> theory (* Normalizers *) val split_not_imp_th: thm -> thm list val split_conj_gen_th: Proof.context -> thm -> thm list val eq_normalizer: normalizer val property_normalizer: normalizer val disj_normalizer: normalizer val logic_thm_update: Proof.context -> box_id * thm -> raw_update val add_disj_normalizers: theory -> theory end; structure Logic_ProofSteps : LOGIC_PROOFSTEPS = struct fun boolVar s = Var ((s, 0), boolT) (* Shadowing based on equivalence. For both PROP and TERM items, shadowing is based on subterm equivalence, skipping any Not (~) at head. *) fun shadow_item_fn ctxt item1 item2 = if #sc item1 = 0 andalso #sc item2 = 0 then [] else let val id = BoxItem.merged_id ctxt [item1, item2] val _ = assert (forall (BoxItem.match_ty_strs [TY_TERM, TY_PROP]) [item1, item2]) "shadow_item_fn" val (tname1, tname2) = (the_single (#tname item1), the_single (#tname item2)) handle List.Empty => raise Fail "shadow_item_fn" val (t1, t2) = (Thm.term_of tname1, Thm.term_of tname2) val (lhs, rhs) = if fastype_of t1 = boolT andalso is_neg t1 andalso fastype_of t2 = boolT andalso is_neg t2 then (UtilLogic.get_cneg tname1, UtilLogic.get_cneg tname2) else (tname1, tname2) val equiv_ids = (RewriteTable.subequiv_info ctxt id (lhs, rhs)) |> map fst |> filter BoxID.has_incr_id |> Util.max_partial (BoxID.is_eq_ancestor ctxt) val item_to_shadow = if #uid item1 > #uid item2 then item1 else item2 fun process_id id' = ShadowItem {id = id', item = item_to_shadow} in map process_id equiv_ids end val shadow_prop_item = {name = "shadow_prop", args = [TypedUniv TY_PROP, TypedUniv TY_PROP], func = TwoStep shadow_item_fn} val shadow_term_item = {name = "shadow_term", args = [TypedUniv TY_TERM, TypedUniv TY_TERM], func = TwoStep shadow_item_fn} fun eq_abs_fn ctxt item1 item2 = let val {id = id1, tname = tname1, ...} = item1 val {id = id2, tname = tname2, ...} = item2 val id = BoxID.merge_boxes ctxt (id1, id2) val (ct1, ct2) = apply2 the_single (tname1, tname2) val (t1, t2) = apply2 Thm.term_of (ct1, ct2) in if not (Util.is_abs t1) orelse not (Util.is_abs t2) then [] else if RewriteTable.is_equiv id ctxt (ct1, ct2) then [] else if Term_Ord.term_ord (t2, t1) = LESS then [] else let fun process_equiv (id', eq_th) = let val (lhs, rhs) = (Util.lhs_of eq_th, Util.rhs_of eq_th) in AddItems {id = id', sc = SOME 1, raw_items = [Fact (TY_EQ, [lhs, rhs], eq_th)]} end in (Matcher.rewrite_match ctxt (t1, ct2) (id, fo_init)) |> map (fn ((id, _), eq_th) => (id, eq_th)) |> filter (BoxID.has_incr_id o fst) |> Util.max_partial (BoxID.id_is_eq_ancestor ctxt) |> map process_equiv end end val eq_abs_prfstep = {name = "eq_abs", args = [TypedUniv TY_TERM, TypedUniv TY_TERM], func = TwoStep eq_abs_fn} (* Given an assumption of the form EX x. A, we produce an assumption A with x in A replaced by a free variable. To avoid name collisions, when the update is produced x is replaced by an "internal" free variable, with suffix '_'. When the update is applied, that internal free variable is replaced by a fresh variable as determined by the context. We produce at most two variables at a time. *) fun exists_elim_fn ctxt {id, prop, ...} = if not (BoxID.has_incr_id id) then [] else let val t = prop_of' prop in if is_ex t orelse is_bex t orelse (is_neg t andalso is_obj_all (dest_not t)) orelse (is_neg t andalso is_ball (dest_not t)) then let val (ritems, th') = prop |> apply_to_thm' (UtilLogic.normalize_exists ctxt) |> Update.apply_exists_ritems ctxt in [AddItems {id = id, sc = NONE, raw_items = ritems @ [Update.thm_to_ritem th']}] end else [] end val exists_elim_prfstep = {name = "exists_elim", args = [TypedUniv TY_PROP], func = OneStep exists_elim_fn} val add_logic_proofsteps = fold add_prfstep [ shadow_prop_item, shadow_term_item, exists_elim_prfstep, eq_abs_prfstep ] (* Given (x_1 ... x_n, A_1 ... A_n), create the corresponding forall-disj term. *) fun mk_all_disj (vars, terms) = case vars of [] => list_disj terms | var :: vars' => mk_obj_all var (mk_all_disj (vars', terms)) (* Normalize t into a disjunction of terms. *) fun strip_disj t = if is_disj t then maps strip_disj [dest_arg1 t, dest_arg t] else if is_imp t then maps strip_disj [get_neg (dest_arg1 t), dest_arg t] else if is_neg t then let val t' = dest_not t in if is_neg t' then strip_disj (dest_not t') else if is_conj t' then maps strip_disj [get_neg (dest_arg1 t'), get_neg (dest_arg t')] else [t] end else [t] (* Normalize a term into the form !x_1 ... x_n. A_1 | ... | A_n *) fun strip_all_disj t = if is_obj_all t then case t of - _ $ Abs (abs as (_, T, _)) => + _ $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u + val var = Free v val (vars, disjs) = strip_all_disj body in if exists (Util.occurs_free var) disjs then (var :: vars, disjs) else (vars, disjs) end | f $ arg => strip_all_disj (f $ UtilLogic.force_abs_form arg) | _ => raise Fail "strip_all_disj" else if is_ball t then case t of - _ $ S $ Abs (abs as (_, T, _)) => + _ $ S $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u + val var = Free v val mem = mk_mem (var, S) val (vars, disjs) = strip_all_disj body in (var :: vars, get_neg mem :: disjs) end | f $ S $ arg => strip_all_disj (f $ S $ UtilLogic.force_abs_form arg) | _ => raise Fail "strip_all_disj" else if is_neg t andalso is_ex (dest_not t) then case dest_not t of - _ $ Abs (abs as (_, T, _)) => + _ $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u + val var = Free v val (vars, disjs) = strip_all_disj (get_neg body) in if exists (Util.occurs_free var) disjs then (var :: vars, disjs) else (vars, disjs) end | f $ arg => strip_all_disj (get_neg (f $ UtilLogic.force_abs_form arg)) | _ => raise Fail "strip_all_disj" else if is_neg t andalso is_bex (dest_not t) then case dest_not t of - _ $ S $ Abs (abs as (_, T, _)) => + _ $ S $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u + val var = Free v val mem = mk_mem (var, S) val (vars, disjs) = strip_all_disj (get_neg body) in (var :: vars, get_neg mem :: disjs) end | f $ S $ arg => strip_all_disj (get_neg (f $ S $ UtilLogic.force_abs_form arg)) | _ => raise Fail "strip_all_disj" else if is_disj t then let val (v1, ts1) = strip_all_disj (dest_arg1 t) val (v2, ts2) = strip_all_disj (dest_arg t) in (v1 @ v2, ts1 @ ts2) end else if is_imp t then let val (v1, ts1) = strip_all_disj (get_neg (dest_arg1 t)) val (v2, ts2) = strip_all_disj (dest_arg t) in (v1 @ v2, ts1 @ ts2) end else if is_neg t then let val t' = dest_not t in if is_neg t' then strip_all_disj (dest_not t') else if is_conj t' then let val (v1, ts1) = strip_all_disj (get_neg (dest_arg1 t')) val (v2, ts2) = strip_all_disj (get_neg (dest_arg t')) in (v1 @ v2, ts1 @ ts2) end else ([], [t]) end else ([], [t]) (* Normalize (A_1 | A_2 | ... | A_m) | (B_1 | B_2 | ... | B_n) *) fun norm_disj_clauses ct = let val (arg1, _) = Util.dest_binop_args (Thm.term_of ct) in if is_disj arg1 then Conv.every_conv [rewr_obj_eq UtilBase.disj_assoc_th, Conv.arg_conv norm_disj_clauses] ct else Conv.all_conv ct end (* Normalize ct. *) fun norm_disj ct = let val t = Thm.term_of ct val _ = assert (fastype_of t = boolT) "norm_disj: wrong type" in if is_disj t then Conv.every_conv [Conv.binop_conv norm_disj, norm_disj_clauses] ct else if is_imp t then Conv.every_conv [rewr_obj_eq UtilBase.imp_conv_disj_th, norm_disj] ct else if is_neg t andalso is_neg (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.nn_cancel_th, norm_disj] ct else if is_neg t andalso is_conj (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.de_Morgan_conj_th, norm_disj] ct else Conv.all_conv ct end (* Normalize to forall at the top-level *) fun norm_all_disj ctxt ct = let val t = Thm.term_of ct in if is_obj_all t then if not (Util.is_subterm (Bound 0) (dest_arg t)) then Conv.every_conv [rewr_obj_eq UtilBase.all_trivial_th, norm_all_disj ctxt] ct else Conv.every_conv [Conv.binder_conv (norm_all_disj o snd) ctxt] ct else if is_ball t then Conv.every_conv [rewr_obj_eq UtilBase.Ball_def_th, norm_all_disj ctxt] ct else if is_neg t andalso is_ex (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.not_ex_th, norm_all_disj ctxt] ct else if is_neg t andalso is_bex (dest_not t) then Conv.every_conv [ Conv.arg_conv (rewr_obj_eq UtilBase.Bex_def_th), norm_all_disj ctxt] ct else if is_disj t then let val eq1 = Conv.binop_conv (norm_all_disj ctxt) ct val rhs = Util.rhs_of eq1 in if is_obj_all (dest_arg1 rhs) then Conv.every_conv [Conv.rewr_conv eq1, rewr_obj_eq UtilBase.disj_commute_th, rewr_obj_eq UtilBase.swap_all_disj_th, norm_all_disj ctxt] ct else if is_obj_all (dest_arg rhs) then Conv.every_conv [Conv.rewr_conv eq1, rewr_obj_eq UtilBase.swap_all_disj_th, norm_all_disj ctxt] ct else Conv.every_conv [Conv.rewr_conv eq1, norm_disj_clauses] ct end else if is_imp t then Conv.every_conv [rewr_obj_eq UtilBase.imp_conv_disj_th, norm_all_disj ctxt] ct else if is_neg t andalso is_neg (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.nn_cancel_th, norm_all_disj ctxt] ct else if is_neg t andalso is_conj (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.de_Morgan_conj_th, norm_all_disj ctxt] ct else Conv.all_conv ct end fun mk_disj_eq eq_ths = case eq_ths of [] => raise Fail "mk_disj_eq" | [eq] => eq | eq :: eqs' => Drule.binop_cong_rule UtilBase.cDisj eq (mk_disj_eq eqs') (* Sort A | (B_1 | B_2 | ... | B_n), assuming the right side is sorted. *) fun sort_disj_clause_aux ct = if not (is_disj (Thm.term_of ct)) then Conv.all_conv ct else let val (arg1, arg2) = Util.dest_binop_args (Thm.term_of ct) in if is_disj arg2 then if Term_Ord.term_ord (dest_arg1 arg2, arg1) = LESS then 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, Conv.arg_conv sort_disj_clause_aux] ct else Conv.all_conv ct else if Term_Ord.term_ord (arg2, arg1) = LESS then rewr_obj_eq (obj_sym UtilBase.disj_commute_th) ct else Conv.all_conv ct end (* Sort A_1 | ... | A_n. *) fun sort_disj_clause ct = if not (is_disj (Thm.term_of ct)) then Conv.all_conv ct else Conv.every_conv [Conv.arg_conv sort_disj_clause, sort_disj_clause_aux] ct (* Apply cv on the body of !x y z. ... .*) fun forall_body_conv cv ctxt ct = if is_obj_all (Thm.term_of ct) then Conv.binder_conv (fn (_, ctxt) => forall_body_conv cv ctxt) ctxt ct else cv ct fun norm_all_disj_sorted ctxt ct = Conv.every_conv [norm_all_disj ctxt, forall_body_conv sort_disj_clause ctxt] ct fun abstract_eq ctxt var eq = let val (x, T) = Term.dest_Free var val all_const = Const (UtilBase.All_name, (T --> boolT) --> boolT) in Drule.arg_cong_rule (Thm.cterm_of ctxt all_const) (Thm.abstract_rule x (Thm.cterm_of ctxt var) eq) end fun replace_disj_vars ctxt (vars, disjs) = let val vars' = vars |> map Term.dest_Free |> Variable.variant_frees ctxt [] |> map Free val subst = vars ~~ vars' in (vars', map (subst_atomic subst) disjs) end (* Matching for all-disj propositions *) fun disj_prop_match ctxt (id, (tyinst, inst)) (t, (var_t, ts), (var_u, cus)) = let val thy = Proof_Context.theory_of ctxt val us = map Thm.term_of cus in if length var_t <> length var_u orelse length ts <> length us then [] else let (* First match the types (return [] if no match). *) val tys_t = map fastype_of var_t val tys_u = map snd var_u val tyinst' = fold (Sign.typ_match thy) (tys_t ~~ tys_u) tyinst val var_t' = map (Envir.subst_term_types tyinst') var_t val ts' = ts |> map (Envir.subst_term_types tyinst') val var_ct' = map (Thm.cterm_of ctxt) var_t' val cus' = cus |> map (Thm.instantiate_cterm (TVars.empty, Vars.make (var_u ~~ var_ct'))) (* Match the type-instantiated pattern with term. *) val insts = Matcher.rewrite_match_subset ctxt var_t' (ts', cus') (id, (tyinst', inst)) fun process_inst ((id', instsp'), ths) = let (* Equality between normalized t and u *) val eq_th = ths |> mk_disj_eq |> fold (abstract_eq ctxt) (rev var_t') |> apply_to_lhs (norm_all_disj_sorted ctxt) |> apply_to_rhs (norm_all_disj_sorted ctxt) (* Equality between un-normalized t and u *) val t' = Util.subst_term_norm instsp' t val norm1 = norm_all_disj_sorted ctxt (Thm.cterm_of ctxt t') val cu = Thm.cterm_of ctxt (mk_all_disj (var_t', map Thm.term_of cus')) val norm2 = norm_all_disj_sorted ctxt cu val eq_th' = Util.transitive_list [norm1, eq_th, meta_sym norm2] in ((id', instsp'), eq_th') end in map process_inst insts end handle Type.TYPE_MATCH => [] end fun norm_conj_de_Morgan ct = let val t = Thm.term_of ct in if is_neg t andalso is_disj (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.de_Morgan_disj_th, Conv.arg_conv norm_conj_de_Morgan] ct else Conv.all_conv ct end fun norm_conj_not_imp ct = let val t = Thm.term_of ct in if is_neg t andalso is_imp (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.not_imp_th, Conv.arg_conv norm_conj_not_imp] ct else Conv.all_conv ct end fun norm_nn_cancel ct = let val t = Thm.term_of ct in if is_neg t andalso is_neg (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.nn_cancel_th, norm_nn_cancel] ct else Conv.all_conv ct end fun norm_conj ct = let val t = Thm.term_of ct val _ = assert (fastype_of t = boolT) "norm_conj: wrong type" in if is_neg t andalso is_neg (dest_not t) then norm_nn_cancel ct else if is_neg t andalso is_imp (dest_not t) then norm_conj_not_imp ct else if is_neg t andalso is_disj (dest_not t) then norm_conj_de_Morgan ct else Conv.all_conv ct end (* DISJ items. *) val TY_DISJ = "DISJ" (* Given a theorem in the form of a disjunction, possibly containing schematic variables, return the corresponding DISJ item. *) fun disj_to_ritems prem_only disj_head th = let val subs = strip_disj (prop_of' th) in if length subs = 1 then if Util.has_vars (Thm.prop_of th) then let fun th_to_ritem th = Fact (TY_DISJ, UtilLogic.term_of_bool prem_only :: disj :: strip_disj (prop_of' th), th) in map th_to_ritem (th |> apply_to_thm' norm_conj |> UtilLogic.split_conj_th) end else [Fact (TY_PROP, [prop_of' th], th)] else let val tname = UtilLogic.term_of_bool prem_only :: disj_head :: subs in [Fact (TY_DISJ, tname, th)] end end fun disj_to_update prem_only disj_head (id, sc, th) = if Thm.prop_of th aconv pFalse then ResolveBox {id = id, th = th} else AddItems {id = id, sc = sc, raw_items = disj_to_ritems prem_only disj_head th} fun get_disj_head t = if is_disj t then disj else if is_imp t then get_disj_head (dest_arg t) else if is_neg t andalso is_neg (dest_not t) then get_disj_head (dest_not (dest_not t)) else if is_neg t andalso is_conj (dest_not t) then conj else if is_obj_all t orelse is_ball t then case dest_arg t of - Abs (x, T, body) => get_disj_head (snd (Term.dest_abs (x, T, body))) + u as Abs _ => get_disj_head (snd (Term.dest_abs_global u)) | _ => imp else if is_neg t andalso is_ex (dest_not t) then conj else if is_neg t andalso is_bex (dest_not t) then conj else imp (* Given a theorem th, return equivalent theorem in disjunctive form, with possible schematic variables. Also return whether th is "active", that is, whether it is originally a conjunctive goal or disjunctive fact, as opposed to implications. *) fun analyze_disj_th ctxt th = let val head = get_disj_head (prop_of' th) val th' = th |> apply_to_thm' (norm_all_disj ctxt) |> apply_to_thm (UtilLogic.to_meta_conv ctxt) |> Util.forall_elim_sch in (head, th') end (* Deconstruct the tname of a DISJ item. *) fun dest_tname_of_disj tname = case tname of _ :: disj_head :: rest => (Thm.term_of disj_head, rest) | _ => raise Fail "dest_tname_of_disj: too few terms in tname." (* Determine whether the item is for matching premises only (from the first entry in tname. *) fun is_match_prem_only {tname, ...} = UtilLogic.bool_of_term (Thm.term_of (hd tname)) fun is_active_head disj_head = (not (disj_head aconv imp)) fun disj_rewr_terms ts = if UtilLogic.bool_of_term (hd ts) then [] else drop 2 ts fun output_disj_fn ctxt (ts, _) = let val (match_prem, disj_head, subs) = (hd ts, hd (tl ts), tl (tl ts)) val prefix = if UtilLogic.bool_of_term match_prem then "(match_prem) " else "" in if disj_head aconv disj then prefix ^ ((foldr1 mk_disj subs) |> Syntax.string_of_term ctxt) else if disj_head aconv conj then prefix ^ ((foldr1 mk_conj (map get_neg subs)) |> get_neg |> Syntax.string_of_term ctxt) else if disj_head aconv imp then prefix ^ ((foldr1 mk_imp (subs |> split_last |> apfst (map get_neg) |> apsnd single |> (op @))) |> Syntax.string_of_term ctxt) else raise Fail "output_disj_fn: unexpected disj_head." end val disj_prop_matcher = let fun pre_match pat {tname, ...} ctxt = let val (var_t, ts) = (strip_all_disj pat) |> replace_disj_vars ctxt val (_, cus) = dest_tname_of_disj tname val us = map Thm.term_of cus val var_u = fold Term.add_vars us [] in length ts = length us andalso length var_t = length var_u end fun match pat item ctxt (id, instsp) = let val {tname, prop = th, ...} = item val (_, cus) = dest_tname_of_disj tname val us = map Thm.term_of cus val var_u = fold Term.add_vars us [] val (var_t, ts) = (strip_all_disj pat) |> replace_disj_vars ctxt fun process_perm perm = map (pair (map Var perm)) (disj_prop_match ctxt (id, instsp) (pat, (var_t, ts), (perm, cus))) fun process_inst (var_u, ((id', instsp'), eq_th)) = let val eq_th' = make_trueprop_eq (meta_sym eq_th) val forall_th = th |> fold Thm.forall_intr (rev (map (Thm.cterm_of ctxt) var_u)) |> apply_to_thm (UtilLogic.to_obj_conv ctxt) in ((id', instsp'), Thm.equal_elim eq_th' forall_th) end in if length var_t <> length var_u orelse length ts <> length us then [] else var_u |> Util.all_permutes |> maps process_perm |> map process_inst end in {pre_match = pre_match, match = match} end (* Given ct in the form p_1 | ... | p_n, apply cv to each of p_i. *) fun ac_disj_conv cv ct = if is_disj (Thm.term_of ct) then Conv.every_conv [Conv.arg1_conv cv, Conv.arg_conv (ac_disj_conv cv)] ct else cv ct (* Assume ct is a disjunction, associating to the right. *) fun reduce_disj_True ct = if is_disj (Thm.term_of ct) then ((rewr_obj_eq UtilBase.disj_True1_th) else_conv ((Conv.arg_conv reduce_disj_True) then_conv (rewr_obj_eq UtilBase.disj_True2_th))) ct else Conv.all_conv ct (* Handles also the case where pat is in not-conj or imp form. *) fun match_prop ctxt (id, item2) pat = let val disj_pats = strip_disj pat (* th is pat'(inst), where pat' is one of the disjunctive terms of pat. *) fun process_inst ((id, inst), th) = let (* Construct the theorem pat'(inst) == True. *) val to_eqT_cv = (th RS UtilBase.eq_True_th) |> rewr_obj_eq |> Conv.try_conv (* Rewrite pat(inst) using the above, then rewrite to True. *) val pat_eqT = pat |> Thm.cterm_of ctxt |> norm_disj |> Util.subst_thm ctxt inst |> apply_to_rhs (ac_disj_conv to_eqT_cv) |> apply_to_rhs reduce_disj_True |> to_obj_eq val patT = pat_eqT RS UtilBase.eq_True_inv_th in ((id, inst), patT) end val insts1 = (ItemIO.match_arg ctxt (PropMatch pat) item2 (id, fo_init)) |> filter (BoxID.has_incr_id o fst o fst) val insts2 = if length disj_pats > 1 then map process_inst (maps (match_prop ctxt (id, item2)) disj_pats) else [] in insts1 @ insts2 end (* Given theorem ~P, cancel any disjunct that is aconv to P. It is possible to leave one disjunct P un-cancelled. *) fun disj_cancel_cv ctxt th ct = if is_disj (Thm.term_of ct) then Conv.every_conv [Conv.arg_conv (disj_cancel_cv ctxt th), Conv.try_conv (rewr_obj_eq (th RS UtilBase.or_cancel1_th)), Conv.try_conv (rewr_obj_eq (th RS UtilBase.or_cancel2_th))] ct else Conv.all_conv ct (* Given theorem P and a disjuncion theorem, return new disjunction theorem with ~P cancelled. If all disjuncts can be cancelled, return False. *) fun disj_cancel_prop ctxt th prop = let val th' = if is_neg (prop_of' th) then th else th RS UtilBase.nn_create_th val prop' = prop |> apply_to_thm' (disj_cancel_cv ctxt th') val P = th' |> prop_of' |> dest_not in if prop_of' prop' aconv P then [th', prop'] MRS UtilBase.contra_triv_th else prop' end (* Reduce a disjunction p_1 | ... | t | ... | p_n by matching ~t with the second item. If the disjunction contains schematic variables, t must have either zero or the largest number of schematic variables. *) fun match_update_fn ctxt item1 item2 = if is_match_prem_only item1 andalso Util.has_vars (Thm.prop_of (#prop item1)) then [] else let val {id, prop, tname, ...} = item1 val thy = Proof_Context.theory_of ctxt val (disj_head, csubs) = dest_tname_of_disj tname val subs = map Thm.term_of csubs fun count_var t = length (Term.add_vars t []) val max_nvar = fold (curry Int.max) (map count_var subs) 0 fun is_priority_term t = if is_neg t then exists (is_ex orf is_bex) (strip_conj (dest_not t)) else exists (is_obj_all orf is_ball) (strip_disj t) val has_priority_term = exists is_priority_term (map get_neg subs) val (NO_MATCH, SLOW_MATCH, YES_MATCH) = (0, 1, 2) (* Test whether to perform matching on pattern. *) fun test_do_match t = let val nvar = count_var t val neg_t = get_neg t in if not (Util.is_pattern t) then NO_MATCH else if length subs > 1 andalso Property.is_property_prem thy neg_t then NO_MATCH else if has_priority_term andalso not (is_priority_term neg_t) then SLOW_MATCH else if is_mem neg_t andalso Term.is_Var (dest_arg1 neg_t) andalso null (Term.add_frees (dest_arg neg_t) []) then SLOW_MATCH else if nvar = 0 orelse nvar = max_nvar then YES_MATCH else NO_MATCH end (* Match the negation of subs[i] with th2. For each match, instantiate in prop all schematic variables in t, so that t becomes ~th2. Then remove t from prop in the instantiated version. *) fun get_matches i = let val t = nth subs i val do_match = test_do_match t fun process_inst ((id', inst), th) = let val prop' = prop |> Util.subst_thm_thy thy inst |> disj_cancel_prop ctxt th val sc = if do_match = SLOW_MATCH then 200 else 10 in disj_to_update false disj_head (id', SOME sc, prop') :: (if count_var t > 0 then [] else [ShadowItem {id = id', item = item1}]) end in if do_match = NO_MATCH then [] else t |> get_neg |> match_prop ctxt (id, item2) |> maps process_inst end fun get_matches_no_var () = let fun process_inst (id', ths) = let val prop' = prop |> fold (disj_cancel_prop ctxt) ths in disj_to_update false disj_head (id', SOME 1, prop') :: (if is_match_prem_only item1 then [] else [ShadowItem {id = id', item = item1}]) end fun get_match_at_id id' insts = insts |> filter (fn ((id, _), _) => BoxID.is_eq_ancestor ctxt id id') |> map snd |> take 1 fun get_matches_at_id all_insts id' = (id', maps (get_match_at_id id') all_insts) fun merge_matches all_insts = let val ids = distinct (op =) (maps (map (fst o fst)) all_insts) in map (get_matches_at_id all_insts) ids end val _ = assert (length subs >= 2) val ts = [hd subs, List.last subs] in ts |> map get_neg |> map (match_prop ctxt (id, item2)) |> merge_matches |> maps process_inst end in if max_nvar = 0 then get_matches_no_var () else maps get_matches (0 upto (length subs - 1)) end val match_update_prfstep = {name = "disj_match_update", args = [TypedUniv TY_DISJ, PropMatch (boolVar "A")], func = TwoStep match_update_fn} (* For DISJ items with a single term, of form f p1 ... pn, match t against each of p_i. *) fun match_one_sch_fn ctxt item1 item2 = if is_match_prem_only item1 then [] else let val {id, tname, prop = th1, ...} = item1 val thy = Proof_Context.theory_of ctxt val subs = (dest_tname_of_disj tname) |> snd |> map Thm.term_of in if length subs > 1 then [] else let val t = the_single subs val args = Util.dest_args t fun count_var t = length (Term.add_vars t []) val nvar = count_var t fun get_matches i = if count_var (nth args i) < nvar then [] else let val arg = nth args i val targ = TypedMatch (TY_TERM, arg) val insts = (ItemIO.match_arg ctxt targ item2 (id, fo_init)) |> filter (BoxID.has_incr_id o fst o fst) fun inst_to_updt ((id', inst), _) = let val th1' = Util.subst_thm_thy thy inst th1 val prop' = prop_of' th1' in if is_eq_term prop' andalso RewriteTable.is_equiv_t id' ctxt (dest_eq prop') then [] else [Update.thm_update (id', th1')] end in maps inst_to_updt insts end in maps get_matches (0 upto (length args - 1)) end end val match_one_sch_prfstep = {name = "disj_match_one_sch", args = [TypedUniv TY_DISJ, TypedUniv TY_TERM], func = TwoStep match_one_sch_fn} fun disj_match_iff_fn ctxt {id, tname, prop, ...} = if not (BoxID.has_incr_id id) then [] else let val (_, csubs) = dest_tname_of_disj tname val subs = map Thm.term_of csubs in if length subs > 1 then [] else if not (is_eq_term (the_single subs) andalso fastype_of (dest_arg (the_single subs)) = boolT) then [] else let val cv = (UtilLogic.to_obj_conv ctxt) then_conv (Trueprop_conv norm_disj) val forward = prop |> UtilLogic.equiv_forward_th |> apply_to_thm cv val backward = prop |> UtilLogic.equiv_backward_th |> apply_to_thm cv in [disj_to_update false imp (id, NONE, forward), disj_to_update false imp (id, NONE, backward)] end end val disj_match_iff_prfstep = {name = "disj_match_iff", args = [TypedUniv TY_DISJ], func = OneStep disj_match_iff_fn} (* For active case, create box checking the next case. *) fun disj_create_case_fn _ {id, tname, ...} = if not (BoxID.has_incr_id id) then [] else if exists Util.has_vars (map Thm.term_of tname) then [] else let val (disj_head, csubs) = dest_tname_of_disj tname in if not (is_active_head disj_head) then [] else if length csubs = 1 then [] else let val subs = map Thm.term_of csubs in [AddBoxes {id = id, sc = NONE, init_assum = mk_Trueprop (hd subs)}] end end val disj_create_case_prfstep = {name = "disj_create_case", args = [TypedUniv TY_DISJ], func = OneStep disj_create_case_fn} (* item1 dominates item2 if the disjunctive terms in item1 is a subset of that for item2. *) fun disj_shadow_fn ctxt (item1 as {tname = tname1, ...}) (item2 as {tname = tname2, ...}) = let val id = BoxItem.merged_id ctxt [item1, item2] val (disj_head1, subs1) = dest_tname_of_disj tname1 val (disj_head2, subs2) = dest_tname_of_disj tname2 in if not (BoxID.has_incr_id id) then [] else if not (is_active_head disj_head1) andalso is_active_head disj_head2 then [] else if is_match_prem_only item1 andalso not (is_match_prem_only item2) then [] else if subset (op aconvc) (subs1, subs2) then [ShadowItem {id = id, item = item2}] else [] end val disj_shadow_prfstep = {name = "disj_shadow", args = [TypedUniv TY_DISJ, TypedUniv TY_DISJ], func = TwoStep disj_shadow_fn} val add_disj_proofsteps = fold ItemIO.add_item_type [ (TY_DISJ, SOME disj_rewr_terms, SOME output_disj_fn, NONE) ] #> fold ItemIO.add_prop_matcher [ (TY_DISJ, disj_prop_matcher) ] #> fold add_prfstep [ match_update_prfstep, match_one_sch_prfstep, disj_match_iff_prfstep, disj_create_case_prfstep, disj_shadow_prfstep ] (* Normalizers *) fun split_not_imp_th th = th |> apply_to_thm' norm_conj_not_imp |> UtilLogic.split_conj_th (* Generalized form of splitting A & B. Also deal with cases ~(A | B) and ~(A --> B). *) fun split_conj_gen_th _ th = th |> apply_to_thm' norm_conj |> UtilLogic.split_conj_th fun eq_normalizer _ ritem = case ritem of Handler _ => [ritem] | Fact (ty_str, _, th) => if ty_str <> TY_PROP then [ritem] else if is_eq_term (prop_of' th) then let val (lhs, rhs) = dest_eq (prop_of' th) in if fastype_of lhs = boolT then map Update.thm_to_ritem (UtilLogic.split_conj_th (th RS UtilBase.iffD_th)) else [Fact (TY_EQ, [lhs, rhs], th)] end else [ritem] fun property_normalizer _ ritem = case ritem of Handler _ => [ritem] | Fact (ty_str, _, th) => if ty_str <> TY_PROP then [ritem] else if Property.is_property (prop_of' th) then [Fact (TY_PROPERTY, [prop_of' th], th)] else [ritem] fun disj_normalizer ctxt ritem = case ritem of Handler _ => [ritem] | Fact (ty_str, _, th) => if ty_str <> TY_PROP then [ritem] else let val t = prop_of' th in if is_neg t andalso is_conj (dest_not t) orelse is_disj t orelse is_imp t orelse is_obj_all t orelse is_ball t orelse is_neg t andalso is_ex (dest_not t) orelse is_neg t andalso is_bex (dest_not t) then let val (disj_head, disj_th) = analyze_disj_th ctxt th val prem_only = Auto2_State.lookup_prem_only ctxt t val disj_th = if prem_only then disj_th else snd (Normalizer.meta_use_vardefs disj_th) in disj_to_ritems prem_only disj_head disj_th end else [ritem] end fun logic_thm_update ctxt (id, th) = let val t = prop_of' th in if is_obj_all t orelse is_ball t orelse is_neg t andalso is_ex (dest_not t) orelse is_neg t andalso is_bex (dest_not t) orelse is_disj t orelse is_imp t orelse is_neg t andalso is_conj (dest_not t) then let val (disj_head, disj_th) = analyze_disj_th ctxt th val raw_items = disj_to_ritems true disj_head disj_th in AddItems {id = id, sc = NONE, raw_items = raw_items} end else Update.thm_update (id, th) end val add_disj_normalizers = Normalizer.add_th_normalizer ( "split_conj_gen", split_conj_gen_th ) #> fold Normalizer.add_normalizer [ ("eq", eq_normalizer), ("property", property_normalizer), ("disj", disj_normalizer) ] end (* structure Logic_ProofSteps. *) val _ = Theory.setup Logic_ProofSteps.add_logic_proofsteps val _ = Theory.setup Logic_ProofSteps.add_disj_proofsteps val _ = Theory.setup Logic_ProofSteps.add_disj_normalizers val TY_DISJ = Logic_ProofSteps.TY_DISJ diff --git a/thys/Auto2_HOL/matcher.ML b/thys/Auto2_HOL/matcher.ML --- a/thys/Auto2_HOL/matcher.ML +++ b/thys/Auto2_HOL/matcher.ML @@ -1,409 +1,409 @@ (* File: matcher.ML Author: Bohua Zhan Matching up to equivalence (E-matching) using a rewrite table. *) signature MATCHER = sig (* Internal *) val check_type_term: theory -> term * term -> id_inst -> (id_inst * term) option val check_type: theory -> typ * typ -> id_inst -> id_inst option val update_inst: term list -> indexname -> cterm -> id_inst -> id_inst_th list (* THe actual matching function. These are defined together. *) val match_list: Proof.context -> term list -> term list * cterm list -> id_inst -> id_inst_ths list val match_comb: Proof.context -> term list -> term * cterm -> id_inst -> id_inst_th list val match_head: Proof.context -> term list -> term * cterm -> id_inst -> id_inst_th list val match_all_head: Proof.context -> term list -> term * cterm -> id_inst -> id_inst_th list val match: Proof.context -> term list -> term * cterm -> id_inst -> id_inst_th list (* Defined in terms of match. *) val rewrite_match: Proof.context -> term * cterm -> id_inst -> id_inst_th list val rewrite_match_head: Proof.context -> term * cterm -> id_inst -> id_inst_th list val rewrite_match_list: Proof.context -> (bool * (term * cterm)) list -> id_inst -> id_inst_ths list val rewrite_match_subset: Proof.context -> term list -> term list * cterm list -> id_inst -> id_inst_ths list (* Prematching. *) val pre_match_type: Proof.context -> typ * typ -> bool val pre_match_comb: Proof.context -> term * cterm -> bool val pre_match_head': Proof.context -> term * cterm -> bool val pre_match_all_head: Proof.context -> term * cterm -> bool val pre_match: Proof.context -> term * cterm -> bool val pre_match_head: Proof.context -> term * cterm -> bool end; structure Matcher : MATCHER = struct fun compare_inst (((id1, inst1), _), ((id2, inst2), _)) = eq_list (op =) (id1, id2) andalso Util.eq_env (inst1, inst2) (* Match type at the top level for t and u. If there is no match, return NONE. Otherwise, return the updated instsp as well as t instantiated with the new type. *) fun check_type_term thy (t, u) (id, (tyinst, inst)) = let val (T, U) = (fastype_of t, fastype_of u) in if T = U then SOME ((id, (tyinst, inst)), t) else let val tyinst' = Sign.typ_match thy (T, U) tyinst val t' = Envir.subst_term_types tyinst' t in SOME ((id, (tyinst', inst)), t') end end handle Type.TYPE_MATCH => NONE (* Match two types. *) fun check_type thy (T, U) (id, (tyinst, inst)) = let val tyinst' = if T = U then tyinst else Sign.typ_match thy (T, U) tyinst in SOME (id, (tyinst', inst)) end handle Type.TYPE_MATCH => NONE (* Starting here, bd_vars is the list of free variables substituted for bound variables, when matching goes inside abstractions. *) fun is_open bd_vars u = case bd_vars of [] => false | _ => length (inter (op aconv) bd_vars (map Free (Term.add_frees u []))) > 0 (* Assign schematic variable with indexname ixn to u. Type of the schematic variable is determined by the type of u. *) fun update_inst bd_vars ixn cu (id, inst) = let val u = Thm.term_of cu in if is_open bd_vars u then [] else [((id, Util.update_env (ixn, u) inst), Thm.reflexive cu)] end (* Matching an order list of patterns against terms. *) fun match_list ctxt bd_vars (ts, cus) instsp = if null ts andalso null cus then [(instsp, [])] else if null ts orelse null cus then [] else let (* Two choices, one of which should always work (encounter no illegal higher-order patterns. *) fun hd_first () = let val insts_t = match ctxt bd_vars (hd ts, hd cus) instsp fun process_inst_t (instsp', th) = let val insts_ts' = match_list ctxt bd_vars (tl ts, tl cus) instsp' in map (apsnd (cons th)) insts_ts' end in maps process_inst_t insts_t end fun tl_first () = let val insts_ts' = match_list ctxt bd_vars (tl ts, tl cus) instsp fun process_inst_ts' (instsp', ths) = let val insts_t = match ctxt bd_vars (hd ts, hd cus) instsp' in map (apsnd (fn th => th :: ths)) insts_t end in maps process_inst_ts' insts_ts' end in hd_first () handle Fail "invalid pattern" => tl_first () end (* Match a non-AC function. *) and match_comb ctxt bd_vars (t, cu) (instsp as (_, (_, inst))) = let val (tf, targs) = Term.strip_comb t val (cuf, cuargs) = Drule.strip_comb cu val uf = Thm.term_of cuf in if Term.aconv_untyped (tf, uf) then let val instsps' = match_list ctxt bd_vars (targs, cuargs) instsp fun process_inst (instsp', ths) = (instsp', Util.comb_equiv (cuf, ths)) in map process_inst instsps' end else if is_Var tf then let val (ixn, _) = Term.dest_Var tf in case Vartab.lookup inst ixn of NONE => if subset (op aconv) (targs, bd_vars) andalso not (has_duplicates (op aconv) targs) then let val cu' = cu |> Thm.term_of |> fold Util.lambda_abstract (rev targs) |> Thm.cterm_of ctxt in map (fn (instsp', _) => (instsp', Thm.reflexive cu)) (update_inst bd_vars ixn cu' instsp) end else raise Fail "invalid pattern" | SOME (_, tf') => let val t' = Term.list_comb (tf', targs) |> Envir.beta_norm in match ctxt bd_vars (t', cu) instsp end end else [] end (* Match t and u at head. *) and match_head ctxt bd_vars (t, cu) (instsp as (_, (_, inst))) = let val u = Thm.term_of cu in if fastype_of t <> fastype_of u then [] else case (t, u) of (Var ((x, i), _), _) => (case Vartab.lookup inst (x, i) of NONE => if x = "NUMC" andalso not (Consts.is_const_ctxt ctxt u) then [] else if x = "FREE" andalso not (Term.is_Free u) then [] else update_inst bd_vars (x, i) cu instsp | SOME (_, u') => match_head ctxt bd_vars (u', cu) instsp) | (Free (a, _), Free (b, _)) => if a = b then [(instsp, Thm.reflexive cu)] else [] | (Const (a, _), Const (b, _)) => if a = b then [(instsp, Thm.reflexive cu)] else [] | (_ $ _, _) => match_comb ctxt bd_vars (t, cu) instsp | _ => [] end (* With fixed t, match with all equivalences of u. *) and match_all_head ctxt bd_vars (t, cu) (id, env) = let val u = Thm.term_of cu val u_equivs = if is_open bd_vars u then [(id, Thm.reflexive cu)] else RewriteTable.get_head_equiv_with_t ctxt (id, cu) t fun process_equiv (id', eq_u) = let val cu' = Thm.rhs_of eq_u val insts_u' = match_head ctxt bd_vars (t, cu') (id', env) fun process_inst ((id', env'), eq_th) = (* eq_th: t(env') == u', eq_u: u == u'. *) ((id', env'), Util.transitive_list [eq_th, meta_sym eq_u]) in map process_inst insts_u' end in maps process_equiv u_equivs end (* Match t and u, possibly by rewriting u at head. *) and match ctxt bd_vars (t, cu) (instsp as (_, (_, inst))) = case check_type_term (Proof_Context.theory_of ctxt) (t, Thm.term_of cu) instsp of NONE => [] | SOME (instsp', t') => case (t', Thm.term_of cu) of (Var ((x, i), _), _) => (case Vartab.lookup inst (x, i) of NONE => if member (op =) ["NUMC", "FREE"] x then match_all_head ctxt bd_vars (t', cu) instsp' else update_inst bd_vars (x, i) cu instsp' | SOME (_, u') => match ctxt bd_vars (u', cu) instsp') | (Abs (_, T, t'), Abs (x, U, _)) => ( case check_type (Proof_Context.theory_of ctxt) (T, U) instsp' of NONE => [] | SOME (instsp'' as (_, (tyinst', _))) => let - val (cv, cu') = Thm.dest_abs cu + val (cv, cu') = Thm.dest_abs_global cu val v = Thm.term_of cv val t'' = Envir.subst_term_types tyinst' t' val t_free = Term.subst_bound (v, t'') val insts' = match ctxt (v :: bd_vars) (t_free, cu') instsp'' fun process_inst (inst', th') = (inst', Thm.abstract_rule x cv th') in map process_inst insts' end) | _ => (* Free, Const, and comb case *) (match_all_head ctxt bd_vars (t', cu) instsp') |> distinct compare_inst (* Function for export *) fun rewrite_match_gen at_head ctxt (t, cu) (id, env) = if at_head then case check_type_term (Proof_Context.theory_of ctxt) (t, Thm.term_of cu) (id, env) of NONE => [] | SOME ((id, env), t) => match_head ctxt [] (t, cu) (id, env) else match ctxt [] (t, cu) (id, env) val rewrite_match = rewrite_match_gen false val rewrite_match_head = rewrite_match_gen true (* pairs is a list of (at_head, (t, u)). Match the pairs in sequence, and return a list of ((id, inst), ths), where ths is the list of equalities t(env) == u. *) fun rewrite_match_list ctxt pairs instsp = case pairs of [] => [(instsp, [])] | (at_head, (t, cu)) :: pairs' => let val insts_t = rewrite_match_gen at_head ctxt (t, cu) instsp fun process_inst_t (instsp', th) = let val insts_ts' = rewrite_match_list ctxt pairs' instsp' in map (apsnd (cons th)) insts_ts' end in maps process_inst_t insts_t end (* Given two lists of terms (ts, us), match ts with a subset of us. Return a list of ((id, inst), ths), where ths is the list of equalities t_i(env) == u_j. *) fun rewrite_match_subset ctxt bd_vars (ts, cus) instsp = case ts of [] => [(instsp, [])] | t :: ts' => let fun match_i i = map (pair i) (match ctxt bd_vars (t, nth cus i) instsp) fun process_match_i (i, (instsp', th)) = let val insts_ts' = rewrite_match_subset ctxt bd_vars (ts', nth_drop i cus) instsp' in map (apsnd (cons th)) insts_ts' end in (0 upto (length cus - 1)) |> maps match_i |> maps process_match_i end handle Fail "invalid pattern" => if length ts' > 0 andalso Term_Ord.term_ord (t, hd ts') = LESS then rewrite_match_subset ctxt bd_vars (ts' @ [t], cus) instsp else raise Fail "rewrite_match_subset: invalid pattern" (* Fast function for determining whether there can be a match between t and u. *) fun pre_match_type ctxt (T, U) = let val thy = Proof_Context.theory_of ctxt val _ = Sign.typ_match thy (T, U) Vartab.empty in true end handle Type.TYPE_MATCH => false fun pre_match_comb ctxt (t, cu) = let val (tf, targs) = Term.strip_comb t val (cuf, cuargs) = Drule.strip_comb cu val uf = Thm.term_of cuf in is_Var tf orelse (Term.aconv_untyped (tf, uf) andalso length targs = length cuargs andalso forall (pre_match ctxt) (targs ~~ cuargs)) end and pre_match_head' ctxt (t, cu) = let val u = Thm.term_of cu in case (t, u) of (Var ((x, _), T), _) => if Term.is_open u then false else if not (pre_match_type ctxt (T, fastype_of u)) then false else if x = "NUMC" then Consts.is_const_ctxt ctxt u else if x = "FREE" then Term.is_Free u else true | (Free (a, T), Free (b, U)) => (a = b andalso pre_match_type ctxt (T, U)) | (Const (a, T), Const (b, U)) => (a = b andalso pre_match_type ctxt (T, U)) | (_ $ _, _) => pre_match_comb ctxt (t, cu) | _ => false end and pre_match_all_head ctxt (t, cu) = let val thy = Proof_Context.theory_of ctxt val u = Thm.term_of cu val tyinst = Sign.typ_match thy (fastype_of t, fastype_of u) Vartab.empty val t' = Envir.subst_term_types tyinst t in if Term.is_open u then pre_match_head' ctxt (t', cu) else let val u_equivs = (RewriteTable.get_head_equiv_with_t ctxt ([], cu) t') |> map snd |> map Thm.rhs_of in exists (fn cu' => pre_match_head' ctxt (t', cu')) u_equivs end end handle Type.TYPE_MATCH => false and pre_match ctxt (t, cu) = let val u = Thm.term_of cu in case (t, u) of (Var ((x, _), T), _) => if Term.is_open u then false else if not (pre_match_type ctxt (T, fastype_of u)) then false else if member (op =) ["NUMC", "FREE"] x then pre_match_all_head ctxt (t, cu) else true | (Abs (_, T, t'), Abs (_, U, _)) => if not (pre_match_type ctxt (T, U)) then false else let - val (cv, cu') = Thm.dest_abs cu + val (cv, cu') = Thm.dest_abs_global cu val t'' = subst_bound (Thm.term_of cv, t') in pre_match ctxt (t'', cu') end | (Bound i, Bound j) => (i = j) | (_, _) => pre_match_all_head ctxt (t, cu) end fun pre_match_head ctxt (t, cu) = let val thy = Proof_Context.theory_of ctxt val u = Thm.term_of cu val tyinst = Sign.typ_match thy (fastype_of t, fastype_of u) Vartab.empty val t' = Envir.subst_term_types tyinst t in pre_match_head' ctxt (t', cu) end handle Type.TYPE_MATCH => false end (* structure Matcher. *) diff --git a/thys/Auto2_HOL/util.ML b/thys/Auto2_HOL/util.ML --- a/thys/Auto2_HOL/util.ML +++ b/thys/Auto2_HOL/util.ML @@ -1,926 +1,925 @@ (* File: util.ML Author: Bohua Zhan Utility functions. *) signature BASIC_UTIL = sig (* Exceptions *) val assert: bool -> string -> unit (* Types *) val propT: typ (* Lists *) val the_pair: 'a list -> 'a * 'a val the_triple: 'a list -> 'a * 'a * 'a val filter_split: ('a -> bool) -> 'a list -> 'a list * 'a list (* Managing matching environments. *) val fo_init: Type.tyenv * Envir.tenv val lookup_instn: Type.tyenv * Envir.tenv -> string * int -> term val lookup_inst: Type.tyenv * Envir.tenv -> string -> term (* Tracing functions. *) val trace_t: Proof.context -> string -> term -> unit val trace_tlist: Proof.context -> string -> term list -> unit val trace_thm: Proof.context -> string -> thm -> unit val trace_fullthm: Proof.context -> string -> thm -> unit val trace_thm_global: string -> thm -> unit val trace_fullthm_global: string -> thm -> unit (* Terms *) val dest_arg: term -> term val dest_arg1: term -> term (* Theorems *) val apply_to_thm: conv -> thm -> thm val meta_sym: thm -> thm val apply_to_lhs: conv -> thm -> thm val apply_to_rhs: conv -> thm -> thm end; signature UTIL = sig include BASIC_UTIL (* Lists *) val max: ('a * 'a -> order) -> 'a list -> 'a val max_partial: ('a -> 'a -> bool) -> 'a list -> 'a list val subsets: 'a list -> 'a list list val all_permutes: 'a list -> 'a list list val all_pairs: 'a list * 'b list -> ('a * 'b) list val remove_dup_lists: ('a * 'a -> order) -> 'a list * 'a list -> 'a list * 'a list val is_subseq: ('a * 'a -> bool) -> 'a list * 'a list -> bool (* Strings. *) val is_prefix_str: string -> string -> bool val is_just_internal: string -> bool (* Managing matching environments. *) val defined_instn: Type.tyenv * Envir.tenv -> string * int -> bool val lookup_tyinst: Type.tyenv * Envir.tenv -> string -> typ val update_env: indexname * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv val eq_env: (Type.tyenv * Envir.tenv) * (Type.tyenv * Envir.tenv) -> bool (* Matching. *) val first_order_match_list: theory -> (term * term) list -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv (* Printing functions, mostly from Isabelle Cookbook. *) val string_of_terms: Proof.context -> term list -> string val string_of_terms_global: theory -> term list -> string val string_of_tyenv: Proof.context -> Type.tyenv -> string val string_of_env: Proof.context -> Envir.tenv -> string val string_of_list: ('a -> string) -> 'a list -> string val string_of_list': ('a -> string) -> 'a list -> string val string_of_bool: bool -> string (* Managing context. *) val declare_free_term: term -> Proof.context -> Proof.context (* Terms. *) val is_abs: term -> bool val is_implies: term -> bool val dest_binop: term -> term * (term * term) val dest_binop_head: term -> term val dest_binop_args: term -> term * term val dest_args: term -> term list val dest_argn: int -> term -> term val get_head_name: term -> string val is_meta_eq: term -> bool val occurs_frees: term list -> term -> bool val occurs_free: term -> term -> bool val has_vars: term -> bool val is_subterm: term -> term -> bool val has_subterm: term list -> term -> bool val is_head: term -> term -> bool val lambda_abstract: term -> term -> term val is_pattern_list: term list -> bool val is_pattern: term -> bool val normalize_meta_all_imp: Proof.context -> conv val swap_meta_imp_alls: Proof.context -> conv val normalize_meta_horn: Proof.context -> conv val strip_meta_horn: term -> term list * (term list * term) val list_meta_horn: term list * (term list * term) -> term val to_internal_vars: Proof.context -> term list * term -> term list * term val rename_abs_term: term list -> term -> term val print_term_detail: Proof.context -> term -> string (* cterms. *) val dest_cargs: cterm -> cterm list val dest_binop_cargs: cterm -> cterm * cterm (* Theorems. *) val arg_backn_conv: int -> conv -> conv val argn_conv: int -> conv -> conv val comb_equiv: cterm * thm list -> thm val name_of_thm: thm -> string val update_name_of_thm: thm -> string -> thm -> thm val lhs_of: thm -> term val rhs_of: thm -> term val assume_meta_eq: theory -> term * term -> thm val assume_thm: Proof.context -> term -> thm val subst_thm_thy: theory -> Type.tyenv * Envir.tenv -> thm -> thm val subst_thm: Proof.context -> Type.tyenv * Envir.tenv -> thm -> thm val send_first_to_hyps: thm -> thm val send_all_to_hyps: thm -> thm val subst_thm_atomic: (cterm * cterm) list -> thm -> thm val subst_term_norm: Type.tyenv * Envir.tenv -> term -> term val concl_conv_n: int -> conv -> conv val concl_conv: conv -> conv val transitive_list: thm list -> thm val skip_n_conv: int -> conv -> conv val pattern_rewr_conv: term -> (term * thm) list -> conv val eq_cong_th: int -> term -> term -> Proof.context -> thm val forall_elim_sch: thm -> thm (* Conversions *) val reverse_eta_conv: Proof.context -> conv val repeat_n_conv: int -> conv -> conv (* Miscellaneous. *) val test_conv: Proof.context -> conv -> string -> string * string -> unit val term_pat_setup: theory -> theory val cterm_pat_setup: theory -> theory val type_pat_setup: theory -> theory val timer: string * (unit -> 'a) -> 'a val exn_trace: (unit -> 'a) -> 'a end; structure Util : UTIL = struct fun assert b exn_str = if b then () else raise Fail exn_str val propT = @{typ prop} fun max comp lst = let fun max2 t1 t2 = if comp (t1, t2) = LESS then t2 else t1 in case lst of [] => raise Fail "max: empty list" | l :: ls => fold max2 ls l end (* Given a function comp, remove y for each pair (x, y) such that comp x y = true (if x dominates y). *) fun max_partial comp lst = let fun helper taken remains = case remains of [] => taken | x :: xs => if exists (fn y => comp y x) taken then helper taken xs else helper (x :: filter_out (fn y => comp x y) taken) xs in helper [] lst end (* Return all subsets of lst. *) fun subsets [] = [[]] | subsets (l::ls) = let val prev = subsets ls in prev @ map (cons l) prev end (* List of all permutations of xs *) fun all_permutes xs = case xs of [] => [[]] | [x] => [[x]] | [x, y] => [[x, y], [y, x]] | _ => maps (fn i => map (cons (nth xs i)) (all_permutes (nth_drop i xs))) (0 upto (length xs - 1)) (* Convert list to pair. List must consist of exactly two items. *) fun the_pair lst = case lst of [i1, i2] => (i1, i2) | _ => raise Fail "the_pair" (* Convert list to triple. List must consist of exactly three items. *) fun the_triple lst = case lst of [i1, i2, i3] => (i1, i2, i3) | _ => raise Fail "the_triple" (* Split list into (ins, outs), where ins satisfy f, and outs don't. *) fun filter_split _ [] = ([], []) | filter_split f (x :: xs) = let val (ins, outs) = filter_split f xs in if f x then (x :: ins, outs) else (ins, x :: outs) end (* Form the Cartesian product of two lists. *) fun all_pairs (l1, l2) = maps (fn y => (map (fn x => (x, y)) l1)) l2 (* Given two sorted lists, remove all pairs of terms that appear in both lists, counting multiplicity. *) fun remove_dup_lists ord (xs, ys) = case xs of [] => ([], ys) | x :: xs' => case ys of [] => (xs, []) | y :: ys' => case ord (x, y) of LESS => apfst (cons x) (remove_dup_lists ord (xs', ys)) | EQUAL => remove_dup_lists ord (xs', ys') | GREATER => apsnd (cons y) (remove_dup_lists ord (xs, ys')) (* Whether l1 is a subsequence of l2. *) fun is_subseq eq (l1, l2) = case l1 of [] => true | x :: l1' => case l2 of [] => false | y :: l2' => if eq (x, y) then is_subseq eq (l1', l2') else is_subseq eq (l1, l2') (* Whether pre is a prefix of str. *) fun is_prefix_str pre str = is_prefix (op =) (String.explode pre) (String.explode str) (* Test whether x is followed by exactly one _. *) fun is_just_internal x = Name.is_internal x andalso not (Name.is_skolem x) val fo_init = (Vartab.empty, Vartab.empty) (* Lookup a Vartab inst with string and integer specifying indexname. *) fun defined_instn (_, inst) (str, n) = Vartab.defined inst (str, n) fun lookup_instn (_, inst) (str, n) = case Vartab.lookup inst (str, n) of NONE => raise Fail ("lookup_inst: not found " ^ str ^ (if n = 0 then "" else string_of_int n)) | SOME (_, u) => u fun lookup_inst (tyinst, inst) str = lookup_instn (tyinst, inst) (str, 0) fun lookup_tyinst (tyinst, _) str = case Vartab.lookup tyinst (str, 0) of NONE => raise Fail ("lookup_tyinst: not found " ^ str) | SOME (_, T) => T fun update_env (idx, t) (tyenv, tenv) = (tyenv, tenv |> Vartab.update_new (idx, (type_of t, t))) (* A rough comparison, simply compare the corresponding terms. *) fun eq_env ((_, inst1), (_, inst2)) = let val data1 = Vartab.dest inst1 val data2 = Vartab.dest inst2 fun compare_data (((x, i), (ty, t)), ((x', i'), (ty', t'))) = x = x' andalso i = i' andalso ty = ty' andalso t aconv t' in eq_set compare_data (data1, data2) end fun first_order_match_list thy pairs inst = case pairs of [] => inst | (t, u) :: rest => let val inst' = Pattern.first_order_match thy (t, u) inst in first_order_match_list thy rest inst' end fun string_of_terms ctxt ts = ts |> map (Syntax.pretty_term ctxt) |> Pretty.commas |> Pretty.block |> Pretty.string_of fun string_of_terms_global thy ts = ts |> map (Syntax.pretty_term_global thy) |> Pretty.commas |> Pretty.block |> Pretty.string_of fun pretty_helper aux env = env |> Vartab.dest |> map aux |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) |> Pretty.enum "," "[" "]" |> Pretty.string_of fun string_of_tyenv ctxt tyenv = let fun get_typs (v, (s, T)) = (TVar (v, s), T) val print = apply2 (Syntax.pretty_typ ctxt) in pretty_helper (print o get_typs) tyenv end fun string_of_env ctxt env = let fun get_ts (v, (T, t)) = (Var (v, T), t) val print = apply2 (Syntax.pretty_term ctxt) in pretty_helper (print o get_ts) env end fun string_of_list func lst = Pretty.str_list "[" "]" (map func lst) |> Pretty.string_of fun string_of_list' func lst = if length lst = 1 then func (the_single lst) else string_of_list func lst fun string_of_bool b = if b then "true" else "false" fun trace_t ctxt s t = tracing (s ^ " " ^ (Syntax.string_of_term ctxt t)) fun trace_tlist ctxt s ts = tracing (s ^ " " ^ (string_of_terms ctxt ts)) fun trace_thm ctxt s th = tracing (s ^ " " ^ (th |> Thm.prop_of |> Syntax.string_of_term ctxt)) fun trace_fullthm ctxt s th = tracing (s ^ " [" ^ (Thm.hyps_of th |> string_of_terms ctxt) ^ "] ==> " ^ (Thm.prop_of th |> Syntax.string_of_term ctxt)) fun trace_thm_global s th = let val thy = Thm.theory_of_thm th in tracing (s ^ " " ^ (th |> Thm.prop_of |> Syntax.string_of_term_global thy)) end fun trace_fullthm_global s th = let val thy = Thm.theory_of_thm th in tracing (s ^ " [" ^ (Thm.hyps_of th |> string_of_terms_global thy) ^ "] ==> " ^ (Thm.prop_of th |> Syntax.string_of_term_global thy)) end fun declare_free_term t ctxt = if not (is_Free t) then raise Fail "declare_free_term: t not free." else ctxt |> Variable.add_fixes_direct [t |> Term.dest_Free |> fst] |> Variable.declare_term t fun is_abs t = case t of Abs _ => true | _ => false (* Whether a given term is of the form A ==> B. *) fun is_implies t = let val _ = assert (fastype_of t = propT) "is_implies: wrong type" in case t of @{const Pure.imp} $ _ $ _ => true | _ => false end (* Extract the last two arguments on t, collecting the rest into f. *) fun dest_binop t = case t of f $ a $ b => (f, (a, b)) | _ => raise Fail "dest_binop" fun dest_binop_head t = fst (dest_binop t) fun dest_binop_args t = snd (dest_binop t) (* Return the argument of t. If t is f applied to multiple arguments, return the last argument. *) fun dest_arg t = case t of _ $ arg => arg | _ => raise Fail "dest_arg" (* Return the first of two arguments of t. *) fun dest_arg1 t = case t of _ $ arg1 $ _ => arg1 | _ => raise Fail "dest_arg1" (* Return the list of all arguments of t. *) fun dest_args t = t |> Term.strip_comb |> snd (* Return the nth argument of t, counting from left and starting at zero. *) fun dest_argn n t = nth (dest_args t) n (* Return the name of the head function. *) fun get_head_name t = case Term.head_of t of Const (nm, _) => nm | _ => raise Fail "get_head_name" (* Whether the term is of the form A == B. *) fun is_meta_eq t = let val _ = assert (fastype_of t = propT) "is_meta_eq_term: wrong type" in case t of Const (@{const_name Pure.eq}, _) $ _ $ _ => true | _ => false end (* Given free variable freevar (or a list of free variables freevars), determine whether any of the inputs appears in t. *) fun occurs_frees freevars t = inter (op aconv) (map Free (Term.add_frees t [])) freevars <> [] fun occurs_free freevar t = occurs_frees [freevar] t (* Whether the given term contains schematic variables. *) fun has_vars t = length (Term.add_vars t []) > 0 (* Whether subt is a subterm of t. *) fun is_subterm subt t = exists_subterm (fn t' => t' aconv subt) t (* Whether any of subts is a subterm of t. *) fun has_subterm subts t = exists_subterm (fn t' => member (op aconv) subts t') t (* Whether s is a head term of t. *) fun is_head s t = let val (sf, sargs) = Term.strip_comb s val (tf, targs) = Term.strip_comb t in sf aconv tf andalso is_prefix (op aconv) sargs targs end (* If stmt is P(t), return %t. P(t). *) fun lambda_abstract t stmt = Term.lambda t (Term.abstract_over (t, stmt)) (* A more general criterion for patterns. In combinations, any argument that is a pattern (in the more general sense) frees up checking for any functional schematic variables in that argument. *) fun is_pattern_list ts = let fun is_funT T = case T of Type ("fun", _) => true | _ => false fun get_fun_vars t = (Term.add_vars t []) |> filter (is_funT o snd) |> map Var fun test_list exclude_vars ts = case ts of [] => true | [t] => test_term exclude_vars t | t :: ts' => if test_term exclude_vars t then test_list (merge (op aconv) (exclude_vars, get_fun_vars t)) ts' else if test_list exclude_vars ts' then test_term (distinct (op aconv) (exclude_vars @ maps get_fun_vars ts')) t else false and test_term exclude_vars t = case t of Abs (_, _, t') => test_term exclude_vars t' | _ => let val (head, args) = strip_comb t in if is_Var head then if member (op aconv) exclude_vars head then test_list exclude_vars args else forall is_Bound args andalso not (has_duplicates (op aconv) args) else test_list exclude_vars args end in test_list [] ts end fun is_pattern t = is_pattern_list [t] (* Push !!x to the right as much as possible. *) fun normalize_meta_all_imp_once ct = Conv.try_conv ( Conv.every_conv [Conv.rewr_conv (Thm.symmetric @{thm Pure.norm_hhf_eq}), Conv.arg_conv normalize_meta_all_imp_once]) ct fun normalize_meta_all_imp ctxt ct = let val t = Thm.term_of ct in if Logic.is_all t then Conv.every_conv [Conv.binder_conv (normalize_meta_all_imp o snd) ctxt, normalize_meta_all_imp_once] ct else if is_implies t then Conv.arg_conv (normalize_meta_all_imp ctxt) ct else Conv.all_conv ct end (* Rewrite A ==> !!v_i. B to !!v_i. A ==> B. *) fun swap_meta_imp_alls ctxt ct = let val t = Thm.term_of ct in if is_implies t andalso Logic.is_all (dest_arg t) then Conv.every_conv [Conv.rewr_conv @{thm Pure.norm_hhf_eq}, Conv.binder_conv (swap_meta_imp_alls o snd) ctxt] ct else Conv.all_conv ct end (* Normalize a horn clause into standard form !!v_i. A_i ==> B. *) fun normalize_meta_horn ctxt ct = let val t = Thm.term_of ct in if Logic.is_all t then Conv.binder_conv (normalize_meta_horn o snd) ctxt ct else if is_implies t then Conv.every_conv [Conv.arg_conv (normalize_meta_horn ctxt), swap_meta_imp_alls ctxt] ct else Conv.all_conv ct end (* Deconstruct a horn clause !!v_i. A_i ==> B into (v_i, (A_i, B)). *) fun strip_meta_horn t = case t of - Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _)) => + Const (@{const_name Pure.all}, _) $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u val (vars, (assums, concl)) = strip_meta_horn body in - (var :: vars, (assums, concl)) + (Free v :: vars, (assums, concl)) end | @{const Pure.imp} $ P $ Q => let val (vars, (assums, concl)) = strip_meta_horn Q in (vars, (P :: assums, concl)) end | _ => ([], ([], t)) fun list_meta_horn (vars, (As, B)) = (Logic.list_implies (As, B)) |> fold Logic.all (rev vars) fun to_internal_vars ctxt (vars, body) = let val vars' = vars |> map Term.dest_Free |> Variable.variant_frees ctxt [] |> map (apfst Name.internal) |> map Free val subst = vars ~~ vars' in (vars', subst_atomic subst body) end fun rename_abs_term vars t = case vars of [] => t | var :: rest => let val (x, _) = Term.dest_Free var in case t of A $ Abs (_, T1, body) => A $ Abs (x, T1, rename_abs_term rest body) | _ => error "rename_abs_term" end fun print_term_detail ctxt t = case t of Const (s, ty) => "Const (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) | Free (s, ty) => "Free (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) ^ ")" | Var ((x, i), ty) => "Var ((" ^ x ^ ", " ^ (string_of_int i) ^ "), " ^ (Syntax.string_of_typ ctxt ty) ^ ")" | Bound n => "Bound " ^ (string_of_int n) | Abs (s, ty, b) => "Abs (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) ^ ", " ^ (print_term_detail ctxt b) ^ ")" | u $ v => "(" ^ print_term_detail ctxt u ^ ") $ (" ^ print_term_detail ctxt v ^ ")" (* Version for ct. *) fun dest_cargs ct = ct |> Drule.strip_comb |> snd fun dest_binop_cargs ct = (Thm.dest_arg1 ct, Thm.dest_arg ct) (* Apply cv to nth argument of t, counting from right and starting at 0. *) fun arg_backn_conv n cv ct = if n = 0 then Conv.arg_conv cv ct else Conv.fun_conv (arg_backn_conv (n-1) cv) ct (* Apply cv to nth argument of t, counting from left and starting at 0. *) fun argn_conv n cv ct = let val args_count = ct |> Thm.term_of |> dest_args |> length val _ = assert (n >= 0 andalso n < args_count) in arg_backn_conv (args_count - n - 1) cv ct end (* Given a head cterm f (function to be applied), and a list of equivalence theorems of arguments, produce an equivalent theorem for the overall term. *) fun comb_equiv (cf, arg_equivs) = Library.foldl (uncurry Thm.combination) (Thm.reflexive cf, arg_equivs) (* Retrive name of theorem. *) fun name_of_thm th = if Thm.has_name_hint th then Thm.get_name_hint th else raise Fail "name_of_thm: not found" (* Set the name of th to the name of ori_th, followed by suffix. *) fun update_name_of_thm ori_th suffix th = if Thm.has_name_hint ori_th then th |> Thm.put_name_hint (Thm.get_name_hint ori_th ^ suffix) else th val lhs_of = Thm.term_of o Thm.lhs_of val rhs_of = Thm.term_of o Thm.rhs_of fun assume_meta_eq thy (t1, t2) = Thm.assume (Thm.global_cterm_of thy (Logic.mk_equals (t1, t2))) fun assume_thm ctxt t = if type_of t <> propT then raise Fail "assume_thm: t is not of type prop" else Thm.assume (Thm.cterm_of ctxt t) (* Similar to Envir.subst_term. Apply an instantiation to a theorem. *) fun subst_thm_thy thy (tyinsts, insts) th = let fun process_tyenv (v, (S, T)) = ((v, S), Thm.global_ctyp_of thy T) val tys = map process_tyenv (Vartab.dest tyinsts) fun process_tenv (v, (T, u)) = ((v, Envir.subst_type tyinsts T), Thm.global_cterm_of thy u) val ts = map process_tenv (Vartab.dest insts) in th |> Drule.instantiate_normalize (TVars.make tys, Vars.make ts) end fun subst_thm ctxt (tyinsts, insts) th = subst_thm_thy (Proof_Context.theory_of ctxt) (tyinsts, insts) th fun send_first_to_hyps th = let val cprem = Thm.cprem_of th 1 in Thm.implies_elim th (Thm.assume cprem) end fun send_all_to_hyps th = let val _ = assert (forall (not o has_vars) (Thm.prems_of th)) "send_all_to_hyps: schematic variables in hyps." in funpow (Thm.nprems_of th) send_first_to_hyps th end (* Replace using subst the internal variables in th. This proceeds in several steps: first, pull any hypotheses of the theorem involving the replaced variables into statement of the theorem, perform the replacement (using forall_intr then forall_elim), finally return the hypotheses to their original place. *) fun subst_thm_atomic subst th = let val old_cts = map fst subst val old_ts = map Thm.term_of old_cts val new_cts = map snd subst val chyps = filter (fn ct => has_subterm old_ts (Thm.term_of ct)) (Thm.chyps_of th) in th |> fold Thm.implies_intr chyps |> fold Thm.forall_intr old_cts |> fold Thm.forall_elim (rev new_cts) |> funpow (length chyps) send_first_to_hyps end (* Substitution into terms used in auto2. Substitute types first and instantiate the types in the table of term instantiations. Also perform beta_norm at the end. *) fun subst_term_norm (tyinsts, insts) t = let fun inst_tenv tenv = tenv |> Vartab.dest |> map (fn (ixn, (T, v)) => (ixn, (Envir.subst_type tyinsts T, v))) |> Vartab.make in t |> Envir.subst_term_types tyinsts |> Envir.subst_term (tyinsts, inst_tenv insts) |> Envir.beta_norm end (* Apply the conversion cv to the statement of th, yielding the equivalent theorem. *) fun apply_to_thm cv th = let val eq = cv (Thm.cprop_of th) in if Thm.is_reflexive eq then th else Thm.equal_elim eq th end (* Given th of form A == B, get th' of form B == A. *) val meta_sym = Thm.symmetric (* Apply conv to rewrite the left hand side of th. *) fun apply_to_lhs cv th = let val eq = cv (Thm.lhs_of th) in if Thm.is_reflexive eq then th else Thm.transitive (meta_sym eq) th end (* Apply conv to rewrite the right hand side of th. *) fun apply_to_rhs cv th = let val eq = cv (Thm.rhs_of th) in if Thm.is_reflexive eq then th else Thm.transitive th eq end (* Using cv, rewrite the part of ct after stripping i premises. *) fun concl_conv_n i cv ct = if i = 0 then cv ct else (Conv.arg_conv (concl_conv_n (i-1) cv)) ct (* Rewrite part of ct after stripping all premises. *) fun concl_conv cv ct = case Thm.term_of ct of @{const Pure.imp} $ _ $ _ => Conv.arg_conv (concl_conv cv) ct | _ => cv ct (* Given a list of theorems A = B, B = C, etc., apply Thm.transitive to get equality between start and end. *) fun transitive_list ths = let fun rev_transitive btoc atob = let val (b, c) = btoc |> Thm.cprop_of |> Thm.dest_equals val (a, b') = atob |> Thm.cprop_of |> Thm.dest_equals in if b aconvc b' then if a aconvc b then btoc else if b aconvc c then atob else Thm.transitive atob btoc else let val _ = map (trace_thm_global "ths:") ths in raise Fail "transitive_list: intermediate does not agree" end end in fold rev_transitive (tl ths) (hd ths) end (* Skip to argument n times. For example, if applied to rewrite a proposition in implication form (==> or -->), it will skip the first n assumptions. *) fun skip_n_conv n cv = if n <= 0 then cv else Conv.arg_conv (skip_n_conv (n-1) cv) (* Given a term t, and pairs (a_i, eq_i), where a_i's are atomic subterms of t. Suppose the input is obtained by replacing each a_i by the left side of eq_i in t, obtain equality from t to the term obtained by replacing each a_i by the right side of eq_i in t. *) fun pattern_rewr_conv t eq_ths ct = case t of Bound _ => raise Fail "pattern_rewr_conv: bound variable." | Abs _ => raise Fail "pattern_rewr_conv: abs not supported." | _ $ _ => let val (f, arg) = Term.strip_comb t val (f', arg') = Drule.strip_comb ct val _ = assert (f aconv Thm.term_of f') "pattern_rewr_conv: input does not match pattern." val ths = map (fn (t, ct) => pattern_rewr_conv t eq_ths ct) (arg ~~ arg') in comb_equiv (f', ths) end | Const _ => let val _ = assert (t aconv Thm.term_of ct) "pattern_rewr_conv: input does not match pattern." in Conv.all_conv ct end | _ => (* Free and Var cases *) (case AList.lookup (op aconv) eq_ths t of NONE => Conv.all_conv ct | SOME eq_th => let val _ = assert (lhs_of eq_th aconv (Thm.term_of ct)) "pattern_rewr_conv: wrong substitution." in eq_th end) (* Given integer i, term b_i, and a term A = f(a_1, ..., a_n), produce the theorem a_i = b_i ==> A = f(a_1, ..., b_i, ..., a_n). *) fun eq_cong_th i bi A ctxt = let val thy = Proof_Context.theory_of ctxt val (cf, cargs) = Drule.strip_comb (Thm.cterm_of ctxt A) val _ = assert (i < length cargs) "eq_cong_th: i out of bounds." val ai = Thm.term_of (nth cargs i) val eq_i = assume_meta_eq thy (ai, bi) val eqs = map Thm.reflexive (take i cargs) @ [eq_i] @ map Thm.reflexive (drop (i + 1) cargs) val eq_A = comb_equiv (cf, eqs) in Thm.implies_intr (Thm.cprop_of eq_i) eq_A end (* Convert theorems of form !!x y. P x y into P ?x ?y (arbitrary number of quantifiers). *) fun forall_elim_sch th = case Thm.prop_of th of Const (@{const_name Pure.all}, _) $ Abs (x, T, _) => let val var_xs = map fst (Term.add_var_names (Thm.prop_of th) []) val x' = if member (op =) var_xs x then singleton (Name.variant_list var_xs) x else x val thy = Thm.theory_of_thm th in th |> Thm.forall_elim (Thm.global_cterm_of thy (Var ((x', 0), T))) |> forall_elim_sch end | _ => th (* Given P of function type, produce P == %x. P x. *) fun reverse_eta_conv ctxt ct = let val t = Thm.term_of ct val argT = Term.domain_type (fastype_of t) handle Match => raise CTERM ("reverse_eta_conv", [ct]) val rhs = Abs ("x", argT, t $ Bound 0) val eq_th = Thm.eta_conversion (Thm.cterm_of ctxt rhs) in meta_sym eq_th end (* Repeat cv exactly n times. *) fun repeat_n_conv n cv t = if n = 0 then Conv.all_conv t else (cv then_conv (repeat_n_conv (n-1) cv)) t (* Generic function for testing a conv. *) fun test_conv ctxt cv err_str (str1, str2) = let val (t1, t2) = (Proof_Context.read_term_pattern ctxt str1, Proof_Context.read_term_pattern ctxt str2) val th = cv (Thm.cterm_of ctxt t1) in if t1 aconv (lhs_of th) andalso t2 aconv (rhs_of th) then () else let val _ = trace_t ctxt "Input:" t1 val _ = trace_t ctxt "Expected:" t2 val _ = trace_t ctxt "Actual:" (Thm.prop_of th) in raise Fail err_str end end (* term_pat and typ_pat, from Isabelle Cookbook. *) val term_pat_setup = let val parser = Args.context -- Scan.lift Args.embedded_inner_syntax fun term_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt |> ML_Syntax.print_term |> ML_Syntax.atomic in ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat) end val cterm_pat_setup = let val parser = Args.context -- Scan.lift Args.embedded_inner_syntax fun cterm_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt |> ML_Syntax.print_term |> ML_Syntax.atomic |> prefix "Thm.cterm_of ML_context" in ML_Antiquotation.value @{binding "cterm_pat"} (parser >> cterm_pat) end val type_pat_setup = let val parser = Args.context -- Scan.lift Args.embedded_inner_syntax fun typ_pat (ctxt, str) = let val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt in str |> Syntax.read_typ ctxt' |> ML_Syntax.print_typ |> ML_Syntax.atomic end in ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat) end (* Time the given function f : unit -> 'a. *) fun timer (msg, f) = let val t_start = Timing.start () val res = f () val t_end = Timing.result t_start in (writeln (msg ^ (Timing.message t_end)); res) end (* When exception is shown when running function f : unit -> 'a, print stack trace. *) fun exn_trace f = Runtime.exn_trace f end (* structure Util. *) structure Basic_Util: BASIC_UTIL = Util open Basic_Util val _ = Theory.setup (Util.term_pat_setup) val _ = Theory.setup (Util.cterm_pat_setup) val _ = Theory.setup (Util.type_pat_setup) diff --git a/thys/Auto2_HOL/util_logic.ML b/thys/Auto2_HOL/util_logic.ML --- a/thys/Auto2_HOL/util_logic.ML +++ b/thys/Auto2_HOL/util_logic.ML @@ -1,630 +1,628 @@ (* File: util_logic.ML Author: Bohua Zhan Utility functions, after fixing object logic. *) signature BASIC_UTIL_LOGIC = sig (* Terms *) val Trueprop: term val is_Trueprop: term -> bool val mk_Trueprop: term -> term val dest_Trueprop: term -> term val Trueprop_conv: conv -> conv val pFalse: term val Not: term val mk_not: term -> term val dest_not: term -> term val is_neg: term -> bool val get_neg: term -> term val get_neg': term -> term val conj: term val is_conj: term -> bool val mk_conj: term * term -> term val strip_conj: term -> term list val list_conj: term list -> term val disj: term val is_disj: term -> bool val mk_disj: term * term -> term val strip_disj: term -> term list val list_disj: term list -> term val imp: term val is_imp: term -> bool val mk_imp: term * term -> term val dest_imp: term -> term * term val strip_obj_imp: term -> term list * term val list_obj_imp: term list * term -> term val is_obj_all: term -> bool val is_ball: term -> bool val mk_obj_all: term -> term -> term val is_ex: term -> bool val is_bex: term -> bool val mk_exists: term -> term -> term val is_mem: term -> bool val mk_mem: term * term -> term (* Theorems *) val is_true_th: thm -> bool val prop_of': thm -> term val cprop_of': thm -> cterm val concl_of': thm -> term val make_trueprop_eq: thm -> thm val assume_eq: theory -> term * term -> thm val apply_to_thm': conv -> thm -> thm val to_meta_eq: thm -> thm val to_obj_eq: thm -> thm val obj_sym: thm -> thm val rewr_obj_eq: thm -> conv val conj_left_th: thm -> thm val conj_right_th: thm -> thm val equiv_forward_th: thm -> thm val equiv_backward_th: thm -> thm val inv_backward_th: thm -> thm val to_obj_eq_th: thm -> thm val to_obj_eq_iff_th: thm -> thm val obj_sym_th: thm -> thm end; signature UTIL_LOGIC = sig include BASIC_UTIL_LOGIC (* Terms *) val term_of_bool: bool -> term val bool_of_term: term -> bool (* Finding subterms *) val list_subterms: term -> term list val get_all_subterms: term -> term list val get_all_subterms_skip_if: term -> term list (* cterms *) val get_cneg: cterm -> cterm (* Theorems *) val make_neg_eq: thm -> thm val rewrite_to_contra_form: conv val rewrite_from_contra_form: conv val to_obj_conv: Proof.context -> conv val to_obj_conv_on_horn: Proof.context -> conv val to_meta_conv: Proof.context -> conv val split_conj_th: thm -> thm list val split_conj_gen_th: thm -> thm list val split_not_disj_th: thm -> thm list val strip_horn': thm -> term list * term val mk_conjs_th: thm list -> thm val ex_elim: Proof.context -> term -> thm -> thm val force_abs_form: term -> term val strip_obj_horn: term -> term list * (term list * term) val list_obj_horn: term list * (term list * term) -> term val is_ex_form_gen: term -> bool val normalize_exists: Proof.context -> conv val strip_exists: term -> term list * term (* Wrapper around common tactics. *) val prove_by_tac: (Proof.context -> int -> tactic) -> Proof.context -> thm list -> term -> thm val contra_by_tac: (Proof.context -> int -> tactic) -> Proof.context -> thm list -> thm end; structure UtilLogic : UTIL_LOGIC = struct (* Booleans *) fun term_of_bool b = (if b then bTrue else bFalse) fun bool_of_term t = if t aconv bTrue then true else if t aconv bFalse then false else raise Fail "bool_of_term: unexpected t." (* Trueprop *) val Trueprop = Const (UtilBase.Trueprop_name, boolT --> propT) (* Returns whether the given term is Trueprop. *) fun is_Trueprop t = let val _ = assert (fastype_of t = propT) "is_Trueprop: wrong type" in case t of Const (c, _) $ _ => c = UtilBase.Trueprop_name | _ => false end fun mk_Trueprop P = Trueprop $ P fun dest_Trueprop t = if is_Trueprop t then dest_arg t else raise Fail "dest_Trueprop" fun Trueprop_conv cv ct = if is_Trueprop (Thm.term_of ct) then Conv.arg_conv cv ct else raise CTERM ("Trueprop_conv", [ct]) val pFalse = Trueprop $ bFalse (* Not *) val Not = Const (UtilBase.Not_name, boolT --> boolT) fun mk_not P = Not $ P (* Returns whether the given term is in neg form. *) fun is_neg t = let val _ = assert (fastype_of t = boolT) "is_neg: wrong type" in case t of Const (c, _) $ _ => c = UtilBase.Not_name | _ => false end fun dest_not t = if is_neg t then dest_arg t else raise Fail "dest_not" (* Returns the negation of the given term. Avoids double negatives. *) fun get_neg t = if is_neg t then dest_not t else Not $ t (* Version of get_neg for Trueprop terms. *) fun get_neg' t = let val _ = assert (is_Trueprop t) "get_neg': input should be a Trueprop." in t |> dest_Trueprop |> get_neg |> mk_Trueprop end (* Conjunction and disjunction *) val conj = Const (UtilBase.Conj_name, boolT --> boolT --> boolT) fun is_conj t = case t of Const (c, _) $ _ $ _ => c = UtilBase.Conj_name | _ => false fun mk_conj (t, u) = conj $ t $ u fun strip_conj t = if is_conj t then (dest_arg1 t) :: strip_conj (dest_arg t) else [t] fun list_conj ts = case ts of [] => error "list_conj" | [t] => t | t :: rest => mk_conj (t, list_conj rest) val disj = Const (UtilBase.Disj_name, boolT --> boolT --> boolT) fun is_disj t = case t of Const (c, _) $ _ $ _ => c = UtilBase.Disj_name | _ => false fun mk_disj (t, u) = disj $ t $ u fun strip_disj t = if is_disj t then (dest_arg1 t) :: strip_disj (dest_arg t) else [t] fun list_disj ts = case ts of [] => raise Fail "list_disj" | [t] => t | t :: ts' => mk_disj (t, list_disj ts') (* Object implication *) val imp = Const (UtilBase.Imp_name, boolT --> boolT --> boolT) fun is_imp t = case t of Const (c, _) $ _ $ _ => c = UtilBase.Imp_name | _ => false fun mk_imp (t, u) = imp $ t $ u fun dest_imp t = if is_imp t then (dest_arg1 t, dest_arg t) else raise Fail "dest_imp" (* Given t of form A1 --> ... --> An, return ([A1, ..., A(n-1)], An). *) fun strip_obj_imp t = if is_imp t then let val (As, B') = strip_obj_imp (dest_arg t) in (dest_arg1 t :: As, B') end else ([], t) fun list_obj_imp (As, C) = case As of [] => C | A :: rest => mk_imp (A, list_obj_imp (rest, C)) fun is_obj_all t = case t of Const (c, _) $ Abs _ => c = UtilBase.All_name | _ => false fun is_ball t = case t of Const (c, _) $ _ $ _ => c = UtilBase.Ball_name | _ => false fun mk_obj_all t body = let val (x, T) = Term.dest_Free t in Const (UtilBase.All_name, (T --> boolT) --> boolT) $ Term.absfree (x, T) body end fun is_ex t = case t of Const (c, _) $ Abs _ => c = UtilBase.Ex_name | _ => false fun is_bex t = case t of Const (c, _) $ _ $ _ => c = UtilBase.Bex_name | _ => false fun mk_exists t body = let val (x, T) = Term.dest_Free t in Const (UtilBase.Ex_name, (T --> boolT) --> boolT) $ Term.absfree (x, T) body end fun is_mem t = case t of Const (c, _) $ _ $ _ => c = UtilBase.Mem_name | _ => false fun mk_mem (x, A) = let val T = fastype_of x in Const (UtilBase.Mem_name, T --> UtilBase.mk_setT T --> boolT) $ x $ A end (* Finding subterms *) (* Get all subterms of t. *) fun list_subterms t = let fun dest_at_head t = case t of Abs (_, _, body) => dest_at_head body | _ => if Term.is_open t then t |> Term.strip_comb |> snd |> maps dest_at_head else [t] and dest t = case t of Abs _ => dest_at_head t | _ $ _ => t |> Term.strip_comb |> snd | _ => [] in dest t end (* List all (closed) subterms. Larger ones will be listed first. *) fun get_all_subterms t = t |> list_subterms |> maps get_all_subterms |> distinct (op aconv) |> cons t (* List all (closed) subterms. For terms of form if cond then yes or no, list only subterms of cond. *) fun get_all_subterms_skip_if t = if UtilBase.is_if t then t |> Util.dest_args |> hd |> get_all_subterms_skip_if |> cons t else t |> list_subterms |> maps get_all_subterms_skip_if |> distinct (op aconv) |> cons t (* cterms *) fun get_cneg ct = let val t = Thm.term_of ct val _ = assert (fastype_of t = boolT) "get_neg: wrong type" in if is_neg t then Thm.dest_arg ct else Thm.apply UtilBase.cNot ct end (* Theorems *) fun is_true_th th = Thm.eq_thm_prop (th, true_th) fun prop_of' th = dest_Trueprop (Thm.prop_of th) fun cprop_of' th = Thm.dest_arg (Thm.cprop_of th) fun concl_of' th = dest_Trueprop (Thm.concl_of th) (* Given an equality between bools, make it an equality between props, by applying the function Trueprop to both sides. *) fun make_trueprop_eq th = Thm.combination (Thm.reflexive UtilBase.cTrueprop) th (* Assumed theorems. *) fun assume_eq thy (t1, t2) = Thm.assume (Thm.global_cterm_of thy (mk_Trueprop (mk_eq (t1, t2)))) (* Apply cv to the statement of th, skipping Trueprop. *) fun apply_to_thm' cv th = apply_to_thm (Trueprop_conv cv) th val to_meta_eq = apply_to_thm (Util.concl_conv UtilBase.to_meta_eq_cv) val to_obj_eq = apply_to_thm (Util.concl_conv UtilBase.to_obj_eq_cv) val obj_sym = apply_to_thm (Util.concl_conv UtilBase.obj_sym_cv) (* Obtain rewriting conv from obj equality. *) fun rewr_obj_eq eq_th = Conv.rewr_conv (to_meta_eq eq_th) (* Given an equality A == B, make the equality ~A == ~B. Cancel ~~ on both sides if exists. *) fun make_neg_eq th = th |> Thm.combination (Thm.reflexive UtilBase.cNot) |> apply_to_lhs (Conv.try_conv (rewr_obj_eq UtilBase.nn_cancel_th)) |> apply_to_rhs (Conv.try_conv (rewr_obj_eq UtilBase.nn_cancel_th)) (* If ct is of the form [...] ==> False, leave it unchanged. Otherwise, change [...] ==> B to [..., ~ B] ==> False and change [...] ==> ~ B to [..., B] ==> False. *) fun rewrite_to_contra_form ct = let val (_, concl) = Logic.strip_horn (Thm.term_of ct) val concl' = dest_Trueprop concl in if concl' aconv bFalse then Conv.all_conv ct else if is_neg concl' then Util.concl_conv (Conv.rewr_conv UtilBase.to_contra_form_th') ct else Util.concl_conv (Conv.rewr_conv UtilBase.to_contra_form_th) ct end (* Rewrite ct from [...] ==> A ==> False to [...] ==> ~ A and from [...] ==> ~ A ==> False to [...] ==> A. *) fun rewrite_from_contra_form ct = let val (prems, concl) = Logic.strip_horn (Thm.term_of ct) val _ = assert (concl aconv pFalse) "rewrite_from_contra_form: concl should be false." val num_prems = length prems val last_prem' = dest_Trueprop (nth prems (num_prems-1)) val to_contra_form = if is_neg last_prem' then UtilBase.to_contra_form_th else UtilBase.to_contra_form_th' in Util.concl_conv_n (num_prems-1) (Conv.rewr_conv (meta_sym to_contra_form)) ct end (* Converts ==> to --> and !! to !. *) fun to_obj_conv ctxt ct = case Thm.term_of ct of @{const Pure.imp} $ _ $ _ => Conv.every_conv [Conv.binop_conv (to_obj_conv ctxt), Conv.rewr_conv UtilBase.atomize_imp_th] ct | Const (@{const_name Pure.all}, _) $ Abs _ => Conv.every_conv [Conv.binder_conv (to_obj_conv o snd) ctxt, Conv.rewr_conv UtilBase.atomize_all_th] ct | _ => Conv.all_conv ct (* When ct is of form A1 ==> ... ==> An, apply to_obj_conv to each Ai. *) fun to_obj_conv_on_horn ctxt ct = case Thm.term_of ct of @{const Pure.imp} $ _ $ _ => Conv.every_conv [Conv.arg1_conv (to_obj_conv ctxt), Conv.arg_conv (to_obj_conv_on_horn ctxt)] ct | Const (@{const_name Pure.all}, _) $ Abs _ => Conv.binder_conv (to_obj_conv_on_horn o snd) ctxt ct | _ => Conv.all_conv ct (* Convert !! and ==> on the outermost level. Pull all !! to the front. *) fun to_meta_conv ctxt ct = let val t = Thm.term_of ct in if is_Trueprop t andalso is_obj_all (dest_Trueprop t) then Conv.every_conv [Conv.rewr_conv (meta_sym UtilBase.atomize_all_th), to_meta_conv ctxt] ct else if is_Trueprop t andalso is_ball (dest_Trueprop t) then Conv.every_conv [Conv.arg_conv (rewr_obj_eq UtilBase.Ball_def_th), to_meta_conv ctxt] ct else if is_Trueprop t andalso is_imp (dest_Trueprop t) then Conv.every_conv [Conv.rewr_conv (meta_sym UtilBase.atomize_imp_th), to_meta_conv ctxt] ct else if Logic.is_all t then Conv.binder_conv (to_meta_conv o snd) ctxt ct else if Util.is_implies t then Conv.every_conv [Conv.arg_conv (to_meta_conv ctxt), Util.swap_meta_imp_alls ctxt] ct else Conv.all_conv ct end (* Modify th using imp_th, and add postfix to name (if available). *) fun thm_RS_mod imp_th suffix th = (th RS imp_th) |> Drule.zero_var_indexes |> Util.update_name_of_thm th suffix (* From A & B, obtain A. *) val conj_left_th = thm_RS_mod UtilBase.conjunct1_th "@left" (* From A & B, obtain B. *) val conj_right_th = thm_RS_mod UtilBase.conjunct2_th "@right" (* From (A::bool) = B, obtain A ==> B. *) val equiv_forward_th = thm_RS_mod UtilBase.iffD1_th "@eqforward" (* From (A::bool) = B, obtain B ==> A. *) val equiv_backward_th = thm_RS_mod UtilBase.iffD2_th "@eqbackward" (* From (A::bool) = B, obtain ~A ==> ~B. *) val inv_backward_th = thm_RS_mod UtilBase.inv_back_th "@invbackward" (* Same as to_obj_eq, except keeping names and indices. *) fun to_obj_eq_th th = th |> to_obj_eq |> Util.update_name_of_thm th "@obj_eq" (* Same as to_obj_eq_iff, except keeping names and indices. *) fun to_obj_eq_iff_th th = th |> UtilBase.to_obj_eq_iff |> Util.update_name_of_thm th "@iff" (* Same as obj_sym, except keeping names and indices. *) fun obj_sym_th th = th |> obj_sym |> Util.update_name_of_thm th "@sym" (* Given th of form (P ==>) A1 & ... & An, return theorems (P ==>) A1, ..., (P ==>) An, where there can be zero or more premises in front. *) fun split_conj_th th = if is_conj (prop_of' th) then (th RS UtilBase.conjunct1_th) :: (split_conj_th (th RS UtilBase.conjunct2_th)) else [th] (* More general form. *) fun split_conj_gen_th th = if is_conj (prop_of' th) then maps split_conj_gen_th [th RS UtilBase.conjunct1_th, th RS UtilBase.conjunct2_th] else [th] (* Given th of form ~ (A1 | ... | An), return theorems ~ A1, ... ~ An. *) fun split_not_disj_th th = let val t = prop_of' th in if is_neg t andalso is_disj (dest_not t) then (th RS UtilBase.or_intro1_th) :: (split_not_disj_th (th RS UtilBase.or_intro2_th)) else [th] end (* Similar to Logic.strip_horn, except remove Trueprop. *) fun strip_horn' th = (Logic.strip_horn (Thm.prop_of th)) |> apfst (map dest_Trueprop) |> apsnd dest_Trueprop fun mk_conjs_th ths = case ths of [] => raise Fail "mk_conjs_th" | [th] => th | th :: rest => [th, mk_conjs_th rest] MRS UtilBase.conjI_th (* Given th of form P x ==> False, where x is the given free variable, obtain new theorem of form (EX x. P x) ==> False. The function is written so it can be applied to multiple variables with fold. For example, "fold (ex_elim ctxt) [x, y] (P x y ==> False) will give (EX y x. P x y) ==> False. *) fun ex_elim ctxt freevar th = let val thy = Proof_Context.theory_of ctxt val th' = th |> Thm.forall_intr (Thm.cterm_of ctxt freevar) val head_prem = hd (Thm.prems_of UtilBase.exE_th') val inst = Pattern.match thy (head_prem, Thm.prop_of th') fo_init val exE_inst = Util.subst_thm ctxt inst UtilBase.exE_th' in Thm.elim_implies th' exE_inst end fun force_abs_form t = case t of Abs _ => t | _ => Abs ("x", domain_type (fastype_of t), t $ Bound 0) (* Normalization of object forall expressions in horn-clause form. *) fun strip_obj_horn t = if is_obj_all t then case t of - _ $ Abs (abs as (_, T, _)) => + _ $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u val (vars, (assum, concl)) = strip_obj_horn body in - (var :: vars, (assum, concl)) + (Free v :: vars, (assum, concl)) end | f $ arg => strip_obj_horn (f $ force_abs_form arg) | _ => raise Fail "strip_obj_horn" else if is_ball t then case t of - _ $ S $ Abs (abs as (_, T, _)) => + _ $ S $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u + val var = Free v val mem = mk_mem (var, S) val (vars, (assum, concl)) = strip_obj_horn body in (var :: vars, (mem :: assum, concl)) end | f $ S $ arg => strip_obj_horn (f $ S $ force_abs_form arg) | _ => raise Fail "strip_obj_horn" else if is_imp t then let val (vars, (assum, concl)) = strip_obj_horn (dest_arg t) in (vars, (dest_arg1 t :: assum, concl)) end else ([], ([], t)) fun list_obj_horn (vars, (As, B)) = (list_obj_imp (As, B)) |> fold mk_obj_all (rev vars) (* Whether t can be immediately rewritten into EX form. *) fun is_ex_form_gen t = is_ex t orelse is_bex t orelse (is_neg t andalso is_obj_all (dest_not t)) orelse (is_neg t andalso is_ball (dest_not t)) orelse (is_conj t andalso is_ex_form_gen (dest_arg t)) (* Rewrite A & EX v_i. B to EX v_i. A & B. *) fun swap_conj_exists ctxt ct = let val t = Thm.term_of ct in if is_conj t andalso is_ex (dest_arg t) then Conv.every_conv [rewr_obj_eq UtilBase.swap_ex_conj_th, Conv.binder_conv (swap_conj_exists o snd) ctxt] ct else Conv.all_conv ct end (* Normalize existence statement into EX v_i. A_1 & ... & A_n. This includes moving as many existence quantifiers to the left as possible. *) fun normalize_exists ctxt ct = let val t = Thm.term_of ct in if is_ex t then Conv.binder_conv (normalize_exists o snd) ctxt ct else if is_bex t then Conv.every_conv [rewr_obj_eq UtilBase.Bex_def_th, normalize_exists ctxt] ct else if is_neg t andalso is_obj_all (dest_not t) then Conv.every_conv [rewr_obj_eq UtilBase.not_all_th, normalize_exists ctxt] ct else if is_neg t andalso is_ball (dest_not t) then Conv.every_conv [Conv.arg_conv (rewr_obj_eq UtilBase.Ball_def_th), rewr_obj_eq UtilBase.not_all_th, Conv.binder_conv (K (rewr_obj_eq UtilBase.not_imp_th)) ctxt, normalize_exists ctxt] ct else if is_conj t then Conv.every_conv [Conv.arg_conv (normalize_exists ctxt), swap_conj_exists ctxt] ct else Conv.all_conv ct end (* Assume t is in normal form. *) fun strip_exists t = if is_ex t then case t of - _ $ Abs (abs as (_, T, _)) => + _ $ (u as Abs _) => let - val (x, body) = Term.dest_abs abs - val var = Free (x, T) + val (v, body) = Term.dest_abs_global u val (vars, body') = strip_exists body in - (var :: vars, body') + (Free v :: vars, body') end | _ => raise Fail "strip_exists" else ([], t) (* Generic wrapper function. tac can be arith_tac, simp_tac, etc. *) fun prove_by_tac tac ctxt ths goal = let val goal' = Logic.list_implies (map Thm.prop_of ths, mk_Trueprop goal) in ths MRS (Goal.prove ctxt [] [] goal' (HEADGOAL o tac o #context)) end fun contra_by_tac tac ctxt ths = prove_by_tac tac ctxt ths bFalse end (* structure UtilLogic *) structure Basic_UtilLogic: BASIC_UTIL_LOGIC = UtilLogic open Basic_UtilLogic diff --git a/thys/Complx/OG_Syntax.thy b/thys/Complx/OG_Syntax.thy --- a/thys/Complx/OG_Syntax.thy +++ b/thys/Complx/OG_Syntax.thy @@ -1,420 +1,420 @@ (* * Copyright 2016, Data61, CSIRO * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(DATA61_BSD) *) section \Shallowly-embedded syntax for COMPLX programs\ theory OG_Syntax imports OG_Hoare OG_Tactics begin datatype ('s, 'p, 'f) ann_com = AnnCom "('s, 'p, 'f) ann" "('s,'p,'f) com" fun ann where "ann (AnnCom p q) = p" fun com where "com (AnnCom p q) = q" lemmas ann.simps[oghoare_simps] com.simps[oghoare_simps] syntax "_quote" :: "'b \ ('a \ 'b)" ("(\_\)" [0] 1000) "_antiquote" :: "('a \ 'b) \ 'b" ("\_" [1000] 1000) "_Assert" :: "'a \ 'a set" ("(\_\)" [0] 1000) translations "\b\" \ "CONST Collect \b\" parse_translation \ let fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t | quote_tr ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_quote"}, K quote_tr)] end \ syntax "_fst" :: "'a \ 'b \ 'a" ("_\<^sub>," [60] 61) "_snd" :: "'a \ 'b \ 'b" ("_\<^sub>." [60] 61) parse_translation \ let fun fst_tr ((Const (@{const_syntax Pair}, _) $ p $ c) :: ts) = p; fun snd_tr ((Const (@{const_syntax Pair}, _) $ p $ c) :: ts) = c; in [(@{syntax_const "_fst"}, K fst_tr), (@{syntax_const "_snd"}, K snd_tr)] end \ text\Syntax for commands and for assertions and boolean expressions in commands \com\ and annotated commands \ann_com\.\ syntax "_Annotation" :: "('s,'p,'f) ann_com \ ('s, 'p, 'f) ann" ("_\<^sub>?" [60] 61) "_Command" :: "('s,'p,'f) ann_com \ ('s,'p,'f) com" ("_\<^sub>!" [60] 61) parse_translation \ let fun ann_tr ((Const (@{const_syntax AnnCom}, _) $ p $ c) :: ts) = p | ann_tr (p :: ts) = Const (@{const_syntax ann}, dummyT) $ p | ann_tr x = raise TERM ("ann_tr", x); fun com_tr ((Const (@{const_syntax AnnCom}, _) $ p $ c) :: ts) = c | com_tr (c :: ts) = Const (@{const_syntax com}, dummyT) $ c | com_tr x = raise TERM ("com_tr", x); in [(@{syntax_const "_Annotation"}, K ann_tr), (@{syntax_const "_Command"}, K com_tr)] end \ syntax "_Seq" :: "('s,'p,'f) ann_com \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_,,/ _)" [55, 56] 55) "_AnnSeq" :: "('s,'p,'f) ann_com \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_;;//_)" [55, 56] 55) translations "_Seq c1 c2" \ "CONST AnnCom (CONST AnnComp (c1\<^sub>?) (c2\<^sub>?)) (CONST Seq (c1\<^sub>!) (c2\<^sub>!))" "_AnnSeq c1 c2" \ "CONST AnnCom (CONST AnnComp (c1\<^sub>?) (c2\<^sub>?)) (CONST Seq (c1\<^sub>!) (c2\<^sub>!))" syntax "_Assign" :: "idt \ 'b \ ('s,'p,'f) ann_com" ("(\_ :=/ _)" [70, 65] 61) "_AnnAssign" :: "'s assn \ idt \ 'b \ ('s,'p,'f) ann_com" ("(_//\_ :=/ _)" [90,70,65] 61) definition "FAKE_ANN \ UNIV" translations "r \x := a" \ "CONST AnnCom (CONST AnnExpr r) (CONST Basic \\(_update_name x (\_. a))\)" "\x := a" \ "CONST FAKE_ANN \x := a" abbreviation "update_var f S s \ (\v. f (\_. v) s) ` S" abbreviation "fun_to_rel f \ \ ((\s. (\v. (s, v)) ` f s) ` UNIV)" syntax "_Spec" :: "idt \ 'b \ ('s,'p,'f) ann_com" ("(\_ :\/ _)" [70, 65] 61) "_AnnSpec" :: "'a assn \ idt \ 'b \ ('s,'p,'f) ann_com" ("(_//\_ :\/ _)" [90,70,65] 61) translations "r \x :\ S" \ "CONST AnnCom (CONST AnnExpr r) (CONST Spec (CONST fun_to_rel \\(CONST update_var (_update_name x) S)\))" "\x :\ S" \ "CONST FAKE_ANN \x :\ S" nonterminal grds and grd syntax "_AnnCond1" :: "'s assn \ 's bexp \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_//IF _//(2THEN/ (_))//(2ELSE/ (_))//FI)" [90,0,0,0] 61) "_AnnCond2" :: "'s assn \ 's bexp \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_//IF _//(2THEN/ (_))//FI)" [90,0,0] 61) "_AnnWhile" :: "'s assn \ 's bexp \ 's assn \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_//WHILE _/ INV _//(2DO/ (_))//OD)" [90,0,0,0] 61) "_AnnAwait" :: "'s assn \ 's bexp \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_//AWAIT _/ (2THEN/ (_))/ END)" [90,0,0] 61) "_AnnAtom" :: "'s assn \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_//\_\)" [90,0] 61) "_AnnWait" :: "'s assn \ 's bexp \ ('s,'p,'f) ann_com" ("(_//WAIT _/ END)" [90,0] 61) "_Cond" :: "'s bexp \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(IF _//(2THEN/ (_))//(2ELSE/ (_))//FI)" [0, 0, 0] 61) "_Cond2" :: "'s bexp \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(IF _//(2THEN/ (_))//FI)" [0,0] 56) "_While_inv" :: "'s bexp \ 's assn \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(WHILE _/ INV _//(2DO/ (_))//OD)" [0, 0, 0] 61) "_While" :: "'s bexp \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(WHILE _//(2DO/ (_))//OD)" [0, 0] 61) "_Await" :: "'s bexp \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(AWAIT _/ (2THEN/ (_))/ END)" [0,0] 61) "_Atom" :: "('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(\_\)" [0] 61) "_Wait" :: "'s bexp \ ('s,'p,'f) ann_com" ("(WAIT _/ END)" [0] 61) "_grd" :: "'f \ 's bexp \ grd" ("'(_, _')" [1000] 1000) "_last_grd" :: "grd \ grds" ("_" 1000) "_grds" :: "[grd, grds] \ grds" ("(_,/ _)" [999,1000] 1000) "_guards" :: "'s assn \ grds \ ('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("(_//(2_ \/ (_)))" [90, 0, 56] 61) "_Throw" :: "('s,'p,'f) ann_com" ("THROW" 61) "_AnnThrow" :: "'s assn \ ('s,'p,'f) ann_com" ("(_/ THROW)" [90] 61) "_Try_Catch" :: "('s,'p,'f) ann_com \('s,'p,'f) ann_com \ ('s,'p,'f) ann_com" ("((2TRY/ (_))//(2CATCH/ (_))/ END)" [0,0] 71) "_AnnCallX" :: "'s assn \ ('s \ 's) \ 's assn \ 'p \ nat \ ('s \ 's \ 's) \ ('s\'s\('s,'p,'f) com) \ 's assn \ 's assn \ 's assn \ 's assn \ ('s,'p,'f) ann_com" ("(_//(2CALLX/ (_)//_/ _/ _//_/ _//_/ _//_/ _))" [90,1000,0,1000,0,1000,1000,0,0,0,0] 61) "_AnnSCall" :: "'s assn \ 'p \ nat \ ('s,'p,'f) ann_com" ("(_//SCALL _/ _)" [90,0,0] 61) "_Skip" :: "('s,'p,'f) ann_com" ("SKIP" 61) "_AnnSkip" :: "'s assn \ ('s,'p,'f) ann_com" ("(_/ SKIP)" [90] 61) translations "r IF b THEN c1 ELSE c2 FI" \ "CONST AnnCom (CONST AnnBin r (c1\<^sub>?) (c2\<^sub>?)) (CONST Cond \b\ (c1\<^sub>!) (c2\<^sub>!))" "r IF b THEN c FI" \ "r IF b THEN c ELSE SKIP FI" "r WHILE b INV i DO c OD" \ "CONST AnnCom (CONST AnnWhile r i (c\<^sub>?)) (CONST While \b\ (c\<^sub>!))" "r AWAIT b THEN c END" \ "CONST AnnCom (CONST AnnRec r (c\<^sub>?)) (CONST Await \b\ (c\<^sub>!))" "r \c\" \ "r AWAIT CONST True THEN c END" "r WAIT b END" \ "r AWAIT b THEN SKIP END" "IF b THEN c1 ELSE c2 FI" \ "CONST FAKE_ANN IF b THEN c1 ELSE c2 FI" "IF b THEN c FI" \ "CONST FAKE_ANN IF b THEN c ELSE SKIP FI" "WHILE b DO c OD" \ "CONST FAKE_ANN WHILE b INV CONST FAKE_ANN DO c OD" "WHILE b INV i DO c OD" \ "CONST FAKE_ANN WHILE b INV i DO c OD" "AWAIT b THEN c END" \ "CONST FAKE_ANN AWAIT b THEN c END" "\c\" \ "CONST FAKE_ANN AWAIT CONST True THEN c END" "WAIT b END" \ "AWAIT b THEN SKIP END" "_grd f g" \ "(f, g)" "_grds g gs" \ "g#gs" "_last_grd g" \ "[g]" "_guards r gs c" \ "CONST AnnCom (CONST ann_guards r gs (c\<^sub>?)) (CONST guards gs (c\<^sub>!))" "ai CALLX init r p n restore return arestoreq areturn arestorea A" \ "CONST AnnCom (CONST ann_call ai r n arestoreq areturn arestorea A) (CONST call init p restore return)" "r SCALL p n" \ "CONST AnnCom (CONST AnnCall r n) (CONST Call p)" "r THROW" \ "CONST AnnCom (CONST AnnExpr r) (CONST Throw)" "THROW" \ "CONST FAKE_ANN THROW" "TRY c1 CATCH c2 END" \ "CONST AnnCom (CONST AnnComp (c1\<^sub>?) (c2\<^sub>?)) (CONST Catch (c1\<^sub>!) (c2\<^sub>!))" "r SKIP" \ "CONST AnnCom (CONST AnnExpr r) (CONST Skip)" "SKIP" \ "CONST FAKE_ANN SKIP" nonterminal prgs syntax "_PAR" :: "prgs \ 'a" ("(COBEGIN//_//COEND)" [57] 56) "_prg" :: "['a, 'a, 'a] \ prgs" ("(2 _//_,/ _)" [60, 90, 90] 57) "_prgs" :: "['a, 'a, 'a, prgs] \ prgs" ("(2 _//_,/ _)//\//_" [60,90,90,57] 57) "_prg_scheme" :: "['a, 'a, 'a, 'a, 'a, 'a] \ prgs" (" (2SCHEME [_ \ _ < _]//_//_,/ _)" [0,0,0,60, 90,90] 57) translations "_prg c q a" \ "([((c\<^sub>?), q, a)], [(c\<^sub>!)])" "_prgs c q a ps" \ "(((c\<^sub>?), q, a) # (ps\<^sub>,), (c\<^sub>!) # (ps\<^sub>.))" "_PAR ps" \ "CONST AnnCom (CONST AnnPar (ps\<^sub>,)) (CONST Parallel (ps\<^sub>.))" "_prg_scheme j i k c q a" \ "(CONST map (\i. ((c\<^sub>?), q, a)) [j..i. (c\<^sub>!)) [j.. ('s,'p,'f) proc_assns \ 'f set \ ('s,'p,'f) ann_com \ 's assn \ 's assn \ bool" ("(4_),/ (4_)/ (|\\<^bsub>'/_\<^esub> (_//_, _))" [60,60,60,20,1000,1000]60) "_oghoare_seq" :: "('s,'p,'f) body \ ('s,'p,'f) proc_assns \ 'f set \'s assn \ ('s,'p,'f) ann_com \ 's assn \ 's assn \ bool" ("(4_),/ (4_)/ (|\\<^bsub>'/_\<^esub> (_//_//_, _))" [60,60,60,1000,20,1000,1000]60) translations "_oghoare \ \ F c Q A" \ "\, \ \\<^bsub>/F\<^esub> (c\<^sub>?) (c\<^sub>!) Q, A" "_oghoare_seq \ \ F P c Q A" \ "\, \ \\<^bsub>/F\<^esub> P (c\<^sub>?) (c\<^sub>!) Q, A" ML \val syntax_debug = false\ print_translation \ let fun quote_tr' f (t :: ts) = Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) | quote_tr' _ _ = raise Match; fun annquote_tr' f (r :: t :: ts) = Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) | annquote_tr' _ _ = raise Match; val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) = annquote_tr' (Syntax.const name) (r :: t :: ts) | annbexp_tr' name (r :: Const (@{const_syntax UNIV}, _) :: ts) = annquote_tr' (Syntax.const name) (r :: Abs ("s", dummyT, Const (@{const_syntax True}, dummyT)) :: ts) | annbexp_tr' name (r :: Const (@{const_syntax Set.empty}, _) :: ts) = annquote_tr' (Syntax.const name) (r :: Abs ("s", dummyT, Const (@{const_syntax False}, dummyT)) :: ts) | annbexp_tr' name x = let val _ = if syntax_debug then writeln ("annbexp_tr'\n " ^ @{make_string} x) else () in raise Match end; fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f) (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | annassign_tr' r = let val _ = writeln ("annassign_tr'\n " ^ @{make_string} r) in raise Match end; fun dest_list (Const (@{const_syntax Nil}, _)) = [] | dest_list (Const (@{const_syntax Cons}, _) $ x $ xs) = x :: dest_list xs | dest_list _ = raise Match; fun guards_lst_tr' [fg] = fg | guards_lst_tr' (t :: ts) = Syntax.const @{syntax_const "_grds"} $ t $ guards_lst_tr' ts | guards_lst_tr' [] = raise Match; fun new_AnnCom r c = (Const (@{const_syntax AnnCom}, dummyT) $ r $ c) fun new_Pair a b = (Const (@{const_syntax Pair}, dummyT) $ a $ b) fun dest_prod (Const (@{const_syntax Pair}, _) $ a $ b) = (a, b) | dest_prod _ = raise Match; fun prgs_tr' f pqa c = let val (p, qa) = dest_prod pqa val (q, a) = dest_prod qa in [new_AnnCom (f p) (f c), f q, f a] end fun prgs_lst_tr' [p] [c] = list_comb (Syntax.const @{syntax_const "_prg"}, prgs_tr' I p c) | prgs_lst_tr' (p :: ps) (c :: cs) = list_comb (Syntax.const @{syntax_const "_prgs"}, prgs_tr' I p c) $ prgs_lst_tr' ps cs | prgs_lst_tr' _ _= raise Match; fun AnnCom_tr (Const (@{const_syntax AnnPar}, _) $ (Const (@{const_syntax map}, _) $ Abs (i, T, p) $ (Const _ $ j $ k)) :: Const (@{const_syntax Parallel}, _) $ (Const (@{const_syntax map}, _) $ Abs (_, _, c) $ _) :: ts) = let val _ = if syntax_debug then writeln "prg_scheme" else () - fun dest_abs body = snd (Term.dest_abs (i, T, body)) in + fun dest_abs body = snd (Term.dest_abs_global (Abs (i, T, body))) in Syntax.const @{syntax_const "_PAR"} $ list_comb (Syntax.const @{syntax_const "_prg_scheme"} $ j $ Free (i, T) $ k, prgs_tr' dest_abs p c) end | AnnCom_tr (Const (@{const_syntax AnnPar}, _) $ ps :: Const (@{const_syntax Parallel}, _) $ cs :: ts) = let val _ = if syntax_debug then writeln "Par" else () val (ps', cs') = (dest_list ps, dest_list cs) in Syntax.const @{syntax_const "_PAR"} $ prgs_lst_tr' ps' cs' end | AnnCom_tr (Const (@{const_syntax AnnExpr}, _) $ r :: Const (@{const_syntax Basic}, _) $ Abs (x, _, f $ k $ Bound 0) :: ts) = let val _ = if syntax_debug then writeln "Basic'" else () in quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f) (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) end | AnnCom_tr (Const (@{const_syntax AnnExpr}, _) $ r :: Const (@{const_syntax Basic}, _) $ (f $ k) :: ts) = let val _ = if syntax_debug then writeln "Basic" else () in quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f) (k :: ts) end | AnnCom_tr (Const (@{const_syntax AnnExpr}, _) $ r :: Const (@{const_syntax Spec}, _) $ (_ $ _ $ Abs (_,_, _ $ _ $ ((_ $ f) $ S $ _))) :: ts) = let val _ = if syntax_debug then writeln ("Spec") else () in (Syntax.const @{syntax_const "_AnnSpec"} $ r $ Syntax_Trans.update_name_tr' f $ Syntax_Trans.antiquote_tr' @{syntax_const "_antiquote"} S) end | AnnCom_tr (Const (@{const_syntax AnnComp}, _) $ r $ r' :: Const (@{const_syntax Seq}, _) $ c $ c' :: ts) = let val _ = if syntax_debug then writeln "Seq" else () in Syntax.const @{syntax_const "_AnnSeq"} $ new_AnnCom r c $ new_AnnCom r' c' end | AnnCom_tr (Const (@{const_syntax AnnRec}, _) $ r $ p :: Const (@{const_syntax Await}, _) $ b $ c :: ts) = let val _ = if syntax_debug then writeln "Await" else () in annbexp_tr' @{syntax_const "_AnnAwait"} (r :: b :: new_AnnCom p c :: ts) end | AnnCom_tr (Const (@{const_syntax AnnWhile}, _) $ r $ i $ p :: Const (@{const_syntax While}, _) $ b $ c :: ts) = let val _ = if syntax_debug then writeln "While" else () in annbexp_tr' @{syntax_const "_AnnWhile"} (r :: b :: i :: new_AnnCom p c :: ts) end | AnnCom_tr (Const (@{const_syntax AnnBin}, _) $ r $ p $ p' :: Const (@{const_syntax Cond}, _) $ b $ c $ c':: ts) = let val _ = if syntax_debug then writeln "Cond" else () in annbexp_tr' @{syntax_const "_AnnCond1"} (r :: b :: new_AnnCom p c :: new_AnnCom p' c' :: ts) end | AnnCom_tr (Const (@{const_syntax ann_guards}, _) $ r $ gs $ p :: Const (@{const_syntax guards}, _) $ _ $ c :: ts) = let val _ = if syntax_debug then writeln "guards" else () in Syntax.const @{syntax_const "_guards"} $ r $ guards_lst_tr' (dest_list gs) $ new_AnnCom p c end | AnnCom_tr (Const (@{const_syntax AnnRec}, _) $ r $ p :: Const (@{const_syntax Guard}, _) $ f $ g $ c :: ts) = let val _ = if syntax_debug then writeln "guards'" else () in Syntax.const @{syntax_const "_guards"} $ r $ new_Pair f g $ new_AnnCom p c end | AnnCom_tr (Const (@{const_syntax AnnCall}, _) $ r $ n :: Const (@{const_syntax Call}, _) $ p :: ts) = let val _ = if syntax_debug then writeln "SCall" else () in Syntax.const @{syntax_const "_AnnSCall"} $ r $ p $ n end | AnnCom_tr (Const (@{const_syntax ann_call}, _) $ ai $ r $ n $ arestoreq $ areturn $ arestorea $ A :: Const (@{const_syntax call}, _) $ init $ p $ restore $ return :: ts) = let val _ = if syntax_debug then writeln "CallX" else () in Syntax.const @{syntax_const "_AnnCallX"} $ ai $ init $ r $ p $ n $ restore $ return $ arestoreq $ areturn $ arestorea $ A end | AnnCom_tr (Const (@{const_syntax AnnComp}, _) $ r $ r' :: Const (@{const_syntax Catch}, _) $ c $ c' :: ts) = let val _ = if syntax_debug then writeln "Catch" else () in Syntax.const @{syntax_const "_Try_Catch"} $ new_AnnCom r c $ new_AnnCom r' c' end | AnnCom_tr (Const (@{const_syntax ann}, _) $ p :: Const (@{const_syntax com}, _) $ p' :: ts) = let val _ = if syntax_debug then writeln "ann_com" else () in if p = p' then p else raise Match end | AnnCom_tr x = let val _ = if syntax_debug then writeln ("AnnCom_tr\n " ^ @{make_string} x) else () in raise Match end; fun oghoare_tr (gamma :: sigma :: F :: r :: c :: Q :: A :: ts) = let val _ = if syntax_debug then writeln "oghoare" else () in Syntax.const @{syntax_const "_oghoare"} $ gamma $ sigma $ F $ new_AnnCom r c $ Q $ A end | oghoare_tr x = let val _ = writeln ("oghoare_tr\n " ^ @{make_string} x) in raise Match end; fun oghoare_seq_tr (gamma :: sigma :: F :: P :: r :: c :: Q :: A :: ts) = let val _ = if syntax_debug then writeln "oghoare_seq" else () in Syntax.const @{syntax_const "_oghoare_seq"} $ gamma $ sigma $ F $ P $ new_AnnCom r c $ Q $ A end | oghoare_seq_tr x = let val _ = writeln ("oghoare_seq_tr\n " ^ @{make_string} x) in raise Match end; in [(@{const_syntax Collect}, K assert_tr'), (@{const_syntax AnnCom}, K AnnCom_tr), (@{const_syntax oghoare}, K oghoare_tr), (@{const_syntax oghoare_seq}, K oghoare_seq_tr)] end \ end diff --git a/thys/Monad_Memo_DP/transform/Transform.ML b/thys/Monad_Memo_DP/transform/Transform.ML --- a/thys/Monad_Memo_DP/transform/Transform.ML +++ b/thys/Monad_Memo_DP/transform/Transform.ML @@ -1,239 +1,239 @@ signature TRANSFORM_DP = sig val dp_fun_part1_cmd: (binding * string) * ((bool * (xstring * Position.T)) * (string * string) list) option -> local_theory -> local_theory val dp_fun_part2_cmd: string * (Facts.ref * Token.src list) list -> local_theory -> local_theory val dp_correct_cmd: local_theory -> Proof.state end structure Transform_DP : TRANSFORM_DP = struct fun dp_interpretation standard_proof locale_name instance qualifier dp_term lthy = lthy |> Interpretation.isar_interpretation ([(locale_name, ((qualifier, true), (Expression.Named (("dp", dp_term) :: instance), [])))], []) |> (if standard_proof then Proof.global_default_proof else Proof.global_immediate_proof) fun prep_params (((scope, tm_str), def_thms_opt), mem_locale_opt) ctxt = let val tm = Syntax.read_term ctxt tm_str val scope' = (Binding.is_empty scope? Binding.map_name (fn _ => Transform_Misc.term_name tm ^ "\<^sub>T")) scope val def_thms_opt' = Option.map (Attrib.eval_thms ctxt) def_thms_opt val mem_locale_opt' = Option.map (Locale.check (Proof_Context.theory_of ctxt)) mem_locale_opt in (scope', tm, def_thms_opt', mem_locale_opt') end (* fun dp_interpretation_cmd args lthy = let val (scope, tm, _, mem_locale_opt) = prep_params args lthy val scope_name = Binding.name_of scope in case mem_locale_opt of NONE => lthy | SOME x => dp_interpretation x scope_name (Transform_Misc.uncurry tm) lthy end *) fun do_monadify heap_name scope tm mem_locale_opt def_thms_opt lthy = let val monad_consts = Transform_Const.get_monad_const heap_name val scope_name = Binding.name_of scope val memoizer_opt = if is_none mem_locale_opt then NONE else SOME (Transform_Misc.locale_term lthy scope_name "checkmem") val old_info_opt = Function_Common.import_function_data tm lthy val old_defs_opt = [ K def_thms_opt, K (Option.mapPartial #simps old_info_opt) ] |> Library.get_first (fn x => x ()) val old_defs = case old_defs_opt of SOME defs => defs | NONE => raise TERM("no definition", [tm]) val ((_, old_defs_imported), ctxt') = lthy |> fold Variable.declare_thm old_defs |> Variable.import true old_defs (* val new_bind = Binding.suffix_name "\<^sub>T'" scope val new_bindT = Binding.suffix_name "\<^sub>T" scope *) val new_bind = Binding.suffix_name "'" scope val new_bindT = scope fun dest_def (def, def_imported) = let val def_imported_meta = def_imported |> Local_Defs.meta_rewrite_rule ctxt' val eqs = def_imported_meta |> Thm.full_prop_of val (head, _) = Logic.dest_equals eqs |> fst |> Transform_Misc.behead tm (*val _ = if Term.aconv_untyped (head, tm) then () else raise THM("invalid definition", 0, [def])*) - val Abs t = Term.lambda_name (Binding.name_of new_bind, head) eqs - val (t_name, eqs') = Term.dest_abs t + val t = Term.lambda_name (Binding.name_of new_bind, head) eqs + val ((t_name, _), eqs') = Term.dest_abs_global t val _ = @{assert} (t_name = Binding.name_of new_bind) (*val eqs' = Term.subst_atomic [(head, Free (Binding.name_of new_bind, fastype_of head))] eqs*) val (rhs_conv, eqsT, n_args) = Transform_Term.lift_equation monad_consts ctxt' (Logic.dest_equals eqs') memoizer_opt val def_meta' = def |> Local_Defs.meta_rewrite_rule ctxt' |> Conv.fconv_rule (Conv.arg_conv (rhs_conv ctxt')) val def_meta_simped = def_meta' |> Conv.fconv_rule ( Transform_Term.repeat_sweep_conv (K Transform_Term.rewrite_pureapp_beta_conv) ctxt' ) (* val eqsT_simped = eqsT |> Syntax.check_term ctxt' |> Thm.cterm_of ctxt' |> Transform_Term.repeat_sweep_conv (K Transform_Term.rewrite_app_beta_conv) ctxt' |> Thm.full_prop_of |> Logic.dest_equals |> snd *) in ((def_meta_simped, eqsT), n_args) end val ((old_defs', new_defs_raw), n_args) = map dest_def (old_defs ~~ old_defs_imported) |> split_list |>> split_list ||> Transform_Misc.the_element val new_defs = Syntax.check_props lthy new_defs_raw |> map (fn eqsT => eqsT |> Thm.cterm_of lthy |> Transform_Term.repeat_sweep_conv (K (#rewrite_app_beta_conv monad_consts)) lthy |> Thm.full_prop_of |> Logic.dest_equals |> snd) (*val _ = map (Pretty.writeln o Syntax.pretty_term @{context} o Thm.full_prop_of) old_defs'*) (*val (new_defs, lthy) = Variable.importT_terms new_defs lthy*) val (new_info, lthy1) = Transform_Misc.add_function new_bind new_defs lthy val replay_tac = case old_info_opt of NONE => no_tac | SOME info => Transform_Tactic.totality_replay_tac info new_info lthy1 val totality_tac = replay_tac ORELSE (Function_Common.termination_prover_tac false lthy1 THEN Transform_Tactic.my_print_tac "termination by default prover") val (new_info, lthy2) = Function.prove_termination NONE totality_tac lthy1 val new_def' = new_info |> #simps |> the val head' = new_info |> #fs |> the_single val headT = Transform_Term.wrap_head monad_consts head' n_args |> Syntax.check_term lthy2 val ((headTC, (_, new_defT)), lthy) = Local_Theory.define ((new_bindT, NoSyn), ((Thm.def_binding new_bindT,[]), headT)) lthy2 val lthy3 = Transform_Data.commit_dp_info (#monad_name monad_consts) ({ old_head = tm, new_head' = head', new_headT = headTC, old_defs = old_defs', new_def' = new_def', new_defT = new_defT }) lthy val _ = Proof_Display.print_consts true (Position.thread_data ()) lthy3 (K false) [ (Binding.name_of new_bind, Term.type_of head'), (Binding.name_of new_bindT, Term.type_of headTC)] in lthy3 end fun gen_dp_monadify prep_term args lthy = let val (scope, tm, def_thms_opt, mem_locale_opt) = prep_params args lthy (* val memoizer_opt = memoizer_scope_opt |> Option.map (fn memoizer_scope => Syntax.read_term lthy (Long_Name.qualify memoizer_scope Transform_Const.checkmemVN)) val _ = memoizer_opt |> Option.map (fn memoizer => if Term.aconv_untyped (head_of memoizer, @{term mem_defs.checkmem}) then () else raise TERM("invalid memoizer", [the memoizer_opt])) *) in do_monadify "state" scope tm mem_locale_opt def_thms_opt lthy end val dp_monadify_cmd = gen_dp_monadify Syntax.read_term fun dp_fun_part1_cmd ((scope, tm_str), (mem_locale_instance_opt)) lthy = let val scope_name = Binding.name_of scope val tm = Syntax.read_term lthy tm_str val _ = if is_Free tm then warning ("Free term: " ^ (Syntax.pretty_term lthy tm |> Pretty.string_of)) else () val mem_locale_opt' = Option.map (Locale.check (Proof_Context.theory_of lthy) o (snd o fst)) mem_locale_instance_opt val lthy1 = case mem_locale_instance_opt of NONE => lthy | SOME ((standard_proof, locale_name), instance) => let val locale_name = Locale.check (Proof_Context.theory_of lthy) locale_name val instance = map (apsnd (Syntax.read_term lthy)) instance in dp_interpretation standard_proof locale_name instance scope_name (Transform_Misc.uncurry tm) lthy end in Transform_Data.add_tmp_cmd_info (Binding.reset_pos scope, tm, mem_locale_opt') lthy1 end fun dp_fun_part2_cmd (heap_name, def_thms_str) lthy = let val {scope, head=tm, locale=locale_opt, dp_info=dp_info_opt} = Transform_Data.get_last_cmd_info lthy val _ = if is_none dp_info_opt then () else raise TERM("already monadified", [tm]) val def_thms = Attrib.eval_thms lthy def_thms_str in do_monadify heap_name scope tm locale_opt (SOME def_thms) lthy end fun dp_correct_cmd lthy = let val {scope, head=tm, locale=locale_opt, dp_info=dp_info_opt} = Transform_Data.get_last_cmd_info lthy val dp_info = case dp_info_opt of SOME x => x | NONE => raise TERM("not yet monadified", [tm]) val _ = if is_some locale_opt then () else raise TERM("not interpreted yet", [tm]) val scope_name = Binding.name_of scope val consistentDP = Transform_Misc.locale_term lthy scope_name "consistentDP" val dpT' = #new_head' dp_info val dpT'_curried = dpT' |> Transform_Misc.uncurry val goal_pat = consistentDP $ dpT'_curried val goal_prop = Syntax.check_term lthy (HOLogic.mk_Trueprop goal_pat) val tuple_pat = type_of dpT' |> strip_type |> fst |> length |> Name.invent_list [] "a" |> map (fn s => Var ((s, 0), TVar ((s, 0), @{sort type}))) |> HOLogic.mk_tuple |> Thm.cterm_of lthy val memoized_thm_opt = Transform_Misc.locale_thms lthy scope_name "memoized" |> the_single |> SOME handle ERROR msg => (warning msg; NONE) val memoized_thm'_opt = memoized_thm_opt |> Option.map (Drule.infer_instantiate' lthy [NONE, SOME tuple_pat]) fun display_thms thm_binds ctxt = Proof_Display.print_results true (Position.thread_data ()) ctxt ((Thm.theoremK, ""), [thm_binds]) val crel_thm_name = "crel" val memoized_thm_name = "memoized_correct" fun afterqed result lthy1 = let val [[crel_thm]] = result val (crel_thm_binds, lthy2) = lthy1 |> Local_Theory.note ((Binding.qualify_name true scope crel_thm_name, []), [crel_thm]) val _ = display_thms crel_thm_binds lthy2 in case memoized_thm'_opt of NONE => lthy2 | SOME memoized_thm' => let val (memoized_thm_binds, lthy3) = lthy2 |> Local_Theory.note ((Binding.qualify_name true scope memoized_thm_name, []), [(crel_thm RS memoized_thm') |> Local_Defs.unfold lthy @{thms prod.case}]) val _ = display_thms memoized_thm_binds lthy3 in lthy3 end end in Proof.theorem NONE afterqed [[(goal_prop, [])]] lthy end end diff --git a/thys/Monad_Memo_DP/transform/Transform_Term.ML b/thys/Monad_Memo_DP/transform/Transform_Term.ML --- a/thys/Monad_Memo_DP/transform/Transform_Term.ML +++ b/thys/Monad_Memo_DP/transform/Transform_Term.ML @@ -1,344 +1,344 @@ signature TRANSFORM_TERM = sig val repeat_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv val rewrite_pureapp_beta_conv: conv val wrap_head: Transform_Const.MONAD_CONSTS -> term -> int -> term val lift_equation: Transform_Const.MONAD_CONSTS -> Proof.context -> term * term -> term option -> (Proof.context -> conv) * term * int end structure Transform_Term : TRANSFORM_TERM = struct fun list_conv (head_conv, arg_convs) ctxt = Library.foldl (uncurry Conv.combination_conv) (head_conv ctxt, map (fn conv => conv ctxt) arg_convs) fun eta_conv1 ctxt = (Conv.abs_conv (K Conv.all_conv) ctxt) else_conv (Thm.eta_long_conversion then_conv Conv.abs_conv (K Thm.eta_conversion) ctxt) fun eta_conv_n n = funpow n (fn conv => fn ctxt => eta_conv1 ctxt then_conv Conv.abs_conv (conv o #2) ctxt) (K Conv.all_conv) fun conv_changed conv ctm = let val eq = conv ctm in if Thm.is_reflexive eq then Conv.no_conv ctm else eq end fun repeat_sweep_conv conv = Conv.repeat_conv o conv_changed o Conv.top_sweep_conv conv val app_mark_conv = Conv.rewr_conv @{thm App_def[symmetric]} val app_unmark_conv = Conv.rewr_conv @{thm App_def} val wrap_mark_conv = Conv.rewr_conv @{thm Wrap_def[symmetric]} fun eta_expand tm = let val n_args = Integer.min 1 (length (binder_types (fastype_of tm))) val (args, body) = Term.strip_abs_eta n_args tm in Library.foldr (uncurry Term.absfree) (args, body) end fun is_ctr_sugar ctxt tp_name = is_some (Ctr_Sugar.ctr_sugar_of ctxt tp_name) fun type_nargs tp = tp |> strip_type |> fst |> length fun term_nargs tm = type_nargs (fastype_of tm) fun lift_type (monad_consts: Transform_Const.MONAD_CONSTS) ctxt tp = #mk_stateT monad_consts (lift_type' monad_consts ctxt tp) and lift_type' monad_consts ctxt (tp as Type (@{type_name fun}, _)) = lift_type' monad_consts ctxt (domain_type tp) --> lift_type monad_consts ctxt (range_type tp) | lift_type' monad_consts ctxt (tp as Type (tp_name, tp_args)) = if is_ctr_sugar ctxt tp_name then Type (tp_name, map (lift_type' monad_consts ctxt) tp_args) else if null tp_args then tp (* int, nat, \ *) else raise TYPE("not a ctr_sugar", [tp], []) | lift_type' _ _ tp = tp fun is_atom_type monad_consts ctxt tp = tp = lift_type' monad_consts ctxt tp fun is_1st_type monad_consts ctxt tp = body_type tp :: binder_types tp |> forall (is_atom_type monad_consts ctxt) fun orig_atom ctxt atom_name = Proof_Context.read_term_pattern ctxt atom_name fun is_1st_term monad_consts ctxt tm = is_1st_type monad_consts ctxt (fastype_of tm) fun is_1st_atom monad_consts ctxt atom_name = is_1st_term monad_consts ctxt (orig_atom ctxt atom_name) fun wrap_1st_term monad_consts tm n_args_opt inner_wrap = let val n_args = the_default (term_nargs tm) n_args_opt val (vars_name_typ, body) = Term.strip_abs_eta n_args tm fun wrap (name_typ, (conv, tm)) = (fn ctxt => eta_conv1 ctxt then_conv Conv.abs_conv (conv o #2) ctxt then_conv wrap_mark_conv, #return monad_consts (Term.absfree name_typ tm)) val (conv, result) = Library.foldr wrap (vars_name_typ, ( if inner_wrap then (K wrap_mark_conv, #return monad_consts body) else (K Conv.all_conv, body) )) in (conv, result) end fun lift_1st_atom monad_consts ctxt atom (name, tp) = let val (arg_typs, body_typ) = strip_type tp val n_args = term_nargs (orig_atom ctxt name) val (arg_typs, body_arg_typs) = chop n_args arg_typs val arg_typs' = map (lift_type' monad_consts ctxt) arg_typs val body_typ' = lift_type' monad_consts ctxt (body_arg_typs ---> body_typ) val tm' = atom (name, arg_typs' ---> body_typ') (* " *) in wrap_1st_term monad_consts tm' (SOME n_args) true end fun fixed_args head_n_args tm = let val (tm_head, tm_args) = strip_comb tm val n_tm_args = length tm_args in head_n_args tm_head |> Option.mapPartial (fn n_args => if n_tm_args > n_args then NONE else if n_tm_args < n_args then raise TERM("need " ^ string_of_int n_args ^ " args", [tm]) else SOME (tm_head, tm_args)) end fun lift_abs' monad_consts ctxt (name, typ) cont lift_dict body = let val free = Free (name, typ) val typ' = lift_type' monad_consts ctxt typ val freeT' = Free (name, typ') val freeT = #return monad_consts (freeT') val lift_dict' = if is_atom_type monad_consts ctxt typ then lift_dict else (free, (K wrap_mark_conv, freeT))::lift_dict val (conv_free, body_free) = (cont (lift_dict') body) val body' = lambda freeT' body_free fun conv ctxt' = eta_conv1 ctxt' then_conv Conv.abs_conv (conv_free o #2) ctxt' in (conv, body') end fun lift_arg monad_consts ctxt lift_dict tm = (* let val (conv, tm') = lift_term ctxt lift_dict (eta_expand tm) fun conv' ctxt = Conv.try_conv (eta_conv1 ctxt) then_conv (conv ctxt) in (conv', tm') end eta_expand AFTER lifting *) lift_term monad_consts ctxt lift_dict tm and lift_term monad_consts ctxt lift_dict tm = let val case_terms = Ctr_Sugar.ctr_sugars_of ctxt |> map #casex fun lookup_case_term tm = find_first (fn x => Term.aconv_untyped (x, tm)) case_terms val check_cont = lift_term monad_consts ctxt val check_cont_arg = lift_arg monad_consts ctxt fun check_const tm = case tm of Const (_, typ) => ( case Transform_Data.get_dp_info (#monad_name monad_consts) ctxt tm of SOME {new_headT=Const (name, _), ...} => SOME (K Conv.all_conv, Const (name, lift_type monad_consts ctxt typ)) | SOME {new_headT=tm', ...} => raise TERM("not a constant", [tm']) | NONE => NONE) | _ => NONE fun check_1st_atom tm = case tm of Const (name, typ) => if is_1st_atom monad_consts ctxt name then SOME (lift_1st_atom monad_consts ctxt Const (name, typ)) else NONE | Free (name, typ) => if is_1st_atom monad_consts ctxt name then SOME (lift_1st_atom monad_consts ctxt Free (name, typ)) else NONE | _ => (* if is_1st_term ctxt tm andalso exists_subterm (AList.defined (op aconv) lift_dict) tm then SOME (wrap_1st_term tm NONE) else *) NONE (* fun check_dict tm = (* TODO: map -> mapT, dummyT *) AList.lookup Term.aconv_untyped lift_dict tm |> Option.map (fn tm' => if is_Const tm then (@{assert} (is_Const tm'); map_types (K (lift_type ctxt (type_of tm))) tm') else tm') *) fun check_dict tm = AList.lookup Term.aconv_untyped lift_dict tm fun check_if tm = fixed_args (fn head => if Term.aconv_untyped (head, @{term If}) then SOME 3 else NONE) tm |> Option.map (fn (_, args) => let val (arg_convs, args') = map (check_cont lift_dict) args |> split_list val conv = list_conv (K Conv.all_conv, arg_convs) val tm' = list_comb (Const (#if_termN monad_consts, dummyT), args') in (conv, tm') end) fun check_abs tm = case tm of - Abs (name, typ, body) => + Abs _ => let - val (name', body') = Term.dest_abs (name, typ, body) + val ((name', typ), body') = Term.dest_abs_global tm val (conv, tm') = lift_abs' monad_consts ctxt (name', typ) check_cont lift_dict body' fun convT ctxt' = conv ctxt' then_conv wrap_mark_conv val tmT = #return monad_consts tm' in SOME (convT, tmT) end | _ => NONE fun check_case tm = fixed_args (lookup_case_term #> Option.map (fn cs => term_nargs cs - 1)) tm |> Option.map (fn (head, args) => let val (case_name, case_type) = lookup_case_term head |> the |> dest_Const val ((clause_typs, _), _) = strip_type case_type |>> split_last val clase_nparams = clause_typs |> map type_nargs (* ('a\'b) \ ('a\'b) |> type_nargs = 1*) fun lift_clause n_param clause = let val (vars_name_typ, body) = Term.strip_abs_eta n_param clause val abs_lift_wraps = map (lift_abs' monad_consts ctxt) vars_name_typ val lift_wrap = Library.foldr (op o) (abs_lift_wraps, I) check_cont val (conv, clauseT) = lift_wrap lift_dict body in (conv, clauseT) end val head' = Const (case_name, dummyT) (* clauses are sufficient for type inference *) val (convs, clauses') = map2 lift_clause clase_nparams args |> split_list fun conv ctxt' = list_conv (K Conv.all_conv, convs) ctxt' then_conv wrap_mark_conv val tm' = #return monad_consts (list_comb (head', clauses')) in (conv, tm') end) fun check_app tm = case tm of f $ x => let val (f_conv, tmf) = check_cont lift_dict f val (x_conv, tmx) = check_cont_arg lift_dict x val tm' = #app monad_consts (tmf, tmx) fun conv ctxt' = Conv.combination_conv (f_conv ctxt' then_conv app_mark_conv) (x_conv ctxt') in SOME (conv, tm') end | _ => NONE fun check_pure tm = if tm |> exists_subterm (AList.defined (op aconv) lift_dict) orelse not (is_1st_term monad_consts ctxt tm) then NONE else SOME (wrap_1st_term monad_consts tm NONE true) fun choke tm = raise TERM("cannot process term", [tm]) val checks = [ check_pure, check_const, check_case, check_if, check_abs, check_app, check_dict, check_1st_atom, choke ] in get_first (fn check => check tm) checks |> the end fun rewrite_pureapp_beta_conv ctm = case Thm.term_of ctm of Const (@{const_name Pure_Monad.App}, _) $ (Const (@{const_name Pure_Monad.Wrap}, _) $ Abs _) $ (Const (@{const_name Pure_Monad.Wrap}, _) $ _) => Conv.rewr_conv @{thm Wrap_App_Wrap} ctm | _ => Conv.no_conv ctm fun monadify monad_consts ctxt tm = let val (_, tm) = lift_term monad_consts ctxt [] tm (*val tm = rewrite_return_app_return tm*) val tm = Syntax.check_term ctxt tm in tm end fun wrap_head (monad_consts: Transform_Const.MONAD_CONSTS) head n_args = Library.foldr (fn (typ, tm) => #return monad_consts (absdummy typ tm)) (replicate n_args dummyT, list_comb (head, rev (map_range Bound n_args))) fun lift_head monad_consts ctxt head n_args = let val dest_head = if is_Const head then dest_Const else dest_Free val (head_name, head_typ) = dest_head head val (arg_typs, body_typ) = strip_type head_typ val (arg_typs0, arg_typs1) = chop n_args arg_typs val arg_typs0' = map (lift_type' monad_consts ctxt) arg_typs0 val arg_typs1T = lift_type monad_consts ctxt (arg_typs1 ---> body_typ) val head_typ' = arg_typs0' ---> arg_typs1T val head' = Free (head_name, head_typ') val (head_conv, headT) = wrap_1st_term monad_consts head' (SOME n_args) false in (head', (head_conv, headT)) end fun lift_equation monad_consts ctxt (lhs, rhs) memoizer_opt = let val (head, args) = strip_comb lhs val n_args = length args val (head', (head_conv, headT)) = lift_head monad_consts ctxt head n_args val args' = args |> map (map_aterms (fn tm => tm |> map_types (if is_Const tm then K dummyT else lift_type' monad_consts ctxt))) val lhs' = list_comb (head', args') val frees = fold Term.add_frees args [] |> filter_out (is_atom_type monad_consts ctxt o snd) val lift_dict_args = frees |> map (fn (name, typ) => ( Free (name, typ), (K wrap_mark_conv, #return monad_consts (Free (name, lift_type' monad_consts ctxt typ))) )) val lift_dict = (head, (head_conv, headT)) :: lift_dict_args val (rhs_conv, rhsT) = lift_term monad_consts ctxt lift_dict rhs val rhsT_memoized = case memoizer_opt of SOME memoizer => memoizer $ HOLogic.mk_tuple args $ rhsT | NONE => rhsT val eqs' = (lhs', rhsT_memoized) |> HOLogic.mk_eq |> HOLogic.mk_Trueprop in (rhs_conv, eqs', n_args) end end diff --git a/thys/Simpl/generalise_state.ML b/thys/Simpl/generalise_state.ML --- a/thys/Simpl/generalise_state.ML +++ b/thys/Simpl/generalise_state.ML @@ -1,301 +1,301 @@ (* Title: generalise_state.ML Author: Norbert Schirmer, TU Muenchen Copyright (C) 2005-2007 Norbert Schirmer This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) signature SPLIT_STATE = sig val isState: term -> bool val abs_state: term -> term option val abs_var: Proof.context -> term -> (string * typ) val split_state: Proof.context -> string -> typ -> term -> (term * term list) val ex_tac: Proof.context -> term list -> tactic (* the term-list is the list of selectors as returned by split_state. They may be used to construct the instatiation of the existentially quantified state. *) end; functor GeneraliseFun (structure SplitState: SPLIT_STATE) = struct val genConj = @{thm generaliseConj}; val genImp = @{thm generaliseImp}; val genImpl = @{thm generaliseImpl}; val genAll = @{thm generaliseAll}; val gen_all = @{thm generalise_all}; val genEx = @{thm generaliseEx}; val genRefl = @{thm generaliseRefl}; val genRefl' = @{thm generaliseRefl'}; val genTrans = @{thm generaliseTrans}; val genAllShift = @{thm generaliseAllShift}; val gen_allShift = @{thm generalise_allShift}; val meta_spec = @{thm meta_spec}; val protectRefl = @{thm protectRefl}; val protectImp = @{thm protectImp}; fun gen_thm decomp (t,ct) = let val (ts,cts,recomb) = decomp (t,ct) in recomb (map (gen_thm decomp) (ts~~cts)) end; fun dest_prop (Const (@{const_name Pure.prop}, _) $ P) = P | dest_prop t = raise TERM ("dest_prop", [t]); fun prem_of thm = #1 (Logic.dest_implies (dest_prop (Thm.prop_of thm))); fun conc_of thm = #2 (Logic.dest_implies (dest_prop (Thm.prop_of thm))); fun dest_All (Const (@{const_name "All"},_)$t) = t | dest_All t = raise TERM ("dest_All",[t]); fun SIMPLE_OF ctxt rule prems = let val mx = fold (fn thm => fn i => Int.max (Thm.maxidx_of thm,i)) prems 0; in DistinctTreeProver.discharge ctxt prems (Thm.incr_indexes (mx + 1) rule) end; infix 0 OF_RAW fun tha OF_RAW thb = thb COMP (Drule.incr_indexes thb tha); fun SIMPLE_OF_RAW ctxt tha thb = SIMPLE_OF ctxt tha [thb]; datatype qantifier = Meta_all | Hol_all | Hol_ex fun list_exists (vs, x) = fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) vs x; fun spec' cv thm = let (* thm = Pure.prop ((all x. P x) ==> Q), where "all" is meta or HOL *) val (ct1,ct2) = thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb; in (case Thm.term_of ct1 of Const (@{const_name "Trueprop"},_) => let val (Var (sP,_)$Var (sV,sVT)) = HOLogic.dest_Trueprop (Thm.concl_of spec); val cvT = Thm.ctyp_of_cterm cv; val vT = Thm.typ_of cvT; in Thm.instantiate (TVars.make [(dest_TVar sVT, cvT)], Vars.make [((sP, vT --> HOLogic.boolT), #2 (Thm.dest_comb ct2)), ((sV, vT), cv)]) spec end | Const (@{const_name Pure.all},_) => let val (Var (sP,_)$Var (sV,sVT)) = Thm.concl_of meta_spec; val cvT = Thm.ctyp_of_cterm cv; val vT = Thm.typ_of cvT; in Thm.instantiate (TVars.make [(dest_TVar sVT, cvT)], Vars.make [((sP, vT --> propT), ct2), ((sV, vT),cv)]) meta_spec end | _ => raise THM ("spec'",0,[thm])) end; fun split_thm qnt ctxt s T t = let val (t',vars) = SplitState.split_state ctxt s T t; val vs = map (SplitState.abs_var ctxt) vars; val prop = (case qnt of Meta_all => Logic.list_all (vs,t') | Hol_all => HOLogic.mk_Trueprop (HOLogic.list_all (vs, t')) | Hol_ex => Logic.mk_implies (HOLogic.mk_Trueprop (list_exists (vs, t')), HOLogic.mk_Trueprop (HOLogic.mk_exists (s,T,t)))) in (case qnt of Hol_ex => Goal.prove ctxt [] [] prop (fn _ => SplitState.ex_tac ctxt vars) | _ => let val rP = conc_of genRefl'; val thm0 = Thm.instantiate (TVars.empty, Vars.make [(dest_Var rP, Thm.cterm_of ctxt prop)]) genRefl'; fun elim_all v thm = let val cv = Thm.cterm_of ctxt v; val spc = Goal.protect 0 (spec' cv thm); in SIMPLE_OF ctxt genTrans [thm,spc] end; val thm = fold elim_all vars thm0; in thm end) end; fun eta_expand ctxt ct = let val mi = Thm.maxidx_of_cterm ct; val T = domain_type (Thm.typ_of_cterm ct); val x = Thm.cterm_of ctxt (Var (("s",mi+1),T)); in Thm.lambda x (Thm.apply ct x) end; fun split_abs ctxt ct = (case Thm.term_of ct of - Abs x => (x, Thm.dest_abs ct) + Abs x => (x, Thm.dest_abs_global ct) | _ => split_abs ctxt (eta_expand ctxt ct)) fun decomp ctxt (Const (@{const_name HOL.conj}, _) $ t $ t', ct) = ([t,t'],snd (Drule.strip_comb ct), fn [thm,thm'] => SIMPLE_OF ctxt genConj [thm,thm']) | decomp ctxt ((allc as Const (@{const_name "All"},aT)) $ f, ct) = let val cf = snd (Thm.dest_comb ct); val (abst as (x,T,_),(cx',cb)) = split_abs ctxt cf; val Free (x',_) = Thm.term_of cx'; val (Const (@{const_name Pure.all},_)$Abs (s,_,_)) = genAll |> Thm.prems_of |> hd |> dest_prop; val genAll' = Drule.rename_bvars [(s,x)] genAll; val (Const (@{const_name Pure.all},_)$Abs (s',_,_)) = genAllShift |> Thm.prems_of |> hd |> dest_prop; val genAllShift' = Drule.rename_bvars [(s',x)] genAllShift; in if SplitState.isState (allc$Abs abst) then ([Thm.term_of cb],[cb], fn [thm] => let val P = HOLogic.dest_Trueprop (dest_prop (prem_of thm)); val thm' = split_thm Hol_all ctxt x' T P; val thm1 = genAllShift' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm')); val thm2 = genAll' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm)); in SIMPLE_OF ctxt genTrans [thm1,thm2] end) else ([Thm.term_of cb],[cb], fn [thm] => genAll' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm))) end | decomp ctxt ((exc as Const (@{const_name "Ex"},_)) $ f, ct) = let val cf = snd (Thm.dest_comb ct); val (abst as (x,T,_),(cx',cb)) = split_abs ctxt cf; val Free (x',_) = Thm.term_of cx'; val (Const (@{const_name Pure.all},_)$Abs (s,_,_)) = genEx |> Thm.prems_of |> hd |> dest_prop; val genEx' = Drule.rename_bvars [(s,x)] genEx; in if SplitState.isState (exc$Abs abst) then ([Thm.term_of cb],[cb], fn [thm] => let val P = HOLogic.dest_Trueprop (dest_prop (prem_of thm)); val thm' = split_thm Hol_ex ctxt x' T P; in SIMPLE_OF_RAW ctxt protectImp (Goal.protect 0 thm') end ) else ([Thm.term_of cb],[cb], fn [thm] => genEx' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm))) end | decomp ctxt (Const (@{const_name HOL.implies},_)$P$Q, ct) = let val [cP,cQ] = (snd (Drule.strip_comb ct)); in ([Q],[cQ],fn [thm] => let val X = genImp |> Thm.concl_of |> dest_prop |> Logic.dest_implies |> #1 |> dest_prop |> HOLogic.dest_Trueprop |> HOLogic.dest_imp |> #1 |> dest_Var; val genImp' = Thm.instantiate (TVars.empty, Vars.make [(X,cP)]) genImp; in SIMPLE_OF ctxt genImp' [thm] end) end | decomp ctxt (Const (@{const_name Pure.imp},_)$P$Q, ct) = let val [cP,cQ] = (snd (Drule.strip_comb ct)); in ([Q],[cQ],fn [thm] => let val X = genImpl |> Thm.concl_of |> dest_prop |> Logic.dest_implies |> #1 |> dest_prop |> Logic.dest_implies |> #1 |> dest_Var; val genImpl' = Thm.instantiate (TVars.empty, Vars.make [(X,cP)]) genImpl; in SIMPLE_OF ctxt genImpl' [thm] end) end | decomp ctxt ((allc as Const (@{const_name Pure.all},_)) $ f, ct) = let val cf = snd (Thm.dest_comb ct); val (abst as (x,T,_),(cx',cb)) = split_abs ctxt cf; val Free (x',_) = Thm.term_of cx'; val (Const (@{const_name Pure.all},_)$Abs (s,_,_)) = gen_all |> Thm.prems_of |> hd |> dest_prop; val gen_all' = Drule.rename_bvars [(s,x)] gen_all; val (Const (@{const_name Pure.all},_)$Abs (s',_,_)) = gen_allShift |> Thm.prems_of |> hd |> dest_prop; val gen_allShift' = Drule.rename_bvars [(s',x)] gen_allShift; in if SplitState.isState (allc$Abs abst) then ([Thm.term_of cb],[cb], fn [thm] => let val P = dest_prop (prem_of thm); val thm' = split_thm Meta_all ctxt x' T P; val thm1 = gen_allShift' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm')); val thm2 = gen_all' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm)); in SIMPLE_OF ctxt genTrans [thm1,thm2] end) else ([Thm.term_of cb],[cb], fn [thm] => gen_all' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm))) end | decomp ctxt (Const (@{const_name "Trueprop"},_)$P, ct) = ([P],snd (Drule.strip_comb ct),fn [thm] => thm) | decomp ctxt (t, ct) = ([],[], fn [] => let val rP = HOLogic.dest_Trueprop (dest_prop (conc_of genRefl)); in Thm.instantiate (TVars.empty, Vars.make [(dest_Var rP, ct)]) genRefl end) fun generalise ctxt ct = gen_thm (decomp ctxt) (Thm.term_of ct,ct); (* -------- (init) #C ==> #C *) fun init ct = Thm.instantiate' [] [SOME ct] protectRefl; fun generalise_over_tac ctxt P i st = let val t = List.nth (Thm.prems_of st, i - 1); (* FIXME !? *) in (case P t of SOME t' => let val ct = Thm.cterm_of ctxt t'; val meta_spec_protect' = infer_instantiate ctxt [(("x", 0), ct)] @{thm meta_spec_protect}; in (init (Thm.adjust_maxidx_cterm 0 (List.nth (Drule.cprems_of st, i - 1))) |> resolve_tac ctxt [meta_spec_protect'] 1 |> Seq.maps (fn st' => Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, Goal.conclude st', Thm.nprems_of st') i st)) end | NONE => no_tac st) end; fun generalise_over_all_states_tac ctxt i = REPEAT (generalise_over_tac ctxt SplitState.abs_state i); fun generalise_tac ctxt i st = let val ct = List.nth (Drule.cprems_of st, i - 1); val ct' = Thm.dest_equals_rhs (Thm.cprop_of (Thm.eta_conversion ct)); val r = Goal.conclude (generalise ctxt ct'); in (init (Thm.adjust_maxidx_cterm 0 (List.nth (Drule.cprems_of st, i - 1))) |> (resolve_tac ctxt [r] 1 THEN resolve_tac ctxt [Drule.protectI] 1) |> Seq.maps (fn st' => Thm.bicompose NONE {flatten = true, match = false, incremented = false} (false, Goal.conclude st', Thm.nprems_of st') i st)) end fun GENERALISE ctxt i = generalise_over_all_states_tac ctxt i THEN generalise_tac ctxt i end; diff --git a/thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Logic.ML b/thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Logic.ML --- a/thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Logic.ML +++ b/thys/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Logic.ML @@ -1,44 +1,44 @@ (* Title: ETTS/ETTS_Tools/More_Logic.ML Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins An extension of the structure Logic from the standard library of Isabelle/Pure. *) signature LOGIC = sig include LOGIC val forall_elim_all : term -> term * (string * typ) list val get_forall_ftv_permute : term -> term * ((string * typ) list * int list) end structure Logic: LOGIC = struct open Logic; (*forall elimination*) fun forall_elim_all t = let - fun forall_elim_all_impl t ftv_specs = - let val (ftv_spec, t) = Logic.dest_all t - in forall_elim_all_impl t (ftv_spec::ftv_specs) end - handle TERM ("dest_all", _) => (t, ftv_specs) + fun forall_elim_all_impl t ftv_specs = + (case \<^try>\Logic.dest_all_global t\ of + SOME (ftv_spec, t) => forall_elim_all_impl t (ftv_spec::ftv_specs) + | NONE => (t, ftv_specs)) in forall_elim_all_impl t [] ||> rev end; (*indices of the universally quantified variables with respect to the order of their appearance in the term in the sense of Term.add_frees*) fun get_forall_ftv_permute t = let val (t', forall_ftv_specs) = forall_elim_all t val ftv_specs = Term.add_frees t' [] |> rev val call_ftv_specs = ftv_specs |> subtract op= (ftv_specs |> subtract op= forall_ftv_specs) val index_of_ftv = (call_ftv_specs ~~ (0 upto (length call_ftv_specs - 1))) |> AList.lookup op= #> the val forall_ftv_permute = map index_of_ftv forall_ftv_specs in (t', (forall_ftv_specs, forall_ftv_permute)) end; end; \ No newline at end of file