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
statements.

cheers,
lucas

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>)
> 
> Tobias
> 
> Lucas Dixon wrote:
>> Hello,
>>
>> What is the best way to get Isabelle to automatically perform certain
>> case analysis steps within simplification?
>>
>> e.g.
>>
>> datatype gate = D | S | T1 | T2 | T3 | T4 | B1 | B2 | B3 | B4
>>
>> fun reduce1_false2 :: "gate => bool => bool"
>> where
>>   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".
>>
>> suggestions?
>>
>> thanks,
>> lucas
>>
>>
>>
> 
> 

-- 
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 MHonArc.