src/HOL/TLA/Stfun.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 12607 16b63730cfbb
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 Stfun.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@6255
     4
    Copyright:   1998 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
Lemmas and tactics for states and state functions.
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@12607
     9
Goalw [basevars_def] "!!vs. basevars vs ==> EX u. vs u = c";
wenzelm@12607
    10
by (res_inst_tac [("b","c"),("f","vs")] rangeE 1);
wenzelm@12607
    11
by Auto_tac;
wenzelm@12607
    12
qed "basevars";
wenzelm@12607
    13
wenzelm@12607
    14
Goal "!!x y. basevars (x,y) ==> basevars x";
wenzelm@12607
    15
by (simp_tac (simpset() addsimps [basevars_def]) 1);
wenzelm@12607
    16
by (rtac equalityI 1);
wenzelm@12607
    17
 by (rtac subset_UNIV 1);
wenzelm@12607
    18
by (rtac subsetI 1);
wenzelm@12607
    19
by (dres_inst_tac [("c", "(xa, arbitrary)")] basevars 1);
wenzelm@12607
    20
by Auto_tac;
wenzelm@12607
    21
qed "base_pair1";
wenzelm@12607
    22
wenzelm@12607
    23
Goal "!!x y. basevars (x,y) ==> basevars y";
wenzelm@12607
    24
by (simp_tac (simpset() addsimps [basevars_def]) 1);
wenzelm@12607
    25
by (rtac equalityI 1);
wenzelm@12607
    26
 by (rtac subset_UNIV 1);
wenzelm@12607
    27
by (rtac subsetI 1);
wenzelm@12607
    28
by (dres_inst_tac [("c", "(arbitrary, xa)")] basevars 1);
wenzelm@12607
    29
by Auto_tac;
wenzelm@12607
    30
qed "base_pair2";
wenzelm@12607
    31
wenzelm@12607
    32
Goal "!!x y. basevars (x,y) ==> basevars x & basevars y";
wenzelm@12607
    33
by (rtac conjI 1);
wenzelm@12607
    34
by (etac base_pair1 1);
wenzelm@12607
    35
by (etac base_pair2 1);
wenzelm@12607
    36
qed "base_pair";
wenzelm@12607
    37
wenzelm@12607
    38
(* Since the unit type has just one value, any state function can be
wenzelm@12607
    39
   regarded as "base". The following axiom can sometimes be useful
wenzelm@12607
    40
   because it gives a trivial solution for "basevars" premises.
wenzelm@12607
    41
*)
wenzelm@12607
    42
Goalw [basevars_def] "basevars (v::unit stfun)";
wenzelm@12607
    43
by Auto_tac;
wenzelm@12607
    44
qed "unit_base";
wenzelm@12607
    45
wenzelm@6255
    46
(*  [| basevars v; !!x. v x = c ==> Q |] ==> Q  *)
wenzelm@6255
    47
bind_thm("baseE", (standard (basevars RS exE)));
wenzelm@3807
    48
wenzelm@6255
    49
(* -------------------------------------------------------------------------------
wenzelm@6255
    50
   The following shows that there should not be duplicates in a "stvars" tuple:
wenzelm@3807
    51
wenzelm@6255
    52
Goal "!!v. basevars (v::bool stfun, v) ==> False";
wenzelm@6255
    53
by (etac baseE 1);
wenzelm@6255
    54
by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1); 
wenzelm@6255
    55
by (atac 2);
wenzelm@6255
    56
by (Asm_full_simp_tac 1);
wenzelm@3807
    57
wenzelm@6255
    58
------------------------------------------------------------------------------- *)