Theory Monomorphic_Superposition

theory Monomorphic_Superposition
  imports 
    Superposition

    First_Order_Clause.IsaFoR_Nonground_Clause_With_Equality
    First_Order_Clause.IsaFoR_Nonground_Context
    First_Order_Clause.Monomorphic_Typing
begin

locale monomorphic_superposition_calculus =
  monomorphic_term_typing +

  superposition_calculus where
  comp_subst = "(∘s)" and id_subst = Var and term_subst = "(⋅)" and term_vars = term.vars and
  apply_subst = apply_subst and subst_update = fun_upd and compose_context = "(∘c)" and
  term_from_ground = term.from_ground and term_to_ground = term.to_ground and hole = □ and
  apply_context = ctxt_apply_term and occurences = occurences and ground_hole = □ and
  apply_ground_context = apply_ground_context and compose_ground_context = "(∘c)" and
  welltyped = welltyped and term_is_ground = term.is_ground and GFun = "λf _. GFun f" and
  GMore = "λf _. More f" and ground_fun_symc = fun_symc and ground_extrac = "λ_. ()" and
  ground_subtermsl = subtermsl and ground_subcontext = subcontext and
  ground_subtermsr = subtermsr and ground_size = size and ground_hole_position = hole_pos and
  ground_context_at = context_atG and ground_sizec = size and ground_subterms = gargs and
  ground_fun_sym = groot_sym and ground_extra = "λ_. ()" and
  context_is_ground = context.is_ground and context_vars = context.vars and
  context_subst = context.subst and context_to_ground = context.to_ground and
  context_from_ground = context.from_ground


end