Theory Consts
section ‹Special constants›
theory Consts
imports
Constructors
Higher_Order_Terms.Nterm
begin
locale special_constants = constructors
locale pre_constants = special_constants +
fixes heads :: "name fset"
begin
definition all_consts :: "name fset" where
"all_consts = heads |∪| C"
abbreviation welldefined :: "'a::term ⇒ bool" where
"welldefined t ≡ consts t |⊆| all_consts"
sublocale welldefined: simple_syntactic_and welldefined
by standard auto
end
declare pre_constants.all_consts_def[code]
locale constants = pre_constants +
assumes disjnt: "fdisjnt heads C"
assumes distinct_ctr: "distinct all_constructors"
begin
lemma distinct_ctr': "distinct (map as_string all_constructors)"
unfolding distinct_map
using distinct_ctr
by (auto intro: inj_onI dest: name.expand)
end
end