52     if null avoid then [] else [vc_goal]

    60     if null avoid then [] else [vc_goal, finite_goal]

   160      

   174 

   163         |> flag ? (simplify (HOL_basic_ss addsimps @{thms permute_minus_cancel}))

   177         |> flag ? (eqvt_srule context)

   178 

   179       val _ = tracing ("prm':" ^ @{make_string} prm')

   165       simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def })) 1

   181       print_tac "start helper"

   182       THEN asm_full_simp_tac (HOL_ss addsimps (prm' :: @{thms induct_forall_def})) 1

   183       THEN print_tac "final helper"

   181       fun tac1 prm = helper_tac true prm p context

   199       fun tac1 prm = helper_tac true prm p context 

   192       EVERY1 [rtac prem', RANGE (map (SUBGOAL o select) prems) ]

   210       EVERY1 [eqvt_stac ctxt, rtac prem', RANGE (map (SUBGOAL o select) prems) ]

   198 fun fresh_thm ctxt fresh_thms p c prms avoid_trm =

   216 fun fresh_thm ctxt user_thm p c concl_args avoid_trm =

   203       mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) prms))) (Bound 0)

   221       mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) concl_args))) (Bound 0)

   207     val _ = tracing ("fresh goal: " ^ Syntax.string_of_term ctxt fresh_goal)

   225     val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ 

   226              @{thms fresh_star_Pair fresh_star_permute_iff}

   227     val simp = asm_full_simp_tac (HOL_ss addsimps ss)

   210       (K (HEADGOAL (rtac @{thm at_set_avoiding2})))

   230       (K (HEADGOAL (rtac @{thm at_set_avoiding2} 

   211   end

   231           THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp])))

   212 *}

   232   end

   213 

   233 *}

   214 ML {*

   234 

   215 fun binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt = 

   235 ML {* 

   216   Subgoal.FOCUS (fn {context, params, ...} =>

   236 val supp_perm_eq' = 

   237   @{lemma "supp (p \<bullet> x) \<sharp>* q ==> p \<bullet> x == (q + p) \<bullet> x" by (simp add: supp_perm_eq)}

   238 val fresh_star_plus =

   239   @{lemma "(q \<bullet> (p \<bullet> x)) \<sharp>* c ==> ((q + p) \<bullet> x) \<sharp>* c" by (simp add: permute_plus)}

   240 *}

   241 

   242 ML {*

   243 fun binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt = 

   244   Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} =>

   218       val thy = ProofContext.theory_of context

   246       val thy = ProofContext.theory_of ctxt

   223       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 

   270       val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms 

   224       val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem

   271       val prem' = cterm_instantiate (intr_cvars ~~ qp_prms) prem

   225       val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm      

   272 

   226 

   273       val fprop' = eqvt_srule ctxt' fprop 

   227       val fthm = fresh_thm context fresh_thms (term_of p) (term_of c) (map term_of prms) avoid_trm'

   274       val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop'])

   275 

   276       (* for inductive-premises*)

   277       fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' 

   278 

   279       (* for non-inductive premises *)   

   280       fun tac2 prm =  

   281         EVERY' [ minus_permute_intro_tac (mk_cplus q p), 

   282                  eqvt_stac ctxt, 

   283                  helper_tac false prm (mk_cplus q p) ctxt' ]

   284 

   285       fun select prm (t, i) =

   286         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i

   287 

   288       val _ = tracing ("fthm:\n" ^ @{make_string} fthm)

   289       val _ = tracing ("fr_eqs:\n" ^ cat_lines (map @{make_string} fresh_eqs))

   290       val _ = tracing ("fprop:\n" ^ @{make_string} fprop)

   291       val _ = tracing ("fprop':\n" ^ @{make_string} fprop')

   292       val _ = tracing ("fperm:\n" ^ @{make_string} q)

   293       val _ = tracing ("prem':\n" ^ @{make_string} prem')

   294 

   295       val side_thm = Goal.prove ctxt' [] [] (term_of concl)

   296         (fn {context, ...} => 

   297            EVERY1 [ CONVERSION (expand_conv_bot context),

   298                     eqvt_stac context,

   299                     rtac prem',

   300                     RANGE (tac_fresh :: map (SUBGOAL o select) prems),

   301                     K (print_tac "GOAL") ])

   302         |> singleton (ProofContext.export ctxt' ctxt)        

   229       Skip_Proof.cheat_tac thy

   304       rtac side_thm 1

   230       (* EVERY1 [rtac prem'] *)  

   235 fun case_tac ctxt fresh_thms Ps (avoid, avoid_trm) intr_cvars param_trms prem =

   309 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =

   238     val tac2 = binder_tac prem intr_cvars param_trms Ps fresh_thms avoid avoid_trm ctxt

   312     val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt

   240     EVERY' [ rtac @{thm allI}, rtac @{thm allI}, eqvt_stac ctxt,

   314     EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ]

   241              if null avoid then tac1 else tac2 ]

   315   end

   242   end

   316 *}

   243 *}

   317 

   244 

   318 ML {*

   245 ML {*

   319 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args 

   246 fun prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms {prems, context} =

   320   {prems, context} =

   247   let

   321   let

   248     val cases_tac = map4 (case_tac context fresh_thms Ps) (avoids ~~avoid_trms) intr_cvars param_trms prems

   322     val cases_tac = 

   323       map7 (case_tac context Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args

   258 ML {*

   333 ML {* Local_Theory.note *}

   259 fun prove_strong_inductive rule_names avoids raw_induct intrs ctxt =

   334 

   335 ML {*

   336 fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt =

   314     fun after_qed ctxt_outside fresh_thms ctxt = 

   391     fun after_qed ctxt_outside user_thms ctxt = 

   316         val thms = Goal.prove ctxt [] ind_prems' ind_concl' 

   393         val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' 

   317           (prove_sinduct_tac raw_induct fresh_thms Ps avoids avoid_trms intr_cvars param_trms) 

   394         (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) 

   325         val _ = tracing ("RESULTS\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) thms))

   402         val qualified_thm_name = pred_names

   403           |> map Long_Name.base_name

   404           |> space_implode "_"

   405           |> (fn s => Binding.qualify false s (Binding.name "strong_induct"))

   406 

   407         val attrs = 

   408           [ Attrib.internal (K (Rule_Cases.consumes 1)),

   409             Attrib.internal (K (Rule_Cases.case_names rule_names)) ]

   410         val _ = tracing ("RESULTS\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) strong_ind_thms))

   411         val _ = tracing ("rule_names: " ^ commas rule_names)

   412         val _ = tracing ("pred_names: " ^ commas pred_names)

   328       end 

   415         |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms)    

   416         |> snd   

   417       end

   369     prove_strong_inductive rule_names avoid_trms raw_induct intrs ctxt

   458     prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt

   444   "valid []"

   535   v_Nil[intro]: "valid []"

   445 | "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"

   536 | v_Cons[intro]: "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"

   470 

   559 thm typing.strong_induct

   471 

   560 

   472 lemma

   561 abbreviation

   473   fixes c::"'a::fs"

   562   "sub_context" :: "(name \<times> ty) list \<Rightarrow> (name \<times> ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 

   474   assumes a: "\<Gamma> \<turnstile> t : T" 

   563 where

   475   and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"

   564   "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x, T) \<in> set \<Gamma>1 \<longrightarrow> (x, T) \<in> set \<Gamma>2"

   476   and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk> 

   565 

   477            \<Longrightarrow> P c \<Gamma> (App t1 t2) T2"

   566 text {* Now it comes: The Weakening Lemma *}

   478   and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>{atom x} \<sharp>* c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk> 

   567 

   479            \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"

   568 text {*

   480   shows "P c \<Gamma> t T"

   569   The first version is, after setting up the induction, 

   481 proof -

   570   completely automatic except for use of atomize. *}

   482   from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"

   571 

   483   proof (induct)

   572 lemma weakening_version2: 

   484     case (t_Var \<Gamma> x T p c)

   573   fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list"

   485     then show ?case

   574   and   t ::"lam"

   486       apply -

   575   and   \<tau> ::"ty"

   487       apply(perm_strict_simp)

   576   assumes a: "\<Gamma>1 \<turnstile> t : T"

   488       thm a1

   577   and     b: "valid \<Gamma>2" 

   489       apply(rule a1)

   578   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"

   490       apply(drule_tac p="p" in permute_boolI)

   579   shows "\<Gamma>2 \<turnstile> t : T"

   491       apply(perm_strict_simp add: permute_minus_cancel)

   580 using a b c

   492       apply(assumption)

   581 proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)

   493       apply(rotate_tac 1)

   582   case (t_Var \<Gamma>1 x T)  (* variable case *)

   494       apply(drule_tac p="p" in permute_boolI)

   583   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 

   495       apply(perm_strict_simp add: permute_minus_cancel)

   584   moreover  

   496       apply(assumption)

   585   have "valid \<Gamma>2" by fact 

   497       done

   586   moreover 

   498   next

   587   have "(x,T)\<in> set \<Gamma>1" by fact

   499     case (t_App \<Gamma> t1 T1 T2 t2 p c)

   588   ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto

   500     then show ?case

   589 next

   501       apply -

   590   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)

   502       apply(perm_strict_simp)

   591   have vc: "atom x \<sharp> \<Gamma>2" by fact   (* variable convention *)

   503       apply(rule a2)

   592   have ih: "\<lbrakk>valid ((x, T1) # \<Gamma>2); (x, T1) # \<Gamma>1 \<subseteq> (x, T1) # \<Gamma>2\<rbrakk> \<Longrightarrow> (x, T1) # \<Gamma>2 \<turnstile> t : T2" by fact

   504       apply(drule_tac p="p" in permute_boolI)

   593   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact

   505       apply(perm_strict_simp add: permute_minus_cancel)

   594   then have "(x, T1) # \<Gamma>1 \<subseteq> (x, T1) # \<Gamma>2" by simp

   506       apply(assumption)

   595   moreover

   507       apply(assumption)

   596   have "valid \<Gamma>2" by fact

   508       apply(rotate_tac 2)

   597   then have "valid ((x, T1) # \<Gamma>2)" using vc by (simp add: v_Cons)

   509       apply(drule_tac p="p" in permute_boolI)

   598   ultimately have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp

   510       apply(perm_strict_simp add: permute_minus_cancel)

   599   with vc show "\<Gamma>2 \<turnstile> Lam x t : T1 \<rightarrow> T2" by auto

   511       apply(assumption)

   600 qed (auto) (* app case *)

   512       apply(assumption)

   601 

   513       done

   602 lemma weakening_version1: 

   514   next

   603   fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list"

   515     case (t_Lam x \<Gamma> T1 t T2 p c)

   604   assumes a: "\<Gamma>1 \<turnstile> t : T" 

   516     then show ?case

   605   and     b: "valid \<Gamma>2" 

   517       apply -

   606   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"

   518       apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> 

   607   shows "\<Gamma>2 \<turnstile> t : T"

   519         supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")

   608 using a b c

   520       apply(erule exE)

   609 apply (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)

   521       apply(rule_tac t="p \<bullet> \<Gamma>" and  s="(q + p) \<bullet> \<Gamma>" in subst)

   610 apply (auto | atomize)+

   522       apply(simp only: permute_plus)

   611 done

   523       apply(rule supp_perm_eq)

   612 

   524       apply(simp add: supp_Pair fresh_star_Un)

   525       apply(rule_tac t="p \<bullet> Lam x t" and  s="(q + p) \<bullet> Lam x t" in subst)

   526       apply(simp only: permute_plus)

   527       apply(rule supp_perm_eq)

   528       apply(simp add: supp_Pair fresh_star_Un)

   529       apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)

   530       apply(simp only: permute_plus)

   531       apply(rule supp_perm_eq)

   532       apply(simp add: supp_Pair fresh_star_Un)

   533       (* apply(perm_simp) *) 

   534       apply(simp (no_asm) only: eqvts)

   535       apply(rule a3)

   536       apply(simp only: eqvts permute_plus)

   537       apply(rule_tac p="- (q + p)" in permute_boolE)

   538       apply(perm_strict_simp add: permute_minus_cancel)

   539       apply(assumption)

   540        apply(rule_tac p="- (q + p)" in permute_boolE)

   541       apply(perm_strict_simp add: permute_minus_cancel)

   542       apply(assumption)

   543       apply(perm_strict_simp)

   544       apply(simp only:)

   545       thm at_set_avoiding2

   546       apply(rule at_set_avoiding2)

   547       apply(simp add: finite_supp)

   548       apply(simp add: finite_supp)

   549       apply(simp add: finite_supp)

   550       apply(rule_tac p="-p" in permute_boolE)

   551       apply(perm_strict_simp add: permute_minus_cancel)

   552 	--"supplied by the user"

   553       apply(simp add: fresh_star_Pair)

   554       sorry

   555   qed

   556   then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" .

   557   then show "P c \<Gamma> t T" by simp

   558 qed

   559 

   560 *)