From: <mj...@us...> - 2008-09-30 11:22:52
|
Revision: 6228 http://hol.svn.sourceforge.net/hol/?rev=6228&view=rev Author: mjcg Date: 2008-09-30 11:22:42 +0000 (Tue, 30 Sep 2008) Log Message: ----------- Made some rewrites persistent for EVAL (add_funs --> add_persistent_funs) Modified Paths: -------------- HOL/examples/opsemTools/newOpsemScript.sml HOL/examples/opsemTools/verify/PATH_EVAL.sml HOL/examples/opsemTools/verify/PATH_EVAL_Examples.ml HOL/examples/opsemTools/verify/examples.ml Modified: HOL/examples/opsemTools/newOpsemScript.sml =================================================================== --- HOL/examples/opsemTools/newOpsemScript.sml 2008-09-30 02:07:44 UTC (rev 6227) +++ HOL/examples/opsemTools/newOpsemScript.sml 2008-09-30 11:22:42 UTC (rev 6228) @@ -541,6 +541,18 @@ val _ = new_theory "newOpsem"; +val _ = computeLib.add_persistent_funs + [("finite_mapTheory.FUPDATE_LIST_THM",FUPDATE_LIST_THM), + ("finite_mapTheory.DOMSUB_FUPDATE_THM",DOMSUB_FUPDATE_THM), + ("finite_mapTheory.DOMSUB_FEMPTY",DOMSUB_FEMPTY), + ("finite_mapTheory.FDOM_FUPDATE",FDOM_FUPDATE), + ("finite_mapTheory.FAPPLY_FUPDATE_THM",FAPPLY_FUPDATE_THM), + ("finite_mapTheory.FDOM_FEMPTY",FDOM_FEMPTY), + ("pred_setTheory.IN_INSERT",pred_setTheory.IN_INSERT), + ("pred_setTheory.NOT_IN_EMPTY",pred_setTheory.NOT_IN_EMPTY), + ("integerTheory.NUM_OF_INT", integerTheory.NUM_OF_INT) + ]; + (* make infix ``$/`` equal to ``$DIV`` *) val DIV_AUX_def = xDefine "DIV_AUX" `m / n = m DIV n`; @@ -1460,7 +1472,11 @@ THEN RW_TAC std_ss []]); (* Add to EVAL compset *) -val _ = computeLib.add_funs[outcome_case_def,outcome_case_if,pair_case_if]; +val _ = computeLib.add_persistent_funs + [("outcome_case_def",outcome_case_def), + ("outcome_case_if",outcome_case_if), + ("pair_case_if",pair_case_if) + ]; (* Technical theorem to make EVAL work with lists for executing STEP_LIST *) val CONS_if = @@ -1521,7 +1537,7 @@ RW_TAC std_ss [RUN_BIND_RUN_RETURN_def,RUN_BIND_def,RUN_RETURN_def]); (* Add to EVAL compset *) -val _ = computeLib.add_funs[CONS_if]; +val _ = computeLib.add_persistent_funs[("CONS_if",CONS_if)]; (*===========================================================================*) (* Clocked big step evaluator *) @@ -1690,18 +1706,9 @@ THEN RW_TAC arith_ss [RUN_def,RUN_BIND_def]); (* Tell EVAL about RUN and various properties of finite mape *) -val _ = computeLib.add_funs - [RUN, - FAPPLY_FUPDATE_THM, - DOMSUB_FUPDATE_THM, - DOMSUB_FEMPTY, - FDOM_FUPDATE, - FAPPLY_FUPDATE_THM, - FDOM_FEMPTY, - pred_setTheory.IN_INSERT, - pred_setTheory.NOT_IN_EMPTY - ]; +val _ = computeLib.add_persistent_funs[("RUN",RUN)]; + (*===========================================================================*) (* Small step next-state function *) (*===========================================================================*) @@ -1768,7 +1775,7 @@ THEN RW_TAC list_ss [STEP1_def]); (* Add to EVAL compset *) -val _ = computeLib.add_funs [STEP1]; +val _ = computeLib.add_persistent_funs [("STEP1",STEP1)]; (* Various lemmas follow -- I'm not sure they are all needed *) val SMALL_EVAL_IMP_STEP1 = @@ -2524,7 +2531,7 @@ THEN RW_TAC std_ss [ACC_STEP_def,ACC_STEP_BIND_def]); (* Add to EVAL compset *) -val _ = computeLib.add_funs [ACC_STEP]; +val _ = computeLib.add_persistent_funs [("ACC_STEP",ACC_STEP)]; val ACC_STEP_STEP = store_thm Modified: HOL/examples/opsemTools/verify/PATH_EVAL.sml =================================================================== --- HOL/examples/opsemTools/verify/PATH_EVAL.sml 2008-09-30 02:07:44 UTC (rev 6227) +++ HOL/examples/opsemTools/verify/PATH_EVAL.sml 2008-09-30 11:22:42 UTC (rev 6228) @@ -32,7 +32,8 @@ FDOM_FEMPTY, pred_setTheory.IN_INSERT, pred_setTheory.NOT_IN_EMPTY, - ACC_STEP + ACC_STEP, + integerTheory.NUM_OF_INT ]; (* Modified: HOL/examples/opsemTools/verify/PATH_EVAL_Examples.ml =================================================================== --- HOL/examples/opsemTools/verify/PATH_EVAL_Examples.ml 2008-09-30 02:07:44 UTC (rev 6227) +++ HOL/examples/opsemTools/verify/PATH_EVAL_Examples.ml 2008-09-30 11:22:42 UTC (rev 6228) @@ -19,7 +19,7 @@ quietdec := false; (* turn printing back on *) -(* Set up the compset for computeLib.EVAL *) +(* Set up the compset for computeLib.EVAL add_funs [outcome_case_def, outcome_case_if, @@ -36,6 +36,7 @@ pred_setTheory.IN_INSERT, pred_setTheory.NOT_IN_EMPTY ]; +*) (* Cause assumptions and tags to be printed *) show_assums := true; Modified: HOL/examples/opsemTools/verify/examples.ml =================================================================== --- HOL/examples/opsemTools/verify/examples.ml 2008-09-30 02:07:44 UTC (rev 6227) +++ HOL/examples/opsemTools/verify/examples.ml 2008-09-30 11:22:42 UTC (rev 6228) @@ -19,24 +19,6 @@ quietdec := false; (* turn printing back on *) -(* Set up the compset for computeLib.EVAL *) -add_funs - [outcome_case_def, - outcome_case_if, - pair_case_if, - RUN, - STEP1, - FAPPLY_FUPDATE_THM, - FUPDATE_LIST_THM, - DOMSUB_FUPDATE_THM, - DOMSUB_FEMPTY, - FDOM_FUPDATE, - FAPPLY_FUPDATE_THM, - FDOM_FEMPTY, - pred_setTheory.IN_INSERT, - pred_setTheory.NOT_IN_EMPTY - ]; - (* Cause assumptions and tags to be printed show_assums := true; show_tags := true; This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |