src/HOL/IMP/Natural.ML
changeset 1973 8c94c9a5be10
parent 1958 6f20ecbd87cb
child 4089 96fba19bcbe2
equal deleted inserted replaced
1972:cc65911dceef 1973:8c94c9a5be10
     4     Copyright   1996 TUM
     4     Copyright   1996 TUM
     5 *)
     5 *)
     6 
     6 
     7 open Natural;
     7 open Natural;
     8 
     8 
       
     9 AddIs evalc.intrs;
       
    10 
     9 val evalc_elim_cases = map (evalc.mk_cases com.simps)
    11 val evalc_elim_cases = map (evalc.mk_cases com.simps)
    10    ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
    12    ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
    11     "<IF b THEN c1 ELSE c2, s> -c-> t"];
    13     "<IF b THEN c1 ELSE c2, s> -c-> t"];
    12 
    14 
    13 val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
    15 val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
    14 
    16 
    15 val evalc_cs = set_cs addSEs evalc_elim_cases
    17 AddSEs evalc_elim_cases;
    16                       addEs  [evalc_WHILE_case];
       
    17 
    18 
    18 (* evaluation of com is deterministic *)
    19 (* evaluation of com is deterministic *)
    19 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
    20 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
    20 by (etac evalc.induct 1);
    21 by (etac evalc.induct 1);
    21 by (thin_tac "<?c,s2> -c-> s1" 7);
    22 by (thin_tac "<?c,s2> -c-> s1" 7);
    22 by (ALLGOALS (deepen_tac evalc_cs 4));
    23 by (ALLGOALS (deepen_tac (!claset addEs [evalc_WHILE_case]) 4));
    23 qed_spec_mp "com_det";
    24 qed_spec_mp "com_det";