# HG changeset patch # User bulwahn # Date 1328173931 -3600 # Node ID f56be74d7f51d8b3a51dc99c4e6425f6a57414f2 # Parent 68f973ffd763141bd52e4303ad4af3665aea95b4 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type diff -r 68f973ffd763 -r f56be74d7f51 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Feb 01 15:28:02 2012 +0100 +++ b/src/HOL/IsaMakefile Thu Feb 02 10:12:11 2012 +0100 @@ -1051,10 +1051,10 @@ ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \ ex/Coercion_Examples.thy ex/Coherent.thy \ ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \ - ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \ - ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ - ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ - ex/Iff_Oracle.thy ex/Induction_Schema.thy \ + ex/Eval_Examples.thy ex/Executable_Relation.thy ex/Fundefs.thy \ + ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ + ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ + ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \ ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy \ ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy \ ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy \ diff -r 68f973ffd763 -r f56be74d7f51 src/HOL/ex/Executable_Relation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Executable_Relation.thy Thu Feb 02 10:12:11 2012 +0100 @@ -0,0 +1,79 @@ +theory Executable_Relation +imports Main +begin + +text {* + Current problem: rtrancl is not executable on an infinite type. +*} + +lemma + "(x, (y :: nat)) : rtrancl (R Un S) \ (x, y) : (rtrancl R) Un (rtrancl S)" +(* quickcheck[exhaustive] fails ! *) +oops + +code_thms rtrancl + +hide_const (open) rtrancl trancl + +quotient_type 'a rel = "('a * 'a) set" / "(op =)" +morphisms set_of_rel rel_of_set by (metis identity_equivp) + +lemma [simp]: + "rel_of_set (set_of_rel S) = S" +by (rule Quotient_abs_rep[OF Quotient_rel]) + +lemma [simp]: + "set_of_rel (rel_of_set R) = R" +by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl) + +no_notation + Set.member ("(_/ : _)" [50, 51] 50) + +quotient_definition member :: "'a * 'a => 'a rel => bool" where + "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" + +notation + member ("(_/ : _)" [50, 51] 50) + +quotient_definition union :: "'a rel => 'a rel => 'a rel" where + "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" + +quotient_definition rtrancl :: "'a rel => 'a rel" where + "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" + +definition reflcl_raw +where "reflcl_raw R = R \ Id" + +quotient_definition reflcl :: "('a * 'a) set => 'a rel" where + "reflcl" is "reflcl_raw :: ('a * 'a) set => ('a * 'a) set" + +code_datatype reflcl rel_of_set + +lemma member_code[code]: + "(x, y) : rel_of_set R = Set.member (x, y) R" + "(x, y) : reflcl R = ((x = y) \ Set.member (x, y) R)" +unfolding member_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def +by auto + +lemma union_code[code]: + "union (rel_of_set R) (rel_of_set S) = rel_of_set (Set.union R S)" + "union (reflcl R) (rel_of_set S) = reflcl (Set.union R S)" + "union (reflcl R) (reflcl S) = reflcl (Set.union R S)" + "union (rel_of_set R) (reflcl S) = reflcl (Set.union R S)" +unfolding union_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def +by (auto intro: arg_cong[where f=rel_of_set]) + +lemma rtrancl_code[code]: + "rtrancl (rel_of_set R) = reflcl (Transitive_Closure.trancl R)" + "rtrancl (reflcl R) = reflcl (Transitive_Closure.trancl R)" +unfolding rtrancl_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def +by (auto intro: arg_cong[where f=rel_of_set]) + +quickcheck_generator rel constructors: rel_of_set + +lemma + "(x, (y :: nat)) : rtrancl (union R S) \ (x, y) : (union (rtrancl R) (rtrancl S))" +quickcheck[exhaustive] +oops + +end diff -r 68f973ffd763 -r f56be74d7f51 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Feb 01 15:28:02 2012 +0100 +++ b/src/HOL/ex/ROOT.ML Thu Feb 02 10:12:11 2012 +0100 @@ -72,7 +72,8 @@ "List_to_Set_Comprehension_Examples", "Set_Algebras", "Seq", - "Simproc_Tests" + "Simproc_Tests", + "Executable_Relation" ]; if getenv "ISABELLE_GHC" = "" then ()