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