# HG changeset patch
# User nipkow
# Date 1251295999 -7200
# Node ID a1a85b0a26f76bf0f735d0d4669019522e9b0b9e
# Parent  5ca6f9a344c010ec7fc5bf7e13e33b8f0473a1fb
new interval lemma
CCS example for predicate compiler

diff -r 5ca6f9a344c0 -r a1a85b0a26f7 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/SetInterval.thy	Wed Aug 26 16:13:19 2009 +0200
@@ -242,6 +242,14 @@
 
 end
 
+lemma (in linorder) atLeastLessThan_subset_iff:
+  "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
+apply (auto simp:subset_eq Ball_def)
+apply(frule_tac x=a in spec)
+apply(erule_tac x=d in allE)
+apply (simp add: less_imp_le)
+done
+
 subsection {* Intervals of natural numbers *}
 
 subsubsection {* The Constant @{term lessThan} *}
diff -r 5ca6f9a344c0 -r a1a85b0a26f7 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Aug 26 16:13:19 2009 +0200
@@ -99,4 +99,33 @@
 values 20 "{(n, m). tranclp succ n m}"
 *)
 
+subsection{* CCS *}
+
+text{* This example formalizes finite CCS processes without communication or
+recursion. For simplicity, labels are natural numbers. *}
+
+datatype proc = nil | pre nat proc | or proc proc | par proc proc
+
+inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
+"step (pre n p) n p" |
+"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
+"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
+"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
+"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
+
+code_pred step .
+
+inductive steps where
+"steps p [] p" |
+"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
+
+code_pred steps .
+
+values 5
+ "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
+
+(* FIXME
+values 3 "{(a,q). step (par nil nil) a q}"
+*)
+
 end
\ No newline at end of file