1structure tripleSyntax :> tripleSyntax =
2struct
3
4open Abbrev HolKernel
5open tripleTheory
6
7val ERR = mk_HOL_ERR "tripleSyntax"
8
9(* ----------------------------------------------------------------------- *)
10
11val (triple_tm, mk_triple, dest_triple, is_triple) =
12   HolKernel.syntax_fns4 "triple" "TRIPLE"
13
14val (case_sum_tm, mk_case_sum, dest_case_sum, is_case_sum) =
15   HolKernel.syntax_fns3 "triple" "case_sum"
16
17fun dest_model tm = let val (m, _, _, _) = dest_triple tm in m end
18fun dest_pre tm = let val (_, p, _, _) = dest_triple tm in p end
19fun dest_code tm = let val (_, _, c, _) = dest_triple tm in c end
20fun dest_post tm = let val (_, _, _, q) = dest_triple tm in q end
21fun dest_pre_post tm = let val (_, p, _, q) = dest_triple tm in (p, q) end
22
23fun get_component P thm =
24   case Thm.hyp thm of
25      [h] => let
26                val (l, r) = boolSyntax.dest_eq h
27                val l = pairSyntax.strip_pair l
28                val r = pairSyntax.strip_pair r
29             in
30                case Lib.total (Lib.index P) r of
31                   SOME n => List.nth (l, n)
32                 | NONE => raise ERR "get_component" "not found"
33             end
34    | _ => raise ERR "get_component" "not single hyp"
35
36(* ----------------------------------------------------------------------- *)
37
38end
39