src/LCF/LCF.thy
changeset 19757 4a2a71c31968
parent 17249 e89fbfd778c1
child 19758 093690d4ba60
equal deleted inserted replaced
19756:61c4117345c6 19757:4a2a71c31968
     1 (*  Title:      LCF/lcf.thy
     1 (*  Title:      LCF/LCF.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 header {* LCF on top of First-Order Logic *}
     7 header {* LCF on top of First-Order Logic *}
     8 
     8 
     9 theory LCF
     9 theory LCF
    10 imports FOL
    10 imports FOL
    11 uses ("LCF_lemmas.ML") ("pair.ML") ("fix.ML")
       
    12 begin
    11 begin
    13 
    12 
    14 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
    13 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
    15 
    14 
    16 subsection {* Natural Deduction Rules for LCF *}
    15 subsection {* Natural Deduction Rules for LCF *}
   116   adm_conj:      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))"
   115   adm_conj:      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))"
   117   adm_disj:      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))"
   116   adm_disj:      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))"
   118   adm_imp:       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
   117   adm_imp:       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
   119   adm_all:       "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
   118   adm_all:       "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
   120 
   119 
   121 ML {* use_legacy_bindings (the_context ()) *}
   120 
   122 
   121 lemma eq_imp_less1: "x = y ==> x << y"
   123 use "LCF_lemmas.ML"
   122   by (simp add: eq_def)
       
   123 
       
   124 lemma eq_imp_less2: "x = y ==> y << x"
       
   125   by (simp add: eq_def)
       
   126 
       
   127 lemma less_refl [simp]: "x << x"
       
   128   apply (rule eq_imp_less1)
       
   129   apply (rule refl)
       
   130   done
       
   131 
       
   132 lemma less_anti_sym: "[| x << y; y << x |] ==> x=y"
       
   133   by (simp add: eq_def)
       
   134 
       
   135 lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
       
   136   apply (rule less_anti_sym)
       
   137   apply (rule less_ext)
       
   138   apply simp
       
   139   apply simp
       
   140   done
       
   141 
       
   142 lemma cong: "[| f=g; x=y |] ==> f(x)=g(y)"
       
   143   by simp
       
   144 
       
   145 lemma less_ap_term: "x << y ==> f(x) << f(y)"
       
   146   by (rule less_refl [THEN mono])
       
   147 
       
   148 lemma less_ap_thm: "f << g ==> f(x) << g(x)"
       
   149   by (rule less_refl [THEN [2] mono])
       
   150 
       
   151 lemma ap_term: "(x::'a::cpo) = y ==> (f(x)::'b::cpo) = f(y)"
       
   152   apply (rule cong [OF refl])
       
   153   apply simp
       
   154   done
       
   155 
       
   156 lemma ap_thm: "f = g ==> f(x) = g(x)"
       
   157   apply (erule cong)
       
   158   apply (rule refl)
       
   159   done
       
   160 
       
   161 
       
   162 lemma UU_abs: "(%x::'a::cpo. UU) = UU"
       
   163   apply (rule less_anti_sym)
       
   164   prefer 2
       
   165   apply (rule minimal)
       
   166   apply (rule less_ext)
       
   167   apply (rule allI)
       
   168   apply (rule minimal)
       
   169   done
       
   170 
       
   171 lemma UU_app: "UU(x) = UU"
       
   172   by (rule UU_abs [symmetric, THEN ap_thm])
       
   173 
       
   174 lemma less_UU: "x << UU ==> x=UU"
       
   175   apply (rule less_anti_sym)
       
   176   apply assumption
       
   177   apply (rule minimal)
       
   178   done
       
   179 
       
   180 lemma tr_induct: "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
       
   181   apply (rule allI)
       
   182   apply (rule mp)
       
   183   apply (rule_tac [2] p = b in tr_cases)
       
   184   apply blast
       
   185   done
       
   186 
       
   187 lemma Contrapos: "~ B ==> (A ==> B) ==> ~A"
       
   188   by blast
       
   189 
       
   190 lemma not_less_imp_not_eq1: "~ x << y \<Longrightarrow> x \<noteq> y"
       
   191   apply (erule Contrapos)
       
   192   apply simp
       
   193   done
       
   194 
       
   195 lemma not_less_imp_not_eq2: "~ y << x \<Longrightarrow> x \<noteq> y"
       
   196   apply (erule Contrapos)
       
   197   apply simp
       
   198   done
       
   199 
       
   200 lemma not_UU_eq_TT: "UU \<noteq> TT"
       
   201   by (rule not_less_imp_not_eq2) (rule not_TT_less_UU)
       
   202 lemma not_UU_eq_FF: "UU \<noteq> FF"
       
   203   by (rule not_less_imp_not_eq2) (rule not_FF_less_UU)
       
   204 lemma not_TT_eq_UU: "TT \<noteq> UU"
       
   205   by (rule not_less_imp_not_eq1) (rule not_TT_less_UU)
       
   206 lemma not_TT_eq_FF: "TT \<noteq> FF"
       
   207   by (rule not_less_imp_not_eq1) (rule not_TT_less_FF)
       
   208 lemma not_FF_eq_UU: "FF \<noteq> UU"
       
   209   by (rule not_less_imp_not_eq1) (rule not_FF_less_UU)
       
   210 lemma not_FF_eq_TT: "FF \<noteq> TT"
       
   211   by (rule not_less_imp_not_eq1) (rule not_FF_less_TT)
       
   212 
       
   213 
       
   214 lemma COND_cases_iff [rule_format]:
       
   215     "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
       
   216   apply (insert not_UU_eq_TT not_UU_eq_FF not_TT_eq_UU
       
   217     not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT)
       
   218   apply (rule tr_induct)
       
   219   apply (simplesubst COND_UU)
       
   220   apply blast
       
   221   apply (simplesubst COND_TT)
       
   222   apply blast
       
   223   apply (simplesubst COND_FF)
       
   224   apply blast
       
   225   done
       
   226 
       
   227 lemma COND_cases: 
       
   228   "[| x = UU --> P(UU); x = TT --> P(xa); x = FF --> P(y) |] ==> P(x => xa | y)"
       
   229   apply (rule COND_cases_iff [THEN iffD2])
       
   230   apply blast
       
   231   done
       
   232 
       
   233 lemmas [simp] =
       
   234   minimal
       
   235   UU_app
       
   236   UU_app [THEN ap_thm]
       
   237   UU_app [THEN ap_thm, THEN ap_thm]
       
   238   not_TT_less_FF not_FF_less_TT not_TT_less_UU not_FF_less_UU not_UU_eq_TT
       
   239   not_UU_eq_FF not_TT_eq_UU not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT
       
   240   COND_UU COND_TT COND_FF
       
   241   surj_pairing FST SND
   124 
   242 
   125 
   243 
   126 subsection {* Ordered pairs and products *}
   244 subsection {* Ordered pairs and products *}
   127 
   245 
   128 use "pair.ML"
   246 lemma expand_all_PROD: "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))"
       
   247   apply (rule iffI)
       
   248   apply blast
       
   249   apply (rule allI)
       
   250   apply (rule surj_pairing [THEN subst])
       
   251   apply blast
       
   252   done
       
   253 
       
   254 lemma PROD_less: "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
       
   255   apply (rule iffI)
       
   256   apply (rule conjI)
       
   257   apply (erule less_ap_term)
       
   258   apply (erule less_ap_term)
       
   259   apply (erule conjE)
       
   260   apply (rule surj_pairing [of p, THEN subst])
       
   261   apply (rule surj_pairing [of q, THEN subst])
       
   262   apply (rule mono, erule less_ap_term, assumption)
       
   263   done
       
   264 
       
   265 lemma PROD_eq: "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)"
       
   266   apply (rule iffI)
       
   267   apply simp
       
   268   apply (unfold eq_def)
       
   269   apply (simp add: PROD_less)
       
   270   done
       
   271 
       
   272 lemma PAIR_less [simp]: "<a,b> << <c,d> <-> a<<c & b<<d"
       
   273   by (simp add: PROD_less)
       
   274 
       
   275 lemma PAIR_eq [simp]: "<a,b> = <c,d> <-> a=c & b=d"
       
   276   by (simp add: PROD_eq)
       
   277 
       
   278 lemma UU_is_UU_UU [simp]: "<UU,UU> = UU"
       
   279   by (rule less_UU) (simp add: PROD_less)
       
   280 
       
   281 lemma FST_STRICT [simp]: "FST(UU) = UU"
       
   282   apply (rule subst [OF UU_is_UU_UU])
       
   283   apply (simp del: UU_is_UU_UU)
       
   284   done
       
   285 
       
   286 lemma SND_STRICT [simp]: "SND(UU) = UU"
       
   287   apply (rule subst [OF UU_is_UU_UU])
       
   288   apply (simp del: UU_is_UU_UU)
       
   289   done
   129 
   290 
   130 
   291 
   131 subsection {* Fixedpoint theory *}
   292 subsection {* Fixedpoint theory *}
   132 
   293 
   133 use "fix.ML"
   294 lemma adm_eq: "adm(%x. t(x)=(u(x)::'a::cpo))"
   134 
   295   apply (unfold eq_def)
       
   296   apply (rule adm_conj adm_less)+
       
   297   done
       
   298 
       
   299 lemma adm_not_not: "adm(P) ==> adm(%x.~~P(x))"
       
   300   by simp
       
   301 
       
   302 lemma not_eq_TT: "ALL p. ~p=TT <-> (p=FF | p=UU)"
       
   303   and not_eq_FF: "ALL p. ~p=FF <-> (p=TT | p=UU)"
       
   304   and not_eq_UU: "ALL p. ~p=UU <-> (p=TT | p=FF)"
       
   305   by (rule tr_induct, simp_all)+
       
   306 
       
   307 lemma adm_not_eq_tr: "ALL p::tr. adm(%x. ~t(x)=p)"
       
   308   apply (rule tr_induct)
       
   309   apply (simp_all add: not_eq_TT not_eq_FF not_eq_UU)
       
   310   apply (rule adm_disj adm_eq)+
       
   311   done
       
   312 
       
   313 lemmas adm_lemmas =
       
   314   adm_not_free adm_eq adm_less adm_not_less
       
   315   adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
       
   316 
       
   317 
       
   318 ML {*
       
   319 local
       
   320   val adm_lemmas = thms "adm_lemmas"
       
   321   val induct = thm "induct"
       
   322 in
       
   323   fun induct_tac v i =
       
   324     res_inst_tac[("f",v)] induct i THEN REPEAT (resolve_tac adm_lemmas i)
   135 end
   325 end
       
   326 *}
       
   327 
       
   328 lemma least_FIX: "f(p) = p ==> FIX(f) << p"
       
   329   apply (tactic {* induct_tac "f" 1 *})
       
   330   apply (rule minimal)
       
   331   apply (intro strip)
       
   332   apply (erule subst)
       
   333   apply (erule less_ap_term)
       
   334   done
       
   335 
       
   336 lemma lfp_is_FIX:
       
   337   assumes 1: "f(p) = p"
       
   338     and 2: "ALL q. f(q)=q --> p << q"
       
   339   shows "p = FIX(f)"
       
   340   apply (rule less_anti_sym)
       
   341   apply (rule 2 [THEN spec, THEN mp])
       
   342   apply (rule FIX_eq)
       
   343   apply (rule least_FIX)
       
   344   apply (rule 1)
       
   345   done
       
   346 
       
   347 
       
   348 lemma FIX_pair: "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"
       
   349   apply (rule lfp_is_FIX)
       
   350   apply (simp add: FIX_eq [of f] FIX_eq [of g])
       
   351   apply (intro strip)
       
   352   apply (simp add: PROD_less)
       
   353   apply (rule conjI)
       
   354   apply (rule least_FIX)
       
   355   apply (erule subst, rule FST [symmetric])
       
   356   apply (rule least_FIX)
       
   357   apply (erule subst, rule SND [symmetric])
       
   358   done
       
   359 
       
   360 lemma FIX1: "FIX(f) = FST(FIX(%p. <f(FST(p)),g(SND(p))>))"
       
   361   by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1])
       
   362 
       
   363 lemma FIX2: "FIX(g) = SND(FIX(%p. <f(FST(p)),g(SND(p))>))"
       
   364   by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct2])
       
   365 
       
   366 lemma induct2:
       
   367   assumes 1: "adm(%p. P(FST(p),SND(p)))"
       
   368     and 2: "P(UU::'a,UU::'b)"
       
   369     and 3: "ALL x y. P(x,y) --> P(f(x),g(y))"
       
   370   shows "P(FIX(f),FIX(g))"
       
   371   apply (rule FIX1 [THEN ssubst, of _ f g])
       
   372   apply (rule FIX2 [THEN ssubst, of _ f g])
       
   373   apply (rule induct [OF 1, where ?f = "%x. <f(FST(x)),g(SND(x))>"])
       
   374   apply simp
       
   375   apply (rule 2)
       
   376   apply (simp add: expand_all_PROD)
       
   377   apply (rule 3)
       
   378   done
       
   379 
       
   380 ML {*
       
   381 local
       
   382   val induct2 = thm "induct2"
       
   383   val adm_lemmas = thms "adm_lemmas"
       
   384 in
       
   385 
       
   386 fun induct2_tac (f,g) i =
       
   387   res_inst_tac[("f",f),("g",g)] induct2 i THEN
       
   388   REPEAT(resolve_tac adm_lemmas i)
       
   389 
       
   390 end
       
   391 *}
       
   392 
       
   393 end