src/HOLCF/Tools/domain/domain_theorems.ML
author huffman
Tue Jan 29 18:00:12 2008 +0100 (2008-01-29)
changeset 26012 f6917792f8a4
parent 25895 0eaadfa8889e
child 26336 a0e2b706ce73
permissions -rw-r--r--
new term-building combinators
     1 (*  Title:      HOLCF/Tools/domain/domain_theorems.ML
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4                 New proofs/tactics by Brian Huffman
     5 
     6 Proof generator for domain command.
     7 *)
     8 
     9 val HOLCF_ss = simpset();
    10 
    11 structure Domain_Theorems = struct
    12 
    13 local
    14 
    15 val adm_impl_admw = @{thm adm_impl_admw};
    16 val adm_all = @{thm adm_all};
    17 val adm_conj = @{thm adm_conj};
    18 val adm_subst = @{thm adm_subst};
    19 val antisym_less_inverse = @{thm antisym_less_inverse};
    20 val beta_cfun = @{thm beta_cfun};
    21 val cfun_arg_cong = @{thm cfun_arg_cong};
    22 val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
    23 val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
    24 val chain_iterate = @{thm chain_iterate};
    25 val compact_ONE = @{thm compact_ONE};
    26 val compact_sinl = @{thm compact_sinl};
    27 val compact_sinr = @{thm compact_sinr};
    28 val compact_spair = @{thm compact_spair};
    29 val compact_up = @{thm compact_up};
    30 val contlub_cfun_arg = @{thm contlub_cfun_arg};
    31 val contlub_cfun_fun = @{thm contlub_cfun_fun};
    32 val fix_def2 = @{thm fix_def2};
    33 val injection_eq = @{thm injection_eq};
    34 val injection_less = @{thm injection_less};
    35 val lub_equal = @{thm lub_equal};
    36 val monofun_cfun_arg = @{thm monofun_cfun_arg};
    37 val retraction_strict = @{thm retraction_strict};
    38 val spair_eq = @{thm spair_eq};
    39 val spair_less = @{thm spair_less};
    40 val sscase1 = @{thm sscase1};
    41 val ssplit1 = @{thm ssplit1};
    42 val strictify1 = @{thm strictify1};
    43 val wfix_ind = @{thm wfix_ind};
    44 
    45 val iso_intro       = @{thm iso.intro};
    46 val iso_abs_iso     = @{thm iso.abs_iso};
    47 val iso_rep_iso     = @{thm iso.rep_iso};
    48 val iso_abs_strict  = @{thm iso.abs_strict};
    49 val iso_rep_strict  = @{thm iso.rep_strict};
    50 val iso_abs_defin'  = @{thm iso.abs_defin'};
    51 val iso_rep_defin'  = @{thm iso.rep_defin'};
    52 val iso_abs_defined = @{thm iso.abs_defined};
    53 val iso_rep_defined = @{thm iso.rep_defined};
    54 val iso_compact_abs = @{thm iso.compact_abs};
    55 val iso_compact_rep = @{thm iso.compact_rep};
    56 val iso_iso_swap    = @{thm iso.iso_swap};
    57 
    58 val exh_start = @{thm exh_start};
    59 val ex_defined_iffs = @{thms ex_defined_iffs};
    60 val exh_casedist0 = @{thm exh_casedist0};
    61 val exh_casedists = @{thms exh_casedists};
    62 
    63 open Domain_Library;
    64 infixr 0 ===>;
    65 infixr 0 ==>;
    66 infix 0 == ; 
    67 infix 1 ===;
    68 infix 1 ~= ;
    69 infix 1 <<;
    70 infix 1 ~<<;
    71 infix 9 `   ;
    72 infix 9 `% ;
    73 infix 9 `%%;
    74 infixr 9 oo;
    75 
    76 (* ----- general proof facilities ------------------------------------------- *)
    77 
    78 fun legacy_infer_term thy t =
    79   let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
    80   in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end;
    81 
    82 fun pg'' thy defs t tacs =
    83   let
    84     val t' = legacy_infer_term thy t;
    85     val asms = Logic.strip_imp_prems t';
    86     val prop = Logic.strip_imp_concl t';
    87     fun tac prems =
    88       rewrite_goals_tac defs THEN
    89       EVERY (tacs (map (rewrite_rule defs) prems));
    90   in Goal.prove_global thy [] asms prop tac end;
    91 
    92 fun pg' thy defs t tacsf =
    93   let
    94     fun tacs [] = tacsf
    95       | tacs prems = cut_facts_tac prems 1 :: tacsf;
    96   in pg'' thy defs t tacs end;
    97 
    98 fun case_UU_tac rews i v =
    99   case_tac (v^"=UU") i THEN
   100   asm_simp_tac (HOLCF_ss addsimps rews) i;
   101 
   102 val chain_tac =
   103   REPEAT_DETERM o resolve_tac 
   104     [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
   105 
   106 (* ----- general proofs ----------------------------------------------------- *)
   107 
   108 val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
   109   (fn prems =>[
   110     resolve_tac prems 1,
   111     cut_facts_tac prems 1,
   112     fast_tac HOL_cs 1]);
   113 
   114 val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
   115   (fn prems =>
   116     [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
   117 
   118 in
   119 
   120 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
   121 let
   122 
   123 val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
   124 val pg = pg' thy;
   125 
   126 (* ----- getting the axioms and definitions --------------------------------- *)
   127 
   128 local
   129   fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
   130 in
   131   val ax_abs_iso  = ga "abs_iso"  dname;
   132   val ax_rep_iso  = ga "rep_iso"  dname;
   133   val ax_when_def = ga "when_def" dname;
   134   fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;
   135   val axs_con_def = map (get_def extern_name) cons;
   136   val axs_dis_def = map (get_def dis_name) cons;
   137   val axs_mat_def = map (get_def mat_name) cons;
   138   val axs_pat_def = map (get_def pat_name) cons;
   139   val axs_sel_def =
   140     let
   141       fun def_of_sel sel = ga (sel^"_def") dname;
   142       fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
   143       fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
   144     in
   145       List.concat (map defs_of_con cons)
   146     end;
   147   val ax_copy_def = ga "copy_def" dname;
   148 end; (* local *)
   149 
   150 (* ----- theorems concerning the isomorphism -------------------------------- *)
   151 
   152 val dc_abs  = %%:(dname^"_abs");
   153 val dc_rep  = %%:(dname^"_rep");
   154 val dc_copy = %%:(dname^"_copy");
   155 val x_name = "x";
   156 
   157 val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
   158 val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
   159 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
   160 val abs_defin' = iso_locale RS iso_abs_defin';
   161 val rep_defin' = iso_locale RS iso_rep_defin';
   162 val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
   163 
   164 (* ----- generating beta reduction rules from definitions-------------------- *)
   165 
   166 local
   167   fun arglist (Const _ $ Abs (s, _, t)) =
   168     let
   169       val (vars,body) = arglist t;
   170     in (s :: vars, body) end
   171     | arglist t = ([], t);
   172   fun bind_fun vars t = Library.foldr mk_All (vars, t);
   173   fun bound_vars 0 = []
   174     | bound_vars i = Bound (i-1) :: bound_vars (i - 1);
   175 in
   176   fun appl_of_def def =
   177     let
   178       val (_ $ con $ lam) = concl_of def;
   179       val (vars, rhs) = arglist lam;
   180       val lhs = list_ccomb (con, bound_vars (length vars));
   181       val appl = bind_fun vars (lhs == rhs);
   182       val cs = ContProc.cont_thms lam;
   183       val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
   184     in pg (def::betas) appl [rtac reflexive_thm 1] end;
   185 end;
   186 
   187 val when_appl = appl_of_def ax_when_def;
   188 val con_appls = map appl_of_def axs_con_def;
   189 
   190 local
   191   fun arg2typ n arg =
   192     let val t = TVar (("'a", n), pcpoS)
   193     in (n + 1, if is_lazy arg then mk_uT t else t) end;
   194 
   195   fun args2typ n [] = (n, oneT)
   196     | args2typ n [arg] = arg2typ n arg
   197     | args2typ n (arg::args) =
   198     let
   199       val (n1, t1) = arg2typ n arg;
   200       val (n2, t2) = args2typ n1 args
   201     in (n2, mk_sprodT (t1, t2)) end;
   202 
   203   fun cons2typ n [] = (n,oneT)
   204     | cons2typ n [con] = args2typ n (snd con)
   205     | cons2typ n (con::cons) =
   206     let
   207       val (n1, t1) = args2typ n (snd con);
   208       val (n2, t2) = cons2typ n1 cons
   209     in (n2, mk_ssumT (t1, t2)) end;
   210 in
   211   fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
   212 end;
   213 
   214 local 
   215   val iso_swap = iso_locale RS iso_iso_swap;
   216   fun one_con (con, args) =
   217     let
   218       val vns = map vname args;
   219       val eqn = %:x_name === con_app2 con %: vns;
   220       val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
   221     in Library.foldr mk_ex (vns, conj) end;
   222 
   223   val conj_assoc = @{thm conj_assoc};
   224   val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
   225   val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
   226   val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
   227   val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
   228 
   229   (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
   230   val tacs = [
   231     rtac disjE 1,
   232     etac (rep_defin' RS disjI1) 2,
   233     etac disjI2 2,
   234     rewrite_goals_tac [mk_meta_eq iso_swap],
   235     rtac thm3 1];
   236 in
   237   val exhaust = pg con_appls (mk_trp exh) tacs;
   238   val casedist =
   239     standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   240 end;
   241 
   242 local 
   243   fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
   244   fun bound_fun i _ = Bound (length cons - i);
   245   val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
   246 in
   247   val when_strict =
   248     let
   249       val axs = [when_appl, mk_meta_eq rep_strict];
   250       val goal = bind_fun (mk_trp (strict when_app));
   251       val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
   252     in pg axs goal tacs end;
   253 
   254   val when_apps =
   255     let
   256       fun one_when n (con,args) =
   257         let
   258           val axs = when_appl :: con_appls;
   259           val goal = bind_fun (lift_defined %: (nonlazy args, 
   260                 mk_trp (when_app`(con_app con args) ===
   261                        list_ccomb (bound_fun n 0, map %# args))));
   262           val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
   263         in pg axs goal tacs end;
   264     in mapn one_when 1 cons end;
   265 end;
   266 val when_rews = when_strict :: when_apps;
   267 
   268 (* ----- theorems concerning the constructors, discriminators and selectors - *)
   269 
   270 local
   271   fun dis_strict (con, _) =
   272     let
   273       val goal = mk_trp (strict (%%:(dis_name con)));
   274     in pg axs_dis_def goal [rtac when_strict 1] end;
   275 
   276   fun dis_app c (con, args) =
   277     let
   278       val lhs = %%:(dis_name c) ` con_app con args;
   279       val rhs = if con = c then TT else FF;
   280       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
   281       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   282     in pg axs_dis_def goal tacs end;
   283 
   284   val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons);
   285 
   286   fun dis_defin (con, args) =
   287     let
   288       val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
   289       val tacs =
   290         [rtac casedist 1,
   291          contr_tac 1,
   292          DETERM_UNTIL_SOLVED (CHANGED
   293           (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
   294     in pg [] goal tacs end;
   295 
   296   val dis_stricts = map dis_strict cons;
   297   val dis_defins = map dis_defin cons;
   298 in
   299   val dis_rews = dis_stricts @ dis_defins @ dis_apps;
   300 end;
   301 
   302 local
   303   fun mat_strict (con, _) =
   304     let
   305       val goal = mk_trp (strict (%%:(mat_name con)));
   306       val tacs = [rtac when_strict 1];
   307     in pg axs_mat_def goal tacs end;
   308 
   309   val mat_stricts = map mat_strict cons;
   310 
   311   fun one_mat c (con, args) =
   312     let
   313       val lhs = %%:(mat_name c) ` con_app con args;
   314       val rhs =
   315         if con = c
   316         then mk_return (mk_ctuple (map %# args))
   317         else mk_fail;
   318       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
   319       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   320     in pg axs_mat_def goal tacs end;
   321 
   322   val mat_apps =
   323     List.concat (map (fn (c,_) => map (one_mat c) cons) cons);
   324 in
   325   val mat_rews = mat_stricts @ mat_apps;
   326 end;
   327 
   328 local
   329   fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
   330 
   331   fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
   332 
   333   fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
   334     | pat_rhs (con,args) =
   335         (mk_branch (mk_ctuple_pat (ps args)))
   336           `(%:"rhs")`(mk_ctuple (map %# args));
   337 
   338   fun pat_strict c =
   339     let
   340       val axs = @{thm branch_def} :: axs_pat_def;
   341       val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
   342       val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
   343     in pg axs goal tacs end;
   344 
   345   fun pat_app c (con, args) =
   346     let
   347       val axs = @{thm branch_def} :: axs_pat_def;
   348       val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
   349       val rhs = if con = fst c then pat_rhs c else mk_fail;
   350       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
   351       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   352     in pg axs goal tacs end;
   353 
   354   val pat_stricts = map pat_strict cons;
   355   val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons);
   356 in
   357   val pat_rews = pat_stricts @ pat_apps;
   358 end;
   359 
   360 local
   361   val rev_contrapos = @{thm rev_contrapos};
   362   fun con_strict (con, args) = 
   363     let
   364       fun one_strict vn =
   365         let
   366           fun f arg = if vname arg = vn then UU else %# arg;
   367           val goal = mk_trp (con_app2 con f args === UU);
   368           val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
   369         in pg con_appls goal tacs end;
   370     in map one_strict (nonlazy args) end;
   371 
   372   fun con_defin (con, args) =
   373     let
   374       val concl = mk_trp (defined (con_app con args));
   375       val goal = lift_defined %: (nonlazy args, concl);
   376       val tacs = [
   377         rtac @{thm rev_contrapos} 1,
   378         eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
   379         asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
   380     in pg [] goal tacs end;
   381 in
   382   val con_stricts = List.concat (map con_strict cons);
   383   val con_defins = map con_defin cons;
   384   val con_rews = con_stricts @ con_defins;
   385 end;
   386 
   387 local
   388   val rules =
   389     [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
   390   fun con_compact (con, args) =
   391     let
   392       val concl = mk_trp (mk_compact (con_app con args));
   393       val goal = lift (fn x => mk_compact (%#x)) (args, concl);
   394       val tacs = [
   395         rtac (iso_locale RS iso_compact_abs) 1,
   396         REPEAT (resolve_tac rules 1 ORELSE atac 1)];
   397     in pg con_appls goal tacs end;
   398 in
   399   val con_compacts = map con_compact cons;
   400 end;
   401 
   402 local
   403   fun one_sel sel =
   404     pg axs_sel_def (mk_trp (strict (%%:sel)))
   405       [simp_tac (HOLCF_ss addsimps when_rews) 1];
   406 
   407   fun sel_strict (_, args) =
   408     List.mapPartial (Option.map one_sel o sel_of) args;
   409 in
   410   val sel_stricts = List.concat (map sel_strict cons);
   411 end;
   412 
   413 local
   414   fun sel_app_same c n sel (con, args) =
   415     let
   416       val nlas = nonlazy args;
   417       val vns = map vname args;
   418       val vnn = List.nth (vns, n);
   419       val nlas' = List.filter (fn v => v <> vnn) nlas;
   420       val lhs = (%%:sel)`(con_app con args);
   421       val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
   422       val tacs1 =
   423         if vnn mem nlas
   424         then [case_UU_tac (when_rews @ con_stricts) 1 vnn]
   425         else [];
   426       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   427     in pg axs_sel_def goal (tacs1 @ tacs2) end;
   428 
   429   fun sel_app_diff c n sel (con, args) =
   430     let
   431       val nlas = nonlazy args;
   432       val goal = mk_trp (%%:sel ` con_app con args === UU);
   433       val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas;
   434       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   435     in pg axs_sel_def goal (tacs1 @ tacs2) end;
   436 
   437   fun sel_app c n sel (con, args) =
   438     if con = c
   439     then sel_app_same c n sel (con, args)
   440     else sel_app_diff c n sel (con, args);
   441 
   442   fun one_sel c n sel = map (sel_app c n sel) cons;
   443   fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
   444   fun one_con (c, args) =
   445     List.concat (List.mapPartial I (mapn (one_sel' c) 0 args));
   446 in
   447   val sel_apps = List.concat (map one_con cons);
   448 end;
   449 
   450 local
   451   fun sel_defin sel =
   452     let
   453       val goal = defined (%:x_name) ==> defined (%%:sel`%x_name);
   454       val tacs = [
   455         rtac casedist 1,
   456         contr_tac 1,
   457         DETERM_UNTIL_SOLVED (CHANGED
   458           (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
   459     in pg [] goal tacs end;
   460 in
   461   val sel_defins =
   462     if length cons = 1
   463     then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
   464                  (filter_out is_lazy (snd (hd cons)))
   465     else [];
   466 end;
   467 
   468 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
   469 val rev_contrapos = @{thm rev_contrapos};
   470 
   471 val distincts_le =
   472   let
   473     fun dist (con1, args1) (con2, args2) =
   474       let
   475         val goal = lift_defined %: (nonlazy args1,
   476                         mk_trp (con_app con1 args1 ~<< con_app con2 args2));
   477         val tacs = [
   478           rtac @{thm rev_contrapos} 1,
   479           eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1]
   480           @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
   481           @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
   482       in pg [] goal tacs end;
   483 
   484     fun distinct (con1, args1) (con2, args2) =
   485         let
   486           val arg1 = (con1, args1);
   487           val arg2 =
   488             (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
   489               (args2, Name.variant_list (map vname args1) (map vname args2)));
   490         in [dist arg1 arg2, dist arg2 arg1] end;
   491     fun distincts []      = []
   492       | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
   493   in distincts cons end;
   494 val dist_les = List.concat (List.concat distincts_le);
   495 val dist_eqs =
   496   let
   497     fun distinct (_,args1) ((_,args2), leqs) =
   498       let
   499         val (le1,le2) = (hd leqs, hd(tl leqs));
   500         val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI)
   501       in
   502         if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
   503         if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
   504           [eq1, eq2]
   505       end;
   506     fun distincts []      = []
   507       | distincts ((c,leqs)::cs) = List.concat
   508 	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
   509 		    distincts cs;
   510   in map standard (distincts (cons ~~ distincts_le)) end;
   511 
   512 local 
   513   fun pgterm rel con args =
   514     let
   515       fun append s = upd_vname (fn v => v^s);
   516       val (largs, rargs) = (args, map (append "'") args);
   517       val concl =
   518         foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs));
   519       val prem = rel (con_app con largs, con_app con rargs);
   520       val sargs = case largs of [_] => [] | _ => nonlazy args;
   521       val prop = lift_defined %: (sargs, mk_trp (prem === concl));
   522     in pg con_appls prop end;
   523   val cons' = List.filter (fn (_,args) => args<>[]) cons;
   524 in
   525   val inverts =
   526     let
   527       val abs_less = ax_abs_iso RS (allI RS injection_less);
   528       val tacs =
   529         [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
   530     in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end;
   531 
   532   val injects =
   533     let
   534       val abs_eq = ax_abs_iso RS (allI RS injection_eq);
   535       val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
   536     in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end;
   537 end;
   538 
   539 (* ----- theorems concerning one induction step ----------------------------- *)
   540 
   541 val copy_strict =
   542   let
   543     val goal = mk_trp (strict (dc_copy `% "f"));
   544     val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1];
   545   in pg [ax_copy_def] goal tacs end;
   546 
   547 local
   548   fun copy_app (con, args) =
   549     let
   550       val lhs = dc_copy`%"f"`(con_app con args);
   551       val rhs = con_app2 con (app_rec_arg (cproj (%:"f") eqs)) args;
   552       val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
   553       val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
   554       val stricts = abs_strict::when_strict::con_stricts;
   555       val tacs1 = map (case_UU_tac stricts 1 o vname) args';
   556       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
   557     in pg [ax_copy_def] goal (tacs1 @ tacs2) end;
   558 in
   559   val copy_apps = map copy_app cons;
   560 end;
   561 
   562 local
   563   fun one_strict (con, args) = 
   564     let
   565       val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
   566       val rews = copy_strict :: copy_apps @ con_rews;
   567       val tacs = map (case_UU_tac rews 1) (nonlazy args) @
   568         [asm_simp_tac (HOLCF_ss addsimps rews) 1];
   569     in pg [] goal tacs end;
   570 
   571   fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
   572 in
   573   val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
   574 end;
   575 
   576 val copy_rews = copy_strict :: copy_apps @ copy_stricts;
   577 
   578 in
   579   thy
   580     |> Sign.add_path (Sign.base_name dname)
   581     |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
   582         ("iso_rews" , iso_rews  ),
   583         ("exhaust"  , [exhaust] ),
   584         ("casedist" , [casedist]),
   585         ("when_rews", when_rews ),
   586         ("compacts", con_compacts),
   587         ("con_rews", con_rews),
   588         ("sel_rews", sel_rews),
   589         ("dis_rews", dis_rews),
   590         ("pat_rews", pat_rews),
   591         ("dist_les", dist_les),
   592         ("dist_eqs", dist_eqs),
   593         ("inverts" , inverts ),
   594         ("injects" , injects ),
   595         ("copy_rews", copy_rews)])))
   596     |> (snd o PureThy.add_thmss
   597         [(("match_rews", mat_rews), [Simplifier.simp_add])])
   598     |> Sign.parent_path
   599     |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
   600         pat_rews @ dist_les @ dist_eqs @ copy_rews)
   601 end; (* let *)
   602 
   603 fun comp_theorems (comp_dnam, eqs: eq list) thy =
   604 let
   605 val dnames = map (fst o fst) eqs;
   606 val conss  = map  snd        eqs;
   607 val comp_dname = Sign.full_name thy comp_dnam;
   608 
   609 val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
   610 val pg = pg' thy;
   611 
   612 (* ----- getting the composite axiom and definitions ------------------------ *)
   613 
   614 local
   615   fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
   616 in
   617   val axs_reach      = map (ga "reach"     ) dnames;
   618   val axs_take_def   = map (ga "take_def"  ) dnames;
   619   val axs_finite_def = map (ga "finite_def") dnames;
   620   val ax_copy2_def   =      ga "copy_def"  comp_dnam;
   621   val ax_bisim_def   =      ga "bisim_def" comp_dnam;
   622 end;
   623 
   624 local
   625   fun gt  s dn = get_thm  thy (Name (dn ^ "." ^ s));
   626   fun gts s dn = get_thms thy (Name (dn ^ "." ^ s));
   627 in
   628   val cases = map (gt  "casedist" ) dnames;
   629   val con_rews  = List.concat (map (gts "con_rews" ) dnames);
   630   val copy_rews = List.concat (map (gts "copy_rews") dnames);
   631 end;
   632 
   633 fun dc_take dn = %%:(dn^"_take");
   634 val x_name = idx_name dnames "x"; 
   635 val P_name = idx_name dnames "P";
   636 val n_eqs = length eqs;
   637 
   638 (* ----- theorems concerning finite approximation and finite induction ------ *)
   639 
   640 local
   641   val iterate_Cprod_ss = simpset_of (theory "Fix");
   642   val copy_con_rews  = copy_rews @ con_rews;
   643   val copy_take_defs =
   644     (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
   645   val take_stricts =
   646     let
   647       fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
   648       val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
   649       val tacs = [
   650         induct_tac "n" 1,
   651         simp_tac iterate_Cprod_ss 1,
   652         asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
   653     in pg copy_take_defs goal tacs end;
   654 
   655   val take_stricts' = rewrite_rule copy_take_defs take_stricts;
   656   fun take_0 n dn =
   657     let
   658       val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
   659     in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end;
   660   val take_0s = mapn take_0 1 dnames;
   661   val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
   662   val take_apps =
   663     let
   664       fun mk_eqn dn (con, args) =
   665         let
   666           fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
   667           val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
   668           val rhs = con_app2 con (app_rec_arg mk_take) args;
   669         in Library.foldr mk_all (map vname args, lhs === rhs) end;
   670       fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
   671       val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs)));
   672       val simps = List.filter (has_fewer_prems 1) copy_rews;
   673       fun con_tac (con, args) =
   674         if nonlazy_rec args = []
   675         then all_tac
   676         else EVERY (map c_UU_tac (nonlazy_rec args)) THEN
   677           asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
   678       fun eq_tacs ((dn, _), cons) = map con_tac cons;
   679       val tacs =
   680         simp_tac iterate_Cprod_ss 1 ::
   681         induct_tac "n" 1 ::
   682         simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
   683         asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
   684         TRY (safe_tac HOL_cs) ::
   685         List.concat (map eq_tacs eqs);
   686     in pg copy_take_defs goal tacs end;
   687 in
   688   val take_rews = map standard
   689     (atomize take_stricts @ take_0s @ atomize take_apps);
   690 end; (* local *)
   691 
   692 local
   693   fun one_con p (con,args) =
   694     let
   695       fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
   696       val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
   697       val t2 = lift ind_hyp (List.filter is_rec args, t1);
   698       val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
   699     in Library.foldr mk_All (map vname args, t3) end;
   700 
   701   fun one_eq ((p, cons), concl) =
   702     mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
   703 
   704   fun ind_term concf = Library.foldr one_eq
   705     (mapn (fn n => fn x => (P_name n, x)) 1 conss,
   706      mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
   707   val take_ss = HOL_ss addsimps take_rews;
   708   fun quant_tac i = EVERY
   709     (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
   710 
   711   fun ind_prems_tac prems = EVERY
   712     (List.concat (map (fn cons =>
   713       (resolve_tac prems 1 ::
   714         List.concat (map (fn (_,args) => 
   715           resolve_tac prems 1 ::
   716           map (K(atac 1)) (nonlazy args) @
   717           map (K(atac 1)) (List.filter is_rec args))
   718         cons)))
   719       conss));
   720   local 
   721     (* check whether every/exists constructor of the n-th part of the equation:
   722        it has a possibly indirectly recursive argument that isn't/is possibly 
   723        indirectly lazy *)
   724     fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
   725           is_rec arg andalso not(rec_of arg mem ns) andalso
   726           ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
   727             rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
   728               (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
   729           ) o snd) cons;
   730     fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
   731     fun warn (n,cons) =
   732       if all_rec_to [] false (n,cons)
   733       then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
   734       else false;
   735     fun lazy_rec_to ns = rec_to exists I  lazy_rec_to ns;
   736 
   737   in
   738     val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
   739     val is_emptys = map warn n__eqs;
   740     val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
   741   end;
   742 in (* local *)
   743   val finite_ind =
   744     let
   745       fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
   746       val goal = ind_term concf;
   747 
   748       fun tacf prems =
   749         let
   750           val tacs1 = [
   751             quant_tac 1,
   752             simp_tac HOL_ss 1,
   753             induct_tac "n" 1,
   754             simp_tac (take_ss addsimps prems) 1,
   755             TRY (safe_tac HOL_cs)];
   756           fun arg_tac arg =
   757             case_UU_tac (prems @ con_rews) 1
   758               (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
   759           fun con_tacs (con, args) = 
   760             asm_simp_tac take_ss 1 ::
   761             map arg_tac (List.filter is_nonlazy_rec args) @
   762             [resolve_tac prems 1] @
   763             map (K (atac 1))      (nonlazy args) @
   764             map (K (etac spec 1)) (List.filter is_rec args);
   765           fun cases_tacs (cons, cases) =
   766             res_inst_tac [("x","x")] cases 1 ::
   767             asm_simp_tac (take_ss addsimps prems) 1 ::
   768             List.concat (map con_tacs cons);
   769         in
   770           tacs1 @ List.concat (map cases_tacs (conss ~~ cases))
   771         end;
   772     in pg'' thy [] goal tacf end;
   773 
   774   val take_lemmas =
   775     let
   776       fun take_lemma n (dn, ax_reach) =
   777         let
   778           val lhs = dc_take dn $ Bound 0 `%(x_name n);
   779           val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
   780           val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
   781           val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
   782           fun tacf prems = [
   783             res_inst_tac [("t", x_name n    )] (ax_reach RS subst) 1,
   784             res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1,
   785             stac fix_def2 1,
   786             REPEAT (CHANGED
   787               (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
   788             stac contlub_cfun_fun 1,
   789             stac contlub_cfun_fun 2,
   790             rtac lub_equal 3,
   791             chain_tac 1,
   792             rtac allI 1,
   793             resolve_tac prems 1];
   794         in pg'' thy axs_take_def goal tacf end;
   795     in mapn take_lemma 1 (dnames ~~ axs_reach) end;
   796 
   797 (* ----- theorems concerning finiteness and induction ----------------------- *)
   798 
   799   val (finites, ind) =
   800     if is_finite
   801     then (* finite case *)
   802       let 
   803         fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
   804         fun dname_lemma dn =
   805           let
   806             val prem1 = mk_trp (defined (%:"x"));
   807             val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
   808             val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
   809             val concl = mk_trp (take_enough dn);
   810             val goal = prem1 ===> prem2 ===> concl;
   811             val tacs = [
   812               etac disjE 1,
   813               etac notE 1,
   814               resolve_tac take_lemmas 1,
   815               asm_simp_tac take_ss 1,
   816               atac 1];
   817           in pg [] goal tacs end;
   818         val finite_lemmas1a = map dname_lemma dnames;
   819  
   820         val finite_lemma1b =
   821           let
   822             fun mk_eqn n ((dn, args), _) =
   823               let
   824                 val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
   825                 val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
   826               in
   827                 mk_constrainall
   828                   (x_name n, Type (dn,args), mk_disj (disj1, disj2))
   829               end;
   830             val goal =
   831               mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
   832             fun arg_tacs vn = [
   833               eres_inst_tac [("x", vn)] all_dupE 1,
   834               etac disjE 1,
   835               asm_simp_tac (HOL_ss addsimps con_rews) 1,
   836               asm_simp_tac take_ss 1];
   837             fun con_tacs (con, args) =
   838               asm_simp_tac take_ss 1 ::
   839               List.concat (map arg_tacs (nonlazy_rec args));
   840             fun foo_tacs n (cons, cases) =
   841               simp_tac take_ss 1 ::
   842               rtac allI 1 ::
   843               res_inst_tac [("x",x_name n)] cases 1 ::
   844               asm_simp_tac take_ss 1 ::
   845               List.concat (map con_tacs cons);
   846             val tacs =
   847               rtac allI 1 ::
   848               induct_tac "n" 1 ::
   849               simp_tac take_ss 1 ::
   850               TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
   851               List.concat (mapn foo_tacs 1 (conss ~~ cases));
   852           in pg [] goal tacs end;
   853 
   854         fun one_finite (dn, l1b) =
   855           let
   856             val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
   857             val tacs = [
   858               case_UU_tac take_rews 1 "x",
   859               eresolve_tac finite_lemmas1a 1,
   860               step_tac HOL_cs 1,
   861               step_tac HOL_cs 1,
   862               cut_facts_tac [l1b] 1,
   863               fast_tac HOL_cs 1];
   864           in pg axs_finite_def goal tacs end;
   865 
   866         val finites = map one_finite (dnames ~~ atomize finite_lemma1b);
   867         val ind =
   868           let
   869             fun concf n dn = %:(P_name n) $ %:(x_name n);
   870             fun tacf prems =
   871               let
   872                 fun finite_tacs (finite, fin_ind) = [
   873                   rtac(rewrite_rule axs_finite_def finite RS exE)1,
   874                   etac subst 1,
   875                   rtac fin_ind 1,
   876                   ind_prems_tac prems];
   877               in
   878                 TRY (safe_tac HOL_cs) ::
   879                 List.concat (map finite_tacs (finites ~~ atomize finite_ind))
   880               end;
   881           in pg'' thy [] (ind_term concf) tacf end;
   882       in (finites, ind) end (* let *)
   883 
   884     else (* infinite case *)
   885       let
   886         fun one_finite n dn =
   887           read_instantiate_sg thy
   888             [("P",dn^"_finite "^x_name n)] excluded_middle;
   889         val finites = mapn one_finite 1 dnames;
   890 
   891         val goal =
   892           let
   893             fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
   894             fun concf n dn = %:(P_name n) $ %:(x_name n);
   895           in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
   896         fun tacf prems =
   897           map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
   898           quant_tac 1,
   899           rtac (adm_impl_admw RS wfix_ind) 1,
   900           REPEAT_DETERM (rtac adm_all 1),
   901           REPEAT_DETERM (
   902             TRY (rtac adm_conj 1) THEN 
   903             rtac adm_subst 1 THEN 
   904             cont_tacR 1 THEN resolve_tac prems 1),
   905           strip_tac 1,
   906           rtac (rewrite_rule axs_take_def finite_ind) 1,
   907           ind_prems_tac prems];
   908         val ind = (pg'' thy [] goal tacf
   909           handle ERROR _ =>
   910             (warning "Cannot prove infinite induction rule"; refl));
   911       in (finites, ind) end;
   912 end; (* local *)
   913 
   914 (* ----- theorem concerning coinduction ------------------------------------- *)
   915 
   916 local
   917   val xs = mapn (fn n => K (x_name n)) 1 dnames;
   918   fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
   919   val take_ss = HOL_ss addsimps take_rews;
   920   val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
   921   val coind_lemma =
   922     let
   923       fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
   924       fun mk_eqn n dn =
   925         (dc_take dn $ %:"n" ` bnd_arg n 0) ===
   926         (dc_take dn $ %:"n" ` bnd_arg n 1);
   927       fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
   928       val goal =
   929         mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
   930           Library.foldr mk_all2 (xs,
   931             Library.foldr mk_imp (mapn mk_prj 0 dnames,
   932               foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
   933       fun x_tacs n x = [
   934         rotate_tac (n+1) 1,
   935         etac all2E 1,
   936         eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
   937         TRY (safe_tac HOL_cs),
   938         REPEAT (CHANGED (asm_simp_tac take_ss 1))];
   939       val tacs = [
   940         rtac impI 1,
   941         induct_tac "n" 1,
   942         simp_tac take_ss 1,
   943         safe_tac HOL_cs] @
   944         List.concat (mapn x_tacs 0 xs);
   945     in pg [ax_bisim_def] goal tacs end;
   946 in
   947   val coind = 
   948     let
   949       fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
   950       fun mk_eqn x = %:x === %:(x^"'");
   951       val goal =
   952         mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
   953           Logic.list_implies (mapn mk_prj 0 xs,
   954             mk_trp (foldr1 mk_conj (map mk_eqn xs)));
   955       val tacs =
   956         TRY (safe_tac HOL_cs) ::
   957         List.concat (map (fn take_lemma => [
   958           rtac take_lemma 1,
   959           cut_facts_tac [coind_lemma] 1,
   960           fast_tac HOL_cs 1])
   961         take_lemmas);
   962     in pg [] goal tacs end;
   963 end; (* local *)
   964 
   965 in thy |> Sign.add_path comp_dnam
   966        |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
   967 		("take_rews"  , take_rews  ),
   968 		("take_lemmas", take_lemmas),
   969 		("finites"    , finites    ),
   970 		("finite_ind", [finite_ind]),
   971 		("ind"       , [ind       ]),
   972 		("coind"     , [coind     ])])))
   973        |> Sign.parent_path |> rpair take_rews
   974 end; (* let *)
   975 end; (* local *)
   976 end; (* struct *)