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