src/HOL/UNITY/UNITY_tactics.ML
author nipkow
Fri, 27 Mar 2020 12:28:05 +0100
changeset 71593 71579bd59cd4
parent 60774 6c28d8ed2488
permissions -rw-r--r--
added lemma
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??*)
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 51717
diff changeset
     9
fun Always_Int_tac ctxt =
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
    10
  dresolve_tac ctxt @{thms Always_Int_I} THEN'
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
    11
  assume_tac ctxt THEN'
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
    12
  eresolve_tac ctxt @{thms Always_thin}
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
    13
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
    14
(*Combines a list of invariance THEOREMS into one.*)
24147
edc90be09ac1 misc cleanup of ML bindings (for multihreading);
wenzelm
parents: 21669
diff changeset
    15
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
    16
13812
91713a1915ee converting HOL/UNITY to use unconditional fairness
paulson
parents: 13798
diff changeset
    17
(*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
    18
  (from weak constrains) must have been done already.*)
42767
e6d920bea7a6 prefer Proof.context over old-style clasimpset;
wenzelm
parents: 37936
diff changeset
    19
fun constrains_tac ctxt i =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    20
  SELECT_GOAL
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    21
    (EVERY
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 51717
diff changeset
    22
     [REPEAT (Always_Int_tac ctxt 1),
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    23
      (*reduce the fancy safety properties to "constrains"*)
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
    24
      REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    25
              ORELSE
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58963
diff changeset
    26
              resolve_tac ctxt [@{thm StableI}, @{thm stableI},
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    27
                           @{thm constrains_imp_Constrains}] 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    28
      (*for safety, the totalize operator can be ignored*)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    29
      simp_tac (put_simpset HOL_ss ctxt
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    30
        addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
    31
      resolve_tac ctxt @{thms constrainsI} 1,
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    32
      full_simp_tac ctxt 1,
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
    33
      REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    34
      ALLGOALS (clarify_tac ctxt),
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    35
      ALLGOALS (asm_full_simp_tac ctxt)]) i;
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    36
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    37
(*proves "ensures/leadsTo" properties when the program is specified*)
42767
e6d920bea7a6 prefer Proof.context over old-style clasimpset;
wenzelm
parents: 37936
diff changeset
    38
fun ensures_tac ctxt sact =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    39
  SELECT_GOAL
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    40
    (EVERY
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 51717
diff changeset
    41
     [REPEAT (Always_Int_tac ctxt 1),
60754
02924903a6fd prefer tactics with explicit context;
wenzelm
parents: 59780
diff changeset
    42
      eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    43
          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
60774
6c28d8ed2488 proper context;
wenzelm
parents: 60754
diff changeset
    44
          REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    45
                            @{thm EnsuresI}, @{thm ensuresI}] 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    46
      (*now there are two subgoals: co & transient*)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    47
      simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
59763
56d2c357e6b5 tuned signature;
wenzelm
parents: 59755
diff changeset
    48
      Rule_Insts.res_inst_tac ctxt
59780
23b67731f4f0 support 'for' fixes in rule_tac etc.;
wenzelm
parents: 59763
diff changeset
    49
        [((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
59763
56d2c357e6b5 tuned signature;
wenzelm
parents: 59755
diff changeset
    50
      ORELSE Rule_Insts.res_inst_tac ctxt
59780
23b67731f4f0 support 'for' fixes in rule_tac etc.;
wenzelm
parents: 59763
diff changeset
    51
        [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    52
         (*simplify the command's domain*)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    53
      simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    54
      constrains_tac ctxt 1,
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42767
diff changeset
    55
      ALLGOALS (clarify_tac ctxt),
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    56
      ALLGOALS (asm_lr_simp_tac ctxt)]);
13796
19f50fa807ae converting more UNITY theories to new-style
paulson
parents: 13792
diff changeset
    57
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    58
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    59
(*Composition equivalences, from Lift_prog*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    60
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    61
fun make_o_equivs ctxt th =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    62
  [th,
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    63
   th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46752
diff changeset
    64
   th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    65