--- a/src/HOL/Nat_Transfer.thy Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Nat_Transfer.thy Mon Mar 08 09:38:58 2010 +0100
@@ -10,8 +10,12 @@
subsection {* Generic transfer machinery *}
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
- where "TransferMorphism a B \<longleftrightarrow> True"
+definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+ where "transfer_morphism f A \<longleftrightarrow> True"
+
+lemma transfer_morphismI:
+ "transfer_morphism f A"
+ by (simp add: transfer_morphism_def)
use "Tools/transfer.ML"
@@ -22,10 +26,10 @@
text {* set up transfer direction *}
-lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
- by (simp add: TransferMorphism_def)
+lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
+ by (simp add: transfer_morphism_def)
-declare TransferMorphism_nat_int [transfer
+declare transfer_morphism_nat_int [transfer
add mode: manual
return: nat_0_le
labels: natint
@@ -80,7 +84,7 @@
(nat (x::int) dvd nat y) = (x dvd y)"
by (auto simp add: zdvd_int)
-declare TransferMorphism_nat_int [transfer add return:
+declare transfer_morphism_nat_int [transfer add return:
transfer_nat_int_numerals
transfer_nat_int_functions
transfer_nat_int_function_closures
@@ -118,7 +122,7 @@
(EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
by auto
-declare TransferMorphism_nat_int [transfer add
+declare transfer_morphism_nat_int [transfer add
return: transfer_nat_int_quantifiers
cong: all_cong ex_cong]
@@ -129,7 +133,7 @@
nat (if P then x else y)"
by auto
-declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
+declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
text {* operations with sets *}
@@ -190,7 +194,7 @@
{(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
by auto
-declare TransferMorphism_nat_int [transfer add
+declare transfer_morphism_nat_int [transfer add
return: transfer_nat_int_set_functions
transfer_nat_int_set_function_closures
transfer_nat_int_set_relations
@@ -262,7 +266,7 @@
apply (subst setprod_cong, assumption, auto)
done
-declare TransferMorphism_nat_int [transfer add
+declare transfer_morphism_nat_int [transfer add
return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
transfer_nat_int_sum_prod_closure
cong: transfer_nat_int_sum_prod_cong]
@@ -272,10 +276,10 @@
text {* set up transfer direction *}
-lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
- by (simp add: TransferMorphism_def)
+lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
+ by (simp add: transfer_morphism_def)
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
mode: manual
(* labels: int-nat *)
return: nat_int
@@ -326,7 +330,7 @@
"(int x dvd int y) = (x dvd y)"
by (auto simp add: zdvd_int)
-declare TransferMorphism_int_nat [transfer add return:
+declare transfer_morphism_int_nat [transfer add return:
transfer_int_nat_numerals
transfer_int_nat_functions
transfer_int_nat_function_closures
@@ -346,7 +350,7 @@
apply auto
done
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
return: transfer_int_nat_quantifiers]
@@ -356,7 +360,7 @@
int (if P then x else y)"
by auto
-declare TransferMorphism_int_nat [transfer add return: int_if_cong]
+declare transfer_morphism_int_nat [transfer add return: int_if_cong]
@@ -401,7 +405,7 @@
{(x::nat). P x} = {x. P' x}"
by auto
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
return: transfer_int_nat_set_functions
transfer_int_nat_set_function_closures
transfer_int_nat_set_relations
@@ -433,7 +437,7 @@
apply (subst int_setprod, auto simp add: cong: setprod_cong)
done
-declare TransferMorphism_int_nat [transfer add
+declare transfer_morphism_int_nat [transfer add
return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
cong: setsum_cong setprod_cong]