src/HOL/UNITY/UNITY_tactics.ML
author wenzelm
Thu Jul 23 22:13:42 2015 +0200 (2015-07-23)
changeset 60773 d09c66a0ea10
parent 60754 02924903a6fd
child 60774 6c28d8ed2488
permissions -rw-r--r--
more symbols by default, without xsymbols mode;
paulson@13786
     1
(*  Title:      HOL/UNITY/UNITY_tactics.ML
paulson@13786
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13786
     3
    Copyright   2003  University of Cambridge
paulson@13786
     4
wenzelm@24147
     5
Specialized UNITY tactics.
paulson@13786
     6
*)
paulson@13786
     7
paulson@13797
     8
(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
wenzelm@58963
     9
fun Always_Int_tac ctxt =
wenzelm@60754
    10
  dresolve_tac ctxt @{thms Always_Int_I} THEN'
wenzelm@60754
    11
  assume_tac ctxt THEN'
wenzelm@60754
    12
  eresolve_tac ctxt @{thms Always_thin}
paulson@13797
    13
paulson@13797
    14
(*Combines a list of invariance THEOREMS into one.*)
wenzelm@24147
    15
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
paulson@13797
    16
paulson@13812
    17
(*Proves "co" properties when the program is specified.  Any use of invariants
paulson@13812
    18
  (from weak constrains) must have been done already.*)
wenzelm@42767
    19
fun constrains_tac ctxt i =
wenzelm@42793
    20
  SELECT_GOAL
wenzelm@42793
    21
    (EVERY
wenzelm@58963
    22
     [REPEAT (Always_Int_tac ctxt 1),
wenzelm@42793
    23
      (*reduce the fancy safety properties to "constrains"*)
wenzelm@60754
    24
      REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
wenzelm@42793
    25
              ORELSE
wenzelm@59498
    26
              resolve_tac ctxt [@{thm StableI}, @{thm stableI},
wenzelm@42793
    27
                           @{thm constrains_imp_Constrains}] 1),
wenzelm@42793
    28
      (*for safety, the totalize operator can be ignored*)
wenzelm@51717
    29
      simp_tac (put_simpset HOL_ss ctxt
wenzelm@51717
    30
        addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
wenzelm@60754
    31
      resolve_tac ctxt @{thms constrainsI} 1,
wenzelm@51717
    32
      full_simp_tac ctxt 1,
wenzelm@60754
    33
      REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
wenzelm@42793
    34
      ALLGOALS (clarify_tac ctxt),
wenzelm@51717
    35
      ALLGOALS (asm_full_simp_tac ctxt)]) i;
paulson@13786
    36
paulson@13786
    37
(*proves "ensures/leadsTo" properties when the program is specified*)
wenzelm@42767
    38
fun ensures_tac ctxt sact =
wenzelm@42793
    39
  SELECT_GOAL
wenzelm@42793
    40
    (EVERY
wenzelm@58963
    41
     [REPEAT (Always_Int_tac ctxt 1),
wenzelm@60754
    42
      eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
wenzelm@42793
    43
          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
wenzelm@42793
    44
          REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
wenzelm@42793
    45
                            @{thm EnsuresI}, @{thm ensuresI}] 1),
wenzelm@42793
    46
      (*now there are two subgoals: co & transient*)
wenzelm@51717
    47
      simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
wenzelm@59763
    48
      Rule_Insts.res_inst_tac ctxt
wenzelm@59780
    49
        [((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
wenzelm@59763
    50
      ORELSE Rule_Insts.res_inst_tac ctxt
wenzelm@59780
    51
        [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
wenzelm@42793
    52
         (*simplify the command's domain*)
wenzelm@51717
    53
      simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
wenzelm@42793
    54
      constrains_tac ctxt 1,
wenzelm@42793
    55
      ALLGOALS (clarify_tac ctxt),
wenzelm@51717
    56
      ALLGOALS (asm_lr_simp_tac ctxt)]);
paulson@13796
    57
paulson@13786
    58
paulson@13786
    59
(*Composition equivalences, from Lift_prog*)
paulson@13786
    60
wenzelm@51717
    61
fun make_o_equivs ctxt th =
wenzelm@51717
    62
  [th,
wenzelm@51717
    63
   th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
wenzelm@51717
    64
   th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];
paulson@13786
    65