# HG changeset patch # User Cezary Kaliszyk # Date 1269594446 -3600 # Node ID a2142526bb01c901667e1a4613446e22ad086c50 # Parent 3b9c05d158f393455d77068005fa622e46e71ec9 Removed another cheat and cleaned the code a bit. diff -r 3b9c05d158f3 -r a2142526bb01 Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Fri Mar 26 09:23:23 2010 +0100 +++ b/Nominal/ExCoreHaskell.thy Fri Mar 26 10:07:26 2010 +0100 @@ -6,7 +6,6 @@ ML {* val _ = recursive := false *} ML {* val _ = cheat_const_rsp := true *} -ML {* val _ = cheat_alpha_bn_rsp := true *} atom_decl var atom_decl tvar diff -r 3b9c05d158f3 -r a2142526bb01 Nominal/ExLet.thy --- a/Nominal/ExLet.thy Fri Mar 26 09:23:23 2010 +0100 +++ b/Nominal/ExLet.thy Fri Mar 26 10:07:26 2010 +0100 @@ -22,8 +22,6 @@ "bn Lnil = {}" | "bn (Lcons x t l) = {atom x} \ (bn l)" - - thm trm_lts.fv thm trm_lts.eq_iff thm trm_lts.bn diff -r 3b9c05d158f3 -r a2142526bb01 Nominal/Fv.thy --- 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 \ 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) \ (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} \ (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 diff -r 3b9c05d158f3 -r a2142526bb01 Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Mar 26 09:23:23 2010 +0100 +++ b/Nominal/Parser.thy Fri Mar 26 10:07:26 2010 +0100 @@ -286,12 +286,10 @@ end *} +ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} ML {* val cheat_equivp = Unsynchronized.ref false *} -ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} -ML {* val cheat_bn_rsp = Unsynchronized.ref false *} ML {* val cheat_fv_rsp = Unsynchronized.ref false *} ML {* val cheat_const_rsp = Unsynchronized.ref false *} -ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} ML {* fun map_option _ NONE = NONE | map_option f (SOME x) = SOME (f x) *} @@ -342,7 +340,7 @@ (rel_distinct ~~ alpha_ts_nobn)); val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) - val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 + val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 val _ = tracing "Proving equivariance"; val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5 @@ -394,13 +392,9 @@ in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] const_rsp_tac) raw_consts lthy11 + val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11a; val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] - (fn _ => - if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy - else - let val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts - (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) in - asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end)) alpha_ts_bn lthy11a + (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; diff -r 3b9c05d158f3 -r a2142526bb01 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Fri Mar 26 09:23:23 2010 +0100 +++ b/Nominal/Rsp.thy Fri Mar 26 10:07:26 2010 +0100 @@ -1,5 +1,5 @@ theory Rsp -imports Abs +imports Abs Tacs begin ML {* @@ -74,12 +74,8 @@ *} ML {* -fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct -*} - -ML {* fun fvbv_rsp_tac induct fvbv_simps ctxt = - ind_tac induct THEN_ALL_NEW + rel_indtac induct THEN_ALL_NEW (TRY o rtac @{thm TrueI}) THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW @@ -92,13 +88,12 @@ fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) fun all_eqvts ctxt = Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt -val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) *} ML {* fun constr_rsp_tac inj rsp = REPEAT o rtac impI THEN' - simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW + simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW (asm_simp_tac HOL_ss THEN_ALL_NEW ( REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW @@ -107,23 +102,6 @@ )) *} -(* Testing code -local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] - (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) - -(*ML {* - val rsp_goals = map (const_rsp @{context}) [@{term rbv2}] - val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals) - val fixed' = distinct (op =) (flat fixed) - val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) -*} -prove ug: {* user_goal *} -ML_prf {* -val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} -val fv_simps = @{thms rbv2.simps} -*} -*) - ML {* fun perm_arg arg = let @@ -150,13 +128,13 @@ ML {* fun alpha_eqvt_tac induct simps ctxt = - ind_tac induct THEN_ALL_NEW + rel_indtac induct THEN_ALL_NEW simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW - REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW + REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW - (split_conjs THEN_ALL_NEW TRY o resolve_tac + (split_conj_tac THEN_ALL_NEW TRY o resolve_tac @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) @@ -231,6 +209,8 @@ end *} +(** alpha_bn_rsp **) + lemma equivp_rspl: "equivp r \ r a b \ r a c = r b c" unfolding equivp_reflp_symp_transp symp_def transp_def @@ -242,39 +222,38 @@ by blast ML {* -fun prove_alpha_bn_rsp alphas inducts exhausts inj_dis equivps ctxt (alpha_bn, n) = +fun alpha_bn_rsp_tac simps res exhausts a ctxt = + rtac allI THEN_ALL_NEW + case_rules_tac ctxt a exhausts THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW + TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) THEN_ALL_NEW + TRY o eresolve_tac res THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps simps); +*} + + +ML {* +fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt = let - val alpha = nth alphas n; - val ty = domain_type (fastype_of alpha); - val ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt; - val [l, r] = map (fn x => (Free (x, ty))) [x, y] - val lhs = HOLogic.mk_Trueprop (alpha $ l $ r) - val g1 = - Logic.mk_implies (lhs, - HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty, - HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)))); - val g2 = - Logic.mk_implies (lhs, - HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty, - HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r)))); - val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps; - val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps; - fun tac {context, ...} = ( - etac (nth inducts n) THEN_ALL_NEW - (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW - split_conjs THEN_ALL_NEW - InductTacs.case_rule_tac context a (nth exhausts n) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW - TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) THEN_ALL_NEW - TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps inj_dis) - ) 1; - val t1 = Goal.prove ctxt [] [] g1 tac; - val t2 = Goal.prove ctxt [] [] g2 tac; + val ty = domain_type (fastype_of alpha_bn); + val (l, r) = the (AList.lookup (op=) alphas ty); in - Variable.export ctxt' ctxt [t1, t2] + ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)), + HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt) end *} +ML {* +fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt = +let + val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt; + val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps; + val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps; + val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind + (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt +in + Variable.export ctxt' ctxt ths_loc +end +*} end diff -r 3b9c05d158f3 -r a2142526bb01 Nominal/Tacs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Tacs.thy Fri Mar 26 10:07:26 2010 +0100 @@ -0,0 +1,129 @@ +theory Tacs +imports Main +begin + +(* General not-nominal/quotient functionality useful for proving *) + +(* A version of case_rule_tac that takes more exhaust rules *) +ML {* +fun case_rules_tac ctxt0 s rules i st = +let + val (_, ctxt) = Variable.focus_subgoal i st ctxt0; + val ty = fastype_of (ProofContext.read_term_schematic ctxt s) + fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1)))); + val ty_rules = filter (fn x => exhaust_ty x = ty) rules; +in + InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st +end +*} + +ML {* +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}; +*} + +ML {* +val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) +*} + +(* 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,...} = ( + InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind] + THEN_ALL_NEW split_conj_tac 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 +*} + +(* An induction for a single relation is "R x y \ P x y" + but for multiple relations is "(R1 x y \ P x y) \ (R2 a b \ P2 a b)" *) +ML {* +fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct +*} + +ML {* +fun prove_by_rel_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); + fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW + TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 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 +*} +(* Code for transforming an inductive relation to a function *) +ML {* +fun rel_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_rel_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_rel_inj intrs dist_inj elims ctxt = +let + val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt; + val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp; + fun tac _ = rel_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 +*} + +end +