# HG changeset patch # User Christian Urban # Date 1280446832 -3600 # Node ID ebf253d806708b84af70fd0541520af0305b66bf # Parent 082d9fd28f89f39d9219f992088e0c22e2256442 equivariance for size diff -r 082d9fd28f89 -r ebf253d80670 Nominal-General/Nominal2_Supp.thy --- a/Nominal-General/Nominal2_Supp.thy Thu Jul 29 10:16:33 2010 +0100 +++ b/Nominal-General/Nominal2_Supp.thy Fri Jul 30 00:40:32 2010 +0100 @@ -58,12 +58,18 @@ shows "(a \* (x, y) \ PROP C) \ (a \* x \ a \* y \ PROP C)" by (rule, simp_all add: fresh_star_prod) +lemma fresh_star_zero: + shows "as \* (0::perm)" + unfolding fresh_star_def + by (simp add: fresh_zero_perm) + lemma fresh_star_plus: fixes p q::perm shows "\a \* p; a \* q\ \ a \* (p + q)" unfolding fresh_star_def by (simp add: fresh_plus_perm) + lemma fresh_star_permute_iff: shows "(p \ a) \* (p \ x) \ a \* x" unfolding fresh_star_def diff -r 082d9fd28f89 -r ebf253d80670 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Thu Jul 29 10:16:33 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Fri Jul 30 00:40:32 2010 +0100 @@ -4,7 +4,7 @@ atom_decl name -declare [[STEPS = 16]] +declare [[STEPS = 17]] nominal_datatype trm = Var "name" @@ -21,6 +21,7 @@ where "bn (As x y t) = {atom x}" +thm size_eqvt thm alpha_bn_imps thm distinct thm eq_iff @@ -28,6 +29,7 @@ thm fv_defs thm perm_simps thm perm_laws +thm funs_rsp typ trm @@ -40,61 +42,31 @@ term alpha_bn -lemma a2: - shows "alpha_trm_raw x1 y1 \ fv_trm_raw x1 = fv_trm_raw y1" - and "alpha_assg_raw x2 y2 \ fv_assg_raw x2 = fv_assg_raw y2 \ bn_raw x2 = bn_raw y2" - and "alpha_bn_raw x3 y3 \ fv_bn_raw x3 = fv_bn_raw y3" -apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) -apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps - alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms) -done +lemma exi_zero: "P 0 \ \(x::perm). P x" by auto + +ML {* + val pre_ss = @{thms fun_rel_def} + val post_ss = @{thms alphas prod_alpha_def prod_rel.simps + prod_fv.simps fresh_star_zero permute_zero funs_rsp prod.cases alpha_bn_imps} + + val tac = + asm_full_simp_tac (HOL_ss addsimps pre_ss) + THEN' REPEAT o (resolve_tac @{thms allI impI}) + THEN' resolve_tac @{thms alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros} + THEN_ALL_NEW (TRY o (rtac @{thm exi_zero}) THEN' asm_full_simp_tac (HOL_ss addsimps post_ss)) +*} lemma [quot_respect]: "(op= ===> alpha_trm_raw) Var_raw Var_raw" "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw" "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw" - "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) + "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Foo_raw Foo_raw" "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" -apply(simp only: fun_rel_def) -apply(simp only: eq_iff) -apply(simp only: simp_thms) -apply(simp only: fun_rel_def) -apply(simp only: eq_iff) -apply(tactic {* asm_full_simp_tac HOL_ss 1*}) -apply(simp only: fun_rel_def) -apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2) -apply(rule allI | rule impI)+ -apply(rule_tac x="0" in exI) -apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2) -apply(simp add: a2) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) -apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) -apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) -apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) -apply(rule_tac x="0" in exI) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) -apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) -apply(assumption) +apply(tactic {* ALLGOALS tac *}) done lemma [quot_respect]: @@ -103,7 +75,7 @@ "(alpha_assg_raw ===> op =) bn_raw bn_raw" "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw" "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" -apply(simp_all add: a2 a1) +apply(simp_all add: alpha_bn_imps funs_rsp) sorry ML {* diff -r 082d9fd28f89 -r ebf253d80670 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Thu Jul 29 10:16:33 2010 +0100 +++ b/Nominal/NewParser.thy Fri Jul 30 00:40:32 2010 +0100 @@ -305,24 +305,31 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo - val all_raw_tys = map (fn (_, (n, _, _)) => n) descr + val all_raw_tys = all_dtyps descr sorts + val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr val all_raw_constrs = flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_tys + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names val inject_thms = flat (map #inject dtinfos); val distinct_thms = flat (map #distinct dtinfos); val constr_thms = inject_thms @ distinct_thms val rel_dtinfos = List.take (dtinfos, (length dts)); val raw_constrs_distinct = (map #distinct rel_dtinfos); - val induct_thm = #induct dtinfo; + val raw_induct_thm = #induct dtinfo; + val raw_induct_thms = #inducts dtinfo; val exhaust_thms = map #exhaust dtinfos; + val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys + val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) + |> `(fn thms => (length thms) div 2) + |> (uncurry drop) + (* definitions of raw permutations *) val _ = warning "Definition of raw permutations"; val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = if get_STEPS lthy0 > 1 - then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 + then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0 else raise TEST lthy0 (* noting the raw permutations as eqvt theorems *) @@ -338,7 +345,7 @@ val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = if get_STEPS lthy3 > 2 - then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 + then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 else raise TEST lthy3 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = @@ -367,7 +374,7 @@ then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases else raise TEST lthy4 - (* proving equivariance lemmas for bns, fvs and alpha *) + (* proving equivariance lemmas for bns, fvs, size and alpha *) val _ = warning "Proving equivariance"; val bn_eqvt = if get_STEPS lthy > 6 @@ -381,13 +388,19 @@ val fv_eqvt = if get_STEPS lthy > 7 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) - (Local_Theory.restore lthy_tmp) + (Local_Theory.restore lthy_tmp) + else raise TEST lthy4 + + val size_eqvt = + if get_STEPS lthy > 8 + then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) + (Local_Theory.restore lthy_tmp) else raise TEST lthy4 val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) val (alpha_eqvt, lthy6) = - if get_STEPS lthy > 8 + if get_STEPS lthy > 9 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 else raise TEST lthy4 @@ -395,23 +408,23 @@ val _ = warning "Proving equivalence" val alpha_refl_thms = - if get_STEPS lthy > 9 - then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy6 + if get_STEPS lthy > 10 + then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 else raise TEST lthy6 val alpha_sym_thms = - if get_STEPS lthy > 10 + if get_STEPS lthy > 11 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 else raise TEST lthy6 val alpha_trans_thms = - if get_STEPS lthy > 11 + if get_STEPS lthy > 12 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) alpha_intros alpha_induct alpha_cases lthy6 else raise TEST lthy6 val alpha_equivp_thms = - if get_STEPS lthy > 12 + if get_STEPS lthy > 13 then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6 else raise TEST lthy6 @@ -419,16 +432,14 @@ val _ = warning "Proving alpha implies bn" val alpha_bn_imp_thms = - if get_STEPS lthy > 13 + if get_STEPS lthy > 14 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 else raise TEST lthy6 (* auxiliary lemmas for respectfulness proofs *) - (* HERE *) - - val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns - alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 - val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test)) + val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs + raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 + (* defining the quotient type *) val _ = warning "Declaring the quotient types" @@ -438,7 +449,7 @@ val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *) val (qty_infos, lthy7) = - if get_STEPS lthy > 14 + if get_STEPS lthy > 15 then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 else raise TEST lthy6 @@ -463,7 +474,7 @@ map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = - if get_STEPS lthy > 15 + if get_STEPS lthy > 16 then lthy7 |> qconst_defs qtys qconstrs_descr @@ -479,7 +490,7 @@ val qfv_bns = map #qconst qfv_bns_info val qalpha_bns = map #qconst qalpha_bns_info - (* HERE *) + (* temporary theorem bindings *) val (_, lthy8') = lthy8 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) @@ -489,9 +500,11 @@ ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) + ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) + ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), size_eqvt) val _ = - if get_STEPS lthy > 16 + if get_STEPS lthy > 17 then true else raise TEST lthy8' (* old stuff *) @@ -558,7 +571,7 @@ fun suffix_bind s = Binding.qualify true q_name (Binding.name s); val _ = warning "Lifting induction"; val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; - val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm); + val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 raw_induct_thm); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); fun note_simp_suffix s th ctxt = diff -r 082d9fd28f89 -r ebf253d80670 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Thu Jul 29 10:16:33 2010 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Fri Jul 30 00:40:32 2010 +0100 @@ -258,11 +258,11 @@ val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} fun subproof_tac const_names simps = - Subgoal.FOCUS (fn {prems, context, ...} => + SUBPROOF (fn {prems, context, ...} => HEADGOAL (simp_tac (HOL_basic_ss addsimps simps) THEN' Nominal_Permeq.eqvt_tac context [] const_names - THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems)))) + THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) fun prove_eqvt_tac insts ind_thms const_names simps ctxt = HEADGOAL