# HG changeset patch # User wenzelm # Date 1004747891 -3600 # Node ID 0b1d80ada4ab012b7bb7ffc6f99efecf87fea90f # Parent edf306d60e4f46078f59957cec6ee804173e4dbf rep_datatype lift; converted to new-style theory; diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift.ML --- a/src/HOLCF/Lift.ML Sat Nov 03 01:36:19 2001 +0100 +++ b/src/HOLCF/Lift.ML Sat Nov 03 01:38:11 2001 +0100 @@ -1,108 +1,53 @@ -(* Title: HOLCF/Lift.ML - ID: $Id$ - Author: Olaf Mueller - Copyright 1997 Technische Universitaet Muenchen -Theorems for Lift.thy -*) - - -(* ---------------------------------------------------------- *) - section"Continuity Proofs for flift1, flift2, if"; -(* ---------------------------------------------------------- *) -(* need the instance into flat *) - - -(* flift1 is continuous in its argument itself*) -Goal "cont (lift_case UU f)"; -by (rtac flatdom_strict2cont 1); -by (Simp_tac 1); -qed"cont_flift1_arg"; - -(* flift1 is continuous in a variable that occurs only - in the Def branch *) +(* legacy ML bindings *) -Goal "!!f. [| !! a. cont (%y. (f y) a) |] ==> \ -\ cont (%y. lift_case UU (f y))"; -by (rtac cont2cont_CF1L_rev 1); -by (strip_tac 1); -by (res_inst_tac [("x","y")] Lift_cases 1); -by (Asm_simp_tac 1); -by (fast_tac (HOL_cs addss simpset()) 1); -qed"cont_flift1_not_arg"; - -(* flift1 is continuous in a variable that occurs either - in the Def branch or in the argument *) - -Goal "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \ -\ cont (%y. lift_case UU (f y) (g y))"; -by (res_inst_tac [("tt","g")] cont2cont_app 1); -by (rtac cont_flift1_not_arg 1); -by Auto_tac; -by (rtac cont_flift1_arg 1); -qed"cont_flift1_arg_and_not_arg"; - -(* flift2 is continuous in its argument itself *) - -Goal "cont (lift_case UU (%y. Def (f y)))"; -by (rtac flatdom_strict2cont 1); -by (Simp_tac 1); -qed"cont_flift2_arg"; - +structure lift = +struct + val distinct = thms "lift.distinct"; + val inject = thms "lift.inject"; + val exhaust = thm "lift.exhaust"; + val cases = thms "lift.cases"; + val split = thm "lift.split"; + val split_asm = thm "lift.split_asm"; + val induct = thm "lift.induct"; + val recs = thms "lift.recs"; + val simps = thms "lift.simps"; + val size = thms "lift.size"; +end; -(* ---------------------------------------------------------- *) -(* Extension of cont_tac and installation of simplifier *) -(* ---------------------------------------------------------- *) - -bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev); - -val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg, - cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, - cont_Rep_CFun_app,cont_Rep_CFun_app_app,cont_if]; - -val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext; - -Addsimps cont_lemmas_ext; - -fun cont_tac i = resolve_tac cont_lemmas2 i; -fun cont_tacR i = REPEAT (cont_tac i); - -fun cont_tacRs i = simp_tac (simpset() addsimps [flift1_def,flift2_def]) i THEN - REPEAT (cont_tac i); - - -simpset_ref() := simpset() addSolver - (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac))); - - - -(* ---------------------------------------------------------- *) - section"flift1, flift2"; -(* ---------------------------------------------------------- *) - - -Goal "flift1 f$(Def x) = (f x)"; -by (simp_tac (simpset() addsimps [flift1_def]) 1); -qed"flift1_Def"; - -Goal "flift2 f$(Def x) = Def (f x)"; -by (simp_tac (simpset() addsimps [flift2_def]) 1); -qed"flift2_Def"; - -Goal "flift1 f$UU = UU"; -by (simp_tac (simpset() addsimps [flift1_def]) 1); -qed"flift1_UU"; - -Goal "flift2 f$UU = UU"; -by (simp_tac (simpset() addsimps [flift2_def]) 1); -qed"flift2_UU"; - -Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU]; - -Goal "x~=UU ==> (flift2 f)$x~=UU"; -by (def_tac 1); -qed"flift2_nUU"; - -Addsimps [flift2_nUU]; - - +val Def_not_UU = thm "Def_not_UU"; +val DefE = thm "DefE"; +val DefE2 = thm "DefE2"; +val Def_inject_less_eq = thm "Def_inject_less_eq"; +val Def_less_is_eq = thm "Def_less_is_eq"; +val Lift_cases = thm "Lift_cases"; +val Lift_exhaust = thm "Lift_exhaust"; +val UU_lift_def = thm "UU_lift_def"; +val Undef_eq_UU = thm "Undef_eq_UU"; +val chain_mono2_po = thm "chain_mono2_po"; +val cont2cont_CF1L_rev2 = thm "cont2cont_CF1L_rev2"; +val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; +val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; +val cont_flift1_arg = thm "cont_flift1_arg"; +val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg"; +val cont_flift1_not_arg = thm "cont_flift1_not_arg"; +val cont_flift2_arg = thm "cont_flift2_arg"; +val cont_if = thm "cont_if"; +val cpo_lift = thm "cpo_lift"; +val flat_imp_chfin_poo = thm "flat_imp_chfin_poo"; +val flift1_Def = thm "flift1_Def"; +val flift1_UU = thm "flift1_UU"; +val flift1_def = thm "flift1_def"; +val flift2_Def = thm "flift2_Def"; +val flift2_UU = thm "flift2_UU"; +val flift2_def = thm "flift2_def"; +val flift2_nUU = thm "flift2_nUU"; +val inst_lift_pcpo = thm "inst_lift_pcpo"; +val inst_lift_po = thm "inst_lift_po"; +val least_lift = thm "least_lift"; +val less_lift = thm "less_lift"; +val less_lift_def = thm "less_lift_def"; +val liftpair_def = thm "liftpair_def"; +val minimal_lift = thm "minimal_lift"; +val notUndef_I = thm "notUndef_I"; +val not_Undef_is_Def = thm "not_Undef_is_Def"; diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Sat Nov 03 01:36:19 2001 +0100 +++ b/src/HOLCF/Lift.thy Sat Nov 03 01:38:11 2001 +0100 @@ -1,16 +1,339 @@ (* Title: HOLCF/Lift.thy ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen + Author: Olaf Mueller + License: GPL (GNU GENERAL PUBLIC LICENSE) *) -Lift = Lift3 + +header {* Lifting types of class term to flat pcpo's *} + +theory Lift = Cprod3: + +defaultsort "term" + + +typedef 'a lift = "UNIV :: 'a option set" .. + +constdefs + Undef :: "'a lift" + "Undef == Abs_lift None" + Def :: "'a => 'a lift" + "Def x == Abs_lift (Some x)" + +instance lift :: ("term") sq_ord .. + +defs (overloaded) + less_lift_def: "x << y == (x=y | x=Undef)" + +instance lift :: ("term") po +proof + fix x y z :: "'a lift" + show "x << x" by (unfold less_lift_def) blast + { assume "x << y" and "y << x" thus "x = y" by (unfold less_lift_def) blast } + { assume "x << y" and "y << z" thus "x << z" by (unfold less_lift_def) blast } +qed + +lemma inst_lift_po: "(op <<) = (\x y. x = y | x = Undef)" + -- {* For compatibility with old HOLCF-Version. *} + by (simp only: less_lift_def [symmetric]) + + +subsection {* Type lift is pointed *} + +lemma minimal_lift [iff]: "Undef << x" + by (simp add: inst_lift_po) + +lemma UU_lift_def: "(SOME u. \y. u \ y) = Undef" + apply (rule minimal2UU [symmetric]) + apply (rule minimal_lift) + done + +lemma least_lift: "EX x::'a lift. ALL y. x << y" + apply (rule_tac x = Undef in exI) + apply (rule minimal_lift [THEN allI]) + done + + +subsection {* Type lift is a cpo *} + +text {* + The following lemmas have already been proved in @{text Pcpo.ML} and + @{text Fix.ML}, but there class @{text pcpo} is assumed, although + only @{text po} is necessary and a least element. Therefore they are + redone here for the @{text po} lift with least element @{text + Undef}. +*} + +lemma notUndef_I: "[| x< y ~= Undef" + -- {* Tailoring @{text notUU_I} of @{text Pcpo.ML} to @{text Undef} *} + by (blast intro: antisym_less) + +lemma chain_mono2_po: "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] + ==> EX j. ALL i. j~Y(i)=Undef" + -- {* Tailoring @{text chain_mono2} of @{text Pcpo.ML} to @{text Undef} *} + apply safe + apply (rule exI) + apply (intro strip) + apply (rule notUndef_I) + apply (erule (1) chain_mono) + apply assumption + done + +lemma flat_imp_chfin_poo: "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))" + -- {* Tailoring @{text flat_imp_chfin} of @{text Fix.ML} to @{text lift} *} + apply (unfold max_in_chain_def) + apply (intro strip) + apply (rule_tac P = "ALL i. Y (i) = Undef" in case_split) + apply (rule_tac x = 0 in exI) + apply (intro strip) + apply (rule trans) + apply (erule spec) + apply (rule sym) + apply (erule spec) + apply (subgoal_tac "ALL x y. x << (y:: ('a) lift) --> x=Undef | x=y") + prefer 2 apply (simp add: inst_lift_po) + apply (rule chain_mono2_po [THEN exE]) + apply fast + apply assumption + apply (rule_tac x = "Suc x" in exI) + apply (intro strip) + apply (rule disjE) + prefer 3 apply assumption + apply (rule mp) + apply (drule spec) + apply (erule spec) + apply (erule le_imp_less_or_eq [THEN disjE]) + apply (erule chain_mono) + apply auto + done + +theorem cpo_lift: "chain (Y::nat => 'a lift) ==> EX x. range Y <<| x" + apply (cut_tac flat_imp_chfin_poo) + apply (blast intro: lub_finch1) + done + +instance lift :: ("term") pcpo + apply intro_classes + apply (erule cpo_lift) + apply (rule least_lift) + done + +lemma inst_lift_pcpo: "UU = Undef" + -- {* For compatibility with old HOLCF-Version. *} + by (simp add: UU_def UU_lift_def) + + +subsection {* Lift as a datatype *} + +lemma lift_distinct1: "UU ~= Def x" + by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo) + +lemma lift_distinct2: "Def x ~= UU" + by (simp add: Undef_def Def_def Abs_lift_inject lift_def inst_lift_pcpo) + +lemma Def_inject: "(Def x = Def x') = (x = x')" + by (simp add: Def_def Abs_lift_inject lift_def) + +lemma lift_induct: "P UU ==> (!!x. P (Def x)) ==> P y" + apply (induct y) + apply (induct_tac y) + apply (simp_all add: Undef_def Def_def inst_lift_pcpo) + done + +rep_datatype lift + distinct lift_distinct1 lift_distinct2 + inject Def_inject + induction lift_induct + +lemma Def_not_UU: "Def a ~= UU" + by simp + + +subsection {* Further operations *} + +consts + flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)" + flift2 :: "('a => 'b) => ('a lift -> 'b lift)" + liftpair ::"'a::term lift * 'b::term lift => ('a * 'b) lift" -instance lift :: (term)flat (ax_flat_lift) +defs + flift1_def: + "flift1 f == (LAM x. (case x of + UU => UU + | Def y => (f y)))" + flift2_def: + "flift2 f == (LAM x. (case x of + UU => UU + | Def y => Def (f y)))" + liftpair_def: + "liftpair x == (case (cfst$x) of + UU => UU + | Def x1 => (case (csnd$x) of + UU => UU + | Def x2 => Def (x1,x2)))" + + +declare inst_lift_pcpo [symmetric, simp] + + +lemma less_lift: "(x::'a lift) << y = (x=y | x=UU)" + by (simp add: inst_lift_po) + + +text {* @{text UU} and @{text Def} *} + +lemma Lift_exhaust: "x = UU | (EX y. x = Def y)" + by (induct x) simp_all + +lemma Lift_cases: "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P" + by (insert Lift_exhaust) blast + +lemma not_Undef_is_Def: "(x ~= UU) = (EX y. x = Def y)" + by (cases x) simp_all + +text {* + For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text + x} by @{text "Def a"} in conclusion. *} + +ML {* + local val not_Undef_is_Def = thm "not_Undef_is_Def" + in val def_tac = SIMPSET' (fn ss => + etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss) + end; +*} + +lemma Undef_eq_UU: "Undef = UU" + by (rule inst_lift_pcpo [symmetric]) + +lemma DefE: "Def x = UU ==> R" + by simp + +lemma DefE2: "[| x = Def s; x = UU |] ==> R" + by simp + +lemma Def_inject_less_eq: "Def x << Def y = (x = y)" + by (simp add: less_lift_def) + +lemma Def_less_is_eq [simp]: "Def x << y = (Def x = y)" + by (simp add: less_lift) + + +subsection {* Lift is flat *} + +instance lift :: ("term") flat +proof + show "ALL x y::'a lift. x << y --> x = UU | x = y" + by (simp add: less_lift) +qed + +defaultsort pcpo + + +text {* + \medskip Two specific lemmas for the combination of LCF and HOL + terms. +*} + +lemma cont_Rep_CFun_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)" + apply (rule cont2cont_CF1L) + apply (tactic "resolve_tac cont_lemmas1 1")+ + apply auto + done + +lemma cont_Rep_CFun_app_app: "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)" + apply (rule cont2cont_CF1L) + apply (erule cont_Rep_CFun_app) + apply assumption + done -default pcpo +text {* Continuity of if-then-else. *} + +lemma cont_if: "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)" + by (cases b) simp_all + + +subsection {* Continuity Proofs for flift1, flift2, if *} + +text {* Need the instance of @{text flat}. *} + +lemma cont_flift1_arg: "cont (lift_case UU f)" + -- {* @{text flift1} is continuous in its argument itself. *} + apply (rule flatdom_strict2cont) + apply simp + done + +lemma cont_flift1_not_arg: "!!f. [| !! a. cont (%y. (f y) a) |] ==> + cont (%y. lift_case UU (f y))" + -- {* @{text flift1} is continuous in a variable that occurs only + in the @{text Def} branch. *} + apply (rule cont2cont_CF1L_rev) + apply (intro strip) + apply (case_tac y) + apply simp + apply simp + done + +lemma cont_flift1_arg_and_not_arg: "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> + cont (%y. lift_case UU (f y) (g y))" + -- {* @{text flift1} is continuous in a variable that occurs either + in the @{text Def} branch or in the argument. *} + apply (rule_tac tt = g in cont2cont_app) + apply (rule cont_flift1_not_arg) + apply auto + apply (rule cont_flift1_arg) + done + +lemma cont_flift2_arg: "cont (lift_case UU (%y. Def (f y)))" + -- {* @{text flift2} is continuous in its argument itself. *} + apply (rule flatdom_strict2cont) + apply simp + done + +text {* + \medskip Extension of cont_tac and installation of simplifier. +*} + +lemma cont2cont_CF1L_rev2: "(!!y. cont (%x. c1 x y)) ==> cont c1" + apply (rule cont2cont_CF1L_rev) + apply simp + done + +lemmas cont_lemmas_ext [simp] = + cont_flift1_arg cont_flift2_arg + cont_flift1_arg_and_not_arg cont2cont_CF1L_rev2 + cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if + +ML_setup {* +val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext"; + +fun cont_tac i = resolve_tac cont_lemmas2 i; +fun cont_tacR i = REPEAT (cont_tac i); + +local val flift1_def = thm "flift1_def" and flift2_def = thm "flift2_def" +in fun cont_tacRs i = + simp_tac (simpset() addsimps [flift1_def, flift2_def]) i THEN + REPEAT (cont_tac i) +end; + +simpset_ref() := simpset() addSolver + (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac))); +*} + + +subsection {* flift1, flift2 *} + +lemma flift1_Def [simp]: "flift1 f$(Def x) = (f x)" + by (simp add: flift1_def) + +lemma flift2_Def [simp]: "flift2 f$(Def x) = Def (f x)" + by (simp add: flift2_def) + +lemma flift1_UU [simp]: "flift1 f$UU = UU" + by (simp add: flift1_def) + +lemma flift2_UU [simp]: "flift2 f$UU = UU" + by (simp add: flift2_def) + +lemma flift2_nUU [simp]: "x~=UU ==> (flift2 f)$x~=UU" + by (tactic "def_tac 1") end - - - diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift1.ML --- a/src/HOLCF/Lift1.ML Sat Nov 03 01:36:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* Title: HOLCF/Lift1.ML - ID: $Id$ - Author: Olaf Mueller - Copyright 1996 Technische Universitaet Muenchen - -Theorems for Lift1.thy -*) - - -open Lift1; - -(* ------------------------------------------------------------------------ *) -(* less_lift is a partial order on type 'a -> 'b *) -(* ------------------------------------------------------------------------ *) - -Goalw [less_lift_def] "(x::'a lift) << x"; -by (fast_tac HOL_cs 1); -qed"refl_less_lift"; - -Goalw [less_lift_def] - "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2"; -by (fast_tac HOL_cs 1); -qed"antisym_less_lift"; - -Goalw [less_lift_def] - "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3"; -by (fast_tac HOL_cs 1); -qed"trans_less_lift"; diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift1.thy --- a/src/HOLCF/Lift1.thy Sat Nov 03 01:36:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -(* Title: HOLCF/Lift1.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1996 Technische Universitaet Muenchen - -Lifting types of class term to flat pcpo's -*) - -Lift1 = Cprod3 + Datatype + - -default term - -datatype 'a lift = Undef | Def 'a - -instance lift :: (term)sq_ord -defs - - less_lift_def "x << y == (x=y | x=Undef)" - -end diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift2.ML --- a/src/HOLCF/Lift2.ML Sat Nov 03 01:36:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -(* Title: HOLCF/Lift2.ML - ID: $Id$ - Author: Olaf Mueller - Copyright 1996 Technische Universitaet Muenchen - -Class Instance lift::(term)po -*) - -(* for compatibility with old HOLCF-Version *) -Goal "(op <<)=(%x y. x=y|x=Undef)"; -by (fold_goals_tac [less_lift_def]); -by (rtac refl 1); -qed "inst_lift_po"; - -(* -------------------------------------------------------------------------*) -(* type ('a)lift is pointed *) -(* ------------------------------------------------------------------------ *) - -Goal "Undef << x"; -by (simp_tac (simpset() addsimps [inst_lift_po]) 1); -qed"minimal_lift"; - -bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym); - -AddIffs [minimal_lift]; - -Goal "EX x::'a lift. ALL y. x< ~y=Undef"; -by (blast_tac (claset() addIs [antisym_less]) 1); -qed"notUndef_I"; - - -(* Tailoring chain_mono2 of Pcpo.ML to Undef *) - -Goal "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] \ -\ ==> EX j. ALL i. j~Y(i)=Undef"; -by Safe_tac; -by (Step_tac 1); -by (strip_tac 1); -by (rtac notUndef_I 1); -by (atac 2); -by (etac (chain_mono) 1); -by (atac 1); -qed"chain_mono2_po"; - - -(* Tailoring flat_imp_chfin of Fix.ML to lift *) - -Goal "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))"; -by (rewtac max_in_chain_def); -by (strip_tac 1); -by (res_inst_tac [("P","ALL i. Y(i)=Undef")] case_split_thm 1); -by (res_inst_tac [("x","0")] exI 1); -by (strip_tac 1); -by (rtac trans 1); -by (etac spec 1); -by (rtac sym 1); -by (etac spec 1); -by (subgoal_tac "ALL x y. x<<(y::('a)lift) --> x=Undef | x=y" 1); -by (simp_tac (simpset() addsimps [inst_lift_po]) 2); -by (rtac (chain_mono2_po RS exE) 1); -by (Fast_tac 1); -by (atac 1); -by (res_inst_tac [("x","Suc(x)")] exI 1); -by (strip_tac 1); -by (rtac disjE 1); -by (atac 3); -by (rtac mp 1); -by (dtac spec 1); -by (etac spec 1); -by (etac (le_imp_less_or_eq RS disjE) 1); -by (etac (chain_mono) 1); -by Auto_tac; -qed"flat_imp_chfin_poo"; - - -(* Main Lemma: cpo_lift *) - -Goal "chain(Y::nat=>('a)lift) ==> EX x. range(Y) <<|x"; -by (cut_inst_tac [] flat_imp_chfin_poo 1); -by (blast_tac (claset() addIs [lub_finch1]) 1); -qed"cpo_lift"; - - - diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift2.thy --- a/src/HOLCF/Lift2.thy Sat Nov 03 01:36:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: HOLCF/Lift2.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1996 Technische Universitaet Muenchen - -Class Instance lift::(term)po -*) - -Lift2 = Lift1 + - -instance "lift" :: (term)po (refl_less_lift,antisym_less_lift,trans_less_lift) - -end - - diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift3.ML --- a/src/HOLCF/Lift3.ML Sat Nov 03 01:36:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,155 +0,0 @@ -(* Title: HOLCF/Lift3.ML - ID: $Id$ - Author: Olaf Mueller - Copyright 1996 Technische Universitaet Muenchen - -Class Instance lift::(term)pcpo -*) - - -(* for compatibility with old HOLCF-Version *) -Goal "UU = Undef"; -by (simp_tac (HOL_ss addsimps [UU_def,UU_lift_def]) 1); -qed "inst_lift_pcpo"; - -(* ----------------------------------------------------------- *) -(* In lift.simps Undef is replaced by UU *) -(* Undef should be invisible from now on *) -(* ----------------------------------------------------------- *) - - -Addsimps [inst_lift_pcpo]; - -local - -val case1' = prove_goal thy "lift_case f1 f2 UU = f1" - (fn _ => [simp_tac (simpset() addsimps lift.simps) 1]); -val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a" - (fn _ => [Simp_tac 1]); -val distinct1' = prove_goal thy "UU ~= Def a" - (fn _ => [Simp_tac 1]); -val distinct2' = prove_goal thy "Def a ~= UU" - (fn _ => [Simp_tac 1]); -val inject' = prove_goal thy "(Def a = Def aa) = (a = aa)" - (fn _ => [Simp_tac 1]); -val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1" - (fn _ => [Simp_tac 1]); -val rec2' = prove_goal thy "lift_rec f1 f2 (Def a) = f2 a" - (fn _ => [Simp_tac 1]); -val induct' = prove_goal thy "[| P UU; !a. P (Def a) |] ==> P lift" - (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1, - etac Lift1.lift.induct 1,fast_tac HOL_cs 1]); - -in - -val Def_not_UU = distinct2'; - -structure lift = -struct -val cases = [case1',case2']; -val distinct = [distinct1',distinct2']; -val inject = [inject']; -val induct = allI RSN(2,induct'); -val recs = [rec1',rec2']; -val simps = cases@distinct@inject@recs; -fun induct_tac (s:string) (i:int) = - (res_inst_tac [("lift",s)] induct i); -end; - -end; (* local *) - -Delsimps Lift1.lift.simps; -Delsimps [inst_lift_pcpo]; -Addsimps [inst_lift_pcpo RS sym]; -Addsimps lift.simps; - - -(* --------------------------------------------------------*) - section"less_lift"; -(* --------------------------------------------------------*) - -Goal "(x::'a lift) << y = (x=y | x=UU)"; -by (stac inst_lift_po 1); -by (Simp_tac 1); -qed"less_lift"; - - -(* ---------------------------------------------------------- *) - section"UU and Def"; -(* ---------------------------------------------------------- *) - -Goal "x=UU | (? y. x=Def y)"; -by (lift.induct_tac "x" 1); -by (Asm_simp_tac 1); -by (rtac disjI2 1); -by (rtac exI 1); -by (Asm_simp_tac 1); -qed"Lift_exhaust"; - -val prems = Goal "[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"; -by (cut_facts_tac [Lift_exhaust] 1); -by (fast_tac (HOL_cs addSEs prems) 1); -qed"Lift_cases"; - -Goal "(x~=UU)=(? y. x=Def y)"; -by (rtac iffI 1); -by (rtac Lift_cases 1); -by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1)); -qed"not_Undef_is_Def"; - -(* For x~=UU in assumptions def_tac replaces x by (Def a) in conclusion *) -val def_tac = etac (not_Undef_is_Def RS iffD1 RS exE) THEN' Asm_simp_tac; - -bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym); - -Goal "Def x = UU ==> R"; -by (asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1); -qed "DefE"; - -Goal "[| x = Def s; x = UU |] ==> R"; -by (fast_tac (HOL_cs addSDs [DefE]) 1); -qed"DefE2"; - -Goal "Def x << Def y = (x = y)"; -by (stac (hd lift.inject RS sym) 1); -back(); -by (rtac iffI 1); -by (asm_full_simp_tac (simpset() addsimps [inst_lift_po] ) 1); -by (etac (antisym_less_inverse RS conjunct1) 1); -qed"Def_inject_less_eq"; - -Goal "Def x << y = (Def x = y)"; -by (simp_tac (simpset() addsimps [less_lift]) 1); -qed"Def_less_is_eq"; - -Addsimps [Def_less_is_eq]; - -(* ---------------------------------------------------------- *) - section"Lift is flat"; -(* ---------------------------------------------------------- *) - -Goal "! x y::'a lift. x << y --> x = UU | x = y"; -by (simp_tac (simpset() addsimps [less_lift]) 1); -qed"ax_flat_lift"; - -(* Two specific lemmas for the combination of LCF and HOL terms *) - -Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)"; -by (rtac cont2cont_CF1L 1); -by (REPEAT (resolve_tac cont_lemmas1 1)); -by Auto_tac; -qed"cont_Rep_CFun_app"; - -Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)"; -by (rtac cont2cont_CF1L 1); -by (etac cont_Rep_CFun_app 1); -by (assume_tac 1); -qed"cont_Rep_CFun_app_app"; - - -(* continuity of if then else *) -Goal "[| cont f1; cont f2 |] ==> cont (%x. if b then f1 x else f2 x)"; -by (case_tac "b" 1); -by Auto_tac; -qed"cont_if"; - diff -r edf306d60e4f -r 0b1d80ada4ab src/HOLCF/Lift3.thy --- a/src/HOLCF/Lift3.thy Sat Nov 03 01:36:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: HOLCF/Lift3.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1996 Technische Universitaet Muenchen - -Class Instance lift::(term)pcpo -*) - -Lift3 = Lift2 + - -instance lift :: (term)pcpo (cpo_lift,least_lift) - -consts - flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)" - flift2 :: "('a => 'b) => ('a lift -> 'b lift)" - - liftpair ::"'a::term lift * 'b::term lift => ('a * 'b) lift" - -translations - "UU" <= "Undef" - -defs - flift1_def - "flift1 f == (LAM x. (case x of - Undef => UU - | Def y => (f y)))" - flift2_def - "flift2 f == (LAM x. (case x of - Undef => UU - | Def y => Def (f y)))" - liftpair_def - "liftpair x == (case (cfst$x) of - Undef => UU - | Def x1 => (case (csnd$x) of - Undef => UU - | Def x2 => Def (x1,x2)))" - -end -