Stage work on pi-calculus

examples/formal-languages/pi-calculus/pi_agentScript.sml

@@ -18,17 +18,17 @@ val _ = new_theory "pi_agent";
 
    Nominal_datatype :
 
-           name = Name 'free
+           name = Name string
 
            pi   = Nil                      (* 0 *)
                 | Tau pi                   (* tau.P *)
-                | Input name 'bound pi     (* a(x).P *)
+                | Input name ''name pi     (* a(x).P *)
                 | Output name name pi      (* {a}b.P *)
                 | Match name name pi       (* [a == b] P *)
                 | Mismatch name name pi    (* [a <> b] P *)
                 | Sum pi pi                (* P + Q *)
                 | Par pi pi                (* P | Q *)
-                | Res 'bound pi            (* nu x. P *)
+                | Res ''name pi            (* nu x. P *)
 
        residual = TauR pi
                 | InputR name 'bound pi      (* (Bound) input *)
@@ -440,8 +440,8 @@ val {tpm_thm, term_REP_tpm, t_pmact_t, tpm_t} =
                         genind_term_REP = genind_term_REP1};
 
 Theorem tpm_thm[allow_rebind] =
-        tpm_thm |> REWRITE_RULE [GSYM term_REP_npm, GSYM Input_def, Output_def', Match_def',
-                                 Mismatch_def'];
+        tpm_thm |> REWRITE_RULE [GSYM term_REP_npm, GSYM Input_def, Output_def',
+                                 Match_def', Mismatch_def'];
 
 Theorem tpm_eqr :
     t = tpm pi u <=> tpm (REVERSE pi) t = (u :pi)
@@ -711,7 +711,6 @@ Theorem FV_rpm[simp] = “x IN FV (rpm p (t :residual))”
     term induction
    ---------------------------------------------------------------------- *)
 
-(*
 fun genit th = let
   val (_, args) = strip_comb (concl th)
   val (tm, x) = case args of [x,y] => (x,y) | _ => raise Fail "Bind"
@@ -726,21 +725,26 @@ val LIST_REL_NIL = listTheory.LIST_REL_NIL;
 
 val term_ind =
     bvc_genind
-        |> INST_TYPE [alpha |-> rep_t, beta |-> “:unit”]
+        |> INST_TYPE [alpha |-> glam_rep_t, beta |-> gvar_rep_t]
         |> Q.INST [‘vp’ |-> ‘^vp’, ‘lp’ |-> ‘^lp’]
         |> SIMP_RULE std_ss [LIST_REL_CONS1, RIGHT_AND_OVER_OR,
                              LEFT_AND_OVER_OR, DISJ_IMP_THM, LIST_REL_NIL]
         |> Q.SPECL [‘\n t0 x. Q t0 x’, ‘fv’]
-        |> UNDISCH |> Q.SPEC ‘0’ |> DISCH_ALL
+        |> UNDISCH |> Q.SPEC ‘1’ |> DISCH_ALL
         |> SIMP_RULE (std_ss ++ DNF_ss)
                      [sumTheory.FORALL_SUM, supp_listpm,
                       IN_UNION, NOT_IN_EMPTY, oneTheory.FORALL_ONE,
-                      genind_exists, LIST_REL_CONS1, LIST_REL_NIL]
-        |> Q.INST [‘Q’ |-> ‘\t. P (^term_ABS_t t)’]
-        |> SIMP_RULE std_ss [GSYM var_def, prefix_def',
-                             sum_def', par_def', restr_def', relab_def',
-                             GSYM rec_def, absrep_id]
-        |> SIMP_RULE (srw_ss()) [GSYM supp_tpm]
+                      genind_exists0,
+                      genind_exists1,
+                      genind_exists2,
+                      LIST_REL_CONS1, LIST_REL_NIL]
+        |> Q.INST [‘Q’ |-> ‘\t. P (^term_ABS_t1 t)’]
+        |> SIMP_RULE std_ss [absrep_id1,
+                             GSYM Name_def,
+                             Nil_def', Tau_def', GSYM Input_def,
+                             Output_def', Match_def', Mismatch_def',
+                             Sum_def', Par_def', GSYM Res_def]
+        |> SIMP_RULE (srw_ss()) [GSYM supp_tpm, GSYM supp_npm]
         |> elim_unnecessary_atoms {finite_fv = FINITE_FV}
                                   [ASSUME “!x:'c. FINITE (fv x:string set)”]
         |> SPEC_ALL |> UNDISCH
@@ -751,8 +755,9 @@ fun mkX_ind th = th |> Q.SPECL [‘\t x. Q t’, ‘\x. X’]
                     |> Q.INST [‘Q’ |-> ‘P’] |> Q.GEN ‘P’;
 
 (* NOTE: not recommended unless in generated theorems *)
-Theorem nc_INDUCTION[local] = mkX_ind term_ind
+Theorem nc_INDUCTION = mkX_ind term_ind
 
+(*
 (* The recommended induction theorem containing correctly named
    binding variables (L, rf, y, etc.)
  *)