--- a/Quot/Examples/FSet.thy Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/FSet.thy Fri Dec 11 11:14:05 2009 +0100
@@ -27,18 +27,18 @@
done
quotient_def
- EMPTY :: "EMPTY :: 'a fset"
-where
+ "EMPTY :: 'a fset"
+as
"[]::'a list"
quotient_def
- INSERT :: "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+ "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
"op #"
quotient_def
- FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+ "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
"op @"
fun
@@ -48,8 +48,8 @@
| card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
quotient_def
- CARD :: "CARD :: 'a fset \<Rightarrow> nat"
-where
+ "CARD :: 'a fset \<Rightarrow> nat"
+as
"card1"
(* text {*
@@ -111,18 +111,18 @@
done
quotient_def
- IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-where
+ "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+as
"op mem"
quotient_def
- FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+ "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
"fold1"
quotient_def
- fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-where
+ "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+as
"map"
lemma mem_rsp:
@@ -275,13 +275,13 @@
by (rule equivp_list_eq)
quotient_def
- EMPTY2 :: "EMPTY2 :: 'a fset2"
-where
+ "EMPTY2 :: 'a fset2"
+as
"[]::'a list"
quotient_def
- INSERT2 :: "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
-where
+ "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+as
"op #"
lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
@@ -293,13 +293,13 @@
done
quotient_def
- fset_rec::"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+ "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
"list_rec"
quotient_def
- fset_case::"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+ "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
"list_case"
(* Probably not true without additional assumptions about the function *)
--- a/Quot/Examples/FSet2.thy Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/FSet2.thy Fri Dec 11 11:14:05 2009 +0100
@@ -24,23 +24,23 @@
quotient fset = "'a list" / "list_eq"
by (rule equivp_list_eq)
-quotient_def
- fempty :: "fempty :: 'a fset" ("{||}")
-where
+quotient_def
+ "fempty :: 'a fset" ("{||}")
+as
"[]"
-quotient_def
- finsert :: "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+quotient_def
+ "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
"(op #)"
lemma finsert_rsp[quot_respect]:
shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
by (auto intro: list_eq.intros)
-quotient_def
- funion :: "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
-where
+quotient_def
+ "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
+as
"(op @)"
lemma append_rsp_aux1:
@@ -65,9 +65,9 @@
by (auto simp add: append_rsp_aux2)
-quotient_def
- fmem :: " fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
-where
+quotient_def
+ "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+as
"(op mem)"
lemma memb_rsp_aux:
@@ -89,9 +89,9 @@
where
"inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
-quotient_def
- finter :: "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
-where
+quotient_def
+ "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+as
"inter_list"
no_syntax
--- a/Quot/Examples/IntEx.thy Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/IntEx.thy Fri Dec 11 11:14:05 2009 +0100
@@ -22,13 +22,13 @@
print_quotients
quotient_def
- ZERO::"zero :: my_int"
-where
+ "ZERO :: my_int"
+as
"(0::nat, 0::nat)"
quotient_def
- ONE::"one :: my_int"
-where
+ "ONE :: my_int"
+as
"(1::nat, 0::nat)"
fun
@@ -37,8 +37,8 @@
"my_plus (x, y) (u, v) = (x + u, y + v)"
quotient_def
- PLUS::"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
+ "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+as
"my_plus"
fun
@@ -47,8 +47,8 @@
"my_neg (x, y) = (y, x)"
quotient_def
- NEG::"NEG :: my_int \<Rightarrow> my_int"
-where
+ "NEG :: my_int \<Rightarrow> my_int"
+as
"my_neg"
definition
@@ -62,8 +62,8 @@
"my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
quotient_def
- MULT::"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
+ "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+as
"my_mult"
@@ -74,8 +74,8 @@
"my_le (x, y) (u, v) = (x+v \<le> u+y)"
quotient_def
- LE :: "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
-where
+ "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
+as
"my_le"
term LE
--- a/Quot/Examples/IntEx2.thy Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/IntEx2.thy Fri Dec 11 11:14:05 2009 +0100
@@ -18,15 +18,13 @@
instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
begin
-quotient_def
- zero_int::"0 :: int"
-where
- "(0::nat, 0::nat)"
+ML {* @{term "0 :: int"} *}
quotient_def
- one_int::"1 :: int"
-where
- "(1::nat, 0::nat)"
+ "0 :: int" as "(0::nat, 0::nat)"
+
+quotient_def
+ "1 :: int" as "(1::nat, 0::nat)"
fun
plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -34,9 +32,7 @@
"plus_raw (x, y) (u, v) = (x + u, y + v)"
quotient_def
- plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)"
-where
- "plus_raw"
+ "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
fun
uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -44,9 +40,7 @@
"uminus_raw (x, y) = (y, x)"
quotient_def
- uminus_int::"(uminus :: (int \<Rightarrow> int))"
-where
- "uminus_raw"
+ "(uminus :: (int \<Rightarrow> int))" as "uminus_raw"
definition
minus_int_def [code del]: "z - w = z + (-w::int)"
@@ -57,9 +51,7 @@
"times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
quotient_def
- times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)"
-where
- "times_raw"
+ "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "times_raw"
(* PROBLEM: this should be called le_int and le_raw / or odd *)
fun
@@ -68,9 +60,7 @@
"less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"
quotient_def
- less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
-where
- "less_eq_raw"
+ le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "less_eq_raw"
definition
less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -218,8 +208,7 @@
"int_of_nat_raw m = (m :: nat, 0 :: nat)"
quotient_def
- int_of_nat :: "int_of_nat :: nat \<Rightarrow> int"
-where "int_of_nat_raw"
+ "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
lemma[quot_respect]:
shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
--- a/Quot/Examples/LFex.thy Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/LFex.thy Fri Dec 11 11:14:05 2009 +0100
@@ -81,49 +81,49 @@
by (auto intro: alpha_equivps)
quotient_def
- TYP :: "TYP :: KIND"
-where
+ "TYP :: KIND"
+as
"Type"
quotient_def
- KPI :: "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
-where
+ "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
+as
"KPi"
quotient_def
- TCONST :: "TCONST :: ident \<Rightarrow> TY"
-where
+ "TCONST :: ident \<Rightarrow> TY"
+as
"TConst"
quotient_def
- TAPP :: "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
-where
+ "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
+as
"TApp"
quotient_def
- TPI :: "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
-where
+ "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
+as
"TPi"
(* FIXME: does not work with CONST *)
quotient_def
- CONS :: "CONS :: ident \<Rightarrow> TRM"
-where
+ "CONS :: ident \<Rightarrow> TRM"
+as
"Const"
quotient_def
- VAR :: "VAR :: name \<Rightarrow> TRM"
-where
+ "VAR :: name \<Rightarrow> TRM"
+as
"Var"
quotient_def
- APP :: "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+ "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
+as
"App"
quotient_def
- LAM :: "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+ "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
+as
"Lam"
thm TYP_def
@@ -138,18 +138,18 @@
(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
quotient_def
- FV_kind :: "FV_kind :: KIND \<Rightarrow> name set"
-where
+ "FV_kind :: KIND \<Rightarrow> name set"
+as
"fv_kind"
quotient_def
- FV_ty :: "FV_ty :: TY \<Rightarrow> name set"
-where
+ "FV_ty :: TY \<Rightarrow> name set"
+as
"fv_ty"
quotient_def
- FV_trm :: "FV_trm :: TRM \<Rightarrow> name set"
-where
+ "FV_trm :: TRM \<Rightarrow> name set"
+as
"fv_trm"
thm FV_kind_def
@@ -164,18 +164,18 @@
begin
quotient_def
- perm_kind :: "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
-where
+ "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
+as
"(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
quotient_def
- perm_ty :: "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
-where
+ "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
+as
"(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
quotient_def
- perm_trm :: "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+ "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+as
"(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
end
--- a/Quot/Examples/LamEx.thy Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/LamEx.thy Fri Dec 11 11:14:05 2009 +0100
@@ -57,18 +57,18 @@
print_quotients
quotient_def
- Var :: "Var :: name \<Rightarrow> lam"
-where
+ "Var :: name \<Rightarrow> lam"
+as
"rVar"
quotient_def
- App :: "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-where
+ "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
+as
"rApp"
quotient_def
- Lam :: "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-where
+ "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
+as
"rLam"
thm Var_def
@@ -76,8 +76,8 @@
thm Lam_def
quotient_def
- fv :: "fv :: lam \<Rightarrow> name set"
-where
+ "fv :: lam \<Rightarrow> name set"
+as
"rfv"
thm fv_def
@@ -89,18 +89,12 @@
begin
quotient_def
- perm_lam :: "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
-where
+ "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
+as
"perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
end
-(*quotient_def (for lam)
- abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
-where
- "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"*)
-
-
thm perm_lam_def
(* lemmas that need to lift *)
--- a/Quot/Examples/LarryDatatype.thy Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy Fri Dec 11 11:14:05 2009 +0100
@@ -128,23 +128,23 @@
text{*The abstract message constructors*}
quotient_def
- Nonce::"Nonce :: nat \<Rightarrow> msg"
-where
+ "Nonce :: nat \<Rightarrow> msg"
+as
"NONCE"
quotient_def
- MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-where
+ "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+as
"MPAIR"
quotient_def
- Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
+ "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+as
"CRYPT"
quotient_def
- Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
+ "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+as
"DECRYPT"
lemma [quot_respect]:
@@ -165,8 +165,8 @@
subsection{*The Abstract Function to Return the Set of Nonces*}
quotient_def
- nonces :: "nonces:: msg \<Rightarrow> nat set"
-where
+ "nonces:: msg \<Rightarrow> nat set"
+as
"freenonces"
text{*Now prove the four equations for @{term nonces}*}
@@ -201,8 +201,8 @@
subsection{*The Abstract Function to Return the Left Part*}
quotient_def
- left :: "left:: msg \<Rightarrow> msg"
-where
+ "left:: msg \<Rightarrow> msg"
+as
"freeleft"
lemma [quot_respect]:
@@ -228,8 +228,8 @@
subsection{*The Abstract Function to Return the Right Part*}
quotient_def
- right :: "right:: msg \<Rightarrow> msg"
-where
+ "right:: msg \<Rightarrow> msg"
+as
"freeright"
text{*Now prove the four equations for @{term right}*}
@@ -362,8 +362,8 @@
need this function in order to prove discrimination theorems.*}
quotient_def
- discrim :: "discrim:: msg \<Rightarrow> int"
-where
+ "discrim:: msg \<Rightarrow> int"
+as
"freediscrim"
text{*Now prove the four equations for @{term discrim}*}
--- a/Quot/quotient_def.ML Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/quotient_def.ML Fri Dec 11 11:14:05 2009 +0100
@@ -3,12 +3,9 @@
sig
datatype flag = absF | repF
val get_fun: flag -> Proof.context -> typ * typ -> term
- val make_def: binding -> mixfix -> Attrib.binding -> term -> term ->
+ val make_def: mixfix -> Attrib.binding -> term -> term ->
Proof.context -> (term * thm) * local_theory
-
- val quotdef: (binding * term * mixfix) * (Attrib.binding * term) ->
- local_theory -> (term * thm) * local_theory
- val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
+ val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
local_theory -> local_theory
end;
@@ -79,9 +76,11 @@
| (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
| _ => raise (LIFT_MATCH "get_fun")
-fun make_def qconst_bname mx attr lhs rhs lthy =
+fun make_def mx attr lhs rhs lthy =
let
- val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs
+ val Free (lhs_str, lhs_ty) = lhs;
+ val qconst_bname = Binding.name lhs_str;
+ val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
|> Syntax.check_term lthy
val prop = Logic.mk_equals (lhs, absrep_trm)
val (_, prop') = LocalDefs.cert_def lthy prop
@@ -91,12 +90,7 @@
fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
val lthy'' = Local_Theory.declaration true
- (fn phi =>
- let
- val qconst_str = Binding.name_of qconst_bname
- in
- qconsts_update_gen qconst_str (qcinfo phi)
- end) lthy'
+ (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
in
((trm, thm), lthy'')
end
@@ -111,22 +105,21 @@
(* - a meta-equation defining the constant, *)
(* and the attributes of for this meta-equality *)
-fun quotdef ((bind, lhs, mx), (attr, rhs)) lthy =
- make_def bind mx attr lhs rhs lthy
-
-fun quotdef_cmd ((bind, lhsstr, mx), (attr, rhsstr)) lthy =
+fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy =
let
val lhs = Syntax.read_term lthy lhsstr
val rhs = Syntax.read_term lthy rhsstr
in
- quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd
+ make_def mx attr lhs rhs lthy |> snd
end
+val _ = OuterKeyword.keyword "as";
+
val quotdef_parser =
- (OuterParse.binding --
- (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.term --
- OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
- (SpecParse.opt_thm_name ":" -- OuterParse.term)
+ (SpecParse.opt_thm_name ":" --
+ OuterParse.term) --
+ (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
+ OuterParse.term)
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
--- a/isar-keywords-prove.el Fri Dec 11 11:12:53 2009 +0100
+++ b/isar-keywords-prove.el Fri Dec 11 11:14:05 2009 +0100
@@ -257,6 +257,7 @@
(defconst isar-keywords-minor
'("advanced"
"and"
+ "as"
"assumes"
"attach"
"avoids"