--- a/Nominal/nominal_dt_alpha.ML Wed Jun 29 23:08:44 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML Thu Jun 30 02:19:59 2011 +0100
@@ -10,8 +10,7 @@
val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
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 * alpha_result * local_theory
+ bclause list list list -> term list -> Proof.context -> alpha_result * local_theory
val induct_prove: typ list -> (typ * (term -> term)) list -> thm ->
(Proof.context -> int -> tactic) -> Proof.context -> thm list
@@ -26,14 +25,13 @@
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
- val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
- val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
- val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list
- val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list ->
- Proof.context -> thm list
+ val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list
+ val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list ->
+ thm list -> thm list
+ val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list
+ val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
+ val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list
+ val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
val mk_funs_rsp: thm -> thm
val mk_alpha_permute_rsp: thm -> thm
@@ -267,20 +265,14 @@
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_tys = map (domain_type o fastype_of) alpha_trms
+ val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms
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
+ in
+ (AlphaResult
{alpha_names = alpha_names,
alpha_trms = alpha_trms,
alpha_tys = alpha_tys,
@@ -289,9 +281,7 @@
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_raw_induct, alpha_result, lthy')
+ alpha_raw_induct = alpha_raw_induct}, lthy')
end
@@ -645,11 +635,13 @@
(* proves that alpha_raw implies alpha_bn *)
-fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt =
+fun raw_prove_bn_imp_tac alpha_result ctxt =
SUBPROOF (fn {prems, context, ...} =>
let
+ val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result
+
val prems' = flat (map Datatype_Aux.split_conj_thm prems)
- val prems'' = map (transform_prem1 context pred_names) prems'
+ val prems'' = map (transform_prem1 context alpha_names) prems'
in
HEADGOAL
(REPEAT_ALL_NEW
@@ -660,24 +652,28 @@
resolve_tac alpha_intros ]))
end) ctxt
-fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =
+
+fun raw_prove_bn_imp ctxt alpha_result =
let
+ val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result
+
val arg_ty = domain_type o fastype_of
- val alpha_names = map (fst o dest_Const) alpha_trms
- val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+ val ty_assoc = alpha_tys ~~ alpha_trms
val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
in
- alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct
- (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt
+ alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct
+ (raw_prove_bn_imp_tac alpha_result) ctxt
end
(* respectfulness for fv_raw / bn_raw *)
-fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
+fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps =
let
- val arg_ty = fst o dest_Type o domain_type o fastype_of
- val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+ val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result
+
+ val arg_ty = domain_type o fastype_of
+ val ty_assoc = alpha_tys ~~ alpha_trms
fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
@@ -687,28 +683,29 @@
val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps}
@ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left})
in
- alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct
+ alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct
(K (asm_full_simp_tac ss)) ctxt
end
(* respectfulness for size *)
-fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
+fun raw_size_rsp_aux ctxt alpha_result simps =
let
- val arg_tys = map (domain_type o fastype_of) all_alpha_trms
-
+ val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} =
+ alpha_result
+
fun mk_prop ty (x, y) = HOLogic.mk_eq
(HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
- val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys
+ val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys))
val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def
permute_prod_def prod.cases prod.recs})
val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
in
- alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
+ alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
end
@@ -726,12 +723,12 @@
THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
end
-fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
+fun raw_constrs_rsp ctxt alpha_result constrs simps =
let
- val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
-
+ val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result
+
fun lookup ty =
- case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
+ case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of
NONE => HOLogic.eq_const ty
| SOME alpha => alpha
@@ -763,8 +760,10 @@
(* we have to reorder the alpha_bn_imps theorems in order
to be in order with alpha_bn_trms *)
-fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps =
+fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps =
let
+ val AlphaResult {alpha_bn_trms, ...} = alpha_result
+
fun mk_map thm =
thm |> `prop_of
|>> List.last o snd o strip_comb
@@ -787,11 +786,12 @@
val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"
by (simp add: fun_rel_def)}
-fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt =
+fun raw_prove_perm_bn_tac alpha_result simps ctxt =
SUBPROOF (fn {prems, context, ...} =>
let
+ val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result
val prems' = flat (map Datatype_Aux.split_conj_thm prems)
- val prems'' = map (transform_prem1 context pred_names) prems'
+ val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
in
HEADGOAL
(simp_tac (HOL_basic_ss addsimps (simps @ prems'))
@@ -804,11 +804,13 @@
resolve_tac alpha_intros ]))
end) ctxt
-fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt =
+fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
let
- val arg_ty = domain_type o fastype_of
+ val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} =
+ alpha_result
+
val perm_bn_ty = range_type o range_type o fastype_of
- val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+ val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms)
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
val p = Free (p, @{typ perm})
@@ -820,12 +822,10 @@
(alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y))
end
- val goals = map mk_prop perm_bns
- val alpha_names = map (fst o dest_Const) alpha_trms
-
+ val goals = map mk_prop perm_bns
in
- alpha_prove alpha_trms goals alpha_induct
- (raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt
+ alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct
+ (raw_prove_perm_bn_tac alpha_result simps) ctxt
|> ProofContext.export ctxt' ctxt
|> map atomize
|> map single