src/HOL/UNITY/UNITY_tactics.ML
author haftmann
Thu, 13 Oct 2011 22:56:19 +0200
changeset 45138 ba618e9288b8
parent 42795 66fcc9882784
child 46752 e9e7209eb375
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/UNITY_tactics.ML
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     3
    Copyright   2003  University of Cambridge
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     4
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21669
diff changeset
     5
Specialized UNITY tactics.
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     6
*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     7
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
     8
(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21669
diff changeset
     9
val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
    10
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
    11
(*Combines a list of invariance THEOREMS into one.*)
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21669
diff changeset
    12
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
    13
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13798
diff changeset
    14
(*Proves "co" properties when the program is specified.  Any use of invariants
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13798
diff changeset
    15
  (from weak constrains) must have been done already.*)
42767
e6d920bea7a6 prefer Proof.context over old-style clasimpset;
wenzelm
parents: 37936
diff changeset
    16
fun constrains_tac ctxt i =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    17
  SELECT_GOAL
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    18
    (EVERY
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    19
     [REPEAT (Always_Int_tac 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    20
      (*reduce the fancy safety properties to "constrains"*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    21
      REPEAT (etac @{thm Always_ConstrainsI} 1
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    22
              ORELSE
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    23
              resolve_tac [@{thm StableI}, @{thm stableI},
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    24
                           @{thm constrains_imp_Constrains}] 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    25
      (*for safety, the totalize operator can be ignored*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    26
      simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    27
      rtac @{thm constrainsI} 1,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    28
      full_simp_tac (simpset_of ctxt) 1,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    29
      REPEAT (FIRSTGOAL (etac disjE)),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    30
      ALLGOALS (clarify_tac ctxt),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    31
      ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    32
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    33
(*proves "ensures/leadsTo" properties when the program is specified*)
42767
e6d920bea7a6 prefer Proof.context over old-style clasimpset;
wenzelm
parents: 37936
diff changeset
    34
fun ensures_tac ctxt sact =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    35
  SELECT_GOAL
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    36
    (EVERY
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    37
     [REPEAT (Always_Int_tac 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    38
      etac @{thm Always_LeadsTo_Basis} 1
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    39
          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    40
          REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    41
                            @{thm EnsuresI}, @{thm ensuresI}] 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    42
      (*now there are two subgoals: co & transient*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    43
      simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    44
      res_inst_tac ctxt
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    45
        [(("act", 0), sact)] @{thm totalize_transientI} 2
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    46
      ORELSE res_inst_tac ctxt
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    47
        [(("act", 0), sact)] @{thm transientI} 2,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    48
         (*simplify the command's domain*)
45138
haftmann
parents: 42795
diff changeset
    49
      simp_tac (simpset_of ctxt addsimps @{thms Domain_def}) 3,
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    50
      constrains_tac ctxt 1,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    51
      ALLGOALS (clarify_tac ctxt),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    52
      ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
13796
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 13792
diff changeset
    53
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    54
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    55
(*Composition equivalences, from Lift_prog*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    56
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    57
fun make_o_equivs th =
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    58
    [th,
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21669
diff changeset
    59
     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21669
diff changeset
    60
     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    61