--- a/Nominal/Fv.thy Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/Fv.thy Fri Mar 26 10:07:26 2010 +0100
@@ -198,11 +198,6 @@
if a = b then a else
HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf})
- fun mk_conjl props =
- fold (fn a => fn b =>
- if a = @{term True} then b else
- if b = @{term True} then a else
- HOLogic.mk_conj (a, b)) (rev props) @{term True};
fun mk_diff a b =
if b = noatoms then a else
if b = a then noatoms else
@@ -597,102 +592,7 @@
end
*}
-(*
-atom_decl name
-datatype lam =
- VAR "name"
-| APP "lam" "lam"
-| LET "bp" "lam"
-and bp =
- BP "name" "lam"
-primrec
- bi::"bp \<Rightarrow> atom set"
-where
- "bi (BP x t) = {atom x}"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *}
-local_setup {*
- snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
- [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
-print_theorems
-*)
-(*atom_decl name
-datatype rtrm1 =
- rVr1 "name"
-| rAp1 "rtrm1" "rtrm1"
-| rLm1 "name" "rtrm1" --"name is bound in trm1"
-| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
-and bp =
- BUnit
-| BVr "name"
-| BPr "bp" "bp"
-primrec
- bv1
-where
- "bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *}
-local_setup {*
- snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1")
- [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]],
- [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
-print_theorems
-*)
-
-(*
-atom_decl name
-datatype rtrm5 =
- rVr5 "name"
-| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
-and rlts =
- rLnil
-| rLcons "name" "rtrm5" "rlts"
-primrec
- rbv5
-where
- "rbv5 rLnil = {}"
-| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *}
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5")
- [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
-print_theorems
-*)
-
-ML {*
-fun alpha_inj_tac dist_inj intrs elims =
- SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
- (rtac @{thm iffI} THEN' RANGE [
- (eresolve_tac elims THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps dist_inj)
- ),
- asm_full_simp_tac (HOL_ss addsimps intrs)])
-*}
-
-ML {*
-fun build_alpha_inj_gl thm =
- let
- val prop = prop_of thm;
- val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
- val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
- fun list_conj l = foldr1 HOLogic.mk_conj l;
- in
- if hyps = [] then concl
- else HOLogic.mk_eq (concl, list_conj hyps)
- end;
-*}
-
-ML {*
-fun build_alpha_inj intrs dist_inj elims ctxt =
-let
- val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
- val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp;
- fun tac _ = alpha_inj_tac dist_inj intrs elims 1;
- val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
-in
- Variable.export ctxt' ctxt thms
-end
-*}
ML {*
fun build_alpha_sym_trans_gl alphas (x, y, z) =
@@ -746,8 +646,8 @@
fun reflp_tac induct eq_iff ctxt =
rtac induct THEN_ALL_NEW
simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW
- split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
- THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+ split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
+ THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
@{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
add_0_left supp_zero_perm Int_empty_left split_conv})
*}
@@ -799,12 +699,12 @@
ML {*
fun symp_tac induct inj eqvt ctxt =
- ind_tac induct THEN_ALL_NEW
- simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs
+ rel_indtac induct THEN_ALL_NEW
+ simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conj_tac
THEN_ALL_NEW
REPEAT o etac @{thm exi_neg}
THEN_ALL_NEW
- split_conjs THEN_ALL_NEW
+ split_conj_tac THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
(asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
@@ -864,12 +764,12 @@
ML {*
fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
- ind_tac induct THEN_ALL_NEW
+ rel_indtac induct THEN_ALL_NEW
(TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW
- split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs
+ split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
- THEN_ALL_NEW split_conjs THEN_ALL_NEW
+ THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW
(asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
*}
@@ -955,7 +855,7 @@
ML {*
fun supports_tac perm =
simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
- REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
+ REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
supp_fset_to_set supp_fmap_atom}))
@@ -1009,7 +909,7 @@
*}
ML {*
-fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
+fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
@@ -1079,7 +979,7 @@
ML {*
fun supp_eq_tac ind fv perm eqiff ctxt =
- ind_tac ind THEN_ALL_NEW
+ rel_indtac ind THEN_ALL_NEW
asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
@@ -1099,32 +999,7 @@
simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
*}
-(* Given function for buildng a goal for an input, prepares a
- one common goals for all the inputs and proves it by induction
- together *)
-ML {*
-fun prove_by_induct tys build_goal ind utac inputs ctxt =
-let
- val names = Datatype_Prop.make_tnames tys;
- val (names', ctxt') = Variable.variant_fixes names ctxt;
- val frees = map Free (names' ~~ tys);
- val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
- val gls = flat gls_lists;
- fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
- val trm_gl_lists = map trm_gls_map frees;
- val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
- val trm_gls = map mk_conjl trm_gl_lists;
- val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
- fun tac {context,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN'
- InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
- THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1
- val th_loc = Goal.prove ctxt'' [] [] gl tac
- val ths_loc = HOLogic.conj_elims th_loc
- val ths = Variable.export ctxt'' ctxt ths_loc
-in
- filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
+
ML {*
fun build_eqvt_gl pi frees fnctn ctxt =
@@ -1151,34 +1026,6 @@
*}
ML {*
-fun prove_by_alpha_induct alphas build_goal ind utac inputs ctxt =
-let
- val tys = map (domain_type o fastype_of) alphas;
- val names = Datatype_Prop.make_tnames tys;
- val (namesl, ctxt') = Variable.variant_fixes names ctxt;
- val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
- val freesl = map Free (namesl ~~ tys);
- val freesr = map Free (namesr ~~ tys);
- val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';
- val gls = flat gls_lists;
- fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
- val trm_gl_lists = map trm_gls_map freesl;
- val trm_gls = map mk_conjl trm_gl_lists;
- val pgls = map
- (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl))
- ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
- val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
-(* val _ = tracing (PolyML.makestring gl); *)
- fun tac {context,...} = (ind_tac ind THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1
- val th_loc = Goal.prove ctxt'' [] [] gl tac
- val ths_loc = HOLogic.conj_elims th_loc
- val ths = Variable.export ctxt'' ctxt ths_loc
-in
- filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
-
-ML {*
fun build_rsp_gl alphas fnctn ctxt =
let
val typ = domain_type (fastype_of fnctn);
@@ -1199,7 +1046,7 @@
ML {*
fun build_fvbv_rsps alphas ind simps fnctns ctxt =
- prove_by_alpha_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps ctxt) fnctns ctxt
+ prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
*}
end