1(* ------------------------------------------------------------------------- *)
2(* A conversion to evaluate trichotomy.                                      *)
3(* ------------------------------------------------------------------------- *)
4
5structure prob_trichotomyTools :> prob_trichotomyTools =
6struct
7
8open HolKernel Parse boolLib reduceLib computeLib pairSyntax combinTheory
9     pairTheory sequenceTheory prob_trichotomyTheory state_transformerTheory
10     prob_pseudoTheory;
11
12infix 1 THENC
13infix 0 ORELSEC;
14
15local
16  val compset = num_compset ();
17  val _ = add_thms [PROB_TRICHOTOMY_COMPUTE, BIND_DEF, o_THM, sdest_def,
18                    UNCURRY_DEF, SHD_PROB_PSEUDO, STL_PROB_PSEUDO,
19                    UNIT_DEF] compset;
20in
21  val PROB_TRICHOTOMY_CONV = CBV_CONV compset;
22end;
23
24fun chain f seq 0 = []
25  | chain f seq n =
26  let
27    val th = PROB_TRICHOTOMY_CONV (mk_comb (f, seq))
28    val (_, seq) = (dest_pair o snd o dest_eq o concl) th
29  in
30    th :: chain f seq (n - 1)
31  end;
32
33(*
34PROB_TRICHOTOMY_CONV ``prob_trichotomy (prob_pseudo 103 95 75 0)``;
35
36Count.apply (chain ``prob_trichotomy`` ``prob_pseudo 103 95 75 0``) 10;
37
38runtime: 2.050s,    gctime: 0.150s,     systime: 0.000s.
39Axioms asserted: 0.
40Definitions made: 0.
41Oracle invocations: 0.
42Theorems loaded from disk: 0.
43HOL primitive inference steps: 52505.
44Total: 52505.
45> val it =
46    [|- prob_trichotomy (prob_pseudo 103 95 75 0) =
47        ((T,F),prob_pseudo 103 95 75 65),
48
49     |- prob_trichotomy (prob_pseudo 103 95 75 65) =
50        ((F,T),prob_pseudo 103 95 75 33),
51
52     |- prob_trichotomy (prob_pseudo 103 95 75 33) =
53        ((T,F),prob_pseudo 103 95 75 94),
54
55     |- prob_trichotomy (prob_pseudo 103 95 75 94) =
56        ((T,F),prob_pseudo 103 95 75 107),
57
58     |- prob_trichotomy (prob_pseudo 103 95 75 107) =
59        ((T,T),prob_pseudo 103 95 75 2),
60
61     |- prob_trichotomy (prob_pseudo 103 95 75 2) =
62        ((T,T),prob_pseudo 103 95 75 143),
63
64     |- prob_trichotomy (prob_pseudo 103 95 75 143) =
65        ((F,T),prob_pseudo 103 95 75 55),
66
67     |- prob_trichotomy (prob_pseudo 103 95 75 55) =
68        ((F,T),prob_pseudo 103 95 75 96),
69
70     |- prob_trichotomy (prob_pseudo 103 95 75 96) =
71        ((T,F),prob_pseudo 103 95 75 34),
72
73     |- prob_trichotomy (prob_pseudo 103 95 75 34) =
74        ((T,T),prob_pseudo 103 95 75 32)] : thm list
75*)
76
77end;
78