src/HOL/Predicate_Compile.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 63432 ba7901e94e7b
child 67613 ce654b0e6d69
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@33265
     1
(*  Title:      HOL/Predicate_Compile.thy
wenzelm@33265
     2
    Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
wenzelm@33265
     3
*)
bulwahn@33250
     4
wenzelm@60758
     5
section \<open>A compiler for predicates defined by introduction rules\<close>
bulwahn@33250
     6
bulwahn@33250
     7
theory Predicate_Compile
haftmann@51126
     8
imports Random_Sequence Quickcheck_Exhaustive
wenzelm@63432
     9
keywords
wenzelm@63432
    10
  "code_pred" :: thy_goal and
wenzelm@63432
    11
  "values" :: diag
bulwahn@33250
    12
begin
bulwahn@33250
    13
wenzelm@48891
    14
ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"
wenzelm@48891
    15
ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML"
wenzelm@48891
    16
ML_file "Tools/Predicate_Compile/core_data.ML"
wenzelm@48891
    17
ML_file "Tools/Predicate_Compile/mode_inference.ML"
wenzelm@48891
    18
ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML"
wenzelm@48891
    19
ML_file "Tools/Predicate_Compile/predicate_compile_core.ML"
wenzelm@48891
    20
ML_file "Tools/Predicate_Compile/predicate_compile_data.ML"
wenzelm@48891
    21
ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML"
wenzelm@48891
    22
ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML"
wenzelm@48891
    23
ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
wenzelm@48891
    24
ML_file "Tools/Predicate_Compile/predicate_compile.ML"
wenzelm@48891
    25
bulwahn@33250
    26
wenzelm@60758
    27
subsection \<open>Set membership as a generator predicate\<close>
Andreas@52023
    28
wenzelm@60758
    29
text \<open>
Andreas@52023
    30
  Introduce a new constant for membership to allow 
Andreas@52023
    31
  fine-grained control in code equations. 
wenzelm@60758
    32
\<close>
Andreas@52023
    33
Andreas@52023
    34
definition contains :: "'a set => 'a => bool"
Andreas@52023
    35
where "contains A x \<longleftrightarrow> x : A"
Andreas@52023
    36
Andreas@52023
    37
definition contains_pred :: "'a set => 'a => unit Predicate.pred"
Andreas@52023
    38
where "contains_pred A x = (if x : A then Predicate.single () else bot)"
Andreas@52023
    39
Andreas@52023
    40
lemma pred_of_setE:
Andreas@52023
    41
  assumes "Predicate.eval (pred_of_set A) x"
Andreas@52023
    42
  obtains "contains A x"
Andreas@52023
    43
using assms by(simp add: contains_def)
Andreas@52023
    44
Andreas@52023
    45
lemma pred_of_setI: "contains A x ==> Predicate.eval (pred_of_set A) x"
Andreas@52023
    46
by(simp add: contains_def)
Andreas@52023
    47
Andreas@52023
    48
lemma pred_of_set_eq: "pred_of_set \<equiv> \<lambda>A. Predicate.Pred (contains A)"
Andreas@52023
    49
by(simp add: contains_def[abs_def] pred_of_set_def o_def)
Andreas@52023
    50
Andreas@52023
    51
lemma containsI: "x \<in> A ==> contains A x" 
Andreas@52023
    52
by(simp add: contains_def)
Andreas@52023
    53
Andreas@52023
    54
lemma containsE: assumes "contains A x"
Andreas@52023
    55
  obtains A' x' where "A = A'" "x = x'" "x : A"
Andreas@52023
    56
using assms by(simp add: contains_def)
Andreas@52023
    57
Andreas@52023
    58
lemma contains_predI: "contains A x ==> Predicate.eval (contains_pred A x) ()"
Andreas@52023
    59
by(simp add: contains_pred_def contains_def)
Andreas@52023
    60
Andreas@52023
    61
lemma contains_predE: 
Andreas@52023
    62
  assumes "Predicate.eval (contains_pred A x) y"
Andreas@52023
    63
  obtains "contains A x"
nipkow@62390
    64
using assms by(simp add: contains_pred_def contains_def split: if_split_asm)
Andreas@52023
    65
Andreas@52023
    66
lemma contains_pred_eq: "contains_pred \<equiv> \<lambda>A x. Predicate.Pred (\<lambda>y. contains A x)"
Andreas@52023
    67
by(rule eq_reflection)(auto simp add: contains_pred_def fun_eq_iff contains_def intro: pred_eqI)
Andreas@52023
    68
Andreas@52023
    69
lemma contains_pred_notI:
Andreas@52023
    70
   "\<not> contains A x ==> Predicate.eval (Predicate.not_pred (contains_pred A x)) ()"
Andreas@52023
    71
by(simp add: contains_pred_def contains_def not_pred_eq)
Andreas@52023
    72
wenzelm@60758
    73
setup \<open>
Andreas@52023
    74
let
Andreas@52023
    75
  val Fun = Predicate_Compile_Aux.Fun
Andreas@52023
    76
  val Input = Predicate_Compile_Aux.Input
Andreas@52023
    77
  val Output = Predicate_Compile_Aux.Output
Andreas@52023
    78
  val Bool = Predicate_Compile_Aux.Bool
Andreas@52023
    79
  val io = Fun (Input, Fun (Output, Bool))
Andreas@52023
    80
  val ii = Fun (Input, Fun (Input, Bool))
Andreas@52023
    81
in
Andreas@52023
    82
  Core_Data.PredData.map (Graph.new_node 
Andreas@52023
    83
    (@{const_name contains}, 
Andreas@52023
    84
     Core_Data.PredData {
wenzelm@55543
    85
       pos = Position.thread_data (),
Andreas@52023
    86
       intros = [(NONE, @{thm containsI})], 
Andreas@52023
    87
       elim = SOME @{thm containsE}, 
Andreas@52023
    88
       preprocessed = true,
Andreas@52023
    89
       function_names = [(Predicate_Compile_Aux.Pred, 
Andreas@52023
    90
         [(io, @{const_name pred_of_set}), (ii, @{const_name contains_pred})])], 
Andreas@52023
    91
       predfun_data = [
Andreas@52023
    92
         (io, Core_Data.PredfunData {
Andreas@52023
    93
            elim = @{thm pred_of_setE}, intro = @{thm pred_of_setI},
Andreas@52023
    94
            neg_intro = NONE, definition = @{thm pred_of_set_eq}
Andreas@52023
    95
          }),
Andreas@52023
    96
         (ii, Core_Data.PredfunData {
Andreas@52023
    97
            elim = @{thm contains_predE}, intro = @{thm contains_predI}, 
Andreas@52023
    98
            neg_intro = SOME @{thm contains_pred_notI}, definition = @{thm contains_pred_eq}
Andreas@52023
    99
          })],
Andreas@52023
   100
       needs_random = []}))
bulwahn@34948
   101
end
wenzelm@60758
   102
\<close>
Andreas@52023
   103
Andreas@52023
   104
hide_const (open) contains contains_pred
Andreas@52023
   105
hide_fact (open) pred_of_setE pred_of_setI pred_of_set_eq 
Andreas@52023
   106
  containsI containsE contains_predI contains_predE contains_pred_eq contains_pred_notI
Andreas@52023
   107
Andreas@52023
   108
end