src/HOL/Modelcheck/MuckeSyn.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 22819 a7b425bb668c
child 26342 0f65fa163304
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:      HOL/Modelcheck/MuckeSyn.thy
     2     ID:         $Id$
     3     Author:     Tobias Hamberger
     4     Copyright   1999  TU Muenchen
     5 *)
     6 
     7 theory MuckeSyn
     8 imports MuCalculus
     9 uses "mucke_oracle.ML"
    10 begin
    11 
    12 (* extended with some operators and case treatment (which requires postprocessing with
    13 transform_case (from MuCalculus) (TH) *)
    14 
    15 nonterminals
    16   mutype
    17   decl decls
    18   cases_syn case_syn
    19 
    20 syntax (Mucke output)
    21   True          :: bool                                 ("true")
    22   False         :: bool                                 ("false")
    23   Not           :: "bool => bool"                       ("! _" [40] 40)
    24   If            :: "[bool, 'a, 'a] => 'a"       ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
    25 
    26   "op &"        :: "[bool, bool] => bool"               (infixr "&" 35)
    27   "op |"        :: "[bool, bool] => bool"               (infixr "|" 30)
    28   "op -->"      :: "[bool, bool] => bool"               (infixr "->" 25)
    29   "op ="        :: "['a, 'a] => bool"                   ("(_ =/ _)" [51, 51] 50)
    30   "_not_equal"  :: "['a, 'a] => bool"                   ("(_ !=/ _)" [51, 51] 50)
    31 
    32   All_binder    :: "[idts, bool] => bool"               ("'((3forall _./ _)')" [0, 10] 10)
    33   Ex_binder     :: "[idts, bool] => bool"               ("'((3exists _./ _)')" [0, 10] 10)
    34 
    35   "_lambda"     :: "[idts, 'a] => 'b"                   ("(3L _./ _)" 10)
    36   "_applC"      :: "[('b => 'a), cargs] => aprop"       ("(1_/ '(_'))" [1000,1000] 999)
    37   "_cargs"      :: "['a, cargs] => cargs"               ("_,/ _" [1000,1000] 1000)
    38 
    39   "_idts"       :: "[idt, idts] => idts"                ("_,/ _" [1, 0] 0)
    40 
    41   "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
    42 (* "@pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
    43   "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/ _" [1, 0] 0) *)
    44 
    45   "_decl"       :: "[mutype,pttrn] => decl"             ("_ _")
    46   "_decls"      :: "[decl,decls] => decls"              ("_,/ _")
    47   ""            :: "decl => decls"                      ("_")
    48   "_mu"         :: "[decl,decls,'a pred] => 'a pred"    ("mu _ '(_') _ ;")
    49   "_mudec"      :: "[decl,decls] => 'a pred"            ("mu _ '(_') ;")
    50   "_nu"         :: "[decl,decls,'a pred] => 'a pred"    ("nu _ '(_') _ ;")
    51   "_nudec"      :: "[decl,decls] => 'a pred"            ("nu _ '(_') ;")
    52   "_fun"        :: "[decl,decls,'a pred] => 'a pred"    ("_ '(_') _ ;")
    53   "_dec"        :: "[decl,decls] => 'a pred"            ("_ '(_') ;")
    54 
    55   "_Ex"         :: "[decl,idts,'a pred] => 'a pred"     ("'((3exists _ _./ _)')")
    56   "_All"        :: "[decl,idts,'a pred] => 'a pred"     ("'((3forall _ _./ _)')")
    57 
    58   "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3mu _./ _)" 1000)
    59   "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3nu _./ _)" 1000)
    60 
    61   "_case_syntax":: "['a, cases_syn] => 'b"              ("(case*_* / _ / esac*)" 10)
    62   "_case1"      :: "['a, 'b] => case_syn"               ("(2*= _ :/ _;)" 10)
    63   ""            :: "case_syn => cases_syn"              ("_")
    64   "_case2"      :: "[case_syn, cases_syn] => cases_syn" ("_/ _")
    65 
    66 (*Terms containing a case statement must be post-processed with the
    67   ML function transform_case. There, all asterikses before the "="
    68   will be replaced by the expression between the two asterisks
    69   following "case" and the asterisk after esac will be deleted *)
    70 
    71 oracle mc_mucke_oracle ("term") =
    72   mk_mc_mucke_oracle
    73 
    74 ML {*
    75 (* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
    76    it yields innermost one. If no Mu term is present, search_mu yields NONE
    77 *)
    78 
    79 (* extended for treatment of nu (TH) *)
    80 fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = 
    81 	(case (search_mu t2) of
    82 	      SOME t => SOME t 
    83 	    | NONE => SOME ((Const("MuCalculus.mu",tp)) $ t2))
    84   | search_mu ((Const("MuCalculus.nu",tp)) $ t2) =
    85         (case (search_mu t2) of
    86               SOME t => SOME t
    87             | NONE => SOME ((Const("MuCalculus.nu",tp)) $ t2))
    88   | search_mu (t1 $ t2) = 
    89 	(case (search_mu t1) of
    90 	      SOME t => SOME t 
    91 	    | NONE     => search_mu t2)
    92   | search_mu (Abs(_,_,t)) = search_mu t
    93   | search_mu _ = NONE;
    94 
    95 
    96 
    97 
    98 (* seraching a variable in a term. Used in move_mus to extract the
    99    term-rep of var b in hthm *)
   100 
   101 fun search_var s t =
   102 case t of
   103      t1 $ t2 => (case (search_var s t1) of
   104 		             SOME tt => SOME tt |
   105 			     NONE => search_var s t2) |
   106      Abs(_,_,t) => search_var s t |
   107      Var((s1,_),_) => if s = s1 then SOME t else NONE |
   108      _ => NONE;
   109 	
   110 
   111 (* function move_mus:
   112    Mucke can't deal with nested Mu terms. move_mus i searches for 
   113    Mu terms in the subgoal i and replaces Mu terms in the conclusion
   114    by constants and definitions in the premises recursively.
   115 
   116    move_thm is the theorem the performs the replacement. To create NEW
   117    names for the Mu terms, the indizes of move_thm are incremented by
   118    max_idx of the subgoal.
   119 *)
   120 
   121 local
   122 
   123   val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
   124 	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
   125 		     REPEAT (resolve_tac prems 1)]);
   126 
   127   val sig_move_thm = Thm.theory_of_thm move_thm;
   128   val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
   129   val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
   130 
   131 in
   132 
   133 fun move_mus i state =
   134 let val sign = Thm.theory_of_thm state;
   135     val (subgoal::_) = Library.drop(i-1,prems_of state);
   136     val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
   137     val redex = search_mu concl;
   138     val idx = let val t = #maxidx (rep_thm state) in 
   139 	      if t < 0 then 1 else t+1 end;
   140 in
   141 case redex of
   142      NONE => all_tac state |
   143      SOME redexterm => 
   144 	let val Credex = cterm_of sign redexterm;
   145 	    val aiCterm = 
   146 		cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm));
   147 	    val inst_move_thm = cterm_instantiate 
   148 				[(bCterm,Credex),(aCterm,aiCterm)] move_thm;
   149 	in
   150             ((rtac inst_move_thm i) THEN (dtac eq_reflection i) 
   151 		THEN (move_mus i)) state
   152 	end
   153 end;
   154 end;
   155 
   156 
   157 fun call_mucke_tac i state =
   158 let val thy = Thm.theory_of_thm state;
   159     val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
   160 in 
   161 (cut_facts_tac [OraAss] i) state
   162 end;
   163 
   164 
   165 (* transforming fun-defs into lambda-defs *)
   166 
   167 val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
   168  by (rtac (extensional eq) 1);
   169 qed "ext_rl";
   170 
   171 infix cc;
   172 
   173 fun NONE cc xl = xl
   174   | (SOME x) cc xl = x::xl;
   175 
   176 fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z
   177   | getargs (x $ (Var ((y,_),_))) = y;
   178 
   179 fun getfun ((x $ y) $ z) = getfun (x $ y)
   180   | getfun (x $ _) = x;
   181 
   182 local
   183 
   184 fun delete_bold [] = []
   185 | delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
   186         then (let val (_::_::_::s) = xs in delete_bold s end)
   187         else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
   188                 then  (let val (_::_::_::s) = xs in delete_bold s end)
   189                 else (x::delete_bold xs));
   190 
   191 fun delete_bold_string s = implode(delete_bold (explode s));
   192 
   193 in
   194 
   195 (* extension with removing bold font (TH) *)
   196 fun mk_lam_def (_::_) _ _ = NONE  
   197   | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
   198   | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
   199     let val thy = theory_of_thm t;
   200 	val fnam = Sign.string_of_term thy (getfun LHS);
   201 	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
   202 	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
   203     in
   204 	SOME (prove_goal thy gl (fn prems =>
   205   		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
   206     end
   207 | mk_lam_def [] _ t= NONE; 
   208 
   209 fun mk_lam_defs ([]:thm list) = ([]: thm list) 
   210   | mk_lam_defs (t::l) = 
   211       (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l);
   212 
   213 end;
   214 
   215 
   216 (* first simplification, then model checking *)
   217 
   218 val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
   219 
   220 val pair_eta_expand_proc =
   221   Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
   222   (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
   223 
   224 val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
   225 
   226 
   227 (* the interface *)
   228 
   229 fun mc_mucke_tac defs i state =
   230   (case Library.drop (i - 1, Thm.prems_of state) of
   231     [] => no_tac state
   232   | subgoal :: _ =>
   233       EVERY [
   234         REPEAT (etac thin_rl i),
   235         cut_facts_tac (mk_lam_defs defs) i,
   236         full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
   237         move_mus i, call_mucke_tac i,atac i,
   238         REPEAT (rtac refl i)] state);
   239 
   240 (*check if user has mucke installed*)
   241 fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
   242 fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
   243 
   244 *}
   245 
   246 end