Re: [isabelle] writing an Isar proof for multiple subgoals



On 13.07.2015 14:02, Buday Gergely wrote:
> 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?
[...]
> nominal_function simple4 :: "lam â lam"
> where
>   "simple4 x = x"
> proof -
>   have "eqvt simple4_graph_aux" by (simp add: eqvt_def simple4_graph_aux_def)

  show "eqvt simple4_graph_aux" ...
next
  fix x y assume "simple4_graph x y" show True ...
next
   fix P y assume "!!x. y = x ==> P" show P ...
...




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