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