--- a/Nominal/nominal_dt_alpha.ML Wed Jun 29 17:01:09 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML Wed Jun 29 19:21:26 2011 +0100
@@ -13,18 +13,18 @@
bclause list list list -> term list -> Proof.context ->
term list * term list * thm list * thm list * thm * local_theory
- val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list ->
- term list -> string list -> thm list
-
- val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list ->
- thm list -> thm list
-
val induct_prove: typ list -> (typ * (term -> term)) list -> thm ->
(Proof.context -> int -> tactic) -> Proof.context -> thm list
val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm ->
(Proof.context -> int -> tactic) -> Proof.context -> thm list
+ val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list ->
+ term list -> string list -> thm list
+
+ val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list ->
+ thm list -> thm list
+
val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list
val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list ->
@@ -53,6 +53,7 @@
fun lookup xs x = the (AList.lookup (op=) xs x)
fun group xs = AList.group (op=) xs
+
(** definition of the inductive rules for alpha and alpha_bn **)
(* construct the compound terms for prod_fv and prod_alpha *)
@@ -276,9 +277,97 @@
end
+(** induction proofs **)
+
+
+(* proof by structural induction over data types *)
+
+fun induct_prove tys props induct_thm cases_tac ctxt =
+ let
+ val (arg_names, ctxt') =
+ Variable.variant_fixes (replicate (length tys) "x") ctxt
+
+ val args = map2 (curry Free) arg_names tys
+
+ val true_trms = replicate (length tys) (K @{term True})
+
+ fun apply_all x fs = map (fn f => f x) fs
+
+ val goals =
+ group (props @ (tys ~~ true_trms))
+ |> map snd
+ |> map2 apply_all args
+ |> map fold_conj
+ |> foldr1 HOLogic.mk_conj
+ |> HOLogic.mk_Trueprop
+
+ fun tac ctxt =
+ HEADGOAL
+ (DETERM o (rtac induct_thm)
+ THEN_ALL_NEW
+ (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
+ in
+ Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
+ |> singleton (ProofContext.export ctxt' ctxt)
+ |> Datatype_Aux.split_conj_thm
+ |> map Datatype_Aux.split_conj_thm
+ |> flat
+ |> filter_out (is_true o concl_of)
+ |> map zero_var_indexes
+ end
+
+(* proof by rule induction over the alpha-definitions *)
+
+fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
+ let
+ val arg_tys = map (domain_type o fastype_of) alphas
+
+ val ((arg_names1, arg_names2), ctxt') =
+ ctxt
+ |> Variable.variant_fixes (replicate (length alphas) "x")
+ ||>> Variable.variant_fixes (replicate (length alphas) "y")
+
+ val args1 = map2 (curry Free) arg_names1 arg_tys
+ val args2 = map2 (curry Free) arg_names2 arg_tys
+
+ val true_trms = replicate (length alphas) (K @{term True})
+
+ fun apply_all x fs = map (fn f => f x) fs
+
+ val goals_rhs =
+ group (props @ (alphas ~~ true_trms))
+ |> map snd
+ |> map2 apply_all (args1 ~~ args2)
+ |> map fold_conj
+
+ fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
+ val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
+
+ val goals =
+ (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
+ |> foldr1 HOLogic.mk_conj
+ |> HOLogic.mk_Trueprop
+
+ fun tac ctxt =
+ HEADGOAL
+ (DETERM o (rtac alpha_induct_thm)
+ THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
+ in
+ Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
+ |> singleton (ProofContext.export ctxt' ctxt)
+ |> Datatype_Aux.split_conj_thm
+ |> map (fn th => th RS mp)
+ |> map Datatype_Aux.split_conj_thm
+ |> flat
+ |> filter_out (is_true o concl_of)
+ |> map zero_var_indexes
+ end
+
+
(** produces the distinctness theorems **)
+
(* transforms the distinctness theorems of the constructors
into "not-alphas" of the constructors *)
fun mk_distinct_goal ty_trm_assoc neq =
@@ -296,7 +385,6 @@
rtac notI THEN' eresolve_tac cases_thms
THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
-
fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str =
let
val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms)
@@ -353,91 +441,6 @@
end
-(** proof by induction over types **)
-
-fun induct_prove tys props induct_thm cases_tac ctxt =
- let
- val (arg_names, ctxt') =
- Variable.variant_fixes (replicate (length tys) "x") ctxt
-
- val args = map2 (curry Free) arg_names tys
-
- val true_trms = replicate (length tys) (K @{term True})
-
- fun apply_all x fs = map (fn f => f x) fs
-
- val goals =
- group (props @ (tys ~~ true_trms))
- |> map snd
- |> map2 apply_all args
- |> map fold_conj
- |> foldr1 HOLogic.mk_conj
- |> HOLogic.mk_Trueprop
-
- fun tac ctxt =
- HEADGOAL
- (DETERM o (rtac induct_thm)
- THEN_ALL_NEW
- (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
- in
- Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
- |> singleton (ProofContext.export ctxt' ctxt)
- |> Datatype_Aux.split_conj_thm
- |> map Datatype_Aux.split_conj_thm
- |> flat
- |> filter_out (is_true o concl_of)
- |> map zero_var_indexes
- end
-
-
-(** proof by induction over the alpha-definitions **)
-
-fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
- let
- val arg_tys = map (domain_type o fastype_of) alphas
-
- val ((arg_names1, arg_names2), ctxt') =
- ctxt
- |> Variable.variant_fixes (replicate (length alphas) "x")
- ||>> Variable.variant_fixes (replicate (length alphas) "y")
-
- val args1 = map2 (curry Free) arg_names1 arg_tys
- val args2 = map2 (curry Free) arg_names2 arg_tys
-
- val true_trms = replicate (length alphas) (K @{term True})
-
- fun apply_all x fs = map (fn f => f x) fs
-
- val goals_rhs =
- group (props @ (alphas ~~ true_trms))
- |> map snd
- |> map2 apply_all (args1 ~~ args2)
- |> map fold_conj
-
- fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
- val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
-
- val goals =
- (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
- |> foldr1 HOLogic.mk_conj
- |> HOLogic.mk_Trueprop
-
- fun tac ctxt =
- HEADGOAL
- (DETERM o (rtac alpha_induct_thm)
- THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
- in
- Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
- |> singleton (ProofContext.export ctxt' ctxt)
- |> Datatype_Aux.split_conj_thm
- |> map (fn th => th RS mp)
- |> map Datatype_Aux.split_conj_thm
- |> flat
- |> filter_out (is_true o concl_of)
- |> map zero_var_indexes
- end
-
-
(** reflexivity proof for the alphas **)
val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}