1(* Title: CCL/Hered.thy 2 Author: Martin Coen 3 Copyright 1993 University of Cambridge 4*) 5 6section \<open>Hereditary Termination -- cf. Martin Lo\"f\<close> 7 8theory Hered 9imports Type 10begin 11 12text \<open> 13 Note that this is based on an untyped equality and so \<open>lam 14 x. b(x)\<close> is only hereditarily terminating if \<open>ALL x. b(x)\<close> 15 is. Not so useful for functions! 16\<close> 17 18definition HTTgen :: "i set \<Rightarrow> i set" where 19 "HTTgen(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))}" 22 23definition HTT :: "i set" 24 where "HTT == gfp(HTTgen)" 25 26 27subsection \<open>Hereditary Termination\<close> 28 29lemma HTTgen_mono: "mono(\<lambda>X. HTTgen(X))" 30 apply (unfold HTTgen_def) 31 apply (rule monoI) 32 apply blast 33 done 34 35lemma HTTgenXH: 36 "t : HTTgen(A) \<longleftrightarrow> t=true | t=false | (EX a b. t=<a,b> \<and> a : A \<and> b : A) | 37 (EX f. t=lam x. f(x) \<and> (ALL x. f(x) : A))" 38 apply (unfold HTTgen_def) 39 apply blast 40 done 41 42lemma HTTXH: 43 "t : HTT \<longleftrightarrow> t=true | t=false | (EX a b. t=<a,b> \<and> a : HTT \<and> b : HTT) | 44 (EX f. t=lam x. f(x) \<and> (ALL x. f(x) : HTT))" 45 apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def]) 46 apply blast 47 done 48 49 50subsection \<open>Introduction Rules for HTT\<close> 51 52lemma HTT_bot: "\<not> bot : HTT" 53 by (blast dest: HTTXH [THEN iffD1]) 54 55lemma HTT_true: "true : HTT" 56 by (blast intro: HTTXH [THEN iffD2]) 57 58lemma HTT_false: "false : HTT" 59 by (blast intro: HTTXH [THEN iffD2]) 60 61lemma HTT_pair: "<a,b> : HTT \<longleftrightarrow> a : HTT \<and> b : HTT" 62 apply (rule HTTXH [THEN iff_trans]) 63 apply blast 64 done 65 66lemma HTT_lam: "lam x. f(x) : HTT \<longleftrightarrow> (ALL x. f(x) : HTT)" 67 apply (rule HTTXH [THEN iff_trans]) 68 apply auto 69 done 70 71lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam 72 73lemma HTT_rews2: 74 "one : HTT" 75 "inl(a) : HTT \<longleftrightarrow> a : HTT" 76 "inr(b) : HTT \<longleftrightarrow> b : HTT" 77 "zero : HTT" 78 "succ(n) : HTT \<longleftrightarrow> n : HTT" 79 "[] : HTT" 80 "x$xs : HTT \<longleftrightarrow> x : HTT \<and> xs : HTT" 81 by (simp_all add: data_defs HTT_rews1) 82 83lemmas HTT_rews = HTT_rews1 HTT_rews2 84 85 86subsection \<open>Coinduction for HTT\<close> 87 88lemma HTT_coinduct: "\<lbrakk>t : R; R <= HTTgen(R)\<rbrakk> \<Longrightarrow> t : HTT" 89 apply (erule HTT_def [THEN def_coinduct]) 90 apply assumption 91 done 92 93lemma HTT_coinduct3: "\<lbrakk>t : R; R <= HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))\<rbrakk> \<Longrightarrow> t : HTT" 94 apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]]) 95 apply assumption 96 done 97 98lemma HTTgenIs: 99 "true : HTTgen(R)" 100 "false : HTTgen(R)" 101 "\<lbrakk>a : R; b : R\<rbrakk> \<Longrightarrow> <a,b> : HTTgen(R)" 102 "\<And>b. (\<And>x. b(x) : R) \<Longrightarrow> lam x. b(x) : HTTgen(R)" 103 "one : HTTgen(R)" 104 "a : lfp(\<lambda>x. HTTgen(x) Un R Un HTT) \<Longrightarrow> inl(a) : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))" 105 "b : lfp(\<lambda>x. HTTgen(x) Un R Un HTT) \<Longrightarrow> inr(b) : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))" 106 "zero : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))" 107 "n : lfp(\<lambda>x. HTTgen(x) Un R Un HTT) \<Longrightarrow> succ(n) : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))" 108 "[] : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))" 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))" 111 unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+ 112 113 114subsection \<open>Formation Rules for Types\<close> 115 116lemma UnitF: "Unit <= HTT" 117 by (simp add: subsetXH UnitXH HTT_rews) 118 119lemma BoolF: "Bool <= HTT" 120 by (fastforce simp: subsetXH BoolXH iff: HTT_rews) 121 122lemma PlusF: "\<lbrakk>A <= HTT; B <= HTT\<rbrakk> \<Longrightarrow> A + B <= HTT" 123 by (fastforce simp: subsetXH PlusXH iff: HTT_rews) 124 125lemma SigmaF: "\<lbrakk>A <= HTT; \<And>x. x:A \<Longrightarrow> B(x) <= HTT\<rbrakk> \<Longrightarrow> SUM x:A. B(x) <= HTT" 126 by (fastforce simp: subsetXH SgXH HTT_rews) 127 128 129(*** Formation Rules for Recursive types - using coinduction these only need ***) 130(*** exhaution rule for type-former ***) 131 132(*Proof by induction - needs induction rule for type*) 133lemma "Nat <= HTT" 134 apply (simp add: subsetXH) 135 apply clarify 136 apply (erule Nat_ind) 137 apply (fastforce iff: HTT_rews)+ 138 done 139 140lemma NatF: "Nat <= HTT" 141 apply clarify 142 apply (erule HTT_coinduct3) 143 apply (fast intro: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] dest: NatXH [THEN iffD1]) 144 done 145 146lemma ListF: "A <= HTT \<Longrightarrow> List(A) <= HTT" 147 apply clarify 148 apply (erule HTT_coinduct3) 149 apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] 150 subsetD [THEN HTTgen_mono [THEN ci3_AI]] 151 dest: ListXH [THEN iffD1]) 152 done 153 154lemma ListsF: "A <= HTT \<Longrightarrow> Lists(A) <= HTT" 155 apply clarify 156 apply (erule HTT_coinduct3) 157 apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] 158 subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: ListsXH [THEN iffD1]) 159 done 160 161lemma IListsF: "A <= HTT \<Longrightarrow> ILists(A) <= HTT" 162 apply clarify 163 apply (erule HTT_coinduct3) 164 apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] 165 subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: IListsXH [THEN iffD1]) 166 done 167 168end 169