src/ZF/IMP/Denotation.ML
author clasohm
Thu, 23 Mar 1995 15:39:13 +0100
changeset 971 f4815812665b
parent 511 b2be4790da7a
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
fixed bug: parent theory wasn't loaded if .thy file was completly read before (regardless of the .ML file)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     1
(*  Title: 	ZF/IMP/Denotation.ML
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     2
    ID:         $Id$
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     3
    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     4
    Copyright   1994 TUM
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     5
*)
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     6
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     7
open Denotation;
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     8
511
b2be4790da7a re-organized using new theory sections
lcp
parents: 500
diff changeset
     9
(**** Rewrite Rules for A,B,C ****)
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    10
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    11
val A_rewrite_rules =
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    12
     [A_nat_def,A_loc_def,A_op1_def,A_op2_def];
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    13
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    14
val B_rewrite_rules =
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    15
     [B_true_def,B_false_def,B_op_def,B_not_def,B_and_def,B_or_def]
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    16
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    17
val C_rewrite_rules = 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    18
     [C_skip_def,C_assign_def,C_comp_def,C_if_def,C_while_def]; 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    19
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    20
(**** Type_intr for A ****)
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    21
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    22
val A_type = prove_goal Denotation.thy
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    23
	"!!a.[|a:aexp; sigma:loc->nat|] ==> A(a,sigma):nat"
511
b2be4790da7a re-organized using new theory sections
lcp
parents: 500
diff changeset
    24
   (fn _ => [(etac aexp.induct 1),
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    25
             (rewrite_goals_tac A_rewrite_rules),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    26
             (ALLGOALS (fast_tac (ZF_cs addSIs [apply_type])))]);
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    27
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    28
(**** Type_intr for B ****)
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    29
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    30
val B_type = prove_goal Denotation.thy
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    31
	"!!b. [|b:bexp; sigma:loc->nat|] ==> B(b,sigma):bool"
511
b2be4790da7a re-organized using new theory sections
lcp
parents: 500
diff changeset
    32
   (fn _ => [(etac bexp.induct 1),
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    33
             (rewrite_goals_tac B_rewrite_rules),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    34
             (ALLGOALS (fast_tac (ZF_cs 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    35
                          addSIs [apply_type,A_type]@bool_typechecks)))]);
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    36
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    37
(**** C_subset ****)
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    38
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    39
val C_subset = prove_goal Denotation.thy 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    40
	"!!c. c:com ==> C(c) <= (loc->nat)*(loc->nat)"
511
b2be4790da7a re-organized using new theory sections
lcp
parents: 500
diff changeset
    41
   (fn _ => [(etac com.induct 1),
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    42
             (rewrite_tac C_rewrite_rules),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    43
             (ALLGOALS (fast_tac (comp_cs addDs [lfp_subset RS subsetD])))]);
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    44
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    45
(**** Type_elims for C ****)
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    46
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    47
val C_type = prove_goal Denotation.thy
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    48
	"[| <x,y>:C(c); c:com; 					\
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    49
\	     !!c. [| x:loc->nat; y:loc->nat |]  ==> R |]	\
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    50
\	  ==> R"
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    51
     (fn prems => [(cut_facts_tac prems 1),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    52
                   (fast_tac (ZF_cs addSIs prems 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    53
                                    addDs  [(C_subset RS subsetD)]) 1)]);
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    54
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    55
val C_type_fst = prove_goal Denotation.thy
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    56
	"[| x:C(c); c:com; 					\
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    57
\	     !!c. [| fst(x):loc->nat |]  ==> R |]	\
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    58
\	  ==> R"
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    59
     (fn prems => [(cut_facts_tac prems 1),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    60
                   (resolve_tac prems 1),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    61
                   (dtac (C_subset RS subsetD) 1),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    62
                   (atac 1),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    63
                   (etac SigmaE 1),
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    64
                   (asm_simp_tac ZF_ss 1)]);
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    65
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    66
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    67
(**** bnd_mono (nat->nat*nat->nat,Gamma(b,c) ****)
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    68
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    69
val Gamma_bnd_mono = prove_goalw Denotation.thy [bnd_mono_def,Gamma_def]
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    70
	"!!c. c:com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))"
500
0842a38074e7 some small simplifications
nipkow
parents: 482
diff changeset
    71
     (fn prems => [(best_tac (comp_cs addEs [C_type]) 1)]);
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    72
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    73
(**** End ***)