17456

1 
(* Title: CCL/Fix.thy

1474

2 
Author: Martin Coen

0

3 
Copyright 1993 University of Cambridge


4 
*)


5 

17456

6 
header {* Tentative attempt at including fixed point induction; justified by Smith *}


7 


8 
theory Fix


9 
imports Type


10 
begin

0

11 


12 
consts

1474

13 
idgen :: "[i]=>i"

0

14 
INCL :: "[i=>o]=>o"


15 

24825

16 
defs

17456

17 
idgen_def:

3837

18 
"idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"

0

19 

24825

20 
axioms

17456

21 
INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) > P(fix(f)))"


22 
po_INCL: "INCL(%x. a(x) [= b(x))"


23 
INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"


24 

20140

25 


26 
subsection {* Fixed Point Induction *}


27 


28 
lemma fix_ind:


29 
assumes base: "P(bot)"


30 
and step: "!!x. P(x) ==> P(f(x))"


31 
and incl: "INCL(P)"


32 
shows "P(fix(f))"


33 
apply (rule incl [unfolded INCL_def, rule_format])


34 
apply (rule Nat_ind [THEN ballI], assumption)


35 
apply simp_all


36 
apply (rule base)


37 
apply (erule step)


38 
done


39 


40 


41 
subsection {* Inclusive Predicates *}


42 


43 
lemma inclXH: "INCL(P) <> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) > P(fix(f)))"


44 
by (simp add: INCL_def)


45 


46 
lemma inclI: "[ !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) ] ==> INCL(%x. P(x))"


47 
unfolding inclXH by blast


48 


49 
lemma inclD: "[ INCL(P); !!n. n:Nat ==> P(f^n`bot) ] ==> P(fix(f))"


50 
unfolding inclXH by blast


51 


52 
lemma inclE: "[ INCL(P); (ALL n:Nat. P(f^n`bot))>P(fix(f)) ==> R ] ==> R"


53 
by (blast dest: inclD)


54 


55 


56 
subsection {* Lemmas for Inclusive Predicates *}


57 


58 
lemma npo_INCL: "INCL(%x.~ a(x) [= t)"


59 
apply (rule inclI)


60 
apply (drule bspec)


61 
apply (rule zeroT)


62 
apply (erule contrapos)


63 
apply (rule po_trans)


64 
prefer 2


65 
apply assumption


66 
apply (subst napplyBzero)


67 
apply (rule po_cong, rule po_bot)


68 
done


69 


70 
lemma conj_INCL: "[ INCL(P); INCL(Q) ] ==> INCL(%x. P(x) & Q(x))"


71 
by (blast intro!: inclI dest!: inclD)


72 


73 
lemma all_INCL: "[ !!a. INCL(P(a)) ] ==> INCL(%x. ALL a. P(a,x))"


74 
by (blast intro!: inclI dest!: inclD)


75 


76 
lemma ball_INCL: "[ !!a. a:A ==> INCL(P(a)) ] ==> INCL(%x. ALL a:A. P(a,x))"


77 
by (blast intro!: inclI dest!: inclD)


78 


79 
lemma eq_INCL: "INCL(%x. a(x) = (b(x)::'a::prog))"


80 
apply (simp add: eq_iff)


81 
apply (rule conj_INCL po_INCL)+


82 
done


83 


84 


85 
subsection {* Derivation of Reachability Condition *}


86 


87 
(* Fixed points of idgen *)


88 


89 
lemma fix_idgenfp: "idgen(fix(idgen)) = fix(idgen)"


90 
apply (rule fixB [symmetric])


91 
done


92 


93 
lemma id_idgenfp: "idgen(lam x. x) = lam x. x"


94 
apply (simp add: idgen_def)


95 
apply (rule term_case [THEN allI])


96 
apply simp_all


97 
done


98 


99 
(* All fixed points are lamexpressions *)


100 

36319

101 
schematic_lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"

20140

102 
apply (unfold idgen_def)


103 
apply (erule ssubst)


104 
apply (rule refl)


105 
done


106 


107 
(* Lemmas for rewriting fixed points of idgen *)


108 


109 
lemma l_lemma: "[ a = b; a ` t = u ] ==> b ` t = u"


110 
by (simp add: idgen_def)


111 


112 
lemma idgen_lemmas:


113 
"idgen(d) = d ==> d ` bot = bot"


114 
"idgen(d) = d ==> d ` true = true"


115 
"idgen(d) = d ==> d ` false = false"


116 
"idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>"


117 
"idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"


118 
by (erule l_lemma, simp add: idgen_def)+


119 


120 


121 
(* Proof of Reachability law  show that fix and lam x.x both give LEAST fixed points


122 
of idgen and hence are they same *)


123 


124 
lemma po_eta:


125 
"[ ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) ] ==> t [= u"


126 
apply (drule cond_eta)+


127 
apply (erule ssubst)


128 
apply (erule ssubst)


129 
apply (rule po_lam [THEN iffD2])


130 
apply simp


131 
done


132 

36319

133 
schematic_lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"

20140

134 
apply (unfold idgen_def)


135 
apply (erule sym)


136 
done


137 


138 
lemma lemma1:


139 
"idgen(d) = d ==>


140 
{p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <=


141 
POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)})"


142 
apply clarify


143 
apply (rule_tac t = t in term_case)


144 
apply (simp_all add: POgenXH idgen_lemmas idgen_lemmas [OF fix_idgenfp])


145 
apply blast


146 
apply fast


147 
done


148 


149 
lemma fix_least_idgen: "idgen(d) = d ==> fix(idgen) [= d"


150 
apply (rule allI [THEN po_eta])


151 
apply (rule lemma1 [THEN [2] po_coinduct])


152 
apply (blast intro: po_eta_lemma fix_idgenfp)+


153 
done


154 


155 
lemma lemma2:


156 
"idgen(d) = d ==>


157 
{p. EX a b. p=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})"


158 
apply clarify


159 
apply (rule_tac t = a in term_case)


160 
apply (simp_all add: POgenXH idgen_lemmas)


161 
apply fast


162 
done


163 


164 
lemma id_least_idgen: "idgen(d) = d ==> lam x. x [= d"


165 
apply (rule allI [THEN po_eta])


166 
apply (rule lemma2 [THEN [2] po_coinduct])


167 
apply simp


168 
apply (fast intro: po_eta_lemma fix_idgenfp)+


169 
done


170 


171 
lemma reachability: "fix(idgen) = lam x. x"


172 
apply (fast intro: eq_iff [THEN iffD2]


173 
id_idgenfp [THEN fix_least_idgen] fix_idgenfp [THEN id_least_idgen])


174 
done


175 


176 
(********)


177 


178 
lemma id_apply: "f = lam x. x ==> f`t = t"


179 
apply (erule ssubst)


180 
apply (rule applyB)


181 
done


182 


183 
lemma term_ind:

23467

184 
assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)"


185 
and 4: "!!x y.[ P(x); P(y) ] ==> P(<x,y>)"


186 
and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"


187 
and 6: "INCL(P)"

20140

188 
shows "P(t)"


189 
apply (rule reachability [THEN id_apply, THEN subst])


190 
apply (rule_tac x = t in spec)


191 
apply (rule fix_ind)


192 
apply (unfold idgen_def)


193 
apply (rule allI)


194 
apply (subst applyBbot)

23467

195 
apply (rule 1)

20140

196 
apply (rule allI)


197 
apply (rule applyB [THEN ssubst])


198 
apply (rule_tac t = "xa" in term_case)


199 
apply simp_all

23467

200 
apply (fast intro: assms INCL_subst all_INCL)+

20140

201 
done

0

202 


203 
end
