avoid unnamed infixes;
authorwenzelm
Wed Oct 03 21:29:05 2007 +0200 (2007-10-03)
changeset 24825c4f13ab78f9d
parent 24824 b7866aea0815
child 24826 78e6a3cea367
avoid unnamed infixes;
tuned;
src/CCL/CCL.thy
src/CCL/Fix.thy
src/CCL/Set.thy
src/CCL/Term.thy
src/CCL/Trancl.thy
src/CCL/Type.thy
src/CCL/Wfd.thy
src/CCL/ex/List.thy
src/CCL/ex/Nat.thy
     1.1 --- a/src/CCL/CCL.thy	Wed Oct 03 19:49:33 2007 +0200
     1.2 +++ b/src/CCL/CCL.thy	Wed Oct 03 21:29:05 2007 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  classes prog < "term"
     1.5  defaultsort prog
     1.6  
     1.7 -arities fun :: (prog, prog) prog
     1.8 +arities "fun" :: (prog, prog) prog
     1.9  
    1.10  typedecl i
    1.11  arities i :: prog
    1.12 @@ -28,10 +28,10 @@
    1.13  
    1.14  consts
    1.15    (*** Evaluation Judgement ***)
    1.16 -  "--->"      ::       "[i,i]=>prop"          (infixl 20)
    1.17 +  Eval      ::       "[i,i]=>prop"          (infixl "--->" 20)
    1.18  
    1.19    (*** Bisimulations for pre-order and equality ***)
    1.20 -  "[="        ::       "['a,'a]=>o"           (infixl 50)
    1.21 +  po          ::       "['a,'a]=>o"           (infixl "[=" 50)
    1.22    SIM         ::       "[i,i,i set]=>o"
    1.23    POgen       ::       "i set => i set"
    1.24    EQgen       ::       "i set => i set"
    1.25 @@ -44,7 +44,7 @@
    1.26    pair        ::       "[i,i]=>i"             ("(1<_,/_>)")
    1.27    lambda      ::       "(i=>i)=>i"            (binder "lam " 55)
    1.28    "case"      ::       "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i"
    1.29 -  "`"         ::       "[i,i]=>i"             (infixl 56)
    1.30 +  "apply"     ::       "[i,i]=>i"             (infixl "`" 56)
    1.31    bot         ::       "i"
    1.32    "fix"       ::       "(i=>i)=>i"
    1.33  
    1.34 @@ -188,25 +188,19 @@
    1.35    by simp
    1.36  
    1.37  ML {*
    1.38 -  local
    1.39 -    val arg_cong = thm "arg_cong";
    1.40 -    val eq_lemma = thm "eq_lemma";
    1.41 -    val ss = simpset_of (the_context ());
    1.42 -  in
    1.43 -    fun mk_inj_rl thy rews s =
    1.44 -      let
    1.45 -        fun mk_inj_lemmas r = [arg_cong] RL [r RS (r RS eq_lemma)]
    1.46 -        val inj_lemmas = List.concat (map mk_inj_lemmas rews)
    1.47 -        val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE
    1.48 -          eresolve_tac inj_lemmas 1 ORELSE
    1.49 -          asm_simp_tac (Simplifier.theory_context thy ss addsimps rews) 1)
    1.50 -      in prove_goal thy s (fn _ => [tac]) end  
    1.51 -  end
    1.52 +  fun mk_inj_rl thy rews s =
    1.53 +    let
    1.54 +      fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
    1.55 +      val inj_lemmas = List.concat (map mk_inj_lemmas rews)
    1.56 +      val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE
    1.57 +        eresolve_tac inj_lemmas 1 ORELSE
    1.58 +        asm_simp_tac (Simplifier.theory_context thy @{simpset} addsimps rews) 1)
    1.59 +    in prove_goal thy s (fn _ => [tac]) end  
    1.60  *}
    1.61  
    1.62  ML {*
    1.63    bind_thms ("ccl_injs",
    1.64 -    map (mk_inj_rl (the_context ()) (thms "caseBs"))
    1.65 +    map (mk_inj_rl @{theory} @{thms caseBs})
    1.66        ["<a,b> = <a',b'> <-> (a=a' & b=b')",
    1.67         "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"])
    1.68  *}
     2.1 --- a/src/CCL/Fix.thy	Wed Oct 03 19:49:33 2007 +0200
     2.2 +++ b/src/CCL/Fix.thy	Wed Oct 03 21:29:05 2007 +0200
     2.3 @@ -14,10 +14,11 @@
     2.4    idgen      ::       "[i]=>i"
     2.5    INCL      :: "[i=>o]=>o"
     2.6  
     2.7 -axioms
     2.8 +defs
     2.9    idgen_def:
    2.10    "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
    2.11  
    2.12 +axioms
    2.13    INCL_def:   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
    2.14    po_INCL:    "INCL(%x. a(x) [= b(x))"
    2.15    INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
     3.1 --- a/src/CCL/Set.thy	Wed Oct 03 19:49:33 2007 +0200
     3.2 +++ b/src/CCL/Set.thy	Wed Oct 03 21:29:05 2007 +0200
     3.3 @@ -16,8 +16,8 @@
     3.4  consts
     3.5    Collect       :: "['a => o] => 'a set"                    (*comprehension*)
     3.6    Compl         :: "('a set) => 'a set"                     (*complement*)
     3.7 -  Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
     3.8 -  Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
     3.9 +  Int           :: "['a set, 'a set] => 'a set"         (infixl "Int" 70)
    3.10 +  Un            :: "['a set, 'a set] => 'a set"         (infixl "Un" 65)
    3.11    Union         :: "(('a set)set) => 'a set"                (*...of a set*)
    3.12    Inter         :: "(('a set)set) => 'a set"                (*...of a set*)
    3.13    UNION         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
    3.14 @@ -25,11 +25,10 @@
    3.15    Ball          :: "['a set, 'a => o] => o"                 (*bounded quants*)
    3.16    Bex           :: "['a set, 'a => o] => o"                 (*bounded quants*)
    3.17    mono          :: "['a set => 'b set] => o"                (*monotonicity*)
    3.18 -  ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
    3.19 -  "<="          :: "['a set, 'a set] => o"              (infixl 50)
    3.20 +  mem           :: "['a, 'a set] => o"                  (infixl ":" 50) (*membership*)
    3.21 +  subset        :: "['a set, 'a set] => o"              (infixl "<=" 50)
    3.22    singleton     :: "'a => 'a set"                       ("{_}")
    3.23    empty         :: "'a set"                             ("{}")
    3.24 -  "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)
    3.25  
    3.26  syntax
    3.27    "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
     4.1 --- a/src/CCL/Term.thy	Wed Oct 03 19:49:33 2007 +0200
     4.2 +++ b/src/CCL/Term.thy	Wed Oct 03 21:29:05 2007 +0200
     4.3 @@ -31,7 +31,7 @@
     4.4    nrec       :: "[i,i,[i,i]=>i]=>i"
     4.5  
     4.6    nil        :: "i"                        ("([])")
     4.7 -  "$"        :: "[i,i]=>i"                 (infixr 80)
     4.8 +  cons       :: "[i,i]=>i"                 (infixr "$" 80)
     4.9    lcase      :: "[i,i,[i,i]=>i]=>i"
    4.10    lrec       :: "[i,i,[i,i,i]=>i]=>i"
    4.11  
    4.12 @@ -288,7 +288,7 @@
    4.13  ML_setup {*
    4.14  bind_thms ("term_dstncts",
    4.15    mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
    4.16 -    [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","op $"]]);
    4.17 +    [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
    4.18  *}
    4.19  
    4.20  
     5.1 --- a/src/CCL/Trancl.thy	Wed Oct 03 19:49:33 2007 +0200
     5.2 +++ b/src/CCL/Trancl.thy	Wed Oct 03 21:29:05 2007 +0200
     5.3 @@ -15,11 +15,11 @@
     5.4    id      :: "i set"
     5.5    rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
     5.6    trancl  :: "i set => i set"               ("(_^+)" [100] 100)
     5.7 -  O       :: "[i set,i set] => i set"       (infixr 60)
     5.8 +  relcomp :: "[i set,i set] => i set"       (infixr "O" 60)
     5.9  
    5.10  axioms
    5.11    trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    5.12 -  comp_def:        (*composition of relations*)
    5.13 +  relcomp_def:     (*composition of relations*)
    5.14                     "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    5.15    id_def:          (*the identity relation*)
    5.16                     "id == {p. EX x. p = <x,x>}"
    5.17 @@ -57,14 +57,14 @@
    5.18  subsection {* Composition of two relations *}
    5.19  
    5.20  lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
    5.21 -  unfolding comp_def by blast
    5.22 +  unfolding relcomp_def by blast
    5.23  
    5.24  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    5.25  lemma compE:
    5.26      "[| xz : r O s;
    5.27          !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P
    5.28       |] ==> P"
    5.29 -  unfolding comp_def by blast
    5.30 +  unfolding relcomp_def by blast
    5.31  
    5.32  lemma compEpair:
    5.33    "[| <a,c> : r O s;
     6.1 --- a/src/CCL/Type.thy	Wed Oct 03 19:49:33 2007 +0200
     6.2 +++ b/src/CCL/Type.thy	Wed Oct 03 21:29:05 2007 +0200
     6.3 @@ -15,7 +15,7 @@
     6.4    Subtype       :: "['a set, 'a => o] => 'a set"
     6.5    Bool          :: "i set"
     6.6    Unit          :: "i set"
     6.7 -  "+"           :: "[i set, i set] => i set"         (infixr 55)
     6.8 +  Plus           :: "[i set, i set] => i set"        (infixr "+" 55)
     6.9    Pi            :: "[i set, i => i set] => i set"
    6.10    Sigma         :: "[i set, i => i set] => i set"
    6.11    Nat           :: "i set"
     7.1 --- a/src/CCL/Wfd.thy	Wed Oct 03 19:49:33 2007 +0200
     7.2 +++ b/src/CCL/Wfd.thy	Wed Oct 03 21:29:05 2007 +0200
     7.3 @@ -16,11 +16,11 @@
     7.4        (*** Relations ***)
     7.5    wf         ::       "[i set] => i set"
     7.6    wmap       ::       "[i=>i,i set] => i set"
     7.7 -  "**"       ::       "[i set,i set] => i set"      (infixl 70)
     7.8 +  lex        ::       "[i set,i set] => i set"      (infixl "**" 70)
     7.9    NatPR      ::       "i set"
    7.10    ListPR     ::       "i set => i set"
    7.11  
    7.12 -axioms
    7.13 +defs
    7.14  
    7.15    Wfd_def:
    7.16    "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
    7.17 @@ -442,7 +442,7 @@
    7.18  fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
    7.19    | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
    7.20    | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
    7.21 -  | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t
    7.22 +  | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
    7.23    | get_bno l n (t $ s) = get_bno l n t
    7.24    | get_bno l n (Bound m) = (m-length(l),n)
    7.25  
    7.26 @@ -463,7 +463,7 @@
    7.27  
    7.28  fun is_rigid_prog t =
    7.29       case (Logic.strip_assums_concl t) of
    7.30 -        (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = [])
    7.31 +        (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = [])
    7.32         | _ => false
    7.33  in
    7.34  
     8.1 --- a/src/CCL/ex/List.thy	Wed Oct 03 19:49:33 2007 +0200
     8.2 +++ b/src/CCL/ex/List.thy	Wed Oct 03 21:29:05 2007 +0200
     8.3 @@ -12,9 +12,9 @@
     8.4  
     8.5  consts
     8.6    map       :: "[i=>i,i]=>i"
     8.7 -  "o"       :: "[i=>i,i=>i]=>i=>i"             (infixr 55)
     8.8 -  "@"       :: "[i,i]=>i"             (infixr 55)
     8.9 -  mem       :: "[i,i]=>i"             (infixr 55)
    8.10 +  comp      :: "[i=>i,i=>i]=>i=>i"    (infixr "o" 55)
    8.11 +  append    :: "[i,i]=>i"             (infixr "@" 55)
    8.12 +  member    :: "[i,i]=>i"             (infixr "mem" 55)
    8.13    filter    :: "[i,i]=>i"
    8.14    flat      :: "i=>i"
    8.15    partition :: "[i,i]=>i"
    8.16 @@ -27,7 +27,7 @@
    8.17    map_def:     "map(f,l)   == lrec(l,[],%x xs g. f(x)$g)"
    8.18    comp_def:    "f o g == (%x. f(g(x)))"
    8.19    append_def:  "l @ m == lrec(l,m,%x xs g. x$g)"
    8.20 -  mem_def:     "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
    8.21 +  member_def:  "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
    8.22    filter_def:  "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
    8.23    flat_def:    "flat(l) == lrec(l,[],%h t g. h @ g)"
    8.24  
     9.1 --- a/src/CCL/ex/Nat.thy	Wed Oct 03 19:49:33 2007 +0200
     9.2 +++ b/src/CCL/ex/Nat.thy	Wed Oct 03 21:29:05 2007 +0200
     9.3 @@ -13,12 +13,12 @@
     9.4  consts
     9.5  
     9.6    not   :: "i=>i"
     9.7 -  "#+"  :: "[i,i]=>i"            (infixr 60)
     9.8 -  "#*"  :: "[i,i]=>i"            (infixr 60)
     9.9 -  "#-"  :: "[i,i]=>i"            (infixr 60)
    9.10 -  "##"  :: "[i,i]=>i"            (infixr 60)
    9.11 -  "#<"  :: "[i,i]=>i"            (infixr 60)
    9.12 -  "#<=" :: "[i,i]=>i"            (infixr 60)
    9.13 +  add   :: "[i,i]=>i"            (infixr "#+" 60)
    9.14 +  mult  :: "[i,i]=>i"            (infixr "#*" 60)
    9.15 +  sub   :: "[i,i]=>i"            (infixr "#-" 60)
    9.16 +  div   :: "[i,i]=>i"            (infixr "##" 60)
    9.17 +  lt    :: "[i,i]=>i"            (infixr "#<" 60)
    9.18 +  le    :: "[i,i]=>i"            (infixr "#<=" 60)
    9.19    ackermann :: "[i,i]=>i"
    9.20  
    9.21  defs