src/HOL/Modelcheck/MuckeSyn.ML
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18443 a1d53af4c4c7
child 20257 ebe183ff903d
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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 (the_context ()) "[| 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;
    83 end;
    84 
    85 
    86 fun call_mucke_tac i state =
    87 let val thy = Thm.theory_of_thm state;
    88     val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
    89 in 
    90 (cut_facts_tac [OraAss] i) state
    91 end;
    92 
    93 
    94 (* transforming fun-defs into lambda-defs *)
    95 
    96 val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
    97  by (rtac (extensional eq) 1);
    98 qed "ext_rl";
    99 
   100 infix cc;
   101 
   102 fun NONE cc xl = xl
   103   | (SOME x) cc xl = x::xl;
   104 
   105 fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z
   106   | getargs (x $ (Var ((y,_),_))) = y;
   107 
   108 fun getfun ((x $ y) $ z) = getfun (x $ y)
   109   | getfun (x $ _) = x;
   110 
   111 local
   112 
   113 fun delete_bold [] = []
   114 | delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
   115         then (let val (_::_::_::s) = xs in delete_bold s end)
   116         else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
   117                 then  (let val (_::_::_::s) = xs in delete_bold s end)
   118                 else (x::delete_bold xs));
   119 
   120 fun delete_bold_string s = implode(delete_bold (explode s));
   121 
   122 in
   123 
   124 (* extension with removing bold font (TH) *)
   125 fun mk_lam_def (_::_) _ _ = NONE  
   126   | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
   127   | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
   128     let val thy = theory_of_thm t;
   129 	val fnam = Sign.string_of_term thy (getfun LHS);
   130 	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
   131 	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
   132     in
   133 	SOME (prove_goal thy gl (fn prems =>
   134   		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
   135     end
   136 | mk_lam_def [] _ t= NONE; 
   137 
   138 fun mk_lam_defs ([]:thm list) = ([]: thm list) 
   139   | mk_lam_defs (t::l) = 
   140       (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l);
   141 
   142 end;
   143 
   144 (* first simplification, then model checking *)
   145 
   146 goalw (theory "Product_Type") [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
   147   by (rtac ext 1);
   148   by (stac (surjective_pairing RS sym) 1);
   149   by (rtac refl 1);
   150 qed "pair_eta_expand";
   151 
   152 val pair_eta_expand_proc =
   153   Simplifier.simproc (Theory.sign_of (the_context ()))
   154     "pair_eta_expand" ["f::'a*'b=>'c"]
   155     (fn _ => fn _ => fn t =>
   156       case t of Abs _ => SOME (mk_meta_eq pair_eta_expand)
   157       | _ => NONE);
   158 
   159 val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
   160 
   161 
   162 (* the interface *)
   163 
   164 fun mc_mucke_tac defs i state =
   165   (case Library.drop (i - 1, Thm.prems_of state) of
   166     [] => no_tac state
   167   | subgoal :: _ =>
   168       EVERY [
   169         REPEAT (etac thin_rl i),
   170         cut_facts_tac (mk_lam_defs defs) i,
   171         full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
   172         move_mus i, call_mucke_tac i,atac i,
   173         REPEAT (rtac refl i)] state);
   174 
   175 (*check if user has mucke installed*)
   176 fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
   177 fun if_mucke_enabled f x = if mucke_enabled () then f x else ();