# HG changeset patch
# User fahad
# Date 1422530585 0
# Node ID 45274393f28ce6884a0e0488f727289cc0a5918b
# Parent 38cde0214ad52359e189c4bd277736f9111a78db
no changes
diff -r 38cde0214ad5 -r 45274393f28c thys/Chap03.thy
--- a/thys/Chap03.thy Thu Jan 29 09:05:40 2015 +0000
+++ b/thys/Chap03.thy Thu Jan 29 11:23:05 2015 +0000
@@ -1,8 +1,77 @@
-(* test *)
theory Chap03
imports Main
begin
+(* 2.5.6 Case Study: Boolean Expressions *)
+
+datatype boolex = Const bool | Var nat | Neg boolex
+| And boolex boolex
+
+primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
+"value2 (Const b) env = b" |
+"value2 (Var x) env = env x" |
+"value2 (Neg b) env = (\<not> value2 b env)" |
+"value2 (And b c) env = (value2 b env \<and> value2 c env)"
+
+value "Const true"
+value "Var (Suc(0))"
+value "value2 (Const False) (\<lambda>x. False)"
+value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)"
+value "value2 (Var 11) (\<lambda>x. True )"
+
+definition
+ "en1 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)"
+
+abbreviation
+ "en2 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)"
+
+value "value2 (And (Var 10) (Var 11)) en2"
+
+lemma "value2 (And (Var 10) (Var 11)) en2 = True"
+apply(simp)
+done
+
+datatype ifex =
+ CIF bool
+| VIF nat
+| IF ifex ifex ifex
+
+primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
+"valif (CIF b) env = b" |
+"valif (VIF x) env = env x" |
+"valif (IF b t e) env = (if valif b env then valif t env else valif e env)"
+
+abbreviation "vif1 \<equiv> valif (CIF False) (\<lambda>x. False)"
+abbreviation "vif2 \<equiv> valif (VIF 11) (\<lambda>x. False)"
+abbreviation "vif3 \<equiv> valif (VIF 13) (\<lambda>x. True)"
+
+value "valif (CIF False) (\<lambda>x. False)"
+value "valif (VIF 11) (\<lambda>x. True)"
+value "valif (IF (CIF False) (CIF True) (CIF True))"
+
+primrec bool2if :: "boolex \<Rightarrow> ifex" where
+"bool2if (Const b) = CIF b" |
+"bool2if (Var x) = VIF x" |
+"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)" |
+"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
+
+lemma "valif (bool2if b) env = value2 b env"
+apply(induct_tac b)
+apply(auto)
+done
+
+primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where
+"normif (CIF b) t e = IF (CIF b) t e" |
+"normif (VIF x) t e = IF (VIF x) t e" |
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
+
+primrec norm :: "ifex \<Rightarrow> ifex" where
+"norm (CIF b) = CIF b" |
+"norm (VIF x) = VIF x" |
+"norm (IF b t e) = normif b (norm t) (norm e)"
+
+(*************** CHAPTER-3 ********************************)
+
lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
apply simp
done
@@ -125,7 +194,9 @@
apply(simp add: abc3)
done
-(* added test *)
+find_theorems "_ \<and> _ "
+
+(* added anottest *)
lemma abc5: "add2 m n = m + n"
apply(induction n)
@@ -147,6 +218,8 @@
"value (Vex a) env = env a" |
"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
+value "value (Cex a) (\<lambda>x. True)"
+
datatype ('a,'v)instr =
Const 'v
| Load 'a
@@ -182,34 +255,41 @@
apply(simp split: instr.split)
done
-(* 2.5.6 Case Study: Boolean Expressions *)
-
-datatype boolex = Const bool | Var nat | Neg boolex
-| And boolex boolex
+(* 3.4 Advanced Datatypes *)
-primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
-"value2 (Const b) env = b" |
-"value2 (Var x) env = env x" |
-"value2 (Neg b) env = (\<not> value2 b env)" |
-"value2 (And b c) env = (value2 b env \<and> value2 c env)"
+datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp"
+ | Sum "'a aexp" "'a aexp"
+ | Diff "'a aexp" "'a aexp"
+ | Var 'a
+ | Num nat
+and 'a bexp = Less "'a aexp" "'a aexp"
+ | And "'a bexp" "'a bexp"
+ | Neg "'a bexp"
+
+(* Total Recursive Functions: Fun *)
+(* 3.5.1 Definition *)
-value "Const true"
-value "Var (Suc(0))"
-
-
+fun fib :: "nat \<Rightarrow> nat" where
+"fib 0 = 0" |
+"fib (Suc 0) = 1" |
+"fib (Suc(Suc x)) = fib x + fib (Suc x)"
-value "value2 (Const False) (\<lambda>x. False)"
-value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)"
+value "fib (Suc(Suc(Suc(Suc(Suc 0)))))"
+
+fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"sep a [] = []" |
+"sep a [x] = [x]" |
+"sep a (x#y#zs) = x # a # sep a (y#zs)"
-definition
- "en1 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)"
-
-abbreviation
- "en2 \<equiv> (\<lambda>x. if x = 10 | x = 11 then True else False)"
-
-value "value2 (And (Var 10) (Var 11)) en2"
+fun last :: "'a list \<Rightarrow> 'a" where
+"last [x] = x" |
+"last (_#y#zs) = last (y#zs)"
-lemma "value2 (And (Var 10) (Var 11)) en2 = True"
-apply(simp)
-done
+fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
+"sep1 _ xs = xs"
+fun swap12:: "'a list \<Rightarrow> 'a list" where
+"swap12 (x#y#zs) = y#x#zs" |
+"swap12 zs = zs"
+
diff -r 38cde0214ad5 -r 45274393f28c thys/Re1.thy
--- a/thys/Re1.thy Thu Jan 29 09:05:40 2015 +0000
+++ b/thys/Re1.thy Thu Jan 29 11:23:05 2015 +0000
@@ -42,6 +42,9 @@
| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
+value "L(CHAR c)"
+value "L(SEQ(CHAR c)(CHAR b))"
+
section {* Values *}
@@ -72,6 +75,9 @@
| "flat(Right v) = flat(v)"
| "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
+value "flat(Seq(Char c)(Char b))"
+value "flat(Right(Void))"
+
fun flats :: "val \<Rightarrow> string list"
where
"flats(Void) = [[]]"
@@ -80,6 +86,8 @@
| "flats(Right v) = flats(v)"
| "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
+value "flats(Seq(Char c)(Char b))"
+
lemma Prf_flat_L:
assumes "\<turnstile> v : r" shows "flat v \<in> L r"
using assms
@@ -100,7 +108,7 @@
apply(auto)
done
-definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
+definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
where
"s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"