src/HOL/TLA/Init.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 6255 db63752140c7
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
wenzelm@6255
     1
local
wenzelm@6255
     2
  fun prover s = prove_goal Init.thy s 
wenzelm@6255
     3
                    (K [force_tac (claset(), simpset() addsimps [Init_def]) 1])
wenzelm@6255
     4
in
wenzelm@6255
     5
  val const_simps = map (int_rewrite o prover)
wenzelm@6255
     6
      [ "|- (Init #True) = #True",
wenzelm@6255
     7
        "|- (Init #False) = #False"]
wenzelm@6255
     8
  val Init_simps = map (int_rewrite o prover)
wenzelm@6255
     9
      [ "|- (Init ~F) = (~ Init F)",
wenzelm@6255
    10
        "|- (Init (P --> Q)) = (Init P --> Init Q)",
wenzelm@6255
    11
        "|- (Init (P & Q)) = (Init P & Init Q)",
wenzelm@6255
    12
        "|- (Init (P | Q)) = (Init P | Init Q)",
wenzelm@6255
    13
        "|- (Init (P = Q)) = ((Init P) = (Init Q))",
wenzelm@6255
    14
        "|- (Init (!x. F x)) = (!x. (Init F x))",
wenzelm@6255
    15
        "|- (Init (? x. F x)) = (? x. (Init F x))",
wenzelm@6255
    16
        "|- (Init (?! x. F x)) = (?! x. (Init F x))"
wenzelm@6255
    17
      ]
wenzelm@6255
    18
end;
wenzelm@6255
    19
wenzelm@6255
    20
Addsimps const_simps;
wenzelm@6255
    21
wenzelm@6255
    22
Goal "|- (Init $P) = (Init P)";
wenzelm@6255
    23
by (force_tac (claset(), simpset() addsimps [Init_def,fw_act_def,fw_stp_def]) 1);
wenzelm@6255
    24
qed "Init_stp_act";
wenzelm@6255
    25
val Init_simps = (int_rewrite Init_stp_act)::Init_simps;
wenzelm@6255
    26
bind_thm("Init_stp_act_rev", symmetric(int_rewrite Init_stp_act));
wenzelm@6255
    27
wenzelm@6255
    28
Goal "|- (Init F) = F";
wenzelm@6255
    29
by (force_tac (claset(), simpset() addsimps [Init_def,fw_temp_def]) 1);
wenzelm@6255
    30
qed "Init_temp";
wenzelm@6255
    31
val Init_simps = (int_rewrite Init_temp)::Init_simps;
wenzelm@6255
    32
wenzelm@6255
    33
(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
wenzelm@6255
    34
Goalw [Init_def,fw_stp_def] "(sigma |= Init P) = P (st1 sigma)";
wenzelm@6255
    35
by (rtac refl 1);
wenzelm@6255
    36
qed "Init_stp";
wenzelm@6255
    37
wenzelm@6255
    38
Goalw [Init_def,fw_act_def] "(sigma |= Init A) = A (st1 sigma, st2 sigma)";
wenzelm@6255
    39
by (rtac refl 1);
wenzelm@6255
    40
qed "Init_act";
wenzelm@6255
    41
wenzelm@6255
    42
val Init_defs = [Init_stp, Init_act, int_use Init_temp];
wenzelm@6255
    43