src/HOLCF/domain/theorems.ML

 
 val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
                                 rtac rev_contrapos 1,
                                 etac (antisym_less_inverse RS conjunct1) 1,
                                 resolve_tac prems 1]);
-
-in
-
-fun theorems (((dname,_),cons) : eq, eqs : eq list) thy =
-let
-
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
-val pg = pg' thy;
 (*
 infixr 0 y;
 val b = 0;
 fun _ y t = by t;
 fun g defs t = let val sg = sign_of thy;
                      val ct = Thm.cterm_of sg (inferT sg t);
                  in goalw_cterm defs ct end;
 *)
+
+in
+
+fun theorems (((dname,_),cons) : eq, eqs : eq list) thy =
+let
+
+val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+val pg = pg' thy;
 
 
 (* ----- getting the axioms and definitions --------------------------------- *)
 
 local fun ga s dn = get_axiom thy (dn^"."^s) in

                    asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
                                                    cfst_strict,csnd_strict]) 1];
 val copy_apps = map (fn (con,args) => pg [ax_copy_def]
                     (lift_defined % (nonlazy_rec args,
                         mk_trp(dc_copy`%"f"`(con_app con args) ===
-                (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
+                (con_app2 con (app_rec_arg (cproj (%"f") eqs)) args))))
                         (map (case_UU_tac (abs_strict::when_strict::con_stricts)
                                  1 o vname)
                          (filter (fn a => not (is_rec a orelse is_lazy a)) args)
                         @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
                           simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;

                                                    rtac adm_subst 1 THEN 
                                         cont_tacR 1 THEN resolve_tac prems 1),
                                 strip_tac 1,
                                 rtac (rewrite_rule axs_take_def finite_ind) 1,
                                 ind_prems_tac prems])
-)
+  handle ERROR => (warning "Cannot prove infinite induction rule"; refl))
 end; (* local *)
 
 (* ----- theorem concerning coinduction ------------------------------------- *)
 
 local
   val xs = mapn (fn n => K (x_name n)) 1 dnames;
   fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
   val take_ss = HOL_ss addsimps take_rews;
-  val sproj   = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")");
+  val sproj   = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
   val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
                 foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
-                  foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ 
+                  foldr mk_imp (mapn (fn n => K(proj (%"R") eqs n $ 
                                       bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
                     foldr' mk_conj (mapn (fn n => fn dn => 
                                 (dc_take dn $ %"n" `bnd_arg n 0 === 
                                 (dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
                              ([ rtac impI 1,

                                 simp_tac take_ss 1,
                                 safe_tac HOL_cs] @
                                 flat(mapn (fn n => fn x => [
                                   rotate_tac (n+1) 1,
                                   etac all2E 1,
-                                  eres_inst_tac [("P1", sproj "R" n_eqs n^
+                                  eres_inst_tac [("P1", sproj "R" eqs n^
                                         " "^x^" "^x^"'")](mp RS disjE) 1,
                                   TRY(safe_tac HOL_cs),
                                   REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
                                 0 xs));
 in
 val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
                 foldr (op ===>) (mapn (fn n => fn x => 
-                  mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
+                  mk_trp(proj (%"R") eqs n $ %x $ %(x^"'"))) 0 xs,
                   mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
                                 TRY(safe_tac HOL_cs)] @
                                 flat(map (fn take_lemma => [
                                   rtac take_lemma 1,
                                   cut_facts_tac [coind_lemma] 1,