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