# HG changeset patch # User Christian Urban # Date 1291653342 0 # Node ID 515e5496171c44495d436dda34ba9b0a58cd7c54 # Parent 25dcb2b1329e7edf5ad2dd3ed08c198a02394f19 automated alpha_perm_bn theorems diff -r 25dcb2b1329e -r 515e5496171c Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Mon Dec 06 14:24:17 2010 +0000 +++ b/Nominal/Ex/Foo1.thy Mon Dec 06 16:35:42 2010 +0000 @@ -55,43 +55,6 @@ thm foo.fresh thm foo.bn_finite -lemma uu1: - shows "alpha_bn1 as (permute_bn1 p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[7] -apply(simp add: foo.perm_bn_simps) -apply(simp add: foo.eq_iff) -apply(auto) -done - -lemma uu2: - shows "alpha_bn2 as (permute_bn2 p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[7] -apply(simp add: foo.perm_bn_simps) -apply(simp add: foo.eq_iff) -apply(auto) -done - -lemma uu3: - shows "alpha_bn3 as (permute_bn3 p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[7] -apply(simp add: foo.perm_bn_simps) -apply(simp add: foo.eq_iff) -apply(auto) -done - -lemma uu4: - shows "alpha_bn4 as (permute_bn4 p as)" -apply(induct as rule: foo.inducts(3)) -apply(auto)[8] -apply(simp add: foo.perm_bn_simps) -apply(simp add: foo.eq_iff) -apply(simp add: foo.perm_bn_simps) -apply(simp add: foo.eq_iff) -done - lemma tt1: shows "(p \ bn1 as) = bn1 (permute_bn1 p as)" @@ -129,30 +92,6 @@ apply(simp add: atom_eqvt insert_eqvt) done - -lemma Let1_rename: - assumes "supp ([bn1 assn]lst. trm) \* p" - shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \ trm)" -using assms -apply - -apply(drule supp_perm_eq[symmetric]) -apply(simp only: permute_Abs) -apply(simp only: tt1) -apply(simp only: foo.eq_iff) -apply(rule conjI) -apply(rule refl) -apply(rule uu1) -done - -lemma Let1_rename_a: - fixes c::"'a::fs" - assumes "y = Let1 assn trm" - shows "\p. (p \ (set (bn1 assn))) \* c \ y = Let1 (permute_bn1 p assn) (p \ trm)" -using assms -apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric]) -apply(simp del: permute_Abs) -sorry - lemma strong_exhaust1: fixes c::"'a::fs" assumes "\name. y = Var name \ P" @@ -163,60 +102,7 @@ and "\(c::'a::fs) assn trm. set (bn3 assn) \* c \ y = Let3 assn trm \ P" and "\(c::'a::fs) assn' trm. (bn4 assn') \* c \ y = Let4 assn' trm \ P" shows "P" -apply(rule_tac y="y" in foo.exhaust(1)) -apply(rule assms(1)) -apply(rule exI) -apply(assumption) -apply(rule assms(2)) -apply(rule exI)+ -apply(assumption) -apply(rule assms(3)) -apply(subgoal_tac "\p::perm. (p \ {atom name}) \* (c, name, trm)") -apply(erule exE) -apply(perm_simp) -apply(rule_tac exI)+ -apply(rule conjI) -apply(simp add: fresh_star_prod) -apply(erule conjE)+ -apply(assumption) -apply(simp) -apply(simp add: foo.eq_iff) -(* HERE *) -defer -defer -apply(rule assms(4)) -apply(subgoal_tac "\p::perm. (p \ (set (bn1 assg))) \* (c, assg, trm)") -apply(erule exE) -apply(perm_simp add: tt1) -apply(simp only: fresh_star_prod) -apply(erule conjE)+ -apply(rule_tac exI)+ -apply(rule conjI) -apply(assumption) -apply(simp add: foo.eq_iff) -apply(rule conjI) -apply(simp only: tt1[symmetric]) -defer -apply(rule uu1) -defer -apply(rule assms(5)) -apply(subgoal_tac "\p::perm. (p \ (set (bn2 assg))) \* (c, assg, trm)") -apply(erule exE) -apply(perm_simp add: tt2) -apply(simp only: fresh_star_prod) -apply(erule conjE)+ -apply(rule_tac exI)+ -apply(rule conjI) -apply(assumption) -apply(simp add: foo.eq_iff) -apply(rule conjI) -apply(simp only: tt2[symmetric]) -defer -apply(rule uu2) -defer -apply(rule refl) -apply(subst (asm) fresh_star_supp_conv) -apply(simp) +oops lemma strong_exhaust2: @@ -229,89 +115,7 @@ and "\assn trm. \set (bn3 assn) \* c; y = Let3 assn trm\ \ P" and "\assn' trm. \(bn4 assn') \* c; y = Let4 assn' trm\ \ P" shows "P" -apply(rule strong_exhaust1[where y="y"]) -apply(erule exE)+ -apply(rule assms(1)) -apply(assumption) -apply(erule exE)+ -apply(rule assms(2)) -apply(assumption) -apply(erule exE | erule conjE)? -apply(rule assms(3)) -apply(drule_tac x="c" in spec) -apply(erule exE | erule conjE)+ -apply(assumption)+ -apply(drule_tac x="c" in spec) -apply(erule exE | erule conjE)+ -apply(assumption)+ -apply(erule exE | erule conjE)+ -apply(rule assms(4)) -apply(assumption)+ -apply(erule exE | erule conjE)+ -apply(rule assms(5)) -apply(assumption)+ -apply(erule exE | erule conjE)+ -apply(rule assms(6)) -apply(assumption)+ -apply(erule exE | erule conjE)+ -apply(rule assms(7)) -apply(assumption)+ -done - - - - - - - - - - - - -apply(rule_tac y="y" in foo.exhaust(1)) -apply(rule assms(1)) -apply(rule exI) -apply(assumption) -apply(rule assms(2)) -apply(rule exI)+ -apply(assumption) -apply(rule assms(3)) -apply(rule_tac p="p" in permute_boolE) -apply(perm_simp) -apply(simp) -apply(subgoal_tac "\q. (q \ {atom name}) \* c \ supp (Lam name trm) \* q") -apply(erule exE) -apply(erule conjE) -apply(rule assms(3)) -apply(perm_simp) -apply(assumption) -apply(simp) -apply(drule supp_perm_eq[symmetric]) -apply(perm_simp) -apply(simp) -apply(rule at_set_avoiding2) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: foo.fresh fresh_star_def) -apply(drule Let1_rename_a) -apply(erule exE) -apply(erule conjE) -apply(rule assms(4)) -apply(simp only: set_eqvt tt1) -apply(assumption) -(* -apply(subgoal_tac "\q. (q \ (set (bn2 assg))) \* c \ supp ([bn2 assg]lst.trm) \* q") -apply(erule exE) -apply(erule conjE) -*) -thm assms(5) -apply(rule assms(5)) -prefer 2 -apply(clarify) -unfolding foo.eq_iff -apply +oops lemma strong_exhaust1: fixes c::"'a::fs" @@ -323,95 +127,7 @@ and "\assn trm. \set (bn3 assn) \* c; y = Let3 assn trm\ \ P" and "\assn' trm. \(bn4 assn') \* c; y = Let4 assn' trm\ \ P" shows "P" -apply(rule_tac y="y" in foo.exhaust(1)) -apply(rule assms(1)) -apply(assumption) -apply(rule assms(2)) -apply(assumption) -apply(subgoal_tac "\q. (q \ {atom name}) \* c \ supp (Lam name trm) \* q") -apply(erule exE) -apply(erule conjE) -apply(rule assms(3)) -apply(perm_simp) -apply(assumption) -apply(simp) -apply(drule supp_perm_eq[symmetric]) -apply(perm_simp) -apply(simp) -apply(rule at_set_avoiding2) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: foo.fresh fresh_star_def) -apply(drule Let1_rename_a) -apply(erule exE) -apply(erule conjE) -apply(rule assms(4)) -apply(simp only: set_eqvt tt1) -apply(assumption) -(* -apply(subgoal_tac "\q. (q \ (set (bn2 assg))) \* c \ supp ([bn2 assg]lst.trm) \* q") -apply(erule exE) -apply(erule conjE) -*) -thm assms(5) -apply(rule assms(5)) -prefer 2 -apply(clarify) -unfolding foo.eq_iff -apply(rule conjI) -prefer 2 -apply(rule uu2) -apply(simp only: tt2[symmetric]) -prefer 2 -apply(simp only: tt2[symmetric]) - -apply(simp_all only:)[2] -apply(simp add: set_eqvt) -apply(simp add: tt2) -apply(simp add: foo.eq_iff) -apply(drule supp_perm_eq[symmetric]) -apply(simp) -apply(simp add: tt2 uu2) -apply(rule at_set_avoiding2) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: Abs_fresh_star) -apply(subgoal_tac "\q. (q \ (set (bn3 assg))) \* c \ supp ([bn3 assg]lst.trm) \* q") -apply(erule exE) -apply(erule conjE) -apply(rule assms(6)) -apply(simp add: set_eqvt) -apply(simp add: tt3) -apply(simp add: foo.eq_iff) -apply(drule supp_perm_eq[symmetric]) -apply(simp) -apply(simp add: tt3 uu3) -apply(rule at_set_avoiding2) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: Abs_fresh_star) -apply(subgoal_tac "\q. (q \ (bn4 assg')) \* c \ supp ([bn4 assg']set.trm) \* q") -apply(erule exE) -apply(erule conjE) -apply(rule assms(7)) -apply(simp add: tt4) -apply(simp add: foo.eq_iff) -apply(drule supp_perm_eq[symmetric]) -apply(simp) -apply(simp add: tt4 uu4) -apply(rule at_set_avoiding2) -apply(simp add: foo.bn_finite) -apply(simp add: finite_supp) -apply(simp add: finite_supp) -apply(simp add: Abs_fresh_star) -done - -thm strong_exhaust1 foo.exhaust(1) - - +oops lemma strong_exhaust2: assumes "\x y t. as = As x y t \ P" @@ -448,6 +164,8 @@ and a9: "\c. P3 c (BNil)" and a10: "\c a as. \d. P3 d as \ P3 c (BAs a as)" shows "P1 c t" "P2 c as" "P3 c as'" +oops +(* using assms apply(induction_schema) apply(rule_tac y="t" and c="c" in strong_exhaust1) @@ -459,6 +177,7 @@ apply(relation "measure (sum_case (size o snd) (sum_case (\y. size (snd y)) (\z. size (snd z))))") apply(simp_all add: foo.size) done +*) end diff -r 25dcb2b1329e -r 515e5496171c Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Mon Dec 06 14:24:17 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Mon Dec 06 16:35:42 2010 +0000 @@ -43,17 +43,6 @@ thm foo.supp thm foo.fresh -lemma uu1: - shows "alpha_bn as (permute_bn p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[5] -apply(simp only: foo.perm_bn_simps) -apply(simp only: foo.eq_iff) -apply(simp only: foo.perm_bn_simps) -apply(simp only: foo.eq_iff refl) -apply(simp) -done - lemma tt1: shows "(p \ bn as) = bn (permute_bn p as)" apply(induct as rule: foo.inducts(2)) @@ -286,10 +275,10 @@ apply(rule conjI) apply(assumption) apply(rule conjI) -apply(rule uu1) +apply(rule foo.perm_bn_alpha) apply(rule conjI) apply(assumption) -apply(rule uu1) +apply(rule foo.perm_bn_alpha) apply(rule at_set_avoiding1) apply(simp) apply(simp add: finite_supp) @@ -348,7 +337,6 @@ apply(erule exE)+ apply(rule assms(2)) apply(assumption) -apply(erule exE)+ apply(rule assms(3)) apply(auto)[2] apply(erule exE)+ diff -r 25dcb2b1329e -r 515e5496171c Nominal/Ex/Multi_Recs2.thy --- a/Nominal/Ex/Multi_Recs2.thy Mon Dec 06 14:24:17 2010 +0000 +++ b/Nominal/Ex/Multi_Recs2.thy Mon Dec 06 16:35:42 2010 +0000 @@ -69,34 +69,6 @@ thm fun_recs.fsupp thm fun_recs.supp -term alpha_b_fnclause -term alpha_b_fnclauses -term alpha_b_lrb -term alpha_b_lrbs -term alpha_b_pat - -term alpha_b_fnclause_raw -term alpha_b_fnclauses_raw -term alpha_b_lrb_raw -term alpha_b_lrbs_raw -term alpha_b_pat_raw - -lemma uu1: - fixes as0::exp and as1::fnclause - shows "(\x::exp. True) (as0::exp)" - and "alpha_b_fnclause as1 (permute_b_fnclause p as1)" - and "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)" - and "alpha_b_lrb as3 (permute_b_lrb p as3)" - and "alpha_b_lrbs as4 (permute_b_lrbs p as4)" - and "alpha_b_pat as5 (permute_b_pat p as5)" -apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts) -apply(simp_all) -apply(simp only: fun_recs.perm_bn_simps) -apply(simp only: fun_recs.eq_iff) -apply(simp) -oops - - thm fun_recs.distinct thm fun_recs.induct thm fun_recs.inducts diff -r 25dcb2b1329e -r 515e5496171c Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Dec 06 14:24:17 2010 +0000 +++ b/Nominal/Nominal2.thy Mon Dec 06 16:35:42 2010 +0000 @@ -265,8 +265,6 @@ then define_raw_dts dts bn_funs bn_eqs bclauses lthy else raise TEST lthy - val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs)) - val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo @@ -309,12 +307,6 @@ (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 else raise TEST lthy3 - (* - val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns)) - val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info)) - val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info)) - *) - (* defining the permute_bn functions *) val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = if get_STEPS lthy3a > 2 @@ -493,14 +485,6 @@ val qalpha_bns_descr = map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms - (* - val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info)) - val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs)) - val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns)) - val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns)) - val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms)) - *) - val qperm_descr = map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs @@ -559,7 +543,7 @@ ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) else raise TEST lthy9a - val (((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), lthyB) = + val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = if get_STEPS lthy > 28 then lthyA @@ -568,6 +552,7 @@ ||>> lift_thms qtys [] raw_exhaust_thms ||>> lift_thms qtys [] raw_size_thms ||>> lift_thms qtys [] raw_perm_bn_simps + ||>> lift_thms qtys [] alpha_refl_thms else raise TEST lthyA val qinducts = Project_Rule.projections lthyA qinduct @@ -626,11 +611,11 @@ else [] (* proving that perm_bns preserve alpha *) - val qperm_bn_alpha_thms = @{thms TrueI} - (* if get_STEPS lthy > 33 - then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC - else []*) - + val qperm_bn_alpha_thms = + if get_STEPS lthy > 33 + then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' + qalpha_refl_thms lthyC + else [] (* noting the theorems *) diff -r 25dcb2b1329e -r 515e5496171c Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Dec 06 14:24:17 2010 +0000 +++ b/Nominal/nominal_dt_alpha.ML Mon Dec 06 16:35:42 2010 +0000 @@ -247,8 +247,6 @@ (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) - val _ = tracing ("alpha in def\n" ^ cat_lines (map (@{make_string} o fst o #1) all_alpha_names)) - val (alphas, lthy') = Inductive.add_inductive_i {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} diff -r 25dcb2b1329e -r 515e5496171c Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Mon Dec 06 14:24:17 2010 +0000 +++ b/Nominal/nominal_dt_supp.ML Mon Dec 06 16:35:42 2010 +0000 @@ -18,7 +18,7 @@ val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> - Proof.context -> thm list + thm list -> Proof.context -> thm list end structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = @@ -204,7 +204,7 @@ induct_prove qtys props qinduct (K ss_tac) ctxt end -fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs ctxt = +fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) @@ -218,12 +218,11 @@ val props = map2 mk_goal qperm_bns alpha_bns val ss_tac = (K (print_tac "test")) THEN' - asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs)) + asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls)) in - @{thms TrueI} - (*induct_prove qtys props qinduct (K ss_tac) ctxt' + induct_prove qtys props qinduct (K ss_tac) ctxt' |> ProofContext.export ctxt' ctxt - |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))*) + |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) end