Theory Generator_Aux
section ‹Shared Utilities for all Generator›
text ‹In this theory we mainly provide some Isabelle/ML infrastructure
that is used by several generators. It consists of a uniform interface
to access all the theorems, terms, etc.\ from the BNF package, and
some auxiliary functions which provide recursors on datatypes, common tactics, etc.›
theory Generator_Aux
imports
Main
begin
ML_file ‹bnf_access.ML›
ML_file ‹generator_aux.ML›
lemma in_set_simps:
"x ∈ set (y # z # ys) = (x = y ∨ x ∈ set (z # ys))"
"x ∈ set ([y]) = (x = y)"
"x ∈ set [] = False"
"Ball (set []) P = True"
"Ball (set [x]) P = P x"
"Ball (set (x # y # zs)) P = (P x ∧ Ball (set (y # zs)) P)"
by auto
lemma conj_weak_cong: "a = b ⟹ c = d ⟹ (a ∧ c) = (b ∧ d)" by auto
lemma refl_True: "(x = x) = True" by simp
end