Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Test_Build_Thydata.thy
author Walther Neuper <wneuper@ist.tugraz.at>
Mon, 26 Aug 2019 09:20:07 +0200
changeset 59591 a2b0b338d966
parent 59590 b5ca83bf1ccd
child 59601 0cff71323cdd
permissions -rw-r--r--
cleanup Tools.thy, Descript.thy, Atools.thy 
     1 (* Minimal Thydata for test/../thy-hierarchy *)

     2 

     3 theory Test_Build_Thydata

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

     5 begin

     6 

     7 ML \<open>

     8 open Rule

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

    10 \<close>

    11 axiomatization where

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

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

    14 

    15 ML \<open>

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

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

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

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

    20 	scr = Rule.EmptyScr};

    21 

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

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

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

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

    26 	scr = Rule.EmptyScr};

    27 

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

    29 \<close>

    30 

    31 setup \<open>KEStore_Elems.add_rlss 

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

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

    34 

    35 ML \<open>

    36   @{thm refl};

    37   @{thm o_def};

    38 

    39 \<close> ML \<open>

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

    41 

    42 \<close> ML \<open>

    43 \<close> ML \<open>

    44 \<close> ML \<open>

    45 \<close> ML \<open>

    46 \<close> ML \<open>

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

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

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

    50 \<close> ML \<open>

    51 case ddd of

    52   ("rls111",

    53     ("Test_Build_Thydata",

    54      Rls {calc = [], erls =

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

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

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

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

    59           Prog (Const ("HOL.eq", _) $ (Const ("Atools.auto_generated", _) $ Free ("t_t", _)) $ _),

    60           srls = Erls})) => ()

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

    62 \<close> ML \<open>

    63 case eee of

    64   ("rls222",

    65     ("Test_Build_Thydata",

    66      Rls {calc = [], erls =

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

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

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

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

    71           scr =

    72           Prog (Const ("HOL.eq", _) $ (Const ("Atools.auto_generated", _) $ Free ("t_t", _)) $ _),

    73           srls = Erls})) => ()

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

    75 \<close>

    76 

    77 ML \<open>

    78 \<close> ML \<open>

    79 \<close>

    80 end
wneuper/isa