Add combined binder_inductive command for POPL submission

Author: jvanbruegge

Tools/binder_inductive.ML

@@ -1,6 +1,7 @@
 signature BINDER_INDUCTIVE =
 sig
-
+  val binder_inductive_cmd: (string * (string * string list) list option) * (string list option * string list option)
+    -> local_theory -> Proof.state;
 end
 
 structure Binder_Inductive : BINDER_INDUCTIVE =
@@ -991,7 +992,7 @@ val binder_inductive_parser = Parse.name -- Scan.option (
   ) -- parse_perm_supps
 
 val _ =
-  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>binder_inductive\<close> "derive strengthened induction theorems for inductive predicates"
+  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>binder_inductive_split\<close> "derive strengthened induction theorems for inductive predicates"
     (binder_inductive_parser >> binder_inductive_cmd);
 
 end

Tools/binder_inductive_combined.ML

@@ -0,0 +1,20 @@
+structure Binder_Inductive_Combined =
+struct
+
+fun ind_decl co args =
+  let
+    val names = map (fn (x, _, _) => x) (fst (Parse.vars args));
+    val (inductive, rest) = Inductive.gen_ind_decl Inductive.add_ind_def co args;
+  in (fn lthy =>
+    let
+      val lthy = snd (Local_Theory.begin_nested lthy);
+      val lthy = inductive lthy;
+      val (lthy, old_lthy) = `Local_Theory.end_nested lthy;
+      val state = Binder_Inductive.binder_inductive_cmd ((Binding.name_of (hd names), NONE), (NONE, NONE)) lthy
+    in state end, rest) end;
+
+val _ =
+  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>binder_inductive\<close> "derive strengthened induction theorems for inductive predicates"
+    (ind_decl false);
+
+end

thys/Infinitary_FOL/InfFOL.thy

@@ -342,16 +342,14 @@ qed
 lemma Int_Diff_empty: "A \<inter> (B - C) = {} \<Longrightarrow> A \<inter> C = {} \<Longrightarrow> A \<inter> B = {}"
 by blast
 
-inductive deduct :: "ifol set\<^sub>k \<Rightarrow> ifol \<Rightarrow> bool" (infix "\<turnstile>" 100) where
+binder_inductive deduct :: "ifol set\<^sub>k \<Rightarrow> ifol \<Rightarrow> bool" (infix "\<turnstile>" 100) where
   Hyp: "f \<in>\<^sub>k \<Delta> \<Longrightarrow> \<Delta> \<turnstile> f"
 | ConjI: "(\<And>f. f \<in>\<^sub>k\<^sub>1 F \<Longrightarrow> \<Delta> \<turnstile> f) \<Longrightarrow> \<Delta> \<turnstile> Conj F"
 | ConjE: "\<lbrakk> \<Delta> \<turnstile> Conj F ; f \<in>\<^sub>k\<^sub>1 F \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> f"
 | NegI: "\<Delta>,f \<turnstile> \<bottom> \<Longrightarrow> \<Delta> \<turnstile> Neg f"
 | NegE: "\<lbrakk> \<Delta> \<turnstile> Neg f ; \<Delta> \<turnstile> f \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> \<bottom>"
 | AllI: "\<lbrakk> \<Delta> \<turnstile> f ; set\<^sub>k\<^sub>2 V \<inter> \<Union>(FFVars_ifol' ` set\<^sub>k \<Delta>) = {} \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> All V f"
 | AllE: "\<lbrakk> \<Delta> \<turnstile> All V f ; supp \<rho> \<subseteq> set\<^sub>k\<^sub>2 V \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> f\<lbrakk>\<rho>\<rbrakk>"
-
-binder_inductive deduct
   subgoal for R B \<sigma> x1 x2
     unfolding induct_rulify_fallback split_beta
     apply (elim disj_forward exE)

thys/Infinitary_Lambda_Calculus/ILC_Beta.thy

@@ -18,13 +18,11 @@ lemma small_Tsupp: "small (Tsupp t1 t2)"
 lemma Tvars_dsset: "(Tsupp t1 t2 - dsset xs) \<inter> dsset xs = {}" "|Tsupp t1 t2 - dsset xs| <o |UNIV::ivar set|"
 apply auto by (meson card_of_minus_bound small_Tsupp small_def)
 
-inductive istep :: "itrm \<Rightarrow> itrm \<Rightarrow> bool" where
+binder_inductive istep :: "itrm \<Rightarrow> itrm \<Rightarrow> bool" where
   Beta: "istep (iApp (iLam xs e1) es2) (itvsubst (imkSubst xs es2) e1)"
 | iAppL: "istep e1 e1' \<Longrightarrow> istep (iApp e1 es2) (iApp e1' es2)"
 | iAppR: "istep (snth es2 i) e2' \<Longrightarrow> istep (iApp e1 es2) (iApp e1 (supd es2 i e2'))"
 | Xi: "istep e e' \<Longrightarrow> istep (iLam xs e) (iLam xs e')"
-
-binder_inductive istep
   subgoal for R B \<sigma> x1 x2
     apply (elim disj_forward exE conjE)
     subgoal for xs e1 es2

thys/Infinitary_Lambda_Calculus/ILC_affine.thy

@@ -10,7 +10,7 @@ begin
 lemma Tvars_dsset: "(FFVars t - dsset xs) \<inter> dsset xs = {}" "|FFVars t - dsset xs| <o |UNIV::ivar set|"
 apply auto using card_of_minus_bound iterm.set_bd_UNIV by blast
 
-inductive affine  :: "itrm \<Rightarrow> bool" where
+binder_inductive affine  :: "itrm \<Rightarrow> bool" where
  iVar[simp,intro!]: "affine (iVar x)"
 |iLam: "affine e \<Longrightarrow> affine (iLam xs e)"
 |iApp:
@@ -20,8 +20,6 @@ inductive affine  :: "itrm \<Rightarrow> bool" where
  (\<And>i j. i \<noteq> j \<Longrightarrow> FFVars (snth es2 i) \<inter> FFVars (snth es2 j) = {})
  \<Longrightarrow>
  affine (iApp e1 es2)"
-
-binder_inductive affine
   unfolding isPerm_def induct_rulify_fallback
   subgoal for R B \<sigma> t
     apply(elim disjE)

thys/MRBNF_Recursor.thy

@@ -2,6 +2,7 @@ theory MRBNF_Recursor
   imports MRBNF_FP
   keywords "binder_datatype" :: thy_defn
     and "binder_inductive" :: thy_goal_defn
+    and "binder_inductive_split" :: thy_goal_defn
     and "binds"
 begin
 
@@ -14,6 +15,7 @@ context begin
 ML_file \<open>../Tools/binder_induction.ML\<close>
 end
 ML_file \<open>../Tools/binder_inductive.ML\<close>
+ML_file \<open>../Tools/binder_inductive_combined.ML\<close>
 
 typedecl ('a, 'b) var_selector (infix "::" 999)
 

thys/POPLmark/SystemFSub.thy

@@ -276,7 +276,7 @@ declare ty.intros[intro]
 lemma ty_fresh_extend: "\<Gamma>, x <: U \<turnstile> S <: T \<Longrightarrow> x \<notin> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<and> x \<notin> FFVars_typ U"
   by (metis (no_types, lifting) UnE fst_conv snd_conv subsetD wf_ConsE wf_FFVars wf_context)
 
-binder_inductive ty
+binder_inductive_split ty
   subgoal for R B \<sigma> \<Gamma> T1 T2
     unfolding split_beta
     by (elim disj_forward exE)

thys/Pi_Calculus/Pi_Transition_Early.thy

@@ -2,15 +2,6 @@ theory Pi_Transition_Early
   imports Pi_Transition_Common
 begin
 
-inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
-  InpE: "trans (Inp a x P) (Finp a y (P[y/x]))"
-| ComLeftE: "\<lbrakk> trans P (Finp a x P') ; trans Q (Fout a x Q') \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Tau (P' \<parallel> Q'))"
-| CloseLeftE: "\<lbrakk> trans P (Finp a x P') ; trans Q (Bout a x Q') ; x \<notin> {a} \<union> FFVars P \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Tau (Res x (P' \<parallel> Q')))"
-| Open: "\<lbrakk> trans P (Fout a x P') ; a \<noteq> x \<rbrakk> \<Longrightarrow> trans (Res x P) (Bout a x P')"
-| ScopeFree: "\<lbrakk> trans P (Cmt \<alpha> P') ; fra \<alpha> ; x \<notin> ns \<alpha> \<rbrakk> \<Longrightarrow> trans (Res x P) (Cmt \<alpha> (Res x P'))"
-| ScopeBound: "\<lbrakk> trans P (Bout a x P') ; y \<notin> {a, x} ; x \<notin> FFVars P \<union> {a} \<rbrakk> \<Longrightarrow> trans (Res y P) (Bout a x (Res y P'))"
-| ParLeft: "\<lbrakk> trans P (Cmt \<alpha> P') ; bns \<alpha> \<inter> (FFVars P \<union> FFVars Q) = {} \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Cmt \<alpha> (P' \<parallel> Q))"
-
 (*
 lemma "B = bvars \<alpha>' \<Longrightarrow> P = Paa \<parallel> Qaa \<Longrightarrow> Q = Cmt \<alpha>' (P'a \<parallel> Qaa) \<Longrightarrow> R Paa (Cmt \<alpha>' P'a) \<Longrightarrow>
    bvars \<alpha>' \<inter> (FFVars Paa \<union> FFVars Qaa) = {} \<Longrightarrow>
@@ -22,7 +13,14 @@ lemma "B = bvars \<alpha>' \<Longrightarrow> P = Paa \<parallel> Qaa \<Longright
   apply (cases \<alpha>'; hypsubst_thin; unfold Cmt.simps bns.simps)
 *)
 
-binder_inductive trans
+binder_inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
+  InpE: "trans (Inp a x P) (Finp a y (P[y/x]))"
+| ComLeftE: "\<lbrakk> trans P (Finp a x P') ; trans Q (Fout a x Q') \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Tau (P' \<parallel> Q'))"
+| CloseLeftE: "\<lbrakk> trans P (Finp a x P') ; trans Q (Bout a x Q') ; x \<notin> {a} \<union> FFVars P \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Tau (Res x (P' \<parallel> Q')))"
+| Open: "\<lbrakk> trans P (Fout a x P') ; a \<noteq> x \<rbrakk> \<Longrightarrow> trans (Res x P) (Bout a x P')"
+| ScopeFree: "\<lbrakk> trans P (Cmt \<alpha> P') ; fra \<alpha> ; x \<notin> ns \<alpha> \<rbrakk> \<Longrightarrow> trans (Res x P) (Cmt \<alpha> (Res x P'))"
+| ScopeBound: "\<lbrakk> trans P (Bout a x P') ; y \<notin> {a, x} ; x \<notin> FFVars P \<union> {a} \<rbrakk> \<Longrightarrow> trans (Res y P) (Bout a x (Res y P'))"
+| ParLeft: "\<lbrakk> trans P (Cmt \<alpha> P') ; bns \<alpha> \<inter> (FFVars P \<union> FFVars Q) = {} \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Cmt \<alpha> (P' \<parallel> Q))"
   subgoal for R B \<sigma> x1 x2
     apply simp
     apply (elim disj_forward)

thys/Pi_Calculus/Pi_Transition_Late.thy

@@ -2,16 +2,14 @@ theory Pi_Transition_Late
   imports Pi_Transition_Common
 begin
 
-inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
+binder_inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
   InpL: "trans (Inp a x P) (Binp a x P)"
 | ComLeftL: "\<lbrakk> trans P (Binp a x P') ; trans Q (Fout a y Q') \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Tau ((P'[y/x]) \<parallel> Q'))"
 | CloseLeftL: "\<lbrakk> trans P (Binp a x P') ; trans Q (Bout a x Q') \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Tau (Res x (P' \<parallel> Q')))"
 | Open: "\<lbrakk> trans P (Fout a x P') ; a \<noteq> x \<rbrakk> \<Longrightarrow> trans (Res x P) (Bout a x P')"
 | ScopeFree: "\<lbrakk> trans P (Cmt \<alpha> P') ; fra \<alpha> ; x \<notin> ns \<alpha> \<rbrakk> \<Longrightarrow> trans (Res x P) (Cmt \<alpha> (Res x P'))"
 | ScopeBound: "\<lbrakk> trans P (Bout a x P') ; y \<notin> {a, x} ; x \<notin> FFVars P \<union> {a} \<rbrakk> \<Longrightarrow> trans (Res y P) (Bout a x (Res y P'))"
 | ParLeft: "\<lbrakk> trans P (Cmt \<alpha> P') ; bns \<alpha> \<inter> (FFVars P \<union> FFVars Q) = {} \<rbrakk> \<Longrightarrow> trans (P \<parallel> Q) (Cmt \<alpha> (P' \<parallel> Q))"
-
-binder_inductive trans
   subgoal for R B \<sigma> x1 x2
     apply simp
     apply (elim disj_forward)

thys/Pi_Calculus/Pi_cong.thy

@@ -9,7 +9,7 @@ lemma fresh: "\<exists>xx. xx \<notin> Tsupp (t :: trm) t2"
   by (metis (no_types, lifting) exists_var finite_iff_le_card_var term.Un_bound term.set_bd_UNIV)
 
 (* Structural congurence *)
-inductive cong :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<equiv>\<^sub>\<pi>)" 40) where
+binder_inductive cong :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<equiv>\<^sub>\<pi>)" 40) where
   "P = Q \<Longrightarrow> P \<equiv>\<^sub>\<pi> Q"
 | "Par P Q \<equiv>\<^sub>\<pi> Par Q P"
 | "Par (Par P Q) R \<equiv>\<^sub>\<pi> Par P (Par Q R)"
@@ -18,8 +18,6 @@ inductive cong :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<equiv>\<
 | "Res x Zero \<equiv>\<^sub>\<pi> Zero"
 | "Bang P \<equiv>\<^sub>\<pi> Par P (Bang P)"
 | cong_3: "x \<notin> FFVars Q \<Longrightarrow> Res x (Par P Q) \<equiv>\<^sub>\<pi> Par (Res x P) Q"
-
-binder_inductive cong
   subgoal for R B \<sigma> x1 x2
     apply simp
     by (elim disj_forward case_prodE)
@@ -55,13 +53,11 @@ proof-
   thus ?thesis by auto
 qed
 
-inductive trans :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<rightarrow>)" 30) where
+binder_inductive trans :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<rightarrow>)" 30) where
   "Par (Out x z P) (Inp x y Q) \<rightarrow> Par P (usub Q z y)"
 | "P \<rightarrow> Q \<Longrightarrow> Par P R \<rightarrow> Par P Q"
 | "P \<rightarrow> Q \<Longrightarrow> Res x P \<rightarrow> Res x Q"
 | "P \<equiv>\<^sub>\<pi> P' \<Longrightarrow> P' \<rightarrow> Q' \<Longrightarrow> Q' \<equiv>\<^sub>\<pi> Q \<Longrightarrow> P \<rightarrow> Q"
-
-binder_inductive trans
   subgoal for R B \<sigma> x1 x2
     apply simp
     apply (elim disj_forward exE)