Admin/Benchmarks/HOL-datatype/Verilog.thy

Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.

(*  Title:      Admin/Benchmarks/HOL-datatype/Verilog.thy
    ID:         $Id$
*)

theory Verilog imports Main begin

(* ------------------------------------------------------------------------- *)
(* Example from Daryl: a Verilog grammar.                                    *)
(* ------------------------------------------------------------------------- *)

datatype
  Source_text
     = module string "string list" "Module_item list"
     | Source_textMeta string
and
  Module_item
     = declaration Declaration
     | initial Statement
     | always Statement
     | assign Lvalue Expression
     | Module_itemMeta string
and
  Declaration
     = reg_declaration "Range option" "string list"
     | net_declaration "Range option" "string list"
     | input_declaration "Range option" "string list"
     | output_declaration "Range option" "string list"
     | DeclarationMeta string
and
  Range = range Expression Expression | RangeMeta string
and
  Statement
     = clock_statement Clock Statement_or_null
     | blocking_assignment Lvalue Expression
     | non_blocking_assignment Lvalue Expression
     | conditional_statement
          Expression Statement_or_null "Statement_or_null option"
     | case_statement Expression "Case_item list"
     | while_loop Expression Statement
     | repeat_loop Expression Statement
     | for_loop
          Lvalue Expression Expression Lvalue Expression Statement
     | forever_loop Statement
     | disable string
     | seq_block "string option" "Statement list"
     | StatementMeta string
and
  Statement_or_null
     = statement Statement | null_statement | Statement_or_nullMeta string
and
  Clock
     = posedge string
     | negedge string
     | clock string
     | ClockMeta string
and
  Case_item
     = case_item "Expression list" Statement_or_null
     | default_case_item Statement_or_null
     | Case_itemMeta string
and
  Expression
     = plus Expression Expression
     | minus Expression Expression
     | lshift Expression Expression
     | rshift Expression Expression
     | lt Expression Expression
     | leq Expression Expression
     | gt Expression Expression
     | geq Expression Expression
     | logeq Expression Expression
     | logneq Expression Expression
     | caseeq Expression Expression
     | caseneq Expression Expression
     | bitand Expression Expression
     | bitxor Expression Expression
     | bitor Expression Expression
     | logand Expression Expression
     | logor Expression Expression
     | conditional Expression Expression Expression
     | positive Primary
     | negative Primary
     | lognot Primary
     | bitnot Primary
     | reducand Primary
     | reducxor Primary
     | reducor Primary
     | reducnand Primary
     | reducxnor Primary
     | reducnor Primary
     | primary Primary
     | ExpressionMeta string
and
  Primary
     = primary_number Number
     | primary_IDENTIFIER string
     | primary_bit_select string Expression
     | primary_part_select string Expression Expression
     | primary_gen_bit_select Expression Expression
     | primary_gen_part_select Expression Expression Expression
     | primary_concatenation Concatenation
     | primary_multiple_concatenation Multiple_concatenation
     | brackets Expression
     | PrimaryMeta string
and
  Lvalue
     = lvalue string
     | lvalue_bit_select string Expression
     | lvalue_part_select string Expression Expression
     | lvalue_concatenation Concatenation
     | LvalueMeta string
and
  Number
     = decimal string
     | based "string option" string
     | NumberMeta string
and
  Concatenation
     = concatenation "Expression list" | ConcatenationMeta string
and
  Multiple_concatenation
     = multiple_concatenation Expression "Expression list"
     | Multiple_concatenationMeta string
and
  meta
     = Meta_Source_text Source_text
     | Meta_Module_item Module_item
     | Meta_Declaration Declaration
     | Meta_Range Range
     | Meta_Statement Statement
     | Meta_Statement_or_null Statement_or_null
     | Meta_Clock Clock
     | Meta_Case_item Case_item
     | Meta_Expression Expression
     | Meta_Primary Primary
     | Meta_Lvalue Lvalue
     | Meta_Number Number
     | Meta_Concatenation Concatenation
     | Meta_Multiple_concatenation Multiple_concatenation

end