src/HOL/Predicate_Compile.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 69605 a96320074298
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset
     1
(*  Title:      HOL/Predicate_Compile.thy
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset
     2
    Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset
     3
*)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     5
section \<open>A compiler for predicates defined by introduction rules\<close>
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     6
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     7
theory Predicate_Compile
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50055
diff changeset
     8
imports Random_Sequence Quickcheck_Exhaustive
63432
wenzelm
parents: 62390
diff changeset
     9
keywords
wenzelm
parents: 62390
diff changeset
    10
  "code_pred" :: thy_goal and
wenzelm
parents: 62390
diff changeset
    11
  "values" :: diag
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    12
begin
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    13
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    14
ML_file \<open>Tools/Predicate_Compile/predicate_compile_aux.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    15
ML_file \<open>Tools/Predicate_Compile/predicate_compile_compilations.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    16
ML_file \<open>Tools/Predicate_Compile/core_data.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    17
ML_file \<open>Tools/Predicate_Compile/mode_inference.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    18
ML_file \<open>Tools/Predicate_Compile/predicate_compile_proof.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    19
ML_file \<open>Tools/Predicate_Compile/predicate_compile_core.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    20
ML_file \<open>Tools/Predicate_Compile/predicate_compile_data.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    21
ML_file \<open>Tools/Predicate_Compile/predicate_compile_fun.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    22
ML_file \<open>Tools/Predicate_Compile/predicate_compile_pred.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    23
ML_file \<open>Tools/Predicate_Compile/predicate_compile_specialisation.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    24
ML_file \<open>Tools/Predicate_Compile/predicate_compile.ML\<close>
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46950
diff changeset
    25
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    26
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    27
subsection \<open>Set membership as a generator predicate\<close>
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    28
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    29
text \<open>
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    30
  Introduce a new constant for membership to allow 
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    31
  fine-grained control in code equations. 
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    32
\<close>
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    33
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    34
definition contains :: "'a set => 'a => bool"
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63432
diff changeset
    35
where "contains A x \<longleftrightarrow> x \<in> A"
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    36
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    37
definition contains_pred :: "'a set => 'a => unit Predicate.pred"
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63432
diff changeset
    38
where "contains_pred A x = (if x \<in> A then Predicate.single () else bot)"
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    39
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    40
lemma pred_of_setE:
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    41
  assumes "Predicate.eval (pred_of_set A) x"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    42
  obtains "contains A x"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    43
using assms by(simp add: contains_def)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    44
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    45
lemma pred_of_setI: "contains A x ==> Predicate.eval (pred_of_set A) x"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    46
by(simp add: contains_def)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    47
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    48
lemma pred_of_set_eq: "pred_of_set \<equiv> \<lambda>A. Predicate.Pred (contains A)"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    49
by(simp add: contains_def[abs_def] pred_of_set_def o_def)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    50
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    51
lemma containsI: "x \<in> A ==> contains A x" 
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    52
by(simp add: contains_def)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    53
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    54
lemma containsE: assumes "contains A x"
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 63432
diff changeset
    55
  obtains A' x' where "A = A'" "x = x'" "x \<in> A"
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    56
using assms by(simp add: contains_def)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    57
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    58
lemma contains_predI: "contains A x ==> Predicate.eval (contains_pred A x) ()"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    59
by(simp add: contains_pred_def contains_def)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    60
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    61
lemma contains_predE: 
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    62
  assumes "Predicate.eval (contains_pred A x) y"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    63
  obtains "contains A x"
62390
842917225d56 more canonical names
nipkow
parents: 60758
diff changeset
    64
using assms by(simp add: contains_pred_def contains_def split: if_split_asm)
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    65
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    66
lemma contains_pred_eq: "contains_pred \<equiv> \<lambda>A x. Predicate.Pred (\<lambda>y. contains A x)"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    67
by(rule eq_reflection)(auto simp add: contains_pred_def fun_eq_iff contains_def intro: pred_eqI)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    68
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    69
lemma contains_pred_notI:
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    70
   "\<not> contains A x ==> Predicate.eval (Predicate.not_pred (contains_pred A x)) ()"
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    71
by(simp add: contains_pred_def contains_def not_pred_eq)
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    72
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    73
setup \<open>
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    74
let
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    75
  val Fun = Predicate_Compile_Aux.Fun
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    76
  val Input = Predicate_Compile_Aux.Input
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    77
  val Output = Predicate_Compile_Aux.Output
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    78
  val Bool = Predicate_Compile_Aux.Bool
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    79
  val io = Fun (Input, Fun (Output, Bool))
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    80
  val ii = Fun (Input, Fun (Input, Bool))
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    81
in
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    82
  Core_Data.PredData.map (Graph.new_node 
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67613
diff changeset
    83
    (\<^const_name>\<open>contains\<close>, 
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    84
     Core_Data.PredData {
55543
f0ef75c6c0d8 more informative error;
wenzelm
parents: 52023
diff changeset
    85
       pos = Position.thread_data (),
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    86
       intros = [(NONE, @{thm containsI})], 
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    87
       elim = SOME @{thm containsE}, 
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    88
       preprocessed = true,
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    89
       function_names = [(Predicate_Compile_Aux.Pred, 
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67613
diff changeset
    90
         [(io, \<^const_name>\<open>pred_of_set\<close>), (ii, \<^const_name>\<open>contains_pred\<close>)])], 
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    91
       predfun_data = [
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    92
         (io, Core_Data.PredfunData {
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    93
            elim = @{thm pred_of_setE}, intro = @{thm pred_of_setI},
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    94
            neg_intro = NONE, definition = @{thm pred_of_set_eq}
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    95
          }),
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    96
         (ii, Core_Data.PredfunData {
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    97
            elim = @{thm contains_predE}, intro = @{thm contains_predI}, 
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    98
            neg_intro = SOME @{thm contains_pred_notI}, definition = @{thm contains_pred_eq}
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
    99
          })],
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
   100
       needs_random = []}))
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 33265
diff changeset
   101
end
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   102
\<close>
52023
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
   103
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
   104
hide_const (open) contains contains_pred
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
   105
hide_fact (open) pred_of_setE pred_of_setI pred_of_set_eq 
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
   106
  containsI containsE contains_predI contains_predE contains_pred_eq contains_pred_notI
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
   107
b477be38a7bb setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents: 51126
diff changeset
   108
end