On 26/06/2015 16:43, Iulia Dragomir wrote:
Dear all, I have the following lemma within a theory: theory Test imports Main begin lemma lambda_true_top: "f (Î x . True) = F top" by (simp add: top_fun_def)
I assume you mean the same f/F on both sides. This does not cover abstraction over tuples, which is syntactic sugar for the combinator split :: "('a â 'b â 'c) â 'a Ã 'b â 'c". You also need
lemma lambda_pair_true_top: "f (Î (x,y) . True) = f top" by (simp add: split_def top_fun_def)However, the simplifier will not be able to use such rules, unless you instantiate the f with a concrete term.
end which I would like to use for lambda terms having different variables, like: lemma "F (Î (x,y) . True) = F top" or lemma "F (Î (x,y, (z, t), a, (b, c, d)) . True) = F top"
Now, if I use it as substitution rule, the goal is identical to the lemmas to be proved and if I try to add it as simplification rule, a failed application of proof method is raised. How can I use lambda_true_top in this proof? Or how can I write my original lemma such that it can be used to simplify a term like F (Î (x,y, (z, t), a, (b, c, d)) . True) to F top in general? In my case F is always a constant function. Thanks. Best regards, Iulia Dragomir
Description: S/MIME Cryptographic Signature