1structure tripleLib :> tripleLib =
2struct
3
4open HolKernel Parse boolLib bossLib
5open progTheory tripleTheory helperLib
6
7val ERR = Feedback.mk_HOL_ERR "triple"
8
9(* ------------------------------------------------------------------------ *)
10
11val CODE_CONV = RATOR_CONV o RAND_CONV
12val POST_CONV = RAND_CONV o RAND_CONV
13val PRE_CONV = RATOR_CONV o RATOR_CONV o POST_CONV
14
15(* ------------------------------------------------------------------------ *)
16val PAIR_LEMMA = Q.prove(
17   `((x1 = y1) ==> (x2 = y2) ==> b) ==> (((x2,x1) = (y2:'a,y1:'b)) ==> b)`,
18   SIMP_TAC std_ss [])
19
20val pair_rule =
21   Drule.UNDISCH_ALL o Lib.repeat (Drule.MATCH_MP PAIR_LEMMA) o DISCH_ALL
22
23val precond_thm = Q.prove(
24   `!b. precond b = cond (Abbrev b): 'a set set`,
25   SIMP_TAC std_ss [markerTheory.Abbrev_def,set_sepTheory.precond_def])
26
27val precond_rule =
28   UNDISCH_ALL o
29   Conv.CONV_RULE
30      (helperLib.PRE_CONV
31          (PURE_ONCE_REWRITE_CONV [precond_thm]
32           THENC helperLib.MERGE_CONDS_CONV)
33       THENC PURE_ONCE_REWRITE_CONV [progTheory.SPEC_MOVE_COND])
34
35fun add_prime v = Term.mk_var (fst (Term.dest_var v) ^ "'", Term.type_of v)
36
37fun find_match [] tm = fail()
38  | find_match (x::xs) tm =
39       fst (match_term x tm) handle HOL_ERR _ => find_match xs tm
40
41fun FORCE_DISCH_ALL thm =
42   (if List.null (Thm.hyp thm)
43       then Thm.DISCH boolSyntax.T
44    else Drule.DISCH_ALL) thm
45
46fun spec_to_triple_rule (pc, assert_thm, model_def) =
47   let
48      val assert_rwt =
49         assert_thm
50         |> Drule.SPEC_ALL
51         |> Conv.CONV_RULE (Conv.RHS_CONV helperLib.STAR_AC_CONV)
52         |> GSYM
53      val targets = progSyntax.strip_star (utilsLib.lhsc assert_rwt)
54      val ASSERT_INTRO_CONV = helperLib.STAR_AC_CONV
55                              THENC Conv.REWR_CONV assert_rwt
56      val model = boolSyntax.lhs (Thm.concl model_def)
57      val intro_triple =
58         tripleTheory.INTRO_TRIPLE
59         |> Drule.ISPEC model
60         |> Conv.CONV_RULE (Conv.LAND_CONV (REWRITE_CONV [model_def]))
61      val intro_triple_rule =
62         REWRITE_RULE [] o
63         Thm.SPEC (Term.mk_var ("cond", ``:bool``)) o
64         Drule.MATCH_MP intro_triple o
65         FORCE_DISCH_ALL o
66         Conv.CONV_RULE (helperLib.PRE_POST_CONV ASSERT_INTRO_CONV)
67      (* abbreviate posts *)
68      fun abbrev_conv pat post =
69         if pat = pc
70            then ALL_CONV post
71         else if is_var pat
72            then if pat = post
73                    then ALL_CONV post
74                 else ASSUME (mk_eq (post, add_prime pat))
75         else if is_comb pat
76            then (RAND_CONV (abbrev_conv (rand pat))
77                  THENC RATOR_CONV (abbrev_conv (rator pat))) post
78         else if pat = post
79            then ALL_CONV post
80         else NO_CONV post
81   in
82      fn th =>
83         let
84            val th = precond_rule th
85            val ps = progSyntax.strip_star (progSyntax.dest_pre (Thm.concl th))
86            val fnd = find_match ps
87            val (xs, frame) =
88               List.foldr (fn (t, (sbst, frm)) =>
89                  case Lib.total fnd t of
90                     SOME s => (sbst @ s, frm)
91                   | NONE => (sbst, t :: frm)) ([], []) targets
92            val th =
93               th |> Thm.INST xs
94                  |> helperLib.SPECC_FRAME_RULE (progSyntax.list_mk_star frame)
95                  |> intro_triple_rule
96            val pat = th |> concl |> rator |> rator |> rand
97         in
98            pair_rule (CONV_RULE (RAND_CONV (abbrev_conv pat)) th)
99         end
100   end
101
102(* ------------------------------------------------------------------------ *)
103
104end
105