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