src/CCL/Hered.thy
changeset 27146 443c19953137
parent 20140 98acc6d0fab6
child 27208 5fe899199f85
equal deleted inserted replaced
27145:0337828b7815 27146:443c19953137
    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   local val HTT_coinduct = thm "HTT_coinduct"
   100   fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i
   101   in fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] HTT_coinduct i end
       
   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]])
   107   apply assumption
   106   apply assumption
   108   done
   107   done
   109 
   108 
   110 ML {*
   109 ML {*
   111 local
   110 val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
   112   val HTT_coinduct3 = thm "HTT_coinduct3"
       
   113   val HTTgen_def = thm "HTTgen_def"
       
   114 in
       
   115 
   111 
   116 val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3
   112 fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i
   117 
       
   118 fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i
       
   119 
   113 
   120 val HTTgenIs =
   114 val HTTgenIs =
   121   map (mk_genIs (the_context ()) (thms "data_defs") (thm "HTTgenXH") (thm "HTTgen_mono"))
   115   map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   122   ["true : HTTgen(R)",
   116   ["true : HTTgen(R)",
   123    "false : HTTgen(R)",
   117    "false : HTTgen(R)",
   124    "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
   118    "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
   125    "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
   119    "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
   126    "one : HTTgen(R)",
   120    "one : HTTgen(R)",
   128    "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   122    "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   129    "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   123    "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   130    "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   124    "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   131    "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   125    "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
   132    "[| 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))"]
   126    "[| 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))"]
   133 
       
   134 end
       
   135 *}
   127 *}
   136 
   128 
   137 ML {* bind_thms ("HTTgenIs", HTTgenIs) *}
   129 ML {* bind_thms ("HTTgenIs", HTTgenIs) *}
   138 
   130 
   139 
   131