--- a/src/CCL/CCL.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/CCL.thy Wed Oct 03 21:29:05 2007 +0200
@@ -20,7 +20,7 @@
classes prog < "term"
defaultsort prog
-arities fun :: (prog, prog) prog
+arities "fun" :: (prog, prog) prog
typedecl i
arities i :: prog
@@ -28,10 +28,10 @@
consts
(*** Evaluation Judgement ***)
- "--->" :: "[i,i]=>prop" (infixl 20)
+ Eval :: "[i,i]=>prop" (infixl "--->" 20)
(*** Bisimulations for pre-order and equality ***)
- "[=" :: "['a,'a]=>o" (infixl 50)
+ po :: "['a,'a]=>o" (infixl "[=" 50)
SIM :: "[i,i,i set]=>o"
POgen :: "i set => i set"
EQgen :: "i set => i set"
@@ -44,7 +44,7 @@
pair :: "[i,i]=>i" ("(1<_,/_>)")
lambda :: "(i=>i)=>i" (binder "lam " 55)
"case" :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i"
- "`" :: "[i,i]=>i" (infixl 56)
+ "apply" :: "[i,i]=>i" (infixl "`" 56)
bot :: "i"
"fix" :: "(i=>i)=>i"
@@ -188,25 +188,19 @@
by simp
ML {*
- local
- val arg_cong = thm "arg_cong";
- val eq_lemma = thm "eq_lemma";
- val ss = simpset_of (the_context ());
- in
- fun mk_inj_rl thy rews s =
- let
- fun mk_inj_lemmas r = [arg_cong] RL [r RS (r RS eq_lemma)]
- val inj_lemmas = List.concat (map mk_inj_lemmas rews)
- val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE
- eresolve_tac inj_lemmas 1 ORELSE
- asm_simp_tac (Simplifier.theory_context thy ss addsimps rews) 1)
- in prove_goal thy s (fn _ => [tac]) end
- end
+ fun mk_inj_rl thy rews s =
+ let
+ fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
+ val inj_lemmas = List.concat (map mk_inj_lemmas rews)
+ val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE
+ eresolve_tac inj_lemmas 1 ORELSE
+ asm_simp_tac (Simplifier.theory_context thy @{simpset} addsimps rews) 1)
+ in prove_goal thy s (fn _ => [tac]) end
*}
ML {*
bind_thms ("ccl_injs",
- map (mk_inj_rl (the_context ()) (thms "caseBs"))
+ map (mk_inj_rl @{theory} @{thms caseBs})
["<a,b> = <a',b'> <-> (a=a' & b=b')",
"(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"])
*}
--- a/src/CCL/Fix.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Fix.thy Wed Oct 03 21:29:05 2007 +0200
@@ -14,10 +14,11 @@
idgen :: "[i]=>i"
INCL :: "[i=>o]=>o"
-axioms
+defs
idgen_def:
"idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
+axioms
INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
po_INCL: "INCL(%x. a(x) [= b(x))"
INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
--- a/src/CCL/Set.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Set.thy Wed Oct 03 21:29:05 2007 +0200
@@ -16,8 +16,8 @@
consts
Collect :: "['a => o] => 'a set" (*comprehension*)
Compl :: "('a set) => 'a set" (*complement*)
- Int :: "['a set, 'a set] => 'a set" (infixl 70)
- Un :: "['a set, 'a set] => 'a set" (infixl 65)
+ Int :: "['a set, 'a set] => 'a set" (infixl "Int" 70)
+ Un :: "['a set, 'a set] => 'a set" (infixl "Un" 65)
Union :: "(('a set)set) => 'a set" (*...of a set*)
Inter :: "(('a set)set) => 'a set" (*...of a set*)
UNION :: "['a set, 'a => 'b set] => 'b set" (*general*)
@@ -25,11 +25,10 @@
Ball :: "['a set, 'a => o] => o" (*bounded quants*)
Bex :: "['a set, 'a => o] => o" (*bounded quants*)
mono :: "['a set => 'b set] => o" (*monotonicity*)
- ":" :: "['a, 'a set] => o" (infixl 50) (*membership*)
- "<=" :: "['a set, 'a set] => o" (infixl 50)
+ mem :: "['a, 'a set] => o" (infixl ":" 50) (*membership*)
+ subset :: "['a set, 'a set] => o" (infixl "<=" 50)
singleton :: "'a => 'a set" ("{_}")
empty :: "'a set" ("{}")
- "oo" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) (*composition*)
syntax
"@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*)
--- a/src/CCL/Term.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Term.thy Wed Oct 03 21:29:05 2007 +0200
@@ -31,7 +31,7 @@
nrec :: "[i,i,[i,i]=>i]=>i"
nil :: "i" ("([])")
- "$" :: "[i,i]=>i" (infixr 80)
+ cons :: "[i,i]=>i" (infixr "$" 80)
lcase :: "[i,i,[i,i]=>i]=>i"
lrec :: "[i,i,[i,i,i]=>i]=>i"
@@ -288,7 +288,7 @@
ML_setup {*
bind_thms ("term_dstncts",
mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
- [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","op $"]]);
+ [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
*}
--- a/src/CCL/Trancl.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Trancl.thy Wed Oct 03 21:29:05 2007 +0200
@@ -15,11 +15,11 @@
id :: "i set"
rtrancl :: "i set => i set" ("(_^*)" [100] 100)
trancl :: "i set => i set" ("(_^+)" [100] 100)
- O :: "[i set,i set] => i set" (infixr 60)
+ relcomp :: "[i set,i set] => i set" (infixr "O" 60)
axioms
trans_def: "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
- comp_def: (*composition of relations*)
+ relcomp_def: (*composition of relations*)
"r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
id_def: (*the identity relation*)
"id == {p. EX x. p = <x,x>}"
@@ -57,14 +57,14 @@
subsection {* Composition of two relations *}
lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
- unfolding comp_def by blast
+ unfolding relcomp_def by blast
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
lemma compE:
"[| xz : r O s;
!!x y z. [| xz = <x,z>; <x,y>:s; <y,z>:r |] ==> P
|] ==> P"
- unfolding comp_def by blast
+ unfolding relcomp_def by blast
lemma compEpair:
"[| <a,c> : r O s;
--- a/src/CCL/Type.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Type.thy Wed Oct 03 21:29:05 2007 +0200
@@ -15,7 +15,7 @@
Subtype :: "['a set, 'a => o] => 'a set"
Bool :: "i set"
Unit :: "i set"
- "+" :: "[i set, i set] => i set" (infixr 55)
+ Plus :: "[i set, i set] => i set" (infixr "+" 55)
Pi :: "[i set, i => i set] => i set"
Sigma :: "[i set, i => i set] => i set"
Nat :: "i set"
--- a/src/CCL/Wfd.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/Wfd.thy Wed Oct 03 21:29:05 2007 +0200
@@ -16,11 +16,11 @@
(*** Relations ***)
wf :: "[i set] => i set"
wmap :: "[i=>i,i set] => i set"
- "**" :: "[i set,i set] => i set" (infixl 70)
+ lex :: "[i set,i set] => i set" (infixl "**" 70)
NatPR :: "i set"
ListPR :: "i set => i set"
-axioms
+defs
Wfd_def:
"Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
@@ -442,7 +442,7 @@
fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
| get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
| get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
- | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t
+ | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
| get_bno l n (t $ s) = get_bno l n t
| get_bno l n (Bound m) = (m-length(l),n)
@@ -463,7 +463,7 @@
fun is_rigid_prog t =
case (Logic.strip_assums_concl t) of
- (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = [])
+ (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = [])
| _ => false
in
--- a/src/CCL/ex/List.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/ex/List.thy Wed Oct 03 21:29:05 2007 +0200
@@ -12,9 +12,9 @@
consts
map :: "[i=>i,i]=>i"
- "o" :: "[i=>i,i=>i]=>i=>i" (infixr 55)
- "@" :: "[i,i]=>i" (infixr 55)
- mem :: "[i,i]=>i" (infixr 55)
+ comp :: "[i=>i,i=>i]=>i=>i" (infixr "o" 55)
+ append :: "[i,i]=>i" (infixr "@" 55)
+ member :: "[i,i]=>i" (infixr "mem" 55)
filter :: "[i,i]=>i"
flat :: "i=>i"
partition :: "[i,i]=>i"
@@ -27,7 +27,7 @@
map_def: "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
comp_def: "f o g == (%x. f(g(x)))"
append_def: "l @ m == lrec(l,m,%x xs g. x$g)"
- mem_def: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
+ member_def: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
filter_def: "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
flat_def: "flat(l) == lrec(l,[],%h t g. h @ g)"
--- a/src/CCL/ex/Nat.thy Wed Oct 03 19:49:33 2007 +0200
+++ b/src/CCL/ex/Nat.thy Wed Oct 03 21:29:05 2007 +0200
@@ -13,12 +13,12 @@
consts
not :: "i=>i"
- "#+" :: "[i,i]=>i" (infixr 60)
- "#*" :: "[i,i]=>i" (infixr 60)
- "#-" :: "[i,i]=>i" (infixr 60)
- "##" :: "[i,i]=>i" (infixr 60)
- "#<" :: "[i,i]=>i" (infixr 60)
- "#<=" :: "[i,i]=>i" (infixr 60)
+ add :: "[i,i]=>i" (infixr "#+" 60)
+ mult :: "[i,i]=>i" (infixr "#*" 60)
+ sub :: "[i,i]=>i" (infixr "#-" 60)
+ div :: "[i,i]=>i" (infixr "##" 60)
+ lt :: "[i,i]=>i" (infixr "#<" 60)
+ le :: "[i,i]=>i" (infixr "#<=" 60)
ackermann :: "[i,i]=>i"
defs