try to detect assumptions of transfer rules that are in a shape of a transfer rule
authorkuncar
Mon May 13 12:13:24 2013 +0200 (2013-05-13)
changeset 5195504d9381bebff
parent 51954 2e3f9e72b8c4
child 51956 a4d81cdebf8b
try to detect assumptions of transfer rules that are in a shape of a transfer rule
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/transfer.ML	Mon May 13 12:13:24 2013 +0200
     1.2 +++ b/src/HOL/Tools/transfer.ML	Mon May 13 12:13:24 2013 +0200
     1.3 @@ -111,10 +111,25 @@
     1.4    in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
     1.5  
     1.6  (* Conversion to preprocess a transfer rule *)
     1.7 +fun strip_args n = funpow n (fst o dest_comb)
     1.8 +
     1.9 +fun safe_Rel_conv ct =
    1.10 +  let
    1.11 +    val head = ct |> term_of |> HOLogic.dest_Trueprop |> strip_args 2
    1.12 +    fun is_known (Const (s, _)) = (s = @{const_name DOM})
    1.13 +      | is_known _ = false
    1.14 +  in
    1.15 +    if not (is_known head)
    1.16 +      then HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) ct
    1.17 +    else Conv.all_conv ct
    1.18 +  end
    1.19 +  handle TERM _ => Conv.all_conv ct
    1.20 +;
    1.21 +
    1.22  fun prep_conv ct = (
    1.23 -      Conv.implies_conv Conv.all_conv prep_conv
    1.24 +      Conv.implies_conv safe_Rel_conv prep_conv
    1.25        else_conv
    1.26 -      HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
    1.27 +      safe_Rel_conv
    1.28        else_conv
    1.29        Conv.all_conv) ct
    1.30  
     2.1 --- a/src/HOL/Transfer.thy	Mon May 13 12:13:24 2013 +0200
     2.2 +++ b/src/HOL/Transfer.thy	Mon May 13 12:13:24 2013 +0200
     2.3 @@ -103,6 +103,10 @@
     2.4    shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
     2.5    using assms unfolding Rel_def fun_rel_def by fast
     2.6  
     2.7 +text {* Handling of domains *}
     2.8 +
     2.9 +definition DOM :: "('a => 'b => bool) => ('a => bool) => bool" where "DOM T R \<equiv> Domainp T = R"
    2.10 +
    2.11  ML_file "Tools/transfer.ML"
    2.12  setup Transfer.setup
    2.13