--- a/Nominal/Nominal2.thy Wed Jun 29 19:21:26 2011 +0100
+++ b/Nominal/Nominal2.thy Wed Jun 29 23:08:44 2011 +0100
@@ -232,7 +232,7 @@
(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
val _ = trace_msg (K "Defining alpha relations...")
- val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
+ val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) =
define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct))
@@ -242,11 +242,10 @@
val _ = trace_msg (K "Proving distinct theorems...")
val alpha_distincts =
- raw_prove_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names
+ raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names
val _ = trace_msg (K "Proving eq-iff theorems...")
- val alpha_eq_iff =
- raw_prove_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
+ val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_distinct_thms raw_inject_thms
val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...")
val raw_bn_eqvt =
@@ -273,19 +272,13 @@
val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt
val _ = trace_msg (K "Proving equivalence of alpha...")
- val alpha_refl_thms =
- raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy5
-
- val alpha_sym_thms =
- raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct alpha_eqvt_norm lthy5
-
- val alpha_trans_thms =
- raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms)
- alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5
+ val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm
+ val alpha_sym_thms = raw_prove_sym lthy5 alpha_result alpha_eqvt_norm
+ val alpha_trans_thms =
+ raw_prove_trans lthy5 alpha_result (raw_distinct_thms @ raw_inject_thms) alpha_eqvt_norm
val (alpha_equivp_thms, alpha_bn_equivp_thms) =
- raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms
- alpha_trans_thms lthy5
+ raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms
val _ = trace_msg (K "Proving alpha implies bn...")
val alpha_bn_imp_thms =
--- 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
--- a/Nominal/nominal_dt_data.ML Wed Jun 29 19:21:26 2011 +0100
+++ b/Nominal/nominal_dt_data.ML Wed Jun 29 23:08:44 2011 +0100
@@ -16,11 +16,24 @@
val the_info: Proof.context -> string -> info
val register_info: (string * info) -> Context.generic -> Context.generic
val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
+
+ datatype alpha_result = AlphaResult of
+ {alpha_names : string list,
+ alpha_trms : term list,
+ alpha_tys : typ list,
+ alpha_bn_names : string list,
+ alpha_bn_trms : term list,
+ alpha_bn_tys : typ list,
+ alpha_intros : thm list,
+ alpha_cases : thm list,
+ alpha_raw_induct : thm}
+
end
structure Nominal_Dt_Data: NOMINAL_DT_DATA =
struct
+
(* information generated by nominal_datatype *)
type info =
{inject : thm list,
@@ -55,5 +68,16 @@
map aux ty_names
end
+datatype alpha_result = AlphaResult of
+ {alpha_names : string list,
+ alpha_trms : term list,
+ alpha_tys : typ list,
+ alpha_bn_names : string list,
+ alpha_bn_trms : term list,
+ alpha_bn_tys : typ list,
+ alpha_intros : thm list,
+ alpha_cases : thm list,
+ alpha_raw_induct : thm}
+
end
\ No newline at end of file