src/HOL/ex/Predicate_Compile.thy
author haftmann
Sun, 08 Mar 2009 15:25:28 +0100
changeset 30374 7311a1546d85
child 30810 83642621425a
permissions -rw-r--r--
added predicate compiler, as formally checked prototype, not as user package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30374
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     1
theory Predicate_Compile
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     2
imports Complex_Main Lattice_Syntax
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     3
uses "predicate_compile.ML"
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     4
begin
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     5
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     6
setup {* Predicate_Compile.setup *}
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     7
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     8
primrec "next" :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
     9
  \<Rightarrow> 'a Predicate.seq \<Rightarrow> ('a \<times> 'a Predicate.pred) option" where
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    10
    "next yield Predicate.Empty = None"
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    11
  | "next yield (Predicate.Insert x P) = Some (x, P)"
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    12
  | "next yield (Predicate.Join P xq) = (case yield P
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    13
   of None \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    14
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    15
primrec pull :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    16
  \<Rightarrow> nat \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a list \<times> 'a Predicate.pred" where
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    17
    "pull yield 0 P = ([], \<bottom>)"
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    18
  | "pull yield (Suc n) P = (case yield P
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    19
      of None \<Rightarrow> ([], \<bottom>) | Some (x, Q) \<Rightarrow> let (xs, R) = pull yield n Q in (x # xs, R))"
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    20
7311a1546d85 added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff changeset
    21
end