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