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