Re: [isabelle] automatic case splitting during simp



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.