2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "../../Attic/Prove"

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../../Attic/Prove"

   123 ML {* 

   123 local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]

   124 fun define_quotient_type args tac ctxt =

   124   (rtac @{thm alpha1_equivp(1)} 1) *}

   125 let

   126   val mthd = Method.SIMPLE_METHOD tac

   127   val mthdt = Method.Basic (fn _ => mthd)

   128   val bymt = Proof.global_terminal_proof (mthdt, NONE)

   129 in

   130   bymt (Quotient_Type.quotient_type args ctxt)

   131 end

   132 *}

   133 

   134 local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] 

   135   (rtac @{thm alpha1_equivp(1)} 1)

   136 *}

   148 

   136 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} @{term fv_rtrm1}

   149 ML {*

   137   (fn _ => fv_rsp_tac @{thms alpha_rtrm1_alpha_bp.inducts} @{thms fv_rtrm1_fv_bp.simps} 1) *}

   150 fun const_rsp const lthy =

   138 local_setup {* prove_const_rsp @{binding rVr1_rsp} @{term rVr1}

   151 let

   139   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   152   val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)

   140 local_setup {* prove_const_rsp @{binding rAp1_rsp} @{term rAp1}

   153   val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);

   141   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   154 in

   142 local_setup {* prove_const_rsp @{binding rLm1_rsp} @{term rLm1}

   155   HOLogic.mk_Trueprop (rel $ const $ const)

   143   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   156 end

   144 local_setup {* prove_const_rsp @{binding rLt1_rsp} @{term rLt1}

   157 *}

   145   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   158 

   146 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}

   159 (*local_setup {*

   147   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}

   160 snd o Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), @{thms refl}) *} *)

   161  

   162 prove fv_rtrm1_rsp': {* const_rsp @{term fv_rtrm1} @{context} *}

   163 by (tactic {*

   164   (rtac @{thm fun_rel_id} THEN'

   165   eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW

   166   asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *})

   167 

   168 

   169 lemmas fv_rtrm1_rsp = apply_rsp'[OF fv_rtrm1_rsp']

   170 

   171 (* We need this since 'prove' doesn't support attributes *)

   172 lemma [quot_respect]: "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"

   173   by (rule fv_rtrm1_rsp')

   174 

   175 ML {*

   176 fun contr_rsp_tac inj rsp equivps =

   177 let

   178   val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps

   179 in

   180   REPEAT o rtac @{thm fun_rel_id} THEN'

   181   simp_tac (HOL_ss addsimps inj) THEN'

   182   (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW

   183   (asm_simp_tac HOL_ss THEN_ALL_NEW (

   184    rtac @{thm exI[of _ "0 :: perm"]} THEN'

   185    asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @

   186      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))

   187   ))

   188 end

   189 *}

   190 

   191 ML {*

   192 fun remove_alls trm =

   193 let

   194   val fs = rev (map Free (strip_all_vars trm))

   195 in

   196   subst_bounds (fs, (strip_all_body trm))

   197 end

   198 *}

   199 

   200 ML {*

   201 fun rsp_goal thy trm =

   202 let

   203   val goalstate = Goal.init (cterm_of thy trm);

   204   val tac = REPEAT o rtac @{thm fun_rel_id};

   205 in

   206   case (SINGLE (tac 1) goalstate) of

   207     NONE => error "rsp_goal failed"

   208   | SOME th => remove_alls (term_of (cprem_of th 1))

   209 end

   210 *}

   211 

   212 prove rAp1_rsp': {* rsp_goal @{theory} (const_rsp @{term rAp1} @{context}) *}

   213 by (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})

   214 

   215 thm apply_rsp'[OF apply_rsp'[OF rAp1_rsp']]

   216 

   217 

   218 lemma [quot_respect]:

   219  "(op = ===> alpha_rtrm1) rVr1 rVr1"

   220  "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"

   221  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"

   222  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"

   223 apply (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+

   224 done

   225 

   252 lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]

   170 lemmas

   253 

   171     fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]

   254 lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]

   172 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]

   255 

   173 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   256 lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   395 

   312 local_setup  {* define_quotient_type 

   396 quotient_type

   313   [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})),

   397   trm2 = rtrm2 / alpha_rtrm2

   314    (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))]

   398 and

   315   ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *}

   399   assign = rassign / alpha_rassign

   400   by (rule alpha2_equivp(1)) (rule alpha2_equivp(2))