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>)
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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and