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>
Thu, 30 May 2019 12:04:55 +0200
changeset 59547 a6dcec53aec0
parent 59472 3e904f8ec16c
child 59590 b5ca83bf1ccd
permissions -rw-r--r--
[-Test_Isac] funpack: switch auto-generated programs to partial_function 
     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 case aaa of ("list_rls", _) => () | _ => error "test/../thy-hierarchy CHANGED 1";

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

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

    46 \<close> ML \<open>

    47 case ddd of

    48   ("rls111",

    49     ("Test_Build_Thydata",

    50      Rls {calc = [], erls =

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

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

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

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

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

    56           srls = Erls})) => ()

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

    58 \<close> ML \<open>

    59 case eee of

    60   ("rls222",

    61     ("Test_Build_Thydata",

    62      Rls {calc = [], erls =

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

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

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

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

    67           scr =

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

    69           srls = Erls})) => ()

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

    71 \<close>

    72 

    73 ML \<open>

    74 \<close> ML \<open>

    75 \<close>

    76 end
wneuper/isa