Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Old_Recdef.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Old_Recdef.thy
    Author:     Konrad Slind and Markus Wenzel, TU Muenchen
*)

section \<open>TFL: recursive function definitions\<close>

theory Old_Recdef
imports Main
keywords
  "recdef" :: thy_defn and
  "permissive" "congs" "hints"
begin

subsection \<open>Lemmas for TFL\<close>

lemma tfl_wf_induct: "\R. wf R \
       (\<forall>P. (\<forall>x. (\<forall>y. (y,x)\<in>R \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))"
apply clarify
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
done

lemma tfl_cut_def: "cut f r x \ (\y. if (y,x) \ r then f y else undefined)"
  unfolding cut_def .

lemma tfl_cut_apply: "\f R. (x,a)\R \ (cut f R a)(x) = f(x)"
apply clarify
apply (rule cut_apply, assumption)
done

lemma tfl_wfrec:
     "\M R f. (f=wfrec R M) \ wf R \ (\x. f x = M (cut f R x) x)"
apply clarify
apply (erule wfrec)
done

lemma tfl_eq_True: "(x = True) \ x"
  by blast

lemma tfl_rev_eq_mp: "(x = y) \ y \ x"
  by blast

lemma tfl_simp_thm: "(x \ y) \ (x = x') \ (x' \ y)"
  by blast

lemma tfl_P_imp_P_iff_True: "P \ P = True"
  by blast

lemma tfl_imp_trans: "(A \ B) \ (B \ C) \ (A \ C)"
  by blast

lemma tfl_disj_assoc: "(a \ b) \ c \ a \ (b \ c)"
  by simp

lemma tfl_disjE: "P \ Q \ P \ R \ Q \ R \ R"
  by blast

lemma tfl_exE: "\x. P x \ \x. P x \ Q \ Q"
  by blast

ML_file \<open>old_recdef.ML\<close>

subsection \<open>Rule setup\<close>

lemmas [recdef_simp] =
  inv_image_def
  measure_def
  lex_prod_def
  same_fst_def
  less_Suc_eq [THEN iffD2]

lemmas [recdef_cong] =
  if_cong let_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong
  map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong

lemmas [recdef_wf] =
  wf_trancl
  wf_less_than
  wf_lex_prod
  wf_inv_image
  wf_measure
  wf_measures
  wf_pred_nat
  wf_same_fst
  wf_empty

end

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.