diff -r 9ed5d8ad8fa0 -r faba4800b00b src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Wed Jun 01 19:50:59 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-(*  Title:      HOL/IMP/Expr.thy
-    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
-*)
-
-header "Expressions"
-
-theory Expr imports Main begin
-
-text {*
-  Arithmetic expressions and Boolean expressions.
-  Not used in the rest of the language, but included for completeness.
-*}
-
-subsection "Arithmetic expressions"
-typedecl loc
-
-type_synonym state = "loc => nat"
-
-datatype
-  aexp = N nat
-       | X loc
-       | Op1 "nat => nat" aexp
-       | Op2 "nat => nat => nat" aexp aexp
-
-subsection "Evaluation of arithmetic expressions"
-
-inductive
-  evala :: "[aexp*state,nat] => bool"  (infixl "-a->" 50)
-where
-  N:   "(N(n),s) -a-> n"
-| X:   "(X(x),s) -a-> s(x)"
-| Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
-| Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |]
-        ==> (Op2 f e0 e1,s) -a-> f n0 n1"
-
-lemmas [intro] = N X Op1 Op2
-
-
-subsection "Boolean expressions"
-
-datatype
-  bexp = true
-       | false
-       | ROp  "nat => nat => bool" aexp aexp
-       | noti bexp
-       | andi bexp bexp         (infixl "andi" 60)
-       | ori  bexp bexp         (infixl "ori" 60)
-
-subsection "Evaluation of boolean expressions"
-
-inductive
-  evalb :: "[bexp*state,bool] => bool"  (infixl "-b->" 50)
-  -- "avoid clash with ML constructors true, false"
-where
-  tru:   "(true,s) -b-> True"
-| fls:   "(false,s) -b-> False"
-| ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
-          ==> (ROp f a0 a1,s) -b-> f n0 n1"
-| noti:  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
-| andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
-          ==> (b0 andi b1,s) -b-> (w0 & w1)"
-| ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
-          ==> (b0 ori b1,s) -b-> (w0 | w1)"
-
-lemmas [intro] = tru fls ROp noti andi ori
-
-subsection "Denotational semantics of arithmetic and boolean expressions"
-
-primrec A :: "aexp => state => nat"
-where
-  "A(N(n)) = (%s. n)"
-| "A(X(x)) = (%s. s(x))"
-| "A(Op1 f a) = (%s. f(A a s))"
-| "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-
-primrec B :: "bexp => state => bool"
-where
-  "B(true) = (%s. True)"
-| "B(false) = (%s. False)"
-| "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-| "B(noti(b)) = (%s. ~(B b s))"
-| "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-| "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
-
-inductive_simps
-  evala_simps [simp]:
-  "(N(n),s) -a-> n'" 
-  "(X(x),sigma) -a-> i"
-  "(Op1 f e,sigma) -a-> i"
-  "(Op2 f a1 a2,sigma) -a-> i"
-  "((true,sigma) -b-> w)"
-  "((false,sigma) -b-> w)"
-  "((ROp f a0 a1,sigma) -b-> w)"
-  "((noti(b),sigma) -b-> w)"
-  "((b0 andi b1,sigma) -b-> w)"
-  "((b0 ori b1,sigma) -b-> w)"
-
-
-lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
-  by (induct a arbitrary: n) auto
-
-lemma bexp_iff:
-  "((b,s) -b-> w) = (B b s = w)"
-  by (induct b arbitrary: w) (auto simp add: aexp_iff)
-
-end