--- 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 *)