--- a/Nominal-General/nominal_eqvt.ML Wed Apr 14 15:02:07 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML Wed Apr 14 16:05:58 2010 +0200
@@ -1,5 +1,5 @@
(* Title: nominal_eqvt.ML
- Author: Stefan Berghofer
+ Author: Stefan Berghofer (original code)
Author: Christian Urban
Automatic proofs for equivariance of inductive predicates.
@@ -7,7 +7,9 @@
signature NOMINAL_EQVT =
sig
- val eqvt_rel_tac : xstring -> Proof.context -> local_theory
+ val equivariance: string -> Proof.context -> local_theory
+ val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
+ val eqvt_rel_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
end
structure Nominal_Eqvt : NOMINAL_EQVT =
@@ -23,6 +25,13 @@
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
(Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
+
+(**
+ proves F[f t] from F[t] which is the given theorem
+ - F needs to be monotone
+ - f returns either SOME for a term it fires
+ and NONE elsewhere
+**)
fun map_term f t =
(case f t of
NONE => map_term' f t
@@ -48,24 +57,21 @@
REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
end
-(*
- proves F[f t] from F[t] where F[t] is the given theorem
-
- - F needs to be monotone
- - f returns either SOME for a term it fires
- and NONE elsewhere
-*)
fun map_thm ctxt f tac thm =
let
val opt_goal_trm = map_term f (prop_of thm)
- fun prove goal =
- Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)
in
case opt_goal_trm of
NONE => thm
- | SOME goal => prove goal
+ | 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 picks out
+ the part P ...
+*)
fun transform_prem ctxt names thm =
let
fun split_conj names (Const ("op &", _) $ p $ q) =
@@ -77,36 +83,50 @@
map_thm ctxt (split_conj names) (etac conjunct2 1) thm
end
-fun single_case_tac ctxt pred_names pi intro =
+
+(** equivariance tactics **)
+
+fun eqvt_rel_case_tac ctxt pred_names pi intro =
let
val thy = ProofContext.theory_of ctxt
val cpi = Thm.cterm_of thy (mk_minus pi)
val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE}
+ val permute_cancel = @{thms permute_minus_cancel(2)}
in
eqvt_strict_tac ctxt [] [] THEN'
- SUBPROOF (fn {prems, context as ctxt, ...} =>
+ SUBPROOF (fn {prems, context, ...} =>
let
val prems' = map (transform_prem ctxt pred_names) prems
val side_cond_tac = EVERY'
- [ rtac rule,
- eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],
+ [ rtac rule, eqvt_strict_tac context permute_cancel [],
resolve_tac prems' ]
in
- HEADGOAL (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac))
+ (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 1
end) ctxt
end
+fun eqvt_rel_tac ctxt pred_names pi induct intros =
+let
+ val cases = map (eqvt_rel_case_tac ctxt pred_names pi) intros
+in
+ EVERY' (rtac induct :: cases)
+end
-fun prepare_pred params_no pi pred =
+
+(** equivariance procedure *)
+
+(* sets up goal and makes sure parameters
+ are untouched PROBLEM: this violates the
+ form of eqvt lemmas *)
+fun prepare_goal params_no pi pred =
let
val (c, xs) = strip_comb pred;
val (xs1, xs2) = chop params_no xs
in
- HOLogic.mk_imp
- (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2))
+ HOLogic.mk_imp (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2))
end
-
+(* stores thm under name.eqvt and adds [eqvt]-attribute *)
fun note_named_thm (name, thm) ctxt =
let
val thm_name = Binding.qualified_name
@@ -116,30 +136,28 @@
Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
end
-
-fun eqvt_rel_tac pred_name ctxt =
+fun equivariance pred_name ctxt =
let
val thy = ProofContext.theory_of ctxt
val ({names, ...}, {raw_induct, intrs, ...}) =
Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
- val raw_induct = atomize_induct ctxt raw_induct;
- val intros = map atomize_intr intrs;
+ val raw_induct = atomize_induct ctxt raw_induct
+ val intros = map atomize_intr intrs
val params_no = length (Inductive.params_of raw_induct)
- 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 ["pi"]
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_pred params_no pi) preds))
- val thm = Goal.prove ctxt' [] [] goal (fn {context,...} =>
- HEADGOAL (EVERY' (rtac raw_induct :: map (single_case_tac context names pi) intros)))
- |> singleton (ProofContext.export ctxt' ctxt)
- val thms = map (fn th => zero_var_indexes (th RS mp)) (Datatype_Aux.split_conj_thm thm)
+ (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds))
+ val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal
+ (fn {context,...} => eqvt_rel_tac context names pi raw_induct intros 1)
+ |> singleton (ProofContext.export ctxt' ctxt))
+ val thms' = map (fn th => zero_var_indexes (th RS mp)) thms
in
- ctxt |> fold_map note_named_thm (names ~~ thms)
- |> snd
+ ctxt |> fold_map note_named_thm (names ~~ thms') |> snd
end
@@ -147,9 +165,8 @@
val _ =
OuterSyntax.local_theory "equivariance"
- "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
- (P.xname >> eqvt_rel_tac);
-
+ "prove equivariance for inductive predicate involving nominal datatypes"
+ K.thy_decl (P.xname >> equivariance);
end;
end (* structure *)
\ No newline at end of file