src/HOL/Modelcheck/MuckeSyn.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16429 e871f4b1a4f0
child 17272 c63e5220ed77
permissions -rw-r--r--
Constant "If" is now local
     1 
     2 (* $Id$ *)
     3 
     4 (* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
     5    it yields innermost one. If no Mu term is present, search_mu yields NONE
     6 *)
     7 
     8 (* extended for treatment of nu (TH) *)
     9 fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = 
    10 	(case (search_mu t2) of
    11 	      SOME t => SOME t 
    12 	    | NONE => SOME ((Const("MuCalculus.mu",tp)) $ t2))
    13   | search_mu ((Const("MuCalculus.nu",tp)) $ t2) =
    14         (case (search_mu t2) of
    15               SOME t => SOME t
    16             | NONE => SOME ((Const("MuCalculus.nu",tp)) $ t2))
    17   | search_mu (t1 $ t2) = 
    18 	(case (search_mu t1) of
    19 	      SOME t => SOME t 
    20 	    | NONE     => search_mu t2)
    21   | search_mu (Abs(_,_,t)) = search_mu t
    22   | search_mu _ = NONE;
    23 
    24 
    25 
    26 
    27 (* seraching a variable in a term. Used in move_mus to extract the
    28    term-rep of var b in hthm *)
    29 
    30 fun search_var s t =
    31 case t of
    32      t1 $ t2 => (case (search_var s t1) of
    33 		             SOME tt => SOME tt |
    34 			     NONE => search_var s t2) |
    35      Abs(_,_,t) => search_var s t |
    36      Var((s1,_),_) => if s = s1 then SOME t else NONE |
    37      _ => NONE;
    38 	
    39 
    40 (* function move_mus:
    41    Mucke can't deal with nested Mu terms. move_mus i searches for 
    42    Mu terms in the subgoal i and replaces Mu terms in the conclusion
    43    by constants and definitions in the premises recursively.
    44 
    45    move_thm is the theorem the performs the replacement. To create NEW
    46    names for the Mu terms, the indizes of move_thm are incremented by
    47    max_idx of the subgoal.
    48 *)
    49 
    50 local
    51 
    52   val move_thm = prove_goal MuckeSyn.thy "[| a = b ==> P a; a = b |] ==> P b"
    53 	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
    54 		     REPEAT (resolve_tac prems 1)]);
    55 
    56   val sig_move_thm = #sign (rep_thm move_thm);
    57   val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
    58   val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
    59 
    60 in
    61 
    62 fun move_mus i state =
    63 let val sign = #sign (rep_thm state);
    64     val (subgoal::_) = Library.drop(i-1,prems_of state);
    65     val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
    66     val redex = search_mu concl;
    67     val idx = let val t = #maxidx (rep_thm state) in 
    68 	      if t < 0 then 1 else t+1 end;
    69 in
    70 case redex of
    71      NONE => all_tac state |
    72      SOME redexterm => 
    73 	let val Credex = cterm_of sign redexterm;
    74 	    val aiCterm = 
    75 		cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm));
    76 	    val inst_move_thm = cterm_instantiate 
    77 				[(bCterm,Credex),(aCterm,aiCterm)] move_thm;
    78 	in
    79             ((rtac inst_move_thm i) THEN (dtac eq_reflection i) 
    80 		THEN (move_mus i)) state
    81 	end
    82 end; (* outer let *)
    83 end; (* local *)
    84 
    85 
    86 (* Type of call_mucke_tac has changed: an argument t of type thy was inserted (TH); *)
    87 (* Normally t can be user-instantiated by the value thy of the Isabelle context     *)
    88 fun call_mucke_tac i state =
    89 let val sign = #sign (rep_thm state);
    90     val (subgoal::_) = Library.drop(i-1,prems_of state);
    91     val OraAss = invoke_oracle MuckeSyn.thy "Mucke" (sign,MuckeOracleExn (subgoal));
    92 in 
    93 (cut_facts_tac [OraAss] i) state
    94 end;
    95 
    96 
    97 (* transforming fun-defs into lambda-defs *)
    98 
    99 val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
   100  by (rtac (extensional eq) 1);
   101 qed "ext_rl";
   102 
   103 infix cc;
   104 
   105 fun NONE cc xl = xl
   106   | (SOME x) cc xl = x::xl;
   107 
   108 fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z
   109   | getargs (x $ (Var ((y,_),_))) = y;
   110 
   111 fun getfun ((x $ y) $ z) = getfun (x $ y)
   112   | getfun (x $ _) = x;
   113 
   114 local
   115 
   116 fun is_prefix [] s = true
   117 | is_prefix (p::ps) [] = false
   118 | is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
   119 
   120 fun delete_bold [] = []
   121 | delete_bold (x::xs) = if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
   122         then (let val (_::_::_::s) = xs in delete_bold s end)
   123         else (if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs))
   124                 then  (let val (_::_::_::s) = xs in delete_bold s end)
   125                 else (x::delete_bold xs));
   126 
   127 fun delete_bold_string s = implode(delete_bold (explode s));
   128 
   129 in
   130 
   131 (* extension with removing bold font (TH) *)
   132 fun mk_lam_def (_::_) _ _ = NONE  
   133   | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
   134   | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
   135     let val thy = theory_of_thm t;
   136 	val fnam = Sign.string_of_term thy (getfun LHS);
   137 	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
   138 	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
   139     in
   140 	SOME (prove_goal thy gl (fn prems =>
   141   		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
   142     end
   143 | mk_lam_def [] _ t= NONE; 
   144 
   145 fun mk_lam_defs ([]:thm list) = ([]: thm list) 
   146   | mk_lam_defs (t::l) = 
   147       (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l);
   148 
   149 end;
   150 
   151 (* first simplification, then model checking *)
   152 
   153 goalw (theory "Product_Type") [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
   154   by (rtac ext 1);
   155   by (stac (surjective_pairing RS sym) 1);
   156   by (rtac refl 1);
   157 qed "pair_eta_expand";
   158 
   159 val pair_eta_expand_proc =
   160   Simplifier.simproc (Theory.sign_of (the_context ()))
   161     "pair_eta_expand" ["f::'a*'b=>'c"]
   162     (fn _ => fn _ => fn t =>
   163       case t of Abs _ => SOME (mk_meta_eq pair_eta_expand)
   164       | _ => NONE);
   165 
   166 val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
   167 
   168 
   169 (* the interface *)
   170 
   171 fun mc_mucke_tac defs i state =
   172   (case Library.drop (i - 1, Thm.prems_of state) of
   173     [] => no_tac state
   174   | subgoal :: _ =>
   175       EVERY [
   176         REPEAT (etac thin_rl i),
   177         cut_facts_tac (mk_lam_defs defs) i,
   178         full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
   179         move_mus i, call_mucke_tac i,atac i,
   180         REPEAT (rtac refl i)] state);
   181 
   182 (*check if user has mucke installed*)
   183 fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
   184 fun if_mucke_enabled f x = if mucke_enabled () then f x else ();