# HG changeset patch # User berghofe # Date 1189699919 -7200 # Node ID 621b60b1df00d33332352964bb3c7ed6abe0f11f # Parent c80e1871098b64a6393716d209954c7534846ab9 Generalized equivariance and nominal_inductive commands to inductive definitions involving arbitrary monotone operators. diff -r c80e1871098b -r 621b60b1df00 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Sep 13 18:08:08 2007 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Sep 13 18:11:59 2007 +0200 @@ -15,14 +15,41 @@ structure NominalInductive : NOMINAL_INDUCTIVE = struct +val inductive_forall_name = "HOL.induct_forall"; +val inductive_forall_def = thm "induct_forall_def"; +val inductive_atomize = thms "induct_atomize"; +val inductive_rulify = thms "induct_rulify"; +val inductive_rulify_fallback = thms "induct_rulify_fallback"; + +val rulify = + hol_simplify inductive_rulify + #> hol_simplify inductive_rulify_fallback; + +fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify []; + +val atomize_conv = + MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) + (HOL_basic_ss addsimps inductive_atomize); +val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); +val atomize_induct = Conv.fconv_rule (Conv.prems_conv ~1 + (Conv.forall_conv ~1 (Conv.prems_conv ~1 atomize_conv))); + val finite_Un = thm "finite_Un"; val supp_prod = thm "supp_prod"; val fresh_prod = thm "fresh_prod"; +val perm_bool = mk_meta_eq (thm "perm_bool"); val perm_boolI = thm "perm_boolI"; val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb (Drule.strip_imp_concl (cprop_of perm_boolI)))); +fun mk_perm_bool_simproc names = Simplifier.simproc_i + (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => + fn Const ("Nominal.perm", _) $ _ $ t => + if the_default "" (try (head_of #> dest_Const #> fst) t) mem names + then SOME perm_bool else NONE + | _ => NONE); + val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE; fun transp ([] :: _) = [] @@ -49,11 +76,77 @@ | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs | add_binders thy i _ bs = bs; +fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of + Const (name, _) => + if name mem names then SOME (f p q) else NONE + | _ => NONE) + | split_conj _ _ _ _ = NONE; + +fun strip_all [] t = t + | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t; + +(*********************************************************************) +(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *) +(* or ALL pi_1 ... pi_n. P (pi_1 o ... o pi_n o t) *) +(* to R ... & id (ALL z. (pi_1 o ... o pi_n o t)) *) +(* or id (ALL z. (pi_1 o ... o pi_n o t)) *) +(* *) +(* where "id" protects the subformula from simplification *) +(*********************************************************************) + +fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ = + (case head_of p of + Const (name, _) => + if name mem names then SOME (HOLogic.mk_conj (p, + Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ + (subst_bounds (pis, strip_all pis q)))) + else NONE + | _ => NONE) + | inst_conj_all names ps pis t u = + if member (op aconv) ps (head_of u) then + SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ + (subst_bounds (pis, strip_all pis t))) + else NONE + | inst_conj_all _ _ _ _ _ = NONE; + +fun inst_conj_all_tac k = EVERY + [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]), + REPEAT_DETERM_N k (etac allE 1), + simp_tac (HOL_basic_ss addsimps [id_apply]) 1]; + +fun map_term f t u = (case f t u of + NONE => map_term' f t u | x => x) +and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u 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)) (Abs (s', T', t')) = (case map_term f t t' of + NONE => NONE + | SOME t'' => SOME (Abs (s, T, t''))) + | map_term' _ _ _ = NONE; + +(*********************************************************************) +(* Prove F[f t] from F[t], where F is monotone *) +(*********************************************************************) + +fun map_thm ctxt f tac monos opt th = + let + val prop = prop_of th; + fun prove t = + Goal.prove ctxt [] [] t (fn _ => + EVERY [cut_facts_tac [th] 1, etac rev_mp 1, + REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), + REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) + in Option.map prove (map_term f prop (the_default prop opt)) end; + fun prove_strong_ind s avoids thy = let val ctxt = ProofContext.init thy; val ({names, ...}, {raw_induct, ...}) = InductivePackage.the_inductive ctxt (Sign.intern_const thy s); + val raw_induct = atomize_induct raw_induct; + val monos = InductivePackage.get_monos ctxt; val eqvt_thms = NominalThmDecls.get_eqvt_thms thy; val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of [] => () @@ -104,24 +197,20 @@ val fs_ctxt_name = Name.variant (add_term_names (raw_induct', [])) "z"; val fsT = TFree (fs_ctxt_tyname, ind_sort); + val inductive_forall_def' = Drule.instantiate' + [SOME (ctyp_of thy fsT)] [] inductive_forall_def; + fun lift_pred' t (Free (s, T)) ts = list_comb (Free (s, fsT --> T), t :: ts); val lift_pred = lift_pred' (Bound 0); - fun lift_prem (Const ("Trueprop", _) $ t) = - let val (u, ts) = strip_comb t - in - if u mem ps then - all fsT $ Abs ("z", fsT, HOLogic.mk_Trueprop - (lift_pred u (map (incr_boundvars 1) ts))) - else HOLogic.mk_Trueprop (lift_prem t) - end - | lift_prem (t as (f $ u)) = + fun lift_prem (t as (f $ u)) = let val (p, ts) = strip_comb t in if p mem ps then - HOLogic.all_const fsT $ Abs ("z", fsT, - lift_pred p (map (incr_boundvars 1) ts)) + Const (inductive_forall_name, + (fsT --> HOLogic.boolT) --> HOLogic.boolT) $ + Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) else lift_prem f $ lift_prem u end | lift_prem (Abs (s, T, t)) = Abs (s, T, lift_prem t) @@ -167,13 +256,19 @@ val vc_compat = map (fn (params, bvars, prems, (p, ts)) => map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies - (filter (fn prem => null (ps inter term_frees prem)) prems, q)))) + (List.mapPartial (fn prem => + if null (ps inter term_frees prem) then SOME prem + else map_term (split_conj (K o I) names) prem prem) prems, q)))) (mk_distinct bvars @ maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop (Const ("Nominal.fresh", U --> T --> HOLogic.boolT) $ u $ t)) bvars) (ts ~~ binder_types (fastype_of p)))) prems; - val eqvt_ss = HOL_basic_ss addsimps eqvt_thms; + val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp"); + val pt2_atoms = map (fn aT => PureThy.get_thm thy + (Name ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2"))) atomTs; + val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) + addsimprocs [mk_perm_bool_simproc ["Fun.id"]]; val fresh_bij = PureThy.get_thms thy (Name "fresh_bij"); val perm_bij = PureThy.get_thms thy (Name "perm_bij"); val fs_atoms = map (fn aT => PureThy.get_thm thy @@ -182,8 +277,6 @@ val fresh_atm = PureThy.get_thms thy (Name "fresh_atm"); val calc_atm = PureThy.get_thms thy (Name "calc_atm"); val perm_fresh_fresh = PureThy.get_thms thy (Name "perm_fresh_fresh"); - val pt2_atoms = map (fn aT => PureThy.get_thm thy - (Name ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) RS sym) atomTs; fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) = let @@ -231,14 +324,35 @@ (map snd bvars') ([], [], ctxt'); val freshs2' = NominalPackage.mk_not_sym freshs2; val pis' = map NominalPackage.perm_of_pair (pi_bvars ~~ freshs1); + fun concat_perm pi1 pi2 = + let val T = fastype_of pi1 + in if T = fastype_of pi2 then + Const ("List.append", T --> T --> T) $ pi1 $ pi2 + else pi2 + end; + val pis'' = fold (concat_perm #> map) pis' pis; val env = Pattern.first_order_match thy (ihypt, prop_of ihyp) (Vartab.empty, Vartab.empty); val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy)) (map (Envir.subst_vars env) vs ~~ map (fold_rev (NominalPackage.mk_perm []) (rev pis' @ pis)) params' @ [z])) ihyp; - val (gprems1, gprems2) = pairself (map fst) (List.partition - (fn (th, t) => null (term_frees t inter ps)) (gprems ~~ oprems)); + fun mk_pi th = + Simplifier.simplify (HOL_basic_ss addsimps [id_apply] + addsimprocs [NominalPackage.perm_simproc]) + (Simplifier.simplify eqvt_ss + (fold_rev (fn pi => fn th' => th' RS Drule.cterm_instantiate + [(perm_boolI_pi, cterm_of thy pi)] perm_boolI) + (rev pis' @ pis) th)); + val (gprems1, gprems2) = split_list + (map (fn (th, t) => + if null (term_frees t inter ps) then (SOME th, mk_pi th) + else + (map_thm ctxt (split_conj (K o I) names) + (etac conjunct1 1) monos NONE th, + mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis'')) + (inst_conj_all_tac (length pis'')) monos (SOME t) th)))) + (gprems ~~ oprems)) |>> List.mapPartial I; val vc_compat_ths' = map (fn th => let val th' = gprems1 MRS @@ -258,11 +372,6 @@ in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end) vc_compat_ths; val vc_compat_ths'' = NominalPackage.mk_not_sym vc_compat_ths'; - val gprems1' = map (fn th => fold_rev (fn pi => fn th' => - Simplifier.simplify eqvt_ss (th' RS Drule.cterm_instantiate - [(perm_boolI_pi, cterm_of thy pi)] perm_boolI)) - (rev pis' @ pis) th) gprems1; - val gprems2' = map (Simplifier.simplify eqvt_ss) gprems2; (** Since calc_atm simplifies (pi :: 'a prm) o (x :: 'b) to x **) (** we have to pre-simplify the rewrite rules **) val calc_atm_ss = HOL_ss addsimps calc_atm @ @@ -275,8 +384,8 @@ REPEAT_DETERM_N (nprems_of ihyp - length gprems) (simp_tac calc_atm_ss 1), REPEAT_DETERM_N (length gprems) - (resolve_tac gprems1' 1 ORELSE - simp_tac (HOL_basic_ss addsimps pt2_atoms @ gprems2' + (simp_tac (HOL_ss + addsimps inductive_forall_def' :: gprems2 addsimprocs [NominalPackage.perm_simproc]) 1)])); val final = Goal.prove ctxt'' [] [] (term_of concl) (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss @@ -301,7 +410,9 @@ val ctxt = ProofContext.init thy; val rec_name = space_implode "_" (map Sign.base_name names); val ind_case_names = RuleCases.case_names induct_cases; - val strong_raw_induct = mk_proof thy thss; + val strong_raw_induct = + mk_proof thy (map (map atomize_intr) thss) |> + rulify |> MetaSimplifier.norm_hhf; val strong_induct = if length names > 1 then (strong_raw_induct, [ind_case_names, RuleCases.consumes 0]) @@ -318,7 +429,7 @@ [ind_case_names, RuleCases.consumes 1])] |> snd |> Theory.parent_path end)) - (map (map (rpair [])) vc_compat) + (map (map (rulify_term thy #> rpair [])) vc_compat) end; fun prove_eqvt s xatoms thy = @@ -326,6 +437,10 @@ val ctxt = ProofContext.init thy; val ({names, ...}, {raw_induct, intrs, elims, ...}) = InductivePackage.the_inductive ctxt (Sign.intern_const thy s); + val raw_induct = atomize_induct raw_induct; + val elims = map atomize_induct elims; + val intrs = map atomize_intr intrs; + val monos = InductivePackage.get_monos ctxt; val intrs' = InductivePackage.unpartition_rules intrs (map (fn (((s, ths), (_, k)), th) => (s, ths ~~ InductivePackage.infer_intro_vars th k ths)) @@ -344,7 +459,10 @@ | xs => error ("No such atoms: " ^ commas xs); atoms) end; - val eqvt_ss = HOL_basic_ss addsimps NominalThmDecls.get_eqvt_thms thy; + val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp"); + val eqvt_ss = HOL_basic_ss addsimps + (NominalThmDecls.get_eqvt_thms thy @ perm_pi_simp) addsimprocs + [mk_perm_bool_simproc names]; val t = Logic.unvarify (concl_of raw_induct); val pi = Name.variant (add_term_names (t, [])) "pi"; val ps = map (fst o HOLogic.dest_imp) @@ -357,13 +475,14 @@ (Logic.unvarify (prop_of intr)) ^ "\n" ^ s); val res = SUBPROOF (fn {prems, params, ...} => let - val prems' = map (fn th' => Simplifier.simplify eqvt_ss - (if null (names inter term_consts (prop_of th')) then th' RS th - else th')) prems; + val prems' = map (fn th => the_default th (map_thm ctxt + (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; + val prems'' = map (fn th' => + Simplifier.simplify eqvt_ss (th' RS th)) prems'; val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~ map (cterm_of thy o NominalPackage.mk_perm [] pi o term_of) params) intr - in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems')) 1 + in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 end) ctxt 1 st in case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of