Lines Matching defs:thms
85 fun datatype_thms thms =
87 arm_stepTheory.Align, arm_stepTheory.Aligned] @ thms @ cond_thms @
140 fun addThms thms = (rwts := thms @ !rwts; thms)
181 val thms = [merge_cond, cond_rand_thms, isnot15, IsSecure_def,
186 EV thms [[``Extension_Security NOTIN ^st.Extensions``]] []
190 EV thms
652 fun regEV npcs thms ctxt s tm =
655 val thms =
657 npc_thms @ thms
663 EV thms ctxt s tm
668 fun memEV rl mem thms ctxt s tm =
670 val thms = [NullCheckIfThumbEE_rwt, IncPC_rwt, PC_rwt, R_rwt,
675 alignmentTheory.aligned_add_sub_123] @ thms
677 List.map (fn r => EV ([r] @ thms) ctxt s tm |> List.map rl) mem
682 fun storeEV rl mem thms ctxt s tm =
684 val thms = [NullCheckIfThumbEE_rwt,
692 R_rwt, write'R_rwt] @ thms
696 List.map (fn w => EV ([w] @ thms) ctxt s tm |> List.map rule) mem
1055 val thms = ref word_bit_16_thms
1056 val c = ref (PURE_REWRITE_CONV (!thms))
1067 val () = thms := !thms @ (bit_count_thms v)
1068 val () = c := PURE_REWRITE_CONV (!thms)
1468 val thms = fetch_thm tms
1471 case thms of
2674 val thms = [dfn'BranchTarget_def, PC_rwt, not_cond, align_aligned]
2679 EV (hd BranchWritePC_rwt :: thms) [] []
2686 EV (tl BranchWritePC_rwt @ thms) [] []
3968 val thms =
4122 thm :: thms) [] c
4125 (DATATYPE_CONV THENC REWRITE_CONV thms))
4138 IncPC_rwt] @ thm :: thms)
4142 (DATATYPE_CONV THENC REWRITE_CONV thms THENC DATATYPE_CONV))