splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
authorbulwahn
Thu Sep 23 14:50:18 2010 +0200 (2010-09-23)
changeset 396558ad7fe9d6f0b
parent 39654 1207e39f0c7f
child 39656 f398f66969ce
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
src/HOL/IsaMakefile
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Predicate_Compile_Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 23 14:50:17 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Sep 23 14:50:18 2010 +0200
     1.3 @@ -1345,9 +1345,10 @@
     1.4  
     1.5  $(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL			\
     1.6    Predicate_Compile_Examples/ROOT.ML					\
     1.7 -  Predicate_Compile_Examples/Predicate_Compile_Examples.thy		\
     1.8 +  Predicate_Compile_Examples/Predicate_Compile_Tests.thy		\
     1.9    Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
    1.10    Predicate_Compile_Examples/Code_Prolog_Examples.thy 			\
    1.11 +  Predicate_Compile_Examples/Examples.thy				\
    1.12    Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 		\
    1.13    Predicate_Compile_Examples/Hotel_Example.thy 				\
    1.14    Predicate_Compile_Examples/IMP_1.thy 					\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Thu Sep 23 14:50:18 2010 +0200
     2.3 @@ -0,0 +1,326 @@
     2.4 +theory Examples
     2.5 +imports Main Predicate_Compile_Alternative_Defs
     2.6 +begin
     2.7 +
     2.8 +section {* Formal Languages *}
     2.9 +
    2.10 +subsection {* General Context Free Grammars *}
    2.11 +
    2.12 +text {* a contribution by Aditi Barthwal *}
    2.13 +
    2.14 +datatype ('nts,'ts) symbol = NTS 'nts
    2.15 +                            | TS 'ts
    2.16 +
    2.17 +                            
    2.18 +datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
    2.19 +
    2.20 +types ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
    2.21 +
    2.22 +fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set"
    2.23 +where
    2.24 +  "rules (r, s) = r"
    2.25 +
    2.26 +definition derives 
    2.27 +where
    2.28 +"derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. 
    2.29 +                         (s1 @ [NTS lhs] @ s2 = lsl) \<and>
    2.30 +                         (s1 @ rhs @ s2) = rsl \<and>
    2.31 +                         (rule lhs rhs) \<in> fst g }"
    2.32 +
    2.33 +abbreviation "example_grammar == 
    2.34 +({ rule ''S'' [NTS ''A'', NTS ''B''],
    2.35 +   rule ''S'' [TS ''a''],
    2.36 +  rule ''A'' [TS ''b'']}, ''S'')"
    2.37 +
    2.38 +
    2.39 +code_pred [inductify, skip_proof] derives .
    2.40 +
    2.41 +thm derives.equation
    2.42 +
    2.43 +definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
    2.44 +
    2.45 +code_pred (modes: o \<Rightarrow> bool) [inductify] test .
    2.46 +thm test.equation
    2.47 +
    2.48 +values "{rhs. test rhs}"
    2.49 +
    2.50 +declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def]
    2.51 +
    2.52 +code_pred [inductify] rtrancl .
    2.53 +
    2.54 +definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^*  }"
    2.55 +
    2.56 +code_pred [inductify, skip_proof] test2 .
    2.57 +
    2.58 +values "{rhs. test2 rhs}"
    2.59 +
    2.60 +subsection {* Some concrete Context Free Grammars *}
    2.61 +
    2.62 +datatype alphabet = a | b
    2.63 +
    2.64 +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
    2.65 +  "[] \<in> S\<^isub>1"
    2.66 +| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    2.67 +| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
    2.68 +| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
    2.69 +| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    2.70 +| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
    2.71 +
    2.72 +code_pred [inductify] S\<^isub>1p .
    2.73 +code_pred [random_dseq inductify] S\<^isub>1p .
    2.74 +thm S\<^isub>1p.equation
    2.75 +thm S\<^isub>1p.random_dseq_equation
    2.76 +
    2.77 +values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
    2.78 +
    2.79 +inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
    2.80 +  "[] \<in> S\<^isub>2"
    2.81 +| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
    2.82 +| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
    2.83 +| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
    2.84 +| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
    2.85 +| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
    2.86 +
    2.87 +code_pred [random_dseq inductify] S\<^isub>2p .
    2.88 +thm S\<^isub>2p.random_dseq_equation
    2.89 +thm A\<^isub>2p.random_dseq_equation
    2.90 +thm B\<^isub>2p.random_dseq_equation
    2.91 +
    2.92 +values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
    2.93 +
    2.94 +inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
    2.95 +  "[] \<in> S\<^isub>3"
    2.96 +| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
    2.97 +| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
    2.98 +| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
    2.99 +| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   2.100 +| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   2.101 +
   2.102 +code_pred [inductify, skip_proof] S\<^isub>3p .
   2.103 +thm S\<^isub>3p.equation
   2.104 +
   2.105 +values 10 "{x. S\<^isub>3p x}"
   2.106 +
   2.107 +inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   2.108 +  "[] \<in> S\<^isub>4"
   2.109 +| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   2.110 +| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   2.111 +| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   2.112 +| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   2.113 +| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   2.114 +| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   2.115 +
   2.116 +code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
   2.117 +
   2.118 +hide_const a b
   2.119 +
   2.120 +section {* Semantics of programming languages *}
   2.121 +
   2.122 +subsection {* IMP *}
   2.123 +
   2.124 +types
   2.125 +  var = nat
   2.126 +  state = "int list"
   2.127 +
   2.128 +datatype com =
   2.129 +  Skip |
   2.130 +  Ass var "state => int" |
   2.131 +  Seq com com |
   2.132 +  IF "state => bool" com com |
   2.133 +  While "state => bool" com
   2.134 +
   2.135 +inductive exec :: "com => state => state => bool" where
   2.136 +"exec Skip s s" |
   2.137 +"exec (Ass x e) s (s[x := e(s)])" |
   2.138 +"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
   2.139 +"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
   2.140 +"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
   2.141 +"~b s ==> exec (While b c) s s" |
   2.142 +"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
   2.143 +
   2.144 +code_pred exec .
   2.145 +
   2.146 +values "{t. exec
   2.147 + (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
   2.148 + [3,5] t}"
   2.149 +
   2.150 +subsection {* Lambda *}
   2.151 +
   2.152 +datatype type =
   2.153 +    Atom nat
   2.154 +  | Fun type type    (infixr "\<Rightarrow>" 200)
   2.155 +
   2.156 +datatype dB =
   2.157 +    Var nat
   2.158 +  | App dB dB (infixl "\<degree>" 200)
   2.159 +  | Abs type dB
   2.160 +
   2.161 +primrec
   2.162 +  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
   2.163 +where
   2.164 +  "[]\<langle>i\<rangle> = None"
   2.165 +| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
   2.166 +
   2.167 +inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
   2.168 +where
   2.169 +  "nth_el' (x # xs) 0 x"
   2.170 +| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
   2.171 +
   2.172 +inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   2.173 +  where
   2.174 +    Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
   2.175 +  | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
   2.176 +  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
   2.177 +
   2.178 +primrec
   2.179 +  lift :: "[dB, nat] => dB"
   2.180 +where
   2.181 +    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
   2.182 +  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
   2.183 +  | "lift (Abs T s) k = Abs T (lift s (k + 1))"
   2.184 +
   2.185 +primrec
   2.186 +  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
   2.187 +where
   2.188 +    subst_Var: "(Var i)[s/k] =
   2.189 +      (if k < i then Var (i - 1) else if i = k then s else Var i)"
   2.190 +  | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
   2.191 +  | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
   2.192 +
   2.193 +inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
   2.194 +  where
   2.195 +    beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
   2.196 +  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
   2.197 +  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
   2.198 +  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
   2.199 +
   2.200 +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
   2.201 +thm typing.equation
   2.202 +
   2.203 +code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .
   2.204 +thm beta.equation
   2.205 +
   2.206 +values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
   2.207 +
   2.208 +definition "reduce t = Predicate.the (reduce' t)"
   2.209 +
   2.210 +value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
   2.211 +
   2.212 +code_pred [dseq] typing .
   2.213 +code_pred [random_dseq] typing .
   2.214 +
   2.215 +values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
   2.216 +
   2.217 +subsection {* A minimal example of yet another semantics *}
   2.218 +
   2.219 +text {* thanks to Elke Salecker *}
   2.220 +
   2.221 +types
   2.222 +  vname = nat
   2.223 +  vvalue = int
   2.224 +  var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
   2.225 +
   2.226 +datatype ir_expr = 
   2.227 +  IrConst vvalue
   2.228 +| ObjAddr vname
   2.229 +| Add ir_expr ir_expr
   2.230 +
   2.231 +datatype val =
   2.232 +  IntVal  vvalue
   2.233 +
   2.234 +record  configuration =
   2.235 +  Env :: var_assign
   2.236 +
   2.237 +inductive eval_var ::
   2.238 +  "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
   2.239 +where
   2.240 +  irconst: "eval_var (IrConst i) conf (IntVal i)"
   2.241 +| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
   2.242 +| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
   2.243 +
   2.244 +
   2.245 +code_pred eval_var .
   2.246 +thm eval_var.equation
   2.247 +
   2.248 +values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
   2.249 +
   2.250 +subsection {* Another semantics *}
   2.251 +
   2.252 +types
   2.253 +  name = nat --"For simplicity in examples"
   2.254 +  state' = "name \<Rightarrow> nat"
   2.255 +
   2.256 +datatype aexp = N nat | V name | Plus aexp aexp
   2.257 +
   2.258 +fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where
   2.259 +"aval (N n) _ = n" |
   2.260 +"aval (V x) st = st x" |
   2.261 +"aval (Plus e\<^isub>1 e\<^isub>2) st = aval e\<^isub>1 st + aval e\<^isub>2 st"
   2.262 +
   2.263 +datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
   2.264 +
   2.265 +primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where
   2.266 +"bval (B b) _ = b" |
   2.267 +"bval (Not b) st = (\<not> bval b st)" |
   2.268 +"bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |
   2.269 +"bval (Less a\<^isub>1 a\<^isub>2) st = (aval a\<^isub>1 st < aval a\<^isub>2 st)"
   2.270 +
   2.271 +datatype
   2.272 +  com' = SKIP 
   2.273 +      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
   2.274 +      | Semi   com'  com'          ("_; _"  [60, 61] 60)
   2.275 +      | If     bexp com' com'     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
   2.276 +      | While  bexp com'         ("WHILE _ DO _"  [0, 61] 61)
   2.277 +
   2.278 +inductive
   2.279 +  big_step :: "com' * state' \<Rightarrow> state' \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
   2.280 +where
   2.281 +  Skip:    "(SKIP,s) \<Rightarrow> s"
   2.282 +| Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)"
   2.283 +
   2.284 +| Semi:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3  \<Longrightarrow> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3"
   2.285 +
   2.286 +| IfTrue:  "bval b s  \<Longrightarrow>  (c\<^isub>1,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"
   2.287 +| IfFalse: "\<not>bval b s  \<Longrightarrow>  (c\<^isub>2,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"
   2.288 +
   2.289 +| WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s"
   2.290 +| WhileTrue:  "bval b s\<^isub>1  \<Longrightarrow>  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3
   2.291 +               \<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
   2.292 +
   2.293 +code_pred big_step .
   2.294 +
   2.295 +thm big_step.equation
   2.296 +
   2.297 +subsection {* CCS *}
   2.298 +
   2.299 +text{* This example formalizes finite CCS processes without communication or
   2.300 +recursion. For simplicity, labels are natural numbers. *}
   2.301 +
   2.302 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
   2.303 +
   2.304 +inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
   2.305 +"step (pre n p) n p" |
   2.306 +"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
   2.307 +"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
   2.308 +"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
   2.309 +"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
   2.310 +
   2.311 +code_pred step .
   2.312 +
   2.313 +inductive steps where
   2.314 +"steps p [] p" |
   2.315 +"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
   2.316 +
   2.317 +code_pred steps .
   2.318 +
   2.319 +values 3 
   2.320 + "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   2.321 +
   2.322 +values 5
   2.323 + "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   2.324 +
   2.325 +values 3 "{(a,q). step (par nil nil) a q}"
   2.326 +
   2.327 +
   2.328 +end
   2.329 +
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 23 14:50:17 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,1785 +0,0 @@
     3.4 -theory Predicate_Compile_Examples
     3.5 -imports Predicate_Compile_Alternative_Defs
     3.6 -begin
     3.7 -
     3.8 -subsection {* Basic predicates *}
     3.9 -
    3.10 -inductive False' :: "bool"
    3.11 -
    3.12 -code_pred (expected_modes: bool) False' .
    3.13 -code_pred [dseq] False' .
    3.14 -code_pred [random_dseq] False' .
    3.15 -
    3.16 -values [expected "{}" pred] "{x. False'}"
    3.17 -values [expected "{}" dseq 1] "{x. False'}"
    3.18 -values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
    3.19 -
    3.20 -value "False'"
    3.21 -
    3.22 -inductive True' :: "bool"
    3.23 -where
    3.24 -  "True ==> True'"
    3.25 -
    3.26 -code_pred True' .
    3.27 -code_pred [dseq] True' .
    3.28 -code_pred [random_dseq] True' .
    3.29 -
    3.30 -thm True'.equation
    3.31 -thm True'.dseq_equation
    3.32 -thm True'.random_dseq_equation
    3.33 -values [expected "{()}" ]"{x. True'}"
    3.34 -values [expected "{}" dseq 0] "{x. True'}"
    3.35 -values [expected "{()}" dseq 1] "{x. True'}"
    3.36 -values [expected "{()}" dseq 2] "{x. True'}"
    3.37 -values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
    3.38 -values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
    3.39 -values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
    3.40 -values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
    3.41 -
    3.42 -inductive EmptySet :: "'a \<Rightarrow> bool"
    3.43 -
    3.44 -code_pred (expected_modes: o => bool, i => bool) EmptySet .
    3.45 -
    3.46 -definition EmptySet' :: "'a \<Rightarrow> bool"
    3.47 -where "EmptySet' = {}"
    3.48 -
    3.49 -code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
    3.50 -
    3.51 -inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
    3.52 -
    3.53 -code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
    3.54 -
    3.55 -inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.56 -for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.57 -
    3.58 -code_pred
    3.59 -  (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
    3.60 -         (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
    3.61 -         (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
    3.62 -         (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
    3.63 -         (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
    3.64 -         (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
    3.65 -         (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
    3.66 -         (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
    3.67 -  EmptyClosure .
    3.68 -
    3.69 -thm EmptyClosure.equation
    3.70 -
    3.71 -(* TODO: inductive package is broken!
    3.72 -inductive False'' :: "bool"
    3.73 -where
    3.74 -  "False \<Longrightarrow> False''"
    3.75 -
    3.76 -code_pred (expected_modes: []) False'' .
    3.77 -
    3.78 -inductive EmptySet'' :: "'a \<Rightarrow> bool"
    3.79 -where
    3.80 -  "False \<Longrightarrow> EmptySet'' x"
    3.81 -
    3.82 -code_pred (expected_modes: [1]) EmptySet'' .
    3.83 -code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
    3.84 -*)
    3.85 -
    3.86 -consts a' :: 'a
    3.87 -
    3.88 -inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.89 -where
    3.90 -"Fact a' a'"
    3.91 -
    3.92 -code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
    3.93 -
    3.94 -inductive zerozero :: "nat * nat => bool"
    3.95 -where
    3.96 -  "zerozero (0, 0)"
    3.97 -
    3.98 -code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
    3.99 -code_pred [dseq] zerozero .
   3.100 -code_pred [random_dseq] zerozero .
   3.101 -
   3.102 -thm zerozero.equation
   3.103 -thm zerozero.dseq_equation
   3.104 -thm zerozero.random_dseq_equation
   3.105 -
   3.106 -text {* We expect the user to expand the tuples in the values command.
   3.107 -The following values command is not supported. *}
   3.108 -(*values "{x. zerozero x}" *)
   3.109 -text {* Instead, the user must type *}
   3.110 -values "{(x, y). zerozero (x, y)}"
   3.111 -
   3.112 -values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
   3.113 -values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
   3.114 -values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
   3.115 -values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
   3.116 -values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
   3.117 -
   3.118 -inductive nested_tuples :: "((int * int) * int * int) => bool"
   3.119 -where
   3.120 -  "nested_tuples ((0, 1), 2, 3)"
   3.121 -
   3.122 -code_pred nested_tuples .
   3.123 -
   3.124 -inductive JamesBond :: "nat => int => code_numeral => bool"
   3.125 -where
   3.126 -  "JamesBond 0 0 7"
   3.127 -
   3.128 -code_pred JamesBond .
   3.129 -
   3.130 -values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
   3.131 -values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
   3.132 -values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
   3.133 -values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
   3.134 -values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
   3.135 -values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
   3.136 -
   3.137 -values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
   3.138 -values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
   3.139 -values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
   3.140 -
   3.141 -
   3.142 -subsection {* Alternative Rules *}
   3.143 -
   3.144 -datatype char = C | D | E | F | G | H
   3.145 -
   3.146 -inductive is_C_or_D
   3.147 -where
   3.148 -  "(x = C) \<or> (x = D) ==> is_C_or_D x"
   3.149 -
   3.150 -code_pred (expected_modes: i => bool) is_C_or_D .
   3.151 -thm is_C_or_D.equation
   3.152 -
   3.153 -inductive is_D_or_E
   3.154 -where
   3.155 -  "(x = D) \<or> (x = E) ==> is_D_or_E x"
   3.156 -
   3.157 -lemma [code_pred_intro]:
   3.158 -  "is_D_or_E D"
   3.159 -by (auto intro: is_D_or_E.intros)
   3.160 -
   3.161 -lemma [code_pred_intro]:
   3.162 -  "is_D_or_E E"
   3.163 -by (auto intro: is_D_or_E.intros)
   3.164 -
   3.165 -code_pred (expected_modes: o => bool, i => bool) is_D_or_E
   3.166 -proof -
   3.167 -  case is_D_or_E
   3.168 -  from is_D_or_E.prems show thesis
   3.169 -  proof
   3.170 -    fix xa
   3.171 -    assume x: "x = xa"
   3.172 -    assume "xa = D \<or> xa = E"
   3.173 -    from this show thesis
   3.174 -    proof
   3.175 -      assume "xa = D" from this x is_D_or_E(2) show thesis by simp
   3.176 -    next
   3.177 -      assume "xa = E" from this x is_D_or_E(3) show thesis by simp
   3.178 -    qed
   3.179 -  qed
   3.180 -qed
   3.181 -
   3.182 -thm is_D_or_E.equation
   3.183 -
   3.184 -inductive is_F_or_G
   3.185 -where
   3.186 -  "x = F \<or> x = G ==> is_F_or_G x"
   3.187 -
   3.188 -lemma [code_pred_intro]:
   3.189 -  "is_F_or_G F"
   3.190 -by (auto intro: is_F_or_G.intros)
   3.191 -
   3.192 -lemma [code_pred_intro]:
   3.193 -  "is_F_or_G G"
   3.194 -by (auto intro: is_F_or_G.intros)
   3.195 -
   3.196 -inductive is_FGH
   3.197 -where
   3.198 -  "is_F_or_G x ==> is_FGH x"
   3.199 -| "is_FGH H"
   3.200 -
   3.201 -text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
   3.202 -
   3.203 -code_pred (expected_modes: o => bool, i => bool) is_FGH
   3.204 -proof -
   3.205 -  case is_F_or_G
   3.206 -  from this(1) show thesis
   3.207 -  proof
   3.208 -    fix xa
   3.209 -    assume x: "x = xa"
   3.210 -    assume "xa = F \<or> xa = G"
   3.211 -    from this show thesis
   3.212 -    proof
   3.213 -      assume "xa = F"
   3.214 -      from this x is_F_or_G(2) show thesis by simp
   3.215 -    next
   3.216 -      assume "xa = G"
   3.217 -      from this x is_F_or_G(3) show thesis by simp
   3.218 -    qed
   3.219 -  qed
   3.220 -qed
   3.221 -
   3.222 -subsection {* Named alternative rules *}
   3.223 -
   3.224 -inductive appending
   3.225 -where
   3.226 -  nil: "appending [] ys ys"
   3.227 -| cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
   3.228 -
   3.229 -lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
   3.230 -by (auto intro: appending.intros)
   3.231 -
   3.232 -lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
   3.233 -by (auto intro: appending.intros)
   3.234 -
   3.235 -text {* With code_pred_intro, we can give fact names to the alternative rules,
   3.236 -  which are used for the code_pred command. *}
   3.237 -
   3.238 -declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
   3.239 - 
   3.240 -code_pred appending
   3.241 -proof -
   3.242 -  case appending
   3.243 -  from prems show thesis
   3.244 -  proof(cases)
   3.245 -    case nil
   3.246 -    from alt_nil nil show thesis by auto
   3.247 -  next
   3.248 -    case cons
   3.249 -    from alt_cons cons show thesis by fastsimp
   3.250 -  qed
   3.251 -qed
   3.252 -
   3.253 -
   3.254 -inductive ya_even and ya_odd :: "nat => bool"
   3.255 -where
   3.256 -  even_zero: "ya_even 0"
   3.257 -| odd_plus1: "ya_even x ==> ya_odd (x + 1)"
   3.258 -| even_plus1: "ya_odd x ==> ya_even (x + 1)"
   3.259 -
   3.260 -
   3.261 -declare even_zero[code_pred_intro even_0]
   3.262 -
   3.263 -lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
   3.264 -by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   3.265 -
   3.266 -lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
   3.267 -by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   3.268 -
   3.269 -code_pred ya_even
   3.270 -proof -
   3.271 -  case ya_even
   3.272 -  from ya_even.prems show thesis
   3.273 -  proof (cases)
   3.274 -    case even_zero
   3.275 -    from even_zero even_0 show thesis by simp
   3.276 -  next
   3.277 -    case even_plus1
   3.278 -    from even_plus1 even_Suc show thesis by simp
   3.279 -  qed
   3.280 -next
   3.281 -  case ya_odd
   3.282 -  from ya_odd.prems show thesis
   3.283 -  proof (cases)
   3.284 -    case odd_plus1
   3.285 -    from odd_plus1 odd_Suc show thesis by simp
   3.286 -  qed
   3.287 -qed
   3.288 -
   3.289 -subsection {* Preprocessor Inlining  *}
   3.290 -
   3.291 -definition "equals == (op =)"
   3.292 - 
   3.293 -inductive zerozero' :: "nat * nat => bool" where
   3.294 -  "equals (x, y) (0, 0) ==> zerozero' (x, y)"
   3.295 -
   3.296 -code_pred (expected_modes: i => bool) zerozero' .
   3.297 -
   3.298 -lemma zerozero'_eq: "zerozero' x == zerozero x"
   3.299 -proof -
   3.300 -  have "zerozero' = zerozero"
   3.301 -    apply (auto simp add: mem_def)
   3.302 -    apply (cases rule: zerozero'.cases)
   3.303 -    apply (auto simp add: equals_def intro: zerozero.intros)
   3.304 -    apply (cases rule: zerozero.cases)
   3.305 -    apply (auto simp add: equals_def intro: zerozero'.intros)
   3.306 -    done
   3.307 -  from this show "zerozero' x == zerozero x" by auto
   3.308 -qed
   3.309 -
   3.310 -declare zerozero'_eq [code_pred_inline]
   3.311 -
   3.312 -definition "zerozero'' x == zerozero' x"
   3.313 -
   3.314 -text {* if preprocessing fails, zerozero'' will not have all modes. *}
   3.315 -
   3.316 -code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
   3.317 -
   3.318 -subsection {* Sets and Numerals *}
   3.319 -
   3.320 -definition
   3.321 -  "one_or_two = {Suc 0, (Suc (Suc 0))}"
   3.322 -
   3.323 -code_pred [inductify] one_or_two .
   3.324 -
   3.325 -code_pred [dseq] one_or_two .
   3.326 -code_pred [random_dseq] one_or_two .
   3.327 -thm one_or_two.dseq_equation
   3.328 -values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
   3.329 -values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
   3.330 -
   3.331 -inductive one_or_two' :: "nat => bool"
   3.332 -where
   3.333 -  "one_or_two' 1"
   3.334 -| "one_or_two' 2"
   3.335 -
   3.336 -code_pred one_or_two' .
   3.337 -thm one_or_two'.equation
   3.338 -
   3.339 -values "{x. one_or_two' x}"
   3.340 -
   3.341 -definition one_or_two'':
   3.342 -  "one_or_two'' == {1, (2::nat)}"
   3.343 -
   3.344 -code_pred [inductify] one_or_two'' .
   3.345 -thm one_or_two''.equation
   3.346 -
   3.347 -values "{x. one_or_two'' x}"
   3.348 -
   3.349 -subsection {* even predicate *}
   3.350 -
   3.351 -inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
   3.352 -    "even 0"
   3.353 -  | "even n \<Longrightarrow> odd (Suc n)"
   3.354 -  | "odd n \<Longrightarrow> even (Suc n)"
   3.355 -
   3.356 -code_pred (expected_modes: i => bool, o => bool) even .
   3.357 -code_pred [dseq] even .
   3.358 -code_pred [random_dseq] even .
   3.359 -
   3.360 -thm odd.equation
   3.361 -thm even.equation
   3.362 -thm odd.dseq_equation
   3.363 -thm even.dseq_equation
   3.364 -thm odd.random_dseq_equation
   3.365 -thm even.random_dseq_equation
   3.366 -
   3.367 -values "{x. even 2}"
   3.368 -values "{x. odd 2}"
   3.369 -values 10 "{n. even n}"
   3.370 -values 10 "{n. odd n}"
   3.371 -values [expected "{}" dseq 2] "{x. even 6}"
   3.372 -values [expected "{}" dseq 6] "{x. even 6}"
   3.373 -values [expected "{()}" dseq 7] "{x. even 6}"
   3.374 -values [dseq 2] "{x. odd 7}"
   3.375 -values [dseq 6] "{x. odd 7}"
   3.376 -values [dseq 7] "{x. odd 7}"
   3.377 -values [expected "{()}" dseq 8] "{x. odd 7}"
   3.378 -
   3.379 -values [expected "{}" dseq 0] 8 "{x. even x}"
   3.380 -values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
   3.381 -values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
   3.382 -values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
   3.383 -values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
   3.384 -
   3.385 -values [random_dseq 1, 1, 0] 8 "{x. even x}"
   3.386 -values [random_dseq 1, 1, 1] 8 "{x. even x}"
   3.387 -values [random_dseq 1, 1, 2] 8 "{x. even x}"
   3.388 -values [random_dseq 1, 1, 3] 8 "{x. even x}"
   3.389 -values [random_dseq 1, 1, 6] 8 "{x. even x}"
   3.390 -
   3.391 -values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
   3.392 -values [random_dseq 1, 1, 8] "{x. odd 7}"
   3.393 -values [random_dseq 1, 1, 9] "{x. odd 7}"
   3.394 -
   3.395 -definition odd' where "odd' x == \<not> even x"
   3.396 -
   3.397 -code_pred (expected_modes: i => bool) [inductify] odd' .
   3.398 -code_pred [dseq inductify] odd' .
   3.399 -code_pred [random_dseq inductify] odd' .
   3.400 -
   3.401 -values [expected "{}" dseq 2] "{x. odd' 7}"
   3.402 -values [expected "{()}" dseq 9] "{x. odd' 7}"
   3.403 -values [expected "{}" dseq 2] "{x. odd' 8}"
   3.404 -values [expected "{}" dseq 10] "{x. odd' 8}"
   3.405 -
   3.406 -
   3.407 -inductive is_even :: "nat \<Rightarrow> bool"
   3.408 -where
   3.409 -  "n mod 2 = 0 \<Longrightarrow> is_even n"
   3.410 -
   3.411 -code_pred (expected_modes: i => bool) is_even .
   3.412 -
   3.413 -subsection {* append predicate *}
   3.414 -
   3.415 -inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   3.416 -    "append [] xs xs"
   3.417 -  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
   3.418 -
   3.419 -code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
   3.420 -  i => o => i => bool as suffix, i => i => i => bool) append .
   3.421 -code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix,
   3.422 -  i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
   3.423 -
   3.424 -code_pred [dseq] append .
   3.425 -code_pred [random_dseq] append .
   3.426 -
   3.427 -thm append.equation
   3.428 -thm append.dseq_equation
   3.429 -thm append.random_dseq_equation
   3.430 -
   3.431 -values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
   3.432 -values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
   3.433 -values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
   3.434 -
   3.435 -values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   3.436 -values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   3.437 -values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   3.438 -values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   3.439 -values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   3.440 -values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   3.441 -values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   3.442 -values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   3.443 -values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   3.444 -values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   3.445 -
   3.446 -value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
   3.447 -value [code] "Predicate.the (slice ([]::int list))"
   3.448 -
   3.449 -
   3.450 -text {* tricky case with alternative rules *}
   3.451 -
   3.452 -inductive append2
   3.453 -where
   3.454 -  "append2 [] xs xs"
   3.455 -| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
   3.456 -
   3.457 -lemma append2_Nil: "append2 [] (xs::'b list) xs"
   3.458 -  by (simp add: append2.intros(1))
   3.459 -
   3.460 -lemmas [code_pred_intro] = append2_Nil append2.intros(2)
   3.461 -
   3.462 -code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
   3.463 -  i => o => i => bool, i => i => i => bool) append2
   3.464 -proof -
   3.465 -  case append2
   3.466 -  from append2(1) show thesis
   3.467 -  proof
   3.468 -    fix xs
   3.469 -    assume "xa = []" "xb = xs" "xc = xs"
   3.470 -    from this append2(2) show thesis by simp
   3.471 -  next
   3.472 -    fix xs ys zs x
   3.473 -    assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
   3.474 -    from this append2(3) show thesis by fastsimp
   3.475 -  qed
   3.476 -qed
   3.477 -
   3.478 -inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   3.479 -where
   3.480 -  "tupled_append ([], xs, xs)"
   3.481 -| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
   3.482 -
   3.483 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   3.484 -  i * o * i => bool, i * i * i => bool) tupled_append .
   3.485 -
   3.486 -code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool,
   3.487 -  i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
   3.488 -
   3.489 -code_pred [random_dseq] tupled_append .
   3.490 -thm tupled_append.equation
   3.491 -
   3.492 -values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
   3.493 -
   3.494 -inductive tupled_append'
   3.495 -where
   3.496 -"tupled_append' ([], xs, xs)"
   3.497 -| "[| ys = fst (xa, y); x # zs = snd (xa, y);
   3.498 - tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
   3.499 -
   3.500 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   3.501 -  i * o * i => bool, i * i * i => bool) tupled_append' .
   3.502 -thm tupled_append'.equation
   3.503 -
   3.504 -inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   3.505 -where
   3.506 -  "tupled_append'' ([], xs, xs)"
   3.507 -| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
   3.508 -
   3.509 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   3.510 -  i * o * i => bool, i * i * i => bool) tupled_append'' .
   3.511 -thm tupled_append''.equation
   3.512 -
   3.513 -inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   3.514 -where
   3.515 -  "tupled_append''' ([], xs, xs)"
   3.516 -| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
   3.517 -
   3.518 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   3.519 -  i * o * i => bool, i * i * i => bool) tupled_append''' .
   3.520 -thm tupled_append'''.equation
   3.521 -
   3.522 -subsection {* map_ofP predicate *}
   3.523 -
   3.524 -inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   3.525 -where
   3.526 -  "map_ofP ((a, b)#xs) a b"
   3.527 -| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
   3.528 -
   3.529 -code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
   3.530 -thm map_ofP.equation
   3.531 -
   3.532 -subsection {* filter predicate *}
   3.533 -
   3.534 -inductive filter1
   3.535 -for P
   3.536 -where
   3.537 -  "filter1 P [] []"
   3.538 -| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
   3.539 -| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
   3.540 -
   3.541 -code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
   3.542 -code_pred [dseq] filter1 .
   3.543 -code_pred [random_dseq] filter1 .
   3.544 -
   3.545 -thm filter1.equation
   3.546 -
   3.547 -values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   3.548 -values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   3.549 -values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   3.550 -
   3.551 -inductive filter2
   3.552 -where
   3.553 -  "filter2 P [] []"
   3.554 -| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
   3.555 -| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
   3.556 -
   3.557 -code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
   3.558 -code_pred [dseq] filter2 .
   3.559 -code_pred [random_dseq] filter2 .
   3.560 -
   3.561 -thm filter2.equation
   3.562 -thm filter2.random_dseq_equation
   3.563 -
   3.564 -inductive filter3
   3.565 -for P
   3.566 -where
   3.567 -  "List.filter P xs = ys ==> filter3 P xs ys"
   3.568 -
   3.569 -code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 .
   3.570 -
   3.571 -code_pred filter3 .
   3.572 -thm filter3.equation
   3.573 -
   3.574 -(*
   3.575 -inductive filter4
   3.576 -where
   3.577 -  "List.filter P xs = ys ==> filter4 P xs ys"
   3.578 -
   3.579 -code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
   3.580 -(*code_pred [depth_limited] filter4 .*)
   3.581 -(*code_pred [random] filter4 .*)
   3.582 -*)
   3.583 -subsection {* reverse predicate *}
   3.584 -
   3.585 -inductive rev where
   3.586 -    "rev [] []"
   3.587 -  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   3.588 -
   3.589 -code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
   3.590 -
   3.591 -thm rev.equation
   3.592 -
   3.593 -values "{xs. rev [0, 1, 2, 3::nat] xs}"
   3.594 -
   3.595 -inductive tupled_rev where
   3.596 -  "tupled_rev ([], [])"
   3.597 -| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
   3.598 -
   3.599 -code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
   3.600 -thm tupled_rev.equation
   3.601 -
   3.602 -subsection {* partition predicate *}
   3.603 -
   3.604 -inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   3.605 -  for f where
   3.606 -    "partition f [] [] []"
   3.607 -  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   3.608 -  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
   3.609 -
   3.610 -code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
   3.611 -  (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
   3.612 -  partition .
   3.613 -code_pred [dseq] partition .
   3.614 -code_pred [random_dseq] partition .
   3.615 -
   3.616 -values 10 "{(ys, zs). partition is_even
   3.617 -  [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
   3.618 -values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
   3.619 -values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
   3.620 -
   3.621 -inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
   3.622 -  for f where
   3.623 -   "tupled_partition f ([], [], [])"
   3.624 -  | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
   3.625 -  | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
   3.626 -
   3.627 -code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
   3.628 -  (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
   3.629 -
   3.630 -thm tupled_partition.equation
   3.631 -
   3.632 -lemma [code_pred_intro]:
   3.633 -  "r a b \<Longrightarrow> tranclp r a b"
   3.634 -  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   3.635 -  by auto
   3.636 -
   3.637 -subsection {* transitive predicate *}
   3.638 -
   3.639 -text {* Also look at the tabled transitive closure in the Library *}
   3.640 -
   3.641 -code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
   3.642 -  (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
   3.643 -  (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
   3.644 -proof -
   3.645 -  case tranclp
   3.646 -  from this converse_tranclpE[OF this(1)] show thesis by metis
   3.647 -qed
   3.648 -
   3.649 -
   3.650 -code_pred [dseq] tranclp .
   3.651 -code_pred [random_dseq] tranclp .
   3.652 -thm tranclp.equation
   3.653 -thm tranclp.random_dseq_equation
   3.654 -
   3.655 -inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
   3.656 -where
   3.657 -  "rtrancl' x x r"
   3.658 -| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
   3.659 -
   3.660 -code_pred [random_dseq] rtrancl' .
   3.661 -
   3.662 -thm rtrancl'.random_dseq_equation
   3.663 -
   3.664 -inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  
   3.665 -where
   3.666 -  "rtrancl'' (x, x, r)"
   3.667 -| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
   3.668 -
   3.669 -code_pred rtrancl'' .
   3.670 -
   3.671 -inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
   3.672 -where
   3.673 -  "rtrancl''' (x, (x, x), r)"
   3.674 -| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
   3.675 -
   3.676 -code_pred rtrancl''' .
   3.677 -
   3.678 -
   3.679 -inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   3.680 -    "succ 0 1"
   3.681 -  | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
   3.682 -
   3.683 -code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
   3.684 -code_pred [random_dseq] succ .
   3.685 -thm succ.equation
   3.686 -thm succ.random_dseq_equation
   3.687 -
   3.688 -values 10 "{(m, n). succ n m}"
   3.689 -values "{m. succ 0 m}"
   3.690 -values "{m. succ m 0}"
   3.691 -
   3.692 -text {* values command needs mode annotation of the parameter succ
   3.693 -to disambiguate which mode is to be chosen. *} 
   3.694 -
   3.695 -values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
   3.696 -values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
   3.697 -values 20 "{(n, m). tranclp succ n m}"
   3.698 -
   3.699 -inductive example_graph :: "int => int => bool"
   3.700 -where
   3.701 -  "example_graph 0 1"
   3.702 -| "example_graph 1 2"
   3.703 -| "example_graph 1 3"
   3.704 -| "example_graph 4 7"
   3.705 -| "example_graph 4 5"
   3.706 -| "example_graph 5 6"
   3.707 -| "example_graph 7 6"
   3.708 -| "example_graph 7 8"
   3.709 - 
   3.710 -inductive not_reachable_in_example_graph :: "int => int => bool"
   3.711 -where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
   3.712 -
   3.713 -code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
   3.714 -
   3.715 -thm not_reachable_in_example_graph.equation
   3.716 -thm tranclp.equation
   3.717 -value "not_reachable_in_example_graph 0 3"
   3.718 -value "not_reachable_in_example_graph 4 8"
   3.719 -value "not_reachable_in_example_graph 5 6"
   3.720 -text {* rtrancl compilation is strange! *}
   3.721 -(*
   3.722 -value "not_reachable_in_example_graph 0 4"
   3.723 -value "not_reachable_in_example_graph 1 6"
   3.724 -value "not_reachable_in_example_graph 8 4"*)
   3.725 -
   3.726 -code_pred [dseq] not_reachable_in_example_graph .
   3.727 -
   3.728 -values [dseq 6] "{x. tranclp example_graph 0 3}"
   3.729 -
   3.730 -values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
   3.731 -values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
   3.732 -values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
   3.733 -values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
   3.734 -values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
   3.735 -values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
   3.736 -
   3.737 -
   3.738 -inductive not_reachable_in_example_graph' :: "int => int => bool"
   3.739 -where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
   3.740 -
   3.741 -code_pred not_reachable_in_example_graph' .
   3.742 -
   3.743 -value "not_reachable_in_example_graph' 0 3"
   3.744 -(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
   3.745 -
   3.746 -
   3.747 -(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   3.748 -(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   3.749 -(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
   3.750 -(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   3.751 -(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   3.752 -(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   3.753 -
   3.754 -code_pred [dseq] not_reachable_in_example_graph' .
   3.755 -
   3.756 -(*thm not_reachable_in_example_graph'.dseq_equation*)
   3.757 -
   3.758 -(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   3.759 -(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   3.760 -(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
   3.761 -values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   3.762 -(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   3.763 -(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   3.764 -
   3.765 -subsection {* Free function variable *}
   3.766 -
   3.767 -inductive FF :: "nat => nat => bool"
   3.768 -where
   3.769 -  "f x = y ==> FF x y"
   3.770 -
   3.771 -code_pred FF .
   3.772 -
   3.773 -subsection {* IMP *}
   3.774 -
   3.775 -types
   3.776 -  var = nat
   3.777 -  state = "int list"
   3.778 -
   3.779 -datatype com =
   3.780 -  Skip |
   3.781 -  Ass var "state => int" |
   3.782 -  Seq com com |
   3.783 -  IF "state => bool" com com |
   3.784 -  While "state => bool" com
   3.785 -
   3.786 -inductive exec :: "com => state => state => bool" where
   3.787 -"exec Skip s s" |
   3.788 -"exec (Ass x e) s (s[x := e(s)])" |
   3.789 -"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
   3.790 -"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
   3.791 -"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
   3.792 -"~b s ==> exec (While b c) s s" |
   3.793 -"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
   3.794 -
   3.795 -code_pred exec .
   3.796 -
   3.797 -values "{t. exec
   3.798 - (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
   3.799 - [3,5] t}"
   3.800 -
   3.801 -
   3.802 -inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
   3.803 -"tupled_exec (Skip, s, s)" |
   3.804 -"tupled_exec (Ass x e, s, s[x := e(s)])" |
   3.805 -"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
   3.806 -"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   3.807 -"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   3.808 -"~b s ==> tupled_exec (While b c, s, s)" |
   3.809 -"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
   3.810 -
   3.811 -code_pred tupled_exec .
   3.812 -
   3.813 -values "{s. tupled_exec (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))), [3, 5], s)}"
   3.814 -
   3.815 -subsection {* CCS *}
   3.816 -
   3.817 -text{* This example formalizes finite CCS processes without communication or
   3.818 -recursion. For simplicity, labels are natural numbers. *}
   3.819 -
   3.820 -datatype proc = nil | pre nat proc | or proc proc | par proc proc
   3.821 -
   3.822 -inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
   3.823 -"step (pre n p) n p" |
   3.824 -"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
   3.825 -"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
   3.826 -"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
   3.827 -"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
   3.828 -
   3.829 -code_pred step .
   3.830 -
   3.831 -inductive steps where
   3.832 -"steps p [] p" |
   3.833 -"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
   3.834 -
   3.835 -code_pred steps .
   3.836 -
   3.837 -values 3 
   3.838 - "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   3.839 -
   3.840 -values 5
   3.841 - "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   3.842 -
   3.843 -values 3 "{(a,q). step (par nil nil) a q}"
   3.844 -
   3.845 -
   3.846 -inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
   3.847 -where
   3.848 -"tupled_step (pre n p, n, p)" |
   3.849 -"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   3.850 -"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   3.851 -"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
   3.852 -"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
   3.853 -
   3.854 -code_pred tupled_step .
   3.855 -thm tupled_step.equation
   3.856 -
   3.857 -subsection {* divmod *}
   3.858 -
   3.859 -inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   3.860 -    "k < l \<Longrightarrow> divmod_rel k l 0 k"
   3.861 -  | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
   3.862 -
   3.863 -code_pred divmod_rel .
   3.864 -thm divmod_rel.equation
   3.865 -value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   3.866 -
   3.867 -subsection {* Transforming predicate logic into logic programs *}
   3.868 -
   3.869 -subsection {* Transforming functions into logic programs *}
   3.870 -definition
   3.871 -  "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
   3.872 -
   3.873 -code_pred [inductify, skip_proof] case_f .
   3.874 -thm case_fP.equation
   3.875 -
   3.876 -fun fold_map_idx where
   3.877 -  "fold_map_idx f i y [] = (y, [])"
   3.878 -| "fold_map_idx f i y (x # xs) =
   3.879 - (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
   3.880 - in (y'', x' # xs'))"
   3.881 -
   3.882 -code_pred [inductify] fold_map_idx .
   3.883 -
   3.884 -subsection {* Minimum *}
   3.885 -
   3.886 -definition Min
   3.887 -where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
   3.888 -
   3.889 -code_pred [inductify] Min .
   3.890 -thm Min.equation
   3.891 -
   3.892 -subsection {* Lexicographic order *}
   3.893 -
   3.894 -declare lexord_def[code_pred_def]
   3.895 -code_pred [inductify] lexord .
   3.896 -code_pred [random_dseq inductify] lexord .
   3.897 -
   3.898 -thm lexord.equation
   3.899 -thm lexord.random_dseq_equation
   3.900 -
   3.901 -inductive less_than_nat :: "nat * nat => bool"
   3.902 -where
   3.903 -  "less_than_nat (0, x)"
   3.904 -| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
   3.905 - 
   3.906 -code_pred less_than_nat .
   3.907 -
   3.908 -code_pred [dseq] less_than_nat .
   3.909 -code_pred [random_dseq] less_than_nat .
   3.910 -
   3.911 -inductive test_lexord :: "nat list * nat list => bool"
   3.912 -where
   3.913 -  "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
   3.914 -
   3.915 -code_pred test_lexord .
   3.916 -code_pred [dseq] test_lexord .
   3.917 -code_pred [random_dseq] test_lexord .
   3.918 -thm test_lexord.dseq_equation
   3.919 -thm test_lexord.random_dseq_equation
   3.920 -
   3.921 -values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
   3.922 -(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
   3.923 -
   3.924 -lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
   3.925 -(*
   3.926 -code_pred [inductify] lexn .
   3.927 -thm lexn.equation
   3.928 -*)
   3.929 -(*
   3.930 -code_pred [random_dseq inductify] lexn .
   3.931 -thm lexn.random_dseq_equation
   3.932 -
   3.933 -values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   3.934 -*)
   3.935 -inductive has_length
   3.936 -where
   3.937 -  "has_length [] 0"
   3.938 -| "has_length xs i ==> has_length (x # xs) (Suc i)" 
   3.939 -
   3.940 -lemma has_length:
   3.941 -  "has_length xs n = (length xs = n)"
   3.942 -proof (rule iffI)
   3.943 -  assume "has_length xs n"
   3.944 -  from this show "length xs = n"
   3.945 -    by (rule has_length.induct) auto
   3.946 -next
   3.947 -  assume "length xs = n"
   3.948 -  from this show "has_length xs n"
   3.949 -    by (induct xs arbitrary: n) (auto intro: has_length.intros)
   3.950 -qed
   3.951 -
   3.952 -lemma lexn_intros [code_pred_intro]:
   3.953 -  "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
   3.954 -  "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
   3.955 -proof -
   3.956 -  assume "has_length xs i" "has_length ys i" "r (x, y)"
   3.957 -  from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
   3.958 -    unfolding lexn_conv Collect_def mem_def
   3.959 -    by fastsimp
   3.960 -next
   3.961 -  assume "lexn r i (xs, ys)"
   3.962 -  thm lexn_conv
   3.963 -  from this show "lexn r (Suc i) (x#xs, x#ys)"
   3.964 -    unfolding Collect_def mem_def lexn_conv
   3.965 -    apply auto
   3.966 -    apply (rule_tac x="x # xys" in exI)
   3.967 -    by auto
   3.968 -qed
   3.969 -
   3.970 -code_pred [random_dseq] lexn
   3.971 -proof -
   3.972 -  fix r n xs ys
   3.973 -  assume 1: "lexn r n (xs, ys)"
   3.974 -  assume 2: "\<And>r' i x xs' y ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r' (x, y) ==> thesis"
   3.975 -  assume 3: "\<And>r' i x xs' ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r' i (xs', ys') ==> thesis"
   3.976 -  from 1 2 3 show thesis
   3.977 -    unfolding lexn_conv Collect_def mem_def
   3.978 -    apply (auto simp add: has_length)
   3.979 -    apply (case_tac xys)
   3.980 -    apply auto
   3.981 -    apply fastsimp
   3.982 -    apply fastsimp done
   3.983 -qed
   3.984 -
   3.985 -values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   3.986 -
   3.987 -code_pred [inductify, skip_proof] lex .
   3.988 -thm lex.equation
   3.989 -thm lex_def
   3.990 -declare lenlex_conv[code_pred_def]
   3.991 -code_pred [inductify, skip_proof] lenlex .
   3.992 -thm lenlex.equation
   3.993 -
   3.994 -code_pred [random_dseq inductify] lenlex .
   3.995 -thm lenlex.random_dseq_equation
   3.996 -
   3.997 -values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
   3.998 -
   3.999 -thm lists.intros
  3.1000 -code_pred [inductify] lists .
  3.1001 -thm lists.equation
  3.1002 -
  3.1003 -subsection {* AVL Tree *}
  3.1004 -
  3.1005 -datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
  3.1006 -fun height :: "'a tree => nat" where
  3.1007 -"height ET = 0"
  3.1008 -| "height (MKT x l r h) = max (height l) (height r) + 1"
  3.1009 -
  3.1010 -primrec avl :: "'a tree => bool"
  3.1011 -where
  3.1012 -  "avl ET = True"
  3.1013 -| "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
  3.1014 -  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
  3.1015 -(*
  3.1016 -code_pred [inductify] avl .
  3.1017 -thm avl.equation*)
  3.1018 -
  3.1019 -code_pred [new_random_dseq inductify] avl .
  3.1020 -thm avl.new_random_dseq_equation
  3.1021 -
  3.1022 -values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
  3.1023 -
  3.1024 -fun set_of
  3.1025 -where
  3.1026 -"set_of ET = {}"
  3.1027 -| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
  3.1028 -
  3.1029 -fun is_ord :: "nat tree => bool"
  3.1030 -where
  3.1031 -"is_ord ET = True"
  3.1032 -| "is_ord (MKT n l r h) =
  3.1033 - ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
  3.1034 -
  3.1035 -code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
  3.1036 -thm set_of.equation
  3.1037 -
  3.1038 -code_pred (expected_modes: i => bool) [inductify] is_ord .
  3.1039 -thm is_ord_aux.equation
  3.1040 -thm is_ord.equation
  3.1041 -
  3.1042 -subsection {* Definitions about Relations *}
  3.1043 -
  3.1044 -term "converse"
  3.1045 -code_pred (modes:
  3.1046 -  (i * i => bool) => i * i => bool,
  3.1047 -  (i * o => bool) => o * i => bool,
  3.1048 -  (i * o => bool) => i * i => bool,
  3.1049 -  (o * i => bool) => i * o => bool,
  3.1050 -  (o * i => bool) => i * i => bool,
  3.1051 -  (o * o => bool) => o * o => bool,
  3.1052 -  (o * o => bool) => i * o => bool,
  3.1053 -  (o * o => bool) => o * i => bool,
  3.1054 -  (o * o => bool) => i * i => bool) [inductify] converse .
  3.1055 -
  3.1056 -thm converse.equation
  3.1057 -code_pred [inductify] rel_comp .
  3.1058 -thm rel_comp.equation
  3.1059 -code_pred [inductify] Image .
  3.1060 -thm Image.equation
  3.1061 -declare singleton_iff[code_pred_inline]
  3.1062 -declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
  3.1063 -
  3.1064 -code_pred (expected_modes:
  3.1065 -  (o => bool) => o => bool,
  3.1066 -  (o => bool) => i * o => bool,
  3.1067 -  (o => bool) => o * i => bool,
  3.1068 -  (o => bool) => i => bool,
  3.1069 -  (i => bool) => i * o => bool,
  3.1070 -  (i => bool) => o * i => bool,
  3.1071 -  (i => bool) => i => bool) [inductify] Id_on .
  3.1072 -thm Id_on.equation
  3.1073 -thm Domain_def
  3.1074 -code_pred (modes:
  3.1075 -  (o * o => bool) => o => bool,
  3.1076 -  (o * o => bool) => i => bool,
  3.1077 -  (i * o => bool) => i => bool) [inductify] Domain .
  3.1078 -thm Domain.equation
  3.1079 -
  3.1080 -thm Range_def
  3.1081 -code_pred (modes:
  3.1082 -  (o * o => bool) => o => bool,
  3.1083 -  (o * o => bool) => i => bool,
  3.1084 -  (o * i => bool) => i => bool) [inductify] Range .
  3.1085 -thm Range.equation
  3.1086 -
  3.1087 -code_pred [inductify] Field .
  3.1088 -thm Field.equation
  3.1089 -
  3.1090 -thm refl_on_def
  3.1091 -code_pred [inductify] refl_on .
  3.1092 -thm refl_on.equation
  3.1093 -code_pred [inductify] total_on .
  3.1094 -thm total_on.equation
  3.1095 -code_pred [inductify] antisym .
  3.1096 -thm antisym.equation
  3.1097 -code_pred [inductify] trans .
  3.1098 -thm trans.equation
  3.1099 -code_pred [inductify] single_valued .
  3.1100 -thm single_valued.equation
  3.1101 -thm inv_image_def
  3.1102 -code_pred [inductify] inv_image .
  3.1103 -thm inv_image.equation
  3.1104 -
  3.1105 -subsection {* Inverting list functions *}
  3.1106 -
  3.1107 -code_pred [inductify] size_list .
  3.1108 -code_pred [new_random_dseq inductify] size_list .
  3.1109 -thm size_listP.equation
  3.1110 -thm size_listP.new_random_dseq_equation
  3.1111 -
  3.1112 -values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
  3.1113 -
  3.1114 -code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
  3.1115 -thm concatP.equation
  3.1116 -
  3.1117 -values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
  3.1118 -values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
  3.1119 -
  3.1120 -code_pred [dseq inductify] List.concat .
  3.1121 -thm concatP.dseq_equation
  3.1122 -
  3.1123 -values [dseq 3] 3
  3.1124 -  "{xs. concatP xs ([0] :: nat list)}"
  3.1125 -
  3.1126 -values [dseq 5] 3
  3.1127 -  "{xs. concatP xs ([1] :: int list)}"
  3.1128 -
  3.1129 -values [dseq 5] 3
  3.1130 -  "{xs. concatP xs ([1] :: nat list)}"
  3.1131 -
  3.1132 -values [dseq 5] 3
  3.1133 -  "{xs. concatP xs [(1::int), 2]}"
  3.1134 -
  3.1135 -code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
  3.1136 -thm hdP.equation
  3.1137 -values "{x. hdP [1, 2, (3::int)] x}"
  3.1138 -values "{(xs, x). hdP [1, 2, (3::int)] 1}"
  3.1139 - 
  3.1140 -code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
  3.1141 -thm tlP.equation
  3.1142 -values "{x. tlP [1, 2, (3::nat)] x}"
  3.1143 -values "{x. tlP [1, 2, (3::int)] [3]}"
  3.1144 -
  3.1145 -code_pred [inductify, skip_proof] last .
  3.1146 -thm lastP.equation
  3.1147 -
  3.1148 -code_pred [inductify, skip_proof] butlast .
  3.1149 -thm butlastP.equation
  3.1150 -
  3.1151 -code_pred [inductify, skip_proof] take .
  3.1152 -thm takeP.equation
  3.1153 -
  3.1154 -code_pred [inductify, skip_proof] drop .
  3.1155 -thm dropP.equation
  3.1156 -code_pred [inductify, skip_proof] zip .
  3.1157 -thm zipP.equation
  3.1158 -
  3.1159 -code_pred [inductify, skip_proof] upt .
  3.1160 -code_pred [inductify, skip_proof] remdups .
  3.1161 -thm remdupsP.equation
  3.1162 -code_pred [dseq inductify] remdups .
  3.1163 -values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
  3.1164 -
  3.1165 -code_pred [inductify, skip_proof] remove1 .
  3.1166 -thm remove1P.equation
  3.1167 -values "{xs. remove1P 1 xs [2, (3::int)]}"
  3.1168 -
  3.1169 -code_pred [inductify, skip_proof] removeAll .
  3.1170 -thm removeAllP.equation
  3.1171 -code_pred [dseq inductify] removeAll .
  3.1172 -
  3.1173 -values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
  3.1174 -
  3.1175 -code_pred [inductify] distinct .
  3.1176 -thm distinct.equation
  3.1177 -code_pred [inductify, skip_proof] replicate .
  3.1178 -thm replicateP.equation
  3.1179 -values 5 "{(n, xs). replicateP n (0::int) xs}"
  3.1180 -
  3.1181 -code_pred [inductify, skip_proof] splice .
  3.1182 -thm splice.simps
  3.1183 -thm spliceP.equation
  3.1184 -
  3.1185 -values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
  3.1186 -
  3.1187 -code_pred [inductify, skip_proof] List.rev .
  3.1188 -code_pred [inductify] map .
  3.1189 -code_pred [inductify] foldr .
  3.1190 -code_pred [inductify] foldl .
  3.1191 -code_pred [inductify] filter .
  3.1192 -code_pred [random_dseq inductify] filter .
  3.1193 -
  3.1194 -subsection {* Context Free Grammar *}
  3.1195 -
  3.1196 -datatype alphabet = a | b
  3.1197 -
  3.1198 -inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
  3.1199 -  "[] \<in> S\<^isub>1"
  3.1200 -| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
  3.1201 -| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
  3.1202 -| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
  3.1203 -| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
  3.1204 -| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
  3.1205 -
  3.1206 -code_pred [inductify] S\<^isub>1p .
  3.1207 -code_pred [random_dseq inductify] S\<^isub>1p .
  3.1208 -thm S\<^isub>1p.equation
  3.1209 -thm S\<^isub>1p.random_dseq_equation
  3.1210 -
  3.1211 -values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
  3.1212 -
  3.1213 -inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
  3.1214 -  "[] \<in> S\<^isub>2"
  3.1215 -| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
  3.1216 -| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
  3.1217 -| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
  3.1218 -| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
  3.1219 -| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
  3.1220 -
  3.1221 -code_pred [random_dseq inductify] S\<^isub>2p .
  3.1222 -thm S\<^isub>2p.random_dseq_equation
  3.1223 -thm A\<^isub>2p.random_dseq_equation
  3.1224 -thm B\<^isub>2p.random_dseq_equation
  3.1225 -
  3.1226 -values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
  3.1227 -
  3.1228 -inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
  3.1229 -  "[] \<in> S\<^isub>3"
  3.1230 -| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
  3.1231 -| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
  3.1232 -| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
  3.1233 -| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
  3.1234 -| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
  3.1235 -
  3.1236 -code_pred [inductify, skip_proof] S\<^isub>3p .
  3.1237 -thm S\<^isub>3p.equation
  3.1238 -
  3.1239 -values 10 "{x. S\<^isub>3p x}"
  3.1240 -
  3.1241 -inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
  3.1242 -  "[] \<in> S\<^isub>4"
  3.1243 -| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
  3.1244 -| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
  3.1245 -| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
  3.1246 -| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
  3.1247 -| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
  3.1248 -| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
  3.1249 -
  3.1250 -code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
  3.1251 -
  3.1252 -hide_const a b
  3.1253 -
  3.1254 -subsection {* Lambda *}
  3.1255 -
  3.1256 -datatype type =
  3.1257 -    Atom nat
  3.1258 -  | Fun type type    (infixr "\<Rightarrow>" 200)
  3.1259 -
  3.1260 -datatype dB =
  3.1261 -    Var nat
  3.1262 -  | App dB dB (infixl "\<degree>" 200)
  3.1263 -  | Abs type dB
  3.1264 -
  3.1265 -primrec
  3.1266 -  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
  3.1267 -where
  3.1268 -  "[]\<langle>i\<rangle> = None"
  3.1269 -| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
  3.1270 -
  3.1271 -inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
  3.1272 -where
  3.1273 -  "nth_el' (x # xs) 0 x"
  3.1274 -| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
  3.1275 -
  3.1276 -inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
  3.1277 -  where
  3.1278 -    Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
  3.1279 -  | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
  3.1280 -  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
  3.1281 -
  3.1282 -primrec
  3.1283 -  lift :: "[dB, nat] => dB"
  3.1284 -where
  3.1285 -    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
  3.1286 -  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
  3.1287 -  | "lift (Abs T s) k = Abs T (lift s (k + 1))"
  3.1288 -
  3.1289 -primrec
  3.1290 -  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
  3.1291 -where
  3.1292 -    subst_Var: "(Var i)[s/k] =
  3.1293 -      (if k < i then Var (i - 1) else if i = k then s else Var i)"
  3.1294 -  | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
  3.1295 -  | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
  3.1296 -
  3.1297 -inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
  3.1298 -  where
  3.1299 -    beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
  3.1300 -  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
  3.1301 -  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
  3.1302 -  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
  3.1303 -
  3.1304 -code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
  3.1305 -thm typing.equation
  3.1306 -
  3.1307 -code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .
  3.1308 -thm beta.equation
  3.1309 -
  3.1310 -values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
  3.1311 -
  3.1312 -definition "reduce t = Predicate.the (reduce' t)"
  3.1313 -
  3.1314 -value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
  3.1315 -
  3.1316 -code_pred [dseq] typing .
  3.1317 -code_pred [random_dseq] typing .
  3.1318 -
  3.1319 -values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
  3.1320 -
  3.1321 -subsection {* A minimal example of yet another semantics *}
  3.1322 -
  3.1323 -text {* thanks to Elke Salecker *}
  3.1324 -
  3.1325 -types
  3.1326 -  vname = nat
  3.1327 -  vvalue = int
  3.1328 -  var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
  3.1329 -
  3.1330 -datatype ir_expr = 
  3.1331 -  IrConst vvalue
  3.1332 -| ObjAddr vname
  3.1333 -| Add ir_expr ir_expr
  3.1334 -
  3.1335 -datatype val =
  3.1336 -  IntVal  vvalue
  3.1337 -
  3.1338 -record  configuration =
  3.1339 -  Env :: var_assign
  3.1340 -
  3.1341 -inductive eval_var ::
  3.1342 -  "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
  3.1343 -where
  3.1344 -  irconst: "eval_var (IrConst i) conf (IntVal i)"
  3.1345 -| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
  3.1346 -| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
  3.1347 -
  3.1348 -
  3.1349 -code_pred eval_var .
  3.1350 -thm eval_var.equation
  3.1351 -
  3.1352 -values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
  3.1353 -
  3.1354 -section {* Function predicate replacement *}
  3.1355 -
  3.1356 -text {*
  3.1357 -If the mode analysis uses the functional mode, we
  3.1358 -replace predicates that resulted from functions again by their functions.
  3.1359 -*}
  3.1360 -
  3.1361 -inductive test_append
  3.1362 -where
  3.1363 -  "List.append xs ys = zs ==> test_append xs ys zs"
  3.1364 -
  3.1365 -code_pred [inductify, skip_proof] test_append .
  3.1366 -thm test_append.equation
  3.1367 -
  3.1368 -text {* If append is not turned into a predicate, then the mode
  3.1369 -  o => o => i => bool could not be inferred. *}
  3.1370 -
  3.1371 -values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
  3.1372 -
  3.1373 -text {* If appendP is not reverted back to a function, then mode i => i => o => bool
  3.1374 -  fails after deleting the predicate equation. *}
  3.1375 -
  3.1376 -declare appendP.equation[code del]
  3.1377 -
  3.1378 -values "{xs::int list. test_append [1,2] [3,4] xs}"
  3.1379 -values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
  3.1380 -values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
  3.1381 -
  3.1382 -text {* Redeclaring append.equation as code equation *}
  3.1383 -
  3.1384 -declare appendP.equation[code]
  3.1385 -
  3.1386 -subsection {* Function with tuples *}
  3.1387 -
  3.1388 -fun append'
  3.1389 -where
  3.1390 -  "append' ([], ys) = ys"
  3.1391 -| "append' (x # xs, ys) = x # append' (xs, ys)"
  3.1392 -
  3.1393 -inductive test_append'
  3.1394 -where
  3.1395 -  "append' (xs, ys) = zs ==> test_append' xs ys zs"
  3.1396 -
  3.1397 -code_pred [inductify, skip_proof] test_append' .
  3.1398 -
  3.1399 -thm test_append'.equation
  3.1400 -
  3.1401 -values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
  3.1402 -
  3.1403 -declare append'P.equation[code del]
  3.1404 -
  3.1405 -values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
  3.1406 -
  3.1407 -section {* Arithmetic examples *}
  3.1408 -
  3.1409 -subsection {* Examples on nat *}
  3.1410 -
  3.1411 -inductive plus_nat_test :: "nat => nat => nat => bool"
  3.1412 -where
  3.1413 -  "x + y = z ==> plus_nat_test x y z"
  3.1414 -
  3.1415 -code_pred [inductify, skip_proof] plus_nat_test .
  3.1416 -code_pred [new_random_dseq inductify] plus_nat_test .
  3.1417 -
  3.1418 -thm plus_nat_test.equation
  3.1419 -thm plus_nat_test.new_random_dseq_equation
  3.1420 -
  3.1421 -values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
  3.1422 -values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
  3.1423 -values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
  3.1424 -values [expected "{}"] "{y. plus_nat_test 9 y 8}"
  3.1425 -values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
  3.1426 -values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
  3.1427 -values [expected "{}"] "{x. plus_nat_test x 9 7}"
  3.1428 -values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
  3.1429 -values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
  3.1430 -values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"]
  3.1431 -  "{(x, y). plus_nat_test x y 5}"
  3.1432 -
  3.1433 -inductive minus_nat_test :: "nat => nat => nat => bool"
  3.1434 -where
  3.1435 -  "x - y = z ==> minus_nat_test x y z"
  3.1436 -
  3.1437 -code_pred [inductify, skip_proof] minus_nat_test .
  3.1438 -code_pred [new_random_dseq inductify] minus_nat_test .
  3.1439 -
  3.1440 -thm minus_nat_test.equation
  3.1441 -thm minus_nat_test.new_random_dseq_equation
  3.1442 -
  3.1443 -values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
  3.1444 -values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
  3.1445 -values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
  3.1446 -values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
  3.1447 -values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}"
  3.1448 -values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
  3.1449 -
  3.1450 -subsection {* Examples on int *}
  3.1451 -
  3.1452 -inductive plus_int_test :: "int => int => int => bool"
  3.1453 -where
  3.1454 -  "a + b = c ==> plus_int_test a b c"
  3.1455 -
  3.1456 -code_pred [inductify, skip_proof] plus_int_test .
  3.1457 -code_pred [new_random_dseq inductify] plus_int_test .
  3.1458 -
  3.1459 -thm plus_int_test.equation
  3.1460 -thm plus_int_test.new_random_dseq_equation
  3.1461 -
  3.1462 -values [expected "{1::int}"] "{a. plus_int_test a 6 7}"
  3.1463 -values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"
  3.1464 -values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"
  3.1465 -
  3.1466 -inductive minus_int_test :: "int => int => int => bool"
  3.1467 -where
  3.1468 -  "a - b = c ==> minus_int_test a b c"
  3.1469 -
  3.1470 -code_pred [inductify, skip_proof] minus_int_test .
  3.1471 -code_pred [new_random_dseq inductify] minus_int_test .
  3.1472 -
  3.1473 -thm minus_int_test.equation
  3.1474 -thm minus_int_test.new_random_dseq_equation
  3.1475 -
  3.1476 -values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
  3.1477 -values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
  3.1478 -values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
  3.1479 -
  3.1480 -subsection {* minus on bool *}
  3.1481 -
  3.1482 -inductive All :: "nat => bool"
  3.1483 -where
  3.1484 -  "All x"
  3.1485 -
  3.1486 -inductive None :: "nat => bool"
  3.1487 -
  3.1488 -definition "test_minus_bool x = (None x - All x)"
  3.1489 -
  3.1490 -code_pred [inductify] test_minus_bool .
  3.1491 -thm test_minus_bool.equation
  3.1492 -
  3.1493 -values "{x. test_minus_bool x}"
  3.1494 -
  3.1495 -subsection {* Functions *}
  3.1496 -
  3.1497 -fun partial_hd :: "'a list => 'a option"
  3.1498 -where
  3.1499 -  "partial_hd [] = Option.None"
  3.1500 -| "partial_hd (x # xs) = Some x"
  3.1501 -
  3.1502 -inductive hd_predicate
  3.1503 -where
  3.1504 -  "partial_hd xs = Some x ==> hd_predicate xs x"
  3.1505 -
  3.1506 -code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
  3.1507 -
  3.1508 -thm hd_predicate.equation
  3.1509 -
  3.1510 -subsection {* Locales *}
  3.1511 -
  3.1512 -inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"
  3.1513 -where
  3.1514 -  "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"
  3.1515 -
  3.1516 -
  3.1517 -thm hd_predicate2.intros
  3.1518 -
  3.1519 -code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
  3.1520 -thm hd_predicate2.equation
  3.1521 -
  3.1522 -locale A = fixes partial_hd :: "'a list => 'a option" begin
  3.1523 -
  3.1524 -inductive hd_predicate_in_locale :: "'a list => 'a => bool"
  3.1525 -where
  3.1526 -  "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
  3.1527 -
  3.1528 -end
  3.1529 -
  3.1530 -text {* The global introduction rules must be redeclared as introduction rules and then 
  3.1531 -  one could invoke code_pred. *}
  3.1532 -
  3.1533 -declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro]
  3.1534 -
  3.1535 -code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
  3.1536 -unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases)
  3.1537 -    
  3.1538 -interpretation A partial_hd .
  3.1539 -thm hd_predicate_in_locale.intros
  3.1540 -text {* A locally compliant solution with a trivial interpretation fails, because
  3.1541 -the predicate compiler has very strict assumptions about the terms and their structure. *}
  3.1542 - 
  3.1543 -(*code_pred hd_predicate_in_locale .*)
  3.1544 -
  3.1545 -section {* Integer example *}
  3.1546 -
  3.1547 -definition three :: int
  3.1548 -where "three = 3"
  3.1549 -
  3.1550 -inductive is_three
  3.1551 -where
  3.1552 -  "is_three three"
  3.1553 -
  3.1554 -code_pred is_three .
  3.1555 -
  3.1556 -thm is_three.equation
  3.1557 -
  3.1558 -section {* String.literal example *}
  3.1559 -
  3.1560 -definition Error_1
  3.1561 -where
  3.1562 -  "Error_1 = STR ''Error 1''"
  3.1563 -
  3.1564 -definition Error_2
  3.1565 -where
  3.1566 -  "Error_2 = STR ''Error 2''"
  3.1567 -
  3.1568 -inductive "is_error" :: "String.literal \<Rightarrow> bool"
  3.1569 -where
  3.1570 -  "is_error Error_1"
  3.1571 -| "is_error Error_2"
  3.1572 -
  3.1573 -code_pred is_error .
  3.1574 -
  3.1575 -thm is_error.equation
  3.1576 -
  3.1577 -inductive is_error' :: "String.literal \<Rightarrow> bool"
  3.1578 -where
  3.1579 -  "is_error' (STR ''Error1'')"
  3.1580 -| "is_error' (STR ''Error2'')"
  3.1581 -
  3.1582 -code_pred is_error' .
  3.1583 -
  3.1584 -thm is_error'.equation
  3.1585 -
  3.1586 -datatype ErrorObject = Error String.literal int
  3.1587 -
  3.1588 -inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
  3.1589 -where
  3.1590 -  "is_error'' (Error Error_1 3)"
  3.1591 -| "is_error'' (Error Error_2 4)"
  3.1592 -
  3.1593 -code_pred is_error'' .
  3.1594 -
  3.1595 -thm is_error''.equation
  3.1596 -
  3.1597 -section {* Another function example *}
  3.1598 -
  3.1599 -consts f :: "'a \<Rightarrow> 'a"
  3.1600 -
  3.1601 -inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  3.1602 -where
  3.1603 -  "fun_upd ((x, a), s) (s(x := f a))"
  3.1604 -
  3.1605 -code_pred fun_upd .
  3.1606 -
  3.1607 -thm fun_upd.equation
  3.1608 -
  3.1609 -section {* Another semantics *}
  3.1610 -
  3.1611 -types
  3.1612 -  name = nat --"For simplicity in examples"
  3.1613 -  state' = "name \<Rightarrow> nat"
  3.1614 -
  3.1615 -datatype aexp = N nat | V name | Plus aexp aexp
  3.1616 -
  3.1617 -fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where
  3.1618 -"aval (N n) _ = n" |
  3.1619 -"aval (V x) st = st x" |
  3.1620 -"aval (Plus e\<^isub>1 e\<^isub>2) st = aval e\<^isub>1 st + aval e\<^isub>2 st"
  3.1621 -
  3.1622 -datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
  3.1623 -
  3.1624 -primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where
  3.1625 -"bval (B b) _ = b" |
  3.1626 -"bval (Not b) st = (\<not> bval b st)" |
  3.1627 -"bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |
  3.1628 -"bval (Less a\<^isub>1 a\<^isub>2) st = (aval a\<^isub>1 st < aval a\<^isub>2 st)"
  3.1629 -
  3.1630 -datatype
  3.1631 -  com' = SKIP 
  3.1632 -      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
  3.1633 -      | Semi   com'  com'          ("_; _"  [60, 61] 60)
  3.1634 -      | If     bexp com' com'     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
  3.1635 -      | While  bexp com'         ("WHILE _ DO _"  [0, 61] 61)
  3.1636 -
  3.1637 -inductive
  3.1638 -  big_step :: "com' * state' \<Rightarrow> state' \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
  3.1639 -where
  3.1640 -  Skip:    "(SKIP,s) \<Rightarrow> s"
  3.1641 -| Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)"
  3.1642 -
  3.1643 -| Semi:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3  \<Longrightarrow> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3"
  3.1644 -
  3.1645 -| IfTrue:  "bval b s  \<Longrightarrow>  (c\<^isub>1,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"
  3.1646 -| IfFalse: "\<not>bval b s  \<Longrightarrow>  (c\<^isub>2,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"
  3.1647 -
  3.1648 -| WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s"
  3.1649 -| WhileTrue:  "bval b s\<^isub>1  \<Longrightarrow>  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3
  3.1650 -               \<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
  3.1651 -
  3.1652 -code_pred big_step .
  3.1653 -
  3.1654 -thm big_step.equation
  3.1655 -
  3.1656 -section {* General Context Free Grammars *}
  3.1657 -text {* a contribution by Aditi Barthwal *}
  3.1658 -
  3.1659 -datatype ('nts,'ts) symbol = NTS 'nts
  3.1660 -                            | TS 'ts
  3.1661 -
  3.1662 -                            
  3.1663 -datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
  3.1664 -
  3.1665 -types ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
  3.1666 -
  3.1667 -fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set"
  3.1668 -where
  3.1669 -  "rules (r, s) = r"
  3.1670 -
  3.1671 -definition derives 
  3.1672 -where
  3.1673 -"derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. 
  3.1674 -                         (s1 @ [NTS lhs] @ s2 = lsl) \<and>
  3.1675 -                         (s1 @ rhs @ s2) = rsl \<and>
  3.1676 -                         (rule lhs rhs) \<in> fst g }"
  3.1677 -
  3.1678 -abbreviation "example_grammar == 
  3.1679 -({ rule ''S'' [NTS ''A'', NTS ''B''],
  3.1680 -   rule ''S'' [TS ''a''],
  3.1681 -  rule ''A'' [TS ''b'']}, ''S'')"
  3.1682 -
  3.1683 -
  3.1684 -code_pred [inductify, skip_proof] derives .
  3.1685 -
  3.1686 -thm derives.equation
  3.1687 -
  3.1688 -definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
  3.1689 -
  3.1690 -code_pred (modes: o \<Rightarrow> bool) [inductify] test .
  3.1691 -thm test.equation
  3.1692 -
  3.1693 -values "{rhs. test rhs}"
  3.1694 -
  3.1695 -declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def]
  3.1696 -
  3.1697 -code_pred [inductify] rtrancl .
  3.1698 -
  3.1699 -definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^*  }"
  3.1700 -
  3.1701 -code_pred [inductify, skip_proof] test2 .
  3.1702 -
  3.1703 -values "{rhs. test2 rhs}"
  3.1704 -
  3.1705 -
  3.1706 -section {* Examples for detecting switches *}
  3.1707 -
  3.1708 -inductive detect_switches1 where
  3.1709 -  "detect_switches1 [] []"
  3.1710 -| "detect_switches1 (x # xs) (y # ys)"
  3.1711 -
  3.1712 -code_pred [detect_switches, skip_proof] detect_switches1 .
  3.1713 -
  3.1714 -thm detect_switches1.equation
  3.1715 -
  3.1716 -inductive detect_switches2 :: "('a => bool) => bool"
  3.1717 -where
  3.1718 -  "detect_switches2 P"
  3.1719 -
  3.1720 -code_pred [detect_switches, skip_proof] detect_switches2 .
  3.1721 -thm detect_switches2.equation
  3.1722 -
  3.1723 -inductive detect_switches3 :: "('a => bool) => 'a list => bool"
  3.1724 -where
  3.1725 -  "detect_switches3 P []"
  3.1726 -| "detect_switches3 P (x # xs)" 
  3.1727 -
  3.1728 -code_pred [detect_switches, skip_proof] detect_switches3 .
  3.1729 -
  3.1730 -thm detect_switches3.equation
  3.1731 -
  3.1732 -inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
  3.1733 -where
  3.1734 -  "detect_switches4 P [] []"
  3.1735 -| "detect_switches4 P (x # xs) (y # ys)"
  3.1736 -
  3.1737 -code_pred [detect_switches, skip_proof] detect_switches4 .
  3.1738 -thm detect_switches4.equation
  3.1739 -
  3.1740 -inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
  3.1741 -where
  3.1742 -  "detect_switches5 P [] []"
  3.1743 -| "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
  3.1744 -
  3.1745 -code_pred [detect_switches, skip_proof] detect_switches5 .
  3.1746 -
  3.1747 -thm detect_switches5.equation
  3.1748 -
  3.1749 -inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
  3.1750 -where
  3.1751 -  "detect_switches6 (P, [], [])"
  3.1752 -| "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
  3.1753 -
  3.1754 -code_pred [detect_switches, skip_proof] detect_switches6 .
  3.1755 -
  3.1756 -inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
  3.1757 -where
  3.1758 -  "detect_switches7 P Q (a, [])"
  3.1759 -| "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
  3.1760 -
  3.1761 -code_pred [skip_proof] detect_switches7 .
  3.1762 -
  3.1763 -thm detect_switches7.equation
  3.1764 -
  3.1765 -inductive detect_switches8 :: "nat => bool"
  3.1766 -where
  3.1767 -  "detect_switches8 0"
  3.1768 -| "x mod 2 = 0 ==> detect_switches8 (Suc x)"
  3.1769 -
  3.1770 -code_pred [detect_switches, skip_proof] detect_switches8 .
  3.1771 -
  3.1772 -thm detect_switches8.equation
  3.1773 -
  3.1774 -inductive detect_switches9 :: "nat => nat => bool"
  3.1775 -where
  3.1776 -  "detect_switches9 0 0"
  3.1777 -| "detect_switches9 0 (Suc x)"
  3.1778 -| "detect_switches9 (Suc x) 0"
  3.1779 -| "x = y ==> detect_switches9 (Suc x) (Suc y)"
  3.1780 -| "c1 = c2 ==> detect_switches9 c1 c2"
  3.1781 -
  3.1782 -code_pred [detect_switches, skip_proof] detect_switches9 .
  3.1783 -
  3.1784 -thm detect_switches9.equation
  3.1785 -
  3.1786 -
  3.1787 -
  3.1788 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 23 14:50:18 2010 +0200
     4.3 @@ -0,0 +1,1488 @@
     4.4 +theory Predicate_Compile_Tests
     4.5 +imports Predicate_Compile_Alternative_Defs
     4.6 +begin
     4.7 +
     4.8 +subsection {* Basic predicates *}
     4.9 +
    4.10 +inductive False' :: "bool"
    4.11 +
    4.12 +code_pred (expected_modes: bool) False' .
    4.13 +code_pred [dseq] False' .
    4.14 +code_pred [random_dseq] False' .
    4.15 +
    4.16 +values [expected "{}" pred] "{x. False'}"
    4.17 +values [expected "{}" dseq 1] "{x. False'}"
    4.18 +values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
    4.19 +
    4.20 +value "False'"
    4.21 +
    4.22 +inductive True' :: "bool"
    4.23 +where
    4.24 +  "True ==> True'"
    4.25 +
    4.26 +code_pred True' .
    4.27 +code_pred [dseq] True' .
    4.28 +code_pred [random_dseq] True' .
    4.29 +
    4.30 +thm True'.equation
    4.31 +thm True'.dseq_equation
    4.32 +thm True'.random_dseq_equation
    4.33 +values [expected "{()}" ]"{x. True'}"
    4.34 +values [expected "{}" dseq 0] "{x. True'}"
    4.35 +values [expected "{()}" dseq 1] "{x. True'}"
    4.36 +values [expected "{()}" dseq 2] "{x. True'}"
    4.37 +values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
    4.38 +values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
    4.39 +values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
    4.40 +values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
    4.41 +
    4.42 +inductive EmptySet :: "'a \<Rightarrow> bool"
    4.43 +
    4.44 +code_pred (expected_modes: o => bool, i => bool) EmptySet .
    4.45 +
    4.46 +definition EmptySet' :: "'a \<Rightarrow> bool"
    4.47 +where "EmptySet' = {}"
    4.48 +
    4.49 +code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
    4.50 +
    4.51 +inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
    4.52 +
    4.53 +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
    4.54 +
    4.55 +inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.56 +for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.57 +
    4.58 +code_pred
    4.59 +  (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
    4.60 +         (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
    4.61 +         (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
    4.62 +         (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
    4.63 +         (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
    4.64 +         (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
    4.65 +         (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
    4.66 +         (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
    4.67 +  EmptyClosure .
    4.68 +
    4.69 +thm EmptyClosure.equation
    4.70 +
    4.71 +(* TODO: inductive package is broken!
    4.72 +inductive False'' :: "bool"
    4.73 +where
    4.74 +  "False \<Longrightarrow> False''"
    4.75 +
    4.76 +code_pred (expected_modes: []) False'' .
    4.77 +
    4.78 +inductive EmptySet'' :: "'a \<Rightarrow> bool"
    4.79 +where
    4.80 +  "False \<Longrightarrow> EmptySet'' x"
    4.81 +
    4.82 +code_pred (expected_modes: [1]) EmptySet'' .
    4.83 +code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
    4.84 +*)
    4.85 +
    4.86 +consts a' :: 'a
    4.87 +
    4.88 +inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.89 +where
    4.90 +"Fact a' a'"
    4.91 +
    4.92 +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
    4.93 +
    4.94 +inductive zerozero :: "nat * nat => bool"
    4.95 +where
    4.96 +  "zerozero (0, 0)"
    4.97 +
    4.98 +code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
    4.99 +code_pred [dseq] zerozero .
   4.100 +code_pred [random_dseq] zerozero .
   4.101 +
   4.102 +thm zerozero.equation
   4.103 +thm zerozero.dseq_equation
   4.104 +thm zerozero.random_dseq_equation
   4.105 +
   4.106 +text {* We expect the user to expand the tuples in the values command.
   4.107 +The following values command is not supported. *}
   4.108 +(*values "{x. zerozero x}" *)
   4.109 +text {* Instead, the user must type *}
   4.110 +values "{(x, y). zerozero (x, y)}"
   4.111 +
   4.112 +values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
   4.113 +values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
   4.114 +values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
   4.115 +values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
   4.116 +values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
   4.117 +
   4.118 +inductive nested_tuples :: "((int * int) * int * int) => bool"
   4.119 +where
   4.120 +  "nested_tuples ((0, 1), 2, 3)"
   4.121 +
   4.122 +code_pred nested_tuples .
   4.123 +
   4.124 +inductive JamesBond :: "nat => int => code_numeral => bool"
   4.125 +where
   4.126 +  "JamesBond 0 0 7"
   4.127 +
   4.128 +code_pred JamesBond .
   4.129 +
   4.130 +values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
   4.131 +values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
   4.132 +values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
   4.133 +values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
   4.134 +values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
   4.135 +values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
   4.136 +
   4.137 +values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
   4.138 +values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
   4.139 +values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
   4.140 +
   4.141 +
   4.142 +subsection {* Alternative Rules *}
   4.143 +
   4.144 +datatype char = C | D | E | F | G | H
   4.145 +
   4.146 +inductive is_C_or_D
   4.147 +where
   4.148 +  "(x = C) \<or> (x = D) ==> is_C_or_D x"
   4.149 +
   4.150 +code_pred (expected_modes: i => bool) is_C_or_D .
   4.151 +thm is_C_or_D.equation
   4.152 +
   4.153 +inductive is_D_or_E
   4.154 +where
   4.155 +  "(x = D) \<or> (x = E) ==> is_D_or_E x"
   4.156 +
   4.157 +lemma [code_pred_intro]:
   4.158 +  "is_D_or_E D"
   4.159 +by (auto intro: is_D_or_E.intros)
   4.160 +
   4.161 +lemma [code_pred_intro]:
   4.162 +  "is_D_or_E E"
   4.163 +by (auto intro: is_D_or_E.intros)
   4.164 +
   4.165 +code_pred (expected_modes: o => bool, i => bool) is_D_or_E
   4.166 +proof -
   4.167 +  case is_D_or_E
   4.168 +  from is_D_or_E.prems show thesis
   4.169 +  proof 
   4.170 +    fix xa
   4.171 +    assume x: "x = xa"
   4.172 +    assume "xa = D \<or> xa = E"
   4.173 +    from this show thesis
   4.174 +    proof
   4.175 +      assume "xa = D" from this x is_D_or_E(1) show thesis by simp
   4.176 +    next
   4.177 +      assume "xa = E" from this x is_D_or_E(2) show thesis by simp
   4.178 +    qed
   4.179 +  qed
   4.180 +qed
   4.181 +
   4.182 +thm is_D_or_E.equation
   4.183 +
   4.184 +inductive is_F_or_G
   4.185 +where
   4.186 +  "x = F \<or> x = G ==> is_F_or_G x"
   4.187 +
   4.188 +lemma [code_pred_intro]:
   4.189 +  "is_F_or_G F"
   4.190 +by (auto intro: is_F_or_G.intros)
   4.191 +
   4.192 +lemma [code_pred_intro]:
   4.193 +  "is_F_or_G G"
   4.194 +by (auto intro: is_F_or_G.intros)
   4.195 +
   4.196 +inductive is_FGH
   4.197 +where
   4.198 +  "is_F_or_G x ==> is_FGH x"
   4.199 +| "is_FGH H"
   4.200 +
   4.201 +text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
   4.202 +
   4.203 +code_pred (expected_modes: o => bool, i => bool) is_FGH
   4.204 +proof -
   4.205 +  case is_F_or_G
   4.206 +  from is_F_or_G.prems show thesis
   4.207 +  proof
   4.208 +    fix xa
   4.209 +    assume x: "x = xa"
   4.210 +    assume "xa = F \<or> xa = G"
   4.211 +    from this show thesis
   4.212 +    proof
   4.213 +      assume "xa = F"
   4.214 +      from this x is_F_or_G(1) show thesis by simp
   4.215 +    next
   4.216 +      assume "xa = G"
   4.217 +      from this x is_F_or_G(2) show thesis by simp
   4.218 +    qed
   4.219 +  qed
   4.220 +qed
   4.221 +
   4.222 +subsection {* Named alternative rules *}
   4.223 +
   4.224 +inductive appending
   4.225 +where
   4.226 +  nil: "appending [] ys ys"
   4.227 +| cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
   4.228 +
   4.229 +lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
   4.230 +by (auto intro: appending.intros)
   4.231 +
   4.232 +lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
   4.233 +by (auto intro: appending.intros)
   4.234 +
   4.235 +text {* With code_pred_intro, we can give fact names to the alternative rules,
   4.236 +  which are used for the code_pred command. *}
   4.237 +
   4.238 +declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
   4.239 + 
   4.240 +code_pred appending
   4.241 +proof -
   4.242 +  case appending
   4.243 +  from appending.prems show thesis
   4.244 +  proof(cases)
   4.245 +    case nil
   4.246 +    from alt_nil nil show thesis by auto
   4.247 +  next
   4.248 +    case cons
   4.249 +    from alt_cons cons show thesis by fastsimp
   4.250 +  qed
   4.251 +qed
   4.252 +
   4.253 +
   4.254 +inductive ya_even and ya_odd :: "nat => bool"
   4.255 +where
   4.256 +  even_zero: "ya_even 0"
   4.257 +| odd_plus1: "ya_even x ==> ya_odd (x + 1)"
   4.258 +| even_plus1: "ya_odd x ==> ya_even (x + 1)"
   4.259 +
   4.260 +
   4.261 +declare even_zero[code_pred_intro even_0]
   4.262 +
   4.263 +lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
   4.264 +by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   4.265 +
   4.266 +lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
   4.267 +by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
   4.268 +
   4.269 +code_pred ya_even
   4.270 +proof -
   4.271 +  case ya_even
   4.272 +  from ya_even.prems show thesis
   4.273 +  proof (cases)
   4.274 +    case even_zero
   4.275 +    from even_zero even_0 show thesis by simp
   4.276 +  next
   4.277 +    case even_plus1
   4.278 +    from even_plus1 even_Suc show thesis by simp
   4.279 +  qed
   4.280 +next
   4.281 +  case ya_odd
   4.282 +  from ya_odd.prems show thesis
   4.283 +  proof (cases)
   4.284 +    case odd_plus1
   4.285 +    from odd_plus1 odd_Suc show thesis by simp
   4.286 +  qed
   4.287 +qed
   4.288 +
   4.289 +subsection {* Preprocessor Inlining  *}
   4.290 +
   4.291 +definition "equals == (op =)"
   4.292 + 
   4.293 +inductive zerozero' :: "nat * nat => bool" where
   4.294 +  "equals (x, y) (0, 0) ==> zerozero' (x, y)"
   4.295 +
   4.296 +code_pred (expected_modes: i => bool) zerozero' .
   4.297 +
   4.298 +lemma zerozero'_eq: "zerozero' x == zerozero x"
   4.299 +proof -
   4.300 +  have "zerozero' = zerozero"
   4.301 +    apply (auto simp add: mem_def)
   4.302 +    apply (cases rule: zerozero'.cases)
   4.303 +    apply (auto simp add: equals_def intro: zerozero.intros)
   4.304 +    apply (cases rule: zerozero.cases)
   4.305 +    apply (auto simp add: equals_def intro: zerozero'.intros)
   4.306 +    done
   4.307 +  from this show "zerozero' x == zerozero x" by auto
   4.308 +qed
   4.309 +
   4.310 +declare zerozero'_eq [code_pred_inline]
   4.311 +
   4.312 +definition "zerozero'' x == zerozero' x"
   4.313 +
   4.314 +text {* if preprocessing fails, zerozero'' will not have all modes. *}
   4.315 +
   4.316 +code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
   4.317 +
   4.318 +subsection {* Sets and Numerals *}
   4.319 +
   4.320 +definition
   4.321 +  "one_or_two = {Suc 0, (Suc (Suc 0))}"
   4.322 +
   4.323 +code_pred [inductify] one_or_two .
   4.324 +
   4.325 +code_pred [dseq] one_or_two .
   4.326 +code_pred [random_dseq] one_or_two .
   4.327 +thm one_or_two.dseq_equation
   4.328 +values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
   4.329 +values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
   4.330 +
   4.331 +inductive one_or_two' :: "nat => bool"
   4.332 +where
   4.333 +  "one_or_two' 1"
   4.334 +| "one_or_two' 2"
   4.335 +
   4.336 +code_pred one_or_two' .
   4.337 +thm one_or_two'.equation
   4.338 +
   4.339 +values "{x. one_or_two' x}"
   4.340 +
   4.341 +definition one_or_two'':
   4.342 +  "one_or_two'' == {1, (2::nat)}"
   4.343 +
   4.344 +code_pred [inductify] one_or_two'' .
   4.345 +thm one_or_two''.equation
   4.346 +
   4.347 +values "{x. one_or_two'' x}"
   4.348 +
   4.349 +subsection {* even predicate *}
   4.350 +
   4.351 +inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
   4.352 +    "even 0"
   4.353 +  | "even n \<Longrightarrow> odd (Suc n)"
   4.354 +  | "odd n \<Longrightarrow> even (Suc n)"
   4.355 +
   4.356 +code_pred (expected_modes: i => bool, o => bool) even .
   4.357 +code_pred [dseq] even .
   4.358 +code_pred [random_dseq] even .
   4.359 +
   4.360 +thm odd.equation
   4.361 +thm even.equation
   4.362 +thm odd.dseq_equation
   4.363 +thm even.dseq_equation
   4.364 +thm odd.random_dseq_equation
   4.365 +thm even.random_dseq_equation
   4.366 +
   4.367 +values "{x. even 2}"
   4.368 +values "{x. odd 2}"
   4.369 +values 10 "{n. even n}"
   4.370 +values 10 "{n. odd n}"
   4.371 +values [expected "{}" dseq 2] "{x. even 6}"
   4.372 +values [expected "{}" dseq 6] "{x. even 6}"
   4.373 +values [expected "{()}" dseq 7] "{x. even 6}"
   4.374 +values [dseq 2] "{x. odd 7}"
   4.375 +values [dseq 6] "{x. odd 7}"
   4.376 +values [dseq 7] "{x. odd 7}"
   4.377 +values [expected "{()}" dseq 8] "{x. odd 7}"
   4.378 +
   4.379 +values [expected "{}" dseq 0] 8 "{x. even x}"
   4.380 +values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
   4.381 +values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
   4.382 +values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
   4.383 +values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
   4.384 +
   4.385 +values [random_dseq 1, 1, 0] 8 "{x. even x}"
   4.386 +values [random_dseq 1, 1, 1] 8 "{x. even x}"
   4.387 +values [random_dseq 1, 1, 2] 8 "{x. even x}"
   4.388 +values [random_dseq 1, 1, 3] 8 "{x. even x}"
   4.389 +values [random_dseq 1, 1, 6] 8 "{x. even x}"
   4.390 +
   4.391 +values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
   4.392 +values [random_dseq 1, 1, 8] "{x. odd 7}"
   4.393 +values [random_dseq 1, 1, 9] "{x. odd 7}"
   4.394 +
   4.395 +definition odd' where "odd' x == \<not> even x"
   4.396 +
   4.397 +code_pred (expected_modes: i => bool) [inductify] odd' .
   4.398 +code_pred [dseq inductify] odd' .
   4.399 +code_pred [random_dseq inductify] odd' .
   4.400 +
   4.401 +values [expected "{}" dseq 2] "{x. odd' 7}"
   4.402 +values [expected "{()}" dseq 9] "{x. odd' 7}"
   4.403 +values [expected "{}" dseq 2] "{x. odd' 8}"
   4.404 +values [expected "{}" dseq 10] "{x. odd' 8}"
   4.405 +
   4.406 +
   4.407 +inductive is_even :: "nat \<Rightarrow> bool"
   4.408 +where
   4.409 +  "n mod 2 = 0 \<Longrightarrow> is_even n"
   4.410 +
   4.411 +code_pred (expected_modes: i => bool) is_even .
   4.412 +
   4.413 +subsection {* append predicate *}
   4.414 +
   4.415 +inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   4.416 +    "append [] xs xs"
   4.417 +  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
   4.418 +
   4.419 +code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
   4.420 +  i => o => i => bool as suffix, i => i => i => bool) append .
   4.421 +code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix,
   4.422 +  i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
   4.423 +
   4.424 +code_pred [dseq] append .
   4.425 +code_pred [random_dseq] append .
   4.426 +
   4.427 +thm append.equation
   4.428 +thm append.dseq_equation
   4.429 +thm append.random_dseq_equation
   4.430 +
   4.431 +values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
   4.432 +values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
   4.433 +values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
   4.434 +
   4.435 +values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   4.436 +values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   4.437 +values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   4.438 +values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   4.439 +values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
   4.440 +values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   4.441 +values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   4.442 +values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   4.443 +values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   4.444 +values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
   4.445 +
   4.446 +value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
   4.447 +value [code] "Predicate.the (slice ([]::int list))"
   4.448 +
   4.449 +
   4.450 +text {* tricky case with alternative rules *}
   4.451 +
   4.452 +inductive append2
   4.453 +where
   4.454 +  "append2 [] xs xs"
   4.455 +| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
   4.456 +
   4.457 +lemma append2_Nil: "append2 [] (xs::'b list) xs"
   4.458 +  by (simp add: append2.intros(1))
   4.459 +
   4.460 +lemmas [code_pred_intro] = append2_Nil append2.intros(2)
   4.461 +
   4.462 +code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
   4.463 +  i => o => i => bool, i => i => i => bool) append2
   4.464 +proof -
   4.465 +  case append2
   4.466 +  from append2.prems show thesis
   4.467 +  proof
   4.468 +    fix xs
   4.469 +    assume "xa = []" "xb = xs" "xc = xs"
   4.470 +    from this append2(1) show thesis by simp
   4.471 +  next
   4.472 +    fix xs ys zs x
   4.473 +    assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
   4.474 +    from this append2(2) show thesis by fastsimp
   4.475 +  qed
   4.476 +qed
   4.477 +
   4.478 +inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   4.479 +where
   4.480 +  "tupled_append ([], xs, xs)"
   4.481 +| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
   4.482 +
   4.483 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   4.484 +  i * o * i => bool, i * i * i => bool) tupled_append .
   4.485 +
   4.486 +code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool,
   4.487 +  i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
   4.488 +
   4.489 +code_pred [random_dseq] tupled_append .
   4.490 +thm tupled_append.equation
   4.491 +
   4.492 +values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
   4.493 +
   4.494 +inductive tupled_append'
   4.495 +where
   4.496 +"tupled_append' ([], xs, xs)"
   4.497 +| "[| ys = fst (xa, y); x # zs = snd (xa, y);
   4.498 + tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
   4.499 +
   4.500 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   4.501 +  i * o * i => bool, i * i * i => bool) tupled_append' .
   4.502 +thm tupled_append'.equation
   4.503 +
   4.504 +inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   4.505 +where
   4.506 +  "tupled_append'' ([], xs, xs)"
   4.507 +| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
   4.508 +
   4.509 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   4.510 +  i * o * i => bool, i * i * i => bool) tupled_append'' .
   4.511 +thm tupled_append''.equation
   4.512 +
   4.513 +inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
   4.514 +where
   4.515 +  "tupled_append''' ([], xs, xs)"
   4.516 +| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
   4.517 +
   4.518 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   4.519 +  i * o * i => bool, i * i * i => bool) tupled_append''' .
   4.520 +thm tupled_append'''.equation
   4.521 +
   4.522 +subsection {* map_ofP predicate *}
   4.523 +
   4.524 +inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   4.525 +where
   4.526 +  "map_ofP ((a, b)#xs) a b"
   4.527 +| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
   4.528 +
   4.529 +code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
   4.530 +thm map_ofP.equation
   4.531 +
   4.532 +subsection {* filter predicate *}
   4.533 +
   4.534 +inductive filter1
   4.535 +for P
   4.536 +where
   4.537 +  "filter1 P [] []"
   4.538 +| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
   4.539 +| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
   4.540 +
   4.541 +code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
   4.542 +code_pred [dseq] filter1 .
   4.543 +code_pred [random_dseq] filter1 .
   4.544 +
   4.545 +thm filter1.equation
   4.546 +
   4.547 +values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   4.548 +values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   4.549 +values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
   4.550 +
   4.551 +inductive filter2
   4.552 +where
   4.553 +  "filter2 P [] []"
   4.554 +| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
   4.555 +| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
   4.556 +
   4.557 +code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
   4.558 +code_pred [dseq] filter2 .
   4.559 +code_pred [random_dseq] filter2 .
   4.560 +
   4.561 +thm filter2.equation
   4.562 +thm filter2.random_dseq_equation
   4.563 +
   4.564 +inductive filter3
   4.565 +for P
   4.566 +where
   4.567 +  "List.filter P xs = ys ==> filter3 P xs ys"
   4.568 +
   4.569 +code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 .
   4.570 +
   4.571 +code_pred filter3 .
   4.572 +thm filter3.equation
   4.573 +
   4.574 +(*
   4.575 +inductive filter4
   4.576 +where
   4.577 +  "List.filter P xs = ys ==> filter4 P xs ys"
   4.578 +
   4.579 +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
   4.580 +(*code_pred [depth_limited] filter4 .*)
   4.581 +(*code_pred [random] filter4 .*)
   4.582 +*)
   4.583 +subsection {* reverse predicate *}
   4.584 +
   4.585 +inductive rev where
   4.586 +    "rev [] []"
   4.587 +  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
   4.588 +
   4.589 +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
   4.590 +
   4.591 +thm rev.equation
   4.592 +
   4.593 +values "{xs. rev [0, 1, 2, 3::nat] xs}"
   4.594 +
   4.595 +inductive tupled_rev where
   4.596 +  "tupled_rev ([], [])"
   4.597 +| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
   4.598 +
   4.599 +code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
   4.600 +thm tupled_rev.equation
   4.601 +
   4.602 +subsection {* partition predicate *}
   4.603 +
   4.604 +inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   4.605 +  for f where
   4.606 +    "partition f [] [] []"
   4.607 +  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   4.608 +  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
   4.609 +
   4.610 +code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
   4.611 +  (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
   4.612 +  partition .
   4.613 +code_pred [dseq] partition .
   4.614 +code_pred [random_dseq] partition .
   4.615 +
   4.616 +values 10 "{(ys, zs). partition is_even
   4.617 +  [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
   4.618 +values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
   4.619 +values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
   4.620 +
   4.621 +inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
   4.622 +  for f where
   4.623 +   "tupled_partition f ([], [], [])"
   4.624 +  | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
   4.625 +  | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
   4.626 +
   4.627 +code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
   4.628 +  (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
   4.629 +
   4.630 +thm tupled_partition.equation
   4.631 +
   4.632 +lemma [code_pred_intro]:
   4.633 +  "r a b \<Longrightarrow> tranclp r a b"
   4.634 +  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   4.635 +  by auto
   4.636 +
   4.637 +subsection {* transitive predicate *}
   4.638 +
   4.639 +text {* Also look at the tabled transitive closure in the Library *}
   4.640 +
   4.641 +code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
   4.642 +  (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
   4.643 +  (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
   4.644 +proof -
   4.645 +  case tranclp
   4.646 +  from this converse_tranclpE[OF tranclp.prems] show thesis by metis
   4.647 +qed
   4.648 +
   4.649 +
   4.650 +code_pred [dseq] tranclp .
   4.651 +code_pred [random_dseq] tranclp .
   4.652 +thm tranclp.equation
   4.653 +thm tranclp.random_dseq_equation
   4.654 +
   4.655 +inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
   4.656 +where
   4.657 +  "rtrancl' x x r"
   4.658 +| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
   4.659 +
   4.660 +code_pred [random_dseq] rtrancl' .
   4.661 +
   4.662 +thm rtrancl'.random_dseq_equation
   4.663 +
   4.664 +inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  
   4.665 +where
   4.666 +  "rtrancl'' (x, x, r)"
   4.667 +| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
   4.668 +
   4.669 +code_pred rtrancl'' .
   4.670 +
   4.671 +inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
   4.672 +where
   4.673 +  "rtrancl''' (x, (x, x), r)"
   4.674 +| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
   4.675 +
   4.676 +code_pred rtrancl''' .
   4.677 +
   4.678 +
   4.679 +inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   4.680 +    "succ 0 1"
   4.681 +  | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
   4.682 +
   4.683 +code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
   4.684 +code_pred [random_dseq] succ .
   4.685 +thm succ.equation
   4.686 +thm succ.random_dseq_equation
   4.687 +
   4.688 +values 10 "{(m, n). succ n m}"
   4.689 +values "{m. succ 0 m}"
   4.690 +values "{m. succ m 0}"
   4.691 +
   4.692 +text {* values command needs mode annotation of the parameter succ
   4.693 +to disambiguate which mode is to be chosen. *} 
   4.694 +
   4.695 +values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
   4.696 +values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
   4.697 +values 20 "{(n, m). tranclp succ n m}"
   4.698 +
   4.699 +inductive example_graph :: "int => int => bool"
   4.700 +where
   4.701 +  "example_graph 0 1"
   4.702 +| "example_graph 1 2"
   4.703 +| "example_graph 1 3"
   4.704 +| "example_graph 4 7"
   4.705 +| "example_graph 4 5"
   4.706 +| "example_graph 5 6"
   4.707 +| "example_graph 7 6"
   4.708 +| "example_graph 7 8"
   4.709 + 
   4.710 +inductive not_reachable_in_example_graph :: "int => int => bool"
   4.711 +where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
   4.712 +
   4.713 +code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
   4.714 +
   4.715 +thm not_reachable_in_example_graph.equation
   4.716 +thm tranclp.equation
   4.717 +value "not_reachable_in_example_graph 0 3"
   4.718 +value "not_reachable_in_example_graph 4 8"
   4.719 +value "not_reachable_in_example_graph 5 6"
   4.720 +text {* rtrancl compilation is strange! *}
   4.721 +(*
   4.722 +value "not_reachable_in_example_graph 0 4"
   4.723 +value "not_reachable_in_example_graph 1 6"
   4.724 +value "not_reachable_in_example_graph 8 4"*)
   4.725 +
   4.726 +code_pred [dseq] not_reachable_in_example_graph .
   4.727 +
   4.728 +values [dseq 6] "{x. tranclp example_graph 0 3}"
   4.729 +
   4.730 +values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
   4.731 +values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
   4.732 +values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
   4.733 +values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
   4.734 +values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
   4.735 +values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
   4.736 +
   4.737 +
   4.738 +inductive not_reachable_in_example_graph' :: "int => int => bool"
   4.739 +where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
   4.740 +
   4.741 +code_pred not_reachable_in_example_graph' .
   4.742 +
   4.743 +value "not_reachable_in_example_graph' 0 3"
   4.744 +(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
   4.745 +
   4.746 +
   4.747 +(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   4.748 +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   4.749 +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
   4.750 +(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   4.751 +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   4.752 +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   4.753 +
   4.754 +code_pred [dseq] not_reachable_in_example_graph' .
   4.755 +
   4.756 +(*thm not_reachable_in_example_graph'.dseq_equation*)
   4.757 +
   4.758 +(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
   4.759 +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
   4.760 +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
   4.761 +values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
   4.762 +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   4.763 +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
   4.764 +
   4.765 +subsection {* Free function variable *}
   4.766 +
   4.767 +inductive FF :: "nat => nat => bool"
   4.768 +where
   4.769 +  "f x = y ==> FF x y"
   4.770 +
   4.771 +code_pred FF .
   4.772 +
   4.773 +subsection {* IMP *}
   4.774 +
   4.775 +types
   4.776 +  var = nat
   4.777 +  state = "int list"
   4.778 +
   4.779 +datatype com =
   4.780 +  Skip |
   4.781 +  Ass var "state => int" |
   4.782 +  Seq com com |
   4.783 +  IF "state => bool" com com |
   4.784 +  While "state => bool" com
   4.785 +
   4.786 +inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
   4.787 +"tupled_exec (Skip, s, s)" |
   4.788 +"tupled_exec (Ass x e, s, s[x := e(s)])" |
   4.789 +"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
   4.790 +"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   4.791 +"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
   4.792 +"~b s ==> tupled_exec (While b c, s, s)" |
   4.793 +"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
   4.794 +
   4.795 +code_pred tupled_exec .
   4.796 +
   4.797 +values "{s. tupled_exec (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))), [3, 5], s)}"
   4.798 +
   4.799 +subsection {* CCS *}
   4.800 +
   4.801 +text{* This example formalizes finite CCS processes without communication or
   4.802 +recursion. For simplicity, labels are natural numbers. *}
   4.803 +
   4.804 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
   4.805 +
   4.806 +inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
   4.807 +where
   4.808 +"tupled_step (pre n p, n, p)" |
   4.809 +"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   4.810 +"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
   4.811 +"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
   4.812 +"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
   4.813 +
   4.814 +code_pred tupled_step .
   4.815 +thm tupled_step.equation
   4.816 +
   4.817 +subsection {* divmod *}
   4.818 +
   4.819 +inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   4.820 +    "k < l \<Longrightarrow> divmod_rel k l 0 k"
   4.821 +  | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
   4.822 +
   4.823 +code_pred divmod_rel .
   4.824 +thm divmod_rel.equation
   4.825 +value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
   4.826 +
   4.827 +subsection {* Transforming predicate logic into logic programs *}
   4.828 +
   4.829 +subsection {* Transforming functions into logic programs *}
   4.830 +definition
   4.831 +  "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
   4.832 +
   4.833 +code_pred [inductify, skip_proof] case_f .
   4.834 +thm case_fP.equation
   4.835 +
   4.836 +fun fold_map_idx where
   4.837 +  "fold_map_idx f i y [] = (y, [])"
   4.838 +| "fold_map_idx f i y (x # xs) =
   4.839 + (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
   4.840 + in (y'', x' # xs'))"
   4.841 +
   4.842 +code_pred [inductify] fold_map_idx .
   4.843 +
   4.844 +subsection {* Minimum *}
   4.845 +
   4.846 +definition Min
   4.847 +where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
   4.848 +
   4.849 +code_pred [inductify] Min .
   4.850 +thm Min.equation
   4.851 +
   4.852 +subsection {* Lexicographic order *}
   4.853 +
   4.854 +declare lexord_def[code_pred_def]
   4.855 +code_pred [inductify] lexord .
   4.856 +code_pred [random_dseq inductify] lexord .
   4.857 +
   4.858 +thm lexord.equation
   4.859 +thm lexord.random_dseq_equation
   4.860 +
   4.861 +inductive less_than_nat :: "nat * nat => bool"
   4.862 +where
   4.863 +  "less_than_nat (0, x)"
   4.864 +| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
   4.865 + 
   4.866 +code_pred less_than_nat .
   4.867 +
   4.868 +code_pred [dseq] less_than_nat .
   4.869 +code_pred [random_dseq] less_than_nat .
   4.870 +
   4.871 +inductive test_lexord :: "nat list * nat list => bool"
   4.872 +where
   4.873 +  "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
   4.874 +
   4.875 +code_pred test_lexord .
   4.876 +code_pred [dseq] test_lexord .
   4.877 +code_pred [random_dseq] test_lexord .
   4.878 +thm test_lexord.dseq_equation
   4.879 +thm test_lexord.random_dseq_equation
   4.880 +
   4.881 +values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
   4.882 +(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
   4.883 +
   4.884 +lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
   4.885 +(*
   4.886 +code_pred [inductify] lexn .
   4.887 +thm lexn.equation
   4.888 +*)
   4.889 +(*
   4.890 +code_pred [random_dseq inductify] lexn .
   4.891 +thm lexn.random_dseq_equation
   4.892 +
   4.893 +values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   4.894 +*)
   4.895 +inductive has_length
   4.896 +where
   4.897 +  "has_length [] 0"
   4.898 +| "has_length xs i ==> has_length (x # xs) (Suc i)" 
   4.899 +
   4.900 +lemma has_length:
   4.901 +  "has_length xs n = (length xs = n)"
   4.902 +proof (rule iffI)
   4.903 +  assume "has_length xs n"
   4.904 +  from this show "length xs = n"
   4.905 +    by (rule has_length.induct) auto
   4.906 +next
   4.907 +  assume "length xs = n"
   4.908 +  from this show "has_length xs n"
   4.909 +    by (induct xs arbitrary: n) (auto intro: has_length.intros)
   4.910 +qed
   4.911 +
   4.912 +lemma lexn_intros [code_pred_intro]:
   4.913 +  "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
   4.914 +  "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
   4.915 +proof -
   4.916 +  assume "has_length xs i" "has_length ys i" "r (x, y)"
   4.917 +  from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
   4.918 +    unfolding lexn_conv Collect_def mem_def
   4.919 +    by fastsimp
   4.920 +next
   4.921 +  assume "lexn r i (xs, ys)"
   4.922 +  thm lexn_conv
   4.923 +  from this show "lexn r (Suc i) (x#xs, x#ys)"
   4.924 +    unfolding Collect_def mem_def lexn_conv
   4.925 +    apply auto
   4.926 +    apply (rule_tac x="x # xys" in exI)
   4.927 +    by auto
   4.928 +qed
   4.929 +
   4.930 +code_pred [random_dseq] lexn
   4.931 +proof -
   4.932 +  fix r n xs ys
   4.933 +  assume 1: "lexn r n (xs, ys)"
   4.934 +  assume 2: "\<And>r' i x xs' y ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r' (x, y) ==> thesis"
   4.935 +  assume 3: "\<And>r' i x xs' ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r' i (xs', ys') ==> thesis"
   4.936 +  from 1 2 3 show thesis
   4.937 +    unfolding lexn_conv Collect_def mem_def
   4.938 +    apply (auto simp add: has_length)
   4.939 +    apply (case_tac xys)
   4.940 +    apply auto
   4.941 +    apply fastsimp
   4.942 +    apply fastsimp done
   4.943 +qed
   4.944 +
   4.945 +values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
   4.946 +
   4.947 +code_pred [inductify, skip_proof] lex .
   4.948 +thm lex.equation
   4.949 +thm lex_def
   4.950 +declare lenlex_conv[code_pred_def]
   4.951 +code_pred [inductify, skip_proof] lenlex .
   4.952 +thm lenlex.equation
   4.953 +
   4.954 +code_pred [random_dseq inductify] lenlex .
   4.955 +thm lenlex.random_dseq_equation
   4.956 +
   4.957 +values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
   4.958 +
   4.959 +thm lists.intros
   4.960 +code_pred [inductify] lists .
   4.961 +thm lists.equation
   4.962 +
   4.963 +subsection {* AVL Tree *}
   4.964 +
   4.965 +datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
   4.966 +fun height :: "'a tree => nat" where
   4.967 +"height ET = 0"
   4.968 +| "height (MKT x l r h) = max (height l) (height r) + 1"
   4.969 +
   4.970 +primrec avl :: "'a tree => bool"
   4.971 +where
   4.972 +  "avl ET = True"
   4.973 +| "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
   4.974 +  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
   4.975 +(*
   4.976 +code_pred [inductify] avl .
   4.977 +thm avl.equation*)
   4.978 +
   4.979 +code_pred [new_random_dseq inductify] avl .
   4.980 +thm avl.new_random_dseq_equation
   4.981 +
   4.982 +values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
   4.983 +
   4.984 +fun set_of
   4.985 +where
   4.986 +"set_of ET = {}"
   4.987 +| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
   4.988 +
   4.989 +fun is_ord :: "nat tree => bool"
   4.990 +where
   4.991 +"is_ord ET = True"
   4.992 +| "is_ord (MKT n l r h) =
   4.993 + ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
   4.994 +
   4.995 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
   4.996 +thm set_of.equation
   4.997 +
   4.998 +code_pred (expected_modes: i => bool) [inductify] is_ord .
   4.999 +thm is_ord_aux.equation
  4.1000 +thm is_ord.equation
  4.1001 +
  4.1002 +subsection {* Definitions about Relations *}
  4.1003 +
  4.1004 +term "converse"
  4.1005 +code_pred (modes:
  4.1006 +  (i * i => bool) => i * i => bool,
  4.1007 +  (i * o => bool) => o * i => bool,
  4.1008 +  (i * o => bool) => i * i => bool,
  4.1009 +  (o * i => bool) => i * o => bool,
  4.1010 +  (o * i => bool) => i * i => bool,
  4.1011 +  (o * o => bool) => o * o => bool,
  4.1012 +  (o * o => bool) => i * o => bool,
  4.1013 +  (o * o => bool) => o * i => bool,
  4.1014 +  (o * o => bool) => i * i => bool) [inductify] converse .
  4.1015 +
  4.1016 +thm converse.equation
  4.1017 +code_pred [inductify] rel_comp .
  4.1018 +thm rel_comp.equation
  4.1019 +code_pred [inductify] Image .
  4.1020 +thm Image.equation
  4.1021 +declare singleton_iff[code_pred_inline]
  4.1022 +declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
  4.1023 +
  4.1024 +code_pred (expected_modes:
  4.1025 +  (o => bool) => o => bool,
  4.1026 +  (o => bool) => i * o => bool,
  4.1027 +  (o => bool) => o * i => bool,
  4.1028 +  (o => bool) => i => bool,
  4.1029 +  (i => bool) => i * o => bool,
  4.1030 +  (i => bool) => o * i => bool,
  4.1031 +  (i => bool) => i => bool) [inductify] Id_on .
  4.1032 +thm Id_on.equation
  4.1033 +thm Domain_def
  4.1034 +code_pred (modes:
  4.1035 +  (o * o => bool) => o => bool,
  4.1036 +  (o * o => bool) => i => bool,
  4.1037 +  (i * o => bool) => i => bool) [inductify] Domain .
  4.1038 +thm Domain.equation
  4.1039 +
  4.1040 +thm Range_def
  4.1041 +code_pred (modes:
  4.1042 +  (o * o => bool) => o => bool,
  4.1043 +  (o * o => bool) => i => bool,
  4.1044 +  (o * i => bool) => i => bool) [inductify] Range .
  4.1045 +thm Range.equation
  4.1046 +
  4.1047 +code_pred [inductify] Field .
  4.1048 +thm Field.equation
  4.1049 +
  4.1050 +thm refl_on_def
  4.1051 +code_pred [inductify] refl_on .
  4.1052 +thm refl_on.equation
  4.1053 +code_pred [inductify] total_on .
  4.1054 +thm total_on.equation
  4.1055 +code_pred [inductify] antisym .
  4.1056 +thm antisym.equation
  4.1057 +code_pred [inductify] trans .
  4.1058 +thm trans.equation
  4.1059 +code_pred [inductify] single_valued .
  4.1060 +thm single_valued.equation
  4.1061 +thm inv_image_def
  4.1062 +code_pred [inductify] inv_image .
  4.1063 +thm inv_image.equation
  4.1064 +
  4.1065 +subsection {* Inverting list functions *}
  4.1066 +
  4.1067 +code_pred [inductify] size_list .
  4.1068 +code_pred [new_random_dseq inductify] size_list .
  4.1069 +thm size_listP.equation
  4.1070 +thm size_listP.new_random_dseq_equation
  4.1071 +
  4.1072 +values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
  4.1073 +
  4.1074 +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
  4.1075 +thm concatP.equation
  4.1076 +
  4.1077 +values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
  4.1078 +values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
  4.1079 +
  4.1080 +code_pred [dseq inductify] List.concat .
  4.1081 +thm concatP.dseq_equation
  4.1082 +
  4.1083 +values [dseq 3] 3
  4.1084 +  "{xs. concatP xs ([0] :: nat list)}"
  4.1085 +
  4.1086 +values [dseq 5] 3
  4.1087 +  "{xs. concatP xs ([1] :: int list)}"
  4.1088 +
  4.1089 +values [dseq 5] 3
  4.1090 +  "{xs. concatP xs ([1] :: nat list)}"
  4.1091 +
  4.1092 +values [dseq 5] 3
  4.1093 +  "{xs. concatP xs [(1::int), 2]}"
  4.1094 +
  4.1095 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
  4.1096 +thm hdP.equation
  4.1097 +values "{x. hdP [1, 2, (3::int)] x}"
  4.1098 +values "{(xs, x). hdP [1, 2, (3::int)] 1}"
  4.1099 + 
  4.1100 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
  4.1101 +thm tlP.equation
  4.1102 +values "{x. tlP [1, 2, (3::nat)] x}"
  4.1103 +values "{x. tlP [1, 2, (3::int)] [3]}"
  4.1104 +
  4.1105 +code_pred [inductify, skip_proof] last .
  4.1106 +thm lastP.equation
  4.1107 +
  4.1108 +code_pred [inductify, skip_proof] butlast .
  4.1109 +thm butlastP.equation
  4.1110 +
  4.1111 +code_pred [inductify, skip_proof] take .
  4.1112 +thm takeP.equation
  4.1113 +
  4.1114 +code_pred [inductify, skip_proof] drop .
  4.1115 +thm dropP.equation
  4.1116 +code_pred [inductify, skip_proof] zip .
  4.1117 +thm zipP.equation
  4.1118 +
  4.1119 +code_pred [inductify, skip_proof] upt .
  4.1120 +code_pred [inductify, skip_proof] remdups .
  4.1121 +thm remdupsP.equation
  4.1122 +code_pred [dseq inductify] remdups .
  4.1123 +values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
  4.1124 +
  4.1125 +code_pred [inductify, skip_proof] remove1 .
  4.1126 +thm remove1P.equation
  4.1127 +values "{xs. remove1P 1 xs [2, (3::int)]}"
  4.1128 +
  4.1129 +code_pred [inductify, skip_proof] removeAll .
  4.1130 +thm removeAllP.equation
  4.1131 +code_pred [dseq inductify] removeAll .
  4.1132 +
  4.1133 +values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
  4.1134 +
  4.1135 +code_pred [inductify] distinct .
  4.1136 +thm distinct.equation
  4.1137 +code_pred [inductify, skip_proof] replicate .
  4.1138 +thm replicateP.equation
  4.1139 +values 5 "{(n, xs). replicateP n (0::int) xs}"
  4.1140 +
  4.1141 +code_pred [inductify, skip_proof] splice .
  4.1142 +thm splice.simps
  4.1143 +thm spliceP.equation
  4.1144 +
  4.1145 +values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
  4.1146 +
  4.1147 +code_pred [inductify, skip_proof] List.rev .
  4.1148 +code_pred [inductify] map .
  4.1149 +code_pred [inductify] foldr .
  4.1150 +code_pred [inductify] foldl .
  4.1151 +code_pred [inductify] filter .
  4.1152 +code_pred [random_dseq inductify] filter .
  4.1153 +
  4.1154 +section {* Function predicate replacement *}
  4.1155 +
  4.1156 +text {*
  4.1157 +If the mode analysis uses the functional mode, we
  4.1158 +replace predicates that resulted from functions again by their functions.
  4.1159 +*}
  4.1160 +
  4.1161 +inductive test_append
  4.1162 +where
  4.1163 +  "List.append xs ys = zs ==> test_append xs ys zs"
  4.1164 +
  4.1165 +code_pred [inductify, skip_proof] test_append .
  4.1166 +thm test_append.equation
  4.1167 +
  4.1168 +text {* If append is not turned into a predicate, then the mode
  4.1169 +  o => o => i => bool could not be inferred. *}
  4.1170 +
  4.1171 +values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
  4.1172 +
  4.1173 +text {* If appendP is not reverted back to a function, then mode i => i => o => bool
  4.1174 +  fails after deleting the predicate equation. *}
  4.1175 +
  4.1176 +declare appendP.equation[code del]
  4.1177 +
  4.1178 +values "{xs::int list. test_append [1,2] [3,4] xs}"
  4.1179 +values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
  4.1180 +values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
  4.1181 +
  4.1182 +text {* Redeclaring append.equation as code equation *}
  4.1183 +
  4.1184 +declare appendP.equation[code]
  4.1185 +
  4.1186 +subsection {* Function with tuples *}
  4.1187 +
  4.1188 +fun append'
  4.1189 +where
  4.1190 +  "append' ([], ys) = ys"
  4.1191 +| "append' (x # xs, ys) = x # append' (xs, ys)"
  4.1192 +
  4.1193 +inductive test_append'
  4.1194 +where
  4.1195 +  "append' (xs, ys) = zs ==> test_append' xs ys zs"
  4.1196 +
  4.1197 +code_pred [inductify, skip_proof] test_append' .
  4.1198 +
  4.1199 +thm test_append'.equation
  4.1200 +
  4.1201 +values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
  4.1202 +
  4.1203 +declare append'P.equation[code del]
  4.1204 +
  4.1205 +values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
  4.1206 +
  4.1207 +section {* Arithmetic examples *}
  4.1208 +
  4.1209 +subsection {* Examples on nat *}
  4.1210 +
  4.1211 +inductive plus_nat_test :: "nat => nat => nat => bool"
  4.1212 +where
  4.1213 +  "x + y = z ==> plus_nat_test x y z"
  4.1214 +
  4.1215 +code_pred [inductify, skip_proof] plus_nat_test .
  4.1216 +code_pred [new_random_dseq inductify] plus_nat_test .
  4.1217 +
  4.1218 +thm plus_nat_test.equation
  4.1219 +thm plus_nat_test.new_random_dseq_equation
  4.1220 +
  4.1221 +values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
  4.1222 +values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
  4.1223 +values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
  4.1224 +values [expected "{}"] "{y. plus_nat_test 9 y 8}"
  4.1225 +values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
  4.1226 +values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
  4.1227 +values [expected "{}"] "{x. plus_nat_test x 9 7}"
  4.1228 +values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
  4.1229 +values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
  4.1230 +values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"]
  4.1231 +  "{(x, y). plus_nat_test x y 5}"
  4.1232 +
  4.1233 +inductive minus_nat_test :: "nat => nat => nat => bool"
  4.1234 +where
  4.1235 +  "x - y = z ==> minus_nat_test x y z"
  4.1236 +
  4.1237 +code_pred [inductify, skip_proof] minus_nat_test .
  4.1238 +code_pred [new_random_dseq inductify] minus_nat_test .
  4.1239 +
  4.1240 +thm minus_nat_test.equation
  4.1241 +thm minus_nat_test.new_random_dseq_equation
  4.1242 +
  4.1243 +values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
  4.1244 +values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
  4.1245 +values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
  4.1246 +values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
  4.1247 +values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}"
  4.1248 +values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
  4.1249 +
  4.1250 +subsection {* Examples on int *}
  4.1251 +
  4.1252 +inductive plus_int_test :: "int => int => int => bool"
  4.1253 +where
  4.1254 +  "a + b = c ==> plus_int_test a b c"
  4.1255 +
  4.1256 +code_pred [inductify, skip_proof] plus_int_test .
  4.1257 +code_pred [new_random_dseq inductify] plus_int_test .
  4.1258 +
  4.1259 +thm plus_int_test.equation
  4.1260 +thm plus_int_test.new_random_dseq_equation
  4.1261 +
  4.1262 +values [expected "{1::int}"] "{a. plus_int_test a 6 7}"
  4.1263 +values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"
  4.1264 +values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"
  4.1265 +
  4.1266 +inductive minus_int_test :: "int => int => int => bool"
  4.1267 +where
  4.1268 +  "a - b = c ==> minus_int_test a b c"
  4.1269 +
  4.1270 +code_pred [inductify, skip_proof] minus_int_test .
  4.1271 +code_pred [new_random_dseq inductify] minus_int_test .
  4.1272 +
  4.1273 +thm minus_int_test.equation
  4.1274 +thm minus_int_test.new_random_dseq_equation
  4.1275 +
  4.1276 +values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
  4.1277 +values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
  4.1278 +values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
  4.1279 +
  4.1280 +subsection {* minus on bool *}
  4.1281 +
  4.1282 +inductive All :: "nat => bool"
  4.1283 +where
  4.1284 +  "All x"
  4.1285 +
  4.1286 +inductive None :: "nat => bool"
  4.1287 +
  4.1288 +definition "test_minus_bool x = (None x - All x)"
  4.1289 +
  4.1290 +code_pred [inductify] test_minus_bool .
  4.1291 +thm test_minus_bool.equation
  4.1292 +
  4.1293 +values "{x. test_minus_bool x}"
  4.1294 +
  4.1295 +subsection {* Functions *}
  4.1296 +
  4.1297 +fun partial_hd :: "'a list => 'a option"
  4.1298 +where
  4.1299 +  "partial_hd [] = Option.None"
  4.1300 +| "partial_hd (x # xs) = Some x"
  4.1301 +
  4.1302 +inductive hd_predicate
  4.1303 +where
  4.1304 +  "partial_hd xs = Some x ==> hd_predicate xs x"
  4.1305 +
  4.1306 +code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
  4.1307 +
  4.1308 +thm hd_predicate.equation
  4.1309 +
  4.1310 +subsection {* Locales *}
  4.1311 +
  4.1312 +inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"
  4.1313 +where
  4.1314 +  "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"
  4.1315 +
  4.1316 +
  4.1317 +thm hd_predicate2.intros
  4.1318 +
  4.1319 +code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
  4.1320 +thm hd_predicate2.equation
  4.1321 +
  4.1322 +locale A = fixes partial_hd :: "'a list => 'a option" begin
  4.1323 +
  4.1324 +inductive hd_predicate_in_locale :: "'a list => 'a => bool"
  4.1325 +where
  4.1326 +  "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
  4.1327 +
  4.1328 +end
  4.1329 +
  4.1330 +text {* The global introduction rules must be redeclared as introduction rules and then 
  4.1331 +  one could invoke code_pred. *}
  4.1332 +
  4.1333 +declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro]
  4.1334 +
  4.1335 +code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
  4.1336 +unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases)
  4.1337 +    
  4.1338 +interpretation A partial_hd .
  4.1339 +thm hd_predicate_in_locale.intros
  4.1340 +text {* A locally compliant solution with a trivial interpretation fails, because
  4.1341 +the predicate compiler has very strict assumptions about the terms and their structure. *}
  4.1342 + 
  4.1343 +(*code_pred hd_predicate_in_locale .*)
  4.1344 +
  4.1345 +section {* Integer example *}
  4.1346 +
  4.1347 +definition three :: int
  4.1348 +where "three = 3"
  4.1349 +
  4.1350 +inductive is_three
  4.1351 +where
  4.1352 +  "is_three three"
  4.1353 +
  4.1354 +code_pred is_three .
  4.1355 +
  4.1356 +thm is_three.equation
  4.1357 +
  4.1358 +section {* String.literal example *}
  4.1359 +
  4.1360 +definition Error_1
  4.1361 +where
  4.1362 +  "Error_1 = STR ''Error 1''"
  4.1363 +
  4.1364 +definition Error_2
  4.1365 +where
  4.1366 +  "Error_2 = STR ''Error 2''"
  4.1367 +
  4.1368 +inductive "is_error" :: "String.literal \<Rightarrow> bool"
  4.1369 +where
  4.1370 +  "is_error Error_1"
  4.1371 +| "is_error Error_2"
  4.1372 +
  4.1373 +code_pred is_error .
  4.1374 +
  4.1375 +thm is_error.equation
  4.1376 +
  4.1377 +inductive is_error' :: "String.literal \<Rightarrow> bool"
  4.1378 +where
  4.1379 +  "is_error' (STR ''Error1'')"
  4.1380 +| "is_error' (STR ''Error2'')"
  4.1381 +
  4.1382 +code_pred is_error' .
  4.1383 +
  4.1384 +thm is_error'.equation
  4.1385 +
  4.1386 +datatype ErrorObject = Error String.literal int
  4.1387 +
  4.1388 +inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
  4.1389 +where
  4.1390 +  "is_error'' (Error Error_1 3)"
  4.1391 +| "is_error'' (Error Error_2 4)"
  4.1392 +
  4.1393 +code_pred is_error'' .
  4.1394 +
  4.1395 +thm is_error''.equation
  4.1396 +
  4.1397 +section {* Another function example *}
  4.1398 +
  4.1399 +consts f :: "'a \<Rightarrow> 'a"
  4.1400 +
  4.1401 +inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
  4.1402 +where
  4.1403 +  "fun_upd ((x, a), s) (s(x := f a))"
  4.1404 +
  4.1405 +code_pred fun_upd .
  4.1406 +
  4.1407 +thm fun_upd.equation
  4.1408 +
  4.1409 +section {* Examples for detecting switches *}
  4.1410 +
  4.1411 +inductive detect_switches1 where
  4.1412 +  "detect_switches1 [] []"
  4.1413 +| "detect_switches1 (x # xs) (y # ys)"
  4.1414 +
  4.1415 +code_pred [detect_switches, skip_proof] detect_switches1 .
  4.1416 +
  4.1417 +thm detect_switches1.equation
  4.1418 +
  4.1419 +inductive detect_switches2 :: "('a => bool) => bool"
  4.1420 +where
  4.1421 +  "detect_switches2 P"
  4.1422 +
  4.1423 +code_pred [detect_switches, skip_proof] detect_switches2 .
  4.1424 +thm detect_switches2.equation
  4.1425 +
  4.1426 +inductive detect_switches3 :: "('a => bool) => 'a list => bool"
  4.1427 +where
  4.1428 +  "detect_switches3 P []"
  4.1429 +| "detect_switches3 P (x # xs)" 
  4.1430 +
  4.1431 +code_pred [detect_switches, skip_proof] detect_switches3 .
  4.1432 +
  4.1433 +thm detect_switches3.equation
  4.1434 +
  4.1435 +inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
  4.1436 +where
  4.1437 +  "detect_switches4 P [] []"
  4.1438 +| "detect_switches4 P (x # xs) (y # ys)"
  4.1439 +
  4.1440 +code_pred [detect_switches, skip_proof] detect_switches4 .
  4.1441 +thm detect_switches4.equation
  4.1442 +
  4.1443 +inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
  4.1444 +where
  4.1445 +  "detect_switches5 P [] []"
  4.1446 +| "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
  4.1447 +
  4.1448 +code_pred [detect_switches, skip_proof] detect_switches5 .
  4.1449 +
  4.1450 +thm detect_switches5.equation
  4.1451 +
  4.1452 +inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
  4.1453 +where
  4.1454 +  "detect_switches6 (P, [], [])"
  4.1455 +| "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
  4.1456 +
  4.1457 +code_pred [detect_switches, skip_proof] detect_switches6 .
  4.1458 +
  4.1459 +inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
  4.1460 +where
  4.1461 +  "detect_switches7 P Q (a, [])"
  4.1462 +| "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
  4.1463 +
  4.1464 +code_pred [skip_proof] detect_switches7 .
  4.1465 +
  4.1466 +thm detect_switches7.equation
  4.1467 +
  4.1468 +inductive detect_switches8 :: "nat => bool"
  4.1469 +where
  4.1470 +  "detect_switches8 0"
  4.1471 +| "x mod 2 = 0 ==> detect_switches8 (Suc x)"
  4.1472 +
  4.1473 +code_pred [detect_switches, skip_proof] detect_switches8 .
  4.1474 +
  4.1475 +thm detect_switches8.equation
  4.1476 +
  4.1477 +inductive detect_switches9 :: "nat => nat => bool"
  4.1478 +where
  4.1479 +  "detect_switches9 0 0"
  4.1480 +| "detect_switches9 0 (Suc x)"
  4.1481 +| "detect_switches9 (Suc x) 0"
  4.1482 +| "x = y ==> detect_switches9 (Suc x) (Suc y)"
  4.1483 +| "c1 = c2 ==> detect_switches9 c1 c2"
  4.1484 +
  4.1485 +code_pred [detect_switches, skip_proof] detect_switches9 .
  4.1486 +
  4.1487 +thm detect_switches9.equation
  4.1488 +
  4.1489 +
  4.1490 +
  4.1491 +end
     5.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Thu Sep 23 14:50:17 2010 +0200
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Thu Sep 23 14:50:18 2010 +0200
     5.3 @@ -1,5 +1,6 @@
     5.4  use_thys [
     5.5 -  "Predicate_Compile_Examples",
     5.6 +  "Examples",
     5.7 +  "Predicate_Compile_Tests",
     5.8    "Predicate_Compile_Quickcheck_Examples",
     5.9    "Specialisation_Examples",
    5.10    "IMP_1",