Up to index of Isabelle/HOL
theory Recdef(* Title: HOL/Recdef.thy ID: $Id: Recdef.thy,v 1.21 2005/08/09 09:44:38 nipkow Exp $ Author: Konrad Slind and Markus Wenzel, TU Muenchen *) header {* TFL: recursive function definitions *} theory Recdef imports Wellfounded_Relations Datatype uses ("../TFL/casesplit.ML") ("../TFL/utils.ML") ("../TFL/usyntax.ML") ("../TFL/dcterm.ML") ("../TFL/thms.ML") ("../TFL/rules.ML") ("../TFL/thry.ML") ("../TFL/tfl.ML") ("../TFL/post.ML") ("Tools/recdef_package.ML") begin 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 use "../TFL/casesplit.ML" use "../TFL/utils.ML" use "../TFL/usyntax.ML" use "../TFL/dcterm.ML" use "../TFL/thms.ML" use "../TFL/rules.ML" use "../TFL/thry.ML" use "../TFL/tfl.ML" use "../TFL/post.ML" use "Tools/recdef_package.ML" setup RecdefPackage.setup lemmas [recdef_simp] = inv_image_def measure_def lex_prod_def same_fst_def less_Suc_eq [THEN iffD2] lemmas [recdef_cong] = if_cong image_cong lemma let_cong [recdef_cong]: "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g" by (unfold Let_def) blast lemmas [recdef_wf] = wf_trancl wf_less_than wf_lex_prod wf_inv_image wf_measure wf_pred_nat wf_same_fst wf_empty (* The following should really go into Datatype or Finite_Set, but each one lacks the other theory as a parent . . . *) lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" by (rule set_ext, case_tac x, auto) instance option :: (finite) finite proof have "finite (UNIV :: 'a set)" by (rule finite) hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp also have "insert None (Some ` (UNIV :: 'a set)) = UNIV" by (rule insert_None_conv_UNIV) finally show "finite (UNIV :: 'a option set)" . qed end
lemma tfl_eq_True:
x = True --> x
lemma tfl_rev_eq_mp:
x = y --> y --> x
lemma tfl_simp_thm:
(x --> y) --> x = x' --> x' --> y
lemma tfl_P_imp_P_iff_True:
P ==> P = True
lemma tfl_imp_trans:
[| A --> B; B --> C |] ==> A --> C
lemma tfl_disj_assoc:
(a ∨ b) ∨ c == a ∨ b ∨ c
lemma tfl_disjE:
[| P ∨ Q; P --> R; Q --> R |] ==> R
lemma tfl_exE:
[| ∃x. P x; ∀x. P x --> Q |] ==> Q
lemmas
inv_image r f == {(x, y). (f x, f y) ∈ r}
measure == inv_image less_than
ra <*lex*> rb == {((a, b), a', b'). (a, a') ∈ ra ∨ a = a' ∧ (b, b') ∈ rb}
same_fst P R == {((x', y'), x, y). x' = x ∧ P x ∧ (y', y) ∈ R x}
m1 < n1 ∨ m1 = n1 ==> m1 < Suc n1
lemmas
inv_image r f == {(x, y). (f x, f y) ∈ r}
measure == inv_image less_than
ra <*lex*> rb == {((a, b), a', b'). (a, a') ∈ ra ∨ a = a' ∧ (b, b') ∈ rb}
same_fst P R == {((x', y'), x, y). x' = x ∧ P x ∧ (y', y) ∈ R x}
m1 < n1 ∨ m1 = n1 ==> m1 < Suc n1
lemmas
[| b = c; c ==> x = u; ¬ c ==> y = v |] ==> (if b then x else y) = (if c then u else v)
[| M = N; !!x. x ∈ N ==> f x = g x |] ==> f ` M = g ` N
lemmas
[| b = c; c ==> x = u; ¬ c ==> y = v |] ==> (if b then x else y) = (if c then u else v)
[| M = N; !!x. x ∈ N ==> f x = g x |] ==> f ` M = g ` N
lemma let_cong:
[| M = N; !!x. x = N ==> f x = g x |] ==> Let M f = Let N g
lemmas
wf r ==> wf (r+)
wf less_than
[| wf ra; wf rb |] ==> wf (ra <*lex*> rb)
wf r ==> wf (inv_image r f)
wf (measure f)
wf pred_nat
(!!x. P x ==> wf (R x)) ==> wf (same_fst P R)
wf {}
lemmas
wf r ==> wf (r+)
wf less_than
[| wf ra; wf rb |] ==> wf (ra <*lex*> rb)
wf r ==> wf (inv_image r f)
wf (measure f)
wf pred_nat
(!!x. P x ==> wf (R x)) ==> wf (same_fst P R)
wf {}
lemma insert_None_conv_UNIV:
insert None (range Some) = UNIV