Re: [isabelle] automatic case splitting during simp
Thanks; I found changing everything to using case-statementsm, as you
suggest, seemed to be the best approach (so far).
It would be nice to have some tools that let one derive case statements
from function definitions and visa-versa. Having the function definition
style of equations provides nice simp rules which don't expand the case
Tobias Nipkow wrote:
> You need to have a case-expression in your goal. If not, then you need
> to prove your own splitting lemma first:
> "P (reduce1_false2 gt g) = ((gt=T1 --> P g) & (gt=T2 --> P True) ...)"
> Then you can go
> apply(simp split: <split-lemma>)
> Lucas Dixon wrote:
>> What is the best way to get Isabelle to automatically perform certain
>> case analysis steps within simplification?
>> datatype gate = D | S | T1 | T2 | T3 | T4 | B1 | B2 | B3 | B4
>> fun reduce1_false2 :: "gate => bool => bool"
>> reduce1_false2_in_T1: "reduce1_false2 T1 g = g"
>> | reduce1_false2_in_T2: "reduce1_false2 T2 g = True"
>> | reduce1_false2_in_T3: "reduce1_false2 T3 g = ~ g"
>> | reduce1_false2_in_T4: "reduce1_false2 T4 g = True"
>> | reduce1_false2_in_B1: "reduce1_false2 B1 g = ~ g"
>> | reduce1_false2_in_B2: "reduce1_false2 B2 g = False"
>> | reduce1_false2_in_B3: "reduce1_false2 B3 g = g"
>> | reduce1_false2_in_B4: "reduce1_false2 B4 g = False"
>> | reduce1_false2_in_D: "reduce1_false2 D g = g"
>> | reduce1_false2_in_S: "reduce1_false2 S g = ~ g"
>> later when there is a goal of the form...
>> "P (reduce1_false2 gt g)"
>> I would like simp to automatically consider the cases for "gt".
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and