merged
authorwenzelm
Wed, 05 Sep 2012 13:44:03 +0200
changeset 49154 4c507e92e4a2
parent 49153 c15a7123605c (diff)
parent 49145 0ee5983e3d59 (current diff)
child 49155 f51ab68f882f
merged
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 13:44:03 2012 +0200
@@ -99,9 +99,14 @@
       |> mk_TFrees N
       ||> the_single o fst o mk_TFrees 1;
 
-    fun freeze_rec (T as Type (s, Ts')) =
-        (case find_index (curry (op =) T) Ts of
-          ~1 => Type (s, map freeze_rec Ts')
+    fun is_same_rec (T as Type (s, Us)) (Type (s', Us')) =
+        s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
+          quote (Syntax.string_of_typ fake_lthy T)))
+      | is_same_rec _ _ = false
+
+    fun freeze_rec (T as Type (s, Us)) =
+        (case find_index (is_same_rec T) Ts of
+          ~1 => Type (s, map freeze_rec Us)
         | i => nth Bs i)
       | freeze_rec T = T;
 
@@ -210,11 +215,17 @@
         fun sugar_lfp lthy =
           let
 (*###
-            val iter_Tss = map ( ) ctr_Tss
+            val fld_iter = @{term True}; (*###*)
+
+            val iter_Tss = map (fn Ts => Ts) (*###*) ctr_Tss;
             val iter_Ts = map (fn Ts => Ts ---> C) iter_Tss;
 
             val iter_fs = map2 (fn Free (s, _) => fn T => Free (s, T)) fs iter_Ts
 
+            val iter_rhs =
+              fold_rev Term.lambda fs (fld_iter $ mk_sum_caseN (uncurry_fs fs xss) $ (unf $ v));
+
+
             val uncurried_fs =
               map2 (fn f => fn xs =>
                 HOLogic.tupled_lambda (HOLogic.mk_tuple xs) (Term.list_comb (f, xs))) fs xss;
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Wed Sep 05 13:44:03 2012 +0200
@@ -30,8 +30,9 @@
 fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
   Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
   Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
-  EVERY' (map2 (fn k => fn m => select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN'
-    etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
+  EVERY' (map2 (fn k => fn m =>
+    select_prem_tac k (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' rotate_tac ~1 THEN'
+      etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
 
 fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
   (rtac iffI THEN'
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 13:44:03 2012 +0200
@@ -51,6 +51,7 @@
 
 fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
 
+(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *)
 fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
 
 fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
@@ -98,10 +99,10 @@
 
     val raw_disc_binders' = pad_list no_binder n raw_disc_binders;
 
-    fun can_rely_on_disc i =
-      not (Binding.eq_name (nth raw_disc_binders' i, no_binder)) orelse nth ms i = 0;
+    fun can_rely_on_disc k =
+      not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0;
     fun can_omit_disc_binder k m =
-      n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (2 - k))
+      n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k))
 
     val fallback_disc_binder = Binding.name o prefix is_N o Long_Name.base_name o name_of_ctr;
 
@@ -173,12 +174,14 @@
 
     fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
 
-    fun alternate_disc_lhs i =
+    fun alternate_disc_lhs k =
       HOLogic.mk_not
-        (case nth disc_binders i of NONE => nth exist_xs_v_eq_ctrs i | SOME b => disc_free b $ v);
+        (case nth disc_binders (k - 1) of
+          NONE => nth exist_xs_v_eq_ctrs (k - 1)
+        | SOME b => disc_free b $ v);
 
     fun alternate_disc k =
-      if n = 2 then Term.lambda v (alternate_disc_lhs (2 - k)) else error "Cannot use \"*\" here"
+      if n = 2 then Term.lambda v (alternate_disc_lhs (3 - k)) else error "Cannot use \"*\" here"
 
     fun sel_spec b x xs k =
       let val T' = fastype_of x in
@@ -311,11 +314,11 @@
         fun mk_alternate_disc_def k =
           let
             val goal =
-              mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (2 - k)),
+              mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (3 - k)),
                 nth exist_xs_v_eq_ctrs (k - 1));
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_alternate_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
+              mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
                 exhaust_thm')
             |> singleton (Proof_Context.export names_lthy lthy)
             |> Thm.close_derivation
@@ -421,7 +424,7 @@
             val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
+              mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
             |> singleton (Proof_Context.export names_lthy lthy)
           end;
 
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 13:44:03 2012 +0200
@@ -7,9 +7,10 @@
 
 signature BNF_WRAP_TACTICS =
 sig
-  val mk_alternate_disc_def_tac: Proof.context -> thm -> thm -> thm -> tactic
+  val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
   val mk_case_cong_tac: thm -> thm list -> tactic
-  val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
+  val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
+    tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
   val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
@@ -29,8 +30,10 @@
 fun triangle _ [] = []
   | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss
 
-fun mk_if_P_or_not_P thm =
-  thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P}
+fun mk_case_if_P_or_not_Ps n k thms =
+  let val (negs, pos) = split_last thms in
+    map (fn thm => thm RS @{thm if_not_P}) negs @ (if k = n then [] else [pos RS @{thm if_P}])
+  end;
 
 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
 
@@ -41,10 +44,11 @@
 fun mk_unique_disc_def_tac m exhaust' =
   EVERY' [rtac iffI, rtac exhaust', REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
 
-fun mk_alternate_disc_def_tac ctxt other_disc_def distinct exhaust' =
-  EVERY' [subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
+fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' =
+  EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
     SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct,
-    rtac exhaust', etac notE, atac, REPEAT_DETERM o rtac exI, atac] 1;
+    rtac exhaust'] @
+    (([etac notE, atac], [REPEAT_DETERM o rtac exI, atac]) |> k = 1 ? swap |> op @)) 1;
 
 fun mk_half_disc_exclude_tac m discD disc'_thm =
   (dtac discD THEN'
@@ -70,13 +74,12 @@
       SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
       rtac refl)) 1;
 
-fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
+fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss =
   (rtac exhaust' THEN'
-   EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [
-     hyp_subst_tac THEN'
-     SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN'
-     rtac case_thm]) case_thms
-  (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1;
+   EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
+       EVERY' [hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)),
+         rtac case_thm])
+     case_thms (map2 (mk_case_if_P_or_not_Ps n) (1 upto n) (triangle 1 disc_thmss')) sel_thmss)) 1;
 
 fun mk_case_cong_tac exhaust' case_thms =
   (rtac exhaust' THEN'