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