[isabelle] writing an Isar proof for multiple subgoals



Hi,

I have a Nominal Isabelle definition that ends up in four proof obligations. My question is more about Isar so write it to this general list.

nominal_function simple4 :: "lam â lam"
where
  "simple4 x = x"

goal (4 subgoals):
1. eqvt simple4_graph_aux
2. âx y. simple4_graph x y â True
3. âP x. (âxa. x = xa â P) â P
4. âx xa. x = xa â x = xa

apply (simp_all add: eqvt_def simple4_graph_aux_def)

would solve all the subgoals but how can I write an Isar proof that takes care of the subgoals individually?

I started an Isar proof but it is not clear how can I proceed:

theory Simple
imports "../../thy/Nominal2-Isabelle2015/Nominal/Ex/Lambda"

begin

nominal_function simple4 :: "lam â lam"
where
  "simple4 x = x"
proof -
  have "eqvt simple4_graph_aux" by (simp add: eqvt_def simple4_graph_aux_def)

- Gergely


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