src/ZF/IMP/Com.ML
author clasohm
Thu, 23 Mar 1995 15:39:13 +0100
changeset 971 f4815812665b
parent 511 b2be4790da7a
child 1420 04eabfa73d83
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/Com.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
511
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
     7
open Com;
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
     8
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
     9
val assign_type = prove_goalw Com.thy [assign_def]
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    10
	"!!n. [| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    11
    (fn _ => [ fast_tac (ZF_cs addIs [apply_type,lam_type,if_type]) 1 ]);
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    12
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    13
val type_cs = ZF_cs addSEs [make_elim(evala.dom_subset RS subsetD),
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    14
                            make_elim(evalb.dom_subset RS subsetD),
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    15
                            make_elim(evalc.dom_subset RS subsetD)];
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    16
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    17
(**********     type_intrs for evala     **********)
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    18
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    19
val evala_type_intrs = 
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    20
 map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    21
 ["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    22
  "!!a.<a,sigma> -a-> n ==> n:nat"];
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    23
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    24
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    25
(**********     type_intrs for evalb     **********)
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    26
511
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    27
val evalb_type_intrs = 
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    28
 map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    29
 ["!!b.<b,sigma> -b-> w ==> b:bexp","!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    30
  "!!b.<b,sigma> -b-> w ==> w:bool"];
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    31
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    32
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    33
(**********     type_intrs for evalb     **********)
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    34
511
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    35
val evalc_type_intrs = 
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    36
 map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    37
 ["!!c.<c,sigma> -c-> sigma' ==> c:com",
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    38
  "!!c.<c,sigma> -c-> sigma' ==> sigma:loc->nat",
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    39
  "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    40
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    41
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    42
val op_type_intrs = evala_type_intrs@evalb_type_intrs@evalc_type_intrs;
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    43
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    44
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    45
val aexp_elim_cases = 
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    46
   [
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    47
    evala.mk_cases aexp.con_defs "<N(n),sigma> -a-> i",
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    48
    evala.mk_cases aexp.con_defs "<X(x),sigma> -a-> i",
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    49
    evala.mk_cases aexp.con_defs "<Op1(f,e),sigma> -a-> i",
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    50
    evala.mk_cases aexp.con_defs "<Op2(f,a1,a2),sigma>  -a-> i"
b2be4790da7a re-organized using new theory sections
lcp
parents: 482
diff changeset
    51
   ];