Remove outdated code from Commitment

thys/Pi_Calculus/Commitment.thy

@@ -2,48 +2,6 @@ theory Commitment
 imports Pi  "Prelim.Curry_LFP" "Binders.Generic_Barendregt_Enhanced_Rule_Induction"
 begin
 
-(*local_setup \<open>fn lthy =>
-let
-  val name1 = "commit_internal"
-  val name2 = "commit"
-  val T1 = @{typ "'var term"}
-  val T2 = @{typ "'var * 'var * 'var term +'var * 'var * 'var term + 'var * 'bvar * 'brec + 'var term + 'var * 'bvar * 'brec"}
-  val Xs = map dest_TFree []
-  val resBs = map dest_TFree [@{typ 'var}, @{typ 'bvar}, @{typ 'brec}, @{typ 'rec}]
-  val rel = [[([], [0])]]
-
-  fun flatten_tyargs Ass = subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
-  val qualify1 = Binding.prefix_name (name1 ^ "_pre_")
-  val qualify2 = Binding.prefix_name (name2 ^ "_pre_")
-
-  (* Step 1: Create pre-MRBNF *)
-  val ((mrbnf1, tys1), (accum, lthy)) = MRBNF_Comp.mrbnf_of_typ true MRBNF_Def.Smart_Inline qualify1 flatten_tyargs Xs []
-    [(dest_TFree @{typ 'var}, MRBNF_Def.Free_Var), (dest_TFree @{typ 'bvar}, MRBNF_Def.Bound_Var)] T1
-    ((MRBNF_Comp.empty_comp_cache, MRBNF_Comp.empty_unfolds), lthy)
-  val ((mrbnf2, tys2), (accum, lthy)) = MRBNF_Comp.mrbnf_of_typ true MRBNF_Def.Smart_Inline qualify2 flatten_tyargs Xs []
-    [(dest_TFree @{typ 'var}, MRBNF_Def.Free_Var), (dest_TFree @{typ 'bvar}, MRBNF_Def.Bound_Var)] T2
-    (accum, lthy);
-
-  val (tys, _, (mrbnfs as [mrbnf1, mrbnf2], (accum, lthy))) =
-      MRBNF_Comp.normalize_mrbnfs (K I) [] (map (map dest_TFree) [snd tys1, snd tys2])
-      [] [] (K (resBs @ Xs)) NONE [mrbnf1, mrbnf2] (accum, lthy);
-
-  (* Step 2: Seal the pre-MRBNF with a typedef *)
-  val ((mrbnf1, (Ds, info)), lthy) = MRBNF_Comp.seal_mrbnf I (snd accum) (Binding.name (name1 ^ "_pre")) true (fst tys1) [] mrbnf1 lthy
-  val ((mrbnf2, (Ds, info)), lthy) = MRBNF_Comp.seal_mrbnf I (snd accum) (Binding.name (name2 ^ "_pre")) true (fst tys2) [] mrbnf2 lthy
-
-  (* Step 3: Register the pre-MRBNF as a BNF in its live variables *)
-  val (bnf1, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf1 lthy
-  val (bnf2, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf2 lthy
-
-  (* Step 4: Create fixpoint of pre-MRBNF *)
-  val (res, lthy) = MRBNF_FP.construct_binder_fp MRBNF_Util.Least_FP [
-    ((name1, mrbnf1), 1), ((name2, mrbnf2), 1)
-  ] rel lthy;
-in lthy end
-\<close>*)
-print_theorems
-
 binder_datatype 'var commit =
     Finp 'var 'var "'var term"
   | Fout 'var 'var "'var term"
@@ -206,4 +164,4 @@ lemma fra_eqvt[simp]: "fra (map_action \<sigma> act) = fra act"
 lemma ns_map_action[simp]: "ns (map_action \<sigma> \<alpha>) = \<sigma> ` ns \<alpha>"
   by (cases \<alpha>) auto
 
-end
+end