(* Minimal Thydata for test/../thy-hierarchy *)

theory Test_Build_Thydata

  imports "Specify.ProgLang"

begin

ML \<open>

open Rule

fun termlessI (_: subst) uv = LibraryC.termless uv;

\<close>

axiomatization where

  thm111: "thm111 = thm111 + (111::int)" and

  thm222: "thm222 = thm222 + (222::int)"

ML \<open>

val rls111 = Rule_Def.Repeat {id = "rls111", 

	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule_Set.empty, 

	srls = Rule_Set.Empty, calc = [], errpatts = [],

	rules = [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})],

	scr = Rule.Empty_Prog};

val rls222 = Rule_Def.Repeat {id = "rls222", 

	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule_Set.empty, 

	srls = Rule_Set.Empty, calc = [], errpatts = [],

	rules = [Rule.Thm ("sym_thm111", @{thm thm111} RS @{thm sym}), Rule.Thm ("o_def", @{thm o_def})],

	scr = Rule.Empty_Prog};

val prep_rls' = Auto_Prog.prep_rls @{theory};

\<close>

setup \<open>KEStore_Elems.add_rlss 

  [("rls111", (Context.theory_name @{theory}, prep_rls' rls111)),

   ("rls222", (Context.theory_name @{theory}, prep_rls' rls222))]\<close>

ML \<open>

  @{thm refl};

  @{thm o_def};

\<close> ML \<open>

val [aaa, bbb, ccc, ddd, eee] = KEStore_Elems.get_rlss @{theory};

\<close> ML \<open>

if eq_set op = (map fst [aaa, bbb, ccc], ["e_rrls", "empty", "prog_expr"]) then ()

else raise ERROR "test/../thy-hierarchy CHANGED"

\<close> ML \<open>

case ddd of

  ("rls111",

    ("Test_Build_Thydata",

     Rule_Def.Repeat {calc = [], erls =

          Rule_Def.Repeat {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =

               ("dummy_ord", _), rules = [], scr = Empty_Prog, srls = Rule_Set.Empty},

          errpatts = [], id = "rls111", preconds = [], rew_ord = ("termlessI", _), rules =

          [Thm ("thm111", _), Thm ("refl", _)], scr = Empty_Prog, srls = Rule_Set.Empty})) => ()

| _ => raise ERROR "test/../thy-hierarchy CHANGED 4";

\<close> ML \<open>

case eee of

  ("rls222",

    ("Test_Build_Thydata",

     Rule_Def.Repeat {calc = [], erls =

          Rule_Def.Repeat {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =

               ("dummy_ord", _), rules = [], scr = Empty_Prog, srls = Rule_Set.Empty},

          errpatts = [], id = "rls222", preconds = [], rew_ord = ("termlessI", _), rules =

          [Thm ("sym_thm111", _), Thm ("o_def", _)], scr = Empty_Prog, srls = Rule_Set.Empty})) => ()

| _ => raise ERROR "test/../thy-hierarchy CHANGED 5";

\<close>

ML \<open>

\<close> ML \<open>

\<close>

end