equal
deleted
inserted
replaced
1 theory Ind_General_Scheme |
1 theory Ind_General_Scheme |
2 imports Ind_Interface |
2 imports "../Base" Simple_Inductive_Package |
3 begin |
3 begin |
4 |
4 |
|
5 (*<*) |
|
6 simple_inductive |
|
7 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
8 where |
|
9 base: "trcl R x x" |
|
10 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z" |
|
11 |
|
12 simple_inductive |
|
13 even and odd |
|
14 where |
|
15 even0: "even 0" |
|
16 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
|
17 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
|
18 |
|
19 simple_inductive |
|
20 accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
|
21 where |
|
22 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
|
23 |
|
24 datatype trm = |
|
25 Var "string" |
|
26 | App "trm" "trm" |
|
27 | Lam "string" "trm" |
|
28 |
|
29 simple_inductive |
|
30 fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" |
|
31 where |
|
32 fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)" |
|
33 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)" |
|
34 | fresh_lam1: "fresh a (Lam a t)" |
|
35 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |
|
36 (*>*) |
|
37 |
|
38 |
5 section {* The Code in a Nutshell\label{sec:nutshell} *} |
39 section {* The Code in a Nutshell\label{sec:nutshell} *} |
6 |
|
7 |
40 |
8 |
41 |
9 text {* |
42 text {* |
10 The inductive package will generate the reasoning infrastructure for |
43 The inductive package will generate the reasoning infrastructure for |
11 mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
44 mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |