[isabelle] automatic case splitting during simp


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