src/CCL/Hered.thy
changeset 27239 f2f42f9fa09d
parent 27208 5fe899199f85
child 28262 aa7ca36d67fd
equal deleted inserted replaced
27238:d2bf12727c8a 27239:f2f42f9fa09d
    95   apply (erule HTT_def [THEN def_coinduct])
    95   apply (erule HTT_def [THEN def_coinduct])
    96   apply assumption
    96   apply assumption
    97   done
    97   done
    98 
    98 
    99 ML {*
    99 ML {*
   100   fun HTT_coinduct_tac ctxt s i =
   100   fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
   101     RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
       
   102 *}
   101 *}
   103 
   102 
   104 lemma HTT_coinduct3:
   103 lemma HTT_coinduct3:
   105   "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"
   104   "[|  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]])
   105   apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]])
   109 
   108 
   110 ML {*
   109 ML {*
   111 val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
   110 val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
   112 
   111 
   113 fun HTT_coinduct3_tac ctxt s i =
   112 fun HTT_coinduct3_tac ctxt s i =
   114   RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
   113   res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
   115 
   114 
   116 val HTTgenIs =
   115 val HTTgenIs =
   117   map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   116   map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   118   ["true : HTTgen(R)",
   117   ["true : HTTgen(R)",
   119    "false : HTTgen(R)",
   118    "false : HTTgen(R)",