Re: [isabelle] Ad-hoc-proving attributes



> I was wondering whether it'd make sense to unify the mechanisms behind
> "inductive_cases", "inductive_simps", "fun_cases" etc.; namely, commands
> which prove some theorems on the spot, but apart from binding them to a
> name, have no further side effects on the theory.

Lars just pointed out another candidate: "case_of_simps",
"simps_of_case". With my proposal, one could write

  thm foo_case = [[case_of_simps foo.simps]]
  note foo_case = [[case_of_simps foo.simps]]

instead of using the specialized command

  case_of_simps foo_case: foo.simps

This attribute could be implemented right now, but not "simps_of_case",
because the latter would need to return multiple theorems.




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