# [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.*