oheimb@2276: (* Title: HOLCF/domain/theorems.ML oheimb@2445: ID: $Id$ oheimb@2276: Author : David von Oheimb oheimb@2276: Copyright 1995, 1996 TU Muenchen oheimb@2445: oheimb@2445: proof generator for domain section regensbu@1274: *) regensbu@1274: oheimb@2446: regensbu@1274: structure Domain_Theorems = struct regensbu@1274: regensbu@1274: local regensbu@1274: regensbu@1274: open Domain_Library; regensbu@1274: infixr 0 ===>;infixr 0 ==>;infix 0 == ; regensbu@1274: infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; regensbu@1274: infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; regensbu@1274: oheimb@1637: (* ----- general proof facilities ------------------------------------------- *) regensbu@1274: oheimb@1637: fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true paulson@2033: ([pre_tm],propT)); regensbu@1274: regensbu@1274: fun pg'' thy defs t = let val sg = sign_of thy; paulson@2033: val ct = Thm.cterm_of sg (inferT sg t); paulson@2033: in prove_goalw_cterm defs ct end; regensbu@1274: fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf paulson@2033: | prems=> (cut_facts_tac prems 1)::tacsf); regensbu@1274: regensbu@1274: fun REPEAT_DETERM_UNTIL p tac = regensbu@1274: let fun drep st = if p st then Sequence.single st paulson@2033: else (case Sequence.pull(tac st) of paulson@2033: None => Sequence.null paulson@2033: | Some(st',_) => drep st') oheimb@1638: in drep end; regensbu@1274: val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1); regensbu@1274: oheimb@1674: local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in regensbu@1274: val kill_neq_tac = dtac trueI2 end; paulson@2033: fun case_UU_tac rews i v = case_tac (v^"=UU") i THEN paulson@2033: asm_simp_tac (HOLCF_ss addsimps rews) i; regensbu@1274: regensbu@1274: val chain_tac = REPEAT_DETERM o resolve_tac paulson@2033: [is_chain_iterate, ch2ch_fappR, ch2ch_fappL]; oheimb@1637: oheimb@1637: (* ----- general proofs ----------------------------------------------------- *) regensbu@1274: oheimb@1644: val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R" oheimb@1644: (fn prems =>[ paulson@2033: resolve_tac prems 1, paulson@2033: cut_facts_tac prems 1, paulson@2033: fast_tac HOL_cs 1]); regensbu@1274: slotosch@3323: val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [ oheimb@2445: rtac rev_contrapos 1, paulson@2033: etac (antisym_less_inverse RS conjunct1) 1, paulson@2033: resolve_tac prems 1]); regensbu@1274: regensbu@1274: in regensbu@1274: oheimb@4043: fun theorems (((dname,_),cons) : eq, eqs : eq list) thy = regensbu@1274: let regensbu@1274: oheimb@4030: val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ..."); regensbu@1274: val pg = pg' thy; oheimb@1637: (* oheimb@1637: infixr 0 y; oheimb@1637: val b = 0; oheimb@1637: fun _ y t = by t; oheimb@4030: fun g defs t = let val sg = sign_of thy; paulson@2033: val ct = Thm.cterm_of sg (inferT sg t); paulson@2033: in goalw_cterm defs ct end; oheimb@1637: *) regensbu@1274: oheimb@1637: oheimb@1637: (* ----- getting the axioms and definitions --------------------------------- *) regensbu@1274: oheimb@4043: local fun ga s dn = get_axiom thy (dn^"."^s) in oheimb@4043: val ax_abs_iso = ga "abs_iso" dname; oheimb@4043: val ax_rep_iso = ga "rep_iso" dname; oheimb@4043: val ax_when_def = ga "when_def" dname; oheimb@4043: val axs_con_def = map (fn (con,_) => ga (extern_name con^"_def") dname) cons; oheimb@4043: val axs_dis_def = map (fn (con,_) => ga ( dis_name con^"_def") dname) cons; regensbu@1274: val axs_sel_def = flat(map (fn (_,args) => oheimb@4043: map (fn arg => ga (sel_of arg ^"_def") dname) args) oheimb@4043: cons); oheimb@4043: val ax_copy_def = ga "copy_def" dname; regensbu@1274: end; (* local *) regensbu@1274: oheimb@1637: (* ----- theorems concerning the isomorphism -------------------------------- *) regensbu@1274: regensbu@1274: val dc_abs = %%(dname^"_abs"); regensbu@1274: val dc_rep = %%(dname^"_rep"); regensbu@1274: val dc_copy = %%(dname^"_copy"); regensbu@1274: val x_name = "x"; regensbu@1274: regensbu@1274: val (rep_strict, abs_strict) = let paulson@2033: val r = ax_rep_iso RS (ax_abs_iso RS (allI RSN(2,allI RS iso_strict))) paulson@2033: in (r RS conjunct1, r RS conjunct2) end; regensbu@1274: val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%x_name === UU)) [ paulson@2033: res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1, paulson@2033: etac ssubst 1, rtac rep_strict 1]; regensbu@1274: val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%x_name === UU)) [ paulson@2033: res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1, paulson@2033: etac ssubst 1, rtac abs_strict 1]; regensbu@1274: val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict]; regensbu@1274: regensbu@1274: local regensbu@1274: val iso_swap = pg [] (dc_rep`%"x" === %"y" ==> %"x" === dc_abs`%"y") [ paulson@2033: dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1, paulson@2033: etac (ax_rep_iso RS subst) 1]; regensbu@1274: fun exh foldr1 cn quant foldr2 var = let regensbu@1274: fun one_con (con,args) = let val vns = map vname args in regensbu@1274: foldr quant (vns, foldr2 ((%x_name === con_app2 con (var vns) vns):: paulson@2033: map (defined o (var vns)) (nonlazy args))) end regensbu@1274: in foldr1 ((cn(%x_name===UU))::map one_con cons) end; regensbu@1274: in oheimb@4043: val casedist = let paulson@2033: fun common_tac thm = rtac thm 1 THEN contr_tac 1; oheimb@2276: fun unit_tac true = common_tac upE1 paulson@2033: | unit_tac _ = all_tac; paulson@2033: fun prod_tac [] = common_tac oneE paulson@2033: | prod_tac [arg] = unit_tac (is_lazy arg) paulson@2033: | prod_tac (arg::args) = paulson@2033: common_tac sprodE THEN paulson@2033: kill_neq_tac 1 THEN paulson@2033: unit_tac (is_lazy arg) THEN paulson@2033: prod_tac args; paulson@2033: fun sum_rest_tac p = SELECT_GOAL(EVERY[ paulson@2033: rtac p 1, paulson@2033: rewrite_goals_tac axs_con_def, paulson@2033: dtac iso_swap 1, paulson@2033: simp_tac HOLCF_ss 1, paulson@2033: UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1; paulson@2033: fun sum_tac [(_,args)] [p] = paulson@2033: prod_tac args THEN sum_rest_tac p paulson@2033: | sum_tac ((_,args)::cons') (p::prems) = DETERM( paulson@2033: common_tac ssumE THEN paulson@2033: kill_neq_tac 1 THEN kill_neq_tac 2 THEN paulson@2033: prod_tac args THEN sum_rest_tac p) THEN paulson@2033: sum_tac cons' prems paulson@2033: | sum_tac _ _ = Imposs "theorems:sum_tac"; paulson@2033: in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P"))) paulson@2033: (fn T => T ==> %"P") mk_All paulson@2033: (fn l => foldr (op ===>) (map mk_trp l, paulson@2033: mk_trp(%"P"))) paulson@2033: bound_arg) paulson@2033: (fn prems => [ paulson@2033: cut_facts_tac [excluded_middle] 1, paulson@2033: etac disjE 1, paulson@2033: rtac (hd prems) 2, paulson@2033: etac rep_defin' 2, paulson@2033: if length cons = 1 andalso paulson@2033: length (snd(hd cons)) = 1 andalso paulson@2033: not(is_lazy(hd(snd(hd cons)))) paulson@2033: then rtac (hd (tl prems)) 1 THEN atac 2 THEN paulson@2033: rewrite_goals_tac axs_con_def THEN paulson@2033: simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1 paulson@2033: else sum_tac cons (tl prems)])end; oheimb@1637: val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[ oheimb@4043: rtac casedist 1, paulson@2033: UNTIL_SOLVED(fast_tac HOL_cs 1)]; regensbu@1274: end; regensbu@1274: regensbu@1274: local oheimb@1834: fun bind_fun t = foldr mk_All (when_funs cons,t); oheimb@1829: fun bound_fun i _ = Bound (length cons - i); oheimb@1829: val when_app = foldl (op `) (%%(dname^"_when"), mapn bound_fun 1 cons); oheimb@1829: val when_appl = pg [ax_when_def] (bind_fun(mk_trp(when_app`%x_name === paulson@2033: when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[ paulson@2033: simp_tac HOLCF_ss 1]; regensbu@1274: in oheimb@1829: val when_strict = pg [] (bind_fun(mk_trp(strict when_app))) [ paulson@2033: simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1]; oheimb@1829: val when_apps = let fun one_when n (con,args) = pg axs_con_def paulson@2033: (bind_fun (lift_defined % (nonlazy args, paulson@2033: mk_trp(when_app`(con_app con args) === oheimb@1829: mk_cfapp(bound_fun n 0,map %# args)))))[ paulson@2033: asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1]; paulson@2033: in mapn one_when 1 cons end; regensbu@1274: end; regensbu@1274: val when_rews = when_strict::when_apps; regensbu@1274: oheimb@1637: (* ----- theorems concerning the constructors, discriminators and selectors - *) regensbu@1274: oheimb@1637: val dis_rews = let oheimb@1637: val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp( paulson@2033: strict(%%(dis_name con)))) [ paulson@2033: simp_tac (HOLCF_ss addsimps when_rews) 1]) cons; oheimb@1637: val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def paulson@2033: (lift_defined % (nonlazy args, paulson@2033: (mk_trp((%%(dis_name c))`(con_app con args) === paulson@2033: %%(if con=c then "TT" else "FF"))))) [ paulson@2033: asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; paulson@2033: in flat(map (fn (c,_) => map (one_dis c) cons) cons) end; oheimb@1637: val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==> paulson@2033: defined(%%(dis_name con)`%x_name)) [ oheimb@4043: rtac casedist 1, paulson@2033: contr_tac 1, paulson@2033: UNTIL_SOLVED (CHANGED(asm_simp_tac paulson@2033: (HOLCF_ss addsimps dis_apps) 1))]) cons; oheimb@1637: in dis_stricts @ dis_defins @ dis_apps end; regensbu@1274: regensbu@1274: val con_stricts = flat(map (fn (con,args) => map (fn vn => paulson@2033: pg (axs_con_def) paulson@2033: (mk_trp(con_app2 con (fn arg => if vname arg = vn paulson@2033: then UU else %# arg) args === UU))[ paulson@2033: asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1] paulson@2033: ) (nonlazy args)) cons); regensbu@1274: val con_defins = map (fn (con,args) => pg [] paulson@2033: (lift_defined % (nonlazy args, paulson@2033: mk_trp(defined(con_app con args)))) ([ oheimb@2445: rtac rev_contrapos 1, paulson@2033: eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1, paulson@2033: asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons; regensbu@1274: val con_rews = con_stricts @ con_defins; regensbu@1274: regensbu@1274: val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%sel))) [ paulson@2033: simp_tac (HOLCF_ss addsimps when_rews) 1]; oheimb@1637: in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end; regensbu@1274: val sel_apps = let fun one_sel c n sel = map (fn (con,args) => paulson@2033: let val nlas = nonlazy args; paulson@2033: val vns = map vname args; paulson@2033: in pg axs_sel_def (lift_defined % paulson@2033: (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas, paulson@2033: mk_trp((%%sel)`(con_app con args) === paulson@2033: (if con=c then %(nth_elem(n,vns)) else UU)))) paulson@2033: ( (if con=c then [] paulson@2033: else map(case_UU_tac(when_rews@con_stricts)1) nlas) paulson@2033: @(if con=c andalso ((nth_elem(n,vns)) mem nlas) paulson@2033: then[case_UU_tac (when_rews @ con_stricts) 1 paulson@2033: (nth_elem(n,vns))] else []) paulson@2033: @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons; regensbu@1274: in flat(map (fn (c,args) => oheimb@1637: flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end; oheimb@1637: val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==> paulson@2033: defined(%%(sel_of arg)`%x_name)) [ oheimb@4043: rtac casedist 1, paulson@2033: contr_tac 1, paulson@2033: UNTIL_SOLVED (CHANGED(asm_simp_tac paulson@2033: (HOLCF_ss addsimps sel_apps) 1))]) paulson@2033: (filter_out is_lazy (snd(hd cons))) else []; regensbu@1274: val sel_rews = sel_stricts @ sel_defins @ sel_apps; regensbu@1274: regensbu@1274: val distincts_le = let regensbu@1274: fun dist (con1, args1) (con2, args2) = pg [] paulson@2033: (lift_defined % ((nonlazy args1), paulson@2033: (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([ oheimb@2445: rtac rev_contrapos 1, paulson@2033: eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1] paulson@2033: @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2) paulson@2033: @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]); regensbu@1274: fun distinct (con1,args1) (con2,args2) = paulson@2267: let val arg1 = (con1, args1) paulson@2267: val arg2 = (con2, paulson@2267: ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) paulson@2267: (args2, variantlist(map vname args2,map vname args1))) paulson@2033: in [dist arg1 arg2, dist arg2 arg1] end; regensbu@1274: fun distincts [] = [] regensbu@1274: | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; regensbu@1274: in distincts cons end; oheimb@4043: val dist_les = flat (flat distincts_le); oheimb@4043: val dist_eqs = let regensbu@1274: fun distinct (_,args1) ((_,args2),leqs) = let paulson@2033: val (le1,le2) = (hd leqs, hd(tl leqs)); paulson@2033: val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in paulson@2033: if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else paulson@2033: if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else paulson@2033: [eq1, eq2] end; paulson@4062: open Basis_Library (*restore original List*) regensbu@1274: fun distincts [] = [] paulson@4062: | distincts ((c,leqs)::cs) = List.concat paulson@2267: (ListPair.map (distinct c) ((map #1 cs),leqs)) @ paulson@2267: distincts cs; regensbu@1274: in distincts (cons~~distincts_le) end; regensbu@1274: regensbu@1274: local regensbu@1274: fun pgterm rel con args = let paulson@2033: fun append s = upd_vname(fn v => v^s); paulson@2033: val (largs,rargs) = (args, map (append "'") args); paulson@2033: in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===> paulson@2033: lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs), paulson@2033: mk_trp (foldr' mk_conj paulson@2267: (ListPair.map rel paulson@2267: (map %# largs, map %# rargs)))))) end; regensbu@1274: val cons' = filter (fn (_,args) => args<>[]) cons; regensbu@1274: in regensbu@1274: val inverts = map (fn (con,args) => paulson@2033: pgterm (op <<) con args (flat(map (fn arg => [ paulson@2033: TRY(rtac conjI 1), paulson@2033: dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1, paulson@2033: asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1] paulson@2033: ) args))) cons'; regensbu@1274: val injects = map (fn ((con,args),inv_thm) => paulson@2033: pgterm (op ===) con args [ paulson@2033: etac (antisym_less_inverse RS conjE) 1, paulson@2033: dtac inv_thm 1, REPEAT(atac 1), paulson@2033: dtac inv_thm 1, REPEAT(atac 1), paulson@2033: TRY(safe_tac HOL_cs), paulson@2033: REPEAT(rtac antisym_less 1 ORELSE atac 1)] ) paulson@2033: (cons'~~inverts); regensbu@1274: end; regensbu@1274: oheimb@1637: (* ----- theorems concerning one induction step ----------------------------- *) regensbu@1274: oheimb@1637: val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [ paulson@2033: asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict, paulson@2033: cfst_strict,csnd_strict]) 1]; oheimb@1637: val copy_apps = map (fn (con,args) => pg [ax_copy_def] paulson@2033: (lift_defined % (nonlazy_rec args, paulson@2033: mk_trp(dc_copy`%"f"`(con_app con args) === paulson@2033: (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args)))) paulson@2033: (map (case_UU_tac (abs_strict::when_strict::con_stricts) paulson@2033: 1 o vname) paulson@2033: (filter (fn a => not (is_rec a orelse is_lazy a)) args) paulson@2033: @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1, paulson@2033: simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons; oheimb@1637: val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU` paulson@2033: (con_app con args) ===UU)) oheimb@1637: (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews paulson@2033: in map (case_UU_tac rews 1) (nonlazy args) @ [ paulson@2033: asm_simp_tac (HOLCF_ss addsimps rews) 1] end)) paulson@2033: (filter (fn (_,args)=>exists is_nonlazy_rec args) cons); regensbu@1274: val copy_rews = copy_strict::copy_apps @ copy_stricts; oheimb@4043: in thy |> Theory.add_path (Sign.base_name dname) oheimb@4043: |> PureThy.store_thmss [ oheimb@4043: ("iso_rews" , iso_rews ), oheimb@4043: ("exhaust" , [exhaust] ), oheimb@4043: ("casedist" , [casedist]), oheimb@4043: ("when_rews", when_rews ), oheimb@4043: ("con_rews", con_rews), oheimb@4043: ("sel_rews", sel_rews), oheimb@4043: ("dis_rews", dis_rews), oheimb@4043: ("dist_les", dist_les), oheimb@4043: ("dist_eqs", dist_eqs), oheimb@4043: ("inverts" , inverts ), oheimb@4043: ("injects" , injects ), oheimb@4043: ("copy_rews", copy_rews)] oheimb@4043: |> Theory.add_path ".." regensbu@1274: end; (* let *) regensbu@1274: oheimb@4043: fun comp_theorems (comp_dnam, eqs: eq list) thy = regensbu@1274: let oheimb@4008: val dnames = map (fst o fst) eqs; oheimb@4008: val conss = map snd eqs; oheimb@4008: val comp_dname = Sign.full_name (sign_of thy) comp_dnam; oheimb@4008: oheimb@4030: val d = writeln("Proving induction properties of domain "^comp_dname^" ..."); regensbu@1274: val pg = pg' thy; regensbu@1274: oheimb@1637: (* ----- getting the composite axiom and definitions ------------------------ *) regensbu@1274: oheimb@4043: local fun ga s dn = get_axiom thy (dn^"."^s) in oheimb@4043: val axs_reach = map (ga "reach" ) dnames; oheimb@4043: val axs_take_def = map (ga "take_def" ) dnames; oheimb@4043: val axs_finite_def = map (ga "finite_def") dnames; oheimb@4043: val ax_copy2_def = ga "copy_def" comp_dnam; oheimb@4043: val ax_bisim_def = ga "bisim_def" comp_dnam; oheimb@4043: end; (* local *) oheimb@4043: oheimb@4043: local fun gt s dn = get_thm thy (dn^"."^s); oheimb@4043: fun gts s dn = get_thms thy (dn^"."^s) in oheimb@4043: val cases = map (gt "casedist" ) dnames; oheimb@4043: val con_rews = flat (map (gts "con_rews" ) dnames); oheimb@4043: val copy_rews = flat (map (gts "copy_rews") dnames); regensbu@1274: end; (* local *) regensbu@1274: regensbu@1274: fun dc_take dn = %%(dn^"_take"); regensbu@1274: val x_name = idx_name dnames "x"; regensbu@1274: val P_name = idx_name dnames "P"; oheimb@1637: val n_eqs = length eqs; oheimb@1637: oheimb@1637: (* ----- theorems concerning finite approximation and finite induction ------ *) regensbu@1274: regensbu@1274: local oheimb@1637: val iterate_Cprod_ss = simpset_of "Fix" paulson@2033: addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews; regensbu@1274: val copy_con_rews = copy_rews @ con_rews; oheimb@1637: val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; oheimb@1637: val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=> oheimb@4030: strict(dc_take dn $ %"n")) eqs))) ([ paulson@2033: nat_ind_tac "n" 1, oheimb@4030: simp_tac iterate_Cprod_ss 1, paulson@2033: asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]); regensbu@1274: val take_stricts' = rewrite_rule copy_take_defs take_stricts; oheimb@1637: val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0") paulson@2033: `%x_name n === UU))[ paulson@2033: simp_tac iterate_Cprod_ss 1]) 1 dnames; oheimb@1637: val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1; regensbu@1274: val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj paulson@2033: (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all paulson@2033: (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) === paulson@2033: con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n")) paulson@2033: args)) cons) eqs)))) ([ paulson@2033: simp_tac iterate_Cprod_ss 1, paulson@2033: nat_ind_tac "n" 1, paulson@2033: simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1, paulson@2033: asm_full_simp_tac (HOLCF_ss addsimps paulson@2033: (filter (has_fewer_prems 1) copy_rews)) 1, paulson@2033: TRY(safe_tac HOL_cs)] @ paulson@2033: (flat(map (fn ((dn,_),cons) => map (fn (con,args) => paulson@2033: if nonlazy_rec args = [] then all_tac else paulson@2033: EVERY(map c_UU_tac (nonlazy_rec args)) THEN paulson@2033: asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1 paulson@2033: ) cons) eqs))); regensbu@1274: in regensbu@1274: val take_rews = atomize take_stricts @ take_0s @ atomize take_apps; regensbu@1274: end; (* local *) regensbu@1274: regensbu@1274: local regensbu@1274: fun one_con p (con,args) = foldr mk_All (map vname args, paulson@2033: lift_defined (bound_arg (map vname args)) (nonlazy args, paulson@2033: lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg) oheimb@1637: (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args)))); regensbu@1274: fun one_eq ((p,cons),concl) = (mk_trp(%p $ UU) ===> paulson@2033: foldr (op ===>) (map (one_con p) cons,concl)); oheimb@1637: fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss, paulson@2033: mk_trp(foldr' mk_conj (mapn concf 1 dnames))); regensbu@1274: val take_ss = HOL_ss addsimps take_rews; oheimb@1637: fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i) paulson@2033: 1 dnames); oheimb@1637: fun ind_prems_tac prems = EVERY(flat (map (fn cons => ( paulson@2033: resolve_tac prems 1 :: paulson@2033: flat (map (fn (_,args) => paulson@2033: resolve_tac prems 1 :: paulson@2033: map (K(atac 1)) (nonlazy args) @ paulson@2033: map (K(atac 1)) (filter is_rec args)) paulson@2033: cons))) conss)); regensbu@1274: local oheimb@1637: (* check whether every/exists constructor of the n-th part of the equation: oheimb@1637: it has a possibly indirectly recursive argument that isn't/is possibly oheimb@1637: indirectly lazy *) oheimb@1637: fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => paulson@2033: is_rec arg andalso not(rec_of arg mem ns) andalso paulson@2033: ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse paulson@2033: rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) paulson@2033: (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss)))) paulson@2033: ) o snd) cons; oheimb@1637: fun all_rec_to ns = rec_to forall not all_rec_to ns; oheimb@4030: fun warn (n,cons) = if all_rec_to [] false (n,cons) then (warning oheimb@4030: ("domain "^nth_elem(n,dnames)^" is empty!"); true) else false; oheimb@1637: fun lazy_rec_to ns = rec_to exists Id lazy_rec_to ns; oheimb@1637: oheimb@1637: in val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; oheimb@1637: val is_emptys = map warn n__eqs; oheimb@1637: val is_finite = forall (not o lazy_rec_to [] false) n__eqs; regensbu@1274: end; oheimb@1637: in (* local *) oheimb@1637: val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$ paulson@2033: (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [ paulson@2033: quant_tac 1, oheimb@2445: simp_tac HOL_ss 1, paulson@2033: nat_ind_tac "n" 1, paulson@2033: simp_tac (take_ss addsimps prems) 1, paulson@2033: TRY(safe_tac HOL_cs)] paulson@2033: @ flat(map (fn (cons,cases) => [ paulson@2033: res_inst_tac [("x","x")] cases 1, paulson@2033: asm_simp_tac (take_ss addsimps prems) 1] paulson@2033: @ flat(map (fn (con,args) => paulson@2033: asm_simp_tac take_ss 1 :: paulson@2033: map (fn arg => paulson@2033: case_UU_tac (prems@con_rews) 1 ( nipkow@3044: nth_elem(rec_of arg,dnames)^"_take n`"^vname arg)) paulson@2033: (filter is_nonlazy_rec args) @ [ paulson@2033: resolve_tac prems 1] @ paulson@2033: map (K (atac 1)) (nonlazy args) @ paulson@2033: map (K (etac spec 1)) (filter is_rec args)) paulson@2033: cons)) oheimb@4043: (conss~~cases))); oheimb@1637: oheimb@1637: val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n", paulson@2033: mk_trp(dc_take dn $ Bound 0 `%(x_name n) === paulson@2033: dc_take dn $ Bound 0 `%(x_name n^"'"))) paulson@2033: ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [ paulson@2033: res_inst_tac[("t",x_name n )](ax_reach RS subst) 1, paulson@2033: res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1, paulson@2033: stac fix_def2 1, paulson@2033: REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1 paulson@2033: THEN chain_tac 1)), paulson@2033: stac contlub_cfun_fun 1, paulson@2033: stac contlub_cfun_fun 2, paulson@2033: rtac lub_equal 3, paulson@2033: chain_tac 1, paulson@2033: rtac allI 1, paulson@2033: resolve_tac prems 1])) 1 (dnames~~axs_reach); oheimb@1637: oheimb@1637: (* ----- theorems concerning finiteness and induction ----------------------- *) regensbu@1274: regensbu@1274: val (finites,ind) = if is_finite then oheimb@1637: let oheimb@1637: fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x"); oheimb@1637: val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> paulson@2033: mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU), paulson@2033: take_enough dn)) ===> mk_trp(take_enough dn)) [ paulson@2033: etac disjE 1, paulson@2033: etac notE 1, paulson@2033: resolve_tac take_lemmas 1, paulson@2033: asm_simp_tac take_ss 1, paulson@2033: atac 1]) dnames; oheimb@1637: val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn paulson@2033: (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args), paulson@2033: mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU, paulson@2033: dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([ paulson@2033: rtac allI 1, paulson@2033: nat_ind_tac "n" 1, paulson@2033: simp_tac take_ss 1, paulson@2033: TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @ paulson@2033: flat(mapn (fn n => fn (cons,cases) => [ paulson@2033: simp_tac take_ss 1, paulson@2033: rtac allI 1, paulson@2033: res_inst_tac [("x",x_name n)] cases 1, paulson@2033: asm_simp_tac take_ss 1] @ paulson@2033: flat(map (fn (con,args) => paulson@2033: asm_simp_tac take_ss 1 :: paulson@2033: flat(map (fn vn => [ paulson@2033: eres_inst_tac [("x",vn)] all_dupE 1, paulson@2033: etac disjE 1, paulson@2033: asm_simp_tac (HOL_ss addsimps con_rews) 1, paulson@2033: asm_simp_tac take_ss 1]) paulson@2033: (nonlazy_rec args))) paulson@2033: cons)) oheimb@4043: 1 (conss~~cases))); oheimb@1637: val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp( paulson@2033: %%(dn^"_finite") $ %"x"))[ paulson@2033: case_UU_tac take_rews 1 "x", paulson@2033: eresolve_tac finite_lemmas1a 1, paulson@2033: step_tac HOL_cs 1, paulson@2033: step_tac HOL_cs 1, paulson@2033: cut_facts_tac [l1b] 1, paulson@2033: fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b); oheimb@1637: in oheimb@1637: (finites, oheimb@1637: pg'' thy[](ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))(fn prems => paulson@2033: TRY(safe_tac HOL_cs) :: paulson@2033: flat (map (fn (finite,fin_ind) => [ paulson@2033: rtac(rewrite_rule axs_finite_def finite RS exE)1, paulson@2033: etac subst 1, paulson@2033: rtac fin_ind 1, paulson@2033: ind_prems_tac prems]) paulson@2033: (finites~~(atomize finite_ind)) )) regensbu@1274: ) end (* let *) else oheimb@1637: (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) paulson@2033: [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames, oheimb@1637: pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%"adm" $ %(P_name n)))) paulson@2033: 1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))) paulson@2033: (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) paulson@2033: axs_reach @ [ paulson@2033: quant_tac 1, paulson@2033: rtac (adm_impl_admw RS wfix_ind) 1, oheimb@4030: REPEAT_DETERM(rtac adm_all2 1), oheimb@4030: REPEAT_DETERM(TRY(rtac adm_conj 1) THEN oheimb@4030: rtac adm_subst 1 THEN paulson@2033: cont_tacR 1 THEN resolve_tac prems 1), paulson@2033: strip_tac 1, paulson@2033: rtac (rewrite_rule axs_take_def finite_ind) 1, paulson@2033: ind_prems_tac prems]) regensbu@1274: ) regensbu@1274: end; (* local *) regensbu@1274: oheimb@1637: (* ----- theorem concerning coinduction ------------------------------------- *) oheimb@1637: regensbu@1274: local regensbu@1274: val xs = mapn (fn n => K (x_name n)) 1 dnames; oheimb@1637: fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); regensbu@1274: val take_ss = HOL_ss addsimps take_rews; oheimb@1637: val sproj = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")"); oheimb@1637: val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R", paulson@2033: foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs, paulson@2033: foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ paulson@2033: bnd_arg n 0 $ bnd_arg n 1)) 0 dnames, paulson@2033: foldr' mk_conj (mapn (fn n => fn dn => paulson@2033: (dc_take dn $ %"n" `bnd_arg n 0 === paulson@2033: (dc_take dn $ %"n" `bnd_arg n 1)))0 dnames)))))) paulson@2033: ([ rtac impI 1, paulson@2033: nat_ind_tac "n" 1, paulson@2033: simp_tac take_ss 1, paulson@2033: safe_tac HOL_cs] @ paulson@2033: flat(mapn (fn n => fn x => [ paulson@2033: rotate_tac (n+1) 1, paulson@2033: etac all2E 1, paulson@2033: eres_inst_tac [("P1", sproj "R" n_eqs n^ paulson@2033: " "^x^" "^x^"'")](mp RS disjE) 1, paulson@2033: TRY(safe_tac HOL_cs), paulson@2033: REPEAT(CHANGED(asm_simp_tac take_ss 1))]) paulson@2033: 0 xs)); regensbu@1274: in regensbu@1274: val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===> paulson@2033: foldr (op ===>) (mapn (fn n => fn x => paulson@2033: mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs, paulson@2033: mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([ paulson@2033: TRY(safe_tac HOL_cs)] @ paulson@2033: flat(map (fn take_lemma => [ paulson@2033: rtac take_lemma 1, paulson@2033: cut_facts_tac [coind_lemma] 1, paulson@2033: fast_tac HOL_cs 1]) paulson@2033: take_lemmas)); regensbu@1274: end; (* local *) regensbu@1274: regensbu@1274: oheimb@4043: in thy |> Theory.add_path comp_dnam oheimb@4043: |> PureThy.store_thmss [ oheimb@4043: ("take_rews" , take_rews ), oheimb@4043: ("take_lemmas", take_lemmas), oheimb@4043: ("finites" , finites ), oheimb@4043: ("finite_ind", [finite_ind]), oheimb@4043: ("ind" , [ind ]), oheimb@4043: ("coind" , [coind ])] oheimb@4043: |> Theory.add_path ".." regensbu@1274: end; (* let *) regensbu@1274: end; (* local *) regensbu@1274: end; (* struct *)