diff --git a/thys/Nominal2/nominal_dt_alpha.ML b/thys/Nominal2/nominal_dt_alpha.ML --- a/thys/Nominal2/nominal_dt_alpha.ML +++ b/thys/Nominal2/nominal_dt_alpha.ML @@ -1,878 +1,878 @@ (* Title: nominal_dt_alpha.ML Author: Cezary Kaliszyk Author: Christian Urban Definitions and proofs for the alpha-relations. *) signature NOMINAL_DT_ALPHA = sig val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> Proof.context -> alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> thm list * thm list val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> thm list -> thm list val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list val mk_funs_rsp: Proof.context -> thm -> thm val mk_alpha_permute_rsp: Proof.context -> thm -> thm end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = struct open Nominal_Permeq open Nominal_Dt_Data fun lookup xs x = the (AList.lookup (op=) xs x) fun group xs = AList.group (op=) xs (** definition of the inductive rules for alpha and alpha_bn **) (* construct the compound terms for prod_fv and prod_alpha *) fun mk_prod_fv (t1, t2) = let val ty1 = fastype_of t1 val ty2 = fastype_of t2 val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"} in Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2 end fun mk_prod_alpha (t1, t2) = let val ty1 = fastype_of t1 val ty2 = fastype_of t2 val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) val resT = [prodT, prodT] ---> @{typ "bool"} in Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 end (* generates the compound binder terms *) fun comb_binders lthy bmode args binders = let fun bind_set lthy args (NONE, i) = setify lthy (nth args i) | bind_set _ args (SOME bn, i) = bn $ (nth args i) fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) | bind_lst _ args (SOME bn, i) = bn $ (nth args i) val (combine_fn, bind_fn) = case bmode of Lst => (mk_append, bind_lst) | Set => (mk_union, bind_set) | Res => (mk_union, bind_set) in binders |> map (bind_fn lthy args) |> foldl1 combine_fn end (* produces the term for an alpha with abstraction *) fun mk_alpha_term bmode fv alpha args args' binders binders' = let val (alpha_name, binder_ty) = case bmode of Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) | Set => (@{const_name "alpha_set"}, @{typ "atom set"}) | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) val ty = fastype_of args val pair_ty = HOLogic.mk_prodT (binder_ty, ty) val alpha_ty = [ty, ty] ---> @{typ "bool"} val fv_ty = ty --> @{typ "atom set"} val pair_lhs = HOLogic.mk_prod (binders, args) val pair_rhs = HOLogic.mk_prod (binders', args') in HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs) end (* for non-recursive binders we have to produce alpha_bn premises *) fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = case binder of (NONE, _) => [] | (SOME bn, i) => if member (op=) bodies i then [] else [lookup alpha_bn_map bn $ nth args i $ nth args' i] (* generate the premises for an alpha rule; mk_frees is used if no binders are present *) fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = let fun mk_frees i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in if nth is_rec i then fst (lookup alpha_map ty) $ arg $ arg' else HOLogic.mk_eq (arg, arg') end fun mk_alpha_fv i = let val ty = fastype_of (nth args i) in case AList.lookup (op=) alpha_map ty of NONE => (HOLogic.eq_const ty, supp_const ty) | SOME (alpha, fv) => (alpha, fv) end in case bclause of BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies | BC (bmode, binders, bodies) => let val (alphas, fvs) = split_list (map mk_alpha_fv bodies) val comp_fv = foldl1 mk_prod_fv fvs val comp_alpha = foldl1 mk_prod_alpha alphas val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) val comp_binders = comb_binders lthy bmode args binders val comp_binders' = comb_binders lthy bmode args' binders val alpha_prem = mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) in map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) end end (* produces the introduction rule for an alpha rule *) fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha = fst (lookup alpha_map ty) val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end (* produces the premise of an alpha-bn rule; we only need to treat the case special where the binding clause is empty; - if the body is not included in the bn_info, then we either produce an equation or an alpha-premise - if the body is included in the bn_info, then we create either a recursive call to alpha-bn, or no premise *) fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause = let fun mk_alpha_bn_prem i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in case AList.lookup (op=) bn_args i of NONE => (case (AList.lookup (op=) alpha_map ty) of NONE => [HOLogic.mk_eq (arg, arg')] | SOME (alpha, _) => [alpha $ arg $ arg']) | SOME (NONE) => [] | SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg'] end in case bclause of BC (_, [], bodies) => map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies)) | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause end fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha_bn = lookup alpha_bn_map bn_trm val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let val nth_constrs_info = nth constrs_info bn_n val nth_bclausess = nth bclausesss bn_n in map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy = let val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys val alpha_frees = map Free (alpha_names ~~ alpha_tys) val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val alpha_bn_names = map (prefix "alpha_") bn_names val alpha_bn_arg_tys = map (nth raw_tys) bn_tys val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) val alpha_bn_map = bns ~~ alpha_bn_frees val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros) val (alpha_info, lthy') = lthy |> Local_Theory.begin_nested |> snd |> Inductive.add_inductive {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false} all_alpha_names [] all_alpha_intros [] |> Local_Theory.end_nested_result Inductive.transform_result; val phi = Proof_Context.export_morphism lthy' (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy); val alpha_info_global = Inductive.transform_result phi alpha_info; val all_alpha_trms = #preds alpha_info_global |> map Type.legacy_freeze (*FIXME*) val alpha_raw_induct = #raw_induct alpha_info_global val alpha_intros = #intrs alpha_info_global; val alpha_cases = #elims alpha_info_global; val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms val alpha_tys = map (domain_type o fastype_of) alpha_trms val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms val alpha_names = map (fst o dest_Const) alpha_trms val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms in (AlphaResult {alpha_names = alpha_names, alpha_trms = alpha_trms, alpha_tys = alpha_tys, alpha_bn_names = alpha_bn_names, alpha_bn_trms = alpha_bn_trms, alpha_bn_tys = alpha_bn_tys, alpha_intros = alpha_intros, alpha_cases = alpha_cases, alpha_raw_induct = alpha_raw_induct}, lthy') end (** induction proofs **) (* proof by structural induction over data types *) fun induct_prove tys props induct_thm cases_tac ctxt = let val (arg_names, ctxt') = Variable.variant_fixes (replicate (length tys) "x") ctxt val args = map2 (curry Free) arg_names tys val true_trms = replicate (length tys) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs val goals = group (props @ (tys ~~ true_trms)) |> map snd |> map2 apply_all args |> map fold_conj |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [induct_thm]) THEN_ALL_NEW (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt]))) in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (* proof by rule induction over the alpha-definitions *) fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt = let val arg_tys = map (domain_type o fastype_of) alphas val ((arg_names1, arg_names2), ctxt') = ctxt |> Variable.variant_fixes (replicate (length alphas) "x") ||>> Variable.variant_fixes (replicate (length alphas) "y") val args1 = map2 (curry Free) arg_names1 arg_tys val args2 = map2 (curry Free) arg_names2 arg_tys val true_trms = replicate (length alphas) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs val goals_rhs = group (props @ (alphas ~~ true_trms)) |> map snd |> map2 apply_all (args1 ~~ args2) |> map fold_conj fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2 val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2) val goals = (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs) |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [alpha_induct_thm]) THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt]) in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map (fn th => th RS mp) |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (** produces the distinctness theorems **) (* transforms the distinctness theorems of the constructors into "not-alphas" of the constructors *) fun mk_distinct_goal ty_trm_assoc neq = let val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = HOLogic.dest_not (HOLogic.dest_Trueprop neq) val ty_str = fst (dest_Type (domain_type ty_eq)) in Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |> HOLogic.mk_not |> HOLogic.mk_Trueprop end fun distinct_tac ctxt cases_thms distinct_thms = resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info val ty_trm_assoc = raw_dt_names ~~ alpha_names fun mk_alpha_distinct raw_distinct_trm = let val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm in Goal.prove ctxt [] [] goal (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1)) end in map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms end (** produces the alpha_eq_iff simplification rules **) (* in case a theorem is of the form (Rel Const Const), it will be rewritten to ((Rel Const = Const) = True) *) fun mk_simp_rule thm = case Thm.prop_of thm of @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} | _ => thm fun alpha_eq_iff_tac ctxt dist_inj intros elims = SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' (resolve_tac ctxt @{thms iffI} THEN' RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) fun mk_alpha_eq_iff_goal thm = let val prop = Thm.prop_of thm; val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); fun list_conj l = foldr1 HOLogic.mk_conj l; in if hyps = [] then HOLogic.mk_Trueprop concl else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) end; fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; val goals = map mk_alpha_eq_iff_goal thms_imp; val tac = alpha_eq_iff_tac ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; in Variable.export ctxt' ctxt thms |> map mk_simp_rule end (** reflexivity proof for the alphas **) val exi_zero = @{lemma "P (0::perm) \ (\x. P x)" by auto} fun cases_tac intros ctxt = let val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv} val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt val bound_tac = EVERY' [ resolve_tac ctxt [exi_zero], resolve_tac ctxt @{thms alpha_refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] in resolve_tac ctxt intros THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac] end fun raw_prove_refl ctxt alpha_result raw_dt_induct = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = alpha_result val props = map (fn (ty, c) => (ty, fn x => c $ x $ x)) ((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms)) in induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt end (** symmetry proof for the alphas **) val exi_neg = @{lemma "(\(p::perm). P p) \ (\q. P q \ Q (- q)) \ \p. Q p" by (erule exE, rule_tac x="-p" in exI, auto)} (* for premises that contain binders *) fun prem_bound_tac pred_names alpha_eqvt ctxt = let fun trans_prem_tac pred_names ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val prems' = map (transform_prem1 ctxt' pred_names) prems in resolve_tac ctxt' prems' 1 end) ctxt val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas} in EVERY' [ eresolve_tac ctxt [exi_neg], resolve_tac ctxt @{thms alpha_sym_eqvt}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, trans_prem_tac pred_names ctxt] end fun raw_prove_sym ctxt alpha_result alpha_eqvt = let val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, alpha_intros, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val alpha_names = alpha_names @ alpha_bn_names val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms fun tac ctxt = resolve_tac ctxt alpha_intros THEN_ALL_NEW FIRST' [assume_tac ctxt, resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt, prem_bound_tac alpha_names alpha_eqvt ctxt] in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt end (** transitivity proof for alphas **) (* applies cases rules and resolves them with the last premise *) fun ecases_tac cases = Subgoal.FOCUS (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems])) fun aatac pred_names = SUBPROOF (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems))) (* instantiates exI with the permutation p + q *) val perm_inst_tac = Subgoal.FOCUS (fn {context = ctxt, params, ...} => let val (p, q) = apply2 snd (last2 params) val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} in HEADGOAL (resolve_tac ctxt [exi_inst]) end) fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = let val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv} in resolve_tac ctxt intros THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' TRY o EVERY' (* if binders are present *) [ eresolve_tac ctxt @{thms exE}, eresolve_tac ctxt @{thms exE}, perm_inst_tac ctxt, resolve_tac ctxt @{thms alpha_trans_eqvt}, assume_tac ctxt, aatac pred_names ctxt, eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) end fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result val alpha_names = alpha_names @ alpha_bn_names fun all_cases ctxt = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms impI}, ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] end fun prep_trans_goal alpha_trm (arg1, arg2) = let val arg_ty = fastype_of arg1 val mid = alpha_trm $ arg2 $ (Bound 0) val rhs = alpha_trm $ arg1 $ (Bound 0) in HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) end fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt = let val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val props = map prep_trans_goal alpha_trms in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct (prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt end (** proves the equivp predicate for all alphas **) val reflp_def' = @{lemma "reflp R == \x. R x x" by (simp add: reflp_def refl_on_def)} val symp_def' = @{lemma "symp R \ \x y . R x y --> R y x" by (simp add: symp_def sym_def)} val transp_def' = @{lemma "transp R \ \x y. R x y \ (\z. R y z \ R x z)" by (rule eq_reflection, auto simp add: trans_def transp_def)} fun raw_prove_equivp ctxt alpha_result refl symm trans = let val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) in Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN' RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans'])))) |> chop (length alpha_trms) end (* proves that alpha_raw implies alpha_bn *) fun raw_prove_bn_imp_tac alpha_result ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' alpha_names) prems' in HEADGOAL (REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_prove_bn_imp ctxt alpha_result = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (raw_prove_bn_imp_tac alpha_result) ctxt end (* respectfulness for fv_raw / bn_raw *) fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set_simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) in alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct (K (asm_full_simp_tac simpset)) ctxt end (* respectfulness for size *) fun raw_size_rsp_aux ctxt alpha_result simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result fun mk_prop ty (x, y) = HOLogic.mk_eq (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv permute_prod_def prod.case prod.rec}) val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt end (* respectfulness for constructors *) fun raw_constr_rsp_tac ctxt alpha_intros simps = let val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def} val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps in asm_full_simp_tac pre_simpset THEN' REPEAT o (resolve_tac ctxt @{thms allI impI}) THEN' resolve_tac ctxt alpha_intros THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset) end fun raw_constrs_rsp ctxt alpha_result constrs simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result fun lookup ty = case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of NONE => HOLogic.eq_const ty | SOME alpha => alpha fun rel_fun_app (t1, t2) = Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2 fun prep_goal trm = trm |> strip_type o fastype_of |> (fn (tys, ty) => tys @ [ty]) |> map lookup |> foldr1 rel_fun_app |> (fn t => t $ trm $ trm) |> Syntax.check_term ctxt |> HOLogic.mk_Trueprop in map (fn constrs => Goal.prove_common ctxt NONE [] [] (map prep_goal constrs) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs end (* rsp lemmas for alpha_bn relations *) val rsp_equivp = @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> (=)) Q Q" by (simp only: rel_fun_def equivp_def, metis)} (* we have to reorder the alpha_bn_imps theorems in order to be in order with alpha_bn_trms *) fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps = let val AlphaResult {alpha_bn_trms, ...} = alpha_result fun mk_map thm = thm |> `Thm.prop_of |>> List.last o snd o strip_comb |>> HOLogic.dest_Trueprop |>> head_of |>> fst o dest_Const val alpha_bn_imps' = map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms fun mk_thm thm1 thm2 = - (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) + (Thm.forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) in map2 mk_thm alpha_bn_equivp alpha_bn_imps' end (* rsp for permute_bn functions *) val perm_bn_rsp = @{lemma "(\x y p. R x y \ R (f p x) (f p y)) \ ((=) ===> R ===> R) f f" by (simp add: rel_fun_def)} fun raw_prove_perm_bn_tac alpha_result simps ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems' in HEADGOAL (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems')) THEN' TRY o REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' @{thms refl}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result val perm_bn_ty = range_type o range_type o fastype_of val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms) val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) fun mk_prop t = let val alpha_trm = lookup ty_assoc (perm_bn_ty t) in (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y)) end val goals = map mk_prop perm_bns in alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct (raw_prove_perm_bn_tac alpha_result simps) ctxt |> Proof_Context.export ctxt' ctxt |> map (atomize ctxt) |> map single |> map (curry (op OF) perm_bn_rsp) end (* transformation of the natural rsp-lemmas into standard form *) val fun_rsp = @{lemma "(\x y. R x y \ f x = f y) \ (R ===> (=)) f f" by (simp add: rel_fun_def)} fun mk_funs_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) fun_rsp val permute_rsp = @{lemma "(\x y p. R x y \ R (permute p x) (permute p y)) ==> ((=) ===> R ===> R) permute permute" by (simp add: rel_fun_def)} fun mk_alpha_permute_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) permute_rsp end (* structure *) diff --git a/thys/Nominal2/nominal_function_core.ML b/thys/Nominal2/nominal_function_core.ML --- a/thys/Nominal2/nominal_function_core.ML +++ b/thys/Nominal2/nominal_function_core.ML @@ -1,1104 +1,1104 @@ (* Nominal Function Core Author: Christian Urban heavily based on the code of Alexander Krauss (code forked on 14 January 2011) Core of the nominal function package. *) signature NOMINAL_FUNCTION_CORE = sig val trace: bool Unsynchronized.ref val prepare_nominal_function : Nominal_Function_Common.nominal_function_config -> string (* defname *) -> ((bstring * typ) * mixfix) list (* defined symbol *) -> ((bstring * typ) list * term list * term * term) list (* specification *) -> local_theory -> (term (* f *) * term (* G(raph) *) * thm list (* GIntros *) * thm (* Ginduct *) * thm (* goalstate *) * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* continuation *) ) * local_theory val inductive_def : (binding * typ) * mixfix -> term list -> local_theory -> (term * thm list * thm * thm) * local_theory end structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = struct val trace = Unsynchronized.ref false fun trace_msg msg = if ! trace then tracing (msg ()) else () val boolT = HOLogic.boolT val mk_eq = HOLogic.mk_eq open Function_Lib open Function_Common open Nominal_Function_Common datatype globals = Globals of {fvar: term, domT: typ, ranT: typ, h: term, y: term, x: term, z: term, a: term, P: term, D: term, Pbool:term} datatype rec_call_info = RCInfo of {RIvs: (string * typ) list, (* Call context: fixes and assumes *) CCas: thm list, rcarg: term, (* The recursive argument *) llRI: thm, h_assum: term} datatype clause_context = ClauseContext of {ctxt : Proof.context, qs : term list, gs : term list, lhs: term, rhs: term, cqs: cterm list, ags: thm list, case_hyp : thm} fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = ClauseContext { ctxt = Proof_Context.transfer thy ctxt, qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } datatype clause_info = ClauseInfo of {no: int, qglr : ((string * typ) list * term list * term * term), cdata : clause_context, tree: Function_Context_Tree.ctx_tree, lGI: thm, RCs: rec_call_info list} (* Theory dependencies. *) val acc_induct_rule = @{thm accp_induct_rule} val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence} val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness} val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff} val acc_downward = @{thm accp_downward} val accI = @{thm accp.accI} val case_split = @{thm HOL.case_split} val fundef_default_value = @{thm Fun_Def.fundef_default_value} val not_acc_down = @{thm not_accp_down} fun find_calls tree = let fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs) | add_Ri _ _ _ _ = raise Match in rev (Function_Context_Tree.traverse_tree add_Ri tree []) end (* nominal *) fun mk_eqvt_at (f_trm, arg_trm) = let val f_ty = fastype_of f_trm val arg_ty = domain_type f_ty in Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm |> HOLogic.mk_Trueprop end fun mk_eqvt trm = let val ty = fastype_of trm in Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm |> HOLogic.mk_Trueprop end fun mk_inv inv (f_trm, arg_trm) = betapplys (inv, [arg_trm, (f_trm $ arg_trm)]) |> HOLogic.mk_Trueprop fun mk_invariant (Globals {x, y, ...}) G invariant = let val prem = HOLogic.mk_Trueprop (G $ x $ y) val concl = HOLogic.mk_Trueprop (betapplys (invariant, [x, y])) in Logic.mk_implies (prem, concl) |> mk_forall_rename ("y", y) |> mk_forall_rename ("x", x) end (** building proof obligations *) fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = mk_eqvt_at (fvar, arg) |> curry Logic.list_implies (map Thm.prop_of assms) |> fold_rev (Logic.all o Free) vs |> fold_rev absfree qs |> strip_abs_body fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = mk_inv inv (fvar, arg) |> curry Logic.list_implies (map Thm.prop_of assms) |> fold_rev (Logic.all o Free) vs |> fold_rev absfree qs |> strip_abs_body (** building proof obligations *) fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs = let fun mk_impl (((qs, gs, lhs, rhs), RCs_lhs), ((qs', gs', lhs', rhs'), RCs_rhs)) = let val shift = incr_boundvars (length qs') val eqvts_obligations_lhs = map (shift o mk_eqvt_proof_obligation qs fvar) RCs_lhs val eqvts_obligations_rhs = map (mk_eqvt_proof_obligation qs' fvar) RCs_rhs val invs_obligations_lhs = map (shift o mk_inv_proof_obligation inv qs fvar) RCs_lhs val invs_obligations_rhs = map (mk_inv_proof_obligation inv qs' fvar) RCs_rhs in Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |> fold_rev (curry Logic.mk_implies) invs_obligations_rhs (* nominal *) |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *) |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *) |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *) |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs') |> curry abstract_over fvar |> curry subst_bound f end in map mk_impl (unordered_pairs (glrs ~~ RCss)) end fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = let fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = HOLogic.mk_Trueprop Pbool |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) |> fold_rev (curry Logic.mk_implies) gs |> fold_rev mk_forall_rename (map fst oqs ~~ qs) in HOLogic.mk_Trueprop Pbool |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |> mk_forall_rename ("x", x) |> mk_forall_rename ("P", Pbool) end (** making a context with it's own local bindings **) fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = let val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs fun inst t = subst_bounds (rev qs, t) val gs = map inst pre_gs val lhs = inst pre_lhs val rhs = inst pre_rhs val cqs = map (Thm.cterm_of ctxt') qs val ags = map (Thm.assume o Thm.cterm_of ctxt') gs val case_hyp = Thm.assume (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) in ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } end (* lowlevel term function. FIXME: remove *) fun abstract_over_list vs body = let fun abs lev v tm = if v aconv tm then Bound lev else (case tm of Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) | t $ u => abs lev v t $ abs lev v u | t => t) in fold_index (fn (i, v) => fn t => abs i v t) vs body end fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = let val Globals {h, ...} = globals val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata val cert = Thm.cterm_of ctxt (* Instantiate the GIntro thm with "f" and import into the clause context. *) val lGI = GIntro_thm |> Thm.forall_elim (cert f) |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags fun mk_call_info (rcfix, rcassm, rcarg) RI = let val llRI = RI |> fold Thm.forall_elim cqs |> fold (Thm.forall_elim o cert o Free) rcfix |> fold Thm.elim_implies ags |> fold Thm.elim_implies rcassm val h_assum = HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] [] |> abstract_over_list (rev qs) in RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} end val RC_infos = map2 mk_call_info RCs RIntro_thms in ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos, tree=tree} end fun store_compat_thms 0 thms = [] | store_compat_thms n thms = let val (thms1, thms2) = chop n thms in (thms1 :: store_compat_thms (n - 1) thms2) end (* expects i <= j *) fun lookup_compat_thm i j cts = nth (nth cts (i - 1)) (j - i) (* nominal *) (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) (* if j < i, then turn around *) fun get_compat_thm ctxt cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj = let val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) in if j < i then let val compat = lookup_compat_thm j i cts in compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.elim_implies eqvtsj (* nominal *) |> fold Thm.elim_implies eqvtsi (* nominal *) |> fold Thm.elim_implies invsj (* nominal *) |> fold Thm.elim_implies invsi (* nominal *) |> fold Thm.elim_implies agsj |> fold Thm.elim_implies agsi |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) end else let val compat = lookup_compat_thm i j cts in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.elim_implies eqvtsi (* nominal *) |> fold Thm.elim_implies eqvtsj (* nominal *) |> fold Thm.elim_implies invsi (* nominal *) |> fold Thm.elim_implies invsj (* nominal *) |> fold Thm.elim_implies agsi |> fold Thm.elim_implies agsj |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) end end (* Generates the replacement lemma in fully quantified form. *) fun mk_replacement_lemma ctxt h ih_elim clause = let val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause local open Conv in val ih_conv = arg1_conv o arg_conv o arg_conv end val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs val h_assums = map (fn RCInfo {h_assum, ...} => Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs val (eql, _) = Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree val replace_lemma = (eql RS meta_eq_to_obj_eq) |> Thm.implies_intr (Thm.cprop_of case_hyp) |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs |> Thm.close_derivation \<^here> in replace_lemma end (* nominal *) (* Generates the eqvt lemmas for each clause *) fun mk_eqvt_lemma ctxt ih_eqvt clause = let val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause local open Conv in val ih_conv = arg1_conv o arg_conv o arg_conv end val ih_eqvt_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_eqvt_case) |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs in map prep_eqvt RCs |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags) |> map (Thm.implies_intr (Thm.cprop_of case_hyp)) |> map (fold_rev Thm.forall_intr cqs) |> map (Thm.close_derivation \<^here>) end (* nominal *) fun mk_invariant_lemma ctxt ih_inv clause = let val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause local open Conv in val ih_conv = arg1_conv o arg_conv o arg_conv end val ih_inv_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_inv fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_inv_case) |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs in map prep_inv RCs |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags) |> map (Thm.implies_intr (Thm.cprop_of case_hyp)) |> map (fold_rev Thm.forall_intr cqs) |> map (Thm.close_derivation \<^here>) end (* nominal *) fun mk_uniqueness_clause ctxt globals compat_store eqvts invs clausei clausej RLj = let val thy = Proof_Context.theory_of ctxt val Globals {h, y, x, fvar, ...} = globals val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ags = agsi, ...}, ...} = clausei val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} = mk_clause_context x ctxti cdescj val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' val Ghsj' = map (fn RCInfo {h_assum, ...} => Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj'] val RLj_import = RLj |> fold Thm.forall_elim cqsj' |> fold Thm.elim_implies agsj' |> fold Thm.elim_implies Ghsj' val eqvtsi = nth eqvts (i - 1) |> map (fold Thm.forall_elim cqsi) |> map (fold Thm.elim_implies [case_hyp]) |> map (fold Thm.elim_implies agsi) val eqvtsj = nth eqvts (j - 1) |> map (fold Thm.forall_elim cqsj') |> map (fold Thm.elim_implies [case_hypj']) |> map (fold Thm.elim_implies agsj') val invsi = nth invs (i - 1) |> map (fold Thm.forall_elim cqsi) |> map (fold Thm.elim_implies [case_hyp]) |> map (fold Thm.elim_implies agsi) val invsj = nth invs (j - 1) |> map (fold Thm.forall_elim cqsj') |> map (fold Thm.elim_implies [case_hypj']) |> map (fold Thm.elim_implies agsj') val compat = get_compat_thm ctxt compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |> Thm.implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj' |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h) |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj') |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj') end (* nominal *) fun mk_uniqueness_case ctxt globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems clausei = let val thy = Proof_Context.theory_of ctxt val Globals {x, y, ranT, fvar, ...} = globals val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs val ih_intro_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ih_intro fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs val existence = fold (curry op COMP o prep_RC) RCs lGI val P = Thm.cterm_of ctxt (mk_eq (y, rhsC)) val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y))) val unique_clauses = map2 (mk_uniqueness_clause ctxt globals compat_store eqvtlems invlems clausei) clauses replems fun elim_implies_eta A AB = Thm.bicompose NONE {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB |> Seq.list_of |> the_single val uniqueness = G_cases |> Thm.forall_elim (Thm.cterm_of ctxt lhs) |> Thm.forall_elim (Thm.cterm_of ctxt y) |> Thm.forall_elim P |> Thm.elim_implies G_lhs_y |> fold elim_implies_eta unique_clauses |> Thm.implies_intr (Thm.cprop_of G_lhs_y) |> Thm.forall_intr (Thm.cterm_of ctxt y) val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) val exactly_one = ex1I |> Thm.instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)] |> curry (op COMP) existence |> curry (op COMP) uniqueness |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym]) |> Thm.implies_intr (Thm.cprop_of case_hyp) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs val function_value = existence |> Thm.implies_intr ihyp |> Thm.implies_intr (Thm.cprop_of case_hyp) |> Thm.forall_intr (Thm.cterm_of ctxt x) |> Thm.forall_elim (Thm.cterm_of ctxt lhs) |> curry (op RS) refl in (exactly_one, function_value) end (* nominal *) fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = let val Globals {h, domT, ranT, x, ...} = globals (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |> Thm.cterm_of ctxt val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)] val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop})) val _ = trace_msg (K "Proving Replacement lemmas...") val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses val _ = trace_msg (K "Proving Equivariance lemmas...") val eqvtLemmas = map (mk_eqvt_lemma ctxt ih_eqvt) clauses val _ = trace_msg (K "Proving Invariance lemmas...") val invLemmas = map (mk_invariant_lemma ctxt ih_inv) clauses val _ = trace_msg (K "Proving cases for unique existence...") val (ex1s, values) = split_list (map (mk_uniqueness_case ctxt globals G f ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses) val _ = trace_msg (K "Proving: Graph is a function") val graph_is_function = complete |> Thm.forall_elim_vars 0 |> fold (curry op COMP) ex1s |> Thm.implies_intr ihyp |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |> Thm.forall_intr (Thm.cterm_of ctxt x) |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |> (fn it => fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) (Term.add_vars (Thm.prop_of it) []) it) val goalstate = Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt |> Thm.close_derivation \<^here> |> Goal.protect 0 |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat |> Thm.implies_intr (Thm.cprop_of complete) |> Thm.implies_intr (Thm.cprop_of invariant) |> Thm.implies_intr (Thm.cprop_of G_eqvt) in (goalstate, values) end (* wrapper -- restores quantifiers in rule specifications *) fun inductive_def (binding as ((R, T), _)) intrs lthy = let val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = lthy |> Config.put Inductive.inductive_internals true |> Proof_Context.concealed |> Inductive.add_inductive {quiet_mode = true, verbose = ! trace, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = true} [binding] (* relation *) [] (* no parameters *) (map (fn t => (Binding.empty_atts, t)) intrs) (* intro rules *) [] (* no special monos *) ||> Proof_Context.restore_naming lthy ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals) val cert = Thm.cterm_of lthy fun requantify orig_intro thm = let val (qs, t) = dest_all_all orig_intro val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) val vars = Term.add_vars (Thm.prop_of thm) [] val varmap = AList.lookup (op =) (frees ~~ map fst vars) #> the_default ("",0) in fold_rev (fn Free (n, T) => forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm end in - ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) + ((Rdef, map2 requantify intrs intrs_gen, Thm.forall_intr_vars elim_gen, induct), lthy) end (* nominal *) fun define_graph Gname fvar domT ranT clauses RCss lthy = let val GT = domT --> ranT --> boolT val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT) fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = let fun mk_h_assm (rcfix, rcassm, rcarg) = HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg)) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix in HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs) |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |> fold_rev (curry Logic.mk_implies) gs |> fold_rev Logic.all (fvar :: qs) end val G_intros = map2 mk_GIntro clauses RCss in inductive_def ((Binding.name n, T), NoSyn) G_intros lthy end fun define_function fdefname (fname, mixfix) domT ranT G default lthy = let val f_def = Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |> Syntax.check_term lthy in Local_Theory.define ((Binding.name (fname ^ "C"), mixfix), ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy end (* nominal *) fun define_recursion_relation Rname domT qglrs clauses RCss lthy = let val RT = domT --> domT --> boolT val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT) fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (curry Logic.mk_implies) gs |> fold_rev (Logic.all o Free) rcfix |> fold_rev mk_forall_rename (map fst oqs ~~ qs) (* "!!qs xs. CS ==> G => (r, lhs) : R" *) val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss val ((R, RIntro_thms, R_elim, _), lthy) = inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy in ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) end fun fix_globals domT ranT fvar ctxt = let val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt in (Globals {h = Free (h, domT --> ranT), y = Free (y, ranT), x = Free (x, domT), z = Free (z, domT), a = Free (a, domT), D = Free (D, domT --> boolT), P = Free (P, domT --> boolT), Pbool = Free (Pbool, boolT), fvar = fvar, domT = domT, ranT = ranT}, ctxt') end fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) = let fun inst_term t = subst_bound(f, abstract_over (fvar, t)) in (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg) end (********************************************************** * PROVING THE RULES **********************************************************) fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function = let val Globals {domT, z, ...} = globals fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = let val lhs_acc = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) val z_smaller = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) in ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |> (fn it => it COMP graph_is_function) |> Thm.implies_intr z_smaller |> Thm.forall_intr (Thm.cterm_of ctxt z) |> (fn it => it COMP valthm) |> Thm.implies_intr lhs_acc |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff]) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end in map2 mk_psimp clauses valthms end (** Induction rule **) val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} fun mk_partial_induct_rule ctxt globals R complete_thm clauses = let val Globals {domT, x, z, a, P, D, ...} = globals val acc_R = mk_acc domT R val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x))) val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a)) val D_subset = Thm.cterm_of ctxt (Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), HOLogic.mk_Trueprop (D $ z))))) |> Thm.cterm_of ctxt (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), HOLogic.mk_Trueprop (P $ Bound 0))) |> Thm.cterm_of ctxt val aihyp = Thm.assume ihyp fun prove_case clause = let val ClauseInfo {cdata = ClauseContext {ctxt = ctxt', qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, qglr = (oqs, _, _, _), ...} = clause val case_hyp_conv = K (case_hyp RS eq_reflection) local open Conv in val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D val sih = fconv_rule (Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt') aihyp end fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |> Thm.forall_elim (Thm.cterm_of ctxt rcarg) |> Thm.elim_implies llRI |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) val step = HOLogic.mk_Trueprop (P $ lhs) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs |> fold_rev (curry Logic.mk_implies) gs |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> Thm.cterm_of ctxt val P_lhs = Thm.assume step |> fold Thm.forall_elim cqs |> Thm.elim_implies lhs_D |> fold Thm.elim_implies ags |> fold Thm.elim_implies P_recs val res = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x)) |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |> Thm.symmetric (* P lhs == P x *) |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) |> Thm.implies_intr (Thm.cprop_of case_hyp) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs in (res, step) end val (cases, steps) = split_list (map prove_case clauses) val istep = complete_thm |> Thm.forall_elim_vars 0 |> fold (curry op COMP) cases (* P x *) |> Thm.implies_intr ihyp |> Thm.implies_intr (Thm.cprop_of x_D) |> Thm.forall_intr (Thm.cterm_of ctxt x) val subset_induct_rule = acc_subset_induct |> (curry op COMP) (Thm.assume D_subset) |> (curry op COMP) (Thm.assume D_dcl) |> (curry op COMP) (Thm.assume a_D) |> (curry op COMP) istep |> fold_rev Thm.implies_intr steps |> Thm.implies_intr a_D |> Thm.implies_intr D_dcl |> Thm.implies_intr D_subset val simple_induct_rule = subset_induct_rule |> Thm.forall_intr (Thm.cterm_of ctxt D) |> Thm.forall_elim (Thm.cterm_of ctxt acc_R) |> assume_tac ctxt 1 |> Seq.hd |> (curry op COMP) (acc_downward |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z])) |> Thm.forall_intr (Thm.cterm_of ctxt z) |> Thm.forall_intr (Thm.cterm_of ctxt x)) |> Thm.forall_intr (Thm.cterm_of ctxt a) |> Thm.forall_intr (Thm.cterm_of ctxt P) in simple_induct_rule end (* FIXME: broken by design *) fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = let val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, qglr = (oqs, _, _, _), ...} = clause val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |> fold_rev (curry Logic.mk_implies) gs |> Thm.cterm_of ctxt in Goal.init goal |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the |> (SINGLE (auto_tac ctxt)) |> the |> Goal.conclude |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end (** Termination rule **) val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} val wf_in_rel = @{thm Fun_Def.wf_in_rel} val in_rel_def = @{thm Fun_Def.in_rel_def} fun mk_nest_term_case ctxt globals R' ihyp clause = let val Globals {z, ...} = globals val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, qglr=(oqs, _, _, _), ...} = clause val ih_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ihyp fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = let val used = (u @ sub) |> map (fn (ctx,thm) => Function_Context_Tree.export_thm ctxt ctx thm) val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *) |> Function_Context_Tree.export_term (fixes, assumes) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> Thm.cterm_of ctxt val thm = Thm.assume hyp |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags |> Function_Context_Tree.import_thm ctxt (fixes, assumes) |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) |> Thm.cterm_of ctxt |> Thm.assume val acc = thm COMP ih_case val z_acc_local = acc |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) val ethm = z_acc_local |> Function_Context_Tree.export_thm ctxt (fixes, z_eq_arg :: case_hyp :: ags @ assumes) |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) val sub' = sub @ [(([],[]), acc)] in (sub', (hyp :: hyps, ethm :: thms)) end | step _ _ _ _ = raise Match in Function_Context_Tree.traverse_tree step tree end fun mk_nest_term_rule ctxt globals R R_cases clauses = let val Globals { domT, x, z, ... } = globals val acc_R = mk_acc domT R val R' = Free ("R", fastype_of R) val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) val inrel_R = Const (@{const_name Fun_Def.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R') |> Thm.cterm_of ctxt (* "wf R'" *) (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), HOLogic.mk_Trueprop (acc_R $ Bound 0))) |> Thm.cterm_of ctxt val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x)) val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], []) in R_cases |> Thm.forall_elim (Thm.cterm_of ctxt z) |> Thm.forall_elim (Thm.cterm_of ctxt x) |> Thm.forall_elim (Thm.cterm_of ctxt (acc_R $ z)) |> curry op COMP (Thm.assume R_z_x) |> fold_rev (curry op COMP) cases |> Thm.implies_intr R_z_x |> Thm.forall_intr (Thm.cterm_of ctxt z) |> (fn it => it COMP accI) |> Thm.implies_intr ihyp |> Thm.forall_intr (Thm.cterm_of ctxt x) |> (fn it => Drule.compose (it, 2, wf_induct_rule)) |> curry op RS (Thm.assume wfR') - |> forall_intr_vars + |> Thm.forall_intr_vars |> (fn it => it COMP allI) |> fold Thm.implies_intr hyps |> Thm.implies_intr wfR' |> Thm.forall_intr (Thm.cterm_of ctxt R') |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R)) |> curry op RS wf_in_rel |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def]) |> Thm.forall_intr (Thm.cterm_of ctxt Rrel) end (* nominal *) fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = let val NominalFunctionConfig {domintros, default=default_opt, inv=invariant_opt,...} = config val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) val invariant_str = the_default "%x y. True" invariant_opt val fvar = Free (fname, fT) val domT = domain_type fT val ranT = range_type fT val default = Syntax.parse_term lthy default_str |> Type.constraint fT |> Syntax.check_term lthy val invariant_trm = Syntax.parse_term lthy invariant_str |> Type.constraint ([domT, ranT] ---> @{typ bool}) |> Syntax.check_term lthy val (globals, ctxt') = fix_globals domT ranT fvar lthy val Globals { x, h, ... } = globals val clauses = map (mk_clause_context x ctxt') abstract_qglrs val n = length abstract_qglrs fun build_tree (ClauseContext { ctxt, rhs, ...}) = Function_Context_Tree.mk_tree (Free (fname, fT)) h ctxt rhs val trees = map build_tree clauses val RCss = map find_calls trees val ((G, GIntro_thms, G_elim, G_induct), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy val RCss = map (map (inst_RC lthy fvar f)) RCss val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees val ((R, RIntro_thmss, R_elim), lthy) = PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT abstract_qglrs clauses RCss) lthy val (_, lthy) = Local_Theory.abbrev Syntax.mode_default ((Binding.name (defname ^ "_dom"), NoSyn), mk_acc domT R) lthy val newthy = Proof_Context.theory_of lthy val clauses = map (transfer_clause_ctx newthy) clauses val cert = Thm.cterm_of lthy val xclauses = PROFILE "xclauses" (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss val complete = mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume val compat = mk_compat_proof_obligations domT ranT fvar f RCss invariant_trm abstract_qglrs |> map (cert #> Thm.assume) val G_eqvt = mk_eqvt G |> cert |> Thm.assume val invariant = mk_invariant globals G invariant_trm |> cert |> Thm.assume val compat_store = store_compat_thms n compat val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim G_eqvt invariant) f_defthm fun mk_partial_rules newctxt provedgoal = let val ((graph_is_function, complete_thm), graph_is_eqvt) = provedgoal |> Conjunction.elim |>> fst o Conjunction.elim |>> Conjunction.elim |>> apfst (Thm.forall_elim_vars 0) val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt})) val psimps = PROFILE "Proving simplification rules" (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function val simple_pinduct = PROFILE "Proving partial induction rule" (mk_partial_induct_rule newctxt globals R complete_thm) xclauses val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newctxt globals R R_elim) xclauses val dom_intros = if domintros then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses) else NONE in NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm, psimps=psimps, simple_pinducts=[simple_pinduct], termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]} end in ((f, G, GIntro_thms, G_induct, goalstate, mk_partial_rules), lthy) end end diff --git a/thys/Nominal2/nominal_inductive.ML b/thys/Nominal2/nominal_inductive.ML --- a/thys/Nominal2/nominal_inductive.ML +++ b/thys/Nominal2/nominal_inductive.ML @@ -1,445 +1,445 @@ (* Title: nominal_inductive.ML Author: Christian Urban Author: Tjark Weber Infrastructure for proving strong induction theorems for inductive predicates involving nominal datatypes. Code based on an earlier version by Stefan Berghofer. *) signature NOMINAL_INDUCTIVE = sig val prove_strong_inductive: string list -> string list -> term list list -> thm -> thm list -> Proof.context -> Proof.state val prove_strong_inductive_cmd: xstring * (string * string list) list -> Proof.context -> Proof.state end structure Nominal_Inductive : NOMINAL_INDUCTIVE = struct fun mk_cplus p q = Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q fun mk_cminus p = Thm.apply @{cterm "uminus :: perm => perm"} p fun minus_permute_intro_tac ctxt p = resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}] fun minus_permute_elim p thm = thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) (* fixme: move to nominal_library *) fun real_head_of (@{term Trueprop} $ t) = real_head_of t | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of (Const (@{const_name HOL.induct_forall}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of t = head_of t fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = if null avoid then [] else let val vc_goal = concl_args |> HOLogic.mk_tuple |> mk_fresh_star avoid_trm |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params val finite_goal = avoid_trm |> mk_finite |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params in [vc_goal, finite_goal] end (* fixme: move to nominal_library *) fun map_term prop f trm = if prop trm then f trm else case trm of (t1 $ t2) => map_term prop f t1 $ map_term prop f t2 | Abs (x, T, t) => Abs (x, T, map_term prop f t) | _ => trm fun add_p_c p (c, c_ty) trm = let val (P, args) = strip_comb trm val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = map (mk_perm p) args in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> (fn t => HOLogic.all_const c_ty $ lambda c t ) |> (fn t => HOLogic.all_const @{typ perm} $ lambda p t) end fun induct_forall_const T = Const (@{const_name HOL.induct_forall}, (T --> @{typ bool}) --> @{typ bool}) fun mk_induct_forall (a, T) t = induct_forall_const T $ Abs (a, T, t) fun add_c_prop qnt Ps (c, c_name, c_ty) trm = let fun add t = let val (P, args) = strip_comb t val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = args |> qnt ? map (incr_boundvars 1) in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> qnt ? mk_induct_forall (c_name, c_ty) end in map_term (member (op =) Ps o head_of) add trm end fun prep_prem Ps c_name c_ty (avoid, avoid_trm) (params, prems, concl) = let val prems' = prems |> map (incr_boundvars 1) |> map (add_c_prop true Ps (Bound 0, c_name, c_ty)) val avoid_trm' = avoid_trm |> fold_rev absfree (params @ [(c_name, c_ty)]) |> strip_abs_body |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |> HOLogic.mk_Trueprop val prems'' = if null avoid then prems' else avoid_trm' :: prems' val concl' = concl |> incr_boundvars 1 |> add_c_prop false Ps (Bound 0, c_name, c_ty) in mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' end (* fixme: move to nominal_library *) fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2) | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2) | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2) | same_name _ = false (* fixme: move to nominal_library *) fun map7 _ [] [] [] [] [] [] [] = [] | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = f x y z u v r s :: map7 f xs ys zs us vs rs ss (* local abbreviations *) local open Nominal_Permeq in (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel} fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig end val all_elims = let fun spec' ct = Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec} in fold (fn ct => fn th => th RS spec' ct) end fun helper_tac flag prm p ctxt = Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} => let val prems' = prems |> map (minus_permute_elim p) |> map (eqvt_srule ctxt') val prm' = (prems' MRS prm) |> flag ? (all_elims [p]) |> flag ? (eqvt_srule ctxt') in asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1 end) ctxt fun non_binder_tac prem intr_cvars Ps ctxt = Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} => let val (prms, p, _) = split_last2 (map snd params) val prm_tys = map (fastype_of o Thm.term_of) prms val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms) |> eqvt_srule ctxt' (* for inductive-premises*) fun tac1 prm = helper_tac true prm p ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac ctxt' p, eqvt_stac ctxt', helper_tac false prm p ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i in EVERY1 [ eqvt_stac ctxt', resolve_tac ctxt' [prem'], RANGE (map (SUBGOAL o select) prems) ] end) ctxt fun fresh_thm ctxt user_thm p c concl_args avoid_trm = let val conj1 = mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c val conj2 = mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) concl_args))) (Bound 0) val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2)) |> HOLogic.mk_Trueprop val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ @{thms fresh_star_Pair fresh_star_permute_iff} val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in Goal.prove ctxt [] [] fresh_goal (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2} THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o eresolve_tac ctxt @{thms conjE}, simp]))) end val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x" by (simp add: supp_perm_eq)} val fresh_star_plus = @{lemma "fresh_star (permute q (permute p x)) c ==> fresh_star (permute (q + p) x) c" by (simp add: permute_plus)} fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => let val (prms, p, c) = split_last2 (map snd params) val prm_trms = map Thm.term_of prms val prm_tys = map fastype_of prm_trms val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems))) val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm' val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result (K (EVERY1 [eresolve_tac ctxt @{thms exE}, full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms supp_Pair fresh_star_Un}), REPEAT o eresolve_tac ctxt @{thms conjE}, dresolve_tac ctxt [fresh_star_plus], REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms) |> eqvt_srule ctxt' val fprop' = eqvt_srule ctxt' fprop val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop']) (* for inductive-premises*) fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p), eqvt_stac ctxt', helper_tac false prm (mk_cplus q p) ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl) (fn {context = ctxt'', ...} => EVERY1 [ CONVERSION (expand_conv_bot ctxt''), eqvt_stac ctxt'', resolve_tac ctxt'' [prem'], RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) |> singleton (Proof_Context.export ctxt' ctxt) in resolve_tac ctxt [side_thm] 1 end) ctxt fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = let val tac1 = non_binder_tac prem intr_cvars Ps ctxt val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI}, if null avoid then tac1 else tac2 ] end fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args {prems, context = ctxt} = let val cases_tac = map7 (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args in EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ] end val normalise = @{lemma "(Q \ (\p c. P p c)) \ (\c. Q \ P (0::perm) c)" by simp} fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = let val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt val (ind_prems, ind_concl) = raw_induct' |> Thm.prop_of |> Logic.strip_horn |>> map strip_full_horn val params = map (fn (x, _, _) => x) ind_prems val param_trms = (map o map) Free params val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs val intr_vars = (map o map) fst intr_vars_tys val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys val (intr_prems, intr_concls) = intrs |> map Thm.prop_of |> map2 subst_Vars intr_vars_substs |> map Logic.strip_horn |> split_list val intr_concls_args = map (snd o fixed_nonfixed_args ctxt' o HOLogic.dest_Trueprop) intr_concls val avoid_trms = avoids |> (map o map) (setify ctxt') |> map fold_union val vc_compat_goals = map4 mk_vc_compat (avoids ~~ avoid_trms) intr_prems intr_concls_args params val ([c_name, a, p], ctxt'') = Variable.variant_fixes ["c", "'a", "p"] ctxt' val c_ty = TFree (a, @{sort fs}) val c = Free (c_name, c_ty) val p = Free (p, @{typ perm}) val (preconds, ind_concls) = ind_concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map HOLogic.dest_imp |> split_list val Ps = map (fst o strip_comb) ind_concls val ind_concl' = ind_concls |> map (add_p_c p (c, c_ty)) |> (curry (op ~~)) preconds |> map HOLogic.mk_imp |> fold_conj |> HOLogic.mk_Trueprop val ind_prems' = ind_prems |> map2 (prep_prem Ps c_name c_ty) (avoids ~~ avoid_trms) fun after_qed ctxt_outside user_thms ctxt = let val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |> singleton (Proof_Context.export ctxt ctxt_outside) |> Old_Datatype_Aux.split_conj_thm |> map (fn thm => thm RS normalise) |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms permute_zero induct_rulify})) |> map (Drule.rotate_prems (length ind_prems')) |> map zero_var_indexes val qualified_thm_name = pred_names |> map Long_Name.base_name |> space_implode "_" |> (fn s => Binding.qualify false s (Binding.name "strong_induct")) val attrs = [ Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Rule_Cases.case_names rule_names)) ] in ctxt |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms) |> snd end in Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt'' end fun prove_strong_inductive_cmd (pred_name, avoids) ctxt = let val ({names, ...}, {raw_induct, intrs, ...}) = Inductive.the_inductive_global ctxt (long_name ctxt pred_name) val rule_names = hd names |> the o Induct.lookup_inductP ctxt |> fst o Rule_Cases.get |> map (fst o fst) val case_names = map fst avoids val _ = case duplicates (op =) case_names of [] => () | xs => error ("Duplicate case names: " ^ commas_quote xs) val _ = case subtract (op =) rule_names case_names of [] => () | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs) val avoids_ordered = order_default (op =) [] rule_names avoids fun read_avoids avoid_trms intr = let (* fixme hack *) - val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt - val trms = map (Thm.term_of o snd) ctrms + val (((_, inst), _), ctxt') = Variable.import true [intr] ctxt + val trms = build (inst |> Term_Subst.Vars.fold (cons o Thm.term_of o snd)) val ctxt'' = fold Variable.declare_term trms ctxt' in map (Syntax.read_term ctxt'') avoid_trms end val avoid_trms = map2 read_avoids avoids_ordered intrs in prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt end (* outer syntax *) local val single_avoid_parser = Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term) val avoids_parser = Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] val main_parser = Parse.name -- avoids_parser in val _ = Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} "prove strong induction theorem for inductive predicate involving nominal datatypes" (main_parser >> prove_strong_inductive_cmd) end end diff --git a/thys/Nominal2/nominal_library.ML b/thys/Nominal2/nominal_library.ML --- a/thys/Nominal2/nominal_library.ML +++ b/thys/Nominal2/nominal_library.ML @@ -1,516 +1,516 @@ (* Title: nominal_library.ML Author: Christian Urban Library functions for nominal. *) signature NOMINAL_LIBRARY = sig val mk_sort_of: term -> term val atom_ty: typ -> typ val atom_const: typ -> term val mk_atom_ty: typ -> term -> term val mk_atom: term -> term val mk_atom_set_ty: typ -> term -> term val mk_atom_set: term -> term val mk_atom_fset_ty: typ -> term -> term val mk_atom_fset: term -> term val mk_atom_list_ty: typ -> term -> term val mk_atom_list: term -> term val is_atom: Proof.context -> typ -> bool val is_atom_set: Proof.context -> typ -> bool val is_atom_fset: Proof.context -> typ -> bool val is_atom_list: Proof.context -> typ -> bool val to_set_ty: typ -> term -> term val to_set: term -> term val atomify_ty: Proof.context -> typ -> term -> term val atomify: Proof.context -> term -> term val setify_ty: Proof.context -> typ -> term -> term val setify: Proof.context -> term -> term val listify_ty: Proof.context -> typ -> term -> term val listify: Proof.context -> term -> term val fresh_ty: typ -> typ val fresh_const: typ -> term val mk_fresh_ty: typ -> term -> term -> term val mk_fresh: term -> term -> term val fresh_star_ty: typ -> typ val fresh_star_const: typ -> term val mk_fresh_star_ty: typ -> term -> term -> term val mk_fresh_star: term -> term -> term val supp_ty: typ -> typ val supp_const: typ -> term val mk_supp_ty: typ -> term -> term val mk_supp: term -> term val supp_rel_ty: typ -> typ val supp_rel_const: typ -> term val mk_supp_rel_ty: typ -> term -> term -> term val mk_supp_rel: term -> term -> term val supports_const: typ -> term val mk_supports_ty: typ -> term -> term -> term val mk_supports: term -> term -> term val finite_const: typ -> term val mk_finite_ty: typ -> term -> term val mk_finite: term -> term val mk_diff: term * term -> term val mk_append: term * term -> term val mk_union: term * term -> term val fold_union: term list -> term val fold_append: term list -> term val mk_conj: term * term -> term val fold_conj: term list -> term val fold_conj_balanced: term list -> term (* functions for de-Bruijn open terms *) val mk_binop_env: typ list -> string -> term * term -> term val mk_union_env: typ list -> term * term -> term val fold_union_env: typ list -> term list -> term (* fresh arguments for a term *) val fresh_args: Proof.context -> term -> term list (* some logic operations *) val strip_full_horn: term -> (string * typ) list * term list * term val mk_full_horn: (string * typ) list -> term list -> term -> term (* datatype operations *) type cns_info = (term * typ * typ list * bool list) list val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list (* tactics for function package *) val size_ss: simpset val pat_completeness_simp: thm list -> Proof.context -> tactic val prove_termination_ind: Proof.context -> int -> tactic val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory (* transformations of premises in inductions *) val transform_prem1: Proof.context -> string list -> thm -> thm val transform_prem2: Proof.context -> string list -> thm -> thm (* transformation into the object logic *) val atomize: Proof.context -> thm -> thm val atomize_rule: Proof.context -> int -> thm -> thm val atomize_concl: Proof.context -> thm -> thm (* applies a tactic to a formula composed of conjunctions *) val conj_tac: Proof.context -> (int -> tactic) -> int -> tactic end structure Nominal_Library: NOMINAL_LIBRARY = struct fun mk_sort_of t = @{term "sort_of"} $ t; fun atom_ty ty = ty --> @{typ "atom"}; fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty) fun mk_atom_ty ty t = atom_const ty $ t; fun mk_atom t = mk_atom_ty (fastype_of t) t; fun mk_atom_set_ty ty t = let val atom_ty = HOLogic.dest_setT ty val img_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom set"}; in Const (@{const_name image}, img_ty) $ atom_const atom_ty $ t end fun mk_atom_fset_ty ty t = let val atom_ty = dest_fsetT ty val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; in Const (@{const_name fimage}, fmap_ty) $ atom_const atom_ty $ t end fun mk_atom_list_ty ty t = let val atom_ty = dest_listT ty val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} in Const (@{const_name map}, map_ty) $ atom_const atom_ty $ t end fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t (* coerces a list into a set *) fun to_set_ty ty t = case ty of @{typ "atom list"} => @{term "set :: atom list => atom set"} $ t | @{typ "atom fset"} => @{term "fset :: atom fset => atom set"} $ t | _ => t fun to_set t = to_set_ty (fastype_of t) t (* testing for concrete atom types *) fun is_atom ctxt ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort at_base}) fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty | is_atom_set _ _ = false; fun is_atom_fset ctxt (Type (@{type_name "fset"}, [ty])) = is_atom ctxt ty | is_atom_fset _ _ = false; fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty | is_atom_list _ _ = false (* functions that coerce singletons, sets, fsets and lists of concrete atoms into general atoms sets / lists *) fun atomify_ty ctxt ty t = if is_atom ctxt ty then mk_atom_ty ty t else if is_atom_set ctxt ty then mk_atom_set_ty ty t else if is_atom_fset ctxt ty then mk_atom_fset_ty ty t else if is_atom_list ctxt ty then mk_atom_list_ty ty t else raise TERM ("atomify: term is not an atom, set or list of atoms", [t]) fun setify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] else if is_atom_set ctxt ty then mk_atom_set_ty ty t else if is_atom_fset ctxt ty then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t else if is_atom_list ctxt ty then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t else raise TERM ("setify: term is not an atom, set or list of atoms", [t]) fun listify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] else if is_atom_list ctxt ty then mk_atom_list_ty ty t else raise TERM ("listify: term is not an atom or list of atoms", [t]) fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t fun setify ctxt t = setify_ty ctxt (fastype_of t) t fun listify ctxt t = listify_ty ctxt (fastype_of t) t fun fresh_ty ty = [@{typ atom}, ty] ---> @{typ bool} fun fresh_const ty = Const (@{const_name fresh}, fresh_ty ty) fun mk_fresh_ty ty t1 t2 = fresh_const ty $ t1 $ t2 fun mk_fresh t1 t2 = mk_fresh_ty (fastype_of t2) t1 t2 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty) fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2 fun supp_ty ty = ty --> @{typ "atom set"}; fun supp_const ty = Const (@{const_name supp}, supp_ty ty) fun mk_supp_ty ty t = supp_const ty $ t fun mk_supp t = mk_supp_ty (fastype_of t) t fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"}; fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty) fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool}) fun mk_finite_ty ty t = finite_const ty $ t fun mk_finite t = mk_finite_ty (fastype_of t) t (* functions that construct differences, appends and unions but avoid producing empty atom sets or empty atom lists *) fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} | mk_diff (t1, @{term "{}::atom set"}) = t1 | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"} | mk_diff (t1, @{term "set ([]::atom list)"}) = t1 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) fun mk_append (t1, @{term "[]::atom list"}) = t1 | mk_append (@{term "[]::atom list"}, t2) = t2 | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) fun mk_union (t1, @{term "{}::atom set"}) = t1 | mk_union (@{term "{}::atom set"}, t2) = t2 | mk_union (t1, @{term "set ([]::atom list)"}) = t1 | mk_union (@{term "set ([]::atom list)"}, t2) = t2 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"} fun mk_conj (t1, @{term "True"}) = t1 | mk_conj (@{term "True"}, t2) = t2 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} fun fold_conj_balanced ts = Balanced_Tree.make HOLogic.mk_conj ts (* functions for de-Bruijn open terms *) fun mk_binop_env tys c (t, u) = let val ty = fastype_of1 (tys, t) in Const (c, [ty, ty] ---> ty) $ t $ u end fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} (* produces fresh arguments for a term *) fun fresh_args ctxt f = f |> fastype_of |> binder_types |> map (pair "z") |> Variable.variant_frees ctxt [f] |> map Free (** some logic operations **) (* decompses a formula into params, premises and a conclusion *) fun strip_full_horn trm = let fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) | strip_outer_params B = ([], B) val (params, body) = strip_outer_params trm val (prems, concl) = Logic.strip_horn body in (params, prems, concl) end (* composes a formula out of params, premises and a conclusion *) fun mk_full_horn params prems concl = Logic.list_implies (prems, concl) |> fold_rev mk_all params (** datatypes **) (* constructor infos *) type cns_info = (term * typ * typ list * bool list) list (* - term for constructor constant - type of the constructor - types of the arguments - flags indicating whether the argument is recursive *) (* returns info about constructors in a datatype *) fun all_dtyp_constrs_info descr = map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr (* returns the constants of the constructors plus the corresponding type and types of arguments *) fun all_dtyp_constrs_types descr = let fun aux ((ty_name, vs), (cname, args)) = let val vs_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) vs val ty = Type (ty_name, vs_tys) val arg_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) args val is_rec = map Old_Datatype_Aux.is_rec_type args in (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) end in map (map aux) (all_dtyp_constrs_info descr) end (** function package tactics **) fun pat_completeness_simp simps ctxt = let val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thms sum.inject sum.distinct} @ simps) in Pat_Completeness.pat_completeness_tac ctxt 1 THEN ALLGOALS (asm_full_simp_tac simpset) end (* simpset for size goals *) val size_ss = simpset_of (put_simpset HOL_ss @{context} addsimprocs [@{simproc natless_cancel_numerals}] addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral zero_less_Suc prod.size(1) mult_Suc_right}) val natT = @{typ nat} fun size_prod_const T1 T2 = let val T1_fun = T1 --> natT val T2_fun = T2 --> natT val prodT = HOLogic.mk_prodT (T1, T2) in Const (@{const_name size_prod}, [T1_fun, T2_fun, prodT] ---> natT) end fun snd_const T1 T2 = Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2) fun mk_measure_trm f ctxt T = HOLogic.dest_setT T |> fst o HOLogic.dest_prodT |> f |> curry (op $) (Const (@{const_name "measure"}, dummyT)) |> Syntax.check_term ctxt (* wf-goal arising in induction_schema *) fun prove_termination_ind ctxt = let fun mk_size_measure T = case T of (Type (@{type_name Sum_Type.sum}, [T1, T2])) => Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) | (Type (@{type_name Product_Type.prod}, [T1, T2])) => HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) | _ => HOLogic.size_const T val measure_trm = mk_measure_trm (mk_size_measure) ctxt in Function_Relation.relation_tac ctxt measure_trm end (* wf-goal arising in function definitions *) fun prove_termination_fun size_simps ctxt = let fun mk_size_measure T = case T of (Type (@{type_name Sum_Type.sum}, [T1, T2])) => Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) | (Type (@{type_name Product_Type.prod}, [T1, T2])) => size_prod_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) | _ => HOLogic.size_const T val measure_trm = mk_measure_trm (mk_size_measure) ctxt val tac = Function_Relation.relation_tac ctxt measure_trm THEN_ALL_NEW simp_tac (put_simpset size_ss ctxt addsimps size_simps) in Function.prove_termination NONE (HEADGOAL tac) ctxt end (** transformations of premises (in inductive proofs) **) (* given the theorem F[t]; proves the theorem F[f t] - F needs to be monotone - f returns either SOME for a term it fires on and NONE elsewhere *) fun map_term f t = (case f t of NONE => map_term' f t | x => x) and map_term' f (t $ u) = (case (map_term f t, map_term f u) of (NONE, NONE) => NONE | (SOME t'', NONE) => SOME (t'' $ u) | (NONE, SOME u'') => SOME (t $ u'') | (SOME t'', SOME u'') => SOME (t'' $ u'')) | map_term' f (Abs (s, T, t)) = (case map_term f t of NONE => NONE | SOME t'' => SOME (Abs (s, T, t''))) | map_term' _ _ = NONE; fun map_thm_tac ctxt tac thm = let val monos = Inductive.get_monos ctxt val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} in EVERY [cut_facts_tac [thm] 1, eresolve_tac ctxt [rev_mp] 1, REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)), REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))] end fun map_thm ctxt f tac thm = let val opt_goal_trm = map_term f (Thm.prop_of thm) in case opt_goal_trm of NONE => thm | SOME goal => Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) end (* inductive premises can be of the form R ... /\ P ...; split_conj_i picks out the part R or P part *) fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = (case head_of f1 of Const (name, _) => if member (op =) names name then SOME f1 else NONE | _ => NONE) | split_conj1 _ _ = NONE; fun split_conj2 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = (case head_of f1 of Const (name, _) => if member (op =) names name then SOME f2 else NONE | _ => NONE) | split_conj2 _ _ = NONE; fun transform_prem1 ctxt names thm = map_thm ctxt (split_conj1 names) (eresolve_tac ctxt [conjunct1] 1) thm fun transform_prem2 ctxt names thm = map_thm ctxt (split_conj2 names) (eresolve_tac ctxt [conjunct2] 1) thm (* transforms a theorem into one of the object logic *) -fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; +fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o Thm.forall_intr_vars; fun atomize_rule ctxt i thm = Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm (* applies a tactic to a formula composed of conjunctions *) fun conj_tac ctxt tac i = let fun select (trm, i) = case trm of @{term "Trueprop"} $ t' => select (t', i) | @{term "(&)"} $ _ $ _ => EVERY' [resolve_tac ctxt @{thms conjI}, RANGE [conj_tac ctxt tac, conj_tac ctxt tac]] i | _ => tac i in SUBGOAL select i end end (* structure *) open Nominal_Library; diff --git a/thys/Refine_Monadic/Refine_Automation.thy b/thys/Refine_Monadic/Refine_Automation.thy --- a/thys/Refine_Monadic/Refine_Automation.thy +++ b/thys/Refine_Monadic/Refine_Automation.thy @@ -1,555 +1,555 @@ section "More Automation" theory Refine_Automation imports Refine_Basic Refine_Transfer keywords "concrete_definition" :: thy_decl and "prepare_code_thms" :: thy_decl and "uses" begin text \ This theory provides a tool for extracting definitions from terms, and for generating code equations for recursion combinators. \ ML \ signature REFINE_AUTOMATION = sig type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } val extract_as_def: (string * typ) list -> string -> term -> local_theory -> ((term * thm) * local_theory) val extract_recursion_eqs: extraction list -> string -> thm -> local_theory -> local_theory val add_extraction: string -> extraction -> theory -> theory val prepare_code_thms_cmd: string list -> thm -> local_theory -> local_theory val define_concrete_fun: extraction list option -> binding -> Token.src list -> indexname list -> thm -> cterm list -> local_theory -> (thm * thm) * local_theory val mk_qualified: string -> bstring -> binding val prepare_cd_pattern: Proof.context -> cterm -> cterm val add_cd_pattern: cterm -> Context.generic -> Context.generic val del_cd_pattern: cterm -> Context.generic -> Context.generic val get_cd_patterns: Proof.context -> cterm list val add_vc_rec_thm: thm -> Context.generic -> Context.generic val del_vc_rec_thm: thm -> Context.generic -> Context.generic val get_vc_rec_thms: Proof.context -> thm list val add_vc_solve_thm: thm -> Context.generic -> Context.generic val del_vc_solve_thm: thm -> Context.generic -> Context.generic val get_vc_solve_thms: Proof.context -> thm list val vc_solve_tac: Proof.context -> bool -> tactic' val vc_solve_modifiers: Method.modifier parser list val setup: theory -> theory end structure Refine_Automation :REFINE_AUTOMATION = struct type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } structure extractions = Generic_Data ( type T = extraction list Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge_list ((op =) o apply2 #pattern) ) fun add_extraction name ex = Context.theory_map (extractions.map ( Symtab.update_list ((op =) o apply2 #pattern) (name,ex))) (* Define new constant name for subterm t in context bnd. Returns replacement for t using the new constant and definition theorem. *) fun extract_as_def bnd name t lthy = let val loose = rev (loose_bnos t); val rnames = #1 (Variable.names_of lthy |> fold_map (Name.variant o #1) bnd); val rfrees = map (fn (name,(_,typ)) => Free (name,typ)) (rnames ~~ bnd); val t' = subst_bounds (rfrees,t); val params = map Bound (rev loose); val param_vars = (Library.foldl (fn (l,i) => nth rfrees i :: l) ([],loose)); val param_types = map fastype_of param_vars; val def_t = Logic.mk_equals (list_comb (Free (name,param_types ---> fastype_of t'),param_vars),t'); val ((lhs_t,(_,def_thm)),lthy) = Specification.definition NONE [] [] (Binding.empty_atts,def_t) lthy; (*val _ = tracing "xxxx";*) val app_t = list_comb (lhs_t, params); in ((app_t,def_thm),lthy) end; fun mk_qualified basename q = Binding.qualify true basename (Binding.name q); fun extract_recursion_eqs exs basename orig_def_thm lthy = let val thy = Proof_Context.theory_of lthy val pat_net : extraction Item_Net.T = Item_Net.init ((op =) o apply2 #pattern) (fn {pattern, ...} => [pattern]) |> fold Item_Net.update exs local fun tr env t ctx = let (* Recurse for subterms *) val (t,ctx) = case t of t1$t2 => let val (t1,ctx) = tr env t1 ctx val (t2,ctx) = tr env t2 ctx in (t1$t2,ctx) end | Abs (x,T,t) => let val (t',ctx) = tr ((x,T)::env) t ctx in (Abs (x,T,t'),ctx) end | _ => (t,ctx) (* Check if we match a pattern *) val ex = Item_Net.retrieve_matching pat_net t |> get_first (fn ex => case try (Pattern.first_order_match thy (#pattern ex,t)) (Vartab.empty,Vartab.empty) of NONE => NONE | SOME _ => SOME ex ) in case ex of NONE => (t,ctx) | SOME ex => let (* Extract as new constant *) val (idx,defs,lthy) = ctx val name = (basename ^ "_" ^ string_of_int idx) val ((t,def_thm),lthy) = extract_as_def env name t lthy val ctx = (idx+1,(def_thm,ex)::defs,lthy) in (t,ctx) end end in fun transform t lthy = let val (t,(_,defs,lthy)) = tr [] t (0,[],lthy) in ((t,defs),lthy) end end (* Import theorem and extract RHS *) val ((_,orig_def_thm'),lthy) = yield_singleton2 (Variable.import true) orig_def_thm lthy; val (lhs,rhs) = orig_def_thm' |> Thm.prop_of |> Logic.dest_equals; (* Transform RHS, generating new constants *) val ((rhs',defs),lthy) = transform rhs lthy; val def_thms = map #1 defs (* Register definitions of generated constants *) val (_,lthy) = Local_Theory.note ((mk_qualified basename "defs",[]),def_thms) lthy; (* Obtain new def_thm *) val def_unfold_ss = put_simpset HOL_basic_ss lthy addsimps (orig_def_thm::def_thms) val new_def_thm = Goal.prove_internal lthy [] (Logic.mk_equals (lhs,rhs') |> Thm.cterm_of lthy) (K (simp_tac def_unfold_ss 1)) (* Obtain new theorem by folding with defs of generated constants *) (* TODO: Maybe cleaner to generate eq-thm and prove by "unfold, refl" *) (*val new_def_thm = Library.foldr (fn (dt,t) => Local_Defs.fold lthy [dt] t) (def_thms,orig_def_thm');*) (* Prepare code equations *) fun mk_code_thm lthy (def_thm,{gen_thm, gen_tac, ...}) = let val ((_,def_thm),lthy') = yield_singleton2 (Variable.import true) def_thm lthy; val thm = def_thm RS gen_thm; val tac = SOLVED' (gen_tac lthy') ORELSE' (simp_tac def_unfold_ss THEN' gen_tac lthy') val thm = the (SINGLE (ALLGOALS tac) thm); val thm = singleton (Variable.export lthy' lthy) thm; in thm end; val code_thms = map (mk_code_thm lthy) defs; val _ = if forall Thm.no_prems code_thms then () else warning "Unresolved premises in code theorems" val (_,lthy) = Local_Theory.note ((mk_qualified basename "code",@{attributes [code]}),new_def_thm::code_thms) lthy; in lthy end; fun prepare_code_thms_cmd names thm lthy = let fun name_of (Const (n,_)) = n | name_of (Free (n,_)) = n | name_of _ = raise (THM ("No definitional theorem",0,[thm])); val (lhs,_) = thm |> Thm.prop_of |> Logic.dest_equals; val basename = lhs |> strip_comb |> #1 |> name_of |> Long_Name.base_name; val exs_tab = extractions.get (Context.Proof lthy) fun get_exs name = case Symtab.lookup exs_tab name of NONE => error ("No such extraction mode: " ^ name) | SOME exs => exs val exs = case names of [] => Symtab.dest_list exs_tab |> map #2 | _ => map get_exs names |> flat val _ = case exs of [] => error "No extraction patterns selected" | _ => () val lthy = extract_recursion_eqs exs basename thm lthy in lthy end; fun extract_concrete_fun _ [] concl = raise TERM ("Conclusion does not match any extraction pattern",[concl]) | extract_concrete_fun thy (pat::pats) concl = ( case Refine_Util.fo_matchp thy pat concl of NONE => extract_concrete_fun thy pats concl | SOME [t] => t | SOME (t::_) => ( warning ("concrete_definition: Pattern has multiple holes, taking " ^ "first one: " ^ @{make_string} pat ); t) | _ => (warning ("concrete_definition: Ignoring invalid pattern " ^ @{make_string} pat); extract_concrete_fun thy pats concl) ) (* Define concrete function from refinement lemma *) fun define_concrete_fun gen_code fun_name attribs_raw param_names thm pats (orig_lthy:local_theory) = let val lthy = orig_lthy; - val ((inst,thm'),lthy) = yield_singleton2 (Variable.import true) thm lthy; + val (((_,inst),thm'),lthy) = yield_singleton2 (Variable.import true) thm lthy; val concl = thm' |> Thm.concl_of (*val ((typ_subst,term_subst),lthy) = Variable.import_inst true [concl] lthy; val concl = Term_Subst.instantiate (typ_subst,term_subst) concl; *) - val term_subst = #2 inst |> map (apsnd Thm.term_of) + val term_subst = build (inst |> Term_Subst.Vars.fold (cons o apsnd Thm.term_of)) val param_terms = map (fn name => case AList.lookup (fn (n,v) => n = #1 v) term_subst name of NONE => raise TERM ("No such variable: " ^Term.string_of_vname name,[concl]) | SOME t => t ) param_names; val f_term = extract_concrete_fun (Proof_Context.theory_of lthy) pats concl; val lhs_type = map Term.fastype_of param_terms ---> Term.fastype_of f_term; val lhs_term = list_comb ((Free (Binding.name_of fun_name,lhs_type)),param_terms); val def_term = Logic.mk_equals (lhs_term,f_term) |> fold Logic.all param_terms; val attribs = map (Attrib.check_src lthy) attribs_raw; val ((_,(_,def_thm)),lthy) = Specification.definition (SOME (fun_name,NONE,Mixfix.NoSyn)) [] [] ((Binding.empty,attribs),def_term) lthy; val folded_thm = Local_Defs.fold lthy [def_thm] thm'; val (_,lthy) = Local_Theory.note ((mk_qualified (Binding.name_of fun_name) "refine",[]),[folded_thm]) lthy; val lthy = case gen_code of NONE => lthy | SOME modes => extract_recursion_eqs modes (Binding.name_of fun_name) def_thm lthy in ((def_thm,folded_thm),lthy) end; val cd_pat_eq = apply2 (Thm.term_of #> Refine_Util.anorm_term) #> (op aconv) structure cd_patterns = Generic_Data ( type T = cterm list val empty = [] val extend = I val merge = merge cd_pat_eq ) fun prepare_cd_pattern ctxt pat = case Thm.term_of pat |> fastype_of of @{typ bool} => Thm.term_of pat |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt | _ => pat fun add_cd_pattern pat context = cd_patterns.map (insert cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context fun del_cd_pattern pat context = cd_patterns.map (remove cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context val get_cd_patterns = cd_patterns.get o Context.Proof structure rec_thms = Named_Thms ( val name = @{binding vcs_rec} val description = "VC-Solver: Recursive intro rules" ) structure solve_thms = Named_Thms ( val name = @{binding vcs_solve} val description = "VC-Solver: Solve rules" ) val add_vc_rec_thm = rec_thms.add_thm val del_vc_rec_thm = rec_thms.del_thm val get_vc_rec_thms = rec_thms.get val add_vc_solve_thm = solve_thms.add_thm val del_vc_solve_thm = solve_thms.del_thm val get_vc_solve_thms = solve_thms.get val rec_modifiers = [ Args.$$$ "rec" -- Scan.option Args.add -- Args.colon >> K (Method.modifier rec_thms.add \<^here>), Args.$$$ "rec" -- Scan.option Args.del -- Args.colon >> K (Method.modifier rec_thms.del \<^here>) ]; val solve_modifiers = [ Args.$$$ "solve" -- Scan.option Args.add -- Args.colon >> K (Method.modifier solve_thms.add \<^here>), Args.$$$ "solve" -- Scan.option Args.del -- Args.colon >> K (Method.modifier solve_thms.del \<^here>) ]; val vc_solve_modifiers = clasimp_modifiers @ rec_modifiers @ solve_modifiers; fun vc_solve_tac ctxt no_pre = let val rthms = rec_thms.get ctxt val sthms = solve_thms.get ctxt val pre_tac = if no_pre then K all_tac else clarsimp_tac ctxt val tac = SELECT_GOAL (auto_tac ctxt) in TRY o pre_tac THEN_ALL_NEW_FWD (TRY o REPEAT_ALL_NEW_FWD (resolve_tac ctxt rthms)) THEN_ALL_NEW_FWD (TRY o SOLVED' (resolve_tac ctxt sthms THEN_ALL_NEW_FWD tac)) end val setup = I #> rec_thms.setup #> solve_thms.setup end; \ setup Refine_Automation.setup setup \ let fun parse_cpat cxt = let val (t, (context, tks)) = Scan.lift Args.embedded_inner_syntax cxt val ctxt = Context.proof_of context val t = Proof_Context.read_term_pattern ctxt t in (Thm.cterm_of ctxt t, (context, tks)) end fun do_p f = Scan.repeat1 parse_cpat >> (fn pats => Thm.declaration_attribute (K (fold f pats))) in Attrib.setup @{binding "cd_patterns"} ( Scan.lift Args.add |-- do_p Refine_Automation.add_cd_pattern || Scan.lift Args.del |-- do_p Refine_Automation.del_cd_pattern || do_p Refine_Automation.add_cd_pattern ) "Add/delete concrete_definition pattern" end \ (* Command setup *) (* TODO: Folding of .refine-lemma seems not to work, if the function has parameters on which it does not depend *) ML \Outer_Syntax.local_theory @{command_keyword concrete_definition} "Define function from refinement theorem" (Parse.binding -- Parse.opt_attribs -- Scan.optional (@{keyword "for"} |-- Scan.repeat1 Args.var) [] --| @{keyword "uses"} -- Parse.thm -- Scan.optional (@{keyword "is"} |-- Scan.repeat1 Args.embedded_inner_syntax) [] >> (fn ((((name,attribs),params),raw_thm),pats) => fn lthy => let val thm = case Attrib.eval_thms lthy [raw_thm] of [thm] => thm | _ => error "Expecting exactly one theorem"; val pats = case pats of [] => Refine_Automation.get_cd_patterns lthy | l => map (Proof_Context.read_term_pattern lthy #> Thm.cterm_of lthy #> Refine_Automation.prepare_cd_pattern lthy) l in Refine_Automation.define_concrete_fun NONE name attribs params thm pats lthy |> snd end)) \ text \ Command: \concrete_definition name [attribs] for params uses thm is patterns\ where \attribs\, \for\, and \is\-parts are optional. Declares a new constant \name\ by matching the theorem \thm\ against a pattern. If the \for\ clause is given, it lists variables in the theorem, and thus determines the order of parameters of the defined constant. Otherwise, parameters will be in order of occurrence. If the \is\ clause is given, it lists patterns. The conclusion of the theorem will be matched against each of these patterns. For the first matching pattern, the constant will be declared to be the term that matches the first non-dummy variable of the pattern. If no \is\-clause is specified, the default patterns will be tried. Attribute: \cd_patterns pats\. Declaration attribute. Declares default patterns for the \concrete_definition\ command. \ declare [[ cd_patterns "(?f,_)\_"]] declare [[ cd_patterns "RETURN ?f \ _" "nres_of ?f \ _"]] declare [[ cd_patterns "(RETURN ?f,_)\_" "(nres_of ?f,_)\_"]] declare [[ cd_patterns "_ = ?f" "_ == ?f" ]] ML \ let val modes = (Scan.optional (@{keyword "("} |-- Parse.list1 Parse.name --| @{keyword ")"}) []) in Outer_Syntax.local_theory @{command_keyword prepare_code_thms} "Refinement framework: Prepare theorems for code generation" (modes -- Parse.thms1 >> (fn (modes,raw_thms) => fn lthy => let val thms = Attrib.eval_thms lthy raw_thms in fold (Refine_Automation.prepare_code_thms_cmd modes) thms lthy end) ) end \ text \ Command: \prepare_code_thms (modes) thm\ where the \(mode)\-part is optional. Set up code-equations for recursions in constant defined by \thm\. The optional \modes\ is a comma-separated list of extraction modes. \ lemma gen_code_thm_RECT: fixes x assumes D: "f \ RECT B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst RECT_unfold) by (rule M) lemma gen_code_thm_REC: fixes x assumes D: "f \ REC B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst REC_unfold) by (rule M) setup \ Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "REC x"}, gen_thm = @{thm gen_code_thm_REC}, gen_tac = Refine_Mono_Prover.mono_tac } #> Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "RECT x"}, gen_thm = @{thm gen_code_thm_RECT}, gen_tac = Refine_Mono_Prover.mono_tac } \ text \ Method \vc_solve (no_pre) clasimp_modifiers rec (add/del): ... solve (add/del): ...\ Named theorems \vcs_rec\ and \vcs_solve\. This method is specialized to solve verification conditions. It first clarsimps all goals, then it tries to apply a set of safe introduction rules (\vcs_rec\, \rec add\). Finally, it applies introduction rules (\vcs_solve\, \solve add\) and tries to discharge all emerging subgoals by auto. If this does not succeed, it backtracks over the application of the solve-rule. \ method_setup vc_solve = \Scan.lift (Args.mode "nopre") --| Method.sections Refine_Automation.vc_solve_modifiers >> (fn (nopre) => fn ctxt => SIMPLE_METHOD ( CHANGED (ALLGOALS (Refine_Automation.vc_solve_tac ctxt nopre)) ))\ "Try to solve verification conditions" end