equal
deleted
inserted
replaced
1 theory Ind_General_Scheme |
1 theory Ind_General_Scheme |
2 imports Simple_Inductive_Package Ind_Prelims |
2 imports Ind_Interface |
3 begin |
3 begin |
4 |
4 |
5 (*<*) |
|
6 datatype trm = |
|
7 Var "string" |
|
8 | App "trm" "trm" |
|
9 | Lam "string" "trm" |
|
10 |
|
11 simple_inductive |
|
12 fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" |
|
13 where |
|
14 fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)" |
|
15 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)" |
|
16 | fresh_lam1: "fresh a (Lam a t)" |
|
17 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |
|
18 (*>*) |
|
19 |
|
20 section {* The Code in a Nutshell\label{sec:nutshell} *} |
5 section {* The Code in a Nutshell\label{sec:nutshell} *} |
|
6 |
|
7 |
21 |
8 |
22 text {* |
9 text {* |
23 The inductive package will generate the reasoning infrastructure for |
10 The inductive package will generate the reasoning infrastructure for |
24 mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
11 mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what |
25 follows we will have the convention that various, possibly empty collections |
12 follows we will have the convention that various, possibly empty collections |