# HG changeset patch # User Christian Urban # Date 1273678430 -3600 # Node ID 238062c4c9f2b4c1641efd5bb91956a937dd37d3 # Parent 0e52851acac4b48f03d0eac143b79d9a6f12f218# Parent ce228f7b2b7221fb4192de28e3b0e676136f69d1 merged diff -r 0e52851acac4 -r 238062c4c9f2 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Wed May 12 16:33:25 2010 +0100 +++ b/Nominal/Ex/Classical.thy Wed May 12 16:33:50 2010 +0100 @@ -12,9 +12,7 @@ atom_decl name atom_decl coname -ML {* val _ = cheat_alpha_eqvt := true *} ML {* val _ = cheat_equivp := true *} -ML {* val _ = cheat_fv_rsp := true *} nominal_datatype trm = Ax "name" "coname" diff -r 0e52851acac4 -r 238062c4c9f2 Nominal/Ex/ExPS3.thy --- a/Nominal/Ex/ExPS3.thy Wed May 12 16:33:25 2010 +0100 +++ b/Nominal/Ex/ExPS3.thy Wed May 12 16:33:50 2010 +0100 @@ -6,7 +6,6 @@ atom_decl name -ML {* val _ = cheat_alpha_eqvt := true *} ML {* val _ = cheat_equivp := true *} ML {* val _ = cheat_alpha_bn_rsp := true *} diff -r 0e52851acac4 -r 238062c4c9f2 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Wed May 12 16:33:25 2010 +0100 +++ b/Nominal/Ex/ExPS8.thy Wed May 12 16:33:50 2010 +0100 @@ -7,6 +7,7 @@ atom_decl name ML {* val _ = cheat_fv_rsp := true *} +ML {* val _ = cheat_equivp := true *} ML {* val _ = cheat_alpha_bn_rsp := true *} nominal_datatype exp = diff -r 0e52851acac4 -r 238062c4c9f2 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed May 12 16:33:25 2010 +0100 +++ b/Nominal/NewParser.thy Wed May 12 16:33:50 2010 +0100 @@ -278,7 +278,6 @@ end *} -ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} ML {* val cheat_equivp = Unsynchronized.ref false *} ML {* val cheat_fv_rsp = Unsynchronized.ref false *} ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} @@ -436,23 +435,20 @@ val _ = warning "Proving equivariance"; val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 - fun alpha_eqvt_tac' _ = - if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy - else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1 - val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; + val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; (* proving alpha equivalence *) val _ = warning "Proving equivalence"; val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; - val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6; + val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; val alpha_equivp = - if !cheat_equivp then map (equivp_hack lthy6) alpha_ts + if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts else build_equivps alpha_ts reflps alpha_induct - inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6; + inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names - val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; + val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6a; val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); val raw_consts = flat (map (fn (i, (_, _, l)) => diff -r 0e52851acac4 -r 238062c4c9f2 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Wed May 12 16:33:25 2010 +0100 +++ b/Nominal/Rsp.thy Wed May 12 16:33:50 2010 +0100 @@ -62,8 +62,7 @@ fun fvbv_rsp_tac induct fvbv_simps ctxt = rtac induct THEN_ALL_NEW (TRY o rtac @{thm TrueI}) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps set.simps append.simps alphas} @ fvbv_simps)) THEN_ALL_NEW REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW TRY o blast_tac (claset_of ctxt) @@ -87,51 +86,6 @@ )) *} - -lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (pi \ p)) \ \pi. Q pi" -apply (erule exE) -apply (rule_tac x="pi \ pia" in exI) -by auto - - -ML {* -fun alpha_eqvt_tac induct simps ctxt = - rtac induct THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac 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 alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW - (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)) -*} - -ML {* -fun build_alpha_eqvt alpha names = -let - val pi = Free ("p", @{typ perm}); - val (tys, _) = strip_type (fastype_of alpha) - val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys)); - val args = map Free (indnames ~~ tys); - val perm_args = map (fn x => mk_perm pi x) args -in - (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) -end -*} - -ML {* -fun build_alpha_eqvts funs tac ctxt = -let - val (gls, names) = fold_map build_alpha_eqvt funs ["p"] - val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls) - val thm = Goal.prove ctxt names [] gl tac -in - map (fn x => mp OF [x]) (HOLogic.conj_elims thm) -end -*} - ML {* fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt = let diff -r 0e52851acac4 -r 238062c4c9f2 Nominal/Unused.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Unused.thy Wed May 12 16:33:50 2010 +0100 @@ -0,0 +1,43 @@ +lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (pi \ p)) \ \pi. Q pi" +apply (erule exE) +apply (rule_tac x="pi \ pia" in exI) +by auto + +ML {* +fun alpha_eqvt_tac induct simps ctxt = + rtac induct THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac 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 alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW + (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)) +*} + +ML {* +fun build_alpha_eqvt alpha names = +let + val pi = Free ("p", @{typ perm}); + val (tys, _) = strip_type (fastype_of alpha) + val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys)); + val args = map Free (indnames ~~ tys); + val perm_args = map (fn x => mk_perm pi x) args +in + (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) +end +*} + +ML {* +fun build_alpha_eqvts funs tac ctxt = +let + val (gls, names) = fold_map build_alpha_eqvt funs ["p"] + val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls) + val thm = Goal.prove ctxt names [] gl tac +in + map (fn x => mp OF [x]) (HOLogic.conj_elims thm) +end +*} +