diff -r 000000000000 -r a5a9c433f639 src/CCL/ccl.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CCL/ccl.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,362 @@ +(* Title: CCL/ccl + ID: $Id$ + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +For ccl.thy. +*) + +open CCL; + +val ccl_data_defs = [apply_def,fix_def]; + +(*** Simplifier for pre-order and equality ***) + +structure CCL_SimpData : SIMP_DATA = + struct + val refl_thms = [refl, po_refl, iff_refl] + val trans_thms = [trans, iff_trans, po_trans] + val red1 = iffD1 + val red2 = iffD2 + val mk_rew_rules = mk_rew_rules + val case_splits = [] (*NO IF'S!*) + val norm_thms = norm_thms + val subst_thms = [subst]; + val dest_red = dest_red + end; + +structure CCL_Simp = SimpFun(CCL_SimpData); +open CCL_Simp; + +val auto_ss = empty_ss setauto (fn hyps => ares_tac (TrueI::hyps)); + +val po_refl_iff_T = make_iff_T po_refl; + +val CCL_ss = auto_ss addcongs (FOL_congs @ set_congs) + addrews ([po_refl_iff_T] @ FOL_rews @ mem_rews); + +(*** Congruence Rules ***) + +(*similar to AP_THM in Gordon's HOL*) +val fun_cong = prove_goal CCL.thy "(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*) +val arg_cong = prove_goal CCL.thy "x=y ==> f(x)=f(y)" + (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); + +goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))"; +by (SIMP_TAC (CCL_ss addrews [eq_iff]) 1); +by (fast_tac (set_cs addIs [po_abstractn]) 1); +val 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; + +fun ccl_mk_congs thy cs = map abs_prems (mk_congs thy cs); + +val ccl_congs = ccl_mk_congs CCL.thy + ["op [=","SIM","POgen","EQgen","pair","lambda","case","op `","fix"]; + +val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot]; + +(*** Termination and Divergence ***) + +goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot"; +br iff_refl 1; +val Trm_iff = result(); + +goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot"; +br iff_refl 1; +val Dvg_iff = result(); + +(*** Constructors are injective ***) + +val prems = goal CCL.thy + "[| x=a; y=b; x=y |] ==> a=b"; +by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals])))); +val eq_lemma = result(); + +fun mk_inj_rl thy rews congs s = + let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]); + val inj_lemmas = flat (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 addrews rews + addcongs congs) 1) + in prove_goal thy s (fn _ => [tac]) + end; + +val ccl_injs = map (mk_inj_rl CCL.thy caseBs ccl_congs) + [" = <-> (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.Symtab.lookup(#const_tab(Sign.rep_sg sg),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 CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)" + (fn _ => [SIMP_TAC (CCL_ss addcongs ccl_congs) 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 = flat (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 CCL.thy s (fn _=> [rtac notI 1,eresolve_tac rls 1]) + in map (mk_raw_dstnct_thm caseB_lemmas) + (mk_dstnct_rls CCL.thy ["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 addrews (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 = flat (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 addrews ccl_rews addcongs ccl_congs; + +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 Set.thy "[| A=B; a:B <-> P |] ==> a:A <-> P"; +brs (prems RL [major RS ssubst]) 1; +val XHlemma1 = result(); + +goal CCL.thy "(P(t,t') <-> Q) --> ( : {p.EX t t'.p= & P(t,t')} <-> Q)"; +by (fast_tac ccl_cs 1); +val XHlemma2 = result() RS mp; + +(*** Pre-Order ***) + +goalw CCL.thy [POgen_def,SIM_def] "mono(%X.POgen(X))"; +br 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)); +val POgen_mono = result(); + +goalw CCL.thy [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))"; +br (iff_refl RS XHlemma2) 1; +val POgenXH = result(); + +goal CCL.thy + "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 addrews [PO_iff]) 1); +br (rewrite_rule [POgen_def,SIM_def] + (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1; +br (iff_refl RS XHlemma2) 1; +val poXH = result(); + +goal CCL.thy "bot [= b"; +br (poXH RS iffD2) 1; +by (SIMP_TAC ccl_ss 1); +val po_bot = result(); + +goal CCL.thy "a [= bot --> a=bot"; +br impI 1; +bd (poXH RS iffD1) 1; +be rev_mp 1; +by (SIMP_TAC ccl_ss 1); +val bot_poleast = result() RS mp; + +goal CCL.thy " [= <-> a [= a' & b [= b'"; +br (poXH RS iff_trans) 1; +by (SIMP_TAC ccl_ss 1); +by (fast_tac ccl_cs 1); +val po_pair = result(); + +goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))"; +br (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); +val po_lam = result(); + +val ccl_porews = [po_bot,po_pair,po_lam]; + +val [p1,p2,p3,p4,p5] = goal CCL.thy + "[| 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')"; +br (p1 RS po_cong RS po_trans) 1; +br (p2 RS po_cong RS po_trans) 1; +br (p3 RS po_cong RS po_trans) 1; +br (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); +br po_refl 1; +val case_pocong = result(); + +val [p1,p2] = goalw CCL.thy 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)); +val apply_pocong = result(); + + +val prems = goal CCL.thy "~ lam x.b(x) [= bot"; +br notI 1; +bd bot_poleast 1; +be (distinctness RS notE) 1; +val npo_lam_bot = result(); + +val eq1::eq2::prems = goal CCL.thy + "[| x=a; y=b; x[=y |] ==> a[=b"; +br (eq1 RS subst) 1; +br (eq2 RS subst) 1; +brs prems 1; +val po_lemma = result(); + +goal CCL.thy "~ [= lam x.f(x)"; +br notI 1; +br (npo_lam_bot RS notE) 1; +be (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1; +by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); +val npo_pair_lam = result(); + +goal CCL.thy "~ lam x.f(x) [= "; +br notI 1; +br (npo_lam_bot RS notE) 1; +be (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1; +by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); +val npo_lam_pair = result(); + +fun mk_thm s = prove_goal CCL.thy 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 CCL.thy "[| : R; R <= POgen(R) |] ==> t [= u"; +br (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1; +by (REPEAT (ares_tac prems 1)); +val po_coinduct = result(); + +fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i; + +(*************** EQUALITY *******************) + +goalw CCL.thy [EQgen_def,SIM_def] "mono(%X.EQgen(X))"; +br 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)); +val EQgen_mono = result(); + +goalw CCL.thy [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))"; +br (iff_refl RS XHlemma2) 1; +val EQgenXH = result(); + +goal CCL.thy + "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); +be rev_mp 1; +by (SIMP_TAC (CCL_ss addrews [EQ_iff RS iff_sym]) 1); +br (rewrite_rule [EQgen_def,SIM_def] + (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1; +br (iff_refl RS XHlemma2) 1; +val eqXH = result(); + +val prems = goal CCL.thy "[| : R; R <= EQgen(R) |] ==> t = u"; +br (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1; +by (REPEAT (ares_tac prems 1)); +val eq_coinduct = result(); + +val prems = goal CCL.thy + "[| : R; R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u"; +br (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1; +by (REPEAT (ares_tac (EQgen_mono::prems) 1)); +val eq_coinduct3 = result(); + +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 CCL.thy [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); +val cond_eta = result() RS mp; + +goal CCL.thy "(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); +val exhaustion = result(); + +val prems = goal CCL.thy + "[| 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])); +val term_case = result(); + +fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;