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