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

theory Test_Build_Thydata

imports "~~/src/Tools/isac/ProgLang/ProgLang"

begin

ML {*

open Rule

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

*}

axiomatization where

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

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

ML {*

val rls111 = Rule.Rls {id = "rls111", 

	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule.e_rls, 

	srls = Rule.Erls, calc = [], errpatts = [],

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

	scr = Rule.EmptyScr};

val rls222 = Rule.Rls {id = "rls222", 

	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule.e_rls, 

	srls = Rule.Erls, calc = [], errpatts = [],

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

	scr = Rule.EmptyScr};

val prep_rls' = LTool.prep_rls @{theory ProgLang};

*}

setup {* KEStore_Elems.add_rlss 

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

   ("rls222", (Context.theory_name @{theory ProgLang}, prep_rls' rls222))] *}

ML {*

  @{thm refl};

  @{thm o_def};

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

case aaa of ("list_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 1";

case bbb of ("e_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 2";

case ccc of ("e_rrls", _) => () | _ => error "test/../thy-hierarchy CHANGED 3";

case ddd of

  ("rls111",

    ("ProgLang",

     Rls {calc = [], erls =

          Rls {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =

               ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Erls},

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

          [Thm ("thm111", _), Thm ("refl", _)], scr =

          Prog (Const ("Script.Stepwise", _) $ Free ("t_t", _) $ _),

          srls = Erls})) => ()

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

case eee of

  ("rls222",

    ("ProgLang",

     Rls {calc = [], erls =

          Rls {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =

               ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Erls},

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

          [Thm ("sym_thm111", _), Thm ("o_def", _)],

          scr =

          Prog (Const ("Script.Stepwise", _) $ Free ("t_t", _) $ _),

          srls = Erls})) => ()

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

*}

ML {*

*} ML {*

*}

end