# HG changeset patch # User huffman # Date 1117837473 -7200 # Node ID 57094b83774e146802a1fe2b0f329efe1d3ca779 # Parent 84a177eeb49c717fc932b355ba9e1c05404b66ec Domain package generates match functions for new datatypes, for use with the fixrec package diff -r 84a177eeb49c -r 57094b83774e src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Sat Jun 04 00:23:40 2005 +0200 +++ b/src/HOLCF/domain/axioms.ML Sat Jun 04 00:24:33 2005 +0200 @@ -61,6 +61,13 @@ (if con'=con then %%:"TT" else %%:"FF") args)) cons)) in map ddef cons end; + val mat_defs = let + fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == + mk_cRep_CFun(%%:(dname^"_when"),map + (fn (con',args) => (foldr /\# + (if con'=con then (%%:"return")`(mk_ctuple (map (bound_arg args) args)) else %%:"fail") args)) cons)) + in map mdef cons end; + val sel_defs = let fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) == mk_cRep_CFun(%%:(dname^"_when"),map @@ -81,7 +88,7 @@ in (dnam, [abs_iso_ax, rep_iso_ax, reach_ax], [when_def, copy_def] @ - con_defs @ dis_defs @ sel_defs @ + con_defs @ dis_defs @ mat_defs @ sel_defs @ [take_def, finite_def]) end; (* let *) diff -r 84a177eeb49c -r 57094b83774e src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Sat Jun 04 00:23:40 2005 +0200 +++ b/src/HOLCF/domain/library.ML Sat Jun 04 00:24:33 2005 +0200 @@ -56,6 +56,8 @@ | _ => con; fun dis_name con = "is_"^ (extern_name con); fun dis_name_ con = "is_"^ (strip_esc con); +fun mat_name con = "match_"^ (extern_name con); +fun mat_name_ con = "match_"^ (strip_esc con); (* make distinct names out of the type list, forbidding "o","n..","x..","f..","P.." as names *) @@ -174,6 +176,12 @@ fun strict f = f`UU === UU; fun defined t = t ~= UU; fun cpair (S,T) = %%:"cpair"`S`T; +fun mk_ctuple [] = %%:"UU" (* used in match_defs *) +| mk_ctuple (t::[]) = t +| mk_ctuple (t::ts) = cpair (t, mk_ctuple ts); +fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) +| mk_ctupleT (T::[]) = T +| mk_ctupleT (T::Ts) = mk_prodT(T, mk_ctupleT Ts); fun lift_defined f = lift (fn x => defined (f x)); fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); diff -r 84a177eeb49c -r 57094b83774e src/HOLCF/domain/syntax.ML --- a/src/HOLCF/domain/syntax.ML Sat Jun 04 00:23:40 2005 +0200 +++ b/src/HOLCF/domain/syntax.ML Sat Jun 04 00:24:33 2005 +0200 @@ -47,10 +47,13 @@ (* stricly speaking, these constants have one argument, but the mixfix (without arguments) is introduced only to generate parse rules for non-alphanumeric names*) + fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))), + Mixfix(escape ("match_" ^ con), [], Syntax.max_pri)); fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args; in val consts_con = map con cons'; val consts_dis = map dis cons'; + val consts_mat = map mat cons'; val consts_sel = List.concat(map sel cons'); end; @@ -87,7 +90,7 @@ end; in ([const_rep, const_abs, const_when, const_copy] @ - consts_con @ consts_dis @ consts_sel @ + consts_con @ consts_dis @ consts_mat @ consts_sel @ [const_take, const_finite], [case_trans]) end; (* let *) diff -r 84a177eeb49c -r 57094b83774e src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Sat Jun 04 00:23:40 2005 +0200 +++ b/src/HOLCF/domain/theorems.ML Sat Jun 04 00:24:33 2005 +0200 @@ -69,6 +69,7 @@ val ax_when_def = ga "when_def" dname; val axs_con_def = map (fn (con,_) => ga (extern_name con^"_def") dname) cons; val axs_dis_def = map (fn (con,_) => ga ( dis_name con^"_def") dname) cons; +val axs_mat_def = map (fn (con,_) => ga ( mat_name con^"_def") dname) cons; val axs_sel_def = List.concat(map (fn (_,args) => map (fn arg => ga (sel_of arg ^"_def") dname) args) cons); @@ -83,8 +84,8 @@ val x_name = "x"; val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso]; -val abs_strict = iso_locale RS iso_abs_strict; -val rep_strict = iso_locale RS iso_rep_strict; +val abs_strict = ax_rep_iso RS (allI RS retraction_strict); +val rep_strict = ax_abs_iso RS (allI RS retraction_strict); val abs_defin' = iso_locale RS iso_abs_defin'; val rep_defin' = iso_locale RS iso_rep_defin'; val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict]; @@ -217,6 +218,18 @@ (HOLCF_ss addsimps dis_apps) 1))]) cons; in dis_stricts @ dis_defins @ dis_apps end; +val mat_rews = let + val mat_stricts = map (fn (con,_) => pg axs_mat_def (mk_trp( + strict(%%:(mat_name con)))) [ + rtac when_strict 1]) cons; + val mat_apps = let fun one_mat c (con,args)= pg axs_mat_def + (lift_defined %: (nonlazy args, + (mk_trp((%%:(mat_name c))`(con_app con args) === + (if con=c then (%%:"return")`(mk_ctuple (map %# args)) else %%:"fail"))))) [ + asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in List.concat(map (fn (c,_) => map (one_mat c) cons) cons) end; +in mat_stricts @ mat_apps end; + val con_stricts = List.concat(map (fn (con,args) => map (fn vn => pg con_appls (mk_trp(con_app2 con (fn arg => if vname arg = vn @@ -263,7 +276,7 @@ (lift_defined %: ((nonlazy args1), (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([ rtac rev_contrapos 1, - eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1] + eres_inst_tac[("f",dis_name con1)] monofun_cfun_arg 1] @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2) @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]); fun distinct (con1,args1) (con2,args2) = @@ -304,7 +317,7 @@ val inverts = map (fn (con,args) => pgterm (op <<) con args (List.concat(map (fn arg => [ TRY(rtac conjI 1), - dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1, + dres_inst_tac [("f",sel_of arg)] monofun_cfun_arg 1, asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1] ) args))) cons'; val injects = map (fn ((con,args),inv_thm) => @@ -320,8 +333,7 @@ (* ----- theorems concerning one induction step ----------------------------- *) val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [ - asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict, - cfst_strict,csnd_strict]) 1]; + asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict]) 1]; val copy_apps = map (fn (con,args) => pg [ax_copy_def] (lift_defined %: (nonlazy_rec args, mk_trp(dc_copy`%"f"`(con_app con args) === @@ -333,7 +345,7 @@ simp_tac (HOLCF_ss addsimps con_appls) 1]))cons; val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU` (con_app con args) ===UU)) - (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews + (let val rews = copy_strict::copy_apps@con_rews in map (case_UU_tac rews 1) (nonlazy args) @ [ asm_simp_tac (HOLCF_ss addsimps rews) 1] end)) (List.filter (fn (_,args)=>exists is_nonlazy_rec args) cons); @@ -347,6 +359,7 @@ ("con_rews", con_rews), ("sel_rews", sel_rews), ("dis_rews", dis_rews), + ("match_rews", mat_rews), ("dist_les", dist_les), ("dist_eqs", dist_eqs), ("inverts" , inverts ), @@ -390,8 +403,7 @@ (* ----- theorems concerning finite approximation and finite induction ------ *) local - val iterate_Cprod_ss = simpset_of Fix.thy - addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews; + val iterate_Cprod_ss = simpset_of Fix.thy; val copy_con_rews = copy_rews @ con_rews; val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>