eliminated old defs;

--- a/src/CCL/CCL.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/CCL/CCL.thy	Mon Jan 11 21:16:38 2016 +0100
@@ -320,17 +320,17 @@
   apply blast
   done
 
-lemma POgenXH: 
-  "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |  
-           (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |  
+lemma POgenXH:
+  "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
+           (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
            (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(x)> : R))"
   apply (unfold POgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
-lemma poXH: 
-  "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |  
-                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |  
+lemma poXH:
+  "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x) [= f'(x)))"
   apply (simp add: PO_iff del: ex_simps)
   apply (rule POgen_mono
@@ -438,18 +438,18 @@
   apply blast
   done
 
-lemma EQgenXH: 
-  "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |  
-                                             (t=false \<and> t'=false) |  
-                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |  
+lemma EQgenXH:
+  "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |
+                                             (t=false \<and> t'=false) |
+                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
   apply (unfold EQgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
-lemma eqXH: 
-  "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |  
-                     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |  
+lemma eqXH:
+  "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
+                     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |
                      (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))"
   apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow>
     (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |

--- a/src/CCL/Set.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/CCL/Set.thy	Mon Jan 11 21:16:38 2016 +0100
@@ -9,62 +9,18 @@
 typedecl 'a set
 instance set :: ("term") "term" ..
 
-consts
-  Collect       :: "['a \<Rightarrow> o] \<Rightarrow> 'a set"                    (*comprehension*)
-  Compl         :: "('a set) \<Rightarrow> 'a set"                     (*complement*)
-  Int           :: "['a set, 'a set] \<Rightarrow> 'a set"         (infixl "Int" 70)
-  Un            :: "['a set, 'a set] \<Rightarrow> 'a set"         (infixl "Un" 65)
-  Union         :: "(('a set)set) \<Rightarrow> 'a set"                (*...of a set*)
-  Inter         :: "(('a set)set) \<Rightarrow> 'a set"                (*...of a set*)
-  UNION         :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"       (*general*)
-  INTER         :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"       (*general*)
-  Ball          :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"                 (*bounded quants*)
-  Bex           :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"                 (*bounded quants*)
-  mono          :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o"                (*monotonicity*)
-  mem           :: "['a, 'a set] \<Rightarrow> o"                  (infixl ":" 50) (*membership*)
-  subset        :: "['a set, 'a set] \<Rightarrow> o"              (infixl "<=" 50)
-  singleton     :: "'a \<Rightarrow> 'a set"                       ("{_}")
-  empty         :: "'a set"                             ("{}")
+
+subsection \<open>Set comprehension and membership\<close>
+
+axiomatization Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set"
+  and mem :: "['a, 'a set] \<Rightarrow> o"  (infixl ":" 50)
+where mem_Collect_iff: "(a : Collect(P)) \<longleftrightarrow> P(a)"
+  and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
 
 syntax
-  "_Coll"       :: "[idt, o] \<Rightarrow> 'a set"                 ("(1{_./ _})") (*collection*)
-
-  (* Big Intersection / Union *)
-
-  "_INTER"      :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
-  "_UNION"      :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
-
-  (* Bounded Quantifiers *)
-
-  "_Ball"       :: "[idt, 'a set, o] \<Rightarrow> o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
-  "_Bex"        :: "[idt, 'a set, o] \<Rightarrow> o"              ("(EX _:_./ _)" [0, 0, 0] 10)
-
+  "_Coll" :: "[idt, o] \<Rightarrow> 'a set"  ("(1{_./ _})")
 translations
-  "{x. P}"      == "CONST Collect(\<lambda>x. P)"
-  "INT x:A. B"  == "CONST INTER(A, \<lambda>x. B)"
-  "UN x:A. B"   == "CONST UNION(A, \<lambda>x. B)"
-  "ALL x:A. P"  == "CONST Ball(A, \<lambda>x. P)"
-  "EX x:A. P"   == "CONST Bex(A, \<lambda>x. P)"
-
-axiomatization where
-  mem_Collect_iff: "(a : {x. P(x)}) \<longleftrightarrow> P(a)" and
-  set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
-
-defs
-  Ball_def:      "Ball(A, P)  == ALL x. x:A \<longrightarrow> P(x)"
-  Bex_def:       "Bex(A, P)   == EX x. x:A \<and> P(x)"
-  mono_def:      "mono(f)     == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
-  subset_def:    "A <= B      == ALL x:A. x:B"
-  singleton_def: "{a}         == {x. x=a}"
-  empty_def:     "{}          == {x. False}"
-  Un_def:        "A Un B      == {x. x:A | x:B}"
-  Int_def:       "A Int B     == {x. x:A \<and> x:B}"
-  Compl_def:     "Compl(A)    == {x. \<not>x:A}"
-  INTER_def:     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
-  UNION_def:     "UNION(A, B) == {y. EX x:A. y: B(x)}"
-  Inter_def:     "Inter(S)    == (INT x:S. x)"
-  Union_def:     "Union(S)    == (UN x:S. x)"
-
+  "{x. P}" == "CONST Collect(\<lambda>x. P)"
 
 lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
   apply (rule mem_Collect_iff [THEN iffD2])
@@ -85,6 +41,19 @@
 
 subsection \<open>Bounded quantifiers\<close>
 
+definition Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"
+  where "Ball(A, P) == ALL x. x:A \<longrightarrow> P(x)"
+
+definition Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"
+  where "Bex(A, P) == EX x. x:A \<and> P(x)"
+
+syntax
+  "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(ALL _:_./ _)" [0, 0, 0] 10)
+  "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o"  ("(EX _:_./ _)" [0, 0, 0] 10)
+translations
+  "ALL x:A. P"  == "CONST Ball(A, \<lambda>x. P)"
+  "EX x:A. P"   == "CONST Bex(A, \<lambda>x. P)"
+
 lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
   by (simp add: Ball_def)
 
@@ -107,8 +76,7 @@
 lemma ball_rew: "(ALL x:A. True) \<longleftrightarrow> True"
   by (blast intro: ballI)
 
-
-subsection \<open>Congruence rules\<close>
+subsubsection \<open>Congruence rules\<close>
 
 lemma ball_cong:
   "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow>
@@ -121,6 +89,52 @@
   by (blast intro: bexI elim: bexE)
 
 
+subsection \<open>Further operations\<close>
+
+definition subset :: "['a set, 'a set] \<Rightarrow> o"  (infixl "<=" 50)
+  where "A <= B == ALL x:A. x:B"
+
+definition mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o"
+  where "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
+
+definition singleton :: "'a \<Rightarrow> 'a set"  ("{_}")
+  where "{a} == {x. x=a}"
+
+definition empty :: "'a set"  ("{}")
+  where "{} == {x. False}"
+
+definition Un :: "['a set, 'a set] \<Rightarrow> 'a set"  (infixl "Un" 65)
+  where "A Un B == {x. x:A | x:B}"
+
+definition Int :: "['a set, 'a set] \<Rightarrow> 'a set"  (infixl "Int" 70)
+  where "A Int B == {x. x:A \<and> x:B}"
+
+definition Compl :: "('a set) \<Rightarrow> 'a set"
+  where "Compl(A) == {x. \<not>x:A}"
+
+
+subsection \<open>Big Intersection / Union\<close>
+
+definition INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"
+  where "INTER(A, B) == {y. ALL x:A. y: B(x)}"
+
+definition UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"
+  where "UNION(A, B) == {y. EX x:A. y: B(x)}"
+
+syntax
+  "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(INT _:_./ _)" [0, 0, 0] 10)
+  "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set"  ("(UN _:_./ _)" [0, 0, 0] 10)
+translations
+  "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
+  "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
+
+definition Inter :: "(('a set)set) \<Rightarrow> 'a set"
+  where "Inter(S) == (INT x:S. x)"
+
+definition Union :: "(('a set)set) \<Rightarrow> 'a set"
+  where "Union(S) == (UN x:S. x)"
+
+
 subsection \<open>Rules for subsets\<close>
 
 lemma subsetI: "(\<And>x. x:A \<Longrightarrow> x:B) \<Longrightarrow> A <= B"

--- a/src/CCL/Term.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/CCL/Term.thy	Mon Jan 11 21:16:38 2016 +0100
@@ -9,48 +9,69 @@
 imports CCL
 begin
 
-consts
+definition one :: "i"
+  where "one == true"
 
-  one        :: "i"
+definition "if" :: "[i,i,i]\<Rightarrow>i"  ("(3if _/ then _/ else _)" [0,0,60] 60)
+  where "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
 
-  "if"       :: "[i,i,i]\<Rightarrow>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
+definition inl :: "i\<Rightarrow>i"
+  where "inl(a) == <true,a>"
 
-  inl        :: "i\<Rightarrow>i"
-  inr        :: "i\<Rightarrow>i"
-  "when"     :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+definition inr :: "i\<Rightarrow>i"
+  where "inr(b) == <false,b>"
+
+definition split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
 
-  split      :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
-  fst        :: "i\<Rightarrow>i"
-  snd        :: "i\<Rightarrow>i"
-  thd        :: "i\<Rightarrow>i"
+definition "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
+
+definition fst :: "i\<Rightarrow>i"
+  where "fst(t) == split(t, \<lambda>x y. x)"
 
-  zero       :: "i"
-  succ       :: "i\<Rightarrow>i"
-  ncase      :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
-  nrec       :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition snd :: "i\<Rightarrow>i"
+  where "snd(t) == split(t, \<lambda>x y. y)"
+
+definition thd :: "i\<Rightarrow>i"
+  where "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
+
+definition zero :: "i"
+  where "zero == inl(one)"
 
-  nil        :: "i"                        ("([])")
-  cons       :: "[i,i]\<Rightarrow>i"                 (infixr "$" 80)
-  lcase      :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
-  lrec       :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition succ :: "i\<Rightarrow>i"
+  where "succ(n) == inr(n)"
+
+definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
 
-  "let"      :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
-  letrec     :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
-  letrec2    :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
-  letrec3    :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+
+no_syntax
+  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
+
+definition "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
+  where "let(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
 syntax
-  "_let"     :: "[id,i,i]\<Rightarrow>i"             ("(3let _ be _/ in _)"
-                        [0,0,60] 60)
+  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
 
-  "_letrec"  :: "[id,id,i,i]\<Rightarrow>i"         ("(3letrec _ _ be _/ in _)"
-                        [0,0,0,60] 60)
+definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+
+definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec2 (h, f) ==
+    letrec (\<lambda>p g'. split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>))), \<lambda>g'. f(\<lambda>x y. g'(<x,y>)))"
 
-  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"     ("(3letrec _ _ _ be _/ in _)"
-                        [0,0,0,0,60] 60)
+definition letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+  where "letrec3 (h, f) ==
+    letrec (\<lambda>p g'. split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>)))),
+      \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
-  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)"
-                        [0,0,0,0,0,60] 60)
+syntax
+  "_let" :: "[id,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+  "_letrec" :: "[id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
+  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
+  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
 
 ML \<open>
 (** Quantifier translations: variable binding **)
@@ -107,42 +128,24 @@
   (@{const_syntax letrec3}, K letrec3_tr')]
 \<close>
 
-consts
-  napply     :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
+
+definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
+
+definition nil :: "i"  ("([])")
+  where "[] == inl(one)"
 
-defs
-  one_def:                    "one == true"
-  if_def:     "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
-  inl_def:                 "inl(a) == <true,a>"
-  inr_def:                 "inr(b) == <false,b>"
-  when_def:           "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
-  split_def:           "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
-  fst_def:                 "fst(t) == split(t, \<lambda>x y. x)"
-  snd_def:                 "snd(t) == split(t, \<lambda>x y. y)"
-  thd_def:                 "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
-  zero_def:                  "zero == inl(one)"
-  succ_def:               "succ(n) == inr(n)"
-  ncase_def:         "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
-  nrec_def:          " nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
-  nil_def:                     "[] == inl(one)"
-  cons_def:                   "h$t == inr(<h,t>)"
-  lcase_def:         "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
-  lrec_def:           "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
+definition cons :: "[i,i]\<Rightarrow>i"  (infixr "$" 80)
+  where "h$t == inr(<h,t>)"
+
+definition lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
 
-  let_def:  "let x be t in f(x) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-  letrec_def:
-  "letrec g x be h(x,g) in b(g) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+  where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
 
-  letrec2_def:  "letrec g x y be h(x,y,g) in f(g)==
-               letrec g' p be split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>)))
-                          in f(\<lambda>x y. g'(<x,y>))"
-
-  letrec3_def:  "letrec g x y z be h(x,y,z,g) in f(g) ==
-             letrec g' p be split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>))))
-                          in f(\<lambda>x y z. g'(<x,<y,z>>))"
-
-  napply_def: "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
-
+definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  ("(_ ^ _ ` _)" [56,56,56] 56)
+  where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
 
 lemmas simp_can_defs = one_def inl_def inr_def
   and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def

--- a/src/CCL/Type.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/CCL/Type.thy	Mon Jan 11 21:16:38 2016 +0100
@@ -9,42 +9,39 @@
 imports Term
 begin
 
-consts
-
-  Subtype       :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set"
-  Bool          :: "i set"
-  Unit          :: "i set"
-  Plus           :: "[i set, i set] \<Rightarrow> i set"        (infixr "+" 55)
-  Pi            :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
-  Sigma         :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
-  Nat           :: "i set"
-  List          :: "i set \<Rightarrow> i set"
-  Lists         :: "i set \<Rightarrow> i set"
-  ILists        :: "i set \<Rightarrow> i set"
-  TAll          :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"       (binder "TALL " 55)
-  TEx           :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"       (binder "TEX " 55)
-  Lift          :: "i set \<Rightarrow> i set"                  ("(3[_])")
-
-  SPLIT         :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
+definition Subtype :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set"
+  where "Subtype(A, P) == {x. x:A \<and> P(x)}"
 
 syntax
-  "_Pi"         :: "[idt, i set, i set] \<Rightarrow> i set"    ("(3PROD _:_./ _)"
-                                [0,0,60] 60)
+  "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  ("(1{_: _ ./ _})")
+translations
+  "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
 
-  "_Sigma"      :: "[idt, i set, i set] \<Rightarrow> i set"    ("(3SUM _:_./ _)"
-                                [0,0,60] 60)
+definition Unit :: "i set"
+  where "Unit == {x. x=one}"
+
+definition Bool :: "i set"
+  where "Bool == {x. x=true | x=false}"
+
+definition Plus :: "[i set, i set] \<Rightarrow> i set"  (infixr "+" 55)
+  where "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
 
-  "_arrow"      :: "[i set, i set] \<Rightarrow> i set"         ("(_ ->/ _)"  [54, 53] 53)
-  "_star"       :: "[i set, i set] \<Rightarrow> i set"         ("(_ */ _)" [56, 55] 55)
-  "_Subtype"    :: "[idt, 'a set, o] \<Rightarrow> 'a set"      ("(1{_: _ ./ _})")
+definition Pi :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
+  where "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}"
+
+definition Sigma :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
+  where "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
 
+syntax
+  "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set"  ("(3PROD _:_./ _)" [0,0,60] 60)
+  "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set"  ("(3SUM _:_./ _)" [0,0,60] 60)
+  "_arrow" :: "[i set, i set] \<Rightarrow> i set"  ("(_ ->/ _)"  [54, 53] 53)
+  "_star"  :: "[i set, i set] \<Rightarrow> i set"  ("(_ */ _)" [56, 55] 55)
 translations
-  "PROD x:A. B" => "CONST Pi(A, \<lambda>x. B)"
-  "A -> B"      => "CONST Pi(A, \<lambda>_. B)"
-  "SUM x:A. B"  => "CONST Sigma(A, \<lambda>x. B)"
-  "A * B"       => "CONST Sigma(A, \<lambda>_. B)"
-  "{x: A. B}"   == "CONST Subtype(A, \<lambda>x. B)"
-
+  "PROD x:A. B" \<rightharpoonup> "CONST Pi(A, \<lambda>x. B)"
+  "A -> B" \<rightharpoonup> "CONST Pi(A, \<lambda>_. B)"
+  "SUM x:A. B" \<rightharpoonup> "CONST Sigma(A, \<lambda>x. B)"
+  "A * B" \<rightharpoonup> "CONST Sigma(A, \<lambda>_. B)"
 print_translation \<open>
  [(@{const_syntax Pi},
     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
@@ -52,28 +49,34 @@
     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
 \<close>
 
-defs
-  Subtype_def: "{x:A. P(x)} == {x. x:A \<and> P(x)}"
-  Unit_def:          "Unit == {x. x=one}"
-  Bool_def:          "Bool == {x. x=true | x=false}"
-  Plus_def:           "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
-  Pi_def:         "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}"
-  Sigma_def:   "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
-  Nat_def:            "Nat == lfp(\<lambda>X. Unit + X)"
-  List_def:       "List(A) == lfp(\<lambda>X. Unit + A*X)"
+definition Nat :: "i set"
+  where "Nat == lfp(\<lambda>X. Unit + X)"
+
+definition List :: "i set \<Rightarrow> i set"
+  where "List(A) == lfp(\<lambda>X. Unit + A*X)"
+
+definition Lists :: "i set \<Rightarrow> i set"
+  where "Lists(A) == gfp(\<lambda>X. Unit + A*X)"
+
+definition ILists :: "i set \<Rightarrow> i set"
+  where "ILists(A) == gfp(\<lambda>X.{} + A*X)"
 
-  Lists_def:     "Lists(A) == gfp(\<lambda>X. Unit + A*X)"
-  ILists_def:   "ILists(A) == gfp(\<lambda>X.{} + A*X)"
+
+definition TAll :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"  (binder "TALL " 55)
+  where "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
 
-  Tall_def:   "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
-  Tex_def:     "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
-  Lift_def:           "[A] == A Un {bot}"
+definition TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set"  (binder "TEX " 55)
+  where "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
 
-  SPLIT_def:   "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})"
+definition Lift :: "i set \<Rightarrow> i set"  ("(3[_])")
+  where "[A] == A Un {bot}"
+
+definition SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
+  where "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})"
 
 
 lemmas simp_type_defs =
-    Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def
+    Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def TAll_def TEx_def
   and ind_type_defs = Nat_def List_def
   and simp_data_defs = one_def inl_def inr_def
   and ind_data_defs = zero_def succ_def nil_def cons_def