internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
authorhuffman
Tue Nov 30 15:34:51 2010 -0800 (2010-11-30)
changeset 408334f130bd9e17e
parent 40832 4352ca878c41
child 40834 a1249aeff5b6
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 30 14:21:57 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 30 15:34:51 2010 -0800
     1.3 @@ -34,13 +34,8 @@
     1.4  structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
     1.5  struct
     1.6  
     1.7 -val beta_rules =
     1.8 -  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
     1.9 -  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'}
    1.10 -
    1.11 -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
    1.12 -
    1.13 -val beta_tac = simp_tac beta_ss
    1.14 +val beta_ss =
    1.15 +  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
    1.16  
    1.17  fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
    1.18  
    1.19 @@ -165,7 +160,7 @@
    1.20      (* prove applied version of definitions *)
    1.21      fun prove_proj (lhs, rhs) =
    1.22        let
    1.23 -        val tac = rewrite_goals_tac fixdef_thms THEN beta_tac 1
    1.24 +        val tac = rewrite_goals_tac fixdef_thms THEN (simp_tac beta_ss) 1
    1.25          val goal = Logic.mk_equals (lhs, rhs)
    1.26        in Goal.prove_global thy [] [] goal (K tac) end
    1.27      val proj_thms = map prove_proj projs
    1.28 @@ -175,8 +170,14 @@
    1.29      val tuple_fixdef_thm = foldr1 pair_equalI proj_thms
    1.30  
    1.31      val cont_thm =
    1.32 -      Goal.prove_global thy [] [] (mk_trp (mk_cont functional))
    1.33 -        (K (beta_tac 1))
    1.34 +      let
    1.35 +        val prop = mk_trp (mk_cont functional)
    1.36 +        val rules = Cont2ContData.get (ProofContext.init_global thy)
    1.37 +        val tac = REPEAT_ALL_NEW (match_tac rules) 1
    1.38 +      in
    1.39 +        Goal.prove_global thy [] [] prop (K tac)
    1.40 +      end
    1.41 +
    1.42      val tuple_unfold_thm =
    1.43        (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
    1.44        |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv}
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Nov 30 14:21:57 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Nov 30 15:34:51 2010 -0800
     2.3 @@ -107,13 +107,8 @@
     2.4      take_induct_thms    : thm list
     2.5    }
     2.6  
     2.7 -val beta_rules =
     2.8 -  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
     2.9 -  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}
    2.10 -
    2.11 -val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules)
    2.12 -
    2.13 -val beta_tac = simp_tac beta_ss
    2.14 +val beta_ss =
    2.15 +  HOL_basic_ss addsimps simp_thms addsimprocs [@{simproc beta_cfun_proc}]
    2.16  
    2.17  (******************************************************************************)
    2.18  (******************************** theory data *********************************)