1 (*notation ( output) "prop" ("#_" [1000] 1000) *)

     2 notation ( output) "Trueprop" ("#_" [1000] 1000)

     3 

     4 lemma regularize_to_injection:

     5   shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"

     6   by(auto simp add: QUOT_TRUE_def)

     7 

     8 syntax

     9   "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)

    10 translations

    11   "\<exists>!!x\<in>A. P"  == "Bexeq A (%x. P)"

    12 

    13 

    14 (* Atomize infrastructure *)

    15 (* FIXME/TODO: is this really needed? *)

    16 (*

    17 lemma atomize_eqv:

    18   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"

    19 proof

    20   assume "A \<equiv> B"

    21   then show "Trueprop A \<equiv> Trueprop B" by unfold

    22 next

    23   assume *: "Trueprop A \<equiv> Trueprop B"

    24   have "A = B"

    25   proof (cases A)

    26     case True

    27     have "A" by fact

    28     then show "A = B" using * by simp

    29   next

    30     case False

    31     have "\<not>A" by fact

    32     then show "A = B" using * by auto

    33   qed

    34   then show "A \<equiv> B" by (rule eq_reflection)

    35 qed

    36 *)

    37 

    38 

    39 ML {*

    40   fun dest_cbinop t =

    41     let

    42       val (t2, rhs) = Thm.dest_comb t;

    43       val (bop, lhs) = Thm.dest_comb t2;

    44     in

    45       (bop, (lhs, rhs))

    46     end

    47 *}

    48 

    49 ML {*

    50   fun dest_ceq t =

    51     let

    52       val (bop, pair) = dest_cbinop t;

    53       val (bop_s, _) = Term.dest_Const (Thm.term_of bop);

    54     in

    55       if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))

    56     end

    57 *}

    58 

    59 ML {*

    60   fun split_binop_conv t =

    61     let

    62       val (lhs, rhs) = dest_ceq t;

    63       val (bop, _) = dest_cbinop lhs;

    64       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

    65       val [cmT, crT] = Thm.dest_ctyp cr2;

    66     in

    67       Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}

    68     end

    69 *}

    70 

    71 

    72 ML {*

    73   fun split_arg_conv t =

    74     let

    75       val (lhs, rhs) = dest_ceq t;

    76       val (lop, larg) = Thm.dest_comb lhs;

    77       val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

    78     in

    79       Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}

    80     end

    81 *}

    82 

    83 ML {*

    84   fun split_binop_tac n thm =

    85     let

    86       val concl = Thm.cprem_of thm n;

    87       val (_, cconcl) = Thm.dest_comb concl;

    88       val rewr = split_binop_conv cconcl;

    89     in

    90       rtac rewr n thm

    91     end

    92       handle CTERM _ => Seq.empty

    93 *}

    94 

    95 

    96 ML {*

    97   fun split_arg_tac n thm =

    98     let

    99       val concl = Thm.cprem_of thm n;

   100       val (_, cconcl) = Thm.dest_comb concl;

   101       val rewr = split_arg_conv cconcl;

   102     in

   103       rtac rewr n thm

   104     end

   105       handle CTERM _ => Seq.empty

   106 *}

   107 

   108 

   109 lemma trueprop_cong:

   110   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"

   111   by auto

   112 

   113 lemma list_induct_hol4:

   114   fixes P :: "'a list \<Rightarrow> bool"

   115   assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"

   116   shows "\<forall>l. (P l)"

   117   using a

   118   apply (rule_tac allI)

   119   apply (induct_tac "l")

   120   apply (simp)

   121   apply (metis)

   122   done

   123 

   124 ML {*

   125 val no_vars = Thm.rule_attribute (fn context => fn th =>

   126   let

   127     val ctxt = Variable.set_body false (Context.proof_of context);

   128     val ((_, [th']), _) = Variable.import true [th] ctxt;

   129   in th' end);

   130 *}

   131 

   132 (*lemma equality_twice:

   133   "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"

   134 by auto*)

   135 

   136 

   137 (*interpretation code *)

   138 (*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))

   139   val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;

   140   val eqn1i = Thm.prop_of (symmetric eqn1pre)

   141   val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;

   142   val eqn2i = Thm.prop_of (symmetric eqn2pre)

   143 

   144   val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));

   145   val exp_term = Morphism.term exp_morphism;

   146   val exp = Morphism.thm exp_morphism;

   147 

   148   val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN

   149     ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))

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

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

   152   val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),

   153     Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*)

   154 

   155 (*||> Local_Theory.theory (fn thy =>

   156       let

   157         val global_eqns = map exp_term [eqn2i, eqn1i];

   158         (* Not sure if the following context should not be used *)

   159         val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;

   160         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;

   161       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*)