adding code equation for rtranclp in Enum
authorbulwahn
Mon Jan 30 13:55:22 2012 +0100 (2012-01-30)
changeset 463599bc43dc49d0a
parent 46358 b2a936486685
child 46360 5cb81e3fa799
adding code equation for rtranclp in Enum
src/HOL/Enum.thy
src/HOL/Library/Transitive_Closure_Table.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Jan 30 13:55:21 2012 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Jan 30 13:55:22 2012 +0100
     1.3 @@ -791,6 +791,10 @@
     1.4    "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
     1.5  by (simp add: trancl_def)
     1.6  
     1.7 +lemma rtranclp_rtrancl_eq[code, no_atp]:
     1.8 +  "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
     1.9 +unfolding rtrancl_def by auto
    1.10 +
    1.11  lemma max_ext_eq[code]:
    1.12    "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
    1.13  by (auto simp add: max_ext.simps)
     2.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Jan 30 13:55:21 2012 +0100
     2.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Mon Jan 30 13:55:22 2012 +0100
     2.3 @@ -185,6 +185,7 @@
     2.4      by (auto simp add: rtranclp_eq_rtrancl_path)
     2.5  qed
     2.6  
     2.7 +declare rtranclp_rtrancl_eq[code del]
     2.8  declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
     2.9  
    2.10  code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
    2.11 @@ -214,5 +215,4 @@
    2.12  hide_type ty
    2.13  hide_const test A B C
    2.14  
    2.15 -end
    2.16 -
    2.17 +end
    2.18 \ No newline at end of file