1structure ctl2muTools =
2struct
3
4local
5
6open Globals HolKernel Parse
7
8open boolSyntax pairSyntax pairTools PairRules bossLib muTheory
9     muCheck ctlTheory ctl2muTheory Tactical Tactic Drule Rewrite
10     cearTheory ksTheory setLemmasTheory pred_setTheory boolTheory
11     Conv PrimitiveBddRules ksTools lazyTools lzPairRules muSyntax
12     commonTools
13
14(*fun mk_bool_var v = mk_var(v,``:bool``);
15fun mk_primed_bool_var v = mk_bool_var (v^"'");
16fun term_to_string2 t = with_flag (show_types,false) term_to_string t;
17*)
18val dpfx = "c2m_"
19
20in
21
22(* normalise ctl formula to only use constructors from the minimal set *)
23fun ctl_norm_CONV f = Rewrite.REWRITE_CONV [C_IMP2_def,B_IMP2_def,B_AND2_def,B_OR2_def,C_AND2_def,C_OR2_def,C_AX_def,C_AG_def,C_AU_def,C_EF_def,C_IMP_def,C_IFF_def,C_AF_def,B_IMP_def,B_IFF_def,C_OR_def,B_OR_def] f handle ex => (REFL f);
24
25local
26fun ctl2mu_aux  f (cons as (mu_t,mu_f,mu_ap,mu_rv,mu_neg,mu_conj,mu_disj,mu_dmd,mu_box,mu_mu,mu_nu)) =
27  let
28      val (opr,args) = HolKernel.strip_comb f;
29      val (name,ty) = dest_const opr;
30  in case name of
31         "B_PROP" => mu_ap(List.hd args) (* ``AP ^(List.hd args)``*)
32       | "B_NOT"  => mu_neg(ctl2mu_aux (List.hd args) cons) (* ``~^(ctl2mu_aux prop_type (List.hd args))``*)
33       | "B_AND"  => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
34                     in mu_conj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
35       (*``^(ctl2mu_aux prop_type f1) /\ ^(ctl2mu_aux prop_type f2)`` *)
36       | "B_OR"  => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
37                     in mu_disj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
38       (*``^(ctl2mu_aux prop_type f1) \/ ^(ctl2mu_aux prop_type f2)`` *)
39       | "B_TRUE" => mu_t
40       | "B_FALSE" => mu_neg(mu_t) (* as this is how B_FALSE is represented syntactically *)
41       | "C_BOOL" => ctl2mu_aux (List.hd args) cons
42       | "C_NOT"  => mu_neg(ctl2mu_aux (List.hd args) cons)
43       | "C_AND"  => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
44                     in mu_conj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
45       | "C_OR"  => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
46                     in mu_disj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
47       | "C_EX"   => mu_dmd dotacn  (ctl2mu_aux (List.hd args) cons) (*``<<".">> ^(ctl2mu_aux prop_type (List.hd args))``*)
48       (*| "O_AX"   => ``[["."]] ^(ctl2mu_aux prop_type (List.hd args))``*)
49       | "C_EU"   => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
50                     in mu_mu concRV (mu_disj (ctl2mu_aux f2 cons) (mu_conj (ctl2mu_aux f1 cons) (mu_dmd dotacn (mu_rv concRV))))  end
51       (*``mu "Q" .. ^(ctl2mu_aux prop_type f2) \/ (^(ctl2mu_aux prop_type f1)  /\ (<<".">> (RV "Q")))``*)
52       | "C_EG"   => mu_nu concRV (mu_conj (ctl2mu_aux (List.hd args) cons) (mu_dmd dotacn (mu_rv concRV)))
53       (*  ``nu "Q" .. ^(ctl2mu_aux prop_type (List.hd args)) /\ (<<".">> (RV "Q"))``*)
54       | _ => (print name; Raise Match)
55  end
56in
57fun ctl2mu f =
58    let val f' = rhs(concl (ctl_norm_CONV f))
59    in ctl2mu_aux f' (get_ty_cons (get_prop_type f)) end
60
61end
62
63val _ = set_trace "notify type variable guesses" 0;
64val ctl2mu_tm = ``ctl2mu$CTL2MU``
65val _ = set_trace "notify type variable guesses" 1;
66
67(* convert ctl formula to mu formula *)
68fun ctl2mu_CONV f =
69    let val jf = (fn _ => REWRITE_CONV [CTL2MU_def,BEXP2MU_def,C_IMP2_def,B_IMP2_def,B_AND2_def,B_OR2_def,C_AND2_def,C_OR2_def,C_AX_def,
70                                        C_AG_def,C_AU_def,C_EF_def,C_IMP_def,C_IFF_def,C_AF_def,B_IMP_def,B_IFF_def,C_OR_def,B_OR_def,
71                                        B_FALSE_def] (mk_comb(inst [alpha|->get_prop_type f] ctl2mu_tm,f)))
72    in mk_lthm (fn _ => (mk_eq(mk_comb(inst [alpha|->get_prop_type f] ctl2mu_tm,f),ctl2mu f),jf)) jf end
73
74
75(* convert ctl model to mu model *)
76fun ctl2muks_CONV Ithm Rthm cks_def =
77    let val _ = dbgTools.DEN dpfx "c2mks"(*DBG*)
78        val th1 = (ISPEC (rhs(concl cks_def)) ctl2muks_def)
79        val th2 = PURE_REWRITE_RULE [SYM cks_def,combinTheory.K_THM,kripke_structure_accfupds] th1
80        val th3 =  CONV_RULE (RHS_CONV (T_CONV (PURE_REWRITE_CONV [SYM Rthm]))) th2
81        val _ = dbgTools.DTH (dpfx^"c2mks_th3") th3 (*DBG*)
82        val th4 = CONV_RULE (RHS_CONV (S0_CONV (PURE_REWRITE_CONV [SYM Ithm]))) th3
83        val _ = dbgTools.DTH (dpfx^"c2mks_th4") th4 (*DBG*)
84        val th5 = CONV_RULE (RHS_CONV (S0_CONV lzPETA_CONV)) th4
85        val th6 = CONV_RULE (RHS_CONV (T_CONV (ABS_CONV lzPETA_CONV))) th5
86        val _ = dbgTools.DEX dpfx "c2mks"(*DBG*)
87    in th5 end
88
89end
90end
91