src/HOL/Codatatype/Tools/bnf_comp.ML
changeset 49463 83ac281bcdc2
parent 49461 de07eecb2664
child 49502 92a7c1842c78
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:49 2012 +0200
@@ -12,6 +12,7 @@
   val empty_unfold: unfold_thms
   val map_unfolds_of: unfold_thms -> thm list
   val set_unfoldss_of: unfold_thms -> thm list list
+  val pred_unfolds_of: unfold_thms -> thm list
   val rel_unfolds_of: unfold_thms -> thm list
 
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
@@ -36,6 +37,7 @@
 type unfold_thms = {
   map_unfolds: thm list,
   set_unfoldss: thm list list,
+  pred_unfolds: thm list,
   rel_unfolds: thm list
 };
 
@@ -44,17 +46,21 @@
 fun adds_to_thms thms NONE = thms
   | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
 
-val empty_unfold = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
+val empty_unfold = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []};
 
-fun add_to_unfold_opt map_opt sets_opt rel_opt {map_unfolds, set_unfoldss, rel_unfolds} = {
-  map_unfolds = add_to_thms map_unfolds map_opt,
-  set_unfoldss = adds_to_thms set_unfoldss sets_opt,
-  rel_unfolds = add_to_thms rel_unfolds rel_opt};
+fun add_to_unfold_opt map_opt sets_opt pred_opt rel_opt
+  {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} =
+  {map_unfolds = add_to_thms map_unfolds map_opt,
+    set_unfoldss = adds_to_thms set_unfoldss sets_opt,
+    pred_unfolds = add_to_thms pred_unfolds pred_opt,
+    rel_unfolds = add_to_thms rel_unfolds rel_opt};
 
-fun add_to_unfold map sets rel = add_to_unfold_opt (SOME map) (SOME sets) (SOME rel);
+fun add_to_unfold map sets pred rel =
+  add_to_unfold_opt (SOME map) (SOME sets) (SOME pred) (SOME rel);
 
 val map_unfolds_of = #map_unfolds;
 val set_unfoldss_of = #set_unfoldss;
+val pred_unfolds_of = #pred_unfolds;
 val rel_unfolds_of = #rel_unfolds;
 
 val bdTN = "bdT";
@@ -64,8 +70,6 @@
 fun mk_permuteN src dest =
   "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
 
-val subst_rel_def = @{thm subst_rel_def};
-
 (*copied from Envir.expand_term_free*)
 fun expand_term_const defs =
   let
@@ -99,9 +103,9 @@
       (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
     val Bss_repl = replicate olive Bs;
 
-    val ((((fs', Rs'), Asets), xs), _(*names_lthy*)) = lthy
+    val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy
       |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
-      ||>> apfst snd o mk_Frees' "R" (map2 (curry mk_relT) As Bs)
+      ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
       ||>> mk_Frees "A" (map HOLogic.mk_setT As)
       ||>> mk_Frees "x" As;
 
@@ -116,13 +120,13 @@
     (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
     val mapx = fold_rev Term.abs fs'
       (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
-        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
+        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
           mk_map_of_bnf Ds As Bs) Dss inners));
-    (*%R1 ... Rn. outer.rel (inner_1.rel R1 ... Rn) ... (inner_m.rel R1 ... Rn)*)
-    val rel = fold_rev Term.abs Rs'
-      (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
-        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
-          mk_rel_of_bnf Ds As Bs) Dss inners));
+    (*%Q1 ... Qn. outer.pred (inner_1.pred Q1 ... Qn) ... (inner_m.pred Q1 ... Qn)*)
+    val pred = fold_rev Term.abs Qs'
+      (Term.list_comb (mk_pred_of_bnf oDs CAs CBs outer,
+        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
+          mk_pred_of_bnf Ds As Bs) Dss inners));
 
     (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
     (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
@@ -229,16 +233,20 @@
 
     fun rel_O_Gr_tac _ =
       let
+        val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
         val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
         val outer_rel_cong = rel_cong_of_bnf outer;
+        val thm =
+          (trans OF [in_alt_thm RS @{thm subst_rel_def},
+             trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
+               [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
+                 rel_converse_of_bnf outer RS sym], outer_rel_Gr],
+               trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
+                 (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
+          |> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
       in
-        rtac (trans OF [in_alt_thm RS subst_rel_def,
-                trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-                  [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
-                    rel_converse_of_bnf outer RS sym], outer_rel_Gr],
-                  trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
-                    (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym) 1
-      end
+        unfold_defs_tac lthy basic_thms THEN rtac thm 1
+      end;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
@@ -264,10 +272,10 @@
 
     val (bnf', lthy') =
       bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
-        (((((b, mapx), sets), bd), wits), SOME rel) lthy;
+        (((((b, mapx), sets), bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
-      unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+      (rel_def_of_bnf bnf') unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -299,8 +307,8 @@
 
     (*bnf.map id ... id*)
     val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
-    (*bnf.rel Id ... Id*)
-    val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map Id_const killedAs);
+    (*bnf.pred (op =) ... (op =)*)
+    val pred = Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
 
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = drop n bnf_sets;
@@ -312,7 +320,7 @@
 
     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
     fun map_comp_tac {context, ...} =
-      Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
     fun map_cong_tac {context, ...} =
       mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
@@ -340,14 +348,17 @@
     fun rel_O_Gr_tac _ =
       let
         val rel_Gr = rel_Gr_of_bnf bnf RS sym
+        val thm =
+          (trans OF [in_alt_thm RS @{thm subst_rel_def},
+            trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
+              [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
+                rel_converse_of_bnf bnf RS sym], rel_Gr],
+              trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+                (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
+                 replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
+          |> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
       in
-        rtac (trans OF [in_alt_thm RS subst_rel_def,
-                trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-                  [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
-                    rel_converse_of_bnf bnf RS sym], rel_Gr],
-                  trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
-                    (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
-                     replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) 1
+        rtac thm 1
       end;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
@@ -362,10 +373,10 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
-        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
-      unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+      (rel_def_of_bnf bnf') unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -396,9 +407,8 @@
     (*%f1 ... fn. bnf.map*)
     val mapx =
       fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
-    (*%R1 ... Rn. bnf.rel*)
-    val rel =
-      fold_rev Term.absdummy (map2 (curry mk_relT) newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
+    (*%Q1 ... Qn. bnf.pred*)
+    val pred = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_pred_of_bnf Ds As Bs bnf);
 
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
@@ -407,7 +417,7 @@
 
     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
     fun map_comp_tac {context, ...} =
-      Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
     fun map_cong_tac {context, ...} =
       rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
@@ -439,7 +449,7 @@
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
     fun rel_O_Gr_tac _ =
-      rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+      mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
@@ -450,10 +460,10 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
-        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
-      unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+      (pred_def_of_bnf bnf') unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -483,10 +493,10 @@
 
     (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
     val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
-      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
-    (*%R(1) ... R(n). bnf.rel R\<sigma>(1) ... R\<sigma>(n)*)
-    val rel = fold_rev Term.absdummy (permute (map2 (curry mk_relT) As Bs))
-      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
+      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
+    (*%Q(1) ... Q(n). bnf.pred Q\<sigma>(1) ... Q\<sigma>(n)*)
+    val pred = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
+      (Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
 
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = permute bnf_sets;
@@ -517,7 +527,7 @@
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
     fun rel_O_Gr_tac _ =
-      rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+      mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
@@ -528,10 +538,10 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
-        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
-      unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+      (pred_def_of_bnf bnf') unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -607,22 +617,25 @@
 
     val map_unfolds = map_unfolds_of unfold;
     val set_unfoldss = set_unfoldss_of unfold;
+    val pred_unfolds = pred_unfolds_of unfold;
     val rel_unfolds = rel_unfolds_of unfold;
 
     val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
       map_unfolds);
     val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
       set_unfoldss);
-    val expand_rels = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
-      rel_unfolds);
-    val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds;
-    val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss;
-    val unfold_defs = unfold_sets o unfold_maps;
+    val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
+      pred_unfolds);
+    val unfold_maps = fold (unfold_defs lthy o single) map_unfolds;
+    val unfold_sets = fold (unfold_defs lthy) set_unfoldss;
+    val unfold_preds = unfold_defs lthy pred_unfolds;
+    val unfold_rels = unfold_defs lthy rel_unfolds;
+    val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
     val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
     val bnf_sets = map (expand_maps o expand_sets)
       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
     val bnf_bd = mk_bd_of_bnf Ds As bnf;
-    val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);
+    val bnf_pred = expand_preds (mk_pred_of_bnf Ds As Bs bnf);
     val T = mk_T_of_bnf Ds As bnf;
 
     (*bd should only depend on dead type variables!*)
@@ -655,22 +668,24 @@
           @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
             bd_Card_order_of_bnf bnf]];
 
-    fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
+    fun mk_tac thm {context = ctxt, prems = _} =
+      (rtac (unfold_all thm) THEN'
       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
 
     val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
       (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
-      (mk_tac (map_wpull_of_bnf bnf)) (mk_tac (rel_O_Gr_of_bnf bnf));
+      (mk_tac (map_wpull_of_bnf bnf))
+      (mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
+    fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
 
     val policy = user_policy Derive_All_Facts;
 
     val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
-      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_pred) lthy;
   in
     ((bnf', deads), lthy')
   end;