Chengsong Tan (Apr 25 2024 at 18:33): Chengsong Tan (Apr 25 2024 at 18:33):Suppose I have a list of functions [f1, f2, ..., fn] that take a type 'a element and returns a value of type 'a.
Now that I have proven each function satisfied some invariant G, how do I combine these lemmas with a case split to prove these functions as a list still satisfy that invariant? Namely:
lemma f1_good: "G a ==> G (f1 a)"
...
lemma fn_good: "G a ==> G (fn a)"
...
done
lemma together: "G a ==> a' \<in> (concat (map (\<lambda>f. f a) [f1, f2, ..., fn]))
==> G a'"
proof
case f1: using f1_good
case f2: using f2_good
...
qed
For example, in the following MWE, how do I construct a case split in the toplevel lemma, such that each case defines a scenario where a specific element is chosen from a list?
definition "P n = even n"
definition "Q n = (n ≥ 100)"
definition "Giant n = (P n ∧ Q n)"
definition "Rule2 n = (if n > 40 then [n + 2] else [])"
definition "Rule4 n = (if n > 50 then [n + 4] else [])"
definition "Rule6 n = (if n > 150 then [n + 6] else [])"
definition "lotsRules = [Rule2, Rule4, Rule6]"
lemma rule1: assumes "P n" "Q n" shows "Ball (set (Rule2 n)) Giant"
sorry
lemma rule2: assumes "P n" "Q n" shows "Ball (set (Rule4 n)) Giant"
sorry
lemma rule3: assumes "P n" "Q n" shows "Ball (set (Rule6 n)) Giant"
sorry
lemma toplevel: assumes "Giant n" shows "n' ∈ set (concat (map (λrule. rule n) lotsRules)) ⟹ Giant n'"
proof -
from assms(1) have i0: "P n" unfolding Giant_def apply(rule conjE) apply( assumption) done
from assms(1) have i1: "Q n" unfolding Giant_def apply(rule conjE) apply( assumption) done
show ?thesis
proof (cases n')―‹which rules have been taken›
case (rule 1)
case (rule 2)
...
oops
I would have written lots_of_rules as conjunction, completely avoiding the problem okay your rules are not predicates
Mathias Fleury (Apr 27 2024 at 17:11):lemma toplevel: assumes "Giant n" shows "n' ∈ set (concat (map (λrule. rule n) lotsRules)) ⟹ Giant n'"
proof -
from assms(1) have i0: "P n" unfolding Giant_def apply(rule conjE) apply( assumption) done
from assms(1) have i1: "Q n" unfolding Giant_def apply(rule conjE) apply( assumption) done
assume ‹n' ∈ set (concat (map (λrule. rule n) lotsRules))›
then show ?thesis
unfolding lotsRules_def list.map set_concat set_simps image_insert Union_insert Un_iff
proof (elim disjE, goal_cases)―‹which rules have been taken›
case (1)
show ?case
sorry
next
case (2)
show ?case
sorry
but again: is that really better than
definition "lotsRules x ≡ (Rule2 x @ Rule4 x @ Rule6 x)"
That being said, I am unsure why you could not find it by yourself
Mathias Fleury (Apr 27 2024 at 17:25):I mean, you know unfolding and find_theorems
Mathias Fleury (Apr 27 2024 at 17:26):So coming up with the right lemmas does not sound hard to me
Chengsong Tan (May 01 2024 at 22:29):Mathias Fleury said:
That being said, I am unsure why you could not find it by yourself
Thank you very much, Mathias!
My Isabelle/Isar dexterity does not yet get me anything like
n' ∈ set (Rule2 n) ∨ n' ∈ set (Rule4 n) ∨ n' ∈ set (Rule6 n) ∨ n' ∈ ⋃ (set {})
and also goal_cases` in the proof method I cannot come up with myself.
Now I know them :)
Any advice on improving such dexterity to be able to write more succinct and idiomatic proofs like this?
Mathias Fleury (May 02 2024 at 04:48):goal_cases is something you cannot guess (and not everyone like it, because the resulting proof is not really structured)
Mathias Fleury (May 02 2024 at 04:49):For elim, I suggest reading the chapter "the rules of the game" (chapter 5 https://isabelle.in.tum.de/doc/tutorial.pdf) to understand intro/dest
Mathias Fleury (May 02 2024 at 04:49):and then it is just a matter of finding the theorems with find_thm or the panel
Last updated: May 06 2024 at 12:29 UTC