1(* Title: CCL/Fix.thy 2 Author: Martin Coen 3 Copyright 1993 University of Cambridge 4*) 5 6section \<open>Tentative attempt at including fixed point induction; justified by Smith\<close> 7 8theory Fix 9imports Type 10begin 11 12definition idgen :: "i \<Rightarrow> i" 13 where "idgen(f) == lam t. case(t,true,false, \<lambda>x y.<f`x, f`y>, \<lambda>u. lam x. f ` u(x))" 14 15axiomatization INCL :: "[i\<Rightarrow>o]\<Rightarrow>o" where 16 INCL_def: "INCL(\<lambda>x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) \<longrightarrow> P(fix(f)))" and 17 po_INCL: "INCL(\<lambda>x. a(x) [= b(x))" and 18 INCL_subst: "INCL(P) \<Longrightarrow> INCL(\<lambda>x. P((g::i\<Rightarrow>i)(x)))" 19 20 21subsection \<open>Fixed Point Induction\<close> 22 23lemma fix_ind: 24 assumes base: "P(bot)" 25 and step: "\<And>x. P(x) \<Longrightarrow> P(f(x))" 26 and incl: "INCL(P)" 27 shows "P(fix(f))" 28 apply (rule incl [unfolded INCL_def, rule_format]) 29 apply (rule Nat_ind [THEN ballI], assumption) 30 apply simp_all 31 apply (rule base) 32 apply (erule step) 33 done 34 35 36subsection \<open>Inclusive Predicates\<close> 37 38lemma inclXH: "INCL(P) \<longleftrightarrow> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) \<longrightarrow> P(fix(f)))" 39 by (simp add: INCL_def) 40 41lemma inclI: "\<lbrakk>\<And>f. ALL n:Nat. P(f^n`bot) \<Longrightarrow> P(fix(f))\<rbrakk> \<Longrightarrow> INCL(\<lambda>x. P(x))" 42 unfolding inclXH by blast 43 44lemma inclD: "\<lbrakk>INCL(P); \<And>n. n:Nat \<Longrightarrow> P(f^n`bot)\<rbrakk> \<Longrightarrow> P(fix(f))" 45 unfolding inclXH by blast 46 47lemma inclE: "\<lbrakk>INCL(P); (ALL n:Nat. P(f^n`bot)) \<longrightarrow> P(fix(f)) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 48 by (blast dest: inclD) 49 50 51subsection \<open>Lemmas for Inclusive Predicates\<close> 52 53lemma npo_INCL: "INCL(\<lambda>x. \<not> a(x) [= t)" 54 apply (rule inclI) 55 apply (drule bspec) 56 apply (rule zeroT) 57 apply (erule contrapos) 58 apply (rule po_trans) 59 prefer 2 60 apply assumption 61 apply (subst napplyBzero) 62 apply (rule po_cong, rule po_bot) 63 done 64 65lemma conj_INCL: "\<lbrakk>INCL(P); INCL(Q)\<rbrakk> \<Longrightarrow> INCL(\<lambda>x. P(x) \<and> Q(x))" 66 by (blast intro!: inclI dest!: inclD) 67 68lemma all_INCL: "(\<And>a. INCL(P(a))) \<Longrightarrow> INCL(\<lambda>x. ALL a. P(a,x))" 69 by (blast intro!: inclI dest!: inclD) 70 71lemma ball_INCL: "(\<And>a. a:A \<Longrightarrow> INCL(P(a))) \<Longrightarrow> INCL(\<lambda>x. ALL a:A. P(a,x))" 72 by (blast intro!: inclI dest!: inclD) 73 74lemma eq_INCL: "INCL(\<lambda>x. a(x) = (b(x)::'a::prog))" 75 apply (simp add: eq_iff) 76 apply (rule conj_INCL po_INCL)+ 77 done 78 79 80subsection \<open>Derivation of Reachability Condition\<close> 81 82(* Fixed points of idgen *) 83 84lemma fix_idgenfp: "idgen(fix(idgen)) = fix(idgen)" 85 apply (rule fixB [symmetric]) 86 done 87 88lemma id_idgenfp: "idgen(lam x. x) = lam x. x" 89 apply (simp add: idgen_def) 90 apply (rule term_case [THEN allI]) 91 apply simp_all 92 done 93 94(* All fixed points are lam-expressions *) 95 96schematic_goal idgenfp_lam: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)" 97 apply (unfold idgen_def) 98 apply (erule ssubst) 99 apply (rule refl) 100 done 101 102(* Lemmas for rewriting fixed points of idgen *) 103 104lemma l_lemma: "\<lbrakk>a = b; a ` t = u\<rbrakk> \<Longrightarrow> b ` t = u" 105 by (simp add: idgen_def) 106 107lemma idgen_lemmas: 108 "idgen(d) = d \<Longrightarrow> d ` bot = bot" 109 "idgen(d) = d \<Longrightarrow> d ` true = true" 110 "idgen(d) = d \<Longrightarrow> d ` false = false" 111 "idgen(d) = d \<Longrightarrow> d ` <a,b> = <d ` a,d ` b>" 112 "idgen(d) = d \<Longrightarrow> d ` (lam x. f(x)) = lam x. d ` f(x)" 113 by (erule l_lemma, simp add: idgen_def)+ 114 115 116(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points 117 of idgen and hence are they same *) 118 119lemma po_eta: 120 "\<lbrakk>ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x)\<rbrakk> \<Longrightarrow> t [= u" 121 apply (drule cond_eta)+ 122 apply (erule ssubst) 123 apply (erule ssubst) 124 apply (rule po_lam [THEN iffD2]) 125 apply simp 126 done 127 128schematic_goal po_eta_lemma: "idgen(d) = d \<Longrightarrow> d = lam x. ?f(x)" 129 apply (unfold idgen_def) 130 apply (erule sym) 131 done 132 133lemma lemma1: 134 "idgen(d) = d \<Longrightarrow> 135 {p. EX a b. p=<a,b> \<and> (EX t. a=fix(idgen) ` t \<and> b = d ` t)} <= 136 POgen({p. EX a b. p=<a,b> \<and> (EX t. a=fix(idgen) ` t \<and> b = d ` t)})" 137 apply clarify 138 apply (rule_tac t = t in term_case) 139 apply (simp_all add: POgenXH idgen_lemmas idgen_lemmas [OF fix_idgenfp]) 140 apply blast 141 apply fast 142 done 143 144lemma fix_least_idgen: "idgen(d) = d \<Longrightarrow> fix(idgen) [= d" 145 apply (rule allI [THEN po_eta]) 146 apply (rule lemma1 [THEN [2] po_coinduct]) 147 apply (blast intro: po_eta_lemma fix_idgenfp)+ 148 done 149 150lemma lemma2: 151 "idgen(d) = d \<Longrightarrow> 152 {p. EX a b. p=<a,b> \<and> b = d ` a} <= POgen({p. EX a b. p=<a,b> \<and> b = d ` a})" 153 apply clarify 154 apply (rule_tac t = a in term_case) 155 apply (simp_all add: POgenXH idgen_lemmas) 156 apply fast 157 done 158 159lemma id_least_idgen: "idgen(d) = d \<Longrightarrow> lam x. x [= d" 160 apply (rule allI [THEN po_eta]) 161 apply (rule lemma2 [THEN [2] po_coinduct]) 162 apply simp 163 apply (fast intro: po_eta_lemma fix_idgenfp)+ 164 done 165 166lemma reachability: "fix(idgen) = lam x. x" 167 apply (fast intro: eq_iff [THEN iffD2] 168 id_idgenfp [THEN fix_least_idgen] fix_idgenfp [THEN id_least_idgen]) 169 done 170 171(********) 172 173lemma id_apply: "f = lam x. x \<Longrightarrow> f`t = t" 174 apply (erule ssubst) 175 apply (rule applyB) 176 done 177 178lemma term_ind: 179 assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)" 180 and 4: "\<And>x y. \<lbrakk>P(x); P(y)\<rbrakk> \<Longrightarrow> P(<x,y>)" 181 and 5: "\<And>u.(\<And>x. P(u(x))) \<Longrightarrow> P(lam x. u(x))" 182 and 6: "INCL(P)" 183 shows "P(t)" 184 apply (rule reachability [THEN id_apply, THEN subst]) 185 apply (rule_tac x = t in spec) 186 apply (rule fix_ind) 187 apply (unfold idgen_def) 188 apply (rule allI) 189 apply (subst applyBbot) 190 apply (rule 1) 191 apply (rule allI) 192 apply (rule applyB [THEN ssubst]) 193 apply (rule_tac t = "xa" in term_case) 194 apply simp_all 195 apply (fast intro: assms INCL_subst all_INCL)+ 196 done 197 198end 199