src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35443 2e0f9516947e
parent 35288 aa7da51ae1ef
child 35444 73f645fdd4ff
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Feb 24 14:13:15 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Feb 24 14:20:07 2010 -0800
     1.3 @@ -118,6 +118,9 @@
     1.4        else cut_facts_tac prems 1 :: tacsf context;
     1.5    in pg'' thy defs t tacs end;
     1.6  
     1.7 +(* FIXME!!!!!!!!! *)
     1.8 +(* We should NEVER re-parse variable names as strings! *)
     1.9 +(* The names can conflict with existing constants or other syntax! *)
    1.10  fun case_UU_tac ctxt rews i v =
    1.11    InductTacs.case_tac ctxt (v^"=UU") i THEN
    1.12    asm_simp_tac (HOLCF_ss addsimps rews) i;
    1.13 @@ -232,13 +235,14 @@
    1.14    fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons));
    1.15  end;
    1.16  
    1.17 -local 
    1.18 +local
    1.19    val iso_swap = iso_locale RS iso_iso_swap;
    1.20    fun one_con (con, _, args) =
    1.21      let
    1.22 -      val vns = map vname args;
    1.23 +      val vns = Name.variant_list ["x"] (map vname args);
    1.24 +      val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
    1.25        val eqn = %:x_name === con_app2 con %: vns;
    1.26 -      val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
    1.27 +      val conj = foldr1 mk_conj (eqn :: map (defined o %:) nonlazy_vns);
    1.28      in Library.foldr mk_ex (vns, conj) end;
    1.29  
    1.30    val conj_assoc = @{thm conj_assoc};
    1.31 @@ -459,6 +463,7 @@
    1.32        val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
    1.33        fun tacs1 ctxt =
    1.34          if vnn mem nlas
    1.35 +                        (* FIXME! case_UU_tac *)
    1.36          then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
    1.37          else [];
    1.38        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.39 @@ -468,6 +473,7 @@
    1.40      let
    1.41        val nlas = nonlazy args;
    1.42        val goal = mk_trp (%%:sel ` con_app con args === UU);
    1.43 +                        (* FIXME! case_UU_tac *)
    1.44        fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
    1.45        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    1.46      in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
    1.47 @@ -625,6 +631,7 @@
    1.48        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
    1.49        val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
    1.50        val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
    1.51 +                        (* FIXME! case_UU_tac *)
    1.52        fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
    1.53        val rules = [ax_abs_iso] @ @{thms domain_map_simps};
    1.54        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
    1.55 @@ -639,6 +646,7 @@
    1.56      let
    1.57        val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
    1.58        val rews = the_list copy_strict @ copy_apps @ con_rews;
    1.59 +                        (* FIXME! case_UU_tac *)
    1.60        fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
    1.61          [asm_simp_tac (HOLCF_ss addsimps rews) 1];
    1.62      in
    1.63 @@ -775,11 +783,14 @@
    1.64  local
    1.65    fun one_con p (con, _, args) =
    1.66      let
    1.67 +      val P_names = map P_name (1 upto (length dnames));
    1.68 +      val vns = Name.variant_list P_names (map vname args);
    1.69 +      val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
    1.70        fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
    1.71        val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
    1.72        val t2 = lift ind_hyp (filter is_rec args, t1);
    1.73 -      val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
    1.74 -    in Library.foldr mk_All (map vname args, t3) end;
    1.75 +      val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
    1.76 +    in Library.foldr mk_All (vns, t3) end;
    1.77  
    1.78    fun one_eq ((p, cons), concl) =
    1.79      mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
    1.80 @@ -838,6 +849,7 @@
    1.81              simp_tac (take_ss addsimps prems) 1,
    1.82              TRY (safe_tac HOL_cs)];
    1.83            fun arg_tac arg =
    1.84 +                        (* FIXME! case_UU_tac *)
    1.85              case_UU_tac context (prems @ con_rews) 1
    1.86                (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
    1.87            fun con_tacs (con, _, args) = 
    1.88 @@ -948,6 +960,7 @@
    1.89            let
    1.90              val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
    1.91              fun tacs ctxt = [
    1.92 +                        (* FIXME! case_UU_tac *)
    1.93                case_UU_tac ctxt take_rews 1 "x",
    1.94                eresolve_tac finite_lemmas1a 1,
    1.95                step_tac HOL_cs 1,