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