--- a/Nominal/nominal_dt_alpha.ML Sat Jul 31 01:24:39 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML Sat Jul 31 02:05:25 2010 +0100
@@ -381,11 +381,12 @@
(fn {context, ...} => HEADGOAL
(DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context)))
|> singleton (ProofContext.export ctxt' ctxt)
- |> Datatype_Aux.split_conj_thm
+ |> Datatype_Aux.split_conj_thm
+ |> map (fn th => th RS mp)
|> map Datatype_Aux.split_conj_thm
|> flat
|> map zero_var_indexes
- |> map (fn th => th RS mp)
+
|> filter_out (is_true o concl_of)
end
@@ -549,7 +550,8 @@
(prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
end
-(* proves the equivp predicate for all alphas *)
+
+(** proves the equivp predicate for all alphas **)
val equivp_intro =
@{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R"
@@ -587,55 +589,15 @@
resolve_tac alpha_intros ]))
end) ctxt
-fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt =
+fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =
let
+ val arg_ty = domain_type o fastype_of
val alpha_names = map (fst o dest_Const) alpha_trms
-
- val arg_tys =
- alpha_trms
- |> map fastype_of
- |> map domain_type
- val arg_bn_tys =
- alpha_bns
- |> map fastype_of
- |> map domain_type
- val (arg_names1, (arg_names2, ctxt')) =
- ctxt
- |> Variable.variant_fixes (replicate (length arg_tys) "x")
- ||> Variable.variant_fixes (replicate (length arg_tys) "y")
- val arg_bn_names1 = map (lookup (arg_tys ~~ arg_names1)) arg_bn_tys
- val arg_bn_names2 = map (lookup (arg_tys ~~ arg_names2)) arg_bn_tys
- val args1 = map Free (arg_names1 ~~ arg_tys)
- val args2 = map Free (arg_names2 ~~ arg_tys)
- val arg_bns1 = map Free (arg_bn_names1 ~~ arg_bn_tys)
- val arg_bns2 = map Free (arg_bn_names2 ~~ arg_bn_tys)
-
- val alpha_bn_trms = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_bns (arg_bns1 ~~ arg_bns2)
- val true_trms = map (K @{term True}) arg_tys
-
- val goal_rhs =
- group ((arg_bn_tys ~~ alpha_bn_trms) @ (arg_tys ~~ true_trms))
- |> map snd
- |> map (foldr1 HOLogic.mk_conj)
-
- val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_trms (args1 ~~ args2)
- val goal_rest = map (fn t => HOLogic.mk_imp (t, @{term "True"})) alpha_bn_trms
-
- val goal =
- (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) @ goal_rest
- |> foldr1 HOLogic.mk_conj
- |> HOLogic.mk_Trueprop
+ val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+ val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
in
- Goal.prove ctxt' [] [] goal
- (fn {context, ...} =>
- HEADGOAL (DETERM o (rtac alpha_induct)
- THEN_ALL_NEW (raw_prove_bn_imp_tac alpha_names alpha_intros context)))
- |> singleton (ProofContext.export ctxt' ctxt)
- |> Datatype_Aux.split_conj_thm
- |> map (fn th => zero_var_indexes (th RS mp))
- |> map Datatype_Aux.split_conj_thm
- |> flat
- |> filter_out (is_true o concl_of)
+ alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct
+ (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt
end
@@ -643,72 +605,18 @@
fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
let
- val arg_tys =
- alpha_trms
- |> map fastype_of
- |> map domain_type
-
- val fv_bn_tys1 =
- (bns @ fvs)
- |> map fastype_of
- |> map domain_type
-
- val (arg_names1, (arg_names2, ctxt')) =
- ctxt
- |> Variable.variant_fixes (replicate (length arg_tys) "x")
- ||> Variable.variant_fixes (replicate (length arg_tys) "y")
-
- val args1 = map Free (arg_names1 ~~ arg_tys)
- val args2 = map Free (arg_names2 ~~ arg_tys)
-
- val fv_bn_args1a = map (lookup (arg_tys ~~ args1)) fv_bn_tys1
- val fv_bn_args1b = map (lookup (arg_tys ~~ args2)) fv_bn_tys1
- val fv_bn_eqs1 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2))
- (bns @ fvs) (fv_bn_args1a ~~ fv_bn_args1b)
-
- val arg_bn_tys =
- alpha_bn_trms
- |> map fastype_of
- |> map domain_type
+ val arg_ty = domain_type o fastype_of
+ val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
- val fv_bn_tys2 =
- fv_bns
- |> map fastype_of
- |> map domain_type
-
- val (arg_bn_names1, (arg_bn_names2, ctxt'')) =
- ctxt'
- |> Variable.variant_fixes (replicate (length arg_bn_tys) "x")
- ||> Variable.variant_fixes (replicate (length arg_bn_tys) "y")
+ val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs
+ val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns
+ val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns
- val args_bn1 = map Free (arg_bn_names1 ~~ fv_bn_tys2)
- val args_bn2 = map Free (arg_bn_names2 ~~ fv_bn_tys2)
- val fv_bn_eqs2 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2))
- fv_bns (args_bn1 ~~ args_bn2)
-
- val goal_rhs =
- group (fv_bn_tys1 ~~ fv_bn_eqs1)
- |> map snd
- |> map (foldr1 HOLogic.mk_conj)
-
- val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2)
- (alpha_trms @ alpha_bn_trms) ((args1 ~~ args2) @ (args_bn1 ~~ args_bn2))
-
- val goal =
- map2 (curry HOLogic.mk_imp) goal_lhs (goal_rhs @ fv_bn_eqs2)
- |> foldr1 HOLogic.mk_conj
- |> HOLogic.mk_Trueprop
-
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
- Goal.prove ctxt'' [] [] goal (fn {context, ...} =>
- HEADGOAL (DETERM o (rtac alpha_induct) THEN_ALL_NEW (asm_full_simp_tac ss)))
- |> singleton (ProofContext.export ctxt'' ctxt)
- |> Datatype_Aux.split_conj_thm
- |> map (fn th => zero_var_indexes (th RS mp))
- |> map Datatype_Aux.split_conj_thm
- |> flat
+ alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct
+ (K (asm_full_simp_tac ss)) ctxt
end
end (* structure *)