src/LCF/fix.ML
author clasohm
Wed Jun 29 12:03:41 1994 +0200 (1994-06-29)
changeset 442 13ac1fd0a14d
parent 231 cb6a24451544
child 645 77474875da92
permissions -rw-r--r--
added parentheses made necessary by change of constrain's precedence
clasohm@0
     1
signature FIX =
clasohm@0
     2
sig
clasohm@0
     3
  val adm_eq: thm
clasohm@0
     4
  val adm_not_eq_tr: thm
clasohm@0
     5
  val adm_not_not: thm
clasohm@0
     6
  val not_eq_TT: thm
clasohm@0
     7
  val not_eq_FF: thm
clasohm@0
     8
  val not_eq_UU: thm
clasohm@0
     9
  val induct2: thm
clasohm@0
    10
  val induct_tac: string -> int -> tactic
clasohm@0
    11
  val induct2_tac: string*string -> int -> tactic
clasohm@0
    12
end;
clasohm@0
    13
clasohm@0
    14
structure Fix:FIX =
clasohm@0
    15
struct
clasohm@0
    16
clasohm@442
    17
val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))"
clasohm@0
    18
	(fn _ => [rewrite_goals_tac [eq_def],
clasohm@0
    19
		  REPEAT(rstac[adm_conj,adm_less]1)]);
clasohm@0
    20
clasohm@0
    21
val adm_not_not = prove_goal LCF.thy "adm(P) ==> adm(%x.~~P(x))"
clasohm@0
    22
	(fn prems => [simp_tac (LCF_ss addsimps prems) 1]);
clasohm@0
    23
clasohm@0
    24
clasohm@0
    25
val tac = rtac tr_induct 1 THEN REPEAT(simp_tac LCF_ss 1);
clasohm@0
    26
clasohm@0
    27
val not_eq_TT = prove_goal LCF.thy "ALL p. ~p=TT <-> (p=FF | p=UU)"
clasohm@0
    28
	(fn _ => [tac]) RS spec;
clasohm@0
    29
clasohm@0
    30
val not_eq_FF = prove_goal LCF.thy "ALL p. ~p=FF <-> (p=TT | p=UU)"
clasohm@0
    31
	(fn _ => [tac]) RS spec;
clasohm@0
    32
clasohm@0
    33
val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)"
clasohm@0
    34
	(fn _ => [tac]) RS spec;
clasohm@0
    35
clasohm@0
    36
val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr.adm(%x. ~t(x)=p)"
clasohm@0
    37
	(fn _ => [rtac tr_induct 1,
clasohm@0
    38
	REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
clasohm@0
    39
               REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
clasohm@0
    40
clasohm@0
    41
val adm_lemmas = [adm_not_free,adm_eq,adm_less,adm_not_less,adm_not_eq_tr,
clasohm@0
    42
		  adm_conj,adm_disj,adm_imp,adm_all];
clasohm@0
    43
clasohm@0
    44
fun induct_tac v i = res_inst_tac[("f",v)] induct i THEN
clasohm@0
    45
		     REPEAT(rstac adm_lemmas i);
clasohm@0
    46
clasohm@0
    47
clasohm@0
    48
val least_FIX = prove_goal LCF.thy "f(p) = p ==> FIX(f) << p"
clasohm@0
    49
	(fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1,
clasohm@0
    50
			stac (prem RS sym) 1, etac less_ap_term 1]);
clasohm@0
    51
clasohm@0
    52
(*Generates unification messages for some reason*)
clasohm@0
    53
val lfp_is_FIX = prove_goal LCF.thy
clasohm@0
    54
	"[| f(p) = p; ALL q. f(q)=q --> p << q |] ==> p = FIX(f)"
clasohm@0
    55
	(fn [prem1,prem2] => [rtac less_anti_sym 1,
clasohm@0
    56
			      rtac (FIX_eq RS (prem2 RS spec RS mp)) 1,
clasohm@0
    57
			      rtac least_FIX 1, rtac prem1 1]);
clasohm@0
    58
clasohm@0
    59
val ffix = read_instantiate [("f","f::?'a=>?'a")] FIX_eq;
clasohm@0
    60
val gfix = read_instantiate [("f","g::?'a=>?'a")] FIX_eq;
clasohm@0
    61
val ss = LCF_ss addsimps [ffix,gfix];
clasohm@0
    62
clasohm@0
    63
(* Do not use prove_goal because the result is ?ed which leads to divergence
clasohm@0
    64
   when submitted as an argument to SIMP_THM *)
clasohm@0
    65
(*
clasohm@0
    66
local
lcp@231
    67
val thm = trivial(read_cterm(sign_of LCF.thy)
clasohm@0
    68
        ("<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)",propT));
clasohm@0
    69
val tac = EVERY1[rtac lfp_is_FIX, simp_tac ss,
clasohm@0
    70
	  strip_tac, simp_tac (LCF_ss addsimps [PROD_less]),
clasohm@0
    71
	  rtac conjI, rtac least_FIX, etac subst, rtac (FST RS sym),
clasohm@0
    72
	  rtac least_FIX, etac subst, rtac (SND RS sym)];
clasohm@0
    73
in
clasohm@0
    74
val Some(FIX_pair,_) = Sequence.pull(tapply(tac,thm));
clasohm@0
    75
end;
clasohm@0
    76
clasohm@0
    77
val FIX_pair_conj = SIMP_THM (LCF_ss addsimps [PROD_eq]) FIX_pair;
clasohm@0
    78
*)
clasohm@0
    79
val FIX_pair = prove_goal LCF.thy
clasohm@0
    80
  "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"
clasohm@0
    81
  (fn _ => [rtac lfp_is_FIX 1, simp_tac ss 1,
clasohm@0
    82
	  strip_tac 1, simp_tac (LCF_ss addsimps [PROD_less]) 1,
clasohm@0
    83
	  rtac conjI 1, rtac least_FIX 1, etac subst 1, rtac (FST RS sym) 1,
clasohm@0
    84
	  rtac least_FIX 1, etac subst 1, rtac (SND RS sym) 1]);
clasohm@0
    85
clasohm@0
    86
val FIX_pair_conj = rewrite_rule (map mk_meta_eq [PROD_eq,FST,SND]) FIX_pair;
clasohm@0
    87
clasohm@0
    88
val FIX1 = FIX_pair_conj RS conjunct1;
clasohm@0
    89
val FIX2 = FIX_pair_conj RS conjunct2;
clasohm@0
    90
clasohm@0
    91
val induct2 = prove_goal LCF.thy
clasohm@0
    92
	 "[| adm(%p.P(FST(p),SND(p))); P(UU::'a,UU::'b);\
clasohm@0
    93
\	     ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))"
clasohm@0
    94
	(fn prems => [EVERY1
clasohm@0
    95
	[res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)),
clasohm@0
    96
	 res_inst_tac [("f","f"),("g","g")] (standard(FIX2 RS ssubst)),
clasohm@0
    97
	 res_inst_tac [("f","%x. <f(FST(x)),g(SND(x))>")] induct,
clasohm@0
    98
	 rstac prems, simp_tac ss, rstac prems,
clasohm@0
    99
	 simp_tac (LCF_ss addsimps [expand_all_PROD]), rstac prems]]);
clasohm@0
   100
clasohm@0
   101
fun induct2_tac (f,g) i = res_inst_tac[("f",f),("g",g)] induct2 i THEN
clasohm@0
   102
		     REPEAT(rstac adm_lemmas i);
clasohm@0
   103
clasohm@0
   104
end;
clasohm@0
   105
clasohm@0
   106
open Fix;