Theory IsaFoR

(*  Title:      Benchmarks/Datatype_Benchmark/IsaFoR.thy
    Author:     Rene Thiemann, UIBK
    Copyright   2014

Benchmark consisting of datatypes defined in IsaFoR.
*)

section ‹Benchmark Consisting of Datatypes Defined in IsaFoR›

theory IsaFoR
imports HOL.Real
begin

datatype (discs_sels) ('f, 'l) lab =
    Lab "('f, 'l) lab" 'l
  | FunLab "('f, 'l) lab" "('f, 'l) lab list"
  | UnLab 'f
  | Sharp "('f, 'l) lab"

datatype (discs_sels) 'f projL = Projection "(('f × nat) × nat) list"

datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
datatype (discs_sels) ('f, 'v) ctxt =
    Hole ("□")
  | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"

type_synonym ('f, 'v) rule = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) trs  = "('f, 'v) rule set"

type_synonym ('f, 'v) rules = "('f, 'v) rule list"
type_synonym ('f, 'l, 'v) ruleLL  = "(('f, 'l) lab, 'v) rule"
type_synonym ('f, 'l, 'v) trsLL   = "(('f, 'l) lab, 'v) rules"
type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"

datatype (discs_sels) pos = Empty ("ε") | PCons "nat" "pos" (infixr "<#" 70)

type_synonym  ('f, 'v) prseq = "(pos × ('f, 'v) rule × bool × ('f, 'v) term) list"
type_synonym  ('f, 'v) rseq = "(pos × ('f, 'v) rule × ('f, 'v) term) list"

type_synonym ('f, 'l, 'v) rseqL   = "((('f, 'l) lab, 'v) rule × (('f, 'l) lab, 'v) rseq) list"
type_synonym ('f, 'l, 'v) dppLL   =
  "bool × bool × ('f, 'l, 'v) trsLL × ('f, 'l, 'v) trsLL ×
  ('f, 'l, 'v) termsLL ×
  ('f, 'l, 'v) trsLL × ('f, 'l, 'v) trsLL"

type_synonym ('f, 'l, 'v) qreltrsLL =
  "bool × ('f, 'l, 'v) termsLL × ('f, 'l, 'v) trsLL × ('f, 'l, 'v) trsLL"

type_synonym ('f, 'l, 'v) qtrsLL =
  "bool × ('f, 'l, 'v) termsLL × ('f, 'l, 'v) trsLL"

datatype (discs_sels) location = H | A | B | R

type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt × ('f, 'v) term × location"
type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set"

type_synonym ('f, 'l, 'v) fptrsLL =
  "(('f, 'l) lab, 'v) forb_pattern list × ('f, 'l, 'v) trsLL"

type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL"

type_synonym ('f, 'a) lpoly_inter = "'f × nat ⇒ ('a × 'a list)"
type_synonym ('f, 'a) lpoly_interL = "(('f × nat) × ('a × 'a list)) list"

type_synonym 'v monom = "('v × nat) list"
type_synonym ('v, 'a) poly = "('v monom × 'a) list"
type_synonym ('f, 'a) poly_inter_list = "(('f × nat) × (nat, 'a) poly) list"
type_synonym 'a vec = "'a list"
type_synonym 'a mat = "'a vec list"

datatype (discs_sels) arctic = MinInfty | Num_arc int
datatype (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
datatype (discs_sels) order_tag = Lex | Mul

type_synonym 'f status_prec_repr = "(('f × nat) × (nat × order_tag)) list"

datatype (discs_sels) af_entry =
    Collapse nat
  | AFList "nat list"

type_synonym 'f afs_list = "(('f × nat) × af_entry) list"
type_synonym 'f prec_weight_repr = "(('f × nat) × (nat × nat × (nat list option))) list × nat"

datatype (discs_sels) 'f redtriple_impl =
    Int_carrier "('f, int) lpoly_interL"
  | Int_nl_carrier "('f, int) poly_inter_list"
  | Rat_carrier "('f, rat) lpoly_interL"
  | Rat_nl_carrier rat "('f, rat) poly_inter_list"
  | Real_carrier "('f, real) lpoly_interL"
  | Real_nl_carrier real "('f, real) poly_inter_list"
  | Arctic_carrier "('f, arctic) lpoly_interL"
  | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL"
  | Int_mat_carrier nat nat "('f, int mat) lpoly_interL"
  | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL"
  | Real_mat_carrier nat nat "('f, real mat) lpoly_interL"
  | Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL"
  | Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL"
  | RPO "'f status_prec_repr" "'f afs_list"
  | KBO "'f prec_weight_repr" "'f afs_list"

datatype (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext
type_synonym 'f scnp_af = "(('f × nat) × (nat × nat) list) list"

datatype (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"

type_synonym 'f sig_map_list = "(('f × nat) × 'f list) list"
type_synonym ('f, 'v) uncurry_info = "'f × 'f sig_map_list × ('f, 'v) rules × ('f, 'v) rules"

datatype (discs_sels) arithFun =
    Arg nat
  | Const nat
  | Sum "arithFun list"
  | Max "arithFun list"
  | Min "arithFun list"
  | Prod "arithFun list"
  | IfEqual arithFun arithFun arithFun arithFun

datatype (discs_sels) 'f sl_inter = SL_Inter nat "(('f × nat) × arithFun) list"
datatype (discs_sels) ('f, 'v) sl_variant =
    Rootlab "('f × nat) option"
  | Finitelab "'f sl_inter"
  | QuasiFinitelab "'f sl_inter" 'v

type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term × ('f, 'v) rseq × ('f, 'v) term × ('f, 'v) rseq) list"

datatype (discs_sels) 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat

type_synonym unknown_info = string

type_synonym dummy_prf = unit

datatype (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
  "('f, 'v) term"
  "(('f, 'v) rule × ('f, 'v) rule) list"