# HG changeset patch
# User huffman
# Date 1291160091 28800
# Node ID 4f130bd9e17e8465499e0dbc3668b56e75b616d6
# Parent  4352ca878c41ad0890feb708269514233d6440f8
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules

diff -r 4352ca878c41 -r 4f130bd9e17e src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 30 14:21:57 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 30 15:34:51 2010 -0800
@@ -34,13 +34,8 @@
 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
 struct
 
-val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
-  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'}
-
-val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
-
-val beta_tac = simp_tac beta_ss
+val beta_ss =
+  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
 
 fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
 
@@ -165,7 +160,7 @@
     (* prove applied version of definitions *)
     fun prove_proj (lhs, rhs) =
       let
-        val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1
+        val tac = rewrite_goals_tac fixdef_thms THEN (simp_tac beta_ss) 1
         val goal = Logic.mk_equals (lhs, rhs)
       in Goal.prove_global thy [] [] goal (K tac) end
     val proj_thms = map prove_proj projs
@@ -175,8 +170,14 @@
     val tuple_fixdef_thm = foldr1 pair_equalI proj_thms
 
     val cont_thm =
-      Goal.prove_global thy [] [] (mk_trp (mk_cont functional))
-        (K (beta_tac 1))
+      let
+        val prop = mk_trp (mk_cont functional)
+        val rules = Cont2ContData.get (ProofContext.init_global thy)
+        val tac = REPEAT_ALL_NEW (match_tac rules) 1
+      in
+        Goal.prove_global thy [] [] prop (K tac)
+      end
+
     val tuple_unfold_thm =
       (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
       |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv}
diff -r 4352ca878c41 -r 4f130bd9e17e src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Nov 30 14:21:57 2010 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Nov 30 15:34:51 2010 -0800
@@ -107,13 +107,8 @@
     take_induct_thms    : thm list
   }
 
-val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
-  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}
-
-val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
-
-val beta_tac = simp_tac beta_ss
+val beta_ss =
+  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
 
 (******************************************************************************)
 (******************************** theory data *********************************)