Quelle UNITY_tactics.ML Sprache: SML

(*  Title:      HOL/UNITY/UNITY_tactics.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   2003  University of Cambridge

Specialized UNITY tactics.
*)

(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
fun Always_Int_tac ctxt =
  dresolve_tac ctxt @{thms Always_Int_I} THEN'
  assume_tac ctxt THEN'
  eresolve_tac ctxt @{thms Always_thin}

(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})

(*Proves "co" properties when the program is specified.  Any use of invariants
  (from weak constrains) must have been done already.*)
fun constrains_tac ctxt i =
  SELECT_GOAL
    (EVERY
     [REPEAT (Always_Int_tac ctxt 1),
      (*reduce the fancy safety properties to "constrains"*)
      REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
              ORELSE
              resolve_tac ctxt [@{thm StableI}, @{thm stableI},
                           @{thm constrains_imp_Constrains}] 1),
      (*for safety, the totalize operator can be ignored*)
      simp_tac (put_simpset HOL_ss ctxt
        addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
      resolve_tac ctxt @{thms constrainsI} 1,
      full_simp_tac ctxt 1,
      REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
      ALLGOALS (clarify_tac ctxt),
      ALLGOALS (asm_full_simp_tac ctxt)]) i;

(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
  SELECT_GOAL
    (EVERY
     [REPEAT (Always_Int_tac ctxt 1),
      eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
          REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
                            @{thm EnsuresI}, @{thm ensuresI}] 1),
      (*now there are two subgoals: co & transient*)
      simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
      Rule_Insts.res_inst_tac ctxt
        [((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
      ORELSE Rule_Insts.res_inst_tac ctxt
        [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
         (*simplify the command's domain*)
      simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
      constrains_tac ctxt 1,
      ALLGOALS (clarify_tac ctxt),
      ALLGOALS (asm_lr_simp_tac ctxt)]);

(*Composition equivalences, from Lift_prog*)

fun make_o_equivs ctxt th =
  [th,
   th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
   th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.