src/HOL/UNITY/UNITY_tactics.ML
author wenzelm
Thu May 12 18:18:06 2011 +0200 (2011-05-12)
changeset 42767 e6d920bea7a6
parent 37936 1e4c5015a72e
child 42793 88bee9f6eec7
permissions -rw-r--r--
prefer Proof.context over old-style clasimpset;
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@42767
    17
  let
wenzelm@42767
    18
    val cs = claset_of ctxt;
wenzelm@42767
    19
    val ss = simpset_of ctxt;
wenzelm@42767
    20
  in
paulson@13786
    21
   SELECT_GOAL
paulson@13786
    22
      (EVERY [REPEAT (Always_Int_tac 1),
paulson@13812
    23
              (*reduce the fancy safety properties to "constrains"*)
wenzelm@24147
    24
              REPEAT (etac @{thm Always_ConstrainsI} 1
wenzelm@24147
    25
                      ORELSE
wenzelm@24147
    26
                      resolve_tac [@{thm StableI}, @{thm stableI},
wenzelm@24147
    27
                                   @{thm constrains_imp_Constrains}] 1),
paulson@13812
    28
              (*for safety, the totalize operator can be ignored*)
wenzelm@24147
    29
              simp_tac (HOL_ss addsimps
wenzelm@24147
    30
                         [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
wenzelm@24147
    31
              rtac @{thm constrainsI} 1,
wenzelm@24147
    32
              full_simp_tac ss 1,
wenzelm@24147
    33
              REPEAT (FIRSTGOAL (etac disjE)),
wenzelm@24147
    34
              ALLGOALS (clarify_tac cs),
wenzelm@42767
    35
              ALLGOALS (asm_full_simp_tac ss)]) i
wenzelm@42767
    36
  end;
paulson@13786
    37
paulson@13786
    38
(*proves "ensures/leadsTo" properties when the program is specified*)
wenzelm@42767
    39
fun ensures_tac ctxt sact =
wenzelm@42767
    40
  let
wenzelm@42767
    41
    val cs = claset_of ctxt;
wenzelm@42767
    42
    val ss = simpset_of ctxt;
wenzelm@42767
    43
  in
paulson@13786
    44
    SELECT_GOAL
paulson@13786
    45
      (EVERY [REPEAT (Always_Int_tac 1),
wenzelm@24147
    46
              etac @{thm Always_LeadsTo_Basis} 1
wenzelm@24147
    47
                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
wenzelm@24147
    48
                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
wenzelm@24147
    49
                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
wenzelm@24147
    50
              (*now there are two subgoals: co & transient*)
wenzelm@24147
    51
              simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
wenzelm@27239
    52
              res_inst_tac (Simplifier.the_context ss)
wenzelm@27208
    53
                [(("act", 0), sact)] @{thm totalize_transientI} 2
wenzelm@27239
    54
              ORELSE res_inst_tac (Simplifier.the_context ss)
wenzelm@27208
    55
                [(("act", 0), sact)] @{thm transientI} 2,
paulson@13786
    56
                 (*simplify the command's domain*)
wenzelm@24147
    57
              simp_tac (ss addsimps [@{thm Domain_def}]) 3,
wenzelm@42767
    58
              constrains_tac ctxt 1,
wenzelm@24147
    59
              ALLGOALS (clarify_tac cs),
wenzelm@42767
    60
              ALLGOALS (asm_lr_simp_tac ss)])
wenzelm@42767
    61
  end;
paulson@13796
    62
paulson@13786
    63
paulson@13786
    64
(*Composition equivalences, from Lift_prog*)
paulson@13786
    65
paulson@13786
    66
fun make_o_equivs th =
paulson@13786
    67
    [th,
wenzelm@24147
    68
     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
wenzelm@24147
    69
     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
paulson@13786
    70
wenzelm@30610
    71
Simplifier.change_simpset (fn ss => ss
wenzelm@30610
    72
  addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
wenzelm@30610
    73
  addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));