Theory Type

(*  Title:      CCL/Type.thy
    Author:     Martin Coen
    Copyright   1993  University of Cambridge
*)

section Types in CCL are defined as sets of terms

theory Type
imports Term
begin

definition Subtype :: "['a set, 'a  o]  'a set"
  where "Subtype(A, P) == {x. x:A  P(x)}"

syntax
  "_Subtype" :: "[idt, 'a set, o]  'a set"  ("(1{_: _ ./ _})")
translations
  "{x: A. B}" == "CONST Subtype(A, λx. B)"

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]  i set"  (infixr "+" 55)
  where "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"

definition Pi :: "[i set, i  i set]  i set"
  where "Pi(A,B) == {x. EX b. x=lam x. b(x)  (ALL x:A. b(x):B(x))}"

definition Sigma :: "[i set, i  i set]  i set"
  where "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"

syntax
  "_Pi" :: "[idt, i set, i set]  i set"  ("(3PROD _:_./ _)" [0,0,60] 60)
  "_Sigma" :: "[idt, i set, i set]  i set"  ("(3SUM _:_./ _)" [0,0,60] 60)
  "_arrow" :: "[i set, i set]  i set"  ("(_ ->/ _)"  [54, 53] 53)
  "_star"  :: "[i set, i set]  i set"  ("(_ */ _)" [56, 55] 55)
translations
  "PROD x:A. B"  "CONST Pi(A, λx. B)"
  "A -> B"  "CONST Pi(A, λ_. B)"
  "SUM x:A. B"  "CONST Sigma(A, λx. B)"
  "A * B"  "CONST Sigma(A, λ_. B)"
print_translation 
 [(const_syntaxPi,
    fn _ => Syntax_Trans.dependent_tr' (syntax_const‹_Pi›, syntax_const‹_arrow›)),
  (const_syntaxSigma,
    fn _ => Syntax_Trans.dependent_tr' (syntax_const‹_Sigma›, syntax_const‹_star›))]


definition Nat :: "i set"
  where "Nat == lfp(λX. Unit + X)"

definition List :: "i set  i set"
  where "List(A) == lfp(λX. Unit + A*X)"

definition Lists :: "i set  i set"
  where "Lists(A) == gfp(λX. Unit + A*X)"

definition ILists :: "i set  i set"
  where "ILists(A) == gfp(λX.{} + A*X)"


definition TAll :: "(i set  i set)  i set"  (binder "TALL " 55)
  where "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"

definition TEx :: "(i set  i set)  i set"  (binder "TEX " 55)
  where "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"

definition Lift :: "i set  i set"  ("(3[_])")
  where "[A] == A Un {bot}"

definition SPLIT :: "[i, [i, i]  i set]  i set"
  where "SPLIT(p,B) == Union({A. EX x y. p=<x,y>  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
  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

lemma subsetXH: "A <= B  (ALL x. x:A  x:B)"
  by blast


subsection Exhaustion Rules

lemma EmptyXH: "a. a : {}  False"
  and SubtypeXH: "a A P. a : {x:A. P(x)}  (a:A  P(a))"
  and UnitXH: "a. a : Unit           a=one"
  and BoolXH: "a. a : Bool           a=true | a=false"
  and PlusXH: "a A B. a : A+B            (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))"
  and PiXH: "a A B. a : PROD x:A. B(x)  (EX b. a=lam x. b(x)  (ALL x:A. b(x):B(x)))"
  and SgXH: "a A B. a : SUM x:A. B(x)   (EX x:A. EX y:B(x).a=<x,y>)"
  unfolding simp_type_defs by blast+

lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH

lemma LiftXH: "a : [A]  (a=bot | a:A)"
  and TallXH: "a : TALL X. B(X)  (ALL X. a:B(X))"
  and TexXH: "a : TEX X. B(X)  (EX X. a:B(X))"
  unfolding simp_type_defs by blast+

ML ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs})


subsection Canonical Type Rules

lemma oneT: "one : Unit"
  and trueT: "true : Bool"
  and falseT: "false : Bool"
  and lamT: "b B. (x. x:A  b(x):B(x))  lam x. b(x) : Pi(A,B)"
  and pairT: "b B. a:A; b:B(a)  <a,b>:Sigma(A,B)"
  and inlT: "a:A  inl(a) : A+B"
  and inrT: "b:B  inr(b) : A+B"
  by (blast intro: XHs [THEN iffD2])+

lemmas canTs = oneT trueT falseT pairT lamT inlT inrT


subsection Non-Canonical Type Rules

lemma lem: "a:B(u); u = v  a : B(v)"
  by blast


ML 
fun mk_ncanT_tac top_crls crls =
  SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
    resolve_tac ctxt ([major] RL top_crls) 1 THEN
    REPEAT_SOME (eresolve_tac ctxt (crls @ @{thms exE bexE conjE disjE})) THEN
    ALLGOALS (asm_simp_tac ctxt) THEN
    ALLGOALS (assume_tac ctxt ORELSE' resolve_tac ctxt (prems RL [@{thm lem}])
      ORELSE' eresolve_tac ctxt @{thms bspec}) THEN
    safe_tac (ctxt addSIs prems))


method_setup ncanT = 
  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls})


lemma ifT: "b:Bool; b=true  t:A(true); b=false  u:A(false)  if b then t else u : A(b)"
  by ncanT

lemma applyT: "f : Pi(A,B); a:A  f ` a : B(a)"
  by ncanT

lemma splitT: "p:Sigma(A,B); x y. x:A; y:B(x); p=<x,y>  c(x,y):C(<x,y>)  split(p,c):C(p)"
  by ncanT

lemma whenT:
  "p:A+B;
    x. x:A; p=inl(x)  a(x):C(inl(x));
    y. y:B;  p=inr(y)  b(y):C(inr(y))  when(p,a,b) : C(p)"
  by ncanT

lemmas ncanTs = ifT applyT splitT whenT


subsection Subtypes

lemma SubtypeD1: "a : Subtype(A, P)  a : A"
  and SubtypeD2: "a : Subtype(A, P)  P(a)"
  by (simp_all add: SubtypeXH)

lemma SubtypeI: "a:A; P(a)  a : {x:A. P(x)}"
  by (simp add: SubtypeXH)

lemma SubtypeE: "a : {x:A. P(x)}; a:A; P(a)  Q  Q"
  by (simp add: SubtypeXH)


subsection Monotonicity

lemma idM: "mono (λX. X)"
  apply (rule monoI)
  apply assumption
  done

lemma constM: "mono(λX. A)"
  apply (rule monoI)
  apply (rule subset_refl)
  done

lemma "mono(λX. A(X))  mono(λX.[A(X)])"
  apply (rule subsetI [THEN monoI])
  apply (drule LiftXH [THEN iffD1])
  apply (erule disjE)
   apply (erule disjI1 [THEN LiftXH [THEN iffD2]])
  apply (rule disjI2 [THEN LiftXH [THEN iffD2]])
  apply (drule (1) monoD)
  apply blast
  done

lemma SgM:
  "mono(λX. A(X)); x X. x:A(X)  mono(λX. B(X,x)) 
    mono(λX. Sigma(A(X),B(X)))"
  by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls
    dest!: monoD [THEN subsetD])

lemma PiM: "(x. x:A  mono(λX. B(X,x)))  mono(λX. Pi(A,B(X)))"
  by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls
    dest!: monoD [THEN subsetD])

lemma PlusM: "mono(λX. A(X)); mono(λX. B(X))  mono(λX. A(X)+B(X))"
  by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls
    dest!: monoD [THEN subsetD])


subsection Recursive types

subsubsection Conversion Rules for Fixed Points via monotonicity and Tarski

lemma NatM: "mono(λX. Unit+X)"
  apply (rule PlusM constM idM)+
  done

lemma def_NatB: "Nat = Unit + Nat"
  apply (rule def_lfp_Tarski [OF Nat_def])
  apply (rule NatM)
  done

lemma ListM: "mono(λX.(Unit+Sigma(A,λy. X)))"
  apply (rule PlusM SgM constM idM)+
  done

lemma def_ListB: "List(A) = Unit + A * List(A)"
  apply (rule def_lfp_Tarski [OF List_def])
  apply (rule ListM)
  done

lemma def_ListsB: "Lists(A) = Unit + A * Lists(A)"
  apply (rule def_gfp_Tarski [OF Lists_def])
  apply (rule ListM)
  done

lemma IListsM: "mono(λX.({} + Sigma(A,λy. X)))"
  apply (rule PlusM SgM constM idM)+
  done

lemma def_IListsB: "ILists(A) = {} + A * ILists(A)"
  apply (rule def_gfp_Tarski [OF ILists_def])
  apply (rule IListsM)
  done

lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB


subsection Exhaustion Rules

lemma NatXH: "a : Nat  (a=zero | (EX x:Nat. a=succ(x)))"
  and ListXH: "a : List(A)  (a=[] | (EX x:A. EX xs:List(A).a=x$xs))"
  and ListsXH: "a : Lists(A)  (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))"
  and IListsXH: "a : ILists(A)  (EX x:A. EX xs:ILists(A).a=x$xs)"
  unfolding ind_data_defs
  by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+

lemmas iXHs = NatXH ListXH

ML ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs})


subsection Type Rules

lemma zeroT: "zero : Nat"
  and succT: "n:Nat  succ(n) : Nat"
  and nilT: "[] : List(A)"
  and consT: "h:A; t:List(A)  h$t : List(A)"
  by (blast intro: iXHs [THEN iffD2])+

lemmas icanTs = zeroT succT nilT consT


method_setup incanT = 
  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls})


lemma ncaseT: "n:Nat; n=zero  b:C(zero); x. x:Nat; n=succ(x)  c(x):C(succ(x))
     ncase(n,b,c) : C(n)"
  by incanT

lemma lcaseT: "l:List(A); l = []  b:C([]); h t. h:A; t:List(A); l=h$t  c(h,t):C(h$t)
     lcase(l,b,c) : C(l)"
  by incanT

lemmas incanTs = ncaseT lcaseT


subsection Induction Rules

lemmas ind_Ms = NatM ListM

lemma Nat_ind: "n:Nat; P(zero); x. x:Nat; P(x)  P(succ(x))  P(n)"
  apply (unfold ind_data_defs)
  apply (erule def_induct [OF Nat_def _ NatM])
  apply (blast intro: canTs elim!: case_rls)
  done

lemma List_ind: "l:List(A); P([]); x xs. x:A; xs:List(A); P(xs)  P(x$xs)  P(l)"
  apply (unfold ind_data_defs)
  apply (erule def_induct [OF List_def _ ListM])
  apply (blast intro: canTs elim!: case_rls)
  done

lemmas inds = Nat_ind List_ind


subsection Primitive Recursive Rules

lemma nrecT: "n:Nat; b:C(zero); x g. x:Nat; g:C(x)  c(x,g):C(succ(x))
     nrec(n,b,c) : C(n)"
  by (erule Nat_ind) auto

lemma lrecT: "l:List(A); b:C([]); x xs g. x:A; xs:List(A); g:C(xs)  c(x,xs,g):C(x$xs) 
     lrec(l,b,c) : C(l)"
  by (erule List_ind) auto

lemmas precTs = nrecT lrecT


subsection Theorem proving

lemma SgE2: "<a,b> : Sigma(A,B); a:A; b:B(a)  P  P"
  unfolding SgXH by blast

(* General theorem proving ignores non-canonical term-formers,             *)
(*         - intro rules are type rules for canonical terms                *)
(*         - elim rules are case rules (no non-canonical terms appear)     *)

ML ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs})

lemmas [intro!] = SubtypeI canTs icanTs
  and [elim!] = SubtypeE XHEs


subsection Infinite Data Types

lemma lfp_subset_gfp: "mono(f)  lfp(f) <= gfp(f)"
  apply (rule lfp_lowerbound [THEN subset_trans])
   apply (erule gfp_lemma3)
  apply (rule subset_refl)
  done

lemma gfpI:
  assumes "a:A"
    and "x X. x:A; ALL y:A. t(y):X  t(x) : B(X)"
  shows "t(a) : gfp(B)"
  apply (rule coinduct)
   apply (rule_tac P = "λx. EX y:A. x=t (y)" in CollectI)
   apply (blast intro!: assms)+
  done

lemma def_gfpI: "C == gfp(B); a:A; x X. x:A; ALL y:A. t(y):X  t(x) : B(X)  t(a) : C"
  apply unfold
  apply (erule gfpI)
  apply blast
  done

(* EG *)
lemma "letrec g x be zero$g(x) in g(bot) : Lists(Nat)"
  apply (rule refl [THEN UnitXH [THEN iffD2], THEN Lists_def [THEN def_gfpI]])
  apply (subst letrecB)
  apply (unfold cons_def)
  apply blast
  done


subsection Lemmas and tactics for using the rule coinduct3› on [=› and =›

lemma lfpI: "mono(f); a : f(lfp(f))  a : lfp(f)"
  apply (erule lfp_Tarski [THEN ssubst])
  apply assumption
  done

lemma ssubst_single: "a = a'; a' : A  a : A"
  by simp

lemma ssubst_pair: "a = a'; b = b'; <a',b'> : A  <a,b> : A"
  by simp


ML 
  val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} =>
    fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1);


method_setup coinduct3 = Scan.succeed (SIMPLE_METHOD' o coinduct3_tac)

lemma ci3_RI: "mono(Agen); a : R  a : lfp(λx. Agen(x) Un R Un A)"
  by coinduct3

lemma ci3_AgenI: "mono(Agen); a : Agen(lfp(λx. Agen(x) Un R Un A)) 
    a : lfp(λx. Agen(x) Un R Un A)"
  by coinduct3

lemma ci3_AI: "mono(Agen); a : A  a : lfp(λx. Agen(x) Un R Un A)"
  by coinduct3

ML 
fun genIs_tac ctxt genXH gen_mono =
  resolve_tac ctxt [genXH RS @{thm iffD2}] THEN'
  simp_tac ctxt THEN'
  TRY o fast_tac
    (ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])


method_setup genIs = 
  Attrib.thm -- Attrib.thm >>
    (fn (genXH, gen_mono) => fn ctxt => SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))



subsection POgen

lemma PO_refl: "<a,a> : PO"
  by (rule po_refl [THEN PO_iff [THEN iffD1]])

lemma POgenIs:
  "<true,true> : POgen(R)"
  "<false,false> : POgen(R)"
  "<a,a'> : R; <b,b'> : R  <<a,b>,<a',b'>> : POgen(R)"
  "b b'. (x. <b(x),b'(x)> : R)  <lam x. b(x),lam x. b'(x)> : POgen(R)"
  "<one,one> : POgen(R)"
  "<a,a'> : lfp(λx. POgen(x) Un R Un PO) 
    <inl(a),inl(a')> : POgen(lfp(λx. POgen(x) Un R Un PO))"
  "<b,b'> : lfp(λx. POgen(x) Un R Un PO) 
    <inr(b),inr(b')> : POgen(lfp(λx. POgen(x) Un R Un PO))"
  "<zero,zero> : POgen(lfp(λx. POgen(x) Un R Un PO))"
  "<n,n'> : lfp(λx. POgen(x) Un R Un PO) 
    <succ(n),succ(n')> : POgen(lfp(λx. POgen(x) Un R Un PO))"
  "<[],[]> : POgen(lfp(λx. POgen(x) Un R Un PO))"
  "<h,h'> : lfp(λx. POgen(x) Un R Un PO);  <t,t'> : lfp(λx. POgen(x) Un R Un PO)
     <h$t,h'$t'> : POgen(lfp(λx. POgen(x) Un R Un PO))"
  unfolding data_defs by (genIs POgenXH POgen_mono)+

ML 
fun POgen_tac ctxt (rla, rlb) i =
  SELECT_GOAL (safe_tac ctxt) i THEN
  resolve_tac ctxt [rlb RS (rla RS @{thm ssubst_pair})] i THEN
  (REPEAT (resolve_tac ctxt
      (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
        (@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @
        [@{thm POgen_mono} RS @{thm ci3_RI}]) i))



subsection EQgen

lemma EQ_refl: "<a,a> : EQ"
  by (rule refl [THEN EQ_iff [THEN iffD1]])

lemma EQgenIs:
  "<true,true> : EQgen(R)"
  "<false,false> : EQgen(R)"
  "<a,a'> : R; <b,b'> : R  <<a,b>,<a',b'>> : EQgen(R)"
  "b b'. (x. <b(x),b'(x)> : R)  <lam x. b(x),lam x. b'(x)> : EQgen(R)"
  "<one,one> : EQgen(R)"
  "<a,a'> : lfp(λx. EQgen(x) Un R Un EQ) 
    <inl(a),inl(a')> : EQgen(lfp(λx. EQgen(x) Un R Un EQ))"
  "<b,b'> : lfp(λx. EQgen(x) Un R Un EQ) 
    <inr(b),inr(b')> : EQgen(lfp(λx. EQgen(x) Un R Un EQ))"
  "<zero,zero> : EQgen(lfp(λx. EQgen(x) Un R Un EQ))"
  "<n,n'> : lfp(λx. EQgen(x) Un R Un EQ) 
    <succ(n),succ(n')> : EQgen(lfp(λx. EQgen(x) Un R Un EQ))"
  "<[],[]> : EQgen(lfp(λx. EQgen(x) Un R Un EQ))"
  "<h,h'> : lfp(λx. EQgen(x) Un R Un EQ); <t,t'> : lfp(λx. EQgen(x) Un R Un EQ)
     <h$t,h'$t'> : EQgen(lfp(λx. EQgen(x) Un R Un EQ))"
  unfolding data_defs by (genIs EQgenXH EQgen_mono)+

ML 
fun EQgen_raw_tac ctxt i =
  (REPEAT (resolve_tac ctxt (@{thms EQgenIs} @
        [@{thm EQ_refl} RS (@{thm EQgen_mono} RS @{thm ci3_AI})] @
        (@{thms EQgenIs} RL [@{thm EQgen_mono} RS @{thm ci3_AgenI}]) @
        [@{thm EQgen_mono} RS @{thm ci3_RI}]) i))

(* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *)
(* then reduce this to a goal <a',b'> : R (hopefully?)                                *)
(*      rews are rewrite rules that would cause looping in the simpifier              *)

fun EQgen_tac ctxt rews i =
 SELECT_GOAL
   (TRY (safe_tac ctxt) THEN
    resolve_tac ctxt ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN
    ALLGOALS (simp_tac ctxt) THEN
    ALLGOALS (EQgen_raw_tac ctxt)) i


method_setup EQgen = 
  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (EQgen_tac ctxt ths))


end