Well-Founded Recursion
Overview
This is a proof of the recursion theorem for well-founded recursive definitions. It is modelled on Tobias Nipkow's proof for Isabelle HOL and uses relations modelled with ProofPower HOL's SET type constructor.
Introduction
A new "wf_rec" theory is created as a child of "wf_rel". Probably
Well-Founded Recursion
In this section is proved the theorem which justifies well-founded recursive definitions.
Recursive Definition
Proof Context
In this section I will create a decent proof context for recursive definitions, eventually.
Listing of Theory wf_rec
Introduction
A new "wf_rec" theory is created as a child of "wf_rel". Probably
The Theory wf_rec
The new theory is first created, together with a proof context which we will build up as we develop the theory.
xl-sml
open_theory "wf_rel";
force_new_theory "wf_rec";
force_new_pc "wf_rec";
merge_pcs ["xl_cs_∃_conv"] "wf_rec";
set_merge_pcs ["hol", "'bin_rel", "wf_rec"];

Well-Founded Recursion
In this section is proved the theorem which justifies well-founded recursive definitions.
Introduction

The idea here is that a recursive equation is represented by a functional, which is obtained by abstracting the right hand side of the equation on the name of the function. We need to demonstrate that definitions using such a functional have unique solutions.

Is RecFun
is_recfun is the set of 4-tuples <r,a,H,f> such that f solves the recursion equations represented by H for values which are in the left image of a under R. (following Tobias Nipkow)
xl-holconst
is_recfun: (('a × 'a)SET × 'a × (('a × ('a × 'a)SET) → 'a) × ('a × 'a)SET)SET
∀ r a H f •
ftbr (r,a,H,f) ∈ is_recfun ≡ f = {(x,y)|
fttab(x,a) ∈ r ∧
fttaby = H(x, {(v,w)| (v,w) ∈ f ∧ (v,x) ∈ r})
fttab}
Restriction Intersection
The following lemma states that two restriced recursive functions agree over their intersection.
xl-sml
set_goal([],⌜∀r H a f b g• r ∈ twf
fttab∧ (r,a,H,f) ∈ is_recfun
fttab∧ (r,b,H,g) ∈ is_recfun
fttab⇒ ∀x• (x,a)∈r ∧ (x,b)∈r ⇒ ∀y•(x,y)∈f ≡ (x,y)∈g⌝);
a (rewrite_tac(map get_spec [⌜twf⌝, ⌜wf⌝, ⌜is_recfun⌝]));
a (REPEAT_N 7 strip_tac);
a (spec_nth_asm_tac 4 ⌜{x | (x, a) ∈ r ∧ (x, b) ∈ r ⇒ ∀y•(x,y)∈f ≡ (x,y)∈g}⌝);
(* *** Goal "1" *** *)
a (SWAP_NTH_ASM_CONCL_T 1 discard_tac);
a (all_asm_ante_tac THEN REPEAT_N 5 strip_tac);
a (once_asm_rewrite_tac[]);
a (rewrite_tac[] THEN REPEAT strip_tac);
a (DROP_NTH_ASM_T 1 rewrite_thm_tac);
a (LEMMA_T ⌜{(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r}
ftbr = {(v, w)|(v, w) ∈ g ∧ (v, x) ∈ r}⌝
fttabrewrite_thm_tac);
a (rewrite_tac[bin_rel_ext_clauses]);
a (REPEAT strip_tac);
a (spec_nth_asm_tac 5 ⌜x'⌝
ftbr THEN all_asm_fc_tac[]);
a (spec_nth_asm_tac 5 ⌜x'⌝
ftbr THEN all_asm_fc_tac[]);
a (spec_nth_asm_tac 3 ⌜y⌝);
(* *** Goal "2" *** *)
a (SWAP_NTH_ASM_CONCL_T 1 discard_tac);
a (all_asm_ante_tac THEN REPEAT_N 5 strip_tac);
a (once_asm_rewrite_tac[]);
a (rewrite_tac[] THEN REPEAT strip_tac);
a (DROP_NTH_ASM_T 1 rewrite_thm_tac);
a (LEMMA_T ⌜{(v, w)|(v, w) ∈ g ∧ (v, x) ∈ r}
ftbr = {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r}⌝
fttabrewrite_thm_tac);
a (rewrite_tac[bin_rel_ext_clauses]);
a (REPEAT strip_tac);
a (spec_nth_asm_tac 5 ⌜x'⌝
ftbr THEN all_asm_fc_tac[]);
a (spec_nth_asm_tac 3 ⌜y⌝);
a (spec_nth_asm_tac 5 ⌜x'⌝
ftbr THEN all_asm_fc_tac[]);
(* *** Goal "3" *** *)
a (strip_tac THEN strip_tac);
a (spec_nth_asm_tac 3 ⌜x⌝);
val ri_lemma = save_pop_thm "ri_lemma";

Restrict Unique
An immediate corrolory is that there is only one restricted recursive function at any point. First, however we prove a lemma about the domain of a restricted recursive function.
xl-sml
set_goal([],⌜∀r a H f• (r,a,H,f) ∈ is_recfun
fttab⇒ Dom f = {x | (x,a) ∈ r}⌝);
a (REPEAT strip_tac);
a (strip_asm_tac (list_∀_elim [⌜r⌝,⌜a⌝,⌜H⌝,⌜f⌝] (get_spec ⌜is_recfun⌝)));
a (once_asm_rewrite_tac[] THEN rewrite_tac[sets_ext_clauses, ∈_in_clauses]);
a (once_asm_rewrite_tac[]);
a (prove_tac[sets_ext_clauses, ∈_in_clauses]);
val recfun_Dom_thm = save_pop_thm "recfun_Dom_thm";


xl-sml
set_goal([],⌜∀r H a f g• r ∈ twf
fttab∧ (r,a,H,f) ∈ is_recfun
fttab∧ (r,a,H,g) ∈ is_recfun
fttab⇒ f = g⌝);
a (REPEAT strip_tac);
a (strip_asm_tac (list_∀_elim [⌜r⌝,⌜H⌝,⌜a⌝,⌜f⌝,⌜a⌝,⌜g⌝] ri_lemma));
a (pure_rewrite_tac [rel_ext_Dom_thm]);
a (FC_T rewrite_tac [recfun_Dom_thm]);
a (asm_prove_tac[]);
val recfun_unique_thm = save_pop_thm "recfun_unique_thm";


xl-sml
set_goal([],⌜∀r H a f b g• r ∈ twf
fttab∧ (r,a,H,f) ∈ is_recfun
fttab∧ (r,b,H,g) ∈ is_recfun
fttab∧ (a,b) ∈ r
fttab⇒ f = (Dom f) ⊲ g⌝);
a (REPEAT strip_tac);
a (strip_asm_tac (list_∀_elim [⌜r⌝,⌜H⌝,⌜a⌝,⌜f⌝,⌜b⌝,⌜g⌝] ri_lemma));
a (fc_tac [recfun_Dom_thm, get_spec ⌜twf⌝]);
a (pure_asm_rewrite_tac [rel_ext_Dom_thm, Dom_rest_thm]);
a (rewrite_tac [rel_ext_Dom_thm, sets_ext_clauses, ∈_in_clauses]);
a (REPEAT strip_tac THEN_TRY all_asm_fc_tac[]);
a (spec_asm_tac
fttab⌜∀ x• (x, a) ∈ r ∧ (x, b) ∈ r ⇒ (∀ y• (x, y) ∈ f ≡ (x, y) ∈ g)⌝
fttab⌜x⌝);
a (asm_rewrite_tac[]);
val recfun_restr_lemma = save_pop_thm "recfun_restr_lemma";


xl-sml
set_goal([],⌜∀r H a f b• r ∈ twf
fttab∧ (r,a,H,f) ∈ is_recfun
fttab∧ (b,a) ∈ r
fttab⇒ (r,b,H,{(v,w) | (v,w) ∈ f ∧ (v,b) ∈ r}) ∈ is_recfun⌝);
a (REPEAT strip_tac);
a (rewrite_tac [get_spec⌜is_recfun⌝, bin_rel_ext_clauses, ∈_in_clauses]);
a (fc_tac [get_spec⌜is_recfun⌝]);
a (REPEAT_N 4 strip_tac);
(* *** Goal "1" *** *)
a (GET_NTH_ASM_T 1 (fn asm=>STRIP_T (fn x => strip_asm_tac(once_rewrite_rule[asm]x))));
a (REPEAT strip_tac);
a (lemma_tac ⌜{(v, w)|((v, w) ∈ f ∧ (v, b) ∈ r) ∧ (v, x) ∈ r} = {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r}⌝
fttabTHEN1 (rewrite_tac [bin_rel_ext_clauses,∈_in_clauses]));
(* *** Goal "1.1" *** *)
a (REPEAT strip_tac);
a (fc_tac [get_spec⌜twf⌝,get_spec⌜Transitive⌝]);
a (all_asm_fc_tac[]);
(* *** Goal "1.2" *** *)
a (pure_once_asm_rewrite_tac[]);
a (rewrite_tac[]);
(* *** Goal "2" *** *)
a (REPEAT strip_tac);
a (once_asm_rewrite_tac[]);
a (rewrite_tac[]);
a (REPEAT strip_tac);
(* *** Goal "2.1" *** *)
a (fc_tac [get_spec⌜twf⌝,get_spec⌜Transitive⌝]);
a (all_asm_fc_tac[]);
(* *** Goal "2.2" *** *)
a (lemma_tac ⌜{(v, w)|((v, w) ∈ f ∧ (v, b) ∈ r) ∧ (v, x) ∈ r} = {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r}⌝
fttabTHEN1 (rewrite_tac [bin_rel_ext_clauses,∈_in_clauses]));
(* *** Goal "2.2.1" *** *)
a (REPEAT strip_tac);
a (fc_tac [get_spec⌜twf⌝,get_spec⌜Transitive⌝]);
a (all_asm_fc_tac[]);
(* *** Goal "2.2.2" *** *)
a (GET_NTH_ASM_T 1 (fn x=> pure_once_rewrite_tac[x]));
a (rewrite_tac[]);
val restr_is_recfun_lemma = save_pop_thm "restr_is_recfun_lemma";

Now the big one:
xl-sml
set_goal([],⌜∀H R a• R ∈ twf ⇒ ∃f• (R, a, H, f) ∈ is_recfun⌝);
a (REPEAT strip_tac);
a (fc_tac[get_spec⌜twf⌝]);
a (strip_asm_tac (∀_elim ⌜R⌝ (get_spec⌜wf⌝))
fttabTHEN1 REPEAT (all_asm_fc_tac[]));
a (spec_nth_asm_tac 1 ⌜{z|∃ f• (R, z, H, f) ∈ is_recfun}⌝);
(* *** Goal "1" *** *)
a (SWAP_NTH_ASM_CONCL_T 1 discard_tac THEN strip_tac);
a (lemma_tac ⌜∃g• g = { (v,w) | (v,x) ∈ R ∧
fttab∃h• (R,v,H,h) ∈ is_recfun ∧ w = H(v,h)}⌝
fttabTHEN1 prove_∃_tac);
a (∃_tac ⌜g⌝);
a (rewrite_tac[get_spec ⌜is_recfun⌝, bin_rel_ext_clauses, ∈_in_clauses]);
a (REPEAT strip_tac);
(* *** Goal "1.1" *** *)
a (asm_ante_tac ⌜(x', y) ∈ g⌝);
a (asm_rewrite_tac[] THEN REPEAT strip_tac);
(* *** Goal "1.2" *** *)
a (swap_asm_concl_tac ⌜(x', y) ∈ g⌝);
a (asm_rewrite_tac[] THEN swap_nth_asm_concl_tac 1);
a (spec_nth_asm_tac 5 ⌜x'⌝);
a (lemma_tac ⌜h={(v, w)|(v, w) ∈ g ∧ (v, x') ∈ R}⌝);
(* *** Goal "1.2.1" *** *)
a (asm_rewrite_tac[bin_rel_ext_clauses, ∈_in_clauses]);
a (strip_tac THEN strip_tac THEN asm_rewrite_tac[]);
a (FC_T once_rewrite_tac [get_spec⌜is_recfun⌝]);
a (rewrite_tac[]);
a (REPEAT strip_tac);
(* *** Goal "1.2.1.1" *** *)
a (all_asm_fc_tac[]);
(* *** Goal "1.2.1.2" *** *)
a (∃_tac ⌜{(v, w)|(v, w) ∈ h ∧ (v, x'') ∈ R}⌝
fttabTHEN asm_rewrite_tac[]);
a (strip_asm_tac (list_∀_elim [⌜R⌝,⌜H⌝,⌜x'⌝,⌜h⌝,⌜x''⌝] restr_is_recfun_lemma));
(* *** Goal "1.2.1.3" *** *)
a (lemma_tac ⌜(R,x'',H,{(v, w)|(v, w) ∈ h ∧ (v, x'') ∈ R}) ∈ is_recfun⌝
fttabTHEN1 (strip_asm_tac (list_∀_elim [⌜R⌝,⌜H⌝,⌜x'⌝,⌜h⌝,⌜x''⌝] restr_is_recfun_lemma)));
a (strip_asm_tac (list_∀_elim
fttab[⌜R⌝,⌜H⌝,⌜x''⌝,⌜{(v, w)|(v, w) ∈ h ∧ (v, x'') ∈ R}⌝,⌜h'⌝]
fttabrecfun_unique_thm));
a (asm_rewrite_tac[]);
(* *** Goal "1.2.2" *** *)
a (asm_ante_tac ⌜y = H (x', h)⌝);
a (GET_ASM_T ⌜h = {(v, w)|(v, w) ∈ g ∧ (v, x') ∈ R}⌝
fttabrewrite_thm_tac);
(* *** Goal "1.3" *** *)
a (asm_rewrite_tac[]);
a (spec_asm_tac ⌜∀ y• (y, x) ∈ R ⇒ y ∈ {z|∃ f• (R, z, H, f) ∈ is_recfun}⌝
fttab⌜x'⌝);
a (∃_tac ⌜f⌝ THEN asm_rewrite_tac[]);
a (lemma_tac ⌜{(v, w)
ftbr |((v, x) ∈ R
ftbr ∧ (∃ h• (R, v, H, h) ∈ is_recfun ∧ w = H (v, h)))
ftbr ∧ (v, x') ∈ R} = f⌝);
(* *** Goal "1.3.1" *** *)
a (rewrite_tac[bin_rel_ext_clauses]);
a (REPEAT strip_tac);
(* *** Goal "1.3.1.1" *** *)
a (all_fc_tac [recfun_restr_lemma]);
a (all_fc_tac [recfun_Dom_thm]);
a (all_fc_tac [get_spec ⌜is_recfun⌝]);
a (once_asm_rewrite_tac[]);
a (rewrite_tac[∈_in_clauses]);
(*a (once_asm_rewrite_tac[]);*)
a (lemma_tac ⌜{(v, w)|(v, w) ∈ f ∧ (v, x'') ∈ R} = h⌝);
a ((POP_ASM_T discard_tac) THEN (POP_ASM_T discard_tac)
fttabTHEN once_asm_rewrite_tac[]);
a (GET_ASM_T ⌜Dom h = {x|(x, x'') ∈ R}⌝ pure_rewrite_thm_tac);
a (prove_tac[bin_rel_ext_clauses]);
a (POP_ASM_T rewrite_thm_tac THEN strip_tac);
(* *** Goal "1.3.1.2" *** *)
a (POP_ASM_T ante_tac);
a (ALL_FC_T (MAP_EVERY ante_tac) [recfun_Dom_thm]);
a (rewrite_tac[sets_ext_clauses]);
a (REPEAT strip_tac);
a (spec_asm_tac ⌜∀ x• (∃ y• (x, y) ∈ f) ≡ (x, x') ∈ R⌝
fttab⌜x''⌝);
(* *** Goal "1.3.1.2.1" *** *)
a (REPEAT (asm_fc_tac[]));
a (REPEAT (asm_fc_tac[]));
a (REPEAT (asm_fc_tac[]));
(* *** Goal "1.3.1.3" *** *)
a (∃_tac ⌜{(x,y)| (x,y) ∈ f ∧ (x,x'') ∈ R}⌝ THEN REPEAT strip_tac);
(* *** Goal "1.3.1.3.1" *** *)
a (ALL_FC_T
fttab(MAP_EVERY(asm_tac o (rewrite_rule[sets_ext_clauses])))
fttab[recfun_Dom_thm]);
a (spec_asm_tac ⌜∀ x• (∃ y• (x, y) ∈ f) ≡ (x, x') ∈ R⌝ ⌜x''⌝);
a (asm_fc_tac[]);
a (asm_fc_tac[]);
a (all_fc_tac [restr_is_recfun_lemma]);
(* *** Goal "1.3.1.3.2" *** *)
a (ALL_FC_T (MAP_EVERY ante_tac) [get_spec ⌜is_recfun⌝]);
a (POP_ASM_T (fn a=> STRIP_T (fn h=> ante_tac (once_rewrite_rule[h]a))));
a (rewrite_tac [∈_in_clauses]);
a (strip_tac);
(* *** Goal "1.3.1.4" *** *)
a (ALL_FC_T
fttab(MAP_EVERY(asm_tac o (rewrite_rule[sets_ext_clauses])))
fttab[recfun_Dom_thm]);
a (spec_asm_tac ⌜∀ x• (∃ y• (x, y) ∈ f) ≡ (x, x') ∈ R⌝ ⌜x''⌝);
a (asm_fc_tac[]);
a (asm_fc_tac[]);
(* *** Goal "1.3.2" *** *)
a (asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (spec_asm_tac ⌜∀ x• x ∈ {z|∃ f• (R, z, H, f) ∈ is_recfun}⌝ ⌜a⌝);
a (∃_tac ⌜f⌝ THEN strip_tac);
val exists_recfun_thm = save_pop_thm "exists_recfun_thm";


xl-sml
set_goal([],⌜∃ the_recfun
ftbr • ∀ r a H• r ∈ twf ⇒ (r, a, H, the_recfun (r, a, H)) ∈ is_recfun⌝);
a (PC_T "hol" prove_∃_tac THEN strip_tac);
a (∃_tac ⌜εrecfun• Fst x ∈ twf
ftbr ⇒ (Fst x, Fst (Snd x), Snd (Snd x), recfun) ∈ is_recfun⌝);
a strip_tac;
a (fc_tac[list_∀_elim [⌜Snd(Snd x)⌝,⌜Fst x⌝,⌜Fst (Snd x)⌝] exists_recfun_thm]);
a (all_ε_tac);
a (∃_tac ⌜f⌝ THEN asm_rewrite_tac[]);
val recfun_consistent = top_thm();
xl_set_cs_∃_thm (pop_thm());


xl-holconst
the_recfun: (('a × 'a)SET × 'a × (('a × ('a × 'a)SET) → 'a)) → ('a × 'a)SET
∀ r a H• r ∈ twf ⇒ (r,a,H,the_recfun(r,a,H)) ∈ is_recfun
We now define the function wftrec which delivers a solution to a recursion functional.
xl-holconst
wftrecfun: (('a × 'a)SET × (('a × ('a × 'a)SET) → 'a)) → ('a × 'a)SET
∀ r H• wftrecfun (r,H) = {(a,v) | v = H(a,the_recfun(r,a,H))}
The following theorem shows that this is indeed a fixed-point.
xl-holconst
wftrec: (('a × 'a)SET × 'a × (('a × ('a × 'a)SET) → 'a)) → 'a
∀ r a H• wftrec (r,a,H) = H(a,the_recfun(r,a,H))
Recursion Theorem
Proof Context
In this section I will create a decent proof context for recursive definitions, eventually.
Proof Context

xl-sml
(* commit_pc "wf_rec"; *)

up quick index © RBJ

privacy policy

Created:

$Id: WfRec.xml,v 1.4 2008/04/15 18:21:36 rbj01 Exp $

V