wenzelm@17456: (* Title: CCL/Fix.thy clasohm@0: ID: $Id$ clasohm@1474: Author: Martin Coen clasohm@0: Copyright 1993 University of Cambridge clasohm@0: *) clasohm@0: wenzelm@17456: header {* Tentative attempt at including fixed point induction; justified by Smith *} wenzelm@17456: wenzelm@17456: theory Fix wenzelm@17456: imports Type wenzelm@17456: begin clasohm@0: clasohm@0: consts clasohm@1474: idgen :: "[i]=>i" clasohm@0: INCL :: "[i=>o]=>o" clasohm@0: wenzelm@17456: axioms wenzelm@17456: idgen_def: wenzelm@3837: "idgen(f) == lam t. case(t,true,false,%x y.,%u. lam x. f ` u(x))" clasohm@0: wenzelm@17456: INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" wenzelm@17456: po_INCL: "INCL(%x. a(x) [= b(x))" wenzelm@17456: INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" wenzelm@17456: wenzelm@20140: wenzelm@20140: subsection {* Fixed Point Induction *} wenzelm@20140: wenzelm@20140: lemma fix_ind: wenzelm@20140: assumes base: "P(bot)" wenzelm@20140: and step: "!!x. P(x) ==> P(f(x))" wenzelm@20140: and incl: "INCL(P)" wenzelm@20140: shows "P(fix(f))" wenzelm@20140: apply (rule incl [unfolded INCL_def, rule_format]) wenzelm@20140: apply (rule Nat_ind [THEN ballI], assumption) wenzelm@20140: apply simp_all wenzelm@20140: apply (rule base) wenzelm@20140: apply (erule step) wenzelm@20140: done wenzelm@20140: wenzelm@20140: wenzelm@20140: subsection {* Inclusive Predicates *} wenzelm@20140: wenzelm@20140: lemma inclXH: "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))" wenzelm@20140: by (simp add: INCL_def) wenzelm@20140: wenzelm@20140: lemma inclI: "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))" wenzelm@20140: unfolding inclXH by blast wenzelm@20140: wenzelm@20140: lemma inclD: "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))" wenzelm@20140: unfolding inclXH by blast wenzelm@20140: wenzelm@20140: lemma inclE: "[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R" wenzelm@20140: by (blast dest: inclD) wenzelm@20140: wenzelm@20140: wenzelm@20140: subsection {* Lemmas for Inclusive Predicates *} wenzelm@20140: wenzelm@20140: lemma npo_INCL: "INCL(%x.~ a(x) [= t)" wenzelm@20140: apply (rule inclI) wenzelm@20140: apply (drule bspec) wenzelm@20140: apply (rule zeroT) wenzelm@20140: apply (erule contrapos) wenzelm@20140: apply (rule po_trans) wenzelm@20140: prefer 2 wenzelm@20140: apply assumption wenzelm@20140: apply (subst napplyBzero) wenzelm@20140: apply (rule po_cong, rule po_bot) wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma conj_INCL: "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))" wenzelm@20140: by (blast intro!: inclI dest!: inclD) wenzelm@20140: wenzelm@20140: lemma all_INCL: "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))" wenzelm@20140: by (blast intro!: inclI dest!: inclD) wenzelm@20140: wenzelm@20140: lemma ball_INCL: "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))" wenzelm@20140: by (blast intro!: inclI dest!: inclD) wenzelm@20140: wenzelm@20140: lemma eq_INCL: "INCL(%x. a(x) = (b(x)::'a::prog))" wenzelm@20140: apply (simp add: eq_iff) wenzelm@20140: apply (rule conj_INCL po_INCL)+ wenzelm@20140: done wenzelm@20140: wenzelm@20140: wenzelm@20140: subsection {* Derivation of Reachability Condition *} wenzelm@20140: wenzelm@20140: (* Fixed points of idgen *) wenzelm@20140: wenzelm@20140: lemma fix_idgenfp: "idgen(fix(idgen)) = fix(idgen)" wenzelm@20140: apply (rule fixB [symmetric]) wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma id_idgenfp: "idgen(lam x. x) = lam x. x" wenzelm@20140: apply (simp add: idgen_def) wenzelm@20140: apply (rule term_case [THEN allI]) wenzelm@20140: apply simp_all wenzelm@20140: done wenzelm@20140: wenzelm@20140: (* All fixed points are lam-expressions *) wenzelm@20140: wenzelm@20140: lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)" wenzelm@20140: apply (unfold idgen_def) wenzelm@20140: apply (erule ssubst) wenzelm@20140: apply (rule refl) wenzelm@20140: done wenzelm@20140: wenzelm@20140: (* Lemmas for rewriting fixed points of idgen *) wenzelm@20140: wenzelm@20140: lemma l_lemma: "[| a = b; a ` t = u |] ==> b ` t = u" wenzelm@20140: by (simp add: idgen_def) wenzelm@20140: wenzelm@20140: lemma idgen_lemmas: wenzelm@20140: "idgen(d) = d ==> d ` bot = bot" wenzelm@20140: "idgen(d) = d ==> d ` true = true" wenzelm@20140: "idgen(d) = d ==> d ` false = false" wenzelm@20140: "idgen(d) = d ==> d ` = " wenzelm@20140: "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)" wenzelm@20140: by (erule l_lemma, simp add: idgen_def)+ wenzelm@20140: wenzelm@20140: wenzelm@20140: (* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points wenzelm@20140: of idgen and hence are they same *) wenzelm@20140: wenzelm@20140: lemma po_eta: wenzelm@20140: "[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u" wenzelm@20140: apply (drule cond_eta)+ wenzelm@20140: apply (erule ssubst) wenzelm@20140: apply (erule ssubst) wenzelm@20140: apply (rule po_lam [THEN iffD2]) wenzelm@20140: apply simp wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)" wenzelm@20140: apply (unfold idgen_def) wenzelm@20140: apply (erule sym) wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma lemma1: wenzelm@20140: "idgen(d) = d ==> wenzelm@20140: {p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)} <= wenzelm@20140: POgen({p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)})" wenzelm@20140: apply clarify wenzelm@20140: apply (rule_tac t = t in term_case) wenzelm@20140: apply (simp_all add: POgenXH idgen_lemmas idgen_lemmas [OF fix_idgenfp]) wenzelm@20140: apply blast wenzelm@20140: apply fast wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma fix_least_idgen: "idgen(d) = d ==> fix(idgen) [= d" wenzelm@20140: apply (rule allI [THEN po_eta]) wenzelm@20140: apply (rule lemma1 [THEN [2] po_coinduct]) wenzelm@20140: apply (blast intro: po_eta_lemma fix_idgenfp)+ wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma lemma2: wenzelm@20140: "idgen(d) = d ==> wenzelm@20140: {p. EX a b. p= & b = d ` a} <= POgen({p. EX a b. p= & b = d ` a})" wenzelm@20140: apply clarify wenzelm@20140: apply (rule_tac t = a in term_case) wenzelm@20140: apply (simp_all add: POgenXH idgen_lemmas) wenzelm@20140: apply fast wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma id_least_idgen: "idgen(d) = d ==> lam x. x [= d" wenzelm@20140: apply (rule allI [THEN po_eta]) wenzelm@20140: apply (rule lemma2 [THEN [2] po_coinduct]) wenzelm@20140: apply simp wenzelm@20140: apply (fast intro: po_eta_lemma fix_idgenfp)+ wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma reachability: "fix(idgen) = lam x. x" wenzelm@20140: apply (fast intro: eq_iff [THEN iffD2] wenzelm@20140: id_idgenfp [THEN fix_least_idgen] fix_idgenfp [THEN id_least_idgen]) wenzelm@20140: done wenzelm@20140: wenzelm@20140: (********) wenzelm@20140: wenzelm@20140: lemma id_apply: "f = lam x. x ==> f`t = t" wenzelm@20140: apply (erule ssubst) wenzelm@20140: apply (rule applyB) wenzelm@20140: done wenzelm@20140: wenzelm@20140: lemma term_ind: wenzelm@23467: assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)" wenzelm@23467: and 4: "!!x y.[| P(x); P(y) |] ==> P()" wenzelm@23467: and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))" wenzelm@23467: and 6: "INCL(P)" wenzelm@20140: shows "P(t)" wenzelm@20140: apply (rule reachability [THEN id_apply, THEN subst]) wenzelm@20140: apply (rule_tac x = t in spec) wenzelm@20140: apply (rule fix_ind) wenzelm@20140: apply (unfold idgen_def) wenzelm@20140: apply (rule allI) wenzelm@20140: apply (subst applyBbot) wenzelm@23467: apply (rule 1) wenzelm@20140: apply (rule allI) wenzelm@20140: apply (rule applyB [THEN ssubst]) wenzelm@20140: apply (rule_tac t = "xa" in term_case) wenzelm@20140: apply simp_all wenzelm@23467: apply (fast intro: assms INCL_subst all_INCL)+ wenzelm@20140: done clasohm@0: clasohm@0: end