Re: [isabelle-dev] lemma addition
On Thu, 25 Jul 2013, Lars Noschinski wrote: On 25.07.2013 04:16, Christian Sternagel wrote: While the following lemma is proved automatically lemma converse_subset: A¯ ⊆ B¯ ⟷ A ⊆ B by auto I'm not sure exactly how, since simp_trace shows no application of simplification rules and neither of the rules suggested by different ATPs through sledgehammer are -- as far as I can tell -- automatic rules in the sense of [intro], [elim], [dest]. auto's call to safe splits it to goal (2 subgoals): 1. ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B 2. ⋀a b. A ⊆ B ⟹ (b, a) ∈ A ⟹ (b, a) ∈ B Both of which are discharged by blast. If we look at the theorems blast uses to prove ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B (how this can be done is described in Section 3.7 of the Isabelle Cookbook), we see that Relation.converse_iff plays a role, which was declared with the iff attribute. I did not understand this mysterious reference. Which version of the Cookbook, which page exactly? Using only canonical information reveals these possibilities that might be little known: * print_options: blast_trace, blast_stats, but this looks a bit chatty and of limited practical use * method step (see isar-ref manual) lemma A¯ ⊆ B¯ ⟷ A ⊆ B apply step apply step apply step apply step apply step apply step apply step apply step apply step done Note that these steps refer to the classic Classical Reasoner by Larry (safe, fast, best), while blast might work slightly differently. (This refers to Isabelle/b7a83845bc93.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] lemma addition
On 01.08.2013 17:19, Makarius wrote: Both of which are discharged by blast. If we look at the theorems blast uses to prove ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B (how this can be done is described in Section 3.7 of the Isabelle Cookbook), we see that Relation.converse_iff plays a role, which was declared with the iff attribute. I did not understand this mysterious reference. Which version of the Cookbook, which page exactly? It is less mysterious than other references on this list... Section 3.7, p. 66ff in [1] gives recipes how proof terms can be inspected. It is what worked best for me for getting ideas of blast proofs. ` Using only canonical information reveals these possibilities that might be little known: * print_options: blast_trace, blast_stats, but this looks a bit chatty and of limited practical use They seem to be mostly useful for debugging blast itself. [1] http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/file/95d6853dec4a/progtutorial.pdf -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] lemma addition
On 25.07.2013 04:16, Christian Sternagel wrote: While the following lemma is proved automatically lemma converse_subset: A¯ ⊆ B¯ ⟷ A ⊆ B by auto I'm not sure exactly how, since simp_trace shows no application of simplification rules and neither of the rules suggested by different ATPs through sledgehammer are -- as far as I can tell -- automatic rules in the sense of [intro], [elim], [dest]. auto's call to safe splits it to goal (2 subgoals): 1. ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B 2. ⋀a b. A ⊆ B ⟹ (b, a) ∈ A ⟹ (b, a) ∈ B Both of which are discharged by blast. If we look at the theorems blast uses to prove ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B (how this can be done is described in Section 3.7 of the Isabelle Cookbook), we see that Relation.converse_iff plays a role, which was declared with the iff attribute. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] lemma addition
Am 25.07.2013 04:16, schrieb Christian Sternagel: Dear developers, While the following lemma is proved automatically lemma converse_subset: A¯ ⊆ B¯ ⟷ A ⊆ B by auto I'm not sure exactly how, since simp_trace shows no application of simplification rules and neither of the rules suggested by different ATPs through sledgehammer are -- as far as I can tell -- automatic rules in the sense of [intro], [elim], [dest]. Sledgehammer indicates that the following lemmas are relevant in the proof: always: converse_Un converse_converse plus either of: - inf_absorb2 and inf_le1 - subset_Un_eq - le_iff_inf Anyway, I found this lemma useful to have around explicitly. Maybe it could be added to Relation.thy? Any thoughts? I think the usual policy is to have at least two applications before adding such a lemma. However we use the corresponding lemma about conversep in the (co)datatype package. Since the latter will sooner or later become part of the HOL session anyway, I think it's fine to add both versions to Relation.thy. I'll do that (under the name converse(p)_mono). Dmitriy PS: for me this looks like an isabelle-users thread ;-) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
