src/HOL/UNITY/UNITY_tactics.ML
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45138 ba618e9288b8
child 46752 e9e7209eb375
permissions -rw-r--r--
Quotient_Info stores only relation maps
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@24147
     9
val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
paulson@13797
    10
paulson@13797
    11
(*Combines a list of invariance THEOREMS into one.*)
wenzelm@24147
    12
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
paulson@13797
    13
paulson@13812
    14
(*Proves "co" properties when the program is specified.  Any use of invariants
paulson@13812
    15
  (from weak constrains) must have been done already.*)
wenzelm@42767
    16
fun constrains_tac ctxt i =
wenzelm@42793
    17
  SELECT_GOAL
wenzelm@42793
    18
    (EVERY
wenzelm@42793
    19
     [REPEAT (Always_Int_tac 1),
wenzelm@42793
    20
      (*reduce the fancy safety properties to "constrains"*)
wenzelm@42793
    21
      REPEAT (etac @{thm Always_ConstrainsI} 1
wenzelm@42793
    22
              ORELSE
wenzelm@42793
    23
              resolve_tac [@{thm StableI}, @{thm stableI},
wenzelm@42793
    24
                           @{thm constrains_imp_Constrains}] 1),
wenzelm@42793
    25
      (*for safety, the totalize operator can be ignored*)
wenzelm@42793
    26
      simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
wenzelm@42793
    27
      rtac @{thm constrainsI} 1,
wenzelm@42793
    28
      full_simp_tac (simpset_of ctxt) 1,
wenzelm@42793
    29
      REPEAT (FIRSTGOAL (etac disjE)),
wenzelm@42793
    30
      ALLGOALS (clarify_tac ctxt),
wenzelm@42793
    31
      ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
paulson@13786
    32
paulson@13786
    33
(*proves "ensures/leadsTo" properties when the program is specified*)
wenzelm@42767
    34
fun ensures_tac ctxt sact =
wenzelm@42793
    35
  SELECT_GOAL
wenzelm@42793
    36
    (EVERY
wenzelm@42793
    37
     [REPEAT (Always_Int_tac 1),
wenzelm@42793
    38
      etac @{thm Always_LeadsTo_Basis} 1
wenzelm@42793
    39
          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
wenzelm@42793
    40
          REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
wenzelm@42793
    41
                            @{thm EnsuresI}, @{thm ensuresI}] 1),
wenzelm@42793
    42
      (*now there are two subgoals: co & transient*)
wenzelm@42793
    43
      simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
wenzelm@42793
    44
      res_inst_tac ctxt
wenzelm@42793
    45
        [(("act", 0), sact)] @{thm totalize_transientI} 2
wenzelm@42793
    46
      ORELSE res_inst_tac ctxt
wenzelm@42793
    47
        [(("act", 0), sact)] @{thm transientI} 2,
wenzelm@42793
    48
         (*simplify the command's domain*)
haftmann@45138
    49
      simp_tac (simpset_of ctxt addsimps @{thms Domain_def}) 3,
wenzelm@42793
    50
      constrains_tac ctxt 1,
wenzelm@42793
    51
      ALLGOALS (clarify_tac ctxt),
wenzelm@42793
    52
      ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
paulson@13796
    53
paulson@13786
    54
paulson@13786
    55
(*Composition equivalences, from Lift_prog*)
paulson@13786
    56
paulson@13786
    57
fun make_o_equivs th =
paulson@13786
    58
    [th,
wenzelm@24147
    59
     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
wenzelm@24147
    60
     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
paulson@13786
    61