new interval lemma
authornipkow
Wed Aug 26 16:13:19 2009 +0200 (2009-08-26)
changeset 32408a1a85b0a26f7
parent 32401 5ca6f9a344c0
child 32409 7e38dedf3f7d
new interval lemma
CCS example for predicate compiler
src/HOL/SetInterval.thy
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/SetInterval.thy	Wed Aug 26 10:48:45 2009 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Aug 26 16:13:19 2009 +0200
     1.3 @@ -242,6 +242,14 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma (in linorder) atLeastLessThan_subset_iff:
     1.8 +  "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
     1.9 +apply (auto simp:subset_eq Ball_def)
    1.10 +apply(frule_tac x=a in spec)
    1.11 +apply(erule_tac x=d in allE)
    1.12 +apply (simp add: less_imp_le)
    1.13 +done
    1.14 +
    1.15  subsection {* Intervals of natural numbers *}
    1.16  
    1.17  subsubsection {* The Constant @{term lessThan} *}
     2.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Aug 26 10:48:45 2009 +0200
     2.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Aug 26 16:13:19 2009 +0200
     2.3 @@ -99,4 +99,33 @@
     2.4  values 20 "{(n, m). tranclp succ n m}"
     2.5  *)
     2.6  
     2.7 +subsection{* CCS *}
     2.8 +
     2.9 +text{* This example formalizes finite CCS processes without communication or
    2.10 +recursion. For simplicity, labels are natural numbers. *}
    2.11 +
    2.12 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
    2.13 +
    2.14 +inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
    2.15 +"step (pre n p) n p" |
    2.16 +"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
    2.17 +"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
    2.18 +"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
    2.19 +"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
    2.20 +
    2.21 +code_pred step .
    2.22 +
    2.23 +inductive steps where
    2.24 +"steps p [] p" |
    2.25 +"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
    2.26 +
    2.27 +code_pred steps .
    2.28 +
    2.29 +values 5
    2.30 + "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
    2.31 +
    2.32 +(* FIXME
    2.33 +values 3 "{(a,q). step (par nil nil) a q}"
    2.34 +*)
    2.35 +
    2.36  end
    2.37 \ No newline at end of file