# HG changeset patch # User berghofe # Date 1224616817 -7200 # Node ID 4593c70e228eeffa15409ff12bc32b6eaa191c98 # Parent 659d64d59f169b50c01ce6790192f42707f1dbc0 More general, still experimental version of nominal_inductive for avoiding sets of names. diff -r 659d64d59f16 -r 4593c70e228e src/HOL/Nominal/nominal_inductive2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Oct 21 21:20:17 2008 +0200 @@ -0,0 +1,487 @@ +(* Title: HOL/Nominal/nominal_inductive2.ML + ID: $Id$ + Author: Stefan Berghofer, TU Muenchen + +Infrastructure for proving equivariance and strong induction theorems +for inductive predicates involving nominal datatypes. +Experimental version that allows to avoid lists of atoms. +*) + +signature NOMINAL_INDUCTIVE2 = +sig + val prove_strong_ind: string -> (string * string list) list -> theory -> Proof.state +end + +structure NominalInductive2 : NOMINAL_INDUCTIVE2 = +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"; + +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); +fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 + (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); + +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 pi th = th RS Drule.cterm_instantiate + [(perm_boolI_pi, pi)] 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); + +fun transp ([] :: _) = [] + | transp xs = map hd xs :: transp (map tl xs); + +fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of + (Const (s, T), ts) => (case strip_type T of + (Ts, Type (tname, _)) => + (case NominalPackage.get_nominal_datatype thy tname of + NONE => fold (add_binders thy i) ts bs + | SOME {descr, index, ...} => (case AList.lookup op = + (#3 (the (AList.lookup op = descr index))) s of + NONE => fold (add_binders thy i) ts bs + | SOME cargs => fst (fold (fn (xs, x) => fn (bs', cargs') => + let val (cargs1, (u, _) :: cargs2) = chop (length xs) cargs' + in (add_binders thy i u + (fold (fn (u, T) => + if exists (fn j => j < i) (loose_bnos u) then I + else AList.map_default op = (T, []) + (insert op aconv (incr_boundvars (~i) u))) + cargs1 bs'), cargs2) + end) cargs (bs, ts ~~ Ts)))) + | _ => fold (add_binders thy i) ts bs) + | (u, ts) => add_binders thy i u (fold (add_binders thy i) ts bs)) + | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs + | add_binders thy i _ bs = bs; + +fun mk_set T [] = Const ("{}", HOLogic.mk_setT T) + | mk_set T (x :: xs) = + Const ("insert", T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ + mk_set T xs; + +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 z. P z (pi_1 o ... o pi_n o t) *) +(* to R ... & id (ALL z. P z (pi_1 o ... o pi_n o t)) *) +(* or id (ALL z. P 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 [@{thm 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 abs_params params t = + let val vs = map (Var o apfst (rpair 0)) (rename_wrt_term t params) + in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end; + +fun inst_params thy (vs, p) th cts = + let val env = Pattern.first_order_match thy (p, prop_of th) + (Vartab.empty, Vartab.empty) + in Thm.instantiate ([], + map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th + end; + +fun prove_strong_ind s avoids thy = + let + val ctxt = ProofContext.init thy; + val ({names, ...}, {raw_induct, intrs, elims, ...}) = + InductivePackage.the_inductive ctxt (Sign.intern_const thy s); + val ind_params = InductivePackage.params_of raw_induct; + val raw_induct = atomize_induct ctxt raw_induct; + val elims = map (atomize_induct ctxt) elims; + val monos = InductivePackage.get_monos ctxt; + val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; + val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of + [] => () + | xs => error ("Missing equivariance theorem for predicate(s): " ^ + commas_quote xs)); + val induct_cases = map fst (fst (RuleCases.get (the + (Induct.lookup_inductP ctxt (hd names))))); + val induct_cases' = if null induct_cases then replicate (length intrs) "" + else induct_cases; + val raw_induct' = Logic.unvarify (prop_of raw_induct); + val elims' = map (Logic.unvarify o prop_of) elims; + val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> + HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); + val ps = map (fst o snd) concls; + + val _ = (case duplicates (op = o pairself fst) avoids of + [] => () + | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs))); + val _ = (case map fst avoids \\ induct_cases of + [] => () + | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)); + fun mk_avoids params name sets = + let + val (_, ctxt') = ProofContext.add_fixes_i + (map (fn (s, T) => (Name.binding s, SOME T, NoSyn)) params) ctxt; + fun mk s = + let + val t = Syntax.read_term ctxt' s; + val t' = list_abs_free (params, t) |> + funpow (length params) (fn Abs (_, _, t) => t) + in (t', HOLogic.dest_setT (fastype_of t)) end + handle TERM _ => + error ("Expression " ^ quote s ^ " to be avoided in case " ^ + quote name ^ " is not a set type"); + val ps = map mk sets + in + case duplicates op = (map snd ps) of + [] => ps + | Ts => error ("More than one set in case " ^ quote name ^ + " for type(s) " ^ commas_quote (map (Syntax.string_of_typ ctxt') Ts)) + end; + + val prems = map (fn (prem, name) => + let + val prems = map (incr_boundvars 1) (Logic.strip_assums_hyp prem); + val concl = incr_boundvars 1 (Logic.strip_assums_concl prem); + val params = Logic.strip_params prem + in + (params, + if null avoids then + map (fn (T, ts) => (mk_set T ts, T)) + (fold (add_binders thy 0) (prems @ [concl]) []) + else case AList.lookup op = avoids name of + NONE => [] + | SOME sets => + map (apfst (incr_boundvars 1)) (mk_avoids params name sets), + prems, strip_comb (HOLogic.dest_Trueprop concl)) + end) (Logic.strip_imp_prems raw_induct' ~~ induct_cases'); + + val atomTs = distinct op = (maps (map snd o #2) prems); + val atoms = map (fst o dest_Type) atomTs; + val ind_sort = if null atomTs then HOLogic.typeS + else Sign.certify_sort thy (map (fn a => Sign.intern_class thy + ("fs_" ^ Sign.base_name a)) atoms); + val fs_ctxt_tyname = Name.variant (map fst (term_tfrees raw_induct')) "'n"; + 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 (t as (f $ u)) = + let val (p, ts) = strip_comb t + in + if p mem ps then + 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) + | lift_prem t = t; + + fun mk_fresh (x, T) = HOLogic.mk_Trueprop + (NominalPackage.fresh_star_const T fsT $ x $ Bound 0); + + val (prems', prems'') = split_list (map (fn (params, sets, prems, (p, ts)) => + let + val params' = params @ [("y", fsT)]; + val prem = Logic.list_implies + (map mk_fresh sets @ + map (fn prem => + if null (term_frees prem inter ps) then prem + else lift_prem prem) prems, + HOLogic.mk_Trueprop (lift_pred p ts)); + in abs_params params' prem end) prems); + + val ind_vars = + (DatatypeProp.indexify_names (replicate (length atomTs) "pi") ~~ + map NominalAtoms.mk_permT atomTs) @ [("z", fsT)]; + val ind_Ts = rev (map snd ind_vars); + + val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, + HOLogic.list_all (ind_vars, lift_pred p + (map (fold_rev (NominalPackage.mk_perm ind_Ts) + (map Bound (length atomTs downto 1))) ts)))) concls)); + + val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, + lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls)); + + val (vc_compat, vc_compat') = map (fn (params, sets, prems, (p, ts)) => + map (fn q => abs_params params (incr_boundvars ~1 (Logic.list_implies + (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)))) + (maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop + (NominalPackage.fresh_star_const U T $ u $ t)) sets) + (ts ~~ binder_types (fastype_of p)) @ + map (fn (u, U) => HOLogic.mk_Trueprop (Const (@{const_name finite}, + HOLogic.mk_setT U --> HOLogic.boolT) $ u)) sets) |> + split_list) prems |> split_list; + + val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; + val pt2_atoms = map (fn a => PureThy.get_thm thy + ("pt_" ^ Sign.base_name a ^ "2")) atoms; + val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss + addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) + addsimprocs [mk_perm_bool_simproc ["Fun.id"], + NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + val fresh_star_bij = PureThy.get_thms thy "fresh_star_bij"; + val pt_insts = map (NominalAtoms.the_atom_info thy #> #pt_inst) atoms; + val at_insts = map (NominalAtoms.the_atom_info thy #> #at_inst) atoms; + val dj_thms = maps (NominalAtoms.the_atom_info thy #> #dj_thms) atoms; + val finite_ineq = map2 (fn th => fn th' => th' RS (th RS + @{thm pt_set_finite_ineq})) pt_insts at_insts; + val perm_set_forget = + map (fn th => th RS @{thm dj_perm_set_forget}) dj_thms; + val perm_freshs_freshs = atomTs ~~ map2 (fn th => fn th' => th' RS (th RS + @{thm pt_freshs_freshs})) pt_insts at_insts; + + fun obtain_fresh_name ts sets (T, fin) (freshs, ths1, ths2, ths3, ctxt) = + let + val thy = ProofContext.theory_of ctxt; + (** protect terms to avoid that fresh_star_prod_set interferes with **) + (** pairs used in introduction rules of inductive predicate **) + fun protect t = + let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end; + val p = foldr1 HOLogic.mk_prod (map protect ts); + val atom = fst (dest_Type T); + val {at_inst, ...} = NominalAtoms.the_atom_info thy atom; + val fs_atom = PureThy.get_thm thy + ("fs_" ^ Sign.base_name atom ^ "1"); + val avoid_th = Drule.instantiate' + [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)] + ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding}); + val (([cx], th1 :: th2 :: ths), ctxt') = Obtain.result + (fn _ => EVERY + [rtac avoid_th 1, + full_simp_tac (HOL_ss addsimps [@{thm fresh_star_prod_set}]) 1, + full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1, + rotate_tac 1 1, + REPEAT (etac conjE 1)]) + [] ctxt; + val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets); + val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2); + val (pis1, pis2) = chop (length Ts1) + (map Bound (length pTs - 1 downto 0)); + val _ $ (f $ (_ $ pi $ l) $ r) = prop_of th2 + val th2' = + Goal.prove ctxt [] [] + (list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop + (f $ fold_rev (NominalPackage.mk_perm (rev pTs)) + (pis1 @ pi :: pis2) l $ r))) + (fn _ => cut_facts_tac [th2] 1 THEN + full_simp_tac (HOL_basic_ss addsimps perm_set_forget) 1) |> + Simplifier.simplify eqvt_ss + in + (freshs @ [term_of cx], + ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt') + end; + + fun mk_ind_proof thy thss = + Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} => + let val th = Goal.prove ctxt [] [] concl (fn {context, ...} => + rtac raw_induct 1 THEN + EVERY (maps (fn (((((_, sets, oprems, _), + vc_compat_ths), vc_compat_vs), ihyp), vs_ihypt) => + [REPEAT (rtac allI 1), simp_tac eqvt_ss 1, + SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} => + let + val (cparams', (pis, z)) = + chop (length params - length atomTs - 1) params ||> + (map term_of #> split_last); + val params' = map term_of cparams' + val sets' = map (apfst (curry subst_bounds (rev params'))) sets; + val pi_sets = map (fn (t, _) => + fold_rev (NominalPackage.mk_perm []) pis t) sets'; + val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl)); + val gprems1 = List.mapPartial (fn (th, t) => + if null (term_frees t inter ps) then SOME th + else + map_thm ctxt' (split_conj (K o I) names) + (etac conjunct1 1) monos NONE th) + (gprems ~~ oprems); + val vc_compat_ths' = map2 (fn th => fn p => + let + val th' = gprems1 MRS inst_params thy p th cparams'; + val (h, ts) = + strip_comb (HOLogic.dest_Trueprop (concl_of th')) + in + Goal.prove ctxt' [] [] + (HOLogic.mk_Trueprop (list_comb (h, + map (fold_rev (NominalPackage.mk_perm []) pis) ts))) + (fn _ => simp_tac (HOL_basic_ss addsimps + (fresh_star_bij @ finite_ineq)) 1 THEN rtac th' 1) + end) vc_compat_ths vc_compat_vs; + val (vc_compat_ths1, vc_compat_ths2) = + chop (length vc_compat_ths - length sets) vc_compat_ths'; + val vc_compat_ths1' = map + (Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv + (Simplifier.rewrite eqvt_ss)))) vc_compat_ths1; + val (pis', fresh_ths1, fresh_ths2, fresh_ths3, ctxt'') = fold + (obtain_fresh_name ts sets) + (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], ctxt'); + 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_rev (concat_perm #> map) pis' pis; + val ihyp' = inst_params thy vs_ihypt ihyp + (map (fold_rev (NominalPackage.mk_perm []) + (pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]); + fun mk_pi th = + Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}] + addsimprocs [NominalPackage.perm_simproc]) + (Simplifier.simplify eqvt_ss + (fold_rev (mk_perm_bool o cterm_of thy) + (pis' @ pis) th)); + val gprems2 = map (fn (th, t) => + if null (term_frees t inter ps) then mk_pi th + else + 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); + val perm_freshs_freshs' = map (fn (th, (_, T)) => + th RS the (AList.lookup op = perm_freshs_freshs T)) + (fresh_ths2 ~~ sets); + val th = Goal.prove ctxt'' [] [] + (HOLogic.mk_Trueprop (list_comb (P $ hd ts, + map (fold_rev (NominalPackage.mk_perm []) pis') (tl ts)))) + (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1] @ + map (fn th => rtac th 1) fresh_ths3 @ + [REPEAT_DETERM_N (length gprems) + (simp_tac (HOL_basic_ss + addsimps [inductive_forall_def'] + addsimprocs [NominalPackage.perm_simproc]) 1 THEN + resolve_tac gprems2 1)])); + val final = Goal.prove ctxt'' [] [] (term_of concl) + (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss + addsimps vc_compat_ths1' @ fresh_ths1 @ + perm_freshs_freshs') 1); + val final' = ProofContext.export ctxt'' ctxt' [final]; + in resolve_tac final' 1 end) context 1]) + (prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems''))) + in + cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN + REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN + etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN + asm_full_simp_tac (simpset_of thy) 1) + end); + + in + thy |> + ProofContext.init |> + Proof.theorem_i NONE (fn thss => ProofContext.theory (fn thy => + let + 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 induct_cases' = InductivePackage.partition_rules' raw_induct + (intrs ~~ induct_cases); + val thss' = map (map atomize_intr) thss; + val thsss = InductivePackage.partition_rules' raw_induct (intrs ~~ thss'); + val strong_raw_induct = + mk_ind_proof thy thss' |> InductivePackage.rulify; + val strong_induct = + if length names > 1 then + (strong_raw_induct, [ind_case_names, RuleCases.consumes 0]) + else (strong_raw_induct RSN (2, rev_mp), + [ind_case_names, RuleCases.consumes 1]); + val ([strong_induct'], thy') = thy |> + Sign.add_path rec_name |> + PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)]; + val strong_inducts = + ProjectRule.projects ctxt (1 upto length names) strong_induct' + in + thy' |> + PureThy.add_thmss [(("strong_inducts", strong_inducts), + [ind_case_names, RuleCases.consumes 1])] |> snd |> + Sign.parent_path + end)) + (map (map (rulify_term thy #> rpair [])) vc_compat) + end; + + +(* outer syntax *) + +local structure P = OuterParse and K = OuterKeyword in + +val _ = + OuterSyntax.command "nominal_inductive2" + "prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal + (P.name -- Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name -- + (P.$$$ ":" |-- P.and_list1 P.term))) [] >> (fn (name, avoids) => + Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids))); + +end; + +end