# HG changeset patch # User wenzelm # Date 1191439745 -7200 # Node ID c4f13ab78f9df121ad2f03f9d5eef54b9e9a777e # Parent b7866aea0815bea2407200f54f1a5594efcbd443 avoid unnamed infixes; tuned; diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/CCL.thy --- 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=a' & b=b')", "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"]) *} diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/Fix.thy --- 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.,%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)))" diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/Set.thy --- 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*) diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/Term.thy --- 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"]]); *} diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/Trancl.thy --- 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. :r --> :r --> :r)" - comp_def: (*composition of relations*) + relcomp_def: (*composition of relations*) "r O s == {xz. EX x y z. xz = & :s & :r}" id_def: (*the identity relation*) "id == {p. EX x. p = }" @@ -57,14 +57,14 @@ subsection {* Composition of two relations *} lemma compI: "[| :s; :r |] ==> : 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 = ; :s; :r |] ==> P |] ==> P" - unfolding comp_def by blast + unfolding relcomp_def by blast lemma compEpair: "[| : r O s; diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/Type.thy --- 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" diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/Wfd.thy --- 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. : 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 diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/ex/List.thy --- 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)" diff -r b7866aea0815 -r c4f13ab78f9d src/CCL/ex/Nat.thy --- 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