diff -r a8724924a62e -r 13ab4f0a0b0e Nominal/nominal_eqvt.ML --- a/Nominal/nominal_eqvt.ML Tue Mar 26 16:41:31 2013 +0100 +++ b/Nominal/nominal_eqvt.ML Wed Mar 27 16:08:30 2013 +0100 @@ -1,14 +1,14 @@ (* Title: nominal_eqvt.ML Author: Stefan Berghofer (original code) Author: Christian Urban + Author: Tjark Weber Automatic proofs for equivariance of inductive predicates. *) - signature NOMINAL_EQVT = sig - val raw_equivariance: term list -> thm -> thm list -> Proof.context -> thm list + val raw_equivariance: Proof.context -> term list -> thm -> thm list -> thm list val equivariance_cmd: string -> Proof.context -> local_theory end @@ -18,24 +18,26 @@ open Nominal_Permeq; open Nominal_ThmDecls; -val atomize_conv = +val atomize_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) - (HOL_basic_ss addsimps @{thms induct_atomize}); -val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); + (HOL_basic_ss addsimps @{thms induct_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)); + (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)) (** equivariance tactics **) -fun eqvt_rel_single_case_tac ctxt pred_names pi intro = +fun eqvt_rel_single_case_tac ctxt pred_names pi intro = let val thy = Proof_Context.theory_of ctxt val cpi = Thm.cterm_of thy pi val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} val eqvt_sconfig = eqvt_strict_config addexcls pred_names val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all} - val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)} + val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)} in eqvt_tac ctxt eqvt_sconfig THEN' SUBPROOF (fn {prems, context as ctxt, ...} => @@ -43,9 +45,8 @@ val prems' = map (transform_prem2 ctxt pred_names) prems val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' val prems''' = map (simplify simps2 o simplify simps1) prems'' - in - HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) + HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) end) ctxt end @@ -57,78 +58,88 @@ end -(** equivariance procedure *) +(** equivariance procedure **) -fun prepare_goal pi pred = +fun prepare_goal ctxt pi pred_with_args = let - val (c, xs) = strip_comb pred; + val (c, xs) = strip_comb pred_with_args + fun is_nonfixed_Free (Free (s, _)) = not (Variable.is_fixed ctxt s) + | is_nonfixed_Free _ = false + fun mk_perm_nonfixed_Free t = + if is_nonfixed_Free t then mk_perm pi t else t in - HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) + HOLogic.mk_imp (pred_with_args, + list_comb (c, map mk_perm_nonfixed_Free xs)) end -(* stores thm under name.eqvt and adds [eqvt]-attribute *) +fun name_of (Const (s, _)) = s -fun get_name (Const (a, _)) = a - | get_name (Free (a, _)) = a - -fun raw_equivariance pred_trms raw_induct intrs ctxt = +fun raw_equivariance ctxt preds raw_induct intrs = let - val is_already_eqvt = - filter (is_eqvt ctxt) pred_trms - |> map (Syntax.string_of_term ctxt) + (* FIXME: polymorphic predicates should either be rejected or + specialized to arguments of sort pt *) + + val is_already_eqvt = filter (is_eqvt ctxt) preds val _ = if null is_already_eqvt then () - else error ("Already equivariant: " ^ commas is_already_eqvt) + else error ("Already equivariant: " ^ commas + (map (Syntax.string_of_term ctxt) is_already_eqvt)) - val pred_names = map get_name pred_trms + val pred_names = map (name_of o head_of) preds val raw_induct' = atomize_induct ctxt raw_induct val intrs' = map atomize_intr intrs - - val (([raw_concl], [raw_pi]), ctxt') = - ctxt - |> Variable.import_terms false [concl_of raw_induct'] + + val (([raw_concl], [raw_pi]), ctxt') = + ctxt + |> Variable.import_terms false [concl_of raw_induct'] ||>> Variable.variant_fixes ["p"] val pi = Free (raw_pi, @{typ perm}) - - val preds = map (fst o HOLogic.dest_imp) - (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); - - val goal = HOLogic.mk_Trueprop - (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) - in - Goal.prove ctxt' [] [] goal - (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) - |> Datatype_Aux.split_conj_thm + + val preds_with_args = raw_concl + |> HOLogic.dest_Trueprop + |> HOLogic.dest_conj + |> map (fst o HOLogic.dest_imp) + + val goal = preds_with_args + |> map (prepare_goal ctxt pi) + |> foldr1 HOLogic.mk_conj + |> HOLogic.mk_Trueprop + in + Goal.prove ctxt' [] [] goal + (fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) + |> Datatype_Aux.split_conj_thm |> Proof_Context.export ctxt' ctxt |> map (fn th => th RS mp) |> map zero_var_indexes end -fun note_named_thm (name, thm) ctxt = +(** stores thm under name.eqvt and adds [eqvt]-attribute **) + +fun note_named_thm (name, thm) ctxt = let - val thm_name = Binding.qualified_name + val thm_name = Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt") val attr = Attrib.internal (K eqvt_add) - val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt + val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt in (thm', ctxt') end + +(** equivariance command **) + fun equivariance_cmd pred_name ctxt = let - val thy = Proof_Context.theory_of ctxt val ({names, ...}, {preds, raw_induct, intrs, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) - val thms = raw_equivariance preds raw_induct intrs ctxt + Inductive.the_inductive ctxt (long_name ctxt pred_name) + val thms = raw_equivariance ctxt preds raw_induct intrs in fold_map note_named_thm (names ~~ thms) ctxt |> snd end - val _ = Outer_Syntax.local_theory @{command_spec "equivariance"} - "Proves equivariance for inductive predicate involving nominal datatypes." - (Parse.xname >> equivariance_cmd) - + "Proves equivariance for inductive predicate involving nominal datatypes." + (Parse.const >> equivariance_cmd) end (* structure *)