src/ZF/IMP/Evalb.ML
author clasohm
Thu, 23 Mar 1995 15:39:13 +0100
changeset 971 f4815812665b
parent 496 3fc829fa81d2
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/Evalb.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
structure Evalb = Inductive_Fun
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     8
 (
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
     9
  val thy = Evalb0.thy;
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    10
  val thy_name = "Evalb"
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    11
  val rec_doms = [("evalb","bexp * (loc -> nat) * bool")];
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    12
  val sintrs = 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    13
      [
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    14
	"[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1",
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    15
       	"[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0",
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    16
       	"[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    17
\	    ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> ",
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    18
       	"[| <b,sigma> -b-> w |] \
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    19
\	    ==> <noti(b),sigma> -b-> not(w)", 
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    20
       	"[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    21
\	    ==> <b0 andi b1,sigma> -b-> (w0 and w1)",
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    22
       	"[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    23
\	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    24
      ];
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    25
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    26
  val monos = [];
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    27
  val con_defs = [];
496
3fc829fa81d2 Inductive defs need no longer mention SigmaI/E2
lcp
parents: 482
diff changeset
    28
  val type_intrs = Bexp.intrs@[apply_funtype,and_type,or_type,
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    29
		   bool_1I,bool_0I,not_type];
496
3fc829fa81d2 Inductive defs need no longer mention SigmaI/E2
lcp
parents: 482
diff changeset
    30
  val type_elims = [make_elim(Evala.dom_subset RS subsetD) ];
482
3a4e092ba69c Initial revision
nipkow
parents:
diff changeset
    31
 );