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