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