1.1 --- a/src/HOL/IsaMakefile	Wed Feb 01 15:28:02 2012 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Feb 02 10:12:11 2012 +0100
     1.3 @@ -1051,10 +1051,10 @@
     1.4    ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy			\
     1.5    ex/Coercion_Examples.thy ex/Coherent.thy				\
     1.6    ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy			\
     1.7 -  ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy		\
     1.8 -  ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
     1.9 -  ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
    1.10 -  ex/Iff_Oracle.thy ex/Induction_Schema.thy				\
    1.11 +  ex/Eval_Examples.thy ex/Executable_Relation.thy ex/Fundefs.thy	\
    1.12 +  ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
    1.13 +  ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy 		\
    1.14 +  ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy	\
    1.15    ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy			\
    1.16    ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy		\
    1.17    ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy	\

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Executable_Relation.thy	Thu Feb 02 10:12:11 2012 +0100
     2.3 @@ -0,0 +1,79 @@
     2.4 +theory Executable_Relation
     2.5 +imports Main
     2.6 +begin
     2.7 +
     2.8 +text {*
     2.9 + Current problem: rtrancl is not executable on an infinite type. 
    2.10 +*}
    2.11 +
    2.12 +lemma
    2.13 +  "(x, (y :: nat)) : rtrancl (R Un S) \<Longrightarrow> (x, y) : (rtrancl R) Un (rtrancl S)"
    2.14 +(* quickcheck[exhaustive] fails ! *)
    2.15 +oops
    2.16 +
    2.17 +code_thms rtrancl
    2.18 +
    2.19 +hide_const (open) rtrancl trancl
    2.20 +
    2.21 +quotient_type 'a rel = "('a * 'a) set" / "(op =)"
    2.22 +morphisms set_of_rel rel_of_set by (metis identity_equivp)
    2.23 +
    2.24 +lemma [simp]:
    2.25 +  "rel_of_set (set_of_rel S) = S"
    2.26 +by (rule Quotient_abs_rep[OF Quotient_rel])
    2.27 +
    2.28 +lemma [simp]:
    2.29 +  "set_of_rel (rel_of_set R) = R"
    2.30 +by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)
    2.31 +
    2.32 +no_notation
    2.33 +   Set.member ("(_/ : _)" [50, 51] 50)
    2.34 +
    2.35 +quotient_definition member :: "'a * 'a => 'a rel => bool" where
    2.36 +  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"
    2.37 +
    2.38 +notation
    2.39 +   member  ("(_/ : _)" [50, 51] 50)
    2.40 +
    2.41 +quotient_definition union :: "'a rel => 'a rel => 'a rel" where
    2.42 +  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
    2.43 +
    2.44 +quotient_definition rtrancl :: "'a rel => 'a rel" where
    2.45 +  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" 
    2.46 +
    2.47 +definition reflcl_raw 
    2.48 +where "reflcl_raw R = R \<union> Id"
    2.49 +
    2.50 +quotient_definition reflcl :: "('a * 'a) set => 'a rel" where
    2.51 +  "reflcl" is "reflcl_raw :: ('a * 'a) set => ('a * 'a) set"
    2.52 +
    2.53 +code_datatype reflcl rel_of_set
    2.54 +
    2.55 +lemma member_code[code]:
    2.56 +  "(x, y) : rel_of_set R = Set.member (x, y) R"
    2.57 +  "(x, y) : reflcl R = ((x = y) \<or> Set.member (x, y) R)"
    2.58 +unfolding member_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def
    2.59 +by auto
    2.60 +
    2.61 +lemma union_code[code]:
    2.62 +  "union (rel_of_set R) (rel_of_set S) = rel_of_set (Set.union R S)"
    2.63 +  "union (reflcl R) (rel_of_set S) = reflcl (Set.union R S)"
    2.64 +  "union (reflcl R) (reflcl S) = reflcl (Set.union R S)"
    2.65 +  "union (rel_of_set R) (reflcl S) = reflcl (Set.union R S)"
    2.66 +unfolding union_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def
    2.67 +by (auto intro: arg_cong[where f=rel_of_set])
    2.68 +
    2.69 +lemma rtrancl_code[code]:
    2.70 +  "rtrancl (rel_of_set R) = reflcl (Transitive_Closure.trancl R)"
    2.71 +  "rtrancl (reflcl R) = reflcl (Transitive_Closure.trancl R)"
    2.72 +unfolding rtrancl_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def
    2.73 +by (auto intro: arg_cong[where f=rel_of_set])
    2.74 +
    2.75 +quickcheck_generator rel constructors: rel_of_set
    2.76 +
    2.77 +lemma
    2.78 +  "(x, (y :: nat)) : rtrancl (union R S) \<Longrightarrow> (x, y) : (union (rtrancl R) (rtrancl S))"
    2.79 +quickcheck[exhaustive]
    2.80 +oops
    2.81 +
    2.82 +end

     3.1 --- a/src/HOL/ex/ROOT.ML	Wed Feb 01 15:28:02 2012 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Thu Feb 02 10:12:11 2012 +0100
     3.3 @@ -72,7 +72,8 @@
     3.4    "List_to_Set_Comprehension_Examples",
     3.5    "Set_Algebras",
     3.6    "Seq",
     3.7 -  "Simproc_Tests"
     3.8 +  "Simproc_Tests",
     3.9 +  "Executable_Relation"
    3.10  ];
    3.11  
    3.12  if getenv "ISABELLE_GHC" = "" then ()