src/CCL/Hered.thy
author wenzelm
Sat May 15 22:15:57 2010 +0200 (2010-05-15)
changeset 36948 d2cdad45fd14
parent 32154 9721e8e4d48c
child 42156 df219e736a5d
permissions -rw-r--r--
renamed Outer_Parse to Parse (in Scala);
     1 (*  Title:      CCL/Hered.thy
     2     Author:     Martin Coen
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 header {* Hereditary Termination -- cf. Martin Lo\"f *}
     7 
     8 theory Hered
     9 imports Type
    10 begin
    11 
    12 text {*
    13   Note that this is based on an untyped equality and so @{text "lam
    14   x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"}
    15   is.  Not so useful for functions!
    16 *}
    17 
    18 consts
    19       (*** Predicates ***)
    20   HTTgen     ::       "i set => i set"
    21   HTT        ::       "i set"
    22 
    23 axioms
    24   (*** Definitions of Hereditary Termination ***)
    25 
    26   HTTgen_def:
    27   "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b>      & a : R & b : R) |
    28                                       (EX f.  t=lam x. f(x) & (ALL x. f(x) : R))}"
    29   HTT_def:       "HTT == gfp(HTTgen)"
    30 
    31 
    32 subsection {* Hereditary Termination *}
    33 
    34 lemma HTTgen_mono: "mono(%X. HTTgen(X))"
    35   apply (unfold HTTgen_def)
    36   apply (rule monoI)
    37   apply blast
    38   done
    39 
    40 lemma HTTgenXH: 
    41   "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) |  
    42                                         (EX f. t=lam x. f(x) & (ALL x. f(x) : A))"
    43   apply (unfold HTTgen_def)
    44   apply blast
    45   done
    46 
    47 lemma HTTXH: 
    48   "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) |  
    49                                    (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))"
    50   apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def])
    51   apply blast
    52   done
    53 
    54 
    55 subsection {* Introduction Rules for HTT *}
    56 
    57 lemma HTT_bot: "~ bot : HTT"
    58   by (blast dest: HTTXH [THEN iffD1])
    59 
    60 lemma HTT_true: "true : HTT"
    61   by (blast intro: HTTXH [THEN iffD2])
    62 
    63 lemma HTT_false: "false : HTT"
    64   by (blast intro: HTTXH [THEN iffD2])
    65 
    66 lemma HTT_pair: "<a,b> : HTT <->  a : HTT  & b : HTT"
    67   apply (rule HTTXH [THEN iff_trans])
    68   apply blast
    69   done
    70 
    71 lemma HTT_lam: "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)"
    72   apply (rule HTTXH [THEN iff_trans])
    73   apply auto
    74   done
    75 
    76 lemmas HTT_rews1 = HTT_bot HTT_true HTT_false HTT_pair HTT_lam
    77 
    78 lemma HTT_rews2:
    79   "one : HTT"
    80   "inl(a) : HTT <-> a : HTT"
    81   "inr(b) : HTT <-> b : HTT"
    82   "zero : HTT"
    83   "succ(n) : HTT <-> n : HTT"
    84   "[] : HTT"
    85   "x$xs : HTT <-> x : HTT & xs : HTT"
    86   by (simp_all add: data_defs HTT_rews1)
    87 
    88 lemmas HTT_rews = HTT_rews1 HTT_rews2
    89 
    90 
    91 subsection {* Coinduction for HTT *}
    92 
    93 lemma HTT_coinduct: "[|  t : R;  R <= HTTgen(R) |] ==> t : HTT"
    94   apply (erule HTT_def [THEN def_coinduct])
    95   apply assumption
    96   done
    97 
    98 lemma HTT_coinduct3:
    99   "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"
   100   apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]])
   101   apply assumption
   102   done
   103 
   104 lemma HTTgenIs:
   105   "true : HTTgen(R)"
   106   "false : HTTgen(R)"
   107   "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)"
   108   "!!b. [| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)"
   109   "one : HTTgen(R)"
   110   "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
   111   "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
   112   "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
   113   "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
   114   "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
   115   "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>
   116     h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"
   117   unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+
   118 
   119 
   120 subsection {* Formation Rules for Types *}
   121 
   122 lemma UnitF: "Unit <= HTT"
   123   by (simp add: subsetXH UnitXH HTT_rews)
   124 
   125 lemma BoolF: "Bool <= HTT"
   126   by (fastsimp simp: subsetXH BoolXH iff: HTT_rews)
   127 
   128 lemma PlusF: "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT"
   129   by (fastsimp simp: subsetXH PlusXH iff: HTT_rews)
   130 
   131 lemma SigmaF: "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"
   132   by (fastsimp simp: subsetXH SgXH HTT_rews)
   133 
   134 
   135 (*** Formation Rules for Recursive types - using coinduction these only need ***)
   136 (***                                          exhaution rule for type-former ***)
   137 
   138 (*Proof by induction - needs induction rule for type*)
   139 lemma "Nat <= HTT"
   140   apply (simp add: subsetXH)
   141   apply clarify
   142   apply (erule Nat_ind)
   143    apply (fastsimp iff: HTT_rews)+
   144   done
   145 
   146 lemma NatF: "Nat <= HTT"
   147   apply clarify
   148   apply (erule HTT_coinduct3)
   149   apply (fast intro: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] dest: NatXH [THEN iffD1])
   150   done
   151 
   152 lemma ListF: "A <= HTT ==> List(A) <= HTT"
   153   apply clarify
   154   apply (erule HTT_coinduct3)
   155   apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI]
   156     subsetD [THEN HTTgen_mono [THEN ci3_AI]]
   157     dest: ListXH [THEN iffD1])
   158   done
   159 
   160 lemma ListsF: "A <= HTT ==> Lists(A) <= HTT"
   161   apply clarify
   162   apply (erule HTT_coinduct3)
   163   apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI]
   164     subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: ListsXH [THEN iffD1])
   165   done
   166 
   167 lemma IListsF: "A <= HTT ==> ILists(A) <= HTT"
   168   apply clarify
   169   apply (erule HTT_coinduct3)
   170   apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI]
   171     subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: IListsXH [THEN iffD1])
   172   done
   173 
   174 end