1 (* Title: CCL/Hered.thy |
1 (* Title: CCL/Hered.thy |
2 Author: Martin Coen |
2 Author: Martin Coen |
3 Copyright 1993 University of Cambridge |
3 Copyright 1993 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* Hereditary Termination -- cf. Martin Lo\"f *} |
6 section \<open>Hereditary Termination -- cf. Martin Lo\"f\<close> |
7 |
7 |
8 theory Hered |
8 theory Hered |
9 imports Type |
9 imports Type |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text \<open> |
13 Note that this is based on an untyped equality and so @{text "lam |
13 Note that this is based on an untyped equality and so @{text "lam |
14 x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"} |
14 x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"} |
15 is. Not so useful for functions! |
15 is. Not so useful for functions! |
16 *} |
16 \<close> |
17 |
17 |
18 definition HTTgen :: "i set \<Rightarrow> i set" where |
18 definition HTTgen :: "i set \<Rightarrow> i set" where |
19 "HTTgen(R) == |
19 "HTTgen(R) == |
20 {t. t=true | t=false | (EX a b. t= <a, b> \<and> a : R \<and> b : R) | |
20 {t. t=true | t=false | (EX a b. t= <a, b> \<and> a : R \<and> b : R) | |
21 (EX f. t = lam x. f(x) \<and> (ALL x. f(x) : R))}" |
21 (EX f. t = lam x. f(x) \<and> (ALL x. f(x) : R))}" |
22 |
22 |
23 definition HTT :: "i set" |
23 definition HTT :: "i set" |
24 where "HTT == gfp(HTTgen)" |
24 where "HTT == gfp(HTTgen)" |
25 |
25 |
26 |
26 |
27 subsection {* Hereditary Termination *} |
27 subsection \<open>Hereditary Termination\<close> |
28 |
28 |
29 lemma HTTgen_mono: "mono(\<lambda>X. HTTgen(X))" |
29 lemma HTTgen_mono: "mono(\<lambda>X. HTTgen(X))" |
30 apply (unfold HTTgen_def) |
30 apply (unfold HTTgen_def) |
31 apply (rule monoI) |
31 apply (rule monoI) |
32 apply blast |
32 apply blast |
45 apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def]) |
45 apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def]) |
46 apply blast |
46 apply blast |
47 done |
47 done |
48 |
48 |
49 |
49 |
50 subsection {* Introduction Rules for HTT *} |
50 subsection \<open>Introduction Rules for HTT\<close> |
51 |
51 |
52 lemma HTT_bot: "\<not> bot : HTT" |
52 lemma HTT_bot: "\<not> bot : HTT" |
53 by (blast dest: HTTXH [THEN iffD1]) |
53 by (blast dest: HTTXH [THEN iffD1]) |
54 |
54 |
55 lemma HTT_true: "true : HTT" |
55 lemma HTT_true: "true : HTT" |
81 by (simp_all add: data_defs HTT_rews1) |
81 by (simp_all add: data_defs HTT_rews1) |
82 |
82 |
83 lemmas HTT_rews = HTT_rews1 HTT_rews2 |
83 lemmas HTT_rews = HTT_rews1 HTT_rews2 |
84 |
84 |
85 |
85 |
86 subsection {* Coinduction for HTT *} |
86 subsection \<open>Coinduction for HTT\<close> |
87 |
87 |
88 lemma HTT_coinduct: "\<lbrakk>t : R; R <= HTTgen(R)\<rbrakk> \<Longrightarrow> t : HTT" |
88 lemma HTT_coinduct: "\<lbrakk>t : R; R <= HTTgen(R)\<rbrakk> \<Longrightarrow> t : HTT" |
89 apply (erule HTT_def [THEN def_coinduct]) |
89 apply (erule HTT_def [THEN def_coinduct]) |
90 apply assumption |
90 apply assumption |
91 done |
91 done |
109 "\<lbrakk>h : lfp(\<lambda>x. HTTgen(x) Un R Un HTT); t : lfp(\<lambda>x. HTTgen(x) Un R Un HTT)\<rbrakk> \<Longrightarrow> |
109 "\<lbrakk>h : lfp(\<lambda>x. HTTgen(x) Un R Un HTT); t : lfp(\<lambda>x. HTTgen(x) Un R Un HTT)\<rbrakk> \<Longrightarrow> |
110 h$t : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))" |
110 h$t : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))" |
111 unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+ |
111 unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+ |
112 |
112 |
113 |
113 |
114 subsection {* Formation Rules for Types *} |
114 subsection \<open>Formation Rules for Types\<close> |
115 |
115 |
116 lemma UnitF: "Unit <= HTT" |
116 lemma UnitF: "Unit <= HTT" |
117 by (simp add: subsetXH UnitXH HTT_rews) |
117 by (simp add: subsetXH UnitXH HTT_rews) |
118 |
118 |
119 lemma BoolF: "Bool <= HTT" |
119 lemma BoolF: "Bool <= HTT" |