# HG changeset patch # User wenzelm # Date 1153182158 -7200 # Node ID 98acc6d0fab6e7e455b90225374d85709092cc0f # Parent 804927db5311d5e0b87177c659c205a1b17c8ef5 removed obsolete ML files; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/CCL.ML --- a/src/CCL/CCL.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,328 +0,0 @@ -(* Title: CCL/CCL.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -val ccl_data_defs = [apply_def,fix_def]; - -val CCL_ss = set_ss addsimps [po_refl]; - -(*** Congruence Rules ***) - -(*similar to AP_THM in Gordon's HOL*) -qed_goal "fun_cong" (the_context ()) "(f::'a=>'b) = g ==> f(x)=g(x)" - (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); - -(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) -qed_goal "arg_cong" (the_context ()) "x=y ==> f(x)=f(y)" - (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); - -Goal "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))"; -by (simp_tac (CCL_ss addsimps [eq_iff]) 1); -by (fast_tac (set_cs addIs [po_abstractn]) 1); -bind_thm("abstractn", standard (allI RS (result() RS mp))); - -fun type_of_terms (Const("Trueprop",_) $ - (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t; - -fun abs_prems thm = - let fun do_abs n thm (Type ("fun", [_,t])) = do_abs n (abstractn RSN (n,thm)) t - | do_abs n thm _ = thm - fun do_prems n [] thm = thm - | do_prems n (x::xs) thm = do_prems (n+1) xs (do_abs n thm (type_of_terms x)); - in do_prems 1 (prems_of thm) thm - end; - -val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot]; - -(*** Termination and Divergence ***) - -Goalw [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot"; -by (rtac iff_refl 1); -qed "Trm_iff"; - -Goalw [Trm_def,Dvg_def] "Dvg(t) <-> t = bot"; -by (rtac iff_refl 1); -qed "Dvg_iff"; - -(*** Constructors are injective ***) - -val prems = goal (the_context ()) - "[| x=a; y=b; x=y |] ==> a=b"; -by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals])))); -qed "eq_lemma"; - -fun mk_inj_rl thy rews s = - let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]); - val inj_lemmas = List.concat (map mk_inj_lemmas rews); - val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE - eresolve_tac inj_lemmas 1 ORELSE - asm_simp_tac (CCL_ss addsimps rews) 1) - in prove_goal thy s (fn _ => [tac]) - end; - -val ccl_injs = map (mk_inj_rl (the_context ()) caseBs) - [" = <-> (a=a' & b=b')", - "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"]; - -val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE; - -(*** Constructors are distinct ***) - -local - fun pairs_of f x [] = [] - | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys); - - fun mk_combs ff [] = [] - | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs; - -(* Doesn't handle binder types correctly *) - fun saturate thy sy name = - let fun arg_str 0 a s = s - | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")" - | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s); - val sg = sign_of thy; - val T = case Sign.const_type sg (Sign.intern_const (sign_of thy) sy) of - NONE => error(sy^" not declared") | SOME(T) => T; - val arity = length (fst (strip_type T)); - in sy ^ (arg_str arity name "") end; - - fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b"); - - val lemma = prove_goal (the_context ()) "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)" - (fn _ => [simp_tac CCL_ss 1]) RS mp; - fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL - [distinctness RS notE,sym RS (distinctness RS notE)]; -in - fun mk_lemmas rls = List.concat (map mk_lemma (mk_combs pair rls)); - fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs; -end; - - -val caseB_lemmas = mk_lemmas caseBs; - -val ccl_dstncts = - let fun mk_raw_dstnct_thm rls s = - prove_goal (the_context ()) s (fn _=> [rtac notI 1,eresolve_tac rls 1]) - in map (mk_raw_dstnct_thm caseB_lemmas) - (mk_dstnct_rls (the_context ()) ["bot","true","false","pair","lambda"]) end; - -fun mk_dstnct_thms thy defs inj_rls xs = - let fun mk_dstnct_thm rls s = prove_goalw thy defs s - (fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1]) - in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end; - -fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss); - -(*** Rewriting and Proving ***) - -fun XH_to_I rl = rl RS iffD2; -fun XH_to_D rl = rl RS iffD1; -val XH_to_E = make_elim o XH_to_D; -val XH_to_Is = map XH_to_I; -val XH_to_Ds = map XH_to_D; -val XH_to_Es = map XH_to_E; - -val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts; -val ccl_ss = CCL_ss addsimps ccl_rews; - -val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) - addSDs (XH_to_Ds ccl_injs); - -(****** Facts from gfp Definition of [= and = ******) - -val major::prems = goal (the_context ()) "[| A=B; a:B <-> P |] ==> a:A <-> P"; -by (resolve_tac (prems RL [major RS ssubst]) 1); -qed "XHlemma1"; - -Goal "(P(t,t') <-> Q) --> ( : {p. EX t t'. p= & P(t,t')} <-> Q)"; -by (fast_tac ccl_cs 1); -bind_thm("XHlemma2", result() RS mp); - -(*** Pre-Order ***) - -Goalw [POgen_def,SIM_def] "mono(%X. POgen(X))"; -by (rtac monoI 1); -by (safe_tac ccl_cs); -by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); -by (ALLGOALS (simp_tac ccl_ss)); -by (ALLGOALS (fast_tac set_cs)); -qed "POgen_mono"; - -Goalw [POgen_def,SIM_def] - " : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | \ -\ (EX a a' b b'. t= & t'= & : R & : R) | \ -\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))"; -by (rtac (iff_refl RS XHlemma2) 1); -qed "POgenXH"; - -Goal - "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \ -\ (EX a a' b b'. t= & t'= & a [= a' & b [= b') | \ -\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))"; -by (simp_tac (ccl_ss addsimps [PO_iff] delsimps ex_simps) 1); -by (rtac (rewrite_rule [POgen_def,SIM_def] - (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1); -by (rtac (iff_refl RS XHlemma2) 1); -qed "poXH"; - -Goal "bot [= b"; -by (rtac (poXH RS iffD2) 1); -by (simp_tac ccl_ss 1); -qed "po_bot"; - -Goal "a [= bot --> a=bot"; -by (rtac impI 1); -by (dtac (poXH RS iffD1) 1); -by (etac rev_mp 1); -by (simp_tac ccl_ss 1); -bind_thm("bot_poleast", result() RS mp); - -Goal " [= <-> a [= a' & b [= b'"; -by (rtac (poXH RS iff_trans) 1); -by (simp_tac ccl_ss 1); -qed "po_pair"; - -Goal "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))"; -by (rtac (poXH RS iff_trans) 1); -by (simp_tac ccl_ss 1); -by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1)); -by (asm_simp_tac ccl_ss 1); -by (fast_tac ccl_cs 1); -qed "po_lam"; - -val ccl_porews = [po_bot,po_pair,po_lam]; - -val [p1,p2,p3,p4,p5] = goal (the_context ()) - "[| t [= t'; a [= a'; b [= b'; !!x y. c(x,y) [= c'(x,y); \ -\ !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')"; -by (rtac (p1 RS po_cong RS po_trans) 1); -by (rtac (p2 RS po_cong RS po_trans) 1); -by (rtac (p3 RS po_cong RS po_trans) 1); -by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1); -by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] - (p5 RS po_abstractn RS po_cong RS po_trans) 1); -by (rtac po_refl 1); -qed "case_pocong"; - -val [p1,p2] = goalw (the_context ()) ccl_data_defs - "[| f [= f'; a [= a' |] ==> f ` a [= f' ` a'"; -by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1)); -qed "apply_pocong"; - - -val prems = goal (the_context ()) "~ lam x. b(x) [= bot"; -by (rtac notI 1); -by (dtac bot_poleast 1); -by (etac (distinctness RS notE) 1); -qed "npo_lam_bot"; - -val eq1::eq2::prems = goal (the_context ()) - "[| x=a; y=b; x[=y |] ==> a[=b"; -by (rtac (eq1 RS subst) 1); -by (rtac (eq2 RS subst) 1); -by (resolve_tac prems 1); -qed "po_lemma"; - -Goal "~ [= lam x. f(x)"; -by (rtac notI 1); -by (rtac (npo_lam_bot RS notE) 1); -by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1); -by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); -qed "npo_pair_lam"; - -Goal "~ lam x. f(x) [= "; -by (rtac notI 1); -by (rtac (npo_lam_bot RS notE) 1); -by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1); -by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); -qed "npo_lam_pair"; - -fun mk_thm s = prove_goal (the_context ()) s (fn _ => - [rtac notI 1,dtac case_pocong 1,etac rev_mp 5, - ALLGOALS (simp_tac ccl_ss), - REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]); - -val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm - ["~ true [= false", "~ false [= true", - "~ true [= ", "~ [= true", - "~ true [= lam x. f(x)","~ lam x. f(x) [= true", - "~ false [= ", "~ [= false", - "~ false [= lam x. f(x)","~ lam x. f(x) [= false"]; - -(* Coinduction for [= *) - -val prems = goal (the_context ()) "[| : R; R <= POgen(R) |] ==> t [= u"; -by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1); -by (REPEAT (ares_tac prems 1)); -qed "po_coinduct"; - -fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i; - -(*************** EQUALITY *******************) - -Goalw [EQgen_def,SIM_def] "mono(%X. EQgen(X))"; -by (rtac monoI 1); -by (safe_tac set_cs); -by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); -by (ALLGOALS (simp_tac ccl_ss)); -by (ALLGOALS (fast_tac set_cs)); -qed "EQgen_mono"; - -Goalw [EQgen_def,SIM_def] - " : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | \ -\ (t=false & t'=false) | \ -\ (EX a a' b b'. t= & t'= & : R & : R) | \ -\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))"; -by (rtac (iff_refl RS XHlemma2) 1); -qed "EQgenXH"; - -Goal - "t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \ -\ (EX a a' b b'. t= & t'= & a=a' & b=b') | \ -\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))"; -by (subgoal_tac - " : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \ -\ (EX a a' b b'. t= & t'= & : EQ & : EQ) | \ -\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : EQ))" 1); -by (etac rev_mp 1); -by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1); -by (rtac (rewrite_rule [EQgen_def,SIM_def] - (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1); -by (rtac (iff_refl RS XHlemma2) 1); -qed "eqXH"; - -val prems = goal (the_context ()) "[| : R; R <= EQgen(R) |] ==> t = u"; -by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1); -by (REPEAT (ares_tac prems 1)); -qed "eq_coinduct"; - -val prems = goal (the_context ()) - "[| : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u"; -by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1); -by (REPEAT (ares_tac (EQgen_mono::prems) 1)); -qed "eq_coinduct3"; - -fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i; -fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i; - -(*** Untyped Case Analysis and Other Facts ***) - -Goalw [apply_def] "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)"; -by (safe_tac ccl_cs); -by (simp_tac ccl_ss 1); -bind_thm("cond_eta", result() RS mp); - -Goal "(t=bot) | (t=true) | (t=false) | (EX a b. t=) | (EX f. t=lam x. f(x))"; -by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1); -by (fast_tac set_cs 1); -qed "exhaustion"; - -val prems = goal (the_context ()) - "[| P(bot); P(true); P(false); !!x y. P(); !!b. P(lam x. b(x)) |] ==> P(t)"; -by (cut_facts_tac [exhaustion] 1); -by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst])); -qed "term_case"; - -fun term_case_tac a i = res_inst_tac [("t",a)] term_case i; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/CCL.thy Tue Jul 18 02:22:38 2006 +0200 @@ -150,6 +150,344 @@ - wfd induction / coinduction and fixed point induction available *} -ML {* use_legacy_bindings (the_context ()) *} + +lemmas ccl_data_defs = apply_def fix_def + and [simp] = po_refl + + +subsection {* Congruence Rules *} + +(*similar to AP_THM in Gordon's HOL*) +lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" + by simp + +(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) +lemma arg_cong: "x=y ==> f(x)=f(y)" + by simp + +lemma abstractn: "(!!x. f(x) = g(x)) ==> f = g" + apply (simp add: eq_iff) + apply (blast intro: po_abstractn) + done + +lemmas caseBs = caseBtrue caseBfalse caseBpair caseBlam caseBbot + + +subsection {* Termination and Divergence *} + +lemma Trm_iff: "Trm(t) <-> ~ t = bot" + by (simp add: Trm_def Dvg_def) + +lemma Dvg_iff: "Dvg(t) <-> t = bot" + by (simp add: Trm_def Dvg_def) + + +subsection {* Constructors are injective *} + +lemma eq_lemma: "[| x=a; y=b; x=y |] ==> a=b" + by simp + +ML {* + local + val arg_cong = thm "arg_cong"; + val eq_lemma = thm "eq_lemma"; + val ss = simpset_of (the_context ()); + in + fun mk_inj_rl thy rews s = + let + fun mk_inj_lemmas r = [arg_cong] RL [r RS (r RS eq_lemma)] + val inj_lemmas = List.concat (map mk_inj_lemmas rews) + val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE + eresolve_tac inj_lemmas 1 ORELSE + asm_simp_tac (Simplifier.theory_context thy ss addsimps rews) 1) + in prove_goal thy s (fn _ => [tac]) end + end +*} + +ML {* + bind_thms ("ccl_injs", + map (mk_inj_rl (the_context ()) (thms "caseBs")) + [" = <-> (a=a' & b=b')", + "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"]) +*} + + +lemma pair_inject: " = \ (a = a' \ b = b' \ R) \ R" + by (simp add: ccl_injs) + + +subsection {* Constructors are distinct *} + +lemma lem: "t=t' ==> case(t,b,c,d,e) = case(t',b,c,d,e)" + by simp + +ML {* + +local + fun pairs_of f x [] = [] + | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys) + + fun mk_combs ff [] = [] + | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs + + (* Doesn't handle binder types correctly *) + fun saturate thy sy name = + let fun arg_str 0 a s = s + | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")" + | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s) + val T = Sign.the_const_type thy (Sign.intern_const thy sy); + val arity = length (fst (strip_type T)) + in sy ^ (arg_str arity name "") end + + fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b") + + val lemma = thm "lem"; + val eq_lemma = thm "eq_lemma"; + val distinctness = thm "distinctness"; + fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL + [distinctness RS notE,sym RS (distinctness RS notE)] +in + fun mk_lemmas rls = List.concat (map mk_lemma (mk_combs pair rls)) + fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs +end + +*} + +ML {* + +val caseB_lemmas = mk_lemmas (thms "caseBs") + +val ccl_dstncts = + let fun mk_raw_dstnct_thm rls s = + prove_goal (the_context ()) s (fn _=> [rtac notI 1,eresolve_tac rls 1]) + in map (mk_raw_dstnct_thm caseB_lemmas) + (mk_dstnct_rls (the_context ()) ["bot","true","false","pair","lambda"]) end + +fun mk_dstnct_thms thy defs inj_rls xs = + let fun mk_dstnct_thm rls s = prove_goalw thy defs s + (fn _ => [simp_tac (simpset_of thy addsimps (rls@inj_rls)) 1]) + in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end + +fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss) + +(*** Rewriting and Proving ***) + +fun XH_to_I rl = rl RS iffD2 +fun XH_to_D rl = rl RS iffD1 +val XH_to_E = make_elim o XH_to_D +val XH_to_Is = map XH_to_I +val XH_to_Ds = map XH_to_D +val XH_to_Es = map XH_to_E; + +bind_thms ("ccl_rews", thms "caseBs" @ ccl_injs @ ccl_dstncts); +bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]); +bind_thms ("ccl_injDs", XH_to_Ds (thms "ccl_injs")); +*} + +lemmas [simp] = ccl_rews + and [elim!] = pair_inject ccl_dstnctsEs + and [dest!] = ccl_injDs + + +subsection {* Facts from gfp Definition of @{text "[="} and @{text "="} *} + +lemma XHlemma1: "[| A=B; a:B <-> P |] ==> a:A <-> P" + by simp + +lemma XHlemma2: "(P(t,t') <-> Q) ==> ( : {p. EX t t'. p= & P(t,t')} <-> Q)" + by blast + + +subsection {* Pre-Order *} + +lemma POgen_mono: "mono(%X. POgen(X))" + apply (unfold POgen_def SIM_def) + apply (rule monoI) + apply blast + done + +lemma POgenXH: + " : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | + (EX a a' b b'. t= & t'= & : R & : R) | + (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))" + apply (unfold POgen_def SIM_def) + apply (rule iff_refl [THEN XHlemma2]) + done + +lemma poXH: + "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | + (EX a a' b b'. t= & t'= & a [= a' & b [= b') | + (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))" + apply (simp add: PO_iff del: ex_simps) + apply (rule POgen_mono + [THEN PO_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded POgen_def SIM_def]) + apply (rule iff_refl [THEN XHlemma2]) + done + +lemma po_bot: "bot [= b" + apply (rule poXH [THEN iffD2]) + apply simp + done + +lemma bot_poleast: "a [= bot ==> a=bot" + apply (drule poXH [THEN iffD1]) + apply simp + done + +lemma po_pair: " [= <-> a [= a' & b [= b'" + apply (rule poXH [THEN iff_trans]) + apply simp + done + +lemma po_lam: "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))" + apply (rule poXH [THEN iff_trans]) + apply fastsimp + done + +lemmas ccl_porews = po_bot po_pair po_lam + +lemma case_pocong: + assumes 1: "t [= t'" + and 2: "a [= a'" + and 3: "b [= b'" + and 4: "!!x y. c(x,y) [= c'(x,y)" + and 5: "!!u. d(u) [= d'(u)" + shows "case(t,a,b,c,d) [= case(t',a',b',c',d')" + apply (rule 1 [THEN po_cong, THEN po_trans]) + apply (rule 2 [THEN po_cong, THEN po_trans]) + apply (rule 3 [THEN po_cong, THEN po_trans]) + apply (rule 4 [THEN po_abstractn, THEN po_abstractn, THEN po_cong, THEN po_trans]) + apply (rule_tac f1 = "%d. case (t',a',b',c',d)" in + 5 [THEN po_abstractn, THEN po_cong, THEN po_trans]) + apply (rule po_refl) + done + +lemma apply_pocong: "[| f [= f'; a [= a' |] ==> f ` a [= f' ` a'" + unfolding ccl_data_defs + apply (rule case_pocong, (rule po_refl | assumption)+) + apply (erule po_cong) + done + +lemma npo_lam_bot: "~ lam x. b(x) [= bot" + apply (rule notI) + apply (drule bot_poleast) + apply (erule distinctness [THEN notE]) + done + +lemma po_lemma: "[| x=a; y=b; x[=y |] ==> a[=b" + by simp + +lemma npo_pair_lam: "~ [= lam x. f(x)" + apply (rule notI) + apply (rule npo_lam_bot [THEN notE]) + apply (erule case_pocong [THEN caseBlam [THEN caseBpair [THEN po_lemma]]]) + apply (rule po_refl npo_lam_bot)+ + done + +lemma npo_lam_pair: "~ lam x. f(x) [= " + apply (rule notI) + apply (rule npo_lam_bot [THEN notE]) + apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]]) + apply (rule po_refl npo_lam_bot)+ + done + +ML {* + +local + fun mk_thm s = prove_goal (the_context ()) s (fn _ => + [rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5, + ALLGOALS (simp_tac (simpset ())), + REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)]) +in + +val npo_rls = [thm "npo_pair_lam", thm "npo_lam_pair"] @ map mk_thm + ["~ true [= false", "~ false [= true", + "~ true [= ", "~ [= true", + "~ true [= lam x. f(x)","~ lam x. f(x) [= true", + "~ false [= ", "~ [= false", + "~ false [= lam x. f(x)","~ lam x. f(x) [= false"] +end; + +bind_thms ("npo_rls", npo_rls); +*} + + +subsection {* Coinduction for @{text "[="} *} + +lemma po_coinduct: "[| : R; R <= POgen(R) |] ==> t [= u" + apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]]) + apply assumption+ + done + +ML {* + local val po_coinduct = thm "po_coinduct" + in fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i end +*} + + +subsection {* Equality *} + +lemma EQgen_mono: "mono(%X. EQgen(X))" + apply (unfold EQgen_def SIM_def) + apply (rule monoI) + apply blast + done + +lemma EQgenXH: + " : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | + (t=false & t'=false) | + (EX a a' b b'. t= & t'= & : R & : R) | + (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))" + apply (unfold EQgen_def SIM_def) + apply (rule iff_refl [THEN XHlemma2]) + done + +lemma eqXH: + "t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | + (EX a a' b b'. t= & t'= & a=a' & b=b') | + (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))" + apply (subgoal_tac " : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | (EX a a' b b'. t= & t'= & : EQ & : EQ) | (EX f f'. t=lam x. f (x) & t'=lam x. f' (x) & (ALL x. : EQ))") + apply (erule rev_mp) + apply (simp add: EQ_iff [THEN iff_sym]) + apply (rule EQgen_mono [THEN EQ_def [THEN def_gfp_Tarski], THEN XHlemma1, + unfolded EQgen_def SIM_def]) + apply (rule iff_refl [THEN XHlemma2]) + done + +lemma eq_coinduct: "[| : R; R <= EQgen(R) |] ==> t = u" + apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]]) + apply assumption+ + done + +lemma eq_coinduct3: + "[| : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u" + apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]]) + apply (rule EQgen_mono | assumption)+ + done + +ML {* + local + val eq_coinduct = thm "eq_coinduct" + val eq_coinduct3 = thm "eq_coinduct3" + in + fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i + fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i + end +*} + + +subsection {* Untyped Case Analysis and Other Facts *} + +lemma cond_eta: "(EX f. t=lam x. f(x)) ==> t = lam x.(t ` x)" + by (auto simp: apply_def) + +lemma exhaustion: "(t=bot) | (t=true) | (t=false) | (EX a b. t=) | (EX f. t=lam x. f(x))" + apply (cut_tac refl [THEN eqXH [THEN iffD1]]) + apply blast + done + +lemma term_case: + "[| P(bot); P(true); P(false); !!x y. P(); !!b. P(lam x. b(x)) |] ==> P(t)" + using exhaustion [of t] by blast end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Fix.ML --- a/src/CCL/Fix.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,189 +0,0 @@ -(* Title: CCL/Fix.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -(*** Fixed Point Induction ***) - -val [base,step,incl] = goalw (the_context ()) [INCL_def] - "[| P(bot); !!x. P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))"; -by (rtac (incl RS spec RS mp) 1); -by (rtac (Nat_ind RS ballI) 1 THEN atac 1); -by (ALLGOALS (simp_tac term_ss)); -by (REPEAT (ares_tac [base,step] 1)); -qed "fix_ind"; - -(*** Inclusive Predicates ***) - -val prems = goalw (the_context ()) [INCL_def] - "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))"; -by (rtac iff_refl 1); -qed "inclXH"; - -val prems = goal (the_context ()) - "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))"; -by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1); -qed "inclI"; - -val incl::prems = goal (the_context ()) - "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))"; -by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] - @ prems)) 1); -qed "inclD"; - -val incl::prems = goal (the_context ()) - "[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R"; -by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1); -qed "inclE"; - - -(*** Lemmas for Inclusive Predicates ***) - -Goal "INCL(%x.~ a(x) [= t)"; -by (rtac inclI 1); -by (dtac bspec 1); -by (rtac zeroT 1); -by (etac contrapos 1); -by (rtac po_trans 1); -by (assume_tac 2); -by (stac napplyBzero 1); -by (rtac po_cong 1 THEN rtac po_bot 1); -qed "npo_INCL"; - -val prems = goal (the_context ()) "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))"; -by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; -qed "conj_INCL"; - -val prems = goal (the_context ()) "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))"; -by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; -qed "all_INCL"; - -val prems = goal (the_context ()) "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))"; -by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; -qed "ball_INCL"; - -Goal "INCL(%x. a(x) = (b(x)::'a::prog))"; -by (simp_tac (term_ss addsimps [eq_iff]) 1); -by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1)); -qed "eq_INCL"; - -(*** Derivation of Reachability Condition ***) - -(* Fixed points of idgen *) - -Goal "idgen(fix(idgen)) = fix(idgen)"; -by (rtac (fixB RS sym) 1); -qed "fix_idgenfp"; - -Goalw [idgen_def] "idgen(lam x. x) = lam x. x"; -by (simp_tac term_ss 1); -by (rtac (term_case RS allI) 1); -by (ALLGOALS (simp_tac term_ss)); -qed "id_idgenfp"; - -(* All fixed points are lam-expressions *) - -val [prem] = goal (the_context ()) "idgen(d) = d ==> d = lam x.?f(x)"; -by (rtac (prem RS subst) 1); -by (rewtac idgen_def); -by (rtac refl 1); -qed "idgenfp_lam"; - -(* Lemmas for rewriting fixed points of idgen *) - -val prems = goalw (the_context ()) [idgen_def] - "[| a = b; a ` t = u |] ==> b ` t = u"; -by (simp_tac (term_ss addsimps (prems RL [sym])) 1); -qed "l_lemma"; - -val idgen_lemmas = - let fun mk_thm s = prove_goalw (the_context ()) [idgen_def] s - (fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1]) - in map mk_thm - [ "idgen(d) = d ==> d ` bot = bot", - "idgen(d) = d ==> d ` true = true", - "idgen(d) = d ==> d ` false = false", - "idgen(d) = d ==> d ` = ", - "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"] - end; - -(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points - of idgen and hence are they same *) - -val [p1,p2,p3] = goal (the_context ()) - "[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u"; -by (stac (p2 RS cond_eta) 1); -by (stac (p3 RS cond_eta) 1); -by (rtac (p1 RS (po_lam RS iffD2)) 1); -qed "po_eta"; - -val [prem] = goalw (the_context ()) [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)"; -by (rtac (prem RS subst) 1); -by (rtac refl 1); -qed "po_eta_lemma"; - -val [prem] = goal (the_context ()) - "idgen(d) = d ==> \ -\ {p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)} <= \ -\ POgen({p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)})"; -by (REPEAT (step_tac term_cs 1)); -by (term_case_tac "t" 1); -by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas))))); -by (ALLGOALS (fast_tac set_cs)); -qed "lemma1"; - -val [prem] = goal (the_context ()) - "idgen(d) = d ==> fix(idgen) [= d"; -by (rtac (allI RS po_eta) 1); -by (rtac (lemma1 RSN(2,po_coinduct)) 1); -by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); -qed "fix_least_idgen"; - -val [prem] = goal (the_context ()) - "idgen(d) = d ==> \ -\ {p. EX a b. p= & b = d ` a} <= POgen({p. EX a b. p= & b = d ` a})"; -by (REPEAT (step_tac term_cs 1)); -by (term_case_tac "a" 1); -by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas))))); -by (ALLGOALS (fast_tac set_cs)); -qed "lemma2"; - -val [prem] = goal (the_context ()) - "idgen(d) = d ==> lam x. x [= d"; -by (rtac (allI RS po_eta) 1); -by (rtac (lemma2 RSN(2,po_coinduct)) 1); -by (simp_tac term_ss 1); -by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); -qed "id_least_idgen"; - -Goal "fix(idgen) = lam x. x"; -by (fast_tac (term_cs addIs [eq_iff RS iffD2, - id_idgenfp RS fix_least_idgen, - fix_idgenfp RS id_least_idgen]) 1); -qed "reachability"; - -(********) - -val [prem] = goal (the_context ()) "f = lam x. x ==> f`t = t"; -by (rtac (prem RS sym RS subst) 1); -by (rtac applyB 1); -qed "id_apply"; - -val prems = goal (the_context ()) - "[| P(bot); P(true); P(false); \ -\ !!x y.[| P(x); P(y) |] ==> P(); \ -\ !!u.(!!x. P(u(x))) ==> P(lam x. u(x)); INCL(P) |] ==> \ -\ P(t)"; -by (rtac (reachability RS id_apply RS subst) 1); -by (res_inst_tac [("x","t")] spec 1); -by (rtac fix_ind 1); -by (rewtac idgen_def); -by (REPEAT_SOME (ares_tac [allI])); -by (stac applyBbot 1); -by (resolve_tac prems 1); -by (rtac (applyB RS ssubst) 1); -by (res_inst_tac [("t","xa")] term_case 1); -by (ALLGOALS (simp_tac term_ss)); -by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems)))); -qed "term_ind"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Fix.thy --- a/src/CCL/Fix.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Fix.thy Tue Jul 18 02:22:38 2006 +0200 @@ -22,6 +22,181 @@ po_INCL: "INCL(%x. a(x) [= b(x))" INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" -ML {* use_legacy_bindings (the_context ()) *} + +subsection {* Fixed Point Induction *} + +lemma fix_ind: + assumes base: "P(bot)" + and step: "!!x. P(x) ==> P(f(x))" + and incl: "INCL(P)" + shows "P(fix(f))" + apply (rule incl [unfolded INCL_def, rule_format]) + apply (rule Nat_ind [THEN ballI], assumption) + apply simp_all + apply (rule base) + apply (erule step) + done + + +subsection {* Inclusive Predicates *} + +lemma inclXH: "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))" + by (simp add: INCL_def) + +lemma inclI: "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))" + unfolding inclXH by blast + +lemma inclD: "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))" + unfolding inclXH by blast + +lemma inclE: "[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R" + by (blast dest: inclD) + + +subsection {* Lemmas for Inclusive Predicates *} + +lemma npo_INCL: "INCL(%x.~ a(x) [= t)" + apply (rule inclI) + apply (drule bspec) + apply (rule zeroT) + apply (erule contrapos) + apply (rule po_trans) + prefer 2 + apply assumption + apply (subst napplyBzero) + apply (rule po_cong, rule po_bot) + done + +lemma conj_INCL: "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))" + by (blast intro!: inclI dest!: inclD) + +lemma all_INCL: "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))" + by (blast intro!: inclI dest!: inclD) + +lemma ball_INCL: "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))" + by (blast intro!: inclI dest!: inclD) + +lemma eq_INCL: "INCL(%x. a(x) = (b(x)::'a::prog))" + apply (simp add: eq_iff) + apply (rule conj_INCL po_INCL)+ + done + + +subsection {* Derivation of Reachability Condition *} + +(* Fixed points of idgen *) + +lemma fix_idgenfp: "idgen(fix(idgen)) = fix(idgen)" + apply (rule fixB [symmetric]) + done + +lemma id_idgenfp: "idgen(lam x. x) = lam x. x" + apply (simp add: idgen_def) + apply (rule term_case [THEN allI]) + apply simp_all + done + +(* All fixed points are lam-expressions *) + +lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)" + apply (unfold idgen_def) + apply (erule ssubst) + apply (rule refl) + done + +(* Lemmas for rewriting fixed points of idgen *) + +lemma l_lemma: "[| a = b; a ` t = u |] ==> b ` t = u" + by (simp add: idgen_def) + +lemma idgen_lemmas: + "idgen(d) = d ==> d ` bot = bot" + "idgen(d) = d ==> d ` true = true" + "idgen(d) = d ==> d ` false = false" + "idgen(d) = d ==> d ` = " + "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)" + by (erule l_lemma, simp add: idgen_def)+ + + +(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points + of idgen and hence are they same *) + +lemma po_eta: + "[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u" + apply (drule cond_eta)+ + apply (erule ssubst) + apply (erule ssubst) + apply (rule po_lam [THEN iffD2]) + apply simp + done + +lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)" + apply (unfold idgen_def) + apply (erule sym) + done + +lemma lemma1: + "idgen(d) = d ==> + {p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)} <= + POgen({p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)})" + apply clarify + apply (rule_tac t = t in term_case) + apply (simp_all add: POgenXH idgen_lemmas idgen_lemmas [OF fix_idgenfp]) + apply blast + apply fast + done + +lemma fix_least_idgen: "idgen(d) = d ==> fix(idgen) [= d" + apply (rule allI [THEN po_eta]) + apply (rule lemma1 [THEN [2] po_coinduct]) + apply (blast intro: po_eta_lemma fix_idgenfp)+ + done + +lemma lemma2: + "idgen(d) = d ==> + {p. EX a b. p= & b = d ` a} <= POgen({p. EX a b. p= & b = d ` a})" + apply clarify + apply (rule_tac t = a in term_case) + apply (simp_all add: POgenXH idgen_lemmas) + apply fast + done + +lemma id_least_idgen: "idgen(d) = d ==> lam x. x [= d" + apply (rule allI [THEN po_eta]) + apply (rule lemma2 [THEN [2] po_coinduct]) + apply simp + apply (fast intro: po_eta_lemma fix_idgenfp)+ + done + +lemma reachability: "fix(idgen) = lam x. x" + apply (fast intro: eq_iff [THEN iffD2] + id_idgenfp [THEN fix_least_idgen] fix_idgenfp [THEN id_least_idgen]) + done + +(********) + +lemma id_apply: "f = lam x. x ==> f`t = t" + apply (erule ssubst) + apply (rule applyB) + done + +lemma term_ind: + assumes "P(bot)" "P(true)" "P(false)" + "!!x y.[| P(x); P(y) |] ==> P()" + "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))" "INCL(P)" + shows "P(t)" + apply (rule reachability [THEN id_apply, THEN subst]) + apply (rule_tac x = t in spec) + apply (rule fix_ind) + apply (unfold idgen_def) + apply (rule allI) + apply (subst applyBbot) + apply assumption + apply (rule allI) + apply (rule applyB [THEN ssubst]) + apply (rule_tac t = "xa" in term_case) + apply simp_all + apply (fast intro: prems INCL_subst all_INCL)+ + done end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Gfp.ML --- a/src/CCL/Gfp.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,125 +0,0 @@ -(* Title: CCL/Gfp.ML - ID: $Id$ -*) - -(*** Proof of Knaster-Tarski Theorem using gfp ***) - -(* gfp(f) is the least upper bound of {u. u <= f(u)} *) - -val prems = goalw (the_context ()) [gfp_def] "[| A <= f(A) |] ==> A <= gfp(f)"; -by (rtac (CollectI RS Union_upper) 1); -by (resolve_tac prems 1); -qed "gfp_upperbound"; - -val prems = goalw (the_context ()) [gfp_def] - "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A"; -by (REPEAT (ares_tac ([Union_least]@prems) 1)); -by (etac CollectD 1); -qed "gfp_least"; - -val [mono] = goal (the_context ()) "mono(f) ==> gfp(f) <= f(gfp(f))"; -by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, - rtac (mono RS monoD), rtac gfp_upperbound, atac]); -qed "gfp_lemma2"; - -val [mono] = goal (the_context ()) "mono(f) ==> f(gfp(f)) <= gfp(f)"; -by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), - rtac gfp_lemma2, rtac mono]); -qed "gfp_lemma3"; - -val [mono] = goal (the_context ()) "mono(f) ==> gfp(f) = f(gfp(f))"; -by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1)); -qed "gfp_Tarski"; - -(*** Coinduction rules for greatest fixed points ***) - -(*weak version*) -val prems = goal (the_context ()) - "[| a: A; A <= f(A) |] ==> a : gfp(f)"; -by (rtac (gfp_upperbound RS subsetD) 1); -by (REPEAT (ares_tac prems 1)); -qed "coinduct"; - -val [prem,mono] = goal (the_context ()) - "[| A <= f(A) Un gfp(f); mono(f) |] ==> \ -\ A Un gfp(f) <= f(A Un gfp(f))"; -by (rtac subset_trans 1); -by (rtac (mono RS mono_Un) 2); -by (rtac (mono RS gfp_Tarski RS subst) 1); -by (rtac (prem RS Un_least) 1); -by (rtac Un_upper2 1); -qed "coinduct2_lemma"; - -(*strong version, thanks to Martin Coen*) -val ainA::prems = goal (the_context ()) - "[| a: A; A <= f(A) Un gfp(f); mono(f) |] ==> a : gfp(f)"; -by (rtac coinduct 1); -by (rtac (prems MRS coinduct2_lemma) 2); -by (resolve_tac [ainA RS UnI1] 1); -qed "coinduct2"; - -(*** Even Stronger version of coinduct [by Martin Coen] - - instead of the condition A <= f(A) - consider A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***) - -val [prem] = goal (the_context ()) "mono(f) ==> mono(%x. f(x) Un A Un B)"; -by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1)); -qed "coinduct3_mono_lemma"; - -val [prem,mono] = goal (the_context ()) - "[| A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> \ -\ lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))"; -by (rtac subset_trans 1); -by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1); -by (rtac (Un_least RS Un_least) 1); -by (rtac subset_refl 1); -by (rtac prem 1); -by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1); -by (rtac (mono RS monoD) 1); -by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); -by (rtac Un_upper2 1); -qed "coinduct3_lemma"; - -val ainA::prems = goal (the_context ()) - "[| a:A; A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)"; -by (rtac coinduct 1); -by (rtac (prems MRS coinduct3_lemma) 2); -by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1); -by (rtac (ainA RS UnI2 RS UnI1) 1); -qed "coinduct3"; - - -(** Definition forms of gfp_Tarski, to control unfolding **) - -val [rew,mono] = goal (the_context ()) "[| h==gfp(f); mono(f) |] ==> h = f(h)"; -by (rewtac rew); -by (rtac (mono RS gfp_Tarski) 1); -qed "def_gfp_Tarski"; - -val rew::prems = goal (the_context ()) - "[| h==gfp(f); a:A; A <= f(A) |] ==> a: h"; -by (rewtac rew); -by (REPEAT (ares_tac (prems @ [coinduct]) 1)); -qed "def_coinduct"; - -val rew::prems = goal (the_context ()) - "[| h==gfp(f); a:A; A <= f(A) Un h; mono(f) |] ==> a: h"; -by (rewtac rew); -by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct2]) 1)); -qed "def_coinduct2"; - -val rew::prems = goal (the_context ()) - "[| h==gfp(f); a:A; A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h"; -by (rewtac rew); -by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1)); -qed "def_coinduct3"; - -(*Monotonicity of gfp!*) -val prems = goal (the_context ()) - "[| mono(f); !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; -by (rtac gfp_upperbound 1); -by (rtac subset_trans 1); -by (rtac gfp_lemma2 1); -by (resolve_tac prems 1); -by (resolve_tac prems 1); -qed "gfp_mono"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Gfp.thy --- a/src/CCL/Gfp.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Gfp.thy Tue Jul 18 02:22:38 2006 +0200 @@ -10,10 +10,124 @@ imports Lfp begin -constdefs +definition gfp :: "['a set=>'a set] => 'a set" (*greatest fixed point*) "gfp(f) == Union({u. u <= f(u)})" -ML {* use_legacy_bindings (the_context ()) *} +(* gfp(f) is the least upper bound of {u. u <= f(u)} *) + +lemma gfp_upperbound: "[| A <= f(A) |] ==> A <= gfp(f)" + unfolding gfp_def by blast + +lemma gfp_least: "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A" + unfolding gfp_def by blast + +lemma gfp_lemma2: "mono(f) ==> gfp(f) <= f(gfp(f))" + by (rule gfp_least, rule subset_trans, assumption, erule monoD, + rule gfp_upperbound, assumption) + +lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) <= gfp(f)" + by (rule gfp_upperbound, frule monoD, rule gfp_lemma2, assumption+) + +lemma gfp_Tarski: "mono(f) ==> gfp(f) = f(gfp(f))" + by (rule equalityI gfp_lemma2 gfp_lemma3 | assumption)+ + + +(*** Coinduction rules for greatest fixed points ***) + +(*weak version*) +lemma coinduct: "[| a: A; A <= f(A) |] ==> a : gfp(f)" + by (blast dest: gfp_upperbound) + +lemma coinduct2_lemma: + "[| A <= f(A) Un gfp(f); mono(f) |] ==> + A Un gfp(f) <= f(A Un gfp(f))" + apply (rule subset_trans) + prefer 2 + apply (erule mono_Un) + apply (rule subst, erule gfp_Tarski) + apply (erule Un_least) + apply (rule Un_upper2) + done + +(*strong version, thanks to Martin Coen*) +lemma coinduct2: + "[| a: A; A <= f(A) Un gfp(f); mono(f) |] ==> a : gfp(f)" + apply (rule coinduct) + prefer 2 + apply (erule coinduct2_lemma, assumption) + apply blast + done + +(*** Even Stronger version of coinduct [by Martin Coen] + - instead of the condition A <= f(A) + consider A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***) + +lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un A Un B)" + by (rule monoI) (blast dest: monoD) + +lemma coinduct3_lemma: + assumes prem: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))" + and mono: "mono(f)" + shows "lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))" + apply (rule subset_trans) + apply (rule mono [THEN coinduct3_mono_lemma, THEN lfp_lemma3]) + apply (rule Un_least [THEN Un_least]) + apply (rule subset_refl) + apply (rule prem) + apply (rule mono [THEN gfp_Tarski, THEN equalityD1, THEN subset_trans]) + apply (rule mono [THEN monoD]) + apply (subst mono [THEN coinduct3_mono_lemma, THEN lfp_Tarski]) + apply (rule Un_upper2) + done + +lemma coinduct3: + assumes 1: "a:A" + and 2: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))" + and 3: "mono(f)" + shows "a : gfp(f)" + apply (rule coinduct) + prefer 2 + apply (rule coinduct3_lemma [OF 2 3]) + apply (subst lfp_Tarski [OF coinduct3_mono_lemma, OF 3]) + using 1 apply blast + done + + +subsection {* Definition forms of @{text "gfp_Tarski"}, to control unfolding *} + +lemma def_gfp_Tarski: "[| h==gfp(f); mono(f) |] ==> h = f(h)" + apply unfold + apply (erule gfp_Tarski) + done + +lemma def_coinduct: "[| h==gfp(f); a:A; A <= f(A) |] ==> a: h" + apply unfold + apply (erule coinduct) + apply assumption + done + +lemma def_coinduct2: "[| h==gfp(f); a:A; A <= f(A) Un h; mono(f) |] ==> a: h" + apply unfold + apply (erule coinduct2) + apply assumption + apply assumption + done + +lemma def_coinduct3: "[| h==gfp(f); a:A; A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h" + apply unfold + apply (erule coinduct3) + apply assumption + apply assumption + done + +(*Monotonicity of gfp!*) +lemma gfp_mono: "[| mono(f); !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)" + apply (rule gfp_upperbound) + apply (rule subset_trans) + apply (rule gfp_lemma2) + apply assumption + apply (erule meta_spec) + done end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Hered.ML --- a/src/CCL/Hered.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,190 +0,0 @@ -(* Title: CCL/Hered.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t; - -(*** Hereditary Termination ***) - -Goalw [HTTgen_def] "mono(%X. HTTgen(X))"; -by (rtac monoI 1); -by (fast_tac set_cs 1); -qed "HTTgen_mono"; - -Goalw [HTTgen_def] - "t : HTTgen(A) <-> t=true | t=false | (EX a b. t= & a : A & b : A) | \ -\ (EX f. t=lam x. f(x) & (ALL x. f(x) : A))"; -by (fast_tac set_cs 1); -qed "HTTgenXH"; - -Goal - "t : HTT <-> t=true | t=false | (EX a b. t= & a : HTT & b : HTT) | \ -\ (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))"; -by (rtac (rewrite_rule [HTTgen_def] - (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1); -by (fast_tac set_cs 1); -qed "HTTXH"; - -(*** Introduction Rules for HTT ***) - -Goal "~ bot : HTT"; -by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1); -qed "HTT_bot"; - -Goal "true : HTT"; -by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1); -qed "HTT_true"; - -Goal "false : HTT"; -by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1); -qed "HTT_false"; - -Goal " : HTT <-> a : HTT & b : HTT"; -by (rtac (HTTXH RS iff_trans) 1); -by (fast_tac term_cs 1); -qed "HTT_pair"; - -Goal "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)"; -by (rtac (HTTXH RS iff_trans) 1); -by (simp_tac term_ss 1); -by (safe_tac term_cs); -by (asm_simp_tac term_ss 1); -by (fast_tac term_cs 1); -qed "HTT_lam"; - -local - val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam]; - fun mk_thm s = prove_goalw (the_context ()) data_defs s (fn _ => - [simp_tac (term_ss addsimps raw_HTTrews) 1]); -in - val HTT_rews = raw_HTTrews @ - map mk_thm ["one : HTT", - "inl(a) : HTT <-> a : HTT", - "inr(b) : HTT <-> b : HTT", - "zero : HTT", - "succ(n) : HTT <-> n : HTT", - "[] : HTT", - "x$xs : HTT <-> x : HTT & xs : HTT"]; -end; - -val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]); - -(*** Coinduction for HTT ***) - -val prems = goal (the_context ()) "[| t : R; R <= HTTgen(R) |] ==> t : HTT"; -by (rtac (HTT_def RS def_coinduct) 1); -by (REPEAT (ares_tac prems 1)); -qed "HTT_coinduct"; - -fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i; - -val prems = goal (the_context ()) - "[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"; -by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1); -by (REPEAT (ares_tac prems 1)); -qed "HTT_coinduct3"; -val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3; - -fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i; - -val HTTgenIs = map (mk_genIs (the_context ()) data_defs HTTgenXH HTTgen_mono) - ["true : HTTgen(R)", - "false : HTTgen(R)", - "[| a : R; b : R |] ==> : HTTgen(R)", - "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)", - "one : HTTgen(R)", - "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \ -\ inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", - "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> \ -\ inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", - "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", - "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> \ -\ succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", - "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", - "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\ -\ h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"]; - -(*** Formation Rules for Types ***) - -Goal "Unit <= HTT"; -by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1); -qed "UnitF"; - -Goal "Bool <= HTT"; -by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1); -by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); -qed "BoolF"; - -val prems = goal (the_context ()) "[| A <= HTT; B <= HTT |] ==> A + B <= HTT"; -by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1); -by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); -qed "PlusF"; - -val prems = goal (the_context ()) - "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"; -by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1); -by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); -qed "SigmaF"; - -(*** Formation Rules for Recursive types - using coinduction these only need ***) -(*** exhaution rule for type-former ***) - -(*Proof by induction - needs induction rule for type*) -Goal "Nat <= HTT"; -by (simp_tac (term_ss addsimps [subsetXH]) 1); -by (safe_tac set_cs); -by (etac Nat_ind 1); -by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])))); -val NatF = result(); - -Goal "Nat <= HTT"; -by (safe_tac set_cs); -by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addIs HTTgenIs - addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1); -qed "NatF"; - -val [prem] = goal (the_context ()) "A <= HTT ==> List(A) <= HTT"; -by (safe_tac set_cs); -by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addSIs HTTgenIs - addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] - addEs [XH_to_E ListXH]) 1); -qed "ListF"; - -val [prem] = goal (the_context ()) "A <= HTT ==> Lists(A) <= HTT"; -by (safe_tac set_cs); -by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addSIs HTTgenIs - addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] - addEs [XH_to_E ListsXH]) 1); -qed "ListsF"; - -val [prem] = goal (the_context ()) "A <= HTT ==> ILists(A) <= HTT"; -by (safe_tac set_cs); -by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addSIs HTTgenIs - addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] - addEs [XH_to_E IListsXH]) 1); -qed "IListsF"; - -(*** A possible use for this predicate is proving equality from pre-order ***) -(*** but it seems as easy (and more general) to do this directly by coinduction ***) -(* -val prems = goal (the_context ()) "[| t : HTT; t [= u |] ==> u [= t"; -by (po_coinduct_tac "{p. EX a b. p= & b : HTT & b [= a}" 1); -by (fast_tac (ccl_cs addIs prems) 1); -by (safe_tac ccl_cs); -by (dtac (poXH RS iffD1) 1); -by (safe_tac (set_cs addSEs [HTT_bot RS notE])); -by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp)); -by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews))); -by (ALLGOALS (fast_tac ccl_cs)); -qed "HTT_po_op"; - -val prems = goal (the_context ()) "[| t : HTT; t [= u |] ==> t = u"; -by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1)); -qed "HTT_po_eq"; -*) diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Hered.thy --- a/src/CCL/Hered.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Hered.thy Tue Jul 18 02:22:38 2006 +0200 @@ -8,7 +8,6 @@ theory Hered imports Type -uses "coinduction.ML" begin text {* @@ -30,6 +29,166 @@ (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}" HTT_def: "HTT == gfp(HTTgen)" -ML {* use_legacy_bindings (the_context ()) *} + +subsection {* Hereditary Termination *} + +lemma HTTgen_mono: "mono(%X. HTTgen(X))" + apply (unfold HTTgen_def) + apply (rule monoI) + apply blast + done + +lemma HTTgenXH: + "t : HTTgen(A) <-> t=true | t=false | (EX a b. t= & a : A & b : A) | + (EX f. t=lam x. f(x) & (ALL x. f(x) : A))" + apply (unfold HTTgen_def) + apply blast + done + +lemma HTTXH: + "t : HTT <-> t=true | t=false | (EX a b. t= & a : HTT & b : HTT) | + (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))" + apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def]) + apply blast + done + + +subsection {* Introduction Rules for HTT *} + +lemma HTT_bot: "~ bot : HTT" + by (blast dest: HTTXH [THEN iffD1]) + +lemma HTT_true: "true : HTT" + by (blast intro: HTTXH [THEN iffD2]) + +lemma HTT_false: "false : HTT" + by (blast intro: HTTXH [THEN iffD2]) + +lemma HTT_pair: " : HTT <-> a : HTT & b : HTT" + apply (rule HTTXH [THEN iff_trans]) + apply blast + done + +lemma HTT_lam: "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)" + apply (rule HTTXH [THEN iff_trans]) + apply auto + done + +lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam + +lemma HTT_rews2: + "one : HTT" + "inl(a) : HTT <-> a : HTT" + "inr(b) : HTT <-> b : HTT" + "zero : HTT" + "succ(n) : HTT <-> n : HTT" + "[] : HTT" + "x$xs : HTT <-> x : HTT & xs : HTT" + by (simp_all add: data_defs HTT_rews1) + +lemmas HTT_rews = HTT_rews1 HTT_rews2 + + +subsection {* Coinduction for HTT *} + +lemma HTT_coinduct: "[| t : R; R <= HTTgen(R) |] ==> t : HTT" + apply (erule HTT_def [THEN def_coinduct]) + apply assumption + done + +ML {* + local val HTT_coinduct = thm "HTT_coinduct" + in fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] HTT_coinduct i end +*} + +lemma HTT_coinduct3: + "[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT" + apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]]) + apply assumption + done + +ML {* +local + val HTT_coinduct3 = thm "HTT_coinduct3" + val HTTgen_def = thm "HTTgen_def" +in + +val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3 + +fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i + +val HTTgenIs = + map (mk_genIs (the_context ()) (thms "data_defs") (thm "HTTgenXH") (thm "HTTgen_mono")) + ["true : HTTgen(R)", + "false : HTTgen(R)", + "[| a : R; b : R |] ==> : HTTgen(R)", + "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)", + "one : HTTgen(R)", + "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", + "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", + "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", + "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", + "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))", + "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==> h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"] end +*} + +ML {* bind_thms ("HTTgenIs", HTTgenIs) *} + + +subsection {* Formation Rules for Types *} + +lemma UnitF: "Unit <= HTT" + by (simp add: subsetXH UnitXH HTT_rews) + +lemma BoolF: "Bool <= HTT" + by (fastsimp simp: subsetXH BoolXH iff: HTT_rews) + +lemma PlusF: "[| A <= HTT; B <= HTT |] ==> A + B <= HTT" + by (fastsimp simp: subsetXH PlusXH iff: HTT_rews) + +lemma SigmaF: "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT" + by (fastsimp simp: subsetXH SgXH HTT_rews) + + +(*** Formation Rules for Recursive types - using coinduction these only need ***) +(*** exhaution rule for type-former ***) + +(*Proof by induction - needs induction rule for type*) +lemma "Nat <= HTT" + apply (simp add: subsetXH) + apply clarify + apply (erule Nat_ind) + apply (fastsimp iff: HTT_rews)+ + done + +lemma NatF: "Nat <= HTT" + apply clarify + apply (erule HTT_coinduct3) + apply (fast intro: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] dest: NatXH [THEN iffD1]) + done + +lemma ListF: "A <= HTT ==> List(A) <= HTT" + apply clarify + apply (erule HTT_coinduct3) + apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] + subsetD [THEN HTTgen_mono [THEN ci3_AI]] + dest: ListXH [THEN iffD1]) + done + +lemma ListsF: "A <= HTT ==> Lists(A) <= HTT" + apply clarify + apply (erule HTT_coinduct3) + apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] + subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: ListsXH [THEN iffD1]) + done + +lemma IListsF: "A <= HTT ==> ILists(A) <= HTT" + apply clarify + apply (erule HTT_coinduct3) + apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] + subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: IListsXH [THEN iffD1]) + done + +end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/IsaMakefile --- a/src/CCL/IsaMakefile Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/IsaMakefile Tue Jul 18 02:22:38 2006 +0200 @@ -28,11 +28,8 @@ $(OUT)/FOL: FOL -$(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \ - Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \ - Term.thy Trancl.ML Trancl.thy Type.ML Type.thy wfd.ML Wfd.thy \ - coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \ - typecheck.ML +$(OUT)/CCL: $(OUT)/FOL CCL.thy Fix.thy Gfp.thy Hered.thy Lfp.thy ROOT.ML \ + Set.thy Term.thy Trancl.thy Type.thy Wfd.thy @$(ISATOOL) usedir -b -r $(OUT)/FOL CCL @@ -40,8 +37,8 @@ CCL-ex: CCL $(LOG)/CCL-ex.gz -$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.ML ex/Flag.thy ex/List.ML \ - ex/List.thy ex/Nat.ML ex/Nat.thy ex/ROOT.ML ex/Stream.ML ex/Stream.thy +$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.thy ex/List.thy ex/Nat.thy ex/ROOT.ML \ + ex/Stream.thy @$(ISATOOL) usedir $(OUT)/CCL ex diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Lfp.ML --- a/src/CCL/Lfp.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,72 +0,0 @@ -(* Title: CCL/Lfp.ML - ID: $Id$ -*) - -(*** Proof of Knaster-Tarski Theorem ***) - -(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) - -val prems = goalw (the_context ()) [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; -by (rtac (CollectI RS Inter_lower) 1); -by (resolve_tac prems 1); -qed "lfp_lowerbound"; - -val prems = goalw (the_context ()) [lfp_def] - "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)"; -by (REPEAT (ares_tac ([Inter_greatest]@prems) 1)); -by (etac CollectD 1); -qed "lfp_greatest"; - -val [mono] = goal (the_context ()) "mono(f) ==> f(lfp(f)) <= lfp(f)"; -by (EVERY1 [rtac lfp_greatest, rtac subset_trans, - rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); -qed "lfp_lemma2"; - -val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) <= f(lfp(f))"; -by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), - rtac lfp_lemma2, rtac mono]); -qed "lfp_lemma3"; - -val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) = f(lfp(f))"; -by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); -qed "lfp_Tarski"; - - -(*** General induction rule for least fixed points ***) - -val [lfp,mono,indhyp] = goal (the_context ()) - "[| a: lfp(f); mono(f); \ -\ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \ -\ |] ==> P(a)"; -by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1); -by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1); -by (EVERY1 [rtac Int_greatest, rtac subset_trans, - rtac (Int_lower1 RS (mono RS monoD)), - rtac (mono RS lfp_lemma2), - rtac (CollectI RS subsetI), rtac indhyp, atac]); -qed "induct"; - -(** Definition forms of lfp_Tarski and induct, to control unfolding **) - -val [rew,mono] = goal (the_context ()) "[| h==lfp(f); mono(f) |] ==> h = f(h)"; -by (rewtac rew); -by (rtac (mono RS lfp_Tarski) 1); -qed "def_lfp_Tarski"; - -val rew::prems = goal (the_context ()) - "[| A == lfp(f); a:A; mono(f); \ -\ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \ -\ |] ==> P(a)"; -by (EVERY1 [rtac induct, (*backtracking to force correct induction*) - REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); -qed "def_induct"; - -(*Monotonicity of lfp!*) -val prems = goal (the_context ()) - "[| mono(g); !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; -by (rtac lfp_lowerbound 1); -by (rtac subset_trans 1); -by (resolve_tac prems 1); -by (rtac lfp_lemma2 1); -by (resolve_tac prems 1); -qed "lfp_mono"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Lfp.thy --- a/src/CCL/Lfp.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Lfp.thy Tue Jul 18 02:22:38 2006 +0200 @@ -8,13 +8,67 @@ theory Lfp imports Set -uses "subset.ML" "equalities.ML" "mono.ML" begin -constdefs +definition lfp :: "['a set=>'a set] => 'a set" (*least fixed point*) "lfp(f) == Inter({u. f(u) <= u})" -ML {* use_legacy_bindings (the_context ()) *} +(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) + +lemma lfp_lowerbound: "[| f(A) <= A |] ==> lfp(f) <= A" + unfolding lfp_def by blast + +lemma lfp_greatest: "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)" + unfolding lfp_def by blast + +lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) <= lfp(f)" + by (rule lfp_greatest, rule subset_trans, drule monoD, rule lfp_lowerbound, assumption+) + +lemma lfp_lemma3: "mono(f) ==> lfp(f) <= f(lfp(f))" + by (rule lfp_lowerbound, frule monoD, drule lfp_lemma2, assumption+) + +lemma lfp_Tarski: "mono(f) ==> lfp(f) = f(lfp(f))" + by (rule equalityI lfp_lemma2 lfp_lemma3 | assumption)+ + + +(*** General induction rule for least fixed points ***) + +lemma induct: + assumes lfp: "a: lfp(f)" + and mono: "mono(f)" + and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" + shows "P(a)" + apply (rule_tac a = a in Int_lower2 [THEN subsetD, THEN CollectD]) + apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]]) + apply (rule Int_greatest, rule subset_trans, rule Int_lower1 [THEN mono [THEN monoD]], + rule mono [THEN lfp_lemma2], rule CollectI [THEN subsetI], rule indhyp, assumption) + done + +(** Definition forms of lfp_Tarski and induct, to control unfolding **) + +lemma def_lfp_Tarski: "[| h==lfp(f); mono(f) |] ==> h = f(h)" + apply unfold + apply (drule lfp_Tarski) + apply assumption + done + +lemma def_induct: + "[| A == lfp(f); a:A; mono(f); + !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) + |] ==> P(a)" + apply (rule induct [of concl: P a]) + apply simp + apply assumption + apply blast + done + +(*Monotonicity of lfp!*) +lemma lfp_mono: "[| mono(g); !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)" + apply (rule lfp_lowerbound) + apply (rule subset_trans) + apply (erule meta_spec) + apply (erule lfp_lemma2) + done end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/ROOT.ML Tue Jul 18 02:22:38 2006 +0200 @@ -14,7 +14,5 @@ (* CCL - a computational logic for an untyped functional language *) (* with evaluation to weak head-normal form *) -use_thy "CCL"; -use_thy "Hered"; use_thy "Wfd"; use_thy "Fix"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Set.ML --- a/src/CCL/Set.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,330 +0,0 @@ -(* Title: Set/Set.ML - ID: $Id$ -*) - -val [prem] = goal (the_context ()) "[| P(a) |] ==> a : {x. P(x)}"; -by (rtac (mem_Collect_iff RS iffD2) 1); -by (rtac prem 1); -qed "CollectI"; - -val prems = goal (the_context ()) "[| a : {x. P(x)} |] ==> P(a)"; -by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1); -qed "CollectD"; - -val CollectE = make_elim CollectD; - -val [prem] = goal (the_context ()) "[| !!x. x:A <-> x:B |] ==> A = B"; -by (rtac (set_extension RS iffD2) 1); -by (rtac (prem RS allI) 1); -qed "set_ext"; - -(*** Bounded quantifiers ***) - -val prems = goalw (the_context ()) [Ball_def] - "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"; -by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); -qed "ballI"; - -val [major,minor] = goalw (the_context ()) [Ball_def] - "[| ALL x:A. P(x); x:A |] ==> P(x)"; -by (rtac (minor RS (major RS spec RS mp)) 1); -qed "bspec"; - -val major::prems = goalw (the_context ()) [Ball_def] - "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"; -by (rtac (major RS spec RS impCE) 1); -by (REPEAT (eresolve_tac prems 1)); -qed "ballE"; - -(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*) -fun ball_tac i = etac ballE i THEN contr_tac (i+1); - -val prems = goalw (the_context ()) [Bex_def] - "[| P(x); x:A |] ==> EX x:A. P(x)"; -by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); -qed "bexI"; - -qed_goal "bexCI" (the_context ()) - "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)" - (fn prems=> - [ (rtac classical 1), - (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); - -val major::prems = goalw (the_context ()) [Bex_def] - "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; -by (rtac (major RS exE) 1); -by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); -qed "bexE"; - -(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) -val prems = goal (the_context ()) - "(ALL x:A. True) <-> True"; -by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); -qed "ball_rew"; - -(** Congruence rules **) - -val prems = goal (the_context ()) - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ -\ (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"; -by (resolve_tac (prems RL [ssubst,iffD2]) 1); -by (REPEAT (ares_tac [ballI,iffI] 1 - ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); -qed "ball_cong"; - -val prems = goal (the_context ()) - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ -\ (EX x:A. P(x)) <-> (EX x:A'. P'(x))"; -by (resolve_tac (prems RL [ssubst,iffD2]) 1); -by (REPEAT (etac bexE 1 - ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1)); -qed "bex_cong"; - -(*** Rules for subsets ***) - -val prems = goalw (the_context ()) [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; -by (REPEAT (ares_tac (prems @ [ballI]) 1)); -qed "subsetI"; - -(*Rule in Modus Ponens style*) -val major::prems = goalw (the_context ()) [subset_def] "[| A <= B; c:A |] ==> c:B"; -by (rtac (major RS bspec) 1); -by (resolve_tac prems 1); -qed "subsetD"; - -(*Classical elimination rule*) -val major::prems = goalw (the_context ()) [subset_def] - "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"; -by (rtac (major RS ballE) 1); -by (REPEAT (eresolve_tac prems 1)); -qed "subsetCE"; - -(*Takes assumptions A<=B; c:A and creates the assumption c:B *) -fun set_mp_tac i = etac subsetCE i THEN mp_tac i; - -qed_goal "subset_refl" (the_context ()) "A <= A" - (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); - -Goal "[| A<=B; B<=C |] ==> A<=C"; -by (rtac subsetI 1); -by (REPEAT (eresolve_tac [asm_rl, subsetD] 1)); -qed "subset_trans"; - - -(*** Rules for equality ***) - -(*Anti-symmetry of the subset relation*) -val prems = goal (the_context ()) "[| A <= B; B <= A |] ==> A = B"; -by (rtac (iffI RS set_ext) 1); -by (REPEAT (ares_tac (prems RL [subsetD]) 1)); -qed "subset_antisym"; -val equalityI = subset_antisym; - -(* Equality rules from ZF set theory -- are they appropriate here? *) -val prems = goal (the_context ()) "A = B ==> A<=B"; -by (resolve_tac (prems RL [subst]) 1); -by (rtac subset_refl 1); -qed "equalityD1"; - -val prems = goal (the_context ()) "A = B ==> B<=A"; -by (resolve_tac (prems RL [subst]) 1); -by (rtac subset_refl 1); -qed "equalityD2"; - -val prems = goal (the_context ()) - "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"; -by (resolve_tac prems 1); -by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); -qed "equalityE"; - -val major::prems = goal (the_context ()) - "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"; -by (rtac (major RS equalityE) 1); -by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); -qed "equalityCE"; - -Goal "{x. x:A} = A"; -by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1)); -qed "trivial_set"; - -(*** Rules for binary union -- Un ***) - -val prems = goalw (the_context ()) [Un_def] "c:A ==> c : A Un B"; -by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1)); -qed "UnI1"; - -val prems = goalw (the_context ()) [Un_def] "c:B ==> c : A Un B"; -by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1)); -qed "UnI2"; - -(*Classical introduction rule: no commitment to A vs B*) -qed_goal "UnCI" (the_context ()) "(~c:B ==> c:A) ==> c : A Un B" - (fn prems=> - [ (rtac classical 1), - (REPEAT (ares_tac (prems@[UnI1,notI]) 1)), - (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]); - -val major::prems = goalw (the_context ()) [Un_def] - "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; -by (rtac (major RS CollectD RS disjE) 1); -by (REPEAT (eresolve_tac prems 1)); -qed "UnE"; - - -(*** Rules for small intersection -- Int ***) - -val prems = goalw (the_context ()) [Int_def] - "[| c:A; c:B |] ==> c : A Int B"; -by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)); -qed "IntI"; - -val [major] = goalw (the_context ()) [Int_def] "c : A Int B ==> c:A"; -by (rtac (major RS CollectD RS conjunct1) 1); -qed "IntD1"; - -val [major] = goalw (the_context ()) [Int_def] "c : A Int B ==> c:B"; -by (rtac (major RS CollectD RS conjunct2) 1); -qed "IntD2"; - -val [major,minor] = goal (the_context ()) - "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; -by (rtac minor 1); -by (rtac (major RS IntD1) 1); -by (rtac (major RS IntD2) 1); -qed "IntE"; - - -(*** Rules for set complement -- Compl ***) - -val prems = goalw (the_context ()) [Compl_def] - "[| c:A ==> False |] ==> c : Compl(A)"; -by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); -qed "ComplI"; - -(*This form, with negated conclusion, works well with the Classical prover. - Negated assumptions behave like formulae on the right side of the notional - turnstile...*) -val major::prems = goalw (the_context ()) [Compl_def] - "[| c : Compl(A) |] ==> ~c:A"; -by (rtac (major RS CollectD) 1); -qed "ComplD"; - -val ComplE = make_elim ComplD; - - -(*** Empty sets ***) - -Goalw [empty_def] "{x. False} = {}"; -by (rtac refl 1); -qed "empty_eq"; - -val [prem] = goalw (the_context ()) [empty_def] "a : {} ==> P"; -by (rtac (prem RS CollectD RS FalseE) 1); -qed "emptyD"; - -val emptyE = make_elim emptyD; - -val [prem] = goal (the_context ()) "~ A={} ==> (EX x. x:A)"; -by (rtac (prem RS Cla.swap) 1); -by (rtac equalityI 1); -by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD]))); -qed "not_emptyD"; - -(*** Singleton sets ***) - -Goalw [singleton_def] "a : {a}"; -by (rtac CollectI 1); -by (rtac refl 1); -qed "singletonI"; - -val [major] = goalw (the_context ()) [singleton_def] "b : {a} ==> b=a"; -by (rtac (major RS CollectD) 1); -qed "singletonD"; - -val singletonE = make_elim singletonD; - -(*** Unions of families ***) - -(*The order of the premises presupposes that A is rigid; b may be flexible*) -val prems = goalw (the_context ()) [UNION_def] - "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))"; -by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1)); -qed "UN_I"; - -val major::prems = goalw (the_context ()) [UNION_def] - "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R"; -by (rtac (major RS CollectD RS bexE) 1); -by (REPEAT (ares_tac prems 1)); -qed "UN_E"; - -val prems = goal (the_context ()) - "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ -\ (UN x:A. C(x)) = (UN x:B. D(x))"; -by (REPEAT (etac UN_E 1 - ORELSE ares_tac ([UN_I,equalityI,subsetI] @ - (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); -qed "UN_cong"; - -(*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *) - -val prems = goalw (the_context ()) [INTER_def] - "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; -by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); -qed "INT_I"; - -val major::prems = goalw (the_context ()) [INTER_def] - "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; -by (rtac (major RS CollectD RS bspec) 1); -by (resolve_tac prems 1); -qed "INT_D"; - -(*"Classical" elimination rule -- does not require proving X:C *) -val major::prems = goalw (the_context ()) [INTER_def] - "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R"; -by (rtac (major RS CollectD RS ballE) 1); -by (REPEAT (eresolve_tac prems 1)); -qed "INT_E"; - -val prems = goal (the_context ()) - "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ -\ (INT x:A. C(x)) = (INT x:B. D(x))"; -by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); -by (REPEAT (dtac INT_D 1 - ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1)); -qed "INT_cong"; - -(*** Rules for Unions ***) - -(*The order of the premises presupposes that C is rigid; A may be flexible*) -val prems = goalw (the_context ()) [Union_def] - "[| X:C; A:X |] ==> A : Union(C)"; -by (REPEAT (resolve_tac (prems @ [UN_I]) 1)); -qed "UnionI"; - -val major::prems = goalw (the_context ()) [Union_def] - "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; -by (rtac (major RS UN_E) 1); -by (REPEAT (ares_tac prems 1)); -qed "UnionE"; - -(*** Rules for Inter ***) - -val prems = goalw (the_context ()) [Inter_def] - "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; -by (REPEAT (ares_tac ([INT_I] @ prems) 1)); -qed "InterI"; - -(*A "destruct" rule -- every X in C contains A as an element, but - A:X can hold when X:C does not! This rule is analogous to "spec". *) -val major::prems = goalw (the_context ()) [Inter_def] - "[| A : Inter(C); X:C |] ==> A:X"; -by (rtac (major RS INT_D) 1); -by (resolve_tac prems 1); -qed "InterD"; - -(*"Classical" elimination rule -- does not require proving X:C *) -val major::prems = goalw (the_context ()) [Inter_def] - "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R"; -by (rtac (major RS INT_E) 1); -by (REPEAT (eresolve_tac prems 1)); -qed "InterE"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Set.thy --- a/src/CCL/Set.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Set.thy Tue Jul 18 02:22:38 2006 +0200 @@ -72,7 +72,439 @@ Inter_def: "Inter(S) == (INT x:S. x)" Union_def: "Union(S) == (UN x:S. x)" -ML {* use_legacy_bindings (the_context ()) *} + +lemma CollectI: "[| P(a) |] ==> a : {x. P(x)}" + apply (rule mem_Collect_iff [THEN iffD2]) + apply assumption + done + +lemma CollectD: "[| a : {x. P(x)} |] ==> P(a)" + apply (erule mem_Collect_iff [THEN iffD1]) + done + +lemmas CollectE = CollectD [elim_format] + +lemma set_ext: "[| !!x. x:A <-> x:B |] ==> A = B" + apply (rule set_extension [THEN iffD2]) + apply simp + done + + +subsection {* Bounded quantifiers *} + +lemma ballI: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)" + by (simp add: Ball_def) + +lemma bspec: "[| ALL x:A. P(x); x:A |] ==> P(x)" + by (simp add: Ball_def) + +lemma ballE: "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q" + unfolding Ball_def by blast + +lemma bexI: "[| P(x); x:A |] ==> EX x:A. P(x)" + unfolding Bex_def by blast + +lemma bexCI: "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)" + unfolding Bex_def by blast + +lemma bexE: "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q" + unfolding Bex_def by blast + +(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) +lemma ball_rew: "(ALL x:A. True) <-> True" + by (blast intro: ballI) + + +subsection {* Congruence rules *} + +lemma ball_cong: + "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> + (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))" + by (blast intro: ballI elim: ballE) + +lemma bex_cong: + "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> + (EX x:A. P(x)) <-> (EX x:A'. P'(x))" + by (blast intro: bexI elim: bexE) + + +subsection {* Rules for subsets *} + +lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B" + unfolding subset_def by (blast intro: ballI) + +(*Rule in Modus Ponens style*) +lemma subsetD: "[| A <= B; c:A |] ==> c:B" + unfolding subset_def by (blast elim: ballE) + +(*Classical elimination rule*) +lemma subsetCE: "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P" + by (blast dest: subsetD) + +lemma subset_refl: "A <= A" + by (blast intro: subsetI) + +lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C" + by (blast intro: subsetI dest: subsetD) + + +subsection {* Rules for equality *} + +(*Anti-symmetry of the subset relation*) +lemma subset_antisym: "[| A <= B; B <= A |] ==> A = B" + by (blast intro: set_ext dest: subsetD) + +lemmas equalityI = subset_antisym + +(* Equality rules from ZF set theory -- are they appropriate here? *) +lemma equalityD1: "A = B ==> A<=B" + and equalityD2: "A = B ==> B<=A" + by (simp_all add: subset_refl) + +lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" + by (simp add: subset_refl) + +lemma equalityCE: + "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P" + by (blast elim: equalityE subsetCE) + +lemma trivial_set: "{x. x:A} = A" + by (blast intro: equalityI subsetI CollectI dest: CollectD) + + +subsection {* Rules for binary union *} + +lemma UnI1: "c:A ==> c : A Un B" + and UnI2: "c:B ==> c : A Un B" + unfolding Un_def by (blast intro: CollectI)+ + +(*Classical introduction rule: no commitment to A vs B*) +lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B" + by (blast intro: UnI1 UnI2) + +lemma UnE: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" + unfolding Un_def by (blast dest: CollectD) + + +subsection {* Rules for small intersection *} + +lemma IntI: "[| c:A; c:B |] ==> c : A Int B" + unfolding Int_def by (blast intro: CollectI) + +lemma IntD1: "c : A Int B ==> c:A" + and IntD2: "c : A Int B ==> c:B" + unfolding Int_def by (blast dest: CollectD)+ + +lemma IntE: "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" + by (blast dest: IntD1 IntD2) + + +subsection {* Rules for set complement *} + +lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)" + unfolding Compl_def by (blast intro: CollectI) + +(*This form, with negated conclusion, works well with the Classical prover. + Negated assumptions behave like formulae on the right side of the notional + turnstile...*) +lemma ComplD: "[| c : Compl(A) |] ==> ~c:A" + unfolding Compl_def by (blast dest: CollectD) + +lemmas ComplE = ComplD [elim_format] + + +subsection {* Empty sets *} + +lemma empty_eq: "{x. False} = {}" + by (simp add: empty_def) + +lemma emptyD: "a : {} ==> P" + unfolding empty_def by (blast dest: CollectD) + +lemmas emptyE = emptyD [elim_format] + +lemma not_emptyD: + assumes "~ A={}" + shows "EX x. x:A" +proof - + have "\ (EX x. x:A) \ A = {}" + by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+ + with prems show ?thesis by blast +qed + + +subsection {* Singleton sets *} + +lemma singletonI: "a : {a}" + unfolding singleton_def by (blast intro: CollectI) + +lemma singletonD: "b : {a} ==> b=a" + unfolding singleton_def by (blast dest: CollectD) + +lemmas singletonE = singletonD [elim_format] + + +subsection {* Unions of families *} + +(*The order of the premises presupposes that A is rigid; b may be flexible*) +lemma UN_I: "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))" + unfolding UNION_def by (blast intro: bexI CollectI) + +lemma UN_E: "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R" + unfolding UNION_def by (blast dest: CollectD elim: bexE) + +lemma UN_cong: + "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> + (UN x:A. C(x)) = (UN x:B. D(x))" + by (simp add: UNION_def cong: bex_cong) + + +subsection {* Intersections of families *} + +lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))" + unfolding INTER_def by (blast intro: CollectI ballI) + +lemma INT_D: "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)" + unfolding INTER_def by (blast dest: CollectD bspec) + +(*"Classical" elimination rule -- does not require proving X:C *) +lemma INT_E: "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R" + unfolding INTER_def by (blast dest: CollectD bspec) + +lemma INT_cong: + "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> + (INT x:A. C(x)) = (INT x:B. D(x))" + by (simp add: INTER_def cong: ball_cong) + + +subsection {* Rules for Unions *} + +(*The order of the premises presupposes that C is rigid; A may be flexible*) +lemma UnionI: "[| X:C; A:X |] ==> A : Union(C)" + unfolding Union_def by (blast intro: UN_I) + +lemma UnionE: "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R" + unfolding Union_def by (blast elim: UN_E) + + +subsection {* Rules for Inter *} + +lemma InterI: "[| !!X. X:C ==> A:X |] ==> A : Inter(C)" + unfolding Inter_def by (blast intro: INT_I) + +(*A "destruct" rule -- every X in C contains A as an element, but + A:X can hold when X:C does not! This rule is analogous to "spec". *) +lemma InterD: "[| A : Inter(C); X:C |] ==> A:X" + unfolding Inter_def by (blast dest: INT_D) + +(*"Classical" elimination rule -- does not require proving X:C *) +lemma InterE: "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R" + unfolding Inter_def by (blast elim: INT_E) + + +section {* Derived rules involving subsets; Union and Intersection as lattice operations *} + +subsection {* Big Union -- least upper bound of a set *} + +lemma Union_upper: "B:A ==> B <= Union(A)" + by (blast intro: subsetI UnionI) + +lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C" + by (blast intro: subsetI dest: subsetD elim: UnionE) + + +subsection {* Big Intersection -- greatest lower bound of a set *} + +lemma Inter_lower: "B:A ==> Inter(A) <= B" + by (blast intro: subsetI dest: InterD) + +lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)" + by (blast intro: subsetI InterI dest: subsetD) + + +subsection {* Finite Union -- the least upper bound of 2 sets *} + +lemma Un_upper1: "A <= A Un B" + by (blast intro: subsetI UnI1) + +lemma Un_upper2: "B <= A Un B" + by (blast intro: subsetI UnI2) + +lemma Un_least: "[| A<=C; B<=C |] ==> A Un B <= C" + by (blast intro: subsetI elim: UnE dest: subsetD) + + +subsection {* Finite Intersection -- the greatest lower bound of 2 sets *} + +lemma Int_lower1: "A Int B <= A" + by (blast intro: subsetI elim: IntE) + +lemma Int_lower2: "A Int B <= B" + by (blast intro: subsetI elim: IntE) + +lemma Int_greatest: "[| C<=A; C<=B |] ==> C <= A Int B" + by (blast intro: subsetI IntI dest: subsetD) + + +subsection {* Monotonicity *} + +lemma monoI: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)" + unfolding mono_def by blast + +lemma monoD: "[| mono(f); A <= B |] ==> f(A) <= f(B)" + unfolding mono_def by blast + +lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)" + by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2) + +lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)" + by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2) + + +subsection {* Automated reasoning setup *} + +lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI + and [intro] = bexI UnionI UN_I + and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE + and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE + +lemma mem_rews: + "(a : A Un B) <-> (a:A | a:B)" + "(a : A Int B) <-> (a:A & a:B)" + "(a : Compl(B)) <-> (~a:B)" + "(a : {b}) <-> (a=b)" + "(a : {}) <-> False" + "(a : {x. P(x)}) <-> P(a)" + by blast+ + +lemmas [simp] = trivial_set empty_eq mem_rews + and [cong] = ball_cong bex_cong INT_cong UN_cong + + +section {* Equalities involving union, intersection, inclusion, etc. *} + +subsection {* Binary Intersection *} + +lemma Int_absorb: "A Int A = A" + by (blast intro: equalityI) + +lemma Int_commute: "A Int B = B Int A" + by (blast intro: equalityI) + +lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)" + by (blast intro: equalityI) + +lemma Int_Un_distrib: "(A Un B) Int C = (A Int C) Un (B Int C)" + by (blast intro: equalityI) + +lemma subset_Int_eq: "(A<=B) <-> (A Int B = A)" + by (blast intro: equalityI elim: equalityE) + + +subsection {* Binary Union *} + +lemma Un_absorb: "A Un A = A" + by (blast intro: equalityI) + +lemma Un_commute: "A Un B = B Un A" + by (blast intro: equalityI) + +lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)" + by (blast intro: equalityI) + +lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)" + by (blast intro: equalityI) + +lemma Un_Int_crazy: + "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)" + by (blast intro: equalityI) + +lemma subset_Un_eq: "(A<=B) <-> (A Un B = B)" + by (blast intro: equalityI elim: equalityE) + + +subsection {* Simple properties of @{text "Compl"} -- complement of a set *} + +lemma Compl_disjoint: "A Int Compl(A) = {x. False}" + by (blast intro: equalityI) + +lemma Compl_partition: "A Un Compl(A) = {x. True}" + by (blast intro: equalityI) + +lemma double_complement: "Compl(Compl(A)) = A" + by (blast intro: equalityI) + +lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)" + by (blast intro: equalityI) + +lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)" + by (blast intro: equalityI) + +lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))" + by (blast intro: equalityI) + +lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))" + by (blast intro: equalityI) + +(*Halmos, Naive Set Theory, page 16.*) +lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)" + by (blast intro: equalityI elim: equalityE) + + +subsection {* Big Union and Intersection *} + +lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)" + by (blast intro: equalityI) + +lemma Union_disjoint: + "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})" + by (blast intro: equalityI elim: equalityE) + +lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)" + by (blast intro: equalityI) + + +subsection {* Unions and Intersections of Families *} + +lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})" + by (blast intro: equalityI) + +(*Look: it has an EXISTENTIAL quantifier*) +lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})" + by (blast intro: equalityI) + +lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)" + by (blast intro: equalityI) + +lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)" + by (blast intro: equalityI) + + +section {* Monotonicity of various operations *} + +lemma Union_mono: "A<=B ==> Union(A) <= Union(B)" + by blast + +lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)" + by blast + +lemma UN_mono: + "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> + (UN x:A. f(x)) <= (UN x:B. g(x))" + by blast + +lemma INT_anti_mono: + "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> + (INT x:A. f(x)) <= (INT x:A. g(x))" + by blast + +lemma Un_mono: "[| A<=C; B<=D |] ==> A Un B <= C Un D" + by blast + +lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D" + by blast + +lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)" + by blast end - diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Term.ML --- a/src/CCL/Term.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,144 +0,0 @@ -(* Title: CCL/Term.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -val simp_can_defs = [one_def,inl_def,inr_def]; -val simp_ncan_defs = [if_def,when_def,split_def,fst_def,snd_def,thd_def]; -val simp_defs = simp_can_defs @ simp_ncan_defs; - -val ind_can_defs = [zero_def,succ_def,nil_def,cons_def]; -val ind_ncan_defs = [ncase_def,nrec_def,lcase_def,lrec_def]; -val ind_defs = ind_can_defs @ ind_ncan_defs; - -val data_defs = simp_defs @ ind_defs @ [napply_def]; -val genrec_defs = [letrec_def,letrec2_def,letrec3_def]; - -(*** Beta Rules, including strictness ***) - -Goalw [let_def] "~ t=bot--> let x be t in f(x) = f(t)"; -by (res_inst_tac [("t","t")] term_case 1); -by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); -bind_thm("letB", result() RS mp); - -Goalw [let_def] "let x be bot in f(x) = bot"; -by (rtac caseBbot 1); -qed "letBabot"; - -Goalw [let_def] "let x be t in bot = bot"; -by (resolve_tac ([caseBbot] RL [term_case]) 1); -by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); -qed "letBbbot"; - -Goalw [apply_def] "(lam x. b(x)) ` a = b(a)"; -by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); -qed "applyB"; - -Goalw [apply_def] "bot ` a = bot"; -by (rtac caseBbot 1); -qed "applyBbot"; - -Goalw [fix_def] "fix(f) = f(fix(f))"; -by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1); -qed "fixB"; - -Goalw [letrec_def] - "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))"; -by (resolve_tac [fixB RS ssubst] 1 THEN - resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1); -qed "letrecB"; - -val rawBs = caseBs @ [applyB,applyBbot]; - -fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s - (fn _ => [stac letrecB 1, - simp_tac (CCL_ss addsimps rawBs) 1]); -fun mk_beta_rl s = raw_mk_beta_rl data_defs s; - -fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s - (fn _ => [simp_tac (CCL_ss addsimps rawBs - setloop (stac letrecB)) 1]); -fun mk_beta_rl s = raw_mk_beta_rl data_defs s; - -val ifBtrue = mk_beta_rl "if true then t else u = t"; -val ifBfalse = mk_beta_rl "if false then t else u = u"; -val ifBbot = mk_beta_rl "if bot then t else u = bot"; - -val whenBinl = mk_beta_rl "when(inl(a),t,u) = t(a)"; -val whenBinr = mk_beta_rl "when(inr(a),t,u) = u(a)"; -val whenBbot = mk_beta_rl "when(bot,t,u) = bot"; - -val splitB = mk_beta_rl "split(,h) = h(a,b)"; -val splitBbot = mk_beta_rl "split(bot,h) = bot"; -val fstB = mk_beta_rl "fst() = a"; -val fstBbot = mk_beta_rl "fst(bot) = bot"; -val sndB = mk_beta_rl "snd() = b"; -val sndBbot = mk_beta_rl "snd(bot) = bot"; -val thdB = mk_beta_rl "thd(>) = c"; -val thdBbot = mk_beta_rl "thd(bot) = bot"; - -val ncaseBzero = mk_beta_rl "ncase(zero,t,u) = t"; -val ncaseBsucc = mk_beta_rl "ncase(succ(n),t,u) = u(n)"; -val ncaseBbot = mk_beta_rl "ncase(bot,t,u) = bot"; -val nrecBzero = mk_beta_rl "nrec(zero,t,u) = t"; -val nrecBsucc = mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"; -val nrecBbot = mk_beta_rl "nrec(bot,t,u) = bot"; - -val lcaseBnil = mk_beta_rl "lcase([],t,u) = t"; -val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)"; -val lcaseBbot = mk_beta_rl "lcase(bot,t,u) = bot"; -val lrecBnil = mk_beta_rl "lrec([],t,u) = t"; -val lrecBcons = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"; -val lrecBbot = mk_beta_rl "lrec(bot,t,u) = bot"; - -val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def]) - "letrec g x y be h(x,y,g) in g(p,q) = \ -\ h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))"; -val letrec3B = raw_mk_beta_rl (data_defs @ [letrec3_def]) - "letrec g x y z be h(x,y,z,g) in g(p,q,r) = \ -\ h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"; - -val napplyBzero = mk_beta_rl "f^zero`a = a"; -val napplyBsucc = mk_beta_rl "f^succ(n)`a = f(f^n`a)"; - -val termBs = [letB,applyB,applyBbot,splitB,splitBbot, - fstB,fstBbot,sndB,sndBbot,thdB,thdBbot, - ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot, - ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot, - lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot, - napplyBzero,napplyBsucc]; - -(*** Constructors are injective ***) - -val term_injs = map (mk_inj_rl (the_context ()) - [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons]) - ["(inl(a) = inl(a')) <-> (a=a')", - "(inr(a) = inr(a')) <-> (a=a')", - "(succ(a) = succ(a')) <-> (a=a')", - "(a$b = a'$b') <-> (a=a' & b=b')"]; - -(*** Constructors are distinct ***) - -val term_dstncts = mkall_dstnct_thms (the_context ()) data_defs (ccl_injs @ term_injs) - [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]]; - -(*** Rules for pre-order [= ***) - -local - fun mk_thm s = prove_goalw (the_context ()) data_defs s (fn _ => - [simp_tac (ccl_ss addsimps (ccl_porews)) 1]); -in - val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'", - "inr(b) [= inr(b') <-> b [= b'", - "succ(n) [= succ(n') <-> n [= n'", - "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"]; -end; - -(*** Rewriting and Proving ***) - -val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews; -val term_ss = ccl_ss addsimps term_rews; - -val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) - addSDs (XH_to_Ds term_injs); diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Term.thy --- a/src/CCL/Term.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Term.thy Tue Jul 18 02:22:38 2006 +0200 @@ -143,6 +143,183 @@ napply_def: "f ^n` a == nrec(n,a,%x g. f(g))" -ML {* use_legacy_bindings (the_context ()) *} + +lemmas simp_can_defs = one_def inl_def inr_def + and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def +lemmas simp_defs = simp_can_defs simp_ncan_defs + +lemmas ind_can_defs = zero_def succ_def nil_def cons_def + and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def +lemmas ind_defs = ind_can_defs ind_ncan_defs + +lemmas data_defs = simp_defs ind_defs napply_def + and genrec_defs = letrec_def letrec2_def letrec3_def + + +subsection {* Beta Rules, including strictness *} + +lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)" + apply (unfold let_def) + apply (erule rev_mp) + apply (rule_tac t = "t" in term_case) + apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) + done + +lemma letBabot: "let x be bot in f(x) = bot" + apply (unfold let_def) + apply (rule caseBbot) + done + +lemma letBbbot: "let x be t in bot = bot" + apply (unfold let_def) + apply (rule_tac t = t in term_case) + apply (rule caseBbot) + apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) + done + +lemma applyB: "(lam x. b(x)) ` a = b(a)" + apply (unfold apply_def) + apply (simp add: caseBtrue caseBfalse caseBpair caseBlam) + done + +lemma applyBbot: "bot ` a = bot" + apply (unfold apply_def) + apply (rule caseBbot) + done + +lemma fixB: "fix(f) = f(fix(f))" + apply (unfold fix_def) + apply (rule applyB [THEN ssubst], rule refl) + done + +lemma letrecB: + "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))" + apply (unfold letrec_def) + apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl) + done + +lemmas rawBs = caseBs applyB applyBbot + +ML {* +local + val letrecB = thm "letrecB" + val rawBs = thms "rawBs" + val data_defs = thms "data_defs" +in + +fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s + (fn _ => [stac letrecB 1, + simp_tac (simpset () addsimps rawBs) 1]); +fun mk_beta_rl s = raw_mk_beta_rl data_defs s; + +fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s + (fn _ => [simp_tac (simpset () addsimps rawBs + setloop (stac letrecB)) 1]); +fun mk_beta_rl s = raw_mk_beta_rl data_defs s; end +*} + +ML {* +bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t"); +bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u"); +bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot"); + +bind_thm ("whenBinl", mk_beta_rl "when(inl(a),t,u) = t(a)"); +bind_thm ("whenBinr", mk_beta_rl "when(inr(a),t,u) = u(a)"); +bind_thm ("whenBbot", mk_beta_rl "when(bot,t,u) = bot"); + +bind_thm ("splitB", mk_beta_rl "split(,h) = h(a,b)"); +bind_thm ("splitBbot", mk_beta_rl "split(bot,h) = bot"); +bind_thm ("fstB", mk_beta_rl "fst() = a"); +bind_thm ("fstBbot", mk_beta_rl "fst(bot) = bot"); +bind_thm ("sndB", mk_beta_rl "snd() = b"); +bind_thm ("sndBbot", mk_beta_rl "snd(bot) = bot"); +bind_thm ("thdB", mk_beta_rl "thd(>) = c"); +bind_thm ("thdBbot", mk_beta_rl "thd(bot) = bot"); + +bind_thm ("ncaseBzero", mk_beta_rl "ncase(zero,t,u) = t"); +bind_thm ("ncaseBsucc", mk_beta_rl "ncase(succ(n),t,u) = u(n)"); +bind_thm ("ncaseBbot", mk_beta_rl "ncase(bot,t,u) = bot"); +bind_thm ("nrecBzero", mk_beta_rl "nrec(zero,t,u) = t"); +bind_thm ("nrecBsucc", mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"); +bind_thm ("nrecBbot", mk_beta_rl "nrec(bot,t,u) = bot"); + +bind_thm ("lcaseBnil", mk_beta_rl "lcase([],t,u) = t"); +bind_thm ("lcaseBcons", mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)"); +bind_thm ("lcaseBbot", mk_beta_rl "lcase(bot,t,u) = bot"); +bind_thm ("lrecBnil", mk_beta_rl "lrec([],t,u) = t"); +bind_thm ("lrecBcons", mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"); +bind_thm ("lrecBbot", mk_beta_rl "lrec(bot,t,u) = bot"); + +bind_thm ("letrec2B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec2_def"]) + "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))"); + +bind_thm ("letrec3B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec3_def"]) + "letrec g x y z be h(x,y,z,g) in g(p,q,r) = h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"); + +bind_thm ("napplyBzero", mk_beta_rl "f^zero`a = a"); +bind_thm ("napplyBsucc", mk_beta_rl "f^succ(n)`a = f(f^n`a)"); + +bind_thms ("termBs", [thm "letB", thm "applyB", thm "applyBbot", splitB,splitBbot, + fstB,fstBbot,sndB,sndBbot,thdB,thdBbot, + ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot, + ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot, + lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot, + napplyBzero,napplyBsucc]); +*} + + +subsection {* Constructors are injective *} + +ML {* + +bind_thms ("term_injs", map (mk_inj_rl (the_context ()) + [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"]) + ["(inl(a) = inl(a')) <-> (a=a')", + "(inr(a) = inr(a')) <-> (a=a')", + "(succ(a) = succ(a')) <-> (a=a')", + "(a$b = a'$b') <-> (a=a' & b=b')"]) +*} + + +subsection {* Constructors are distinct *} + +ML {* +bind_thms ("term_dstncts", + mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs") + [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","op $"]]); +*} + + +subsection {* Rules for pre-order @{text "[="} *} + +ML {* + +local + fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ => + [simp_tac (simpset () addsimps (thms "ccl_porews")) 1]) +in + val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'", + "inr(b) [= inr(b') <-> b [= b'", + "succ(n) [= succ(n') <-> n [= n'", + "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"] +end; + +bind_thms ("term_porews", term_porews); +*} + + +subsection {* Rewriting and Proving *} + +lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews + +ML {* + bind_thms ("term_injDs", XH_to_Ds term_injs); +*} + +lemmas [simp] = term_rews + and [elim!] = term_dstncts [THEN notE] + and [dest!] = term_injDs + +end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Trancl.ML --- a/src/CCL/Trancl.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,205 +0,0 @@ -(* Title: CCL/Trancl.ML - ID: $Id$ -*) - -(** Natural deduction for trans(r) **) - -val prems = goalw (the_context ()) [trans_def] - "(!! x y z. [| :r; :r |] ==> :r) ==> trans(r)"; -by (REPEAT (ares_tac (prems@[allI,impI]) 1)); -qed "transI"; - -val major::prems = goalw (the_context ()) [trans_def] - "[| trans(r); :r; :r |] ==> :r"; -by (cut_facts_tac [major] 1); -by (fast_tac (FOL_cs addIs prems) 1); -qed "transD"; - -(** Identity relation **) - -Goalw [id_def] " : id"; -by (rtac CollectI 1); -by (rtac exI 1); -by (rtac refl 1); -qed "idI"; - -val major::prems = goalw (the_context ()) [id_def] - "[| p: id; !!x.[| p = |] ==> P \ -\ |] ==> P"; -by (rtac (major RS CollectE) 1); -by (etac exE 1); -by (eresolve_tac prems 1); -qed "idE"; - -(** Composition of two relations **) - -val prems = goalw (the_context ()) [comp_def] - "[| :s; :r |] ==> : r O s"; -by (fast_tac (set_cs addIs prems) 1); -qed "compI"; - -(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) -val prems = goalw (the_context ()) [comp_def] - "[| xz : r O s; \ -\ !!x y z. [| xz = ; :s; :r |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac prems 1); -by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); -qed "compE"; - -val prems = goal (the_context ()) - "[| : r O s; \ -\ !!y. [| :s; :r |] ==> P \ -\ |] ==> P"; -by (rtac compE 1); -by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [pair_inject,ssubst] 1)); -qed "compEpair"; - -val comp_cs = set_cs addIs [compI,idI] - addEs [compE,idE] - addSEs [pair_inject]; - -val prems = goal (the_context ()) - "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; -by (cut_facts_tac prems 1); -by (fast_tac comp_cs 1); -qed "comp_mono"; - -(** The relation rtrancl **) - -Goal "mono(%s. id Un (r O s))"; -by (rtac monoI 1); -by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1)); -qed "rtrancl_fun_mono"; - -val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski); - -(*Reflexivity of rtrancl*) -Goal " : r^*"; -by (stac rtrancl_unfold 1); -by (fast_tac comp_cs 1); -qed "rtrancl_refl"; - -(*Closure under composition with r*) -val prems = goal (the_context ()) - "[| : r^*; : r |] ==> : r^*"; -by (stac rtrancl_unfold 1); -by (fast_tac (comp_cs addIs prems) 1); -qed "rtrancl_into_rtrancl"; - -(*rtrancl of r contains r*) -val [prem] = goal (the_context ()) "[| : r |] ==> : r^*"; -by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1); -by (rtac prem 1); -qed "r_into_rtrancl"; - - -(** standard induction rule **) - -val major::prems = goal (the_context ()) - "[| : r^*; \ -\ !!x. P(); \ -\ !!x y z.[| P(); : r^*; : r |] ==> P() |] \ -\ ==> P()"; -by (rtac (major RS (rtrancl_def RS def_induct)) 1); -by (rtac rtrancl_fun_mono 1); -by (fast_tac (comp_cs addIs prems) 1); -qed "rtrancl_full_induct"; - -(*nice induction rule*) -val major::prems = goal (the_context ()) - "[| : r^*; \ -\ P(a); \ -\ !!y z.[| : r^*; : r; P(y) |] ==> P(z) |] \ -\ ==> P(b)"; -(*by induction on this formula*) -by (subgoal_tac "ALL y. = --> P(y)" 1); -(*now solve first subgoal: this formula is sufficient*) -by (fast_tac FOL_cs 1); -(*now do the induction*) -by (resolve_tac [major RS rtrancl_full_induct] 1); -by (fast_tac (comp_cs addIs prems) 1); -by (fast_tac (comp_cs addIs prems) 1); -qed "rtrancl_induct"; - -(*transitivity of transitive closure!! -- by induction.*) -Goal "trans(r^*)"; -by (rtac transI 1); -by (res_inst_tac [("b","z")] rtrancl_induct 1); -by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1)); -qed "trans_rtrancl"; - -(*elimination of rtrancl -- by induction on a special formula*) -val major::prems = goal (the_context ()) - "[| : r^*; (a = b) ==> P; \ -\ !!y.[| : r^*; : r |] ==> P |] \ -\ ==> P"; -by (subgoal_tac "a = b | (EX y. : r^* & : r)" 1); -by (rtac (major RS rtrancl_induct) 2); -by (fast_tac (set_cs addIs prems) 2); -by (fast_tac (set_cs addIs prems) 2); -by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); -qed "rtranclE"; - - -(**** The relation trancl ****) - -(** Conversions between trancl and rtrancl **) - -val [major] = goalw (the_context ()) [trancl_def] - "[| : r^+ |] ==> : r^*"; -by (resolve_tac [major RS compEpair] 1); -by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1)); -qed "trancl_into_rtrancl"; - -(*r^+ contains r*) -val [prem] = goalw (the_context ()) [trancl_def] - "[| : r |] ==> : r^+"; -by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1)); -qed "r_into_trancl"; - -(*intro rule by definition: from rtrancl and r*) -val prems = goalw (the_context ()) [trancl_def] - "[| : r^*; : r |] ==> : r^+"; -by (REPEAT (resolve_tac ([compI]@prems) 1)); -qed "rtrancl_into_trancl1"; - -(*intro rule from r and rtrancl*) -val prems = goal (the_context ()) - "[| : r; : r^* |] ==> : r^+"; -by (resolve_tac (prems RL [rtranclE]) 1); -by (etac subst 1); -by (resolve_tac (prems RL [r_into_trancl]) 1); -by (rtac (trans_rtrancl RS transD RS rtrancl_into_trancl1) 1); -by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1)); -qed "rtrancl_into_trancl2"; - -(*elimination of r^+ -- NOT an induction rule*) -val major::prems = goal (the_context ()) - "[| : r^+; \ -\ : r ==> P; \ -\ !!y.[| : r^+; : r |] ==> P \ -\ |] ==> P"; -by (subgoal_tac " : r | (EX y. : r^+ & : r)" 1); -by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); -by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); -by (etac rtranclE 1); -by (fast_tac comp_cs 1); -by (fast_tac (comp_cs addSIs [rtrancl_into_trancl1]) 1); -qed "tranclE"; - -(*Transitivity of r^+. - Proved by unfolding since it uses transitivity of rtrancl. *) -Goalw [trancl_def] "trans(r^+)"; -by (rtac transI 1); -by (REPEAT (etac compEpair 1)); -by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1); -by (REPEAT (assume_tac 1)); -qed "trans_trancl"; - -val prems = goal (the_context ()) - "[| : r; : r^+ |] ==> : r^+"; -by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1); -by (resolve_tac prems 1); -by (resolve_tac prems 1); -qed "trancl_into_trancl2"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Trancl.thy --- a/src/CCL/Trancl.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Trancl.thy Tue Jul 18 02:22:38 2006 +0200 @@ -26,6 +26,197 @@ rtrancl_def: "r^* == lfp(%s. id Un (r O s))" trancl_def: "r^+ == r O rtrancl(r)" -ML {* use_legacy_bindings (the_context ()) *} + +subsection {* Natural deduction for @{text "trans(r)"} *} + +lemma transI: + "(!! x y z. [| :r; :r |] ==> :r) ==> trans(r)" + unfolding trans_def by blast + +lemma transD: "[| trans(r); :r; :r |] ==> :r" + unfolding trans_def by blast + + +subsection {* Identity relation *} + +lemma idI: " : id" + apply (unfold id_def) + apply (rule CollectI) + apply (rule exI) + apply (rule refl) + done + +lemma idE: + "[| p: id; !!x.[| p = |] ==> P |] ==> P" + apply (unfold id_def) + apply (erule CollectE) + apply blast + done + + +subsection {* Composition of two relations *} + +lemma compI: "[| :s; :r |] ==> : r O s" + unfolding comp_def by blast + +(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) +lemma compE: + "[| xz : r O s; + !!x y z. [| xz = ; :s; :r |] ==> P + |] ==> P" + unfolding comp_def by blast + +lemma compEpair: + "[| : r O s; + !!y. [| :s; :r |] ==> P + |] ==> P" + apply (erule compE) + apply (simp add: pair_inject) + done + +lemmas [intro] = compI idI + and [elim] = compE idE + and [elim!] = pair_inject + +lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)" + by blast + + +subsection {* The relation rtrancl *} + +lemma rtrancl_fun_mono: "mono(%s. id Un (r O s))" + apply (rule monoI) + apply (rule monoI subset_refl comp_mono Un_mono)+ + apply assumption + done + +lemma rtrancl_unfold: "r^* = id Un (r O r^*)" + by (rule rtrancl_fun_mono [THEN rtrancl_def [THEN def_lfp_Tarski]]) + +(*Reflexivity of rtrancl*) +lemma rtrancl_refl: " : r^*" + apply (subst rtrancl_unfold) + apply blast + done + +(*Closure under composition with r*) +lemma rtrancl_into_rtrancl: "[| : r^*; : r |] ==> : r^*" + apply (subst rtrancl_unfold) + apply blast + done + +(*rtrancl of r contains r*) +lemma r_into_rtrancl: "[| : r |] ==> : r^*" + apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl]) + apply assumption + done + + +subsection {* standard induction rule *} + +lemma rtrancl_full_induct: + "[| : r^*; + !!x. P(); + !!x y z.[| P(); : r^*; : r |] ==> P() |] + ==> P()" + apply (erule def_induct [OF rtrancl_def]) + apply (rule rtrancl_fun_mono) + apply blast + done + +(*nice induction rule*) +lemma rtrancl_induct: + "[| : r^*; + P(a); + !!y z.[| : r^*; : r; P(y) |] ==> P(z) |] + ==> P(b)" +(*by induction on this formula*) + apply (subgoal_tac "ALL y. = --> P(y)") +(*now solve first subgoal: this formula is sufficient*) + apply blast +(*now do the induction*) + apply (erule rtrancl_full_induct) + apply blast + apply blast + done + +(*transitivity of transitive closure!! -- by induction.*) +lemma trans_rtrancl: "trans(r^*)" + apply (rule transI) + apply (rule_tac b = z in rtrancl_induct) + apply (fast elim: rtrancl_into_rtrancl)+ + done + +(*elimination of rtrancl -- by induction on a special formula*) +lemma rtranclE: + "[| : r^*; (a = b) ==> P; + !!y.[| : r^*; : r |] ==> P |] + ==> P" + apply (subgoal_tac "a = b | (EX y. : r^* & : r)") + prefer 2 + apply (erule rtrancl_induct) + apply blast + apply blast + apply blast + done + + +subsection {* The relation trancl *} + +subsubsection {* Conversions between trancl and rtrancl *} + +lemma trancl_into_rtrancl: "[| : r^+ |] ==> : r^*" + apply (unfold trancl_def) + apply (erule compEpair) + apply (erule rtrancl_into_rtrancl) + apply assumption + done + +(*r^+ contains r*) +lemma r_into_trancl: "[| : r |] ==> : r^+" + unfolding trancl_def by (blast intro: rtrancl_refl) + +(*intro rule by definition: from rtrancl and r*) +lemma rtrancl_into_trancl1: "[| : r^*; : r |] ==> : r^+" + unfolding trancl_def by blast + +(*intro rule from r and rtrancl*) +lemma rtrancl_into_trancl2: "[| : r; : r^* |] ==> : r^+" + apply (erule rtranclE) + apply (erule subst) + apply (erule r_into_trancl) + apply (rule trans_rtrancl [THEN transD, THEN rtrancl_into_trancl1]) + apply (assumption | rule r_into_rtrancl)+ + done + +(*elimination of r^+ -- NOT an induction rule*) +lemma tranclE: + "[| : r^+; + : r ==> P; + !!y.[| : r^+; : r |] ==> P + |] ==> P" + apply (subgoal_tac " : r | (EX y. : r^+ & : r)") + apply blast + apply (unfold trancl_def) + apply (erule compEpair) + apply (erule rtranclE) + apply blast + apply (blast intro!: rtrancl_into_trancl1) + done + +(*Transitivity of r^+. + Proved by unfolding since it uses transitivity of rtrancl. *) +lemma trans_trancl: "trans(r^+)" + apply (unfold trancl_def) + apply (rule transI) + apply (erule compEpair)+ + apply (erule rtrancl_into_rtrancl [THEN trans_rtrancl [THEN transD, THEN compI]]) + apply assumption+ + done + +lemma trancl_into_trancl2: "[| : r; : r^+ |] ==> : r^+" + apply (rule r_into_trancl [THEN trans_trancl [THEN transD]]) + apply assumption+ + done end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Type.ML --- a/src/CCL/Type.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,304 +0,0 @@ -(* Title: CCL/Type.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge -*) - -val simp_type_defs = [Subtype_def,Unit_def,Bool_def,Plus_def,Sigma_def,Pi_def, - Lift_def,Tall_def,Tex_def]; -val ind_type_defs = [Nat_def,List_def]; - -val simp_data_defs = [one_def,inl_def,inr_def]; -val ind_data_defs = [zero_def,succ_def,nil_def,cons_def]; - -goal (the_context ()) "A <= B <-> (ALL x. x:A --> x:B)"; -by (fast_tac set_cs 1); -qed "subsetXH"; - -(*** Exhaustion Rules ***) - -fun mk_XH_tac thy defs rls s = prove_goalw thy defs s (fn _ => [cfast_tac rls 1]); -val XH_tac = mk_XH_tac (the_context ()) simp_type_defs []; - -val EmptyXH = XH_tac "a : {} <-> False"; -val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))"; -val UnitXH = XH_tac "a : Unit <-> a=one"; -val BoolXH = XH_tac "a : Bool <-> a=true | a=false"; -val PlusXH = XH_tac "a : A+B <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))"; -val PiXH = XH_tac "a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))"; -val SgXH = XH_tac "a : SUM x:A. B(x) <-> (EX x:A. EX y:B(x).a=)"; - -val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH]; - -val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)"; -val TallXH = XH_tac "a : TALL X. B(X) <-> (ALL X. a:B(X))"; -val TexXH = XH_tac "a : TEX X. B(X) <-> (EX X. a:B(X))"; - -val case_rls = XH_to_Es XHs; - -(*** Canonical Type Rules ***) - -fun mk_canT_tac thy xhs s = prove_goal thy s - (fn prems => [fast_tac (set_cs addIs (prems @ (xhs RL [iffD2]))) 1]); -val canT_tac = mk_canT_tac (the_context ()) XHs; - -val oneT = canT_tac "one : Unit"; -val trueT = canT_tac "true : Bool"; -val falseT = canT_tac "false : Bool"; -val lamT = canT_tac "[| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)"; -val pairT = canT_tac "[| a:A; b:B(a) |] ==> :Sigma(A,B)"; -val inlT = canT_tac "a:A ==> inl(a) : A+B"; -val inrT = canT_tac "b:B ==> inr(b) : A+B"; - -val canTs = [oneT,trueT,falseT,pairT,lamT,inlT,inrT]; - -(*** Non-Canonical Type Rules ***) - -local -val lemma = prove_goal (the_context ()) "[| a:B(u); u=v |] ==> a : B(v)" - (fn prems => [cfast_tac prems 1]); -in -fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s - (fn major::prems => [(resolve_tac ([major] RL top_crls) 1), - (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), - (ALLGOALS (asm_simp_tac term_ss)), - (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' - etac bspec )), - (safe_tac (ccl_cs addSIs prems))]); -end; - -val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls; - -val ifT = ncanT_tac - "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> \ -\ if b then t else u : A(b)"; - -val applyT = ncanT_tac - "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)"; - -val splitT = ncanT_tac - "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p= |] ==> c(x,y):C() |] ==> \ -\ split(p,c):C(p)"; - -val whenT = ncanT_tac - "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); \ -\ !!y.[| y:B; p=inr(y) |] ==> b(y):C(inr(y)) |] ==> \ -\ when(p,a,b) : C(p)"; - -val ncanTs = [ifT,applyT,splitT,whenT]; - -(*** Subtypes ***) - -val SubtypeD1 = standard ((SubtypeXH RS iffD1) RS conjunct1); -val SubtypeD2 = standard ((SubtypeXH RS iffD1) RS conjunct2); - -val prems = goal (the_context ()) - "[| a:A; P(a) |] ==> a : {x:A. P(x)}"; -by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1)); -qed "SubtypeI"; - -val prems = goal (the_context ()) - "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q"; -by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1)); -qed "SubtypeE"; - -(*** Monotonicity ***) - -Goal "mono (%X. X)"; -by (REPEAT (ares_tac [monoI] 1)); -qed "idM"; - -Goal "mono(%X. A)"; -by (REPEAT (ares_tac [monoI,subset_refl] 1)); -qed "constM"; - -val major::prems = goal (the_context ()) - "mono(%X. A(X)) ==> mono(%X.[A(X)])"; -by (rtac (subsetI RS monoI) 1); -by (dtac (LiftXH RS iffD1) 1); -by (etac disjE 1); -by (etac (disjI1 RS (LiftXH RS iffD2)) 1); -by (rtac (disjI2 RS (LiftXH RS iffD2)) 1); -by (etac (major RS monoD RS subsetD) 1); -by (assume_tac 1); -qed "LiftM"; - -val prems = goal (the_context ()) - "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \ -\ mono(%X. Sigma(A(X),B(X)))"; -by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE - eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE - (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE - hyp_subst_tac 1)); -qed "SgM"; - -val prems = goal (the_context ()) - "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))"; -by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE - eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE - (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE - hyp_subst_tac 1)); -qed "PiM"; - -val prems = goal (the_context ()) - "[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))"; -by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE - eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE - (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE - hyp_subst_tac 1)); -qed "PlusM"; - -(**************** RECURSIVE TYPES ******************) - -(*** Conversion Rules for Fixed Points via monotonicity and Tarski ***) - -Goal "mono(%X. Unit+X)"; -by (REPEAT (ares_tac [PlusM,constM,idM] 1)); -qed "NatM"; -bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski)); - -Goal "mono(%X.(Unit+Sigma(A,%y. X)))"; -by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); -qed "ListM"; -bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski)); -bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski)); - -Goal "mono(%X.({} + Sigma(A,%y. X)))"; -by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); -qed "IListsM"; -bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski)); - -val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB]; - -(*** Exhaustion Rules ***) - -fun mk_iXH_tac teqs ddefs rls s = prove_goalw (the_context ()) ddefs s - (fn _ => [resolve_tac (teqs RL [XHlemma1]) 1, - fast_tac (set_cs addSIs canTs addSEs case_rls) 1]); - -val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs []; - -val NatXH = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))"; -val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))"; -val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))"; -val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)"; - -val iXHs = [NatXH,ListXH]; -val icase_rls = XH_to_Es iXHs; - -(*** Type Rules ***) - -val icanT_tac = mk_canT_tac (the_context ()) iXHs; -val incanT_tac = mk_ncanT_tac (the_context ()) [] icase_rls case_rls; - -val zeroT = icanT_tac "zero : Nat"; -val succT = icanT_tac "n:Nat ==> succ(n) : Nat"; -val nilT = icanT_tac "[] : List(A)"; -val consT = icanT_tac "[| h:A; t:List(A) |] ==> h$t : List(A)"; - -val icanTs = [zeroT,succT,nilT,consT]; - -val ncaseT = incanT_tac - "[| n:Nat; n=zero ==> b:C(zero); \ -\ !!x.[| x:Nat; n=succ(x) |] ==> c(x):C(succ(x)) |] ==> \ -\ ncase(n,b,c) : C(n)"; - -val lcaseT = incanT_tac - "[| l:List(A); l=[] ==> b:C([]); \ -\ !!h t.[| h:A; t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \ -\ lcase(l,b,c) : C(l)"; - -val incanTs = [ncaseT,lcaseT]; - -(*** Induction Rules ***) - -val ind_Ms = [NatM,ListM]; - -fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw (the_context ()) ddefs s - (fn major::prems => [resolve_tac (Ms RL ([major] RL (tdefs RL [def_induct]))) 1, - fast_tac (set_cs addSIs (prems @ canTs) addSEs case_rls) 1]); - -val ind_tac = mk_ind_tac ind_data_defs ind_type_defs ind_Ms canTs case_rls; - -val Nat_ind = ind_tac - "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==> \ -\ P(n)"; - -val List_ind = ind_tac - "[| l:List(A); P([]); \ -\ !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \ -\ P(l)"; - -val inds = [Nat_ind,List_ind]; - -(*** Primitive Recursive Rules ***) - -fun mk_prec_tac inds s = prove_goal (the_context ()) s - (fn major::prems => [resolve_tac ([major] RL inds) 1, - ALLGOALS (simp_tac term_ss THEN' - fast_tac (set_cs addSIs prems))]); -val prec_tac = mk_prec_tac inds; - -val nrecT = prec_tac - "[| n:Nat; b:C(zero); \ -\ !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==> \ -\ nrec(n,b,c) : C(n)"; - -val lrecT = prec_tac - "[| l:List(A); b:C([]); \ -\ !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> \ -\ lrec(l,b,c) : C(l)"; - -val precTs = [nrecT,lrecT]; - - -(*** Theorem proving ***) - -val [major,minor] = goal (the_context ()) - "[| : Sigma(A,B); [| a:A; b:B(a) |] ==> P \ -\ |] ==> P"; -by (rtac (major RS (XH_to_E SgXH)) 1); -by (rtac minor 1); -by (ALLGOALS (fast_tac term_cs)); -qed "SgE2"; - -(* General theorem proving ignores non-canonical term-formers, *) -(* - intro rules are type rules for canonical terms *) -(* - elim rules are case rules (no non-canonical terms appear) *) - -val type_cs = term_cs addSIs (SubtypeI::(canTs @ icanTs)) - addSEs (SubtypeE::(XH_to_Es XHs)); - - -(*** Infinite Data Types ***) - -val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) <= gfp(f)"; -by (rtac (lfp_lowerbound RS subset_trans) 1); -by (rtac (mono RS gfp_lemma3) 1); -by (rtac subset_refl 1); -qed "lfp_subset_gfp"; - -val prems = goal (the_context ()) - "[| a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ -\ t(a) : gfp(B)"; -by (rtac coinduct 1); -by (res_inst_tac [("P","%x. EX y:A. x=t(y)")] CollectI 1); -by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); -qed "gfpI"; - -val rew::prem::prems = goal (the_context ()) - "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ -\ t(a) : C"; -by (rewtac rew); -by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1)); -qed "def_gfpI"; - -(* EG *) - -val prems = goal (the_context ()) - "letrec g x be zero$g(x) in g(bot) : Lists(Nat)"; -by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1); -by (stac letrecB 1); -by (rewtac cons_def); -by (fast_tac type_cs 1); -result(); diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Type.thy --- a/src/CCL/Type.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Type.thy Tue Jul 18 02:22:38 2006 +0200 @@ -69,6 +69,419 @@ SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p= & A=B(x,y)})" -ML {* use_legacy_bindings (the_context ()) *} + +lemmas simp_type_defs = + Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def + and ind_type_defs = Nat_def List_def + and simp_data_defs = one_def inl_def inr_def + and ind_data_defs = zero_def succ_def nil_def cons_def + +lemma subsetXH: "A <= B <-> (ALL x. x:A --> x:B)" + by blast + + +subsection {* Exhaustion Rules *} + +lemma EmptyXH: "!!a. a : {} <-> False" + and SubtypeXH: "!!a A P. a : {x:A. P(x)} <-> (a:A & P(a))" + and UnitXH: "!!a. a : Unit <-> a=one" + and BoolXH: "!!a. a : Bool <-> a=true | a=false" + and PlusXH: "!!a A B. a : A+B <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))" + and PiXH: "!!a A B. a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))" + and SgXH: "!!a A B. a : SUM x:A. B(x) <-> (EX x:A. EX y:B(x).a=)" + unfolding simp_type_defs by blast+ + +lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH + +lemma LiftXH: "a : [A] <-> (a=bot | a:A)" + and TallXH: "a : TALL X. B(X) <-> (ALL X. a:B(X))" + and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))" + unfolding simp_type_defs by blast+ + +ML {* +bind_thms ("case_rls", XH_to_Es (thms "XHs")); +*} + + +subsection {* Canonical Type Rules *} + +lemma oneT: "one : Unit" + and trueT: "true : Bool" + and falseT: "false : Bool" + and lamT: "!!b B. [| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)" + and pairT: "!!b B. [| a:A; b:B(a) |] ==> :Sigma(A,B)" + and inlT: "a:A ==> inl(a) : A+B" + and inrT: "b:B ==> inr(b) : A+B" + by (blast intro: XHs [THEN iffD2])+ + +lemmas canTs = oneT trueT falseT pairT lamT inlT inrT + + +subsection {* Non-Canonical Type Rules *} + +lemma lem: "[| a:B(u); u=v |] ==> a : B(v)" + by blast + + +ML {* +local + val lemma = thm "lem" + val bspec = thm "bspec" + val bexE = thm "bexE" +in + + fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s + (fn major::prems => [(resolve_tac ([major] RL top_crls) 1), + (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), + (ALLGOALS (asm_simp_tac (simpset ()))), + (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' + etac bspec )), + (safe_tac (claset () addSIs prems))]) + + val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls +end +*} + +ML {* + +bind_thm ("ifT", ncanT_tac + "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> if b then t else u : A(b)"); + +bind_thm ("applyT", ncanT_tac "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)"); + +bind_thm ("splitT", ncanT_tac + "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p= |] ==> c(x,y):C() |] ==> split(p,c):C(p)"); + +bind_thm ("whenT", ncanT_tac + "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B; p=inr(y) |] ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)"); +*} + +lemmas ncanTs = ifT applyT splitT whenT + + +subsection {* Subtypes *} + +lemma SubtypeD1: "a : Subtype(A, P) ==> a : A" + and SubtypeD2: "a : Subtype(A, P) ==> P(a)" + by (simp_all add: SubtypeXH) + +lemma SubtypeI: "[| a:A; P(a) |] ==> a : {x:A. P(x)}" + by (simp add: SubtypeXH) + +lemma SubtypeE: "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q" + by (simp add: SubtypeXH) + + +subsection {* Monotonicity *} + +lemma idM: "mono (%X. X)" + apply (rule monoI) + apply assumption + done + +lemma constM: "mono(%X. A)" + apply (rule monoI) + apply (rule subset_refl) + done + +lemma "mono(%X. A(X)) ==> mono(%X.[A(X)])" + apply (rule subsetI [THEN monoI]) + apply (drule LiftXH [THEN iffD1]) + apply (erule disjE) + apply (erule disjI1 [THEN LiftXH [THEN iffD2]]) + apply (rule disjI2 [THEN LiftXH [THEN iffD2]]) + apply (drule (1) monoD) + apply blast + done + +lemma SgM: + "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> + mono(%X. Sigma(A(X),B(X)))" + by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls + dest!: monoD [THEN subsetD]) + +lemma PiM: + "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))" + by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls + dest!: monoD [THEN subsetD]) + +lemma PlusM: + "[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))" + by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls + dest!: monoD [THEN subsetD]) + + +subsection {* Recursive types *} + +subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *} + +lemma NatM: "mono(%X. Unit+X)"; + apply (rule PlusM constM idM)+ + done + +lemma def_NatB: "Nat = Unit + Nat" + apply (rule def_lfp_Tarski [OF Nat_def]) + apply (rule NatM) + done + +lemma ListM: "mono(%X.(Unit+Sigma(A,%y. X)))" + apply (rule PlusM SgM constM idM)+ + done + +lemma def_ListB: "List(A) = Unit + A * List(A)" + apply (rule def_lfp_Tarski [OF List_def]) + apply (rule ListM) + done + +lemma def_ListsB: "Lists(A) = Unit + A * Lists(A)" + apply (rule def_gfp_Tarski [OF Lists_def]) + apply (rule ListM) + done + +lemma IListsM: "mono(%X.({} + Sigma(A,%y. X)))" + apply (rule PlusM SgM constM idM)+ + done + +lemma def_IListsB: "ILists(A) = {} + A * ILists(A)" + apply (rule def_gfp_Tarski [OF ILists_def]) + apply (rule IListsM) + done + +lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB + + +subsection {* Exhaustion Rules *} + +lemma NatXH: "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))" + and ListXH: "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))" + and ListsXH: "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))" + and IListsXH: "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)" + unfolding ind_data_defs + by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+ + +lemmas iXHs = NatXH ListXH + +ML {* bind_thms ("icase_rls", XH_to_Es (thms "iXHs")) *} + + +subsection {* Type Rules *} + +lemma zeroT: "zero : Nat" + and succT: "n:Nat ==> succ(n) : Nat" + and nilT: "[] : List(A)" + and consT: "[| h:A; t:List(A) |] ==> h$t : List(A)" + by (blast intro: iXHs [THEN iffD2])+ + +lemmas icanTs = zeroT succT nilT consT + +ML {* +val incanT_tac = mk_ncanT_tac (the_context ()) [] (thms "icase_rls") (thms "case_rls"); + +bind_thm ("ncaseT", incanT_tac + "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat; n=succ(x) |] ==> c(x):C(succ(x)) |] ==> ncase(n,b,c) : C(n)"); + +bind_thm ("lcaseT", incanT_tac + "[| l:List(A); l=[] ==> b:C([]); !!h t.[| h:A; t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> lcase(l,b,c) : C(l)"); +*} + +lemmas incanTs = ncaseT lcaseT + + +subsection {* Induction Rules *} + +lemmas ind_Ms = NatM ListM + +lemma Nat_ind: "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" + apply (unfold ind_data_defs) + apply (erule def_induct [OF Nat_def _ NatM]) + apply (blast intro: canTs elim!: case_rls) + done + +lemma List_ind: + "[| l:List(A); P([]); !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> P(l)" + apply (unfold ind_data_defs) + apply (erule def_induct [OF List_def _ ListM]) + apply (blast intro: canTs elim!: case_rls) + done + +lemmas inds = Nat_ind List_ind + + +subsection {* Primitive Recursive Rules *} + +lemma nrecT: + "[| n:Nat; b:C(zero); + !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==> + nrec(n,b,c) : C(n)" + by (erule Nat_ind) auto + +lemma lrecT: + "[| l:List(A); b:C([]); + !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> + lrec(l,b,c) : C(l)" + by (erule List_ind) auto + +lemmas precTs = nrecT lrecT + + +subsection {* Theorem proving *} + +lemma SgE2: + "[| : Sigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" + unfolding SgXH by blast + +(* General theorem proving ignores non-canonical term-formers, *) +(* - intro rules are type rules for canonical terms *) +(* - elim rules are case rules (no non-canonical terms appear) *) + +ML {* bind_thms ("XHEs", XH_to_Es (thms "XHs")) *} + +lemmas [intro!] = SubtypeI canTs icanTs + and [elim!] = SubtypeE XHEs + + +subsection {* Infinite Data Types *} + +lemma lfp_subset_gfp: "mono(f) ==> lfp(f) <= gfp(f)" + apply (rule lfp_lowerbound [THEN subset_trans]) + apply (erule gfp_lemma3) + apply (rule subset_refl) + done + +lemma gfpI: + assumes "a:A" + and "!!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X)" + shows "t(a) : gfp(B)" + apply (rule coinduct) + apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI) + apply (blast intro!: prems)+ + done + +lemma def_gfpI: + "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> + t(a) : C" + apply unfold + apply (erule gfpI) + apply blast + done + +(* EG *) +lemma "letrec g x be zero$g(x) in g(bot) : Lists(Nat)" + apply (rule refl [THEN UnitXH [THEN iffD2], THEN Lists_def [THEN def_gfpI]]) + apply (subst letrecB) + apply (unfold cons_def) + apply blast + done + + +subsection {* Lemmas and tactics for using the rule @{text + "coinduct3"} on @{text "[="} and @{text "="} *} + +lemma lfpI: "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)" + apply (erule lfp_Tarski [THEN ssubst]) + apply assumption + done + +lemma ssubst_single: "[| a=a'; a' : A |] ==> a : A" + by simp + +lemma ssubst_pair: "[| a=a'; b=b'; : A |] ==> : A" + by simp + + +(***) + +ML {* + +local + val lfpI = thm "lfpI" + val coinduct3_mono_lemma = thm "coinduct3_mono_lemma" + fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems => + [fast_tac (claset () addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1]) +in +val ci3_RI = mk_thm "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)" +val ci3_AgenI = mk_thm "[| mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> a : lfp(%x. Agen(x) Un R Un A)" +val ci3_AI = mk_thm "[| mono(Agen); a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)" + +fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s + (fn prems => [rtac (genXH RS iffD2) 1, + simp_tac (simpset ()) 1, + TRY (fast_tac (claset () addIs + ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] + @ prems)) 1)]) +end; + +bind_thm ("ci3_RI", ci3_RI); +bind_thm ("ci3_AgenI", ci3_AgenI); +bind_thm ("ci3_AI", ci3_AI); +*} + + +subsection {* POgen *} + +lemma PO_refl: " : PO" + apply (rule po_refl [THEN PO_iff [THEN iffD1]]) + done + +ML {* + +val POgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "POgenXH") (thm "POgen_mono")) + [" : POgen(R)", + " : POgen(R)", + "[| : R; : R |] ==> <,> : POgen(R)", + "[|!!x. : R |] ==> : POgen(R)", + " : POgen(R)", + " : lfp(%x. POgen(x) Un R Un PO) ==> : POgen(lfp(%x. POgen(x) Un R Un PO))", + " : lfp(%x. POgen(x) Un R Un PO) ==> : POgen(lfp(%x. POgen(x) Un R Un PO))", + " : POgen(lfp(%x. POgen(x) Un R Un PO))", + " : lfp(%x. POgen(x) Un R Un PO) ==> : POgen(lfp(%x. POgen(x) Un R Un PO))", + "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))", + "[| : lfp(%x. POgen(x) Un R Un PO); : lfp(%x. POgen(x) Un R Un PO) |] ==> : POgen(lfp(%x. POgen(x) Un R Un PO))"]; + +fun POgen_tac (rla,rlb) i = + SELECT_GOAL (CLASET safe_tac) i THEN + rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN + (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @ + (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i)); + +*} + + +subsection {* EQgen *} + +lemma EQ_refl: " : EQ" + apply (rule refl [THEN EQ_iff [THEN iffD1]]) + done + +ML {* + +val EQgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "EQgenXH") (thm "EQgen_mono")) + [" : EQgen(R)", + " : EQgen(R)", + "[| : R; : R |] ==> <,> : EQgen(R)", + "[|!!x. : R |] ==> : EQgen(R)", + " : EQgen(R)", + " : lfp(%x. EQgen(x) Un R Un EQ) ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", + " : lfp(%x. EQgen(x) Un R Un EQ) ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", + " : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", + " : lfp(%x. EQgen(x) Un R Un EQ) ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", + "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", + "[| : lfp(%x. EQgen(x) Un R Un EQ); : lfp(%x. EQgen(x) Un R Un EQ) |] ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"]; + +fun EQgen_raw_tac i = + (REPEAT (resolve_tac (EQgenIs @ [thm "EQ_refl" RS (thm "EQgen_mono" RS ci3_AI)] @ + (EQgenIs RL [thm "EQgen_mono" RS ci3_AgenI]) @ [thm "EQgen_mono" RS ci3_RI]) i)) + +(* Goals of the form R <= EQgen(R) - rewrite elements : EQgen(R) using rews and *) +(* then reduce this to a goal : R (hopefully?) *) +(* rews are rewrite rules that would cause looping in the simpifier *) + +fun EQgen_tac simp_set rews i = + SELECT_GOAL + (TRY (CLASET safe_tac) THEN + resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [thm "ssubst_pair"])) i THEN + ALLGOALS (simp_tac simp_set) THEN + ALLGOALS EQgen_raw_tac) i +*} end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/Wfd.thy Tue Jul 18 02:22:38 2006 +0200 @@ -8,7 +8,6 @@ theory Wfd imports Trancl Type Hered -uses ("wfd.ML") ("genrec.ML") ("typecheck.ML") ("eval.ML") begin consts @@ -35,11 +34,599 @@ NatPR_def: "NatPR == {p. EX x:Nat. p=}" ListPR_def: "ListPR(A) == {p. EX h:A. EX t:List(A). p=}" -ML {* use_legacy_bindings (the_context ()) *} + +lemma wfd_induct: + assumes 1: "Wfd(R)" + and 2: "!!x.[| ALL y. : R --> P(y) |] ==> P(x)" + shows "P(a)" + apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD]) + using 2 apply blast + done + +lemma wfd_strengthen_lemma: + assumes 1: "!!x y. : R ==> Q(x)" + and 2: "ALL x. (ALL y. : R --> y : P) --> x : P" + and 3: "!!x. Q(x) ==> x:P" + shows "a:P" + apply (rule 2 [rule_format]) + using 1 3 + apply blast + done + +ML {* + local val wfd_strengthen_lemma = thm "wfd_strengthen_lemma" in + fun wfd_strengthen_tac s i = + res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN assume_tac (i+1) + end +*} + +lemma wf_anti_sym: "[| Wfd(r); :r; :r |] ==> P" + apply (subgoal_tac "ALL x. :r --> :r --> P") + apply blast + apply (erule wfd_induct) + apply blast + done + +lemma wf_anti_refl: "[| Wfd(r); : r |] ==> P" + apply (rule wf_anti_sym) + apply assumption+ + done + + +subsection {* Irreflexive transitive closure *} + +lemma trancl_wf: + assumes 1: "Wfd(R)" + shows "Wfd(R^+)" + apply (unfold Wfd_def) + apply (rule allI ballI impI)+ +(*must retain the universal formula for later use!*) + apply (rule allE, assumption) + apply (erule mp) + apply (rule 1 [THEN wfd_induct]) + apply (rule impI [THEN allI]) + apply (erule tranclE) + apply blast + apply (erule spec [THEN mp, THEN spec, THEN mp]) + apply assumption+ + done + + +subsection {* Lexicographic Ordering *} + +lemma lexXH: + "p : ra**rb <-> (EX a a' b b'. p = <,> & ( : ra | a=a' & : rb))" + unfolding lex_def by blast + +lemma lexI1: " : ra ==> <,> : ra**rb" + by (blast intro!: lexXH [THEN iffD2]) + +lemma lexI2: " : rb ==> <,> : ra**rb" + by (blast intro!: lexXH [THEN iffD2]) + +lemma lexE: + assumes 1: "p : ra**rb" + and 2: "!!a a' b b'.[| : ra; p=<,> |] ==> R" + and 3: "!!a b b'.[| : rb; p = <,> |] ==> R" + shows R + apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE]) + using 2 3 + apply blast + done + +lemma lex_pair: "[| p : r**s; !!a a' b b'. p = <,> ==> P |] ==>P" + apply (erule lexE) + apply blast+ + done + +lemma lex_wf: + assumes 1: "Wfd(R)" + and 2: "Wfd(S)" + shows "Wfd(R**S)" + apply (unfold Wfd_def) + apply safe + apply (tactic {* wfd_strengthen_tac "%x. EX a b. x=" 1 *}) + apply (blast elim!: lex_pair) + apply (subgoal_tac "ALL a b.:P") + apply blast + apply (rule 1 [THEN wfd_induct, THEN allI]) + apply (rule 2 [THEN wfd_induct, THEN allI]) back + apply (fast elim!: lexE) + done + + +subsection {* Mapping *} + +lemma wmapXH: "p : wmap(f,r) <-> (EX x y. p= & : r)" + unfolding wmap_def by blast + +lemma wmapI: " : r ==> : wmap(f,r)" + by (blast intro!: wmapXH [THEN iffD2]) + +lemma wmapE: "[| p : wmap(f,r); !!a b.[| : r; p= |] ==> R |] ==> R" + by (blast dest!: wmapXH [THEN iffD1]) + +lemma wmap_wf: + assumes 1: "Wfd(r)" + shows "Wfd(wmap(f,r))" + apply (unfold Wfd_def) + apply clarify + apply (subgoal_tac "ALL b. ALL a. f (a) =b-->a:P") + apply blast + apply (rule 1 [THEN wfd_induct, THEN allI]) + apply clarify + apply (erule spec [THEN mp]) + apply (safe elim!: wmapE) + apply (erule spec [THEN mp, THEN spec, THEN mp]) + apply assumption + apply (rule refl) + done + + +subsection {* Projections *} + +lemma wfstI: " : r ==> <,> : wmap(fst,r)" + apply (rule wmapI) + apply simp + done + +lemma wsndI: " : r ==> <,> : wmap(snd,r)" + apply (rule wmapI) + apply simp + done + +lemma wthdI: " : r ==> <>,>> : wmap(thd,r)" + apply (rule wmapI) + apply simp + done + + +subsection {* Ground well-founded relations *} + +lemma wfI: "[| Wfd(r); a : r |] ==> a : wf(r)" + unfolding wf_def by blast + +lemma Empty_wf: "Wfd({})" + unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE]) + +lemma wf_wf: "Wfd(wf(R))" + unfolding wf_def + apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE]) + apply simp_all + apply (rule Empty_wf) + done + +lemma NatPRXH: "p : NatPR <-> (EX x:Nat. p=)" + unfolding NatPR_def by blast + +lemma ListPRXH: "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=)" + unfolding ListPR_def by blast + +lemma NatPRI: "x : Nat ==> : NatPR" + by (auto simp: NatPRXH) + +lemma ListPRI: "[| t : List(A); h : A |] ==> : ListPR(A)" + by (auto simp: ListPRXH) + +lemma NatPR_wf: "Wfd(NatPR)" + apply (unfold Wfd_def) + apply clarify + apply (tactic {* wfd_strengthen_tac "%x. x:Nat" 1 *}) + apply (fastsimp iff: NatPRXH) + apply (erule Nat_ind) + apply (fastsimp iff: NatPRXH)+ + done + +lemma ListPR_wf: "Wfd(ListPR(A))" + apply (unfold Wfd_def) + apply clarify + apply (tactic {* wfd_strengthen_tac "%x. x:List (A)" 1 *}) + apply (fastsimp iff: ListPRXH) + apply (erule List_ind) + apply (fastsimp iff: ListPRXH)+ + done + + +subsection {* General Recursive Functions *} + +lemma letrecT: + assumes 1: "a : A" + and 2: "!!p g.[| p:A; ALL x:{x: A. :wf(R)}. g(x) : D(x) |] ==> h(p,g) : D(p)" + shows "letrec g x be h(x,g) in g(a) : D(a)" + apply (rule 1 [THEN rev_mp]) + apply (rule wf_wf [THEN wfd_induct]) + apply (subst letrecB) + apply (rule impI) + apply (erule 2) + apply blast + done + +lemma SPLITB: "SPLIT(,B) = B(a,b)" + unfolding SPLIT_def + apply (rule set_ext) + apply blast + done -use "wfd.ML" -use "genrec.ML" -use "typecheck.ML" -use "eval.ML" +lemma letrec2T: + assumes "a : A" + and "b : B" + and "!!p q g.[| p:A; q:B; + ALL x:A. ALL y:{y: B. <,>:wf(R)}. g(x,y) : D(x,y) |] ==> + h(p,q,g) : D(p,q)" + shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)" + apply (unfold letrec2_def) + apply (rule SPLITB [THEN subst]) + apply (assumption | rule letrecT pairT splitT prems)+ + apply (subst SPLITB) + apply (assumption | rule ballI SubtypeI prems)+ + apply (rule SPLITB [THEN subst]) + apply (assumption | rule letrecT SubtypeI pairT splitT prems | + erule bspec SubtypeE sym [THEN subst])+ + done + +lemma lem: "SPLIT(>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)" + by (simp add: SPLITB) + +lemma letrec3T: + assumes "a : A" + and "b : B" + and "c : C" + and "!!p q r g.[| p:A; q:B; r:C; + ALL x:A. ALL y:B. ALL z:{z:C. <>,>> : wf(R)}. + g(x,y,z) : D(x,y,z) |] ==> + h(p,q,r,g) : D(p,q,r)" + shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)" + apply (unfold letrec3_def) + apply (rule lem [THEN subst]) + apply (assumption | rule letrecT pairT splitT prems)+ + apply (simp add: SPLITB) + apply (assumption | rule ballI SubtypeI prems)+ + apply (rule lem [THEN subst]) + apply (assumption | rule letrecT SubtypeI pairT splitT prems | + erule bspec SubtypeE sym [THEN subst])+ + done + +lemmas letrecTs = letrecT letrec2T letrec3T + + +subsection {* Type Checking for Recursive Calls *} + +lemma rcallT: + "[| ALL x:{x:A.:wf(R)}.g(x):D(x); + g(a) : D(a) ==> g(a) : E; a:A; :wf(R) |] ==> + g(a) : E" + by blast + +lemma rcall2T: + "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); + g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <,>:wf(R) |] ==> + g(a,b) : E" + by blast + +lemma rcall3T: + "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}. g(x,y,z):D(x,y,z); + g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; + a:A; b:B; c:C; <>,>> : wf(R) |] ==> + g(a,b,c) : E" + by blast + +lemmas rcallTs = rcallT rcall2T rcall3T + + +subsection {* Instantiating an induction hypothesis with an equality assumption *} + +lemma hyprcallT: + assumes 1: "g(a) = b" + and 2: "ALL x:{x:A.:wf(R)}.g(x):D(x)" + and 3: "ALL x:{x:A.:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P" + and 4: "ALL x:{x:A.:wf(R)}.g(x):D(x) ==> a:A" + and 5: "ALL x:{x:A.:wf(R)}.g(x):D(x) ==> :wf(R)" + shows P + apply (rule 3 [OF 2, OF 1 [symmetric]]) + apply (rule rcallT [OF 2]) + apply assumption + apply (rule 4 [OF 2]) + apply (rule 5 [OF 2]) + done + +lemma hyprcall2T: + assumes 1: "g(a,b) = c" + and 2: "ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y)" + and 3: "[| c=g(a,b); g(a,b) : D(a,b) |] ==> P" + and 4: "a:A" + and 5: "b:B" + and 6: "<,>:wf(R)" + shows P + apply (rule 3) + apply (rule 1 [symmetric]) + apply (rule rcall2T) + apply assumption+ + done + +lemma hyprcall3T: + assumes 1: "g(a,b,c) = d" + and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z)" + and 3: "[| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P" + and 4: "a:A" + and 5: "b:B" + and 6: "c:C" + and 7: "<>,>> : wf(R)" + shows P + apply (rule 3) + apply (rule 1 [symmetric]) + apply (rule rcall3T) + apply assumption+ + done + +lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T + + +subsection {* Rules to Remove Induction Hypotheses after Type Checking *} + +lemma rmIH1: "[| ALL x:{x:A.:wf(R)}.g(x):D(x); P |] ==> P" . + +lemma rmIH2: "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); P |] ==> P" . + +lemma rmIH3: + "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); + P |] ==> + P" . + +lemmas rmIHs = rmIH1 rmIH2 rmIH3 + + +subsection {* Lemmas for constructors and subtypes *} + +(* 0-ary constructors do not need additional rules as they are handled *) +(* correctly by applying SubtypeI *) + +lemma Subtype_canTs: + "!!a b A B P. a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}" + "!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}" + "!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}" + "!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}" + "!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" + by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+ + +lemma letT: "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B" + apply (erule letB [THEN ssubst]) + apply assumption + done + +lemma applyT2: "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)" + apply (erule applyT) + apply assumption + done + +lemma rcall_lemma1: "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}" + by blast + +lemma rcall_lemma2: "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}" + by blast + +lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2 + + +subsection {* Typechecking *} + +ML {* + +local + +val type_rls = + thms "canTs" @ thms "icanTs" @ thms "applyT2" @ thms "ncanTs" @ thms "incanTs" @ + thms "precTs" @ thms "letrecTs" @ thms "letT" @ thms "Subtype_canTs"; + +val rcallT = thm "rcallT"; +val rcall2T = thm "rcall2T"; +val rcall3T = thm "rcall3T"; +val rcallTs = thms "rcallTs"; +val rcall_lemmas = thms "rcall_lemmas"; +val SubtypeE = thm "SubtypeE"; +val SubtypeI = thm "SubtypeI"; +val rmIHs = thms "rmIHs"; +val hyprcallTs = thms "hyprcallTs"; + +fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) + | bvars _ l = l + +fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t + | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t + | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t + | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t + | get_bno l n (t $ s) = get_bno l n t + | get_bno l n (Bound m) = (m-length(l),n) + +(* Not a great way of identifying induction hypothesis! *) +fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse + could_unify(x,hd (prems_of rcall2T)) orelse + could_unify(x,hd (prems_of rcall3T)) + +fun IHinst tac rls = SUBGOAL (fn (Bi,i) => + let val bvs = bvars Bi [] + val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi) + val rnames = map (fn x=> + let val (a,b) = get_bno [] 0 x + in (List.nth(bvs,a),b) end) ihs + fun try_IHs [] = no_tac + | try_IHs ((x,y)::xs) = tac [("g",x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs) + in try_IHs rnames end) + +fun is_rigid_prog t = + case (Logic.strip_assums_concl t) of + (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = []) + | _ => false +in + +fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i + in IHinst tac rcallTs i end THEN + eresolve_tac rcall_lemmas i + +fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE + rcall_tac i ORELSE + ematch_tac [SubtypeE] i ORELSE + match_tac [SubtypeI] i + +fun tc_step_tac prems = SUBGOAL (fn (Bi,i) => + if is_rigid_prog Bi then raw_step_tac prems i else no_tac) + +fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i + +val tac = typechk_tac [] 1 + +(*** Clean up Correctness Condictions ***) + +val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE' + hyp_subst_tac) + +val clean_ccs_tac = + let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i + in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE' + eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE' + hyp_subst_tac)) end + +fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN + clean_ccs_tac) i end +*} + + +subsection {* Evaluation *} + +ML {* + +local + +structure Data = GenericDataFun +( + val name = "CCL/eval"; + type T = thm list; + val empty = []; + val extend = I; + fun merge _ (rules1, rules2) = gen_union Drule.eq_thm_prop (rules1, rules2); + fun print _ _ = (); +); + +in + +val eval_add = Thm.declaration_attribute (Data.map o Drule.add_rule); +val eval_del = Thm.declaration_attribute (Data.map o Drule.del_rule); + +fun eval_tac ctxt ths = + METAHYPS (fn prems => + DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get (Context.Proof ctxt)) 1)) 1; + +val eval_setup = + Data.init #> + Attrib.add_attributes + [("eval", Attrib.add_del_args eval_add eval_del, "declaration of evaluation rule")] #> + Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt => + Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")]; + +end; + +*} + +setup eval_setup + +lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam + +lemma applyV [eval]: + assumes "f ---> lam x. b(x)" + and "b(a) ---> c" + shows "f ` a ---> c" + unfolding apply_def by (eval prems) + +lemma letV: + assumes 1: "t ---> a" + and 2: "f(a) ---> c" + shows "let x be t in f(x) ---> c" + apply (unfold let_def) + apply (rule 1 [THEN canonical]) + apply (tactic {* + REPEAT (DEPTH_SOLVE_1 (resolve_tac (thms "prems" @ thms "eval_rls") 1 ORELSE + etac (thm "substitute") 1)) *}) + done + +lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c" + apply (unfold fix_def) + apply (rule applyV) + apply (rule lamV) + apply assumption + done + +lemma letrecV: + "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> + letrec g x be h(x,g) in g(t) ---> c" + apply (unfold letrec_def) + apply (assumption | rule fixV applyV lamV)+ + done + +lemmas [eval] = letV letrecV fixV + +lemma V_rls [eval]: + "true ---> true" + "false ---> false" + "!!b c t u. [| b--->true; t--->c |] ==> if b then t else u ---> c" + "!!b c t u. [| b--->false; u--->c |] ==> if b then t else u ---> c" + "!!a b. ---> " + "!!a b c t h. [| t ---> ; h(a,b) ---> c |] ==> split(t,h) ---> c" + "zero ---> zero" + "!!n. succ(n) ---> succ(n)" + "!!c n t u. [| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c" + "!!c n t u x. [| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c" + "!!c n t u. [| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c" + "!!c n t u x. [| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c" + "[] ---> []" + "!!h t. h$t ---> h$t" + "!!c l t u. [| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c" + "!!c l t u x xs. [| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c" + "!!c l t u. [| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c" + "!!c l t u x xs. [| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c" + unfolding data_defs by eval+ + + +subsection {* Factorial *} + +lemma + "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) + in f(succ(succ(zero))) ---> ?a" + by eval + +lemma + "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) + in f(succ(succ(succ(zero)))) ---> ?a" + by eval + +subsection {* Less Than Or Equal *} + +lemma + "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) + in f() ---> ?a" + by eval + +lemma + "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) + in f() ---> ?a" + by eval + +lemma + "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) + in f() ---> ?a" + by eval + + +subsection {* Reverse *} + +lemma + "letrec id l be lcase(l,[],%x xs. x$id(xs)) + in id(zero$succ(zero)$[]) ---> ?a" + by eval + +lemma + "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) + in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a" + by eval + +end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/coinduction.ML --- a/src/CCL/coinduction.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,108 +0,0 @@ -(* Title: CCL/Coinduction.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Lemmas and tactics for using the rule coinduct3 on [= and =. -*) - -val [mono,prem] = goal (the_context ()) "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)"; -by (stac (mono RS lfp_Tarski) 1); -by (rtac prem 1); -qed "lfpI"; - -val prems = goal (the_context ()) "[| a=a'; a' : A |] ==> a : A"; -by (simp_tac (term_ss addsimps prems) 1); -qed "ssubst_single"; - -val prems = goal (the_context ()) "[| a=a'; b=b'; : A |] ==> : A"; -by (simp_tac (term_ss addsimps prems) 1); -qed "ssubst_pair"; - -(***) - -local -fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems => - [fast_tac (term_cs addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1]); -in -val ci3_RI = mk_thm "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"; -val ci3_AgenI = mk_thm "[| mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> \ -\ a : lfp(%x. Agen(x) Un R Un A)"; -val ci3_AI = mk_thm "[| mono(Agen); a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)"; -end; - -fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s - (fn prems => [rtac (genXH RS iffD2) 1, - (simp_tac term_ss 1), - TRY (fast_tac (term_cs addIs - ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] - @ prems)) 1)]); - -(** POgen **) - -goal (the_context ()) " : PO"; -by (rtac (po_refl RS (XH_to_D PO_iff)) 1); -qed "PO_refl"; - -val POgenIs = map (mk_genIs (the_context ()) data_defs POgenXH POgen_mono) - [" : POgen(R)", - " : POgen(R)", - "[| : R; : R |] ==> <,> : POgen(R)", - "[|!!x. : R |] ==> : POgen(R)", - " : POgen(R)", - " : lfp(%x. POgen(x) Un R Un PO) ==> \ -\ : POgen(lfp(%x. POgen(x) Un R Un PO))", - " : lfp(%x. POgen(x) Un R Un PO) ==> \ -\ : POgen(lfp(%x. POgen(x) Un R Un PO))", - " : POgen(lfp(%x. POgen(x) Un R Un PO))", - " : lfp(%x. POgen(x) Un R Un PO) ==> \ -\ : POgen(lfp(%x. POgen(x) Un R Un PO))", - "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))", - "[| : lfp(%x. POgen(x) Un R Un PO); \ -\ : lfp(%x. POgen(x) Un R Un PO) |] ==> \ -\ : POgen(lfp(%x. POgen(x) Un R Un PO))"]; - -fun POgen_tac (rla,rlb) i = - SELECT_GOAL (safe_tac ccl_cs) i THEN - rtac (rlb RS (rla RS ssubst_pair)) i THEN - (REPEAT (resolve_tac (POgenIs @ [PO_refl RS (POgen_mono RS ci3_AI)] @ - (POgenIs RL [POgen_mono RS ci3_AgenI]) @ [POgen_mono RS ci3_RI]) i)); - -(** EQgen **) - -goal (the_context ()) " : EQ"; -by (rtac (refl RS (EQ_iff RS iffD1)) 1); -qed "EQ_refl"; - -val EQgenIs = map (mk_genIs (the_context ()) data_defs EQgenXH EQgen_mono) -[" : EQgen(R)", - " : EQgen(R)", - "[| : R; : R |] ==> <,> : EQgen(R)", - "[|!!x. : R |] ==> : EQgen(R)", - " : EQgen(R)", - " : lfp(%x. EQgen(x) Un R Un EQ) ==> \ -\ : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - " : lfp(%x. EQgen(x) Un R Un EQ) ==> \ -\ : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - " : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - " : lfp(%x. EQgen(x) Un R Un EQ) ==> \ -\ : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", - "[| : lfp(%x. EQgen(x) Un R Un EQ); \ -\ : lfp(%x. EQgen(x) Un R Un EQ) |] ==> \ -\ : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"]; - -fun EQgen_raw_tac i = - (REPEAT (resolve_tac (EQgenIs @ [EQ_refl RS (EQgen_mono RS ci3_AI)] @ - (EQgenIs RL [EQgen_mono RS ci3_AgenI]) @ [EQgen_mono RS ci3_RI]) i)); - -(* Goals of the form R <= EQgen(R) - rewrite elements : EQgen(R) using rews and *) -(* then reduce this to a goal : R (hopefully?) *) -(* rews are rewrite rules that would cause looping in the simpifier *) - -fun EQgen_tac simp_set rews i = - SELECT_GOAL - (TRY (safe_tac ccl_cs) THEN - resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [ssubst_pair])) i THEN - ALLGOALS (simp_tac simp_set) THEN - ALLGOALS EQgen_raw_tac) i; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/equalities.ML --- a/src/CCL/equalities.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,127 +0,0 @@ -(* Title: CCL/equalities.ML - ID: $Id$ - -Equalities involving union, intersection, inclusion, etc. -*) - -val eq_cs = set_cs addSIs [equalityI]; - -(** Binary Intersection **) - -goal (the_context ()) "A Int A = A"; -by (fast_tac eq_cs 1); -qed "Int_absorb"; - -goal (the_context ()) "A Int B = B Int A"; -by (fast_tac eq_cs 1); -qed "Int_commute"; - -goal (the_context ()) "(A Int B) Int C = A Int (B Int C)"; -by (fast_tac eq_cs 1); -qed "Int_assoc"; - -goal (the_context ()) "(A Un B) Int C = (A Int C) Un (B Int C)"; -by (fast_tac eq_cs 1); -qed "Int_Un_distrib"; - -goal (the_context ()) "(A<=B) <-> (A Int B = A)"; -by (fast_tac (eq_cs addSEs [equalityE]) 1); -qed "subset_Int_eq"; - -(** Binary Union **) - -goal (the_context ()) "A Un A = A"; -by (fast_tac eq_cs 1); -qed "Un_absorb"; - -goal (the_context ()) "A Un B = B Un A"; -by (fast_tac eq_cs 1); -qed "Un_commute"; - -goal (the_context ()) "(A Un B) Un C = A Un (B Un C)"; -by (fast_tac eq_cs 1); -qed "Un_assoc"; - -goal (the_context ()) "(A Int B) Un C = (A Un C) Int (B Un C)"; -by (fast_tac eq_cs 1); -qed "Un_Int_distrib"; - -goal (the_context ()) - "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; -by (fast_tac eq_cs 1); -qed "Un_Int_crazy"; - -goal (the_context ()) "(A<=B) <-> (A Un B = B)"; -by (fast_tac (eq_cs addSEs [equalityE]) 1); -qed "subset_Un_eq"; - -(** Simple properties of Compl -- complement of a set **) - -goal (the_context ()) "A Int Compl(A) = {x. False}"; -by (fast_tac eq_cs 1); -qed "Compl_disjoint"; - -goal (the_context ()) "A Un Compl(A) = {x. True}"; -by (fast_tac eq_cs 1); -qed "Compl_partition"; - -goal (the_context ()) "Compl(Compl(A)) = A"; -by (fast_tac eq_cs 1); -qed "double_complement"; - -goal (the_context ()) "Compl(A Un B) = Compl(A) Int Compl(B)"; -by (fast_tac eq_cs 1); -qed "Compl_Un"; - -goal (the_context ()) "Compl(A Int B) = Compl(A) Un Compl(B)"; -by (fast_tac eq_cs 1); -qed "Compl_Int"; - -goal (the_context ()) "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"; -by (fast_tac eq_cs 1); -qed "Compl_UN"; - -goal (the_context ()) "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"; -by (fast_tac eq_cs 1); -qed "Compl_INT"; - -(*Halmos, Naive Set Theory, page 16.*) - -goal (the_context ()) "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)"; -by (fast_tac (eq_cs addSEs [equalityE]) 1); -qed "Un_Int_assoc_eq"; - - -(** Big Union and Intersection **) - -goal (the_context ()) "Union(A Un B) = Union(A) Un Union(B)"; -by (fast_tac eq_cs 1); -qed "Union_Un_distrib"; - -val prems = goal (the_context ()) - "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})"; -by (fast_tac (eq_cs addSEs [equalityE]) 1); -qed "Union_disjoint"; - -goal (the_context ()) "Inter(A Un B) = Inter(A) Int Inter(B)"; -by (best_tac eq_cs 1); -qed "Inter_Un_distrib"; - -(** Unions and Intersections of Families **) - -goal (the_context ()) "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"; -by (fast_tac eq_cs 1); -qed "UN_eq"; - -(*Look: it has an EXISTENTIAL quantifier*) -goal (the_context ()) "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"; -by (fast_tac eq_cs 1); -qed "INT_eq"; - -goal (the_context ()) "A Int Union(B) = (UN C:B. A Int C)"; -by (fast_tac eq_cs 1); -qed "Int_Union_image"; - -goal (the_context ()) "A Un Inter(B) = (INT C:B. A Un C)"; -by (fast_tac eq_cs 1); -qed "Un_Inter_image"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/eval.ML --- a/src/CCL/eval.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -(* Title: 92/CCL/eval - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge -*) - -(*** Evaluation ***) - -val EVal_rls = ref [trueV,falseV,pairV,lamV,caseVtrue,caseVfalse,caseVpair,caseVlam]; -val eval_tac = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls) 1); -fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1); - -val prems = goalw (the_context ()) [apply_def] - "[| f ---> lam x. b(x); b(a) ---> c |] ==> f ` a ---> c"; -by (ceval_tac prems); -qed "applyV"; - -EVal_rls := !EVal_rls @ [applyV]; - -val major::prems = goalw (the_context ()) [let_def] - "[| t ---> a; f(a) ---> c |] ==> let x be t in f(x) ---> c"; -by (rtac (major RS canonical) 1); -by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE - etac substitute 1))); -qed "letV"; - -val prems = goalw (the_context ()) [fix_def] - "f(fix(f)) ---> c ==> fix(f) ---> c"; -by (rtac applyV 1); -by (rtac lamV 1); -by (resolve_tac prems 1); -qed "fixV"; - -val prems = goalw (the_context ()) [letrec_def] - "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> \ -\ letrec g x be h(x,g) in g(t) ---> c"; -by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1)); -qed "letrecV"; - -EVal_rls := !EVal_rls @ [letV,letrecV,fixV]; - -fun mk_V_rl s = prove_goalw (the_context ()) data_defs s (fn prems => [ceval_tac prems]); - -val V_rls = map mk_V_rl - ["true ---> true", - "false ---> false", - "[| b--->true; t--->c |] ==> if b then t else u ---> c", - "[| b--->false; u--->c |] ==> if b then t else u ---> c", - " ---> ", - "[| t ---> ; h(a,b) ---> c |] ==> split(t,h) ---> c", - "zero ---> zero", - "succ(n) ---> succ(n)", - "[| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c", - "[| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c", - "[| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c", - "[| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c", - "[] ---> []", - "h$t ---> h$t", - "[| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c", - "[| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c", - "[| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c", - "[| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"]; - -EVal_rls := !EVal_rls @ V_rls; - -(* Factorial *) - -val prems = goal (the_context ()) - "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \ -\ in f(succ(succ(zero))) ---> ?a"; -by (ceval_tac []); - -val prems = goal (the_context ()) - "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \ -\ in f(succ(succ(succ(zero)))) ---> ?a"; -by (ceval_tac []); - -(* Less Than Or Equal *) - -fun isle x y = prove_goal (the_context ()) - ("letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) \ -\ in f(<"^x^","^y^">) ---> ?a") - (fn prems => [ceval_tac []]); - -isle "succ(zero)" "succ(zero)"; -isle "succ(zero)" "succ(succ(succ(succ(zero))))"; -isle "succ(succ(succ(succ(succ(zero)))))" "succ(succ(succ(succ(zero))))"; - - -(* Reverse *) - -val prems = goal (the_context ()) - "letrec id l be lcase(l,[],%x xs. x$id(xs)) \ -\ in id(zero$succ(zero)$[]) ---> ?a"; -by (ceval_tac []); - -val prems = goal (the_context ()) - "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) \ -\ in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"; -by (ceval_tac []); diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/Flag.ML --- a/src/CCL/ex/Flag.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -(* Title: CCL/ex/Flag.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -(******) - -val flag_defs = [Colour_def,red_def,white_def,blue_def,ccase_def]; - -(******) - -val ColourXH = mk_XH_tac (the_context ()) (simp_type_defs @flag_defs) [] - "a : Colour <-> (a=red | a=white | a=blue)"; - -val Colour_case = XH_to_E ColourXH; - -val redT = mk_canT_tac (the_context ()) [ColourXH] "red : Colour"; -val whiteT = mk_canT_tac (the_context ()) [ColourXH] "white : Colour"; -val blueT = mk_canT_tac (the_context ()) [ColourXH] "blue : Colour"; - - -val ccaseT = mk_ncanT_tac (the_context ()) flag_defs case_rls case_rls - "[| c:Colour; \ -\ c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> \ -\ ccase(c,r,w,b) : C(c)"; - -(***) - -val prems = goalw (the_context ()) [flag_def] - "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"; -by (typechk_tac [redT,whiteT,blueT,ccaseT] 1); -by clean_ccs_tac; -by (etac (ListPRI RS (ListPR_wf RS wfI)) 1); -by (assume_tac 1); -result(); - - -val prems = goalw (the_context ()) [flag_def] - "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"; -by (gen_ccs_tac [redT,whiteT,blueT,ccaseT] 1); -by (REPEAT_SOME (ares_tac [ListPRI RS (ListPR_wf RS wfI)])); diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/Flag.thy --- a/src/CCL/ex/Flag.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/ex/Flag.thy Tue Jul 18 02:22:38 2006 +0200 @@ -44,6 +44,35 @@ (c mem lb = true --> c=blue)) & Perm(l,lr @ lw @ lb)" -ML {* use_legacy_bindings (the_context ()) *} + +lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def + +lemma ColourXH: "a : Colour <-> (a=red | a=white | a=blue)" + unfolding simp_type_defs flag_defs by blast + +lemma redT: "red : Colour" + and whiteT: "white : Colour" + and blueT: "blue : Colour" + unfolding ColourXH by blast+ + +ML {* +bind_thm ("ccaseT", mk_ncanT_tac (the_context ()) + (thms "flag_defs") (thms "case_rls") (thms "case_rls") + "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> ccase(c,r,w,b) : C(c)"); +*} + + +lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" + apply (unfold flag_def) + apply (tactic {* typechk_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *}) + apply (tactic clean_ccs_tac) + apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) + apply assumption + done + +lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}" + apply (unfold flag_def) + apply (tactic {* gen_ccs_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *}) + oops end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/List.ML --- a/src/CCL/ex/List.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,101 +0,0 @@ -(* Title: CCL/ex/List.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -val list_defs = [map_def,comp_def,append_def,filter_def,flat_def, - insert_def,isort_def,partition_def,qsort_def]; - -(****) - -val listBs = map (fn s=>prove_goalw (the_context ()) list_defs s (fn _ => [simp_tac term_ss 1])) - ["(f o g) = (%a. f(g(a)))", - "(f o g)(a) = f(g(a))", - "map(f,[]) = []", - "map(f,x$xs) = f(x)$map(f,xs)", - "[] @ m = m", - "x$xs @ m = x$(xs @ m)", - "filter(f,[]) = []", - "filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)", - "flat([]) = []", - "flat(x$xs) = x @ flat(xs)", - "insert(f,a,[]) = a$[]", - "insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)"]; - -val list_ss = nat_ss addsimps listBs; - -(****) - -val [prem] = goal (the_context ()) "n:Nat ==> map(f) ^ n ` [] = []"; -by (rtac (prem RS Nat_ind) 1); -by (ALLGOALS (asm_simp_tac list_ss)); -qed "nmapBnil"; - -val [prem] = goal (the_context ()) "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)"; -by (rtac (prem RS Nat_ind) 1); -by (ALLGOALS (asm_simp_tac list_ss)); -qed "nmapBcons"; - -(***) - -val prems = goalw (the_context ()) [map_def] - "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)"; -by (typechk_tac prems 1); -qed "mapT"; - -val prems = goalw (the_context ()) [append_def] - "[| l : List(A); m : List(A) |] ==> l @ m : List(A)"; -by (typechk_tac prems 1); -qed "appendT"; - -val prems = goal (the_context ()) - "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}"; -by (cut_facts_tac prems 1); -by (fast_tac (set_cs addSIs [SubtypeI,appendT] addSEs [SubtypeE]) 1); -qed "appendTS"; - -val prems = goalw (the_context ()) [filter_def] - "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)"; -by (typechk_tac prems 1); -qed "filterT"; - -val prems = goalw (the_context ()) [flat_def] - "l : List(List(A)) ==> flat(l) : List(A)"; -by (typechk_tac (appendT::prems) 1); -qed "flatT"; - -val prems = goalw (the_context ()) [insert_def] - "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)"; -by (typechk_tac prems 1); -qed "insertT"; - -val prems = goal (the_context ()) - "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> \ -\ insert(f,a,l) : {x:List(A). P(x)}"; -by (cut_facts_tac prems 1); -by (fast_tac (set_cs addSIs [SubtypeI,insertT] addSEs [SubtypeE]) 1); -qed "insertTS"; - -val prems = goalw (the_context ()) [partition_def] - "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)"; -by (typechk_tac prems 1); -by clean_ccs_tac; -by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2); -by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1); -by (REPEAT (atac 1)); -qed "partitionT"; - -(*** Correctness Conditions for Insertion Sort ***) - - -val prems = goalw (the_context ()) [isort_def] - "f:A->A->Bool ==> isort(f) : PROD l:List(A).{x: List(A). Ord(f,x) & Perm(x,l)}"; -by (gen_ccs_tac ([insertTS,insertT]@prems) 1); - - -(*** Correctness Conditions for Quick Sort ***) - -val prems = goalw (the_context ()) [qsort_def] - "f:A->A->Bool ==> qsort(f) : PROD l:List(A).{x: List(A). Ord(f,x) & Perm(x,l)}"; -by (gen_ccs_tac ([partitionT,appendTS,appendT]@prems) 1); diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/List.thy --- a/src/CCL/ex/List.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/ex/List.thy Tue Jul 18 02:22:38 2006 +0200 @@ -43,6 +43,80 @@ in split(p,%x y. qsortx(x) @ h$qsortx(y))) in qsortx(l)" -ML {* use_legacy_bindings (the_context ()) *} + +lemmas list_defs = map_def comp_def append_def filter_def flat_def + insert_def isort_def partition_def qsort_def + +lemma listBs [simp]: + "!!f g. (f o g) = (%a. f(g(a)))" + "!!a f g. (f o g)(a) = f(g(a))" + "!!f. map(f,[]) = []" + "!!f x xs. map(f,x$xs) = f(x)$map(f,xs)" + "!!m. [] @ m = m" + "!!x xs m. x$xs @ m = x$(xs @ m)" + "!!f. filter(f,[]) = []" + "!!f x xs. filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)" + "flat([]) = []" + "!!x xs. flat(x$xs) = x @ flat(xs)" + "!!a f. insert(f,a,[]) = a$[]" + "!!a f xs. insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)" + by (simp_all add: list_defs) + +lemma nmapBnil: "n:Nat ==> map(f) ^ n ` [] = []" + apply (erule Nat_ind) + apply simp_all + done + +lemma nmapBcons: "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)" + apply (erule Nat_ind) + apply simp_all + done + + +lemma mapT: "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)" + apply (unfold map_def) + apply (tactic "typechk_tac [] 1") + apply blast + done + +lemma appendT: "[| l : List(A); m : List(A) |] ==> l @ m : List(A)" + apply (unfold append_def) + apply (tactic "typechk_tac [] 1") + done + +lemma appendTS: + "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}" + by (blast intro!: SubtypeI appendT elim!: SubtypeE) + +lemma filterT: "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)" + apply (unfold filter_def) + apply (tactic "typechk_tac [] 1") + done + +lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)" + apply (unfold flat_def) + apply (tactic {* typechk_tac [thm "appendT"] 1 *}) + done + +lemma insertT: "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)" + apply (unfold insert_def) + apply (tactic "typechk_tac [] 1") + done + +lemma insertTS: + "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> + insert(f,a,l) : {x:List(A). P(x)}" + by (blast intro!: SubtypeI insertT elim!: SubtypeE) + +lemma partitionT: + "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)" + apply (unfold partition_def) + apply (tactic "typechk_tac [] 1") + apply (tactic clean_ccs_tac) + apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) + apply assumption+ + apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) + apply assumption+ + done end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/Nat.ML --- a/src/CCL/ex/Nat.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* Title: CCL/ex/Nat.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -val nat_defs = [not_def,add_def,mult_def,sub_def,le_def,lt_def,ack_def,napply_def]; - -val natBs = map (fn s=>prove_goalw (the_context ()) nat_defs s (fn _ => [simp_tac term_ss 1])) - ["not(true) = false", - "not(false) = true", - "zero #+ n = n", - "succ(n) #+ m = succ(n #+ m)", - "zero #* n = zero", - "succ(n) #* m = m #+ (n #* m)", - "f^zero`a = a", - "f^succ(n)`a = f(f^n`a)"]; - -val nat_ss = term_ss addsimps natBs; - -(*** Lemma for napply ***) - -val [prem] = goal (the_context ()) "n:Nat ==> f^n`f(a) = f^succ(n)`a"; -by (rtac (prem RS Nat_ind) 1); -by (ALLGOALS (asm_simp_tac nat_ss)); -qed "napply_f"; - -(****) - -val prems = goalw (the_context ()) [add_def] "[| a:Nat; b:Nat |] ==> a #+ b : Nat"; -by (typechk_tac prems 1); -qed "addT"; - -val prems = goalw (the_context ()) [mult_def] "[| a:Nat; b:Nat |] ==> a #* b : Nat"; -by (typechk_tac (addT::prems) 1); -qed "multT"; - -(* Defined to return zero if a a #- b : Nat"; -by (typechk_tac (prems) 1); -by clean_ccs_tac; -by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1); -qed "subT"; - -val prems = goalw (the_context ()) [le_def] "[| a:Nat; b:Nat |] ==> a #<= b : Bool"; -by (typechk_tac (prems) 1); -by clean_ccs_tac; -by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1); -qed "leT"; - -val prems = goalw (the_context ()) [not_def,lt_def] "[| a:Nat; b:Nat |] ==> a #< b : Bool"; -by (typechk_tac (prems@[leT]) 1); -qed "ltT"; - -(* Correctness conditions for subtractive division **) - -val prems = goalw (the_context ()) [div_def] - "[| a:Nat; b:{x:Nat.~x=zero} |] ==> a ## b : {x:Nat. DIV(a,b,x)}"; -by (gen_ccs_tac (prems@[ltT,subT]) 1); - -(* Termination Conditions for Ackermann's Function *) - -val prems = goalw (the_context ()) [ack_def] - "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat"; -by (gen_ccs_tac prems 1); -val relI = NatPR_wf RS (NatPR_wf RS lex_wf RS wfI); -by (REPEAT (eresolve_tac [NatPRI RS (lexI1 RS relI),NatPRI RS (lexI2 RS relI)] 1)); -result(); diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/Nat.thy --- a/src/CCL/ex/Nat.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/ex/Nat.thy Tue Jul 18 02:22:38 2006 +0200 @@ -40,7 +40,65 @@ ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) in ack(a,b)" -ML {* use_legacy_bindings (the_context ()) *} +lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def + +lemma natBs [simp]: + "not(true) = false" + "not(false) = true" + "zero #+ n = n" + "succ(n) #+ m = succ(n #+ m)" + "zero #* n = zero" + "succ(n) #* m = m #+ (n #* m)" + "f^zero`a = a" + "f^succ(n)`a = f(f^n`a)" + by (simp_all add: nat_defs) + + +lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a" + apply (erule Nat_ind) + apply simp_all + done + +lemma addT: "[| a:Nat; b:Nat |] ==> a #+ b : Nat" + apply (unfold add_def) + apply (tactic {* typechk_tac [] 1 *}) + done + +lemma multT: "[| a:Nat; b:Nat |] ==> a #* b : Nat" + apply (unfold add_def mult_def) + apply (tactic {* typechk_tac [] 1 *}) + done + +(* Defined to return zero if a a #- b : Nat" + apply (unfold sub_def) + apply (tactic {* typechk_tac [] 1 *}) + apply (tactic clean_ccs_tac) + apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) + done + +lemma leT: "[| a:Nat; b:Nat |] ==> a #<= b : Bool" + apply (unfold le_def) + apply (tactic {* typechk_tac [] 1 *}) + apply (tactic clean_ccs_tac) + apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) + done + +lemma ltT: "[| a:Nat; b:Nat |] ==> a #< b : Bool" + apply (unfold not_def lt_def) + apply (tactic {* typechk_tac [thm "leT"] 1 *}) + done + + +subsection {* Termination Conditions for Ackermann's Function *} + +lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]] + +lemma "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat" + apply (unfold ack_def) + apply (tactic "gen_ccs_tac [] 1") + apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ + done end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/Stream.ML --- a/src/CCL/ex/Stream.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,110 +0,0 @@ -(* Title: CCL/ex/Stream.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Proving properties about infinite lists using coinduction: - Lists(A) is the set of all finite and infinite lists of elements of A. - ILists(A) is the set of infinite lists of elements of A. -*) - -(*** Map of composition is composition of maps ***) - -val prems = goal (the_context ()) "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))"; -by (eq_coinduct3_tac - "{p. EX x y. p= & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}" 1); -by (fast_tac (ccl_cs addSIs prems) 1); -by (safe_tac type_cs); -by (etac (XH_to_E ListsXH) 1); -by (EQgen_tac list_ss [] 1); -by (simp_tac list_ss 1); -by (fast_tac ccl_cs 1); -qed "map_comp"; - -(*** Mapping the identity function leaves a list unchanged ***) - -val prems = goal (the_context ()) "l:Lists(A) ==> map(%x. x,l) = l"; -by (eq_coinduct3_tac - "{p. EX x y. p= & (EX l:Lists(A).x=map(%x. x,l) & y=l)}" 1); -by (fast_tac (ccl_cs addSIs prems) 1); -by (safe_tac type_cs); -by (etac (XH_to_E ListsXH) 1); -by (EQgen_tac list_ss [] 1); -by (fast_tac ccl_cs 1); -qed "map_id"; - -(*** Mapping distributes over append ***) - -val prems = goal (the_context ()) - "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)"; -by (eq_coinduct3_tac "{p. EX x y. p= & (EX l:Lists(A).EX m:Lists(A). \ -\ x=map(f,l@m) & y=map(f,l) @ map(f,m))}" 1); -by (fast_tac (ccl_cs addSIs prems) 1); -by (safe_tac type_cs); -by (etac (XH_to_E ListsXH) 1); -by (EQgen_tac list_ss [] 1); -by (etac (XH_to_E ListsXH) 1); -by (EQgen_tac list_ss [] 1); -by (fast_tac ccl_cs 1); -qed "map_append"; - -(*** Append is associative ***) - -val prems = goal (the_context ()) - "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m"; -by (eq_coinduct3_tac - "{p. EX x y. p= & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \ -\ x=k @ l @ m & y=(k @ l) @ m)}" 1); -by (fast_tac (ccl_cs addSIs prems) 1); -by (safe_tac type_cs); -by (etac (XH_to_E ListsXH) 1); -by (EQgen_tac list_ss [] 1); -by (fast_tac ccl_cs 2); -by (DEPTH_SOLVE (etac (XH_to_E ListsXH) 1 THEN EQgen_tac list_ss [] 1)); -qed "append_assoc"; - -(*** Appending anything to an infinite list doesn't alter it ****) - -val prems = goal (the_context ()) "l:ILists(A) ==> l @ m = l"; -by (eq_coinduct3_tac - "{p. EX x y. p= & (EX l:ILists(A).EX m. x=l@m & y=l)}" 1); -by (fast_tac (ccl_cs addSIs prems) 1); -by (safe_tac set_cs); -by (etac (XH_to_E IListsXH) 1); -by (EQgen_tac list_ss [] 1); -by (fast_tac ccl_cs 1); -qed "ilist_append"; - -(*** The equivalance of two versions of an iteration function ***) -(* *) -(* fun iter1(f,a) = a$iter1(f,f(a)) *) -(* fun iter2(f,a) = a$map(f,iter2(f,a)) *) - -Goalw [iter1_def] "iter1(f,a) = a$iter1(f,f(a))"; -by (rtac (letrecB RS trans) 1); -by (simp_tac term_ss 1); -qed "iter1B"; - -Goalw [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))"; -by (rtac (letrecB RS trans) 1); -by (rtac refl 1); -qed "iter2B"; - -val [prem] =goal (the_context ()) - "n:Nat ==> \ -\ map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"; -by (res_inst_tac [("P", "%x. ?lhs(x) = ?rhs")] (iter2B RS ssubst) 1); -by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1); -qed "iter2Blemma"; - -Goal "iter1(f,a) = iter2(f,a)"; -by (eq_coinduct3_tac - "{p. EX x y. p= & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" - 1); -by (fast_tac (type_cs addSIs [napplyBzero RS sym, - napplyBzero RS sym RS arg_cong]) 1); -by (EQgen_tac list_ss [iter1B,iter2Blemma] 1); -by (stac napply_f 1 THEN atac 1); -by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1); -by (fast_tac type_cs 1); -qed "iter1_iter2_eq"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/ex/Stream.thy --- a/src/CCL/ex/Stream.thy Mon Jul 17 18:42:38 2006 +0200 +++ b/src/CCL/ex/Stream.thy Tue Jul 18 02:22:38 2006 +0200 @@ -19,6 +19,127 @@ iter1_def: "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" iter2_def: "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" -ML {* use_legacy_bindings (the_context ()) *} + +(* +Proving properties about infinite lists using coinduction: + Lists(A) is the set of all finite and infinite lists of elements of A. + ILists(A) is the set of infinite lists of elements of A. +*) + + +subsection {* Map of composition is composition of maps *} + +lemma map_comp: + assumes 1: "l:Lists(A)" + shows "map(f o g,l) = map(f,map(g,l))" + apply (tactic {* eq_coinduct3_tac + "{p. EX x y. p= & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *}) + apply (blast intro: 1) + apply safe + apply (drule ListsXH [THEN iffD1]) + apply (tactic "EQgen_tac (simpset ()) [] 1") + apply fastsimp + done + +(*** Mapping the identity function leaves a list unchanged ***) + +lemma map_id: + assumes 1: "l:Lists(A)" + shows "map(%x. x,l) = l" + apply (tactic {* eq_coinduct3_tac + "{p. EX x y. p= & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *}) + apply (blast intro: 1) + apply safe + apply (drule ListsXH [THEN iffD1]) + apply (tactic "EQgen_tac (simpset ()) [] 1") + apply blast + done + + +subsection {* Mapping distributes over append *} + +lemma map_append: + assumes "l:Lists(A)" + and "m:Lists(A)" + shows "map(f,l@m) = map(f,l) @ map(f,m)" + apply (tactic {* eq_coinduct3_tac + "{p. EX x y. p= & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *}) + apply (blast intro: prems) + apply safe + apply (drule ListsXH [THEN iffD1]) + apply (tactic "EQgen_tac (simpset ()) [] 1") + apply (drule ListsXH [THEN iffD1]) + apply (tactic "EQgen_tac (simpset ()) [] 1") + apply blast + done + + +subsection {* Append is associative *} + +lemma append_assoc: + assumes "k:Lists(A)" + and "l:Lists(A)" + and "m:Lists(A)" + shows "k @ l @ m = (k @ l) @ m" + apply (tactic {* eq_coinduct3_tac + "{p. EX x y. p= & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*}) + apply (blast intro: prems) + apply safe + apply (drule ListsXH [THEN iffD1]) + apply (tactic "EQgen_tac (simpset ()) [] 1") + prefer 2 + apply blast + apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1 + THEN EQgen_tac (simpset ()) [] 1) *}) + done + + +subsection {* Appending anything to an infinite list doesn't alter it *} + +lemma ilist_append: + assumes "l:ILists(A)" + shows "l @ m = l" + apply (tactic {* eq_coinduct3_tac + "{p. EX x y. p= & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *}) + apply (blast intro: prems) + apply safe + apply (drule IListsXH [THEN iffD1]) + apply (tactic "EQgen_tac (simpset ()) [] 1") + apply blast + done + +(*** The equivalance of two versions of an iteration function ***) +(* *) +(* fun iter1(f,a) = a$iter1(f,f(a)) *) +(* fun iter2(f,a) = a$map(f,iter2(f,a)) *) + +lemma iter1B: "iter1(f,a) = a$iter1(f,f(a))" + apply (unfold iter1_def) + apply (rule letrecB [THEN trans]) + apply simp + done + +lemma iter2B: "iter2(f,a) = a $ map(f,iter2(f,a))" + apply (unfold iter2_def) + apply (rule letrecB [THEN trans]) + apply (rule refl) + done + +lemma iter2Blemma: + "n:Nat ==> + map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))" + apply (rule_tac P = "%x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst]) + apply (simp add: nmapBcons) + done + +lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)" + apply (tactic {* eq_coinduct3_tac + "{p. EX x y. p= & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) + apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong]) + apply (tactic {* EQgen_tac (simpset ()) [thm "iter1B", thm "iter2Blemma"] 1 *}) + apply (subst napply_f, assumption) + apply (rule_tac f1 = f in napplyBsucc [THEN subst]) + apply blast + done end diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/genrec.ML --- a/src/CCL/genrec.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,165 +0,0 @@ -(* Title: CCL/genrec.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -*) - -(*** General Recursive Functions ***) - -val major::prems = goal (the_context ()) - "[| a : A; \ -\ !!p g.[| p:A; ALL x:{x: A. :wf(R)}. g(x) : D(x) |] ==>\ -\ h(p,g) : D(p) |] ==> \ -\ letrec g x be h(x,g) in g(a) : D(a)"; -by (rtac (major RS rev_mp) 1); -by (rtac (wf_wf RS wfd_induct) 1); -by (stac letrecB 1); -by (rtac impI 1); -by (eresolve_tac prems 1); -by (rtac ballI 1); -by (etac (spec RS mp RS mp) 1); -by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1)); -qed "letrecT"; - -goalw (the_context ()) [SPLIT_def] "SPLIT(,B) = B(a,b)"; -by (rtac set_ext 1); -by (fast_tac ccl_cs 1); -qed "SPLITB"; - -val prems = goalw (the_context ()) [letrec2_def] - "[| a : A; b : B; \ -\ !!p q g.[| p:A; q:B; \ -\ ALL x:A. ALL y:{y: B. <,>:wf(R)}. g(x,y) : D(x,y) |] ==>\ -\ h(p,q,g) : D(p,q) |] ==> \ -\ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"; -by (rtac (SPLITB RS subst) 1); -by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); -by (stac SPLITB 1); -by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); -by (rtac (SPLITB RS subst) 1); -by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE - eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); -qed "letrec2T"; - -goal (the_context ()) "SPLIT(>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"; -by (simp_tac (ccl_ss addsimps [SPLITB]) 1); -qed "lemma"; - -val prems = goalw (the_context ()) [letrec3_def] - "[| a : A; b : B; c : C; \ -\ !!p q r g.[| p:A; q:B; r:C; \ -\ ALL x:A. ALL y:B. ALL z:{z:C. <>,>> : wf(R)}. \ -\ g(x,y,z) : D(x,y,z) |] ==>\ -\ h(p,q,r,g) : D(p,q,r) |] ==> \ -\ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"; -by (rtac (lemma RS subst) 1); -by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); -by (simp_tac (ccl_ss addsimps [SPLITB]) 1); -by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); -by (rtac (lemma RS subst) 1); -by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE - eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); -qed "letrec3T"; - -val letrecTs = [letrecT,letrec2T,letrec3T]; - - -(*** Type Checking for Recursive Calls ***) - -val major::prems = goal (the_context ()) - "[| ALL x:{x:A.:wf(R)}.g(x):D(x); \ -\ g(a) : D(a) ==> g(a) : E; a:A; :wf(R) |] ==> \ -\ g(a) : E"; -by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); -qed "rcallT"; - -val major::prems = goal (the_context ()) - "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); \ -\ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <,>:wf(R) |] ==> \ -\ g(a,b) : E"; -by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); -qed "rcall2T"; - -val major::prems = goal (the_context ()) - "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}. g(x,y,z):D(x,y,z); \ -\ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \ -\ a:A; b:B; c:C; <>,>> : wf(R) |] ==> \ -\ g(a,b,c) : E"; -by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1)); -qed "rcall3T"; - -val rcallTs = [rcallT,rcall2T,rcall3T]; - -(*** Instantiating an induction hypothesis with an equality assumption ***) - -val prems = goal (the_context ()) - "[| g(a) = b; ALL x:{x:A.:wf(R)}.g(x):D(x); \ -\ [| ALL x:{x:A.:wf(R)}.g(x):D(x); b=g(a); g(a) : D(a) |] ==> P; \ -\ ALL x:{x:A.:wf(R)}.g(x):D(x) ==> a:A; \ -\ ALL x:{x:A.:wf(R)}.g(x):D(x) ==> :wf(R) |] ==> \ -\ P"; -by (resolve_tac (prems RL prems) 1); -by (resolve_tac (prems RL [sym]) 1); -by (rtac rcallT 1); -by (REPEAT (ares_tac prems 1)); -val hyprcallT = result(); - -val prems = goal (the_context ()) - "[| g(a) = b; ALL x:{x:A.:wf(R)}.g(x):D(x);\ -\ [| b=g(a); g(a) : D(a) |] ==> P; a:A; :wf(R) |] ==> \ -\ P"; -by (resolve_tac (prems) 1); -by (resolve_tac (prems RL [sym]) 1); -by (rtac rcallT 1); -by (REPEAT (ares_tac prems 1)); -qed "hyprcallT"; - -val prems = goal (the_context ()) - "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); \ -\ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \ -\ a:A; b:B; <,>:wf(R) |] ==> \ -\ P"; -by (resolve_tac (prems) 1); -by (resolve_tac (prems RL [sym]) 1); -by (rtac rcall2T 1); -by (REPEAT (ares_tac prems 1)); -qed "hyprcall2T"; - -val prems = goal (the_context ()) - "[| g(a,b,c) = d; \ -\ ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); \ -\ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \ -\ a:A; b:B; c:C; <>,>> : wf(R) |] ==> \ -\ P"; -by (resolve_tac (prems) 1); -by (resolve_tac (prems RL [sym]) 1); -by (rtac rcall3T 1); -by (REPEAT (ares_tac prems 1)); -qed "hyprcall3T"; - -val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T]; - -(*** Rules to Remove Induction Hypotheses after Type Checking ***) - -val prems = goal (the_context ()) - "[| ALL x:{x:A.:wf(R)}.g(x):D(x); P |] ==> \ -\ P"; -by (REPEAT (ares_tac prems 1)); -qed "rmIH1"; - -val prems = goal (the_context ()) - "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); P |] ==> \ -\ P"; -by (REPEAT (ares_tac prems 1)); -qed "rmIH2"; - -val prems = goal (the_context ()) - "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); \ -\ P |] ==> \ -\ P"; -by (REPEAT (ares_tac prems 1)); -qed "rmIH3"; - -val rmIHs = [rmIH1,rmIH2,rmIH3]; - diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/mono.ML --- a/src/CCL/mono.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: CCL/mono.ML - ID: $Id$ - -Monotonicity of various operations. -*) - -val prems = goal (the_context ()) "A<=B ==> Union(A) <= Union(B)"; -by (cfast_tac prems 1); -qed "Union_mono"; - -val prems = goal (the_context ()) "[| B<=A |] ==> Inter(A) <= Inter(B)"; -by (cfast_tac prems 1); -qed "Inter_anti_mono"; - -val prems = goal (the_context ()) - "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \ -\ (UN x:A. f(x)) <= (UN x:B. g(x))"; -by (REPEAT (eresolve_tac [UN_E,ssubst] 1 - ORELSE ares_tac ((prems RL [subsetD]) @ [subsetI,UN_I]) 1)); -qed "UN_mono"; - -val prems = goal (the_context ()) - "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \ -\ (INT x:A. f(x)) <= (INT x:A. g(x))"; -by (REPEAT (ares_tac ((prems RL [subsetD]) @ [subsetI,INT_I]) 1 - ORELSE etac INT_D 1)); -qed "INT_anti_mono"; - -val prems = goal (the_context ()) "[| A<=C; B<=D |] ==> A Un B <= C Un D"; -by (cfast_tac prems 1); -qed "Un_mono"; - -val prems = goal (the_context ()) "[| A<=C; B<=D |] ==> A Int B <= C Int D"; -by (cfast_tac prems 1); -qed "Int_mono"; - -val prems = goal (the_context ()) "[| A<=B |] ==> Compl(B) <= Compl(A)"; -by (cfast_tac prems 1); -qed "Compl_anti_mono"; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/subset.ML --- a/src/CCL/subset.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,118 +0,0 @@ -(* Title: CCL/subsetI - ID: $Id$ - -Derived rules involving subsets. -Union and Intersection as lattice operations. -*) - -(*** Big Union -- least upper bound of a set ***) - -val prems = goal (the_context ()) - "B:A ==> B <= Union(A)"; -by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)); -qed "Union_upper"; - -val prems = goal (the_context ()) - "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; -by (REPEAT (ares_tac [subsetI] 1 - ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1)); -qed "Union_least"; - - -(*** Big Intersection -- greatest lower bound of a set ***) - -val prems = goal (the_context ()) - "B:A ==> Inter(A) <= B"; -by (REPEAT (resolve_tac (prems@[subsetI]) 1 - ORELSE etac InterD 1)); -qed "Inter_lower"; - -val prems = goal (the_context ()) - "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; -by (REPEAT (ares_tac [subsetI,InterI] 1 - ORELSE eresolve_tac (prems RL [subsetD]) 1)); -qed "Inter_greatest"; - -(*** Finite Union -- the least upper bound of 2 sets ***) - -goal (the_context ()) "A <= A Un B"; -by (REPEAT (ares_tac [subsetI,UnI1] 1)); -qed "Un_upper1"; - -goal (the_context ()) "B <= A Un B"; -by (REPEAT (ares_tac [subsetI,UnI2] 1)); -qed "Un_upper2"; - -val prems = goal (the_context ()) "[| A<=C; B<=C |] ==> A Un B <= C"; -by (cut_facts_tac prems 1); -by (DEPTH_SOLVE (ares_tac [subsetI] 1 - ORELSE eresolve_tac [UnE,subsetD] 1)); -qed "Un_least"; - -(*** Finite Intersection -- the greatest lower bound of 2 sets *) - -goal (the_context ()) "A Int B <= A"; -by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); -qed "Int_lower1"; - -goal (the_context ()) "A Int B <= B"; -by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); -qed "Int_lower2"; - -val prems = goal (the_context ()) "[| C<=A; C<=B |] ==> C <= A Int B"; -by (cut_facts_tac prems 1); -by (REPEAT (ares_tac [subsetI,IntI] 1 - ORELSE etac subsetD 1)); -qed "Int_greatest"; - -(*** Monotonicity ***) - -val [prem] = goalw (the_context ()) [mono_def] - "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; -by (REPEAT (ares_tac [allI, impI, prem] 1)); -qed "monoI"; - -val [major,minor] = goalw (the_context ()) [mono_def] - "[| mono(f); A <= B |] ==> f(A) <= f(B)"; -by (rtac (major RS spec RS spec RS mp) 1); -by (rtac minor 1); -qed "monoD"; - -val [prem] = goal (the_context ()) "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; -by (rtac Un_least 1); -by (rtac (Un_upper1 RS (prem RS monoD)) 1); -by (rtac (Un_upper2 RS (prem RS monoD)) 1); -qed "mono_Un"; - -val [prem] = goal (the_context ()) "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; -by (rtac Int_greatest 1); -by (rtac (Int_lower1 RS (prem RS monoD)) 1); -by (rtac (Int_lower2 RS (prem RS monoD)) 1); -qed "mono_Int"; - -(****) - -val set_cs = FOL_cs - addSIs [ballI, subsetI, InterI, INT_I, CollectI, - ComplI, IntI, UnCI, singletonI] - addIs [bexI, UnionI, UN_I] - addSEs [bexE, UnionE, UN_E, - CollectE, ComplE, IntE, UnE, emptyE, singletonE] - addEs [ballE, InterD, InterE, INT_D, INT_E, subsetD, subsetCE]; - -fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs; - -fun prover s = prove_goal (the_context ()) s (fn _=>[fast_tac set_cs 1]); - -val mem_rews = [trivial_set,empty_eq] @ (map prover - [ "(a : A Un B) <-> (a:A | a:B)", - "(a : A Int B) <-> (a:A & a:B)", - "(a : Compl(B)) <-> (~a:B)", - "(a : {b}) <-> (a=b)", - "(a : {}) <-> False", - "(a : {x. P(x)}) <-> P(a)" ]); - -val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong]; - -val set_ss = FOL_ss addcongs set_congs - addsimps mem_rews; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/typecheck.ML --- a/src/CCL/typecheck.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,134 +0,0 @@ -(* Title: CCL/typecheck.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge -*) - -(*** Lemmas for constructors and subtypes ***) - -(* 0-ary constructors do not need additional rules as they are handled *) -(* correctly by applying SubtypeI *) -(* -val Subtype_canTs = - let fun tac prems = cut_facts_tac prems 1 THEN - REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE - etac SubtypeE 1) - fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems]) - in map solve - ["P(one) ==> one : {x:Unit.P(x)}", - "P(true) ==> true : {x:Bool.P(x)}", - "P(false) ==> false : {x:Bool.P(x)}", - "a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}", - "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}", - "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}", - "P(zero) ==> zero : {x:Nat.P(x)}", - "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}", - "P([]) ==> [] : {x:List(A).P(x)}", - "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" - ] end; -*) -val Subtype_canTs = - let fun tac prems = cut_facts_tac prems 1 THEN - REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE - etac SubtypeE 1) - fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems]) - in map solve - ["a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}", - "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}", - "b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}", - "a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}", - "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" - ] end; - -val prems = goal (the_context ()) - "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; -by (cut_facts_tac prems 1); -by (etac (letB RS ssubst) 1); -by (assume_tac 1); -qed "letT"; - -val prems = goal (the_context ()) - "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)"; -by (REPEAT (ares_tac (applyT::prems) 1)); -qed "applyT2"; - -val prems = goal (the_context ()) - "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}"; -by (fast_tac (type_cs addSIs prems) 1); -qed "rcall_lemma1"; - -val prems = goal (the_context ()) - "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}"; -by (cut_facts_tac prems 1); -by (fast_tac (type_cs addSIs prems) 1); -qed "rcall_lemma2"; - -val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2]; - -(***********************************TYPECHECKING*************************************) - -fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) - | bvars _ l = l; - -fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t - | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t - | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t - | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t - | get_bno l n (t $ s) = get_bno l n t - | get_bno l n (Bound m) = (m-length(l),n); - -(* Not a great way of identifying induction hypothesis! *) -fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse - could_unify(x,hd (prems_of rcall2T)) orelse - could_unify(x,hd (prems_of rcall3T)); - -fun IHinst tac rls = SUBGOAL (fn (Bi,i) => - let val bvs = bvars Bi []; - val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi); - val rnames = map (fn x=> - let val (a,b) = get_bno [] 0 x - in (List.nth(bvs,a),b) end) ihs; - fun try_IHs [] = no_tac - | try_IHs ((x,y)::xs) = tac [("g",x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs); - in try_IHs rnames end); - -(*****) - -val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@ - precTs@letrecTs@[letT]@Subtype_canTs; - -fun is_rigid_prog t = - case (Logic.strip_assums_concl t) of - (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = []) - | _ => false; - -fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i; - in IHinst tac rcallTs i end THEN - eresolve_tac rcall_lemmas i; - -fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE - rcall_tac i ORELSE - ematch_tac [SubtypeE] i ORELSE - match_tac [SubtypeI] i; - -fun tc_step_tac prems = SUBGOAL (fn (Bi,i) => - if is_rigid_prog Bi then raw_step_tac prems i else no_tac); - -fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i; - -val tac = typechk_tac [] 1; - - -(*** Clean up Correctness Condictions ***) - -val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE' - hyp_subst_tac); - -val clean_ccs_tac = - let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i; - in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE' - eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE' - hyp_subst_tac)) end; - -fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN - clean_ccs_tac) i; diff -r 804927db5311 -r 98acc6d0fab6 src/CCL/wfd.ML --- a/src/CCL/wfd.ML Mon Jul 17 18:42:38 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,193 +0,0 @@ -(* Title: CCL/Wfd.ML - ID: $Id$ -*) - -(***********) - -val [major,prem] = goalw (the_context ()) [Wfd_def] - "[| Wfd(R); \ -\ !!x.[| ALL y. : R --> P(y) |] ==> P(x) |] ==> \ -\ P(a)"; -by (rtac (major RS spec RS mp RS spec RS CollectD) 1); -by (fast_tac (set_cs addSIs [prem RS CollectI]) 1); -qed "wfd_induct"; - -val [p1,p2,p3] = goal (the_context ()) - "[| !!x y. : R ==> Q(x); \ -\ ALL x. (ALL y. : R --> y : P) --> x : P; \ -\ !!x. Q(x) ==> x:P |] ==> a:P"; -by (rtac (p2 RS spec RS mp) 1); -by (fast_tac (set_cs addSIs [p1 RS p3]) 1); -qed "wfd_strengthen_lemma"; - -fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN - assume_tac (i+1); - -val wfd::prems = goal (the_context ()) "[| Wfd(r); :r; :r |] ==> P"; -by (subgoal_tac "ALL x. :r --> :r --> P" 1); -by (fast_tac (FOL_cs addIs prems) 1); -by (rtac (wfd RS wfd_induct) 1); -by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); -qed "wf_anti_sym"; - -val prems = goal (the_context ()) "[| Wfd(r); : r |] ==> P"; -by (rtac wf_anti_sym 1); -by (REPEAT (resolve_tac prems 1)); -qed "wf_anti_refl"; - -(*** Irreflexive transitive closure ***) - -val [prem] = goal (the_context ()) "Wfd(R) ==> Wfd(R^+)"; -by (rewtac Wfd_def); -by (REPEAT (ares_tac [allI,ballI,impI] 1)); -(*must retain the universal formula for later use!*) -by (rtac allE 1 THEN assume_tac 1); -by (etac mp 1); -by (rtac (prem RS wfd_induct) 1); -by (rtac (impI RS allI) 1); -by (etac tranclE 1); -by (fast_tac ccl_cs 1); -by (etac (spec RS mp RS spec RS mp) 1); -by (REPEAT (atac 1)); -qed "trancl_wf"; - -(*** Lexicographic Ordering ***) - -Goalw [lex_def] - "p : ra**rb <-> (EX a a' b b'. p = <,> & ( : ra | a=a' & : rb))"; -by (fast_tac ccl_cs 1); -qed "lexXH"; - -val prems = goal (the_context ()) - " : ra ==> <,> : ra**rb"; -by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); -qed "lexI1"; - -val prems = goal (the_context ()) - " : rb ==> <,> : ra**rb"; -by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); -qed "lexI2"; - -val major::prems = goal (the_context ()) - "[| p : ra**rb; \ -\ !!a a' b b'.[| : ra; p=<,> |] ==> R; \ -\ !!a b b'.[| : rb; p = <,> |] ==> R |] ==> \ -\ R"; -by (rtac (major RS (lexXH RS iffD1) RS exE) 1); -by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); -by (ALLGOALS (fast_tac ccl_cs)); -qed "lexE"; - -val [major,minor] = goal (the_context ()) - "[| p : r**s; !!a a' b b'. p = <,> ==> P |] ==>P"; -by (rtac (major RS lexE) 1); -by (ALLGOALS (fast_tac (set_cs addSEs [minor]))); -qed "lex_pair"; - -val [wfa,wfb] = goal (the_context ()) - "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)"; -by (rewtac Wfd_def); -by (safe_tac ccl_cs); -by (wfd_strengthen_tac "%x. EX a b. x=" 1); -by (fast_tac (term_cs addSEs [lex_pair]) 1); -by (subgoal_tac "ALL a b.:P" 1); -by (fast_tac ccl_cs 1); -by (rtac (wfa RS wfd_induct RS allI) 1); -by (rtac (wfb RS wfd_induct RS allI) 1);back(); -by (fast_tac (type_cs addSEs [lexE]) 1); -qed "lex_wf"; - -(*** Mapping ***) - -Goalw [wmap_def] - "p : wmap(f,r) <-> (EX x y. p= & : r)"; -by (fast_tac ccl_cs 1); -qed "wmapXH"; - -val prems = goal (the_context ()) - " : r ==> : wmap(f,r)"; -by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1); -qed "wmapI"; - -val major::prems = goal (the_context ()) - "[| p : wmap(f,r); !!a b.[| : r; p= |] ==> R |] ==> R"; -by (rtac (major RS (wmapXH RS iffD1) RS exE) 1); -by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); -by (ALLGOALS (fast_tac ccl_cs)); -qed "wmapE"; - -val [wf] = goal (the_context ()) - "Wfd(r) ==> Wfd(wmap(f,r))"; -by (rewtac Wfd_def); -by (safe_tac ccl_cs); -by (subgoal_tac "ALL b. ALL a. f(a)=b-->a:P" 1); -by (fast_tac ccl_cs 1); -by (rtac (wf RS wfd_induct RS allI) 1); -by (safe_tac ccl_cs); -by (etac (spec RS mp) 1); -by (safe_tac (ccl_cs addSEs [wmapE])); -by (etac (spec RS mp RS spec RS mp) 1); -by (assume_tac 1); -by (rtac refl 1); -qed "wmap_wf"; - -(* Projections *) - -val prems = goal (the_context ()) " : r ==> <,> : wmap(fst,r)"; -by (rtac wmapI 1); -by (simp_tac (term_ss addsimps prems) 1); -qed "wfstI"; - -val prems = goal (the_context ()) " : r ==> <,> : wmap(snd,r)"; -by (rtac wmapI 1); -by (simp_tac (term_ss addsimps prems) 1); -qed "wsndI"; - -val prems = goal (the_context ()) " : r ==> <>,>> : wmap(thd,r)"; -by (rtac wmapI 1); -by (simp_tac (term_ss addsimps prems) 1); -qed "wthdI"; - -(*** Ground well-founded relations ***) - -val prems = goalw (the_context ()) [wf_def] - "[| Wfd(r); a : r |] ==> a : wf(r)"; -by (fast_tac (set_cs addSIs prems) 1); -qed "wfI"; - -val prems = goalw (the_context ()) [Wfd_def] "Wfd({})"; -by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1); -qed "Empty_wf"; - -val prems = goalw (the_context ()) [wf_def] "Wfd(wf(R))"; -by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1); -by (ALLGOALS (asm_simp_tac CCL_ss)); -by (rtac Empty_wf 1); -qed "wf_wf"; - -Goalw [NatPR_def] "p : NatPR <-> (EX x:Nat. p=)"; -by (fast_tac set_cs 1); -qed "NatPRXH"; - -Goalw [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=)"; -by (fast_tac set_cs 1); -qed "ListPRXH"; - -val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2)); -val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2))); - -Goalw [Wfd_def] "Wfd(NatPR)"; -by (safe_tac set_cs); -by (wfd_strengthen_tac "%x. x:Nat" 1); -by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1); -by (etac Nat_ind 1); -by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH]))); -qed "NatPR_wf"; - -Goalw [Wfd_def] "Wfd(ListPR(A))"; -by (safe_tac set_cs); -by (wfd_strengthen_tac "%x. x:List(A)" 1); -by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1); -by (etac List_ind 1); -by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH]))); -qed "ListPR_wf";