1(*****************************************************************************) 2(* Examples of M1 *) 3(*****************************************************************************) 4 5(* Commands when run interactively: 6quietdec := true; (* Switch off output *) 7 8map load ["sexpTheory","imported_acl2Theory"]; 9open sexpTheory imported_acl2Theory; 10 11quietdec := false; (* Restore output *) 12*) 13 14 15(****************************************************************************** 16* Boilerplate needed for compilation: open HOL4 systems modules. 17******************************************************************************) 18open HolKernel Parse boolLib bossLib; 19 20(****************************************************************************** 21* Open theories (including ratTheory from Jens Brandt). 22******************************************************************************) 23 24open sexpTheory imported_acl2Theory; 25 26(*****************************************************************************) 27(* END BOILERPLATE *) 28(*****************************************************************************) 29 30(****************************************************************************** 31* Function to simplify imported ACL2 32******************************************************************************) 33 34val acl2_simp = 35 SIMP_RULE 36 list_ss 37 ([let_simp,andl_fold,itel_fold,itel_append, 38 forall2_thm,exists2_thm,forall_fold,exists_fold, 39 implies,andl_simp,not_simp,t_nil] 40 @ 41 (map GSYM [int_def,nat_def,List_def,asym_def,csym_def,ksym_def,osym_def])); 42 43(****************************************************************************** 44M1 contains simplified definitions and theorems from other theories 45******************************************************************************) 46 47val Examples1 = 48 [("exclaim_def", acl2_simp exclaim_defun), 49 ("ifact_def", acl2_simp ifact_defun), 50 ("ifact_lemma", acl2_simp ifact_lemma_thm), 51 ("ifact_is_factorial", acl2_simp ifact_is_factorial_thm), 52 ("ifact_correct", acl2_simp ifact_correct_thm), 53 ("repeat_def", acl2_simp repeat_defun), 54 ("ifact_sched_def", acl2_simp ifact_sched_defun), 55 ("test_ifact_examples", acl2_simp test_ifact_examples_thm)]; 56 57val Examples2 = map (I ## acl2_simp) (theorems "imported_acl2"); 58 59