--- a/Nominal/nominal_dt_alpha.ML Wed Jun 29 19:21:26 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML Wed Jun 29 23:08:44 2011 +0100
@@ -11,7 +11,7 @@
val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list ->
bclause list list list -> term list -> Proof.context ->
- term list * term list * thm list * thm list * thm * local_theory
+ term list * term list * thm list * thm list * thm * alpha_result * local_theory
val induct_prove: typ list -> (typ * (term -> term)) list -> thm ->
(Proof.context -> int -> tactic) -> Proof.context -> thm list
@@ -19,19 +19,13 @@
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 ->
- Proof.context -> thm list
- val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list ->
- Proof.context -> thm list * thm list
-
+ val raw_prove_alpha_distincts: Proof.context -> alpha_result -> thm list -> string list -> thm list
+ val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> thm list -> thm list -> thm list
+ val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list
+ val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list
+ val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list
+ val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list ->
+ thm list * thm list
val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list ->
term list -> thm -> thm list -> Proof.context -> thm list
@@ -49,6 +43,7 @@
struct
open Nominal_Permeq
+open Nominal_Dt_Data
fun lookup xs x = the (AList.lookup (op=) xs x)
fun group xs = AList.group (op=) xs
@@ -253,27 +248,50 @@
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
- val (alphas, lthy') = Inductive.add_inductive_i
+ val (alpha_info, lthy') = Inductive.add_inductive_i
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
all_alpha_names [] all_alpha_intros [] lthy
- val all_alpha_trms_loc = #preds alphas;
- val alpha_induct_loc = #raw_induct alphas;
- val alpha_intros_loc = #intrs alphas;
- val alpha_cases_loc = #elims alphas;
+ val all_alpha_trms_loc = #preds alpha_info;
+ val alpha_raw_induct_loc = #raw_induct alpha_info;
+ val alpha_intros_loc = #intrs alpha_info;
+ val alpha_cases_loc = #elims alpha_info;
val phi = ProofContext.export_morphism lthy' lthy;
val all_alpha_trms = all_alpha_trms_loc
|> map (Morphism.term phi)
|> map Type.legacy_freeze
- val alpha_induct = Morphism.thm phi alpha_induct_loc
+ val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc
val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
+ val alpha_tys =
+ alpha_trms
+ |> map fastype_of
+ |> map domain_type
+
+ val alpha_bn_tys =
+ alpha_bn_trms
+ |> map fastype_of
+ |> map domain_type
+
+ val alpha_names = map (fst o dest_Const) alpha_trms
+ val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms
+
+ val alpha_result = AlphaResult
+ {alpha_names = alpha_names,
+ alpha_trms = alpha_trms,
+ alpha_tys = alpha_tys,
+ alpha_bn_names = alpha_bn_names,
+ alpha_bn_trms = alpha_bn_trms,
+ alpha_bn_tys = alpha_bn_tys,
+ alpha_intros = alpha_intros,
+ alpha_cases = alpha_cases,
+ alpha_raw_induct = alpha_raw_induct}
in
- (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
+ (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_raw_induct, alpha_result, lthy')
end
@@ -385,19 +403,21 @@
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 =
+fun raw_prove_alpha_distincts ctxt alpha_result raw_distinct_thms raw_dt_names =
let
- val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms)
+ val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result
- fun mk_alpha_distinct distinct_trm =
+ val ty_trm_assoc = raw_dt_names ~~ alpha_names
+
+ fun mk_alpha_distinct raw_distinct_trm =
let
- val goal = mk_distinct_goal ty_trm_assoc distinct_trm
+ val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm
in
Goal.prove ctxt [] [] goal
- (K (distinct_tac cases_thms distinct_thms 1))
+ (K (distinct_tac alpha_cases raw_distinct_thms 1))
end
in
- map (mk_alpha_distinct o prop_of) distinct_thms
+ map (mk_alpha_distinct o prop_of) raw_distinct_thms
end
@@ -429,11 +449,13 @@
else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
end;
-fun raw_prove_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
+fun raw_prove_alpha_eq_iff ctxt alpha_result raw_distinct_thms raw_inject_thms =
let
+ val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result
+
val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
val goals = map mk_alpha_eq_iff_goal thms_imp;
- val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;
+ val tac = alpha_eq_iff_tac (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1;
val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
in
Variable.export ctxt' ctxt thms
@@ -459,23 +481,16 @@
resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
end
-fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =
+fun raw_prove_refl ctxt alpha_result raw_dt_induct =
let
- val arg_tys =
- alpha_trms
- |> map fastype_of
- |> map domain_type
-
- val arg_bn_tys =
- alpha_bns
- |> map fastype_of
- |> map domain_type
+ val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} =
+ alpha_result
val props =
map (fn (ty, c) => (ty, fn x => c $ x $ x))
- ((arg_tys ~~ alpha_trms) @ (arg_bn_tys ~~ alpha_bns))
+ ((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms))
in
- induct_prove arg_tys props raw_dt_induct (cases_tac alpha_intros) ctxt
+ induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt
end
@@ -505,19 +520,21 @@
trans_prem_tac pred_names ctxt]
end
-fun raw_prove_sym alpha_trms alpha_intros alpha_induct alpha_eqvt ctxt =
+fun raw_prove_sym ctxt alpha_result alpha_eqvt =
let
+ val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms,
+ alpha_intros, alpha_raw_induct, ...} = alpha_result
+
+ val alpha_trms = alpha_trms @ alpha_bn_trms
+ val alpha_names = alpha_names @ alpha_bn_names
+
val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
fun tac ctxt =
- let
- val alpha_names = map (fst o dest_Const) alpha_trms
- in
- resolve_tac alpha_intros THEN_ALL_NEW
- FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt]
- end
+ resolve_tac alpha_intros THEN_ALL_NEW
+ FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt]
in
- alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt
+ alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt
end
@@ -560,14 +577,17 @@
asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
end
-fun prove_trans_tac pred_names raw_dt_thms intros cases alpha_eqvt ctxt =
+fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt =
let
+ val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result
+ val alpha_names = alpha_names @ alpha_bn_names
+
fun all_cases ctxt =
asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms)
- THEN' TRY o non_trivial_cases_tac pred_names intros alpha_eqvt ctxt
+ THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt
in
EVERY' [ rtac @{thm allI}, rtac @{thm impI},
- ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]
+ ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
end
fun prep_trans_goal alpha_trm (arg1, arg2) =
@@ -579,13 +599,17 @@
HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
end
-fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases alpha_eqvt ctxt =
+fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt =
let
- val alpha_names = map (fst o dest_Const) alpha_trms
+ val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms,
+ alpha_raw_induct, ...} = alpha_result
+
+ val alpha_trms = alpha_trms @ alpha_bn_trms
+
val props = map prep_trans_goal alpha_trms
in
- alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
- (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases alpha_eqvt) ctxt
+ alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct
+ (prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt
end
@@ -601,8 +625,10 @@
@{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)"
by (rule eq_reflection, auto simp add: trans_def transp_def)}
-fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt =
+fun raw_prove_equivp ctxt alpha_result refl symm trans =
let
+ val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result
+
val refl' = map (fold_rule [reflp_def'] o atomize) refl
val symm' = map (fold_rule [symp_def'] o atomize) symm
val trans' = map (fold_rule [transp_def'] o atomize) trans
@@ -610,10 +636,10 @@
fun prep_goal t =
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
in
- Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns))
+ Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
(K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN'
RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
- |> chop (length alphas)
+ |> chop (length alpha_trms)
end