|
10370
|
1 |
(* ID: $Id$ *)
|
|
|
2 |
theory Advanced = Main:
|
|
|
3 |
|
|
|
4 |
datatype 'f "term" = Apply 'f "'f term list"
|
|
|
5 |
|
|
|
6 |
consts terms :: "'f set \<Rightarrow> 'f term set"
|
|
|
7 |
inductive "terms F"
|
|
|
8 |
intros
|
|
|
9 |
step[intro]: "\<lbrakk>\<forall>t \<in> set term_list. t \<in> terms F; f \<in> F\<rbrakk>
|
|
|
10 |
\<Longrightarrow> (Apply f term_list) \<in> terms F"
|
|
|
11 |
|
|
|
12 |
|
|
|
13 |
lemma "F\<subseteq>G \<Longrightarrow> terms F \<subseteq> terms G"
|
|
|
14 |
apply clarify
|
|
|
15 |
apply (erule terms.induct)
|
|
|
16 |
apply blast
|
|
|
17 |
done
|
|
|
18 |
|
|
|
19 |
consts term_type :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f term * 't)set"
|
|
|
20 |
inductive "term_type sig"
|
|
|
21 |
intros
|
|
|
22 |
step[intro]: "\<lbrakk>\<forall>et \<in> set term_type_list. et \<in> term_type sig;
|
|
|
23 |
sig f = (map snd term_type_list, rtype)\<rbrakk>
|
|
|
24 |
\<Longrightarrow> (Apply f (map fst term_type_list), rtype) \<in> term_type sig"
|
|
|
25 |
|
|
|
26 |
consts term_type' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f term * 't)set"
|
|
|
27 |
inductive "term_type' sig"
|
|
|
28 |
intros
|
|
|
29 |
step[intro]: "\<lbrakk>term_type_list \<in> lists(term_type' sig);
|
|
|
30 |
sig f = (map snd term_type_list, rtype)\<rbrakk>
|
|
|
31 |
\<Longrightarrow> (Apply f (map fst term_type_list), rtype) \<in> term_type' sig"
|
|
|
32 |
monos lists_mono
|
|
|
33 |
|
|
|
34 |
|
|
|
35 |
lemma "term_type sig \<subseteq> term_type' sig"
|
|
|
36 |
apply clarify
|
|
|
37 |
apply (erule term_type.induct)
|
|
|
38 |
apply auto
|
|
|
39 |
done
|
|
|
40 |
|
|
|
41 |
lemma "term_type' sig \<subseteq> term_type sig"
|
|
|
42 |
apply clarify
|
|
|
43 |
apply (erule term_type'.induct)
|
|
|
44 |
apply auto
|
|
|
45 |
done
|
|
|
46 |
|
|
|
47 |
end
|
|
|
48 |
|