src/HOL/BCV/Fixpoint.ML

Present.setup;

(*  Title:      HOL/BCV/Fixpoint.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1999 TUM
*)

goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd fix.tcs)));
by(asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]
                                addsplits [split_split]) 1);
by(Clarify_tac 1);
br ccontr 1;
by(Asm_full_simp_tac 1);
by(res_inst_tac[("x","0")] allE 1);
ba 1;
by(Clarify_tac 1);
by(rename_tac "next s0" 1);
by(subgoal_tac "!i. fst(f i) = next" 1);
by(eres_inst_tac[("x","%i. snd(f i)")] allE 1);
by(Asm_full_simp_tac 1);
by(Clarify_tac 1);
by(eres_inst_tac[("x","i")] allE 1);
by(eres_inst_tac[("x","i")] allE 1);
by(Force_tac 1);
br allI 1;
by(induct_tac "i" 1);
by(Asm_simp_tac 1);
by(eres_inst_tac[("x","n")] allE 1);
by(Auto_tac);
val fix_tc = result();

Goalw [wf_iff_no_infinite_down_chain RS eq_reflection]
 "[| wf{(t,s). s:A & next s = Some t & t ~= s}; \
\    !a:A. next a : option A; s:A |] ==> \
\ fix(next,s) = (case next s of None => False \
\                | Some t => if t=s then True else fix(next,t))";
by(stac (fix_tc RS (hd fix.rules)) 1);
by(Simp_tac 1);
by(Clarify_tac 1);
by(subgoal_tac "!i. f i : A" 1);
 by(Blast_tac 1);
br allI 1;
by(induct_tac "i" 1);
 by(Asm_simp_tac 1);
by(Auto_tac);
qed "fix_unfold";

(* Thm: next has fixpoint above s iff fix(next,s) *)

Goal "[| x = Some y; x : option A |] ==> y : A";
by(Blast_tac 1);
val lemma = result();

Goal
"[| acc L; \
\   !t:L. !s:L. next t = Some t & s <= t --> (? u. next s = Some u & u <= t); \
\   !a:L. next a : option L; !a:L. !b. next a = Some b --> a <= b |] \
\ ==> s:L --> fix(next,s) = (? t:L. s <= t & next t = Some t)";
by(subgoal_tac "wf{(y,x::'a::order). x : L & next x = Some y & y ~= x}" 1);
 by(full_simp_tac (simpset() addsimps [acc_def]) 2);
 be wf_subset 2;
 by(simp_tac (simpset() addsimps [order_less_le]) 2);
 by(blast_tac (claset() addDs [lemma]) 2);
by(res_inst_tac [("a","s")] wf_induct 1);
 ba 1;
by(Clarify_tac 1);
by(Full_simp_tac 1);
by(stac fix_unfold 1);
   ba 1;
  ba 1;
 ba 1;
by(split_tac [option.split] 1);
br conjI 1;
 by(thin_tac "!a:L. !b. next a = Some b --> a <= b" 1);
 by(Force_tac 1);
by(Clarify_tac 1);
by(split_tac [split_if] 1);
br conjI 1;
 by(Blast_tac 1);
by(Clarify_tac 1);
by(EVERY[etac allE 1, etac impE 1, etac impE 2, etac trans 3]);
  by(Blast_tac 1);
 be lemma 1;
 by(Blast_tac 1);
br iffI 1;
 by(blast_tac (claset() addIs [order_trans]) 1);
by(Clarify_tac 1);
by(EVERY[rtac bexI 1, atac 2, rtac conjI 1, atac 2]);
by(thin_tac "!a:L. !b. next a = Some b --> a <= b" 1);
by(Force_tac 1);
qed_spec_mp "fix_iff_has_fixpoint";


(* This lemma looks more pleasing to the eye, because of the monotonicity
assumption for next, instead of the strange assumption above.
However, function next as defined in DFAimpl is NOT monotone because
None is not required to be detected as early as possible. Thus the following
does not hold: sos <= tos & next sos = None ==> next tos = None

Goal
"[| wf{(y,x::'a::order). x : L & next x = Some y & y ~= x}; \
\   !t:L. !s:L. s <= t & next s = None --> next t = None; \
\   !t:L. !s:L. !u. s <= t & next s = Some u --> \
\                   next t = None | (? v. next t = Some v & u <= v); \
\   !a:L. next a : option L; !a:L. !b. next a = Some b --> a <= b |] \
\ ==> s:L --> fix(next,s) = (? t:L. s <= t & next t = Some t)";
by(res_inst_tac [("a","s")] wf_induct 1);
 ba 1;
by(Clarify_tac 1);
by(Full_simp_tac 1);
by(stac fix_unfold 1);
   ba 1;
  ba 1;
 ba 1;
by(split_tac [option.split] 1);
br conjI 1;
 by(blast_tac (claset() addDs [sym RS trans]) 1);
by(Clarify_tac 1);
by(split_tac [split_if] 1);
br conjI 1;
 by(Blast_tac 1);
by(Clarify_tac 1);
by(EVERY[etac allE 1, etac impE 1, etac impE 2, etac trans 3]);
  by(Blast_tac 1);
 be lemma 1;
 by(Blast_tac 1);
br iffI 1;
 by(subgoal_tac "next a ~= None" 1);
  by(Clarify_tac 1);
  by(EVERY[etac ballE 1, etac ballE 1, etac allE 1, etac impE 1,etac disjE 2]);
      br conjI 1;
       ba 1;
      ba 1;
     by(blast_tac (claset() addDs [sym RS trans]) 1);
    by(blast_tac (claset() addIs [order_trans]) 1);
   by(blast_tac (claset() addIs [order_trans]) 1);
  by(Blast_tac 1);
 br notI 1;
 by(Clarify_tac 1);
 by(blast_tac (claset() addDs [sym RS trans,lemma]) 1);
by(blast_tac (claset() addDs [sym RS trans]) 1);
qed_spec_mp "fix_iff_has_fixpoint";
*)