src/HOL/UNITY/UNITY_tactics.ML
author paulson
Fri Jan 24 18:13:59 2003 +0100 (2003-01-24)
changeset 13786 ab8f39f48a6f
child 13790 8d7e9fce8c50
permissions -rw-r--r--
More conversion of UNITY to Isar new-style theories
paulson@13786
     1
(*  Title:      HOL/UNITY/UNITY_tactics.ML
paulson@13786
     2
    ID:         $Id$
paulson@13786
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13786
     4
    Copyright   2003  University of Cambridge
paulson@13786
     5
paulson@13786
     6
Specialized UNITY tactics, and ML bindings of theorems
paulson@13786
     7
*)
paulson@13786
     8
paulson@13786
     9
paulson@13786
    10
(*Lift_prog*)
paulson@13786
    11
val sub_def = thm "sub_def";
paulson@13786
    12
val lift_map_def = thm "lift_map_def";
paulson@13786
    13
val drop_map_def = thm "drop_map_def";
paulson@13786
    14
val insert_map_inverse = thm "insert_map_inverse";
paulson@13786
    15
val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
paulson@13786
    16
val insert_map_inject1 = thm "insert_map_inject1";
paulson@13786
    17
val insert_map_inject2 = thm "insert_map_inject2";
paulson@13786
    18
val insert_map_inject = thm "insert_map_inject";
paulson@13786
    19
val insert_map_inject = thm "insert_map_inject";
paulson@13786
    20
val lift_map_eq_iff = thm "lift_map_eq_iff";
paulson@13786
    21
val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
paulson@13786
    22
val inj_lift_map = thm "inj_lift_map";
paulson@13786
    23
val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
paulson@13786
    24
val drop_map_inject = thm "drop_map_inject";
paulson@13786
    25
val surj_lift_map = thm "surj_lift_map";
paulson@13786
    26
val bij_lift_map = thm "bij_lift_map";
paulson@13786
    27
val inv_lift_map_eq = thm "inv_lift_map_eq";
paulson@13786
    28
val inv_drop_map_eq = thm "inv_drop_map_eq";
paulson@13786
    29
val bij_drop_map = thm "bij_drop_map";
paulson@13786
    30
val sub_apply = thm "sub_apply";
paulson@13786
    31
val lift_set_empty = thm "lift_set_empty";
paulson@13786
    32
val lift_set_iff = thm "lift_set_iff";
paulson@13786
    33
val lift_set_iff2 = thm "lift_set_iff2";
paulson@13786
    34
val lift_set_mono = thm "lift_set_mono";
paulson@13786
    35
val lift_set_Un_distrib = thm "lift_set_Un_distrib";
paulson@13786
    36
val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
paulson@13786
    37
val bij_lift = thm "bij_lift";
paulson@13786
    38
val lift_SKIP = thm "lift_SKIP";
paulson@13786
    39
val lift_Join = thm "lift_Join";
paulson@13786
    40
val lift_JN = thm "lift_JN";
paulson@13786
    41
val lift_constrains = thm "lift_constrains";
paulson@13786
    42
val lift_stable = thm "lift_stable";
paulson@13786
    43
val lift_invariant = thm "lift_invariant";
paulson@13786
    44
val lift_Constrains = thm "lift_Constrains";
paulson@13786
    45
val lift_Stable = thm "lift_Stable";
paulson@13786
    46
val lift_Always = thm "lift_Always";
paulson@13786
    47
val lift_transient = thm "lift_transient";
paulson@13786
    48
val lift_ensures = thm "lift_ensures";
paulson@13786
    49
val lift_leadsTo = thm "lift_leadsTo";
paulson@13786
    50
val lift_LeadsTo = thm "lift_LeadsTo";
paulson@13786
    51
val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
paulson@13786
    52
val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
paulson@13786
    53
val lift_preserves_snd_I = thm "lift_preserves_snd_I";
paulson@13786
    54
val delete_map_eqE = thm "delete_map_eqE";
paulson@13786
    55
val delete_map_eqE = thm "delete_map_eqE";
paulson@13786
    56
val delete_map_neq_apply = thm "delete_map_neq_apply";
paulson@13786
    57
val vimage_o_fst_eq = thm "vimage_o_fst_eq";
paulson@13786
    58
val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
paulson@13786
    59
val mem_lift_act_iff = thm "mem_lift_act_iff";
paulson@13786
    60
val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
paulson@13786
    61
val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
paulson@13786
    62
val insert_map_upd_same = thm "insert_map_upd_same";
paulson@13786
    63
val insert_map_upd = thm "insert_map_upd";
paulson@13786
    64
val insert_map_eq_diff = thm "insert_map_eq_diff";
paulson@13786
    65
val lift_map_eq_diff = thm "lift_map_eq_diff";
paulson@13786
    66
val lift_transient_eq_disj = thm "lift_transient_eq_disj";
paulson@13786
    67
val lift_map_image_Times = thm "lift_map_image_Times";
paulson@13786
    68
val lift_preserves_eq = thm "lift_preserves_eq";
paulson@13786
    69
val lift_preserves_sub = thm "lift_preserves_sub";
paulson@13786
    70
val o_equiv_assoc = thm "o_equiv_assoc";
paulson@13786
    71
val o_equiv_apply = thm "o_equiv_apply";
paulson@13786
    72
val fst_o_lift_map = thm "fst_o_lift_map";
paulson@13786
    73
val snd_o_lift_map = thm "snd_o_lift_map";
paulson@13786
    74
val extend_act_extend_act = thm "extend_act_extend_act";
paulson@13786
    75
val project_act_project_act = thm "project_act_project_act";
paulson@13786
    76
val project_act_extend_act = thm "project_act_extend_act";
paulson@13786
    77
val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
paulson@13786
    78
val UNION_OK_lift_I = thm "UNION_OK_lift_I";
paulson@13786
    79
val OK_lift_I = thm "OK_lift_I";
paulson@13786
    80
val Allowed_lift = thm "Allowed_lift";
paulson@13786
    81
val lift_image_preserves = thm "lift_image_preserves";
paulson@13786
    82
paulson@13786
    83
paulson@13786
    84
(*PPROD*)
paulson@13786
    85
val Init_PLam = thm "Init_PLam";
paulson@13786
    86
val PLam_empty = thm "PLam_empty";
paulson@13786
    87
val PLam_SKIP = thm "PLam_SKIP";
paulson@13786
    88
val PLam_insert = thm "PLam_insert";
paulson@13786
    89
val PLam_component_iff = thm "PLam_component_iff";
paulson@13786
    90
val component_PLam = thm "component_PLam";
paulson@13786
    91
val PLam_constrains = thm "PLam_constrains";
paulson@13786
    92
val PLam_stable = thm "PLam_stable";
paulson@13786
    93
val PLam_transient = thm "PLam_transient";
paulson@13786
    94
val PLam_ensures = thm "PLam_ensures";
paulson@13786
    95
val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
paulson@13786
    96
val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
paulson@13786
    97
val PLam_preserves_fst = thm "PLam_preserves_fst";
paulson@13786
    98
val PLam_preserves_snd = thm "PLam_preserves_snd";
paulson@13786
    99
val guarantees_PLam_I = thm "guarantees_PLam_I";
paulson@13786
   100
val Allowed_PLam = thm "Allowed_PLam";
paulson@13786
   101
val PLam_preserves = thm "PLam_preserves";
paulson@13786
   102
paulson@13786
   103
paulson@13786
   104
(*proves "co" properties when the program is specified*)
paulson@13786
   105
fun gen_constrains_tac(cs,ss) i = 
paulson@13786
   106
   SELECT_GOAL
paulson@13786
   107
      (EVERY [REPEAT (Always_Int_tac 1),
paulson@13786
   108
	      REPEAT (etac Always_ConstrainsI 1
paulson@13786
   109
		      ORELSE
paulson@13786
   110
		      resolve_tac [StableI, stableI,
paulson@13786
   111
				   constrains_imp_Constrains] 1),
paulson@13786
   112
	      rtac constrainsI 1,
paulson@13786
   113
	      full_simp_tac ss 1,
paulson@13786
   114
	      REPEAT (FIRSTGOAL (etac disjE)),
paulson@13786
   115
	      ALLGOALS (clarify_tac cs),
paulson@13786
   116
	      ALLGOALS (asm_lr_simp_tac ss)]) i;
paulson@13786
   117
paulson@13786
   118
(*proves "ensures/leadsTo" properties when the program is specified*)
paulson@13786
   119
fun gen_ensures_tac(cs,ss) sact = 
paulson@13786
   120
    SELECT_GOAL
paulson@13786
   121
      (EVERY [REPEAT (Always_Int_tac 1),
paulson@13786
   122
	      etac Always_LeadsTo_Basis 1 
paulson@13786
   123
	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
paulson@13786
   124
		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
paulson@13786
   125
				    EnsuresI, ensuresI] 1),
paulson@13786
   126
	      (*now there are two subgoals: co & transient*)
paulson@13786
   127
	      simp_tac ss 2,
paulson@13786
   128
	      res_inst_tac [("act", sact)] transientI 2,
paulson@13786
   129
                 (*simplify the command's domain*)
paulson@13786
   130
	      simp_tac (ss addsimps [Domain_def]) 3,
paulson@13786
   131
	      gen_constrains_tac (cs,ss) 1,
paulson@13786
   132
	      ALLGOALS (clarify_tac cs),
paulson@13786
   133
	      ALLGOALS (asm_lr_simp_tac ss)]);
paulson@13786
   134
paulson@13786
   135
paulson@13786
   136
(*Composition equivalences, from Lift_prog*)
paulson@13786
   137
paulson@13786
   138
fun make_o_equivs th =
paulson@13786
   139
    [th,
paulson@13786
   140
     th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
paulson@13786
   141
     th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
paulson@13786
   142
paulson@13786
   143
Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
paulson@13786
   144
paulson@13786
   145
Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);