Stream: Beginner Questions

Topic: Question about the induct tactic

Hongjian Jiang (Jun 12 2023 at 12:31):

Deal all, I am interested in the induction tactic. There is a question when should we use the apply(induct a b arbitrary: c rule: x_induct).

When reading the tutorial from https://isabelle.in.tum.de/library/HOL/HOL-IMP/Big_Step.html, i am confused about this usage.

lemma sim_while_cong_aux:
  "(WHILE b DO c,s) ⇒ t  ⟹ c ∼ c' ⟹  (WHILE b DO c',s) ⇒ t"
apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct)
 apply blast
apply blast
done

Any help would be appreciated

Last updated: Apr 27 2024 at 12:25 UTC