# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1412605481 -3600
# Node ID c11651bbebf59ac1ccd600ca4dccd79aed2dc850
# Parent  66c9c06c0f0e3f0d8d0d22e68aec1d355bba3f54
some small changes

diff -r 66c9c06c0f0e -r c11651bbebf5 thys/MyFirst.thy
--- a/thys/MyFirst.thy	Mon Oct 06 14:22:13 2014 +0100
+++ b/thys/MyFirst.thy	Mon Oct 06 15:24:41 2014 +0100
@@ -50,11 +50,31 @@
 
 value "add 2 3"
 
+
 (**commutative-associative**)
-lemma add_04: "add m (add n k) = add k (add m n)"
-apply(induct)
-apply(auto)
-oops
+lemma add_04: "add m (add n k) = add (add m n) k"
+apply(induct m)
+apply(simp_all)
+done
+
+lemma add_zero: "add n 0 = n"
+sorry
+
+lemma add_Suc: "add m (Suc n) = Suc (add m n)"
+sorry
+
+lemma add_comm: "add m n = add n m"
+apply(induct m)
+apply(simp add: add_zero)
+apply(simp add: add_Suc)
+done
+
+lemma add_odd: "add m (add n k) = add k (add m n)"
+apply(subst add_04)
+apply(subst (2) add_comm)
+apply(simp)
+done
+
 
 fun dub :: "nat \<Rightarrow> nat" where
 "dub 0 = 0" |
@@ -89,9 +109,54 @@
 value "trip 1"
 value "trip 2"
 
+fun sum :: "nat \<Rightarrow> nat" where
+  "sum 0 = 0"
+| "sum (Suc n) = (Suc n) + sum n"
+
+function sum1 :: "nat \<Rightarrow> nat" where
+  "sum1 0 = 0"
+| "n \<noteq> 0 \<Longrightarrow> sum1 n = n + sum1 (n - 1)"
+apply(auto)
+done
+
+termination sum1
+by (smt2 "termination" diff_less less_than_iff not_gr0 wf_less_than zero_neq_one)
+
+lemma "sum n = sum1 n"
+apply(induct n)
+apply(auto)
+done
+
+lemma "sum n = (\<Sum>i \<le> n. i)"
+apply(induct n)
+apply(simp_all)
+done
+
 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "mull 0 0 = 0" |
 "mull m 0 = 0" |
+"mull m 1 = m" | 
+(**"mull m (1::nat) = m" | **)
+(**"mull m (suc(0)) = m" | **)
+"mull m n = mull m (n-(1::nat))" 
+apply(pat_completeness)
+apply(auto)
+
+done
+
+  "mull 0 n = 0"
+| "mull (Suc m) n = add n (mull m n)" 
+
+lemma test: "mull m n = m * n"
+sorry
+
+fun poww :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "poww 0 n = 1"
+| "poww (Suc m) n = mull n (poww m n)" 
+
+
+"mull 0 0 = 0" |
+"mull m 0 = 0" |
 (**"mull m 1 = m" | **)
 (**"mull m (1::nat) = m" | **)
 (**"mull m (suc(0)) = m" | **)
@@ -104,8 +169,7 @@
 "count  "
 **)
 
-fun sum :: "nat \<Rightarrow> nat" where
-"sum n = 0 + \<dots> + n"
+
 (* prove n = n * (n + 1) div 2  *)
 
 
diff -r 66c9c06c0f0e -r c11651bbebf5 thys/MyFirst.thy~
--- a/thys/MyFirst.thy~	Mon Oct 06 14:22:13 2014 +0100
+++ b/thys/MyFirst.thy~	Mon Oct 06 15:24:41 2014 +0100
@@ -50,10 +50,23 @@
 
 value "add 2 3"
 
-lemma add_04: "add m (add n k) = add k (add m n)"
-apply(induct)
-apply(auto)
-oops
+(**commutative-associative**)
+lemma add_04: "add m (add n k) = add (add m n) k"
+apply(induct m)
+apply(simp_all)
+done
+
+lemma add_zero: "add n 0 = n"
+sorry
+
+lemma add_Suc: "add m (Suc n) = Suc (add m n)"
+sorry
+
+lemma add_comm: "add m n = add n m"
+apply(induct m)
+apply(simp add: add_zero)
+apply(simp add: add_Suc)
+done
 
 fun dub :: "nat \<Rightarrow> nat" where
 "dub 0 = 0" |
@@ -91,14 +104,22 @@
 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "mull 0 0 = 0" |
 "mull m 0 = 0" |
-"mull m 1 = m" |
-"mull m n = 0" 
+(**"mull m 1 = m" | **)
+(**"mull m (1::nat) = m" | **)
+(**"mull m (suc(0)) = m" | **)
+"mull m n = mull m (n-(1::nat))" 
 
+(**Define a function that counts the
+number of occurrences of an element in a list **)
 (**
 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
 "count  "
 **)
 
+fun sum :: "nat \<Rightarrow> nat" where
+"sum n = 0 + \<dots> + n"
+(* prove n = n * (n + 1) div 2  *)
+
 
 
 
@@ -108,3 +129,4 @@
 
 
 
+
diff -r 66c9c06c0f0e -r c11651bbebf5 thys/Re1.thy
--- a/thys/Re1.thy	Mon Oct 06 14:22:13 2014 +0100
+++ b/thys/Re1.thy	Mon Oct 06 15:24:41 2014 +0100
@@ -135,6 +135,10 @@
 where
   "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
 
+definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+where
+  "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')"
+
 
 (*
 lemma POSIX_SEQ:
@@ -192,8 +196,7 @@
 using assms
 unfolding POSIX2_def
 apply(auto)
-
-done
+oops
 
 lemma POSIX_ALT:
   assumes "POSIX (Left v1) (ALT r1 r2)"
@@ -210,6 +213,23 @@
 apply(simp_all)
 done
 
+lemma POSIX2_ALT:
+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
+  shows "POSIX2 v1 r1"
+using assms
+apply(simp add: POSIX2_def)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Left v'" in spec)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
+
 lemma POSIX_ALT1a:
   assumes "POSIX (Right v2) (ALT r1 r2)"
   shows "POSIX v2 r2"
@@ -225,6 +245,22 @@
 apply(simp_all)
 done
 
+lemma POSIX2_ALT1a:
+  assumes "POSIX2 (Right v2) (ALT r1 r2)"
+  shows "POSIX2 v2 r2"
+using assms
+unfolding POSIX2_def
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Right v'" in spec)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
 
 lemma POSIX_ALT1b:
   assumes "POSIX (Right v2) (ALT r1 r2)"
@@ -250,6 +286,23 @@
 apply(rule ValOrd.intros)
 by simp
 
+lemma POSIX2_ALT_I1:
+  assumes "POSIX2 v1 r1" 
+  shows "POSIX2 (Left v1) (ALT r1 r2)"
+using assms
+unfolding POSIX2_def
+apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd.intros)
+apply(auto)
+apply(rule ValOrd.intros)
+oops
+
 lemma POSIX_ALT_I2:
   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
   shows "POSIX (Right v2) (ALT r1 r2)"
@@ -325,6 +378,7 @@
 apply(induct r)
 apply(auto)[1]
 apply(simp add: POSIX2_def)
+oops
 
 lemma mkeps_POSIX:
   assumes "nullable r"
@@ -368,6 +422,45 @@
 by (simp add: ValOrd.intros(5))
 
 
+lemma mkeps_POSIX2:
+  assumes "nullable r"
+  shows "POSIX2 (mkeps r) r"
+using assms
+apply(induct r)
+apply(simp)
+apply(simp)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(simp)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(simp add: mkeps_nullable)
+apply(simp add: mkeps_nullable)
+apply(auto)[1]
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros(2))
+apply(simp)
+apply(simp only: nullable.simps)
+apply(erule disjE)
+apply(simp)
+thm POSIX2_ALT1a
+apply(rule POSIX2_ALT)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(simp add: mkeps_nullable)
+oops
+
+
 section {* Derivatives *}
 
 fun
@@ -561,11 +654,48 @@
 apply (metis POSIX_ALT_I1)
 (* maybe it is too early to instantiate this existential quantifier *)
 (* potentially this is the wrong POSIX value *)
-apply(rule_tac x = "Seq v va" in exI )
+apply(case_tac "r1 = NULL")
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply (metis L.simps(1) L.simps(4) Prf_flat_L mkeps_flat nullable.simps(1) nullable.simps(2) nullable_correctness seq_null(2))
+apply(case_tac "r1 = EMPTY")
+apply(rule_tac x = "Seq Void va" in exI )
 apply(simp (no_asm) add: POSIX_def)
 apply(auto)
 apply(erule Prf.cases)
 apply(simp_all)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule ValOrd.intros(2))
+apply(rule ValOrd.intros)
+apply(case_tac "\<exists>c. r1 = CHAR c")
+apply(auto)
+apply(rule_tac x = "Seq (Char c) va" in exI )
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+apply(rule ValOrd.intros(2))
+apply(rule ValOrd.intros)
+apply(case_tac "\<exists>r1a r1b. r1 = ALT r1a r1b")
+apply(auto)
+apply(rule_tac x = "Seq () va" in exI )
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+apply(rule ValOrd.intros(2))
+apply(rule ValOrd.intros)
+
 apply(case_tac "v \<succ>r1a v1")
 apply (metis ValOrd.intros(2))
 apply(simp add: POSIX_def)
diff -r 66c9c06c0f0e -r c11651bbebf5 thys/Re1.thy~
--- a/thys/Re1.thy~	Mon Oct 06 14:22:13 2014 +0100
+++ b/thys/Re1.thy~	Mon Oct 06 15:24:41 2014 +0100
@@ -135,6 +135,10 @@
 where
   "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
 
+definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+where
+  "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v \<ge> flat v') \<longrightarrow> v \<succ>r v')"
+
 
 (*
 lemma POSIX_SEQ:
@@ -168,6 +172,33 @@
 done
 *)
 
+
+
+
+lemma POSIX_ALT2:
+  assumes "POSIX (Left v1) (ALT r1 r2)"
+  shows "POSIX v1 r1"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(drule_tac x="Left v'" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
+lemma POSIX2_ALT:
+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
+  shows "POSIX2 v1 r1"
+using assms
+unfolding POSIX2_def
+apply(auto)
+
+done
+
 lemma POSIX_ALT:
   assumes "POSIX (Left v1) (ALT r1 r2)"
   shows "POSIX v1 r1"
@@ -183,6 +214,23 @@
 apply(simp_all)
 done
 
+lemma POSIX2_ALT:
+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
+  shows "POSIX2 v1 r1"
+using assms
+apply(simp add: POSIX2_def)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Left v'" in spec)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
+
 lemma POSIX_ALT1a:
   assumes "POSIX (Right v2) (ALT r1 r2)"
   shows "POSIX v2 r2"
@@ -198,6 +246,22 @@
 apply(simp_all)
 done
 
+lemma POSIX2_ALT1a:
+  assumes "POSIX2 (Right v2) (ALT r1 r2)"
+  shows "POSIX2 v2 r2"
+using assms
+unfolding POSIX2_def
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Right v'" in spec)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
 
 lemma POSIX_ALT1b:
   assumes "POSIX (Right v2) (ALT r1 r2)"
@@ -223,6 +287,25 @@
 apply(rule ValOrd.intros)
 by simp
 
+lemma POSIX2_ALT_I1:
+  assumes "POSIX2 v1 r1" 
+  shows "POSIX2 (Left v1) (ALT r1 r2)"
+using assms
+unfolding POSIX2_def
+apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd.intros)
+apply(auto)
+apply(rule ValOrd.intros)
+
+
+by simp
+
 lemma POSIX_ALT_I2:
   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
   shows "POSIX (Right v2) (ALT r1 r2)"
@@ -291,6 +374,14 @@
   value.
 *}
 
+lemma mkeps_POSIX2:
+  assumes "nullable r"
+  shows "POSIX2 (mkeps r) r"
+using assms
+apply(induct r)
+apply(auto)[1]
+apply(simp add: POSIX2_def)
+
 lemma mkeps_POSIX:
   assumes "nullable r"
   shows "POSIX (mkeps r) r"
@@ -333,6 +424,51 @@
 by (simp add: ValOrd.intros(5))
 
 
+lemma mkeps_POSIX2:
+  assumes "nullable r"
+  shows "POSIX2 (mkeps r) r"
+using assms
+apply(induct r)
+apply(simp)
+apply(simp)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(simp)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(simp add: mkeps_nullable)
+apply(simp add: mkeps_nullable)
+apply(auto)[1]
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros(2))
+apply(simp)
+apply(simp only: nullable.simps)
+apply(erule disjE)
+apply(simp)
+thm POSIX2_ALT1a
+apply(rule POSIX2_ALT)
+apply(simp add: POSIX2_def)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(simp add: mkeps_nullable)
+apply(auto)[1]
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(simp)
+apply(rule ValOrd.intros)
+
+
 section {* Derivatives *}
 
 fun