# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261266815 -3600
# Node ID 37285ec4387d463cd0c0c9068cfdca6fa6889747
# Parent  df053507edba2fcf88973371357cc096868253d3
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file

diff -r df053507edba -r 37285ec4387d Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/FSet.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -26,17 +26,17 @@
   fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def
+quotient_definition
    "EMPTY :: 'a fset"
 as
   "[]::'a list"
 
-quotient_def
+quotient_definition
    "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 as
   "op #"
 
-quotient_def
+quotient_definition
    "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 as
   "op @"
@@ -47,7 +47,7 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
 
-quotient_def
+quotient_definition
    "CARD :: 'a fset \<Rightarrow> nat"
 as
   "card1"
@@ -110,17 +110,17 @@
   apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
   done
 
-quotient_def
+quotient_definition
    "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 as
   "op mem"
 
-quotient_def
+quotient_definition
    "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "fold1"
 
-quotient_def
+quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 as
   "map"
@@ -274,12 +274,12 @@
 quotient_type fset2 = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def
+quotient_definition
    "EMPTY2 :: 'a fset2"
 as
   "[]::'a list"
 
-quotient_def
+quotient_definition
    "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 as
   "op #"
@@ -292,12 +292,12 @@
 apply (lifting list_induct_part)
 done
 
-quotient_def
+quotient_definition
   "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "list_rec"
 
-quotient_def
+quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "list_case"
diff -r df053507edba -r 37285ec4387d Quot/Examples/FSet2.thy
--- a/Quot/Examples/FSet2.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/FSet2.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -24,12 +24,12 @@
 quotient_type fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def
+quotient_definition
   "fempty :: 'a fset" ("{||}")
 as
   "[]"
 
-quotient_def
+quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 as
   "(op #)"
@@ -38,7 +38,7 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
 by (auto intro: list_eq.intros)
 
-quotient_def
+quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
 as
   "(op @)"
@@ -65,7 +65,7 @@
   by (auto simp add: append_rsp_aux2)
 
 
-quotient_def
+quotient_definition
   "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
 as
   "(op mem)"
@@ -89,7 +89,7 @@
 where
   "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
 
-quotient_def
+quotient_definition
   "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
 as
   "inter_list"
diff -r df053507edba -r 37285ec4387d Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -209,15 +209,15 @@
 
 section {* Constants on the Quotient Type *} 
 
-quotient_def
+quotient_definition
   "fempty :: 'a fset" 
   as "[]::'a list"
 
-quotient_def
+quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
   as "op #"
 
-quotient_def
+quotient_definition
   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
   as "\<lambda>x X. x \<in> set X"
 
@@ -226,27 +226,27 @@
 where
   "a \<notin>f S \<equiv> \<not>(a \<in>f S)"
 
-quotient_def
+quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat" 
   as "card_raw"
 
-quotient_def
+quotient_definition
   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
   as "delete_raw"
 
-quotient_def
+quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50)
   as "op @"
 
-quotient_def
+quotient_definition
   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
   as "inter_raw"
 
-quotient_def
+quotient_definition
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 
   as "fold_raw"
 
-quotient_def
+quotient_definition
   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
   as "set"
 
@@ -304,7 +304,7 @@
 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 by (lifting append_assoc)
 
-quotient_def
+quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "list_case"
diff -r df053507edba -r 37285ec4387d Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -21,12 +21,12 @@
 print_theorems
 print_quotients
 
-quotient_def
+quotient_definition
   "ZERO :: my_int"
 as
   "(0::nat, 0::nat)"
 
-quotient_def
+quotient_definition
   "ONE :: my_int"
 as
   "(1::nat, 0::nat)"
@@ -36,7 +36,7 @@
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def
+quotient_definition
   "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 as
   "my_plus"
@@ -46,7 +46,7 @@
 where
   "my_neg (x, y) = (y, x)"
 
-quotient_def
+quotient_definition
   "NEG :: my_int \<Rightarrow> my_int"
 as
   "my_neg"
@@ -61,7 +61,7 @@
 where
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def
+quotient_definition
   "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 as
   "my_mult"
@@ -73,7 +73,7 @@
 where
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def
+quotient_definition
    "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
 as
   "my_le"
diff -r df053507edba -r 37285ec4387d Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -20,10 +20,10 @@
 
 ML {* @{term "0 \<Colon> int"} *}
 
-quotient_def
+quotient_definition
   "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)"
 
-quotient_def
+quotient_definition
   "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)"
 
 fun
@@ -31,7 +31,7 @@
 where
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def
+quotient_definition
   "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
 
 fun
@@ -39,7 +39,7 @@
 where
   "uminus_raw (x, y) = (y, x)"
 
-quotient_def
+quotient_definition
   "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw"
 
 definition
@@ -50,7 +50,7 @@
 where
   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def
+quotient_definition
   mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw"
 
 fun
@@ -58,7 +58,7 @@
 where
   "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def
+quotient_definition
   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw"
 
 definition
@@ -206,7 +206,7 @@
 definition int_of_nat_raw: 
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
-quotient_def
+quotient_definition
   "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
 
 lemma[quot_respect]: 
diff -r df053507edba -r 37285ec4387d Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LFex.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -81,48 +81,48 @@
     TRM = trm / atrm
   by (auto intro: alpha_equivps)
 
-quotient_def
+quotient_definition
    "TYP :: KIND"
 as
   "Type"
 
-quotient_def
+quotient_definition
    "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
 as
   "KPi"
 
-quotient_def
+quotient_definition
    "TCONST :: ident \<Rightarrow> TY"
 as
   "TConst"
 
-quotient_def
+quotient_definition
    "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
 as
   "TApp"
 
-quotient_def
+quotient_definition
    "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
 as
   "TPi"
 
 (* FIXME: does not work with CONST *)
-quotient_def
+quotient_definition
    "CONS :: ident \<Rightarrow> TRM"
 as
   "Const"
 
-quotient_def
+quotient_definition
    "VAR :: name \<Rightarrow> TRM"
 as
   "Var"
 
-quotient_def
+quotient_definition
    "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
 as
   "App"
 
-quotient_def
+quotient_definition
    "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
 as
   "Lam"
@@ -138,17 +138,17 @@
 thm LAM_def
 
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
-quotient_def
+quotient_definition
    "FV_kind :: KIND \<Rightarrow> name set"
 as
   "fv_kind"
 
-quotient_def
+quotient_definition
    "FV_ty :: TY \<Rightarrow> name set"
 as
   "fv_ty"
 
-quotient_def
+quotient_definition
    "FV_trm :: TRM \<Rightarrow> name set"
 as
   "fv_trm"
@@ -164,17 +164,17 @@
     perm_trm  \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"     (unchecked) 
 begin
 
-quotient_def
+quotient_definition
    "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
 as
   "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
 
-quotient_def
+quotient_definition
    "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
 as
   "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
 
-quotient_def
+quotient_definition
    "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
 as
   "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
diff -r df053507edba -r 37285ec4387d Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -56,17 +56,17 @@
 
 print_quotients
 
-quotient_def
+quotient_definition
    "Var :: name \<Rightarrow> lam"
 as
   "rVar"
 
-quotient_def
+quotient_definition
    "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
 as
   "rApp"
 
-quotient_def
+quotient_definition
    "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
 as
   "rLam"
@@ -75,7 +75,7 @@
 thm App_def
 thm Lam_def
 
-quotient_def
+quotient_definition
    "fv :: lam \<Rightarrow> name set"
 as
   "rfv"
@@ -88,7 +88,7 @@
   perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
 begin
 
-quotient_def
+quotient_definition
    "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
 as
   "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
diff -r df053507edba -r 37285ec4387d Quot/Examples/LarryDatatype.thy
--- a/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -126,22 +126,22 @@
 
 text{*The abstract message constructors*}
 
-quotient_def
+quotient_definition
   "Nonce :: nat \<Rightarrow> msg"
 as
   "NONCE"
 
-quotient_def
+quotient_definition
   "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
 as
   "MPAIR"
 
-quotient_def
+quotient_definition
   "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
 as
   "CRYPT"
 
-quotient_def
+quotient_definition
   "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
 as
   "DECRYPT"
@@ -163,7 +163,7 @@
 
 subsection{*The Abstract Function to Return the Set of Nonces*}
 
-quotient_def
+quotient_definition
    "nonces:: msg \<Rightarrow> nat set"
 as
   "freenonces"
@@ -199,7 +199,7 @@
 
 subsection{*The Abstract Function to Return the Left Part*}
 
-quotient_def
+quotient_definition
   "left:: msg \<Rightarrow> msg"
 as
   "freeleft"
@@ -226,7 +226,7 @@
 
 subsection{*The Abstract Function to Return the Right Part*}
 
-quotient_def
+quotient_definition
   "right:: msg \<Rightarrow> msg"
 as
   "freeright"
@@ -360,7 +360,7 @@
 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
 need this function in order to prove discrimination theorems.*}
 
-quotient_def
+quotient_definition
   "discrim:: msg \<Rightarrow> int"
 as
   "freediscrim"
diff -r df053507edba -r 37285ec4387d Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LarryInt.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -16,16 +16,16 @@
 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
 begin
 
-quotient_def 
+quotient_definition 
   Zero_int_def: "0::int" as "(0::nat, 0::nat)"
 
-quotient_def
+quotient_definition
   One_int_def: "1::int" as "(1::nat, 0::nat)"
 
 definition
   "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
 
-quotient_def
+quotient_definition
   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
 as 
   "add_raw"
@@ -33,7 +33,7 @@
 definition
   "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
 
-quotient_def
+quotient_definition
   "uminus :: int \<Rightarrow> int" 
 as 
   "uminus_raw"
@@ -43,7 +43,7 @@
 where
   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def
+quotient_definition
   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
 as 
   "mult_raw"
@@ -51,7 +51,7 @@
 definition
   "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
 
-quotient_def 
+quotient_definition 
   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
 as 
   "le_raw"
@@ -343,7 +343,7 @@
 definition
   "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
 
-quotient_def
+quotient_definition
   "nat2::int\<Rightarrow>nat"
 as
   "nat_raw"
diff -r df053507edba -r 37285ec4387d Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/quotient_def.ML	Sun Dec 20 00:53:35 2009 +0100
@@ -127,8 +127,9 @@
       (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
          OuterParse.term)
 
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
-  OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
+val _ = OuterSyntax.local_theory "quotient_definition" 
+	  "definition for constants over the quotient type"
+             OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 
 end; (* structure *)
 
diff -r df053507edba -r 37285ec4387d isar-keywords-quot.el
--- a/isar-keywords-quot.el	Sun Dec 20 00:26:53 2009 +0100
+++ b/isar-keywords-quot.el	Sun Dec 20 00:53:35 2009 +0100
@@ -193,7 +193,7 @@
     "quickcheck"
     "quickcheck_params"
     "quit"
-    "quotient_def"
+    "quotient_definition"
     "quotient_type"
     "realizability"
     "realizers"
@@ -477,7 +477,7 @@
     "print_ast_translation"
     "print_translation"
     "quickcheck_params"
-    "quotient_def"
+    "quotient_definition"
     "realizability"
     "realizers"
     "recdef"