Can I define some names for the theorem?

Question

Suppose I have a theorem:

theorem non_ASCII_thm_name: "True" by simp 

I want to define an ASCII name for non_ASCII_thm_name with something like the notation command. For example, for example:

 notation non_ASCII_thm_name ("ASCII_thm_name") 

The Isar notation and abbreviation commands can only be used with constants. Is there an Isar team that lets me do this?

It is advisable that everything I want my Isar team to provide is synonymous. For example, if I use sledgehammer , it would be preferable that there is only one theorem, non_ASCII_thm_name , so sledgehammer does not use the additional fact ASCII_thm_name .

Answer 1

A partial solution is to use the command:

 lemmas ASCII_thm_name = non_ASCII_thm_name 

This will define a new theorem called ASCII_thm_name , which will be the same as non_ASCII_thm_name .

Unfortunately, there is no guarantee that tools like find_theorems will use your new name, but will instead use their own heuristics to determine what is the "best" name to output back to the user.

An alternative synonym for lemmas is theorems , although the former is considered a more standard approach.