exposed approximation in ML
authoreberlm
Mon Mar 30 10:52:54 2015 +0200 (2015-03-30)
changeset 59850f339ff48a6ee
parent 59849 c3d126c7944f
child 59852 5fd0b3c8a355
child 59853 4039d8aecda4
exposed approximation in ML
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/approximation.ML
src/HOL/Decision_Procs/approximation_generator.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Mar 30 00:13:37 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Mar 30 10:52:54 2015 +0200
     1.3 @@ -3583,130 +3583,31 @@
     1.4  in Thm.global_cterm_of thy (Logic.mk_equals (t, normalize t)) end
     1.5  *}
     1.6  
     1.7 -ML {*
     1.8 -  fun reorder_bounds_tac prems i =
     1.9 -    let
    1.10 -      fun variable_of_bound (Const (@{const_name Trueprop}, _) $
    1.11 -                             (Const (@{const_name Set.member}, _) $
    1.12 -                              Free (name, _) $ _)) = name
    1.13 -        | variable_of_bound (Const (@{const_name Trueprop}, _) $
    1.14 -                             (Const (@{const_name HOL.eq}, _) $
    1.15 -                              Free (name, _) $ _)) = name
    1.16 -        | variable_of_bound t = raise TERM ("variable_of_bound", [t])
    1.17 -
    1.18 -      val variable_bounds
    1.19 -        = map (`(variable_of_bound o Thm.prop_of)) prems
    1.20 -
    1.21 -      fun add_deps (name, bnds)
    1.22 -        = Graph.add_deps_acyclic (name,
    1.23 -            remove (op =) name (Term.add_free_names (Thm.prop_of bnds) []))
    1.24 -
    1.25 -      val order = Graph.empty
    1.26 -                  |> fold Graph.new_node variable_bounds
    1.27 -                  |> fold add_deps variable_bounds
    1.28 -                  |> Graph.strong_conn |> map the_single |> rev
    1.29 -                  |> map_filter (AList.lookup (op =) variable_bounds)
    1.30 -
    1.31 -      fun prepend_prem th tac
    1.32 -        = tac THEN rtac (th RSN (2, @{thm mp})) i
    1.33 -    in
    1.34 -      fold prepend_prem order all_tac
    1.35 -    end
    1.36 -
    1.37 -  fun approximation_conv ctxt ct =
    1.38 -    approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
    1.39 -
    1.40 -  fun approximate ctxt t =
    1.41 -    approximation_oracle (Proof_Context.theory_of ctxt, t)
    1.42 -    |> Thm.prop_of |> Logic.dest_equals |> snd;
    1.43 -
    1.44 -  (* Should be in HOL.thy ? *)
    1.45 -  fun gen_eval_tac conv ctxt = CONVERSION
    1.46 -    (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
    1.47 -    THEN' rtac TrueI
    1.48 -
    1.49 -  val form_equations = @{thms interpret_form_equations};
    1.50 -
    1.51 -  fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
    1.52 -      fun lookup_splitting (Free (name, _))
    1.53 -        = case AList.lookup (op =) splitting name
    1.54 -          of SOME s => HOLogic.mk_number @{typ nat} s
    1.55 -           | NONE => @{term "0 :: nat"}
    1.56 -      val vs = nth (Thm.prems_of st) (i - 1)
    1.57 -               |> Logic.strip_imp_concl
    1.58 -               |> HOLogic.dest_Trueprop
    1.59 -               |> Term.strip_comb |> snd |> List.last
    1.60 -               |> HOLogic.dest_list
    1.61 -      val p = prec
    1.62 -              |> HOLogic.mk_number @{typ nat}
    1.63 -              |> Thm.cterm_of ctxt
    1.64 -    in case taylor
    1.65 -    of NONE => let
    1.66 -         val n = vs |> length
    1.67 -                 |> HOLogic.mk_number @{typ nat}
    1.68 -                 |> Thm.cterm_of ctxt
    1.69 -         val s = vs
    1.70 -                 |> map lookup_splitting
    1.71 -                 |> HOLogic.mk_list @{typ nat}
    1.72 -                 |> Thm.cterm_of ctxt
    1.73 -       in
    1.74 -         (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
    1.75 -                                     (@{cpat "?prec::nat"}, p),
    1.76 -                                     (@{cpat "?ss::nat list"}, s)])
    1.77 -              @{thm "approx_form"}) i
    1.78 -          THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
    1.79 -       end
    1.80 -
    1.81 -     | SOME t =>
    1.82 -       if length vs <> 1
    1.83 -       then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st]))
    1.84 -       else let
    1.85 -         val t = t
    1.86 -              |> HOLogic.mk_number @{typ nat}
    1.87 -              |> Thm.cterm_of ctxt
    1.88 -         val s = vs |> map lookup_splitting |> hd
    1.89 -              |> Thm.cterm_of ctxt
    1.90 -       in
    1.91 -         rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
    1.92 -                                     (@{cpat "?t::nat"}, t),
    1.93 -                                     (@{cpat "?prec::nat"}, p)])
    1.94 -              @{thm "approx_tse_form"}) i st
    1.95 -       end
    1.96 -    end
    1.97 -
    1.98 -  val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) =>
    1.99 -    error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
   1.100 -*}
   1.101 -
   1.102  lemma intervalE: "a \<le> x \<and> x \<le> b \<Longrightarrow> \<lbrakk> x \<in> { a .. b } \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   1.103    by auto
   1.104  
   1.105  lemma meta_eqE: "x \<equiv> a \<Longrightarrow> \<lbrakk> x = a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   1.106    by auto
   1.107  
   1.108 +ML_file "approximation.ML"
   1.109 +
   1.110  method_setup approximation = {*
   1.111 -  Scan.lift Parse.nat
   1.112 -  --
   1.113 -  Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
   1.114 -    |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) []
   1.115 -  --
   1.116 -  Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
   1.117 -    |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat))
   1.118 -  >>
   1.119 -  (fn ((prec, splitting), taylor) => fn ctxt =>
   1.120 -    SIMPLE_METHOD' (fn i =>
   1.121 -      REPEAT (FIRST' [etac @{thm intervalE},
   1.122 -                      etac @{thm meta_eqE},
   1.123 -                      rtac @{thm impI}] i)
   1.124 -      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
   1.125 -      THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
   1.126 -      THEN DETERM (Reification.tac ctxt form_equations NONE i)
   1.127 -      THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
   1.128 -      THEN gen_eval_tac (approximation_conv ctxt) ctxt i))
   1.129 +  let val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) =>
   1.130 +                   error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
   1.131 +  in
   1.132 +    Scan.lift Parse.nat
   1.133 +    --
   1.134 +    Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
   1.135 +      |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) []
   1.136 +    --
   1.137 +    Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
   1.138 +      |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat))
   1.139 +    >>
   1.140 +    (fn ((prec, splitting), taylor) => fn ctxt =>
   1.141 +      SIMPLE_METHOD' (Approximation.approximation_tac prec splitting taylor ctxt))
   1.142 +  end
   1.143  *} "real number approximation"
   1.144  
   1.145 -ML_file "approximation.ML"
   1.146 -
   1.147  
   1.148  section "Quickcheck Generator"
   1.149  
     2.1 --- a/src/HOL/Decision_Procs/approximation.ML	Mon Mar 30 00:13:37 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Mon Mar 30 10:52:54 2015 +0200
     2.3 @@ -5,11 +5,103 @@
     2.4  signature APPROXIMATION =
     2.5  sig
     2.6    val approx: int -> Proof.context -> term -> term
     2.7 +  val approximate: Proof.context -> term -> term
     2.8 +  val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic
     2.9  end
    2.10  
    2.11  structure Approximation: APPROXIMATION =
    2.12  struct
    2.13  
    2.14 +fun reorder_bounds_tac prems i =
    2.15 +  let
    2.16 +    fun variable_of_bound (Const (@{const_name Trueprop}, _) $
    2.17 +                           (Const (@{const_name Set.member}, _) $
    2.18 +                            Free (name, _) $ _)) = name
    2.19 +      | variable_of_bound (Const (@{const_name Trueprop}, _) $
    2.20 +                           (Const (@{const_name HOL.eq}, _) $
    2.21 +                            Free (name, _) $ _)) = name
    2.22 +      | variable_of_bound t = raise TERM ("variable_of_bound", [t])
    2.23 +
    2.24 +    val variable_bounds
    2.25 +      = map (`(variable_of_bound o Thm.prop_of)) prems
    2.26 +
    2.27 +    fun add_deps (name, bnds)
    2.28 +      = Graph.add_deps_acyclic (name,
    2.29 +          remove (op =) name (Term.add_free_names (Thm.prop_of bnds) []))
    2.30 +
    2.31 +    val order = Graph.empty
    2.32 +                |> fold Graph.new_node variable_bounds
    2.33 +                |> fold add_deps variable_bounds
    2.34 +                |> Graph.strong_conn |> map the_single |> rev
    2.35 +                |> map_filter (AList.lookup (op =) variable_bounds)
    2.36 +
    2.37 +    fun prepend_prem th tac
    2.38 +      = tac THEN rtac (th RSN (2, @{thm mp})) i
    2.39 +  in
    2.40 +    fold prepend_prem order all_tac
    2.41 +  end
    2.42 +
    2.43 +fun approximation_conv ctxt ct =
    2.44 +  approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
    2.45 +
    2.46 +fun approximate ctxt t =
    2.47 +  approximation_oracle (Proof_Context.theory_of ctxt, t)
    2.48 +  |> Thm.prop_of |> Logic.dest_equals |> snd;
    2.49 +
    2.50 +(* Should be in HOL.thy ? *)
    2.51 +fun gen_eval_tac conv ctxt = CONVERSION
    2.52 +  (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
    2.53 +  THEN' rtac TrueI
    2.54 +
    2.55 +val form_equations = @{thms interpret_form_equations};
    2.56 +
    2.57 +fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
    2.58 +    fun lookup_splitting (Free (name, _))
    2.59 +      = case AList.lookup (op =) splitting name
    2.60 +        of SOME s => HOLogic.mk_number @{typ nat} s
    2.61 +         | NONE => @{term "0 :: nat"}
    2.62 +    val vs = nth (Thm.prems_of st) (i - 1)
    2.63 +             |> Logic.strip_imp_concl
    2.64 +             |> HOLogic.dest_Trueprop
    2.65 +             |> Term.strip_comb |> snd |> List.last
    2.66 +             |> HOLogic.dest_list
    2.67 +    val p = prec
    2.68 +            |> HOLogic.mk_number @{typ nat}
    2.69 +            |> Thm.cterm_of ctxt
    2.70 +  in case taylor
    2.71 +  of NONE => let
    2.72 +       val n = vs |> length
    2.73 +               |> HOLogic.mk_number @{typ nat}
    2.74 +               |> Thm.cterm_of ctxt
    2.75 +       val s = vs
    2.76 +               |> map lookup_splitting
    2.77 +               |> HOLogic.mk_list @{typ nat}
    2.78 +               |> Thm.cterm_of ctxt
    2.79 +     in
    2.80 +       (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
    2.81 +                                   (@{cpat "?prec::nat"}, p),
    2.82 +                                   (@{cpat "?ss::nat list"}, s)])
    2.83 +            @{thm "approx_form"}) i
    2.84 +        THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
    2.85 +     end
    2.86 +
    2.87 +   | SOME t =>
    2.88 +     if length vs <> 1
    2.89 +     then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st]))
    2.90 +     else let
    2.91 +       val t = t
    2.92 +            |> HOLogic.mk_number @{typ nat}
    2.93 +            |> Thm.cterm_of ctxt
    2.94 +       val s = vs |> map lookup_splitting |> hd
    2.95 +            |> Thm.cterm_of ctxt
    2.96 +     in
    2.97 +       rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
    2.98 +                                   (@{cpat "?t::nat"}, t),
    2.99 +                                   (@{cpat "?prec::nat"}, p)])
   2.100 +            @{thm "approx_tse_form"}) i st
   2.101 +     end
   2.102 +  end
   2.103 +
   2.104  fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
   2.105    | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
   2.106    | calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
   2.107 @@ -156,4 +248,14 @@
   2.108      (opt_modes -- Parse.term
   2.109        >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
   2.110  
   2.111 -end;
   2.112 +fun approximation_tac prec splitting taylor ctxt i =
   2.113 +  REPEAT (FIRST' [etac @{thm intervalE},
   2.114 +                  etac @{thm meta_eqE},
   2.115 +                  rtac @{thm impI}] i)
   2.116 +  THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
   2.117 +  THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
   2.118 +  THEN DETERM (Reification.tac ctxt form_equations NONE i)
   2.119 +  THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
   2.120 +  THEN gen_eval_tac (approximation_conv ctxt) ctxt i
   2.121 +    
   2.122 +end;
   2.123 \ No newline at end of file
     3.1 --- a/src/HOL/Decision_Procs/approximation_generator.ML	Mon Mar 30 00:13:37 2015 +0200
     3.2 +++ b/src/HOL/Decision_Procs/approximation_generator.ML	Mon Mar 30 10:52:54 2015 +0200
     3.3 @@ -141,7 +141,7 @@
     3.4              #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
     3.5            frees
     3.6        in
     3.7 -        if approximate ctxt (mk_approx_form e ts) |> is_True
     3.8 +        if Approximation.approximate ctxt (mk_approx_form e ts) |> is_True
     3.9          then SOME (true, ts')
    3.10          else (if genuine_only then NONE else SOME (false, ts'))
    3.11        end
    3.12 @@ -161,6 +161,8 @@
    3.13      "\<not> \<not> q \<longleftrightarrow> q"
    3.14      by auto}
    3.15  
    3.16 +val form_equations = @{thms interpret_form_equations};
    3.17 +
    3.18  fun reify_goal ctxt t =
    3.19    HOLogic.mk_not t
    3.20      |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)